Library Util
Require Import SfLib.
Require Import LibTactics.
Section Lists.
Lemma skipn_length: ∀ {A:Type} (l l': list A) n,
skipn n l = l' → length l' = length l - n.
Proof. induction l; destruct n; simpl; intros; subst; auto. Qed.
Lemma app_split3: ∀ {A:Type} n (l:list A),
length l > n →
∃ l1 a l2,
l = l1++[a]++l2 ∧ length l1 = n.
Proof.
intros.
case_eq (skipn n l); intros.
apply skipn_length in H0. simpl in H0. false. omega.
∃ (firstn n l) a l0.
split.
rewrite<- (firstn_skipn n l) at 1.
f_equal; auto.
rewrite firstn_length.
apply Min.min_l.
omega.
Qed.
Lemma count_occ_nIn: ∀ {A:Type} eq_dec (x:A) l,
¬In x l →
count_occ eq_dec l x = 0.
Proof.
induction l; simpl; intros; auto.
apply Decidable.not_or in H; destruct H.
destruct (eq_dec a x); subst; auto.
false.
Qed.
Lemma app_inv: ∀ {A:Type} (l1 l2 l3 l4: list A),
l1++l3 = l2++l4 →
length l2 = length l1 →
l2=l1 ∧ l4=l3.
Proof.
induction l1; destruct l2; simpl; intros; try solve [false]; auto.
inverts H0.
inverts H.
edestruct IHl1 as [??]; eauto.
subst; auto.
Qed.
End Lists.
Section SplitCombine.
Lemma combine_nil2: ∀ A B (l:list A),
@combine A B l nil = nil.
Proof. induction l; simpl; intros; auto. Qed.
Lemma split_combine': ∀ {A B:Type} l,
@combine A B (fst (split l)) (snd (split l)) = l.
Proof.
intros.
generalize (split_combine l); intros.
destruct (split l) as [l1 l2].
simpl; auto.
Qed.
Lemma fst_split: ∀ {A B:Type} (a:A) (b:B) l,
fst (let (la,lb):= split l in (a::la, b::lb)) = a::fst (split l).
Proof. simpl; intros; destruct (split l); reflexivity. Qed.
Lemma snd_split: ∀ {A B:Type} (a:A) (b:B) l,
snd (let (la,lb):= split l in (a::la, b::lb)) = b::snd (split l).
Proof. simpl; intros; destruct (split l); reflexivity. Qed.
Lemma fst_split_app: ∀ {A B:Type} (l1 l2: list (A×B)),
fst (split l1) ++ fst (split l2) = fst (split (l1++l2)).
Proof. induction l1; intros; simpl; auto; destruct a; do 2 rewrite fst_split; simpl; f_equal; auto. Qed.
Lemma snd_split_app: ∀ {A B:Type} (l1 l2: list (A×B)),
snd (split l1) ++ snd (split l2) = snd (split (l1++l2)).
Proof. induction l1; intros; simpl; auto; destruct a; do 2 rewrite snd_split; simpl; f_equal; auto. Qed.
Lemma combine_app: ∀ {A B:Type} (l1:list A) (l3:list B) l2 l4,
length l3 = length l1 →
combine (l1++l2) (l3++l4) = (combine l1 l3)++(combine l2 l4).
Proof.
induction l1; destruct l3; intros; auto.
inverts H.
inverts H.
inverts H.
simpl.
f_equal. eauto.
Qed.
Lemma in_split_l': ∀ {A B: Type} (l: list (A×B)) x,
In x (fst (split l)) → ∃ y, In (x,y) l.
Proof.
induction l; simpl; intros.
false.
destruct a. rewrite fst_split in H.
destruct H as [?|?]. subst a.
∃ b; auto.
destruct (IHl x) as [y ?]; auto.
∃ y; auto.
Qed.
End SplitCombine.
Section ListPairFun.
Definition list_pair_fun {A B C: Type} (f:A→B→C) l1 l2 := (map (fun (nd: A×B) ⇒ let (n,d):=nd in f n d) (combine l1 l2)).
Lemma list_pair_fun_comm: ∀ {A B: Type} (f:A→A→B) l1 l2,
(∀ a b, f a b = f b a) →
list_pair_fun f l1 l2 = list_pair_fun f l2 l1.
Proof. induction l1; destruct l2; unfold list_pair_fun; simpl; intros; auto; f_equal; eauto. Qed.
Lemma list_pair_fun_assoc: ∀ {A: Type} (f: A→A→A) l1 l2 l3,
(∀ a b c, f a (f b c) = f (f a b) c) →
list_pair_fun f l1 (list_pair_fun f l2 l3) = list_pair_fun f (list_pair_fun f l1 l2) l3.
Proof. induction l1; destruct l2; destruct l3; unfold list_pair_fun; simpl; intros; auto; f_equal; eauto. Qed.
Lemma list_pair_fun_cons: ∀ {A B C: Type} (f:A→B→C) a1 a2 l1 l2,
list_pair_fun f (a1::l1) (a2::l2) = f a1 a2::list_pair_fun f l1 l2.
Proof. simpl; intros; auto. Qed.
Lemma list_pair_fun_app: ∀ {A B C: Type} (f:A→B→C) l1 l2 l3 l4,
length l3 = length l1 →
list_pair_fun f (l1++l2) (l3++l4) = list_pair_fun f l1 l3 ++ list_pair_fun f l2 l4.
Proof.
induction l1; destruct l3; intros; auto; try solve [false; omega].
rewrite list_pair_fun_cons.
simpl.
rewrite list_pair_fun_cons.
f_equal; auto.
Qed.
Lemma list_pair_fun_length: ∀ {A B C: Type} (f: A→B→C) l1 l2,
length (list_pair_fun f l1 l2) = min (length l1) (length l2).
Proof. intros; unfold list_pair_fun; rewrite map_length; apply combine_length. Qed.
Lemma list_pair_fun_nil_r: ∀ {A B C: Type} (f:A→B→C) l,
list_pair_fun f l [] = [].
Proof. induction l; simpl; intros; auto. Qed.
Lemma list_pair_fun_nil_l: ∀ {A B C: Type} (f:A→B→C) l,
list_pair_fun f [] l = [].
Proof. intros; reflexivity. Qed.
End ListPairFun.
Section ListPlus.
Definition list_plus := list_pair_fun plus.
Lemma list_plus_comm: ∀ l1 l2,
list_plus l1 l2 = list_plus l2 l1.
Proof. intros; apply list_pair_fun_comm; intros; omega. Qed.
Lemma list_plus_assoc: ∀ l1 l2 l3,
list_plus l1 (list_plus l2 l3) = list_plus (list_plus l1 l2) l3.
Proof. intros; apply list_pair_fun_assoc; intros; omega. Qed.
Lemma list_plus_app: ∀ l1 l2 l3 l4,
length l3 = length l1 →
list_plus (l1++l2) (l3++l4) = list_plus l1 l3 ++ list_plus l2 l4.
Proof. intros; apply list_pair_fun_app; auto. Qed.
Lemma list_plus_cons: ∀ a1 a2 l1 l2,
list_plus (a1::l1) (a2::l2) = (a1 + a2::list_plus l1 l2)%nat.
Proof. intros; apply list_pair_fun_cons; auto. Qed.
Lemma list_plus_length: ∀ l1 l2,
length (list_plus l1 l2) = min (length l1) (length l2).
Proof. intros; apply list_pair_fun_length. Qed.
Lemma list_plus_nil_r: ∀ l,
list_plus l [] = [].
Proof. intros; apply list_pair_fun_nil_r. Qed.
End ListPlus.
Section ListLE.
Definition list_le l1 l2 := length l2 = length l1 ∧ ∀ a b, In (a,b) (combine l1 l2) → a ≤ b.
Lemma list_le_trans: ∀ l1 l2 l3,
list_le l1 l2 → list_le l2 l3 → list_le l1 l3.
Proof.
unfold list_le; induction l1; destruct l2; destruct l3; simpl; intros; intuition; try solve [false].
inverts H4. inverts H1; inverts H.
transitivity n.
apply H2; auto.
apply H3; auto.
inverts H1; inverts H.
eapply IHl1; eauto.
Qed.
Lemma list_le_app1: ∀ l1 l2 l3 l4,
list_le (l1++l3) (l2++l4) →
length l2=length l1 →
list_le l1 l2 ∧ list_le l3 l4.
Proof.
unfold list_le; intros.
destruct H.
split; split; intros; auto.
apply H1; rewrite combine_app; auto; apply in_or_app. left; auto.
repeat rewrite app_length in ×. omega.
apply H1.
rewrite combine_app; auto.
apply in_or_app. right; auto.
Qed.
Lemma list_le_app2: ∀ l1 l2 l3 l4,
list_le l1 l2 → list_le l3 l4 →
length l2=length l1 →
list_le (l1++l3) (l2++l4).
Proof.
unfold list_le; intros. destruct H; destruct H0.
repeat rewrite app_length.
split; auto.
intros.
rewrite combine_app in H4; auto.
apply in_app_iff in H4.
destruct H4; auto.
Qed.
Lemma list_le_single: ∀ a b,
list_le [a] [b] ↔ a ≤ b.
Proof. unfold list_le; intuition; simpl in *; eauto; destruct H0 as [?|?]; inverts H0; auto. Qed.
Lemma list_le_plus: ∀ l1 l3,
list_le l1 l3 →
∃ l2,
l3 = list_plus l1 l2.
Proof.
unfold list_le; induction l1; destruct l3; simpl; intuition.
∃ (@nil nat); reflexivity.
inverts H0.
edestruct IHl1 as [l2 ?]; eauto.
subst.
specialize (H1 a n).
lapply H1; intros; auto.
∃ (n-a::l2).
rewrite list_plus_cons.
f_equal.
omega.
Qed.
Lemma list_plus_le: ∀ l1 l2,
length l2 ≥ length l1 →
list_le l1 (list_plus l1 l2).
Proof.
unfold list_le; induction l1; destruct l2; simpl; intuition.
rewrite map_length. rewrite combine_length.
rewrite Min.min_l; auto. omega.
inverts H1.
omega.
destruct (IHl1 l2); clear IHl1; auto.
omega.
Qed.
Lemma list_le_refl: ∀ l,
list_le l l.
Proof. unfold list_le; induction l; simpl; intuition; inverts H2; eauto. Qed.
Lemma list_le_cons2: ∀ x y l1 l2,
x ≤ y →
list_le l1 l2 → list_le (x::l1) (y::l2).
Proof. unfold list_le; simpl; intros; intuition; inverts H3; eauto. Qed.
Lemma list_le_cons1: ∀ x y l1 l2,
list_le (x::l1) (y::l2) →
x≤y ∧ list_le l1 l2.
Proof. unfold list_le; simpl; intros; intuition. Qed.
Lemma min_le: ∀ n m,
min n m = n → n ≤ m.
Proof.
induction n; destruct m; simpl; intros; auto.
omega. false.
inverts H.
rewrite H1. apply IHn in H1. omega.
Qed.
End ListLE.
Section ListRep.
Fixpoint list_rep {A:Type} n (x:A) := match n with 0 ⇒ nil | S n ⇒ x::list_rep n x end.
Definition list_zeros n := list_rep n 0.
Lemma list_plus_zeros2: ∀ l,
list_plus l (list_zeros (length l)) = l.
Proof. unfold list_plus, list_zeros, list_rep, list_pair_fun; induction l; simpl; intros; auto; f_equal; auto; omega. Qed.
Lemma list_plus_zeros1: ∀ l,
list_plus (list_zeros (length l)) l = l.
Proof. intros; rewrite list_plus_comm; apply list_plus_zeros2. Qed.
Lemma list_rep_length: ∀ {A:Type} n (x:A),
length (list_rep n x) = n.
Proof. induction n; simpl; intros; auto. Qed.
Lemma list_zeros_length: ∀ n,
length (list_zeros n) = n.
Proof. intros; apply list_rep_length. Qed.
Lemma list_le_zeros: ∀ l,
list_le (list_zeros (length l)) l.
Proof. intros; rewrite<- list_plus_zeros2; rewrite list_plus_comm; apply list_plus_le; rewrite list_zeros_length; auto. Qed.
End ListRep.
Require Import LibTactics.
Section Lists.
Lemma skipn_length: ∀ {A:Type} (l l': list A) n,
skipn n l = l' → length l' = length l - n.
Proof. induction l; destruct n; simpl; intros; subst; auto. Qed.
Lemma app_split3: ∀ {A:Type} n (l:list A),
length l > n →
∃ l1 a l2,
l = l1++[a]++l2 ∧ length l1 = n.
Proof.
intros.
case_eq (skipn n l); intros.
apply skipn_length in H0. simpl in H0. false. omega.
∃ (firstn n l) a l0.
split.
rewrite<- (firstn_skipn n l) at 1.
f_equal; auto.
rewrite firstn_length.
apply Min.min_l.
omega.
Qed.
Lemma count_occ_nIn: ∀ {A:Type} eq_dec (x:A) l,
¬In x l →
count_occ eq_dec l x = 0.
Proof.
induction l; simpl; intros; auto.
apply Decidable.not_or in H; destruct H.
destruct (eq_dec a x); subst; auto.
false.
Qed.
Lemma app_inv: ∀ {A:Type} (l1 l2 l3 l4: list A),
l1++l3 = l2++l4 →
length l2 = length l1 →
l2=l1 ∧ l4=l3.
Proof.
induction l1; destruct l2; simpl; intros; try solve [false]; auto.
inverts H0.
inverts H.
edestruct IHl1 as [??]; eauto.
subst; auto.
Qed.
End Lists.
Section SplitCombine.
Lemma combine_nil2: ∀ A B (l:list A),
@combine A B l nil = nil.
Proof. induction l; simpl; intros; auto. Qed.
Lemma split_combine': ∀ {A B:Type} l,
@combine A B (fst (split l)) (snd (split l)) = l.
Proof.
intros.
generalize (split_combine l); intros.
destruct (split l) as [l1 l2].
simpl; auto.
Qed.
Lemma fst_split: ∀ {A B:Type} (a:A) (b:B) l,
fst (let (la,lb):= split l in (a::la, b::lb)) = a::fst (split l).
Proof. simpl; intros; destruct (split l); reflexivity. Qed.
Lemma snd_split: ∀ {A B:Type} (a:A) (b:B) l,
snd (let (la,lb):= split l in (a::la, b::lb)) = b::snd (split l).
Proof. simpl; intros; destruct (split l); reflexivity. Qed.
Lemma fst_split_app: ∀ {A B:Type} (l1 l2: list (A×B)),
fst (split l1) ++ fst (split l2) = fst (split (l1++l2)).
Proof. induction l1; intros; simpl; auto; destruct a; do 2 rewrite fst_split; simpl; f_equal; auto. Qed.
Lemma snd_split_app: ∀ {A B:Type} (l1 l2: list (A×B)),
snd (split l1) ++ snd (split l2) = snd (split (l1++l2)).
Proof. induction l1; intros; simpl; auto; destruct a; do 2 rewrite snd_split; simpl; f_equal; auto. Qed.
Lemma combine_app: ∀ {A B:Type} (l1:list A) (l3:list B) l2 l4,
length l3 = length l1 →
combine (l1++l2) (l3++l4) = (combine l1 l3)++(combine l2 l4).
Proof.
induction l1; destruct l3; intros; auto.
inverts H.
inverts H.
inverts H.
simpl.
f_equal. eauto.
Qed.
Lemma in_split_l': ∀ {A B: Type} (l: list (A×B)) x,
In x (fst (split l)) → ∃ y, In (x,y) l.
Proof.
induction l; simpl; intros.
false.
destruct a. rewrite fst_split in H.
destruct H as [?|?]. subst a.
∃ b; auto.
destruct (IHl x) as [y ?]; auto.
∃ y; auto.
Qed.
End SplitCombine.
Section ListPairFun.
Definition list_pair_fun {A B C: Type} (f:A→B→C) l1 l2 := (map (fun (nd: A×B) ⇒ let (n,d):=nd in f n d) (combine l1 l2)).
Lemma list_pair_fun_comm: ∀ {A B: Type} (f:A→A→B) l1 l2,
(∀ a b, f a b = f b a) →
list_pair_fun f l1 l2 = list_pair_fun f l2 l1.
Proof. induction l1; destruct l2; unfold list_pair_fun; simpl; intros; auto; f_equal; eauto. Qed.
Lemma list_pair_fun_assoc: ∀ {A: Type} (f: A→A→A) l1 l2 l3,
(∀ a b c, f a (f b c) = f (f a b) c) →
list_pair_fun f l1 (list_pair_fun f l2 l3) = list_pair_fun f (list_pair_fun f l1 l2) l3.
Proof. induction l1; destruct l2; destruct l3; unfold list_pair_fun; simpl; intros; auto; f_equal; eauto. Qed.
Lemma list_pair_fun_cons: ∀ {A B C: Type} (f:A→B→C) a1 a2 l1 l2,
list_pair_fun f (a1::l1) (a2::l2) = f a1 a2::list_pair_fun f l1 l2.
Proof. simpl; intros; auto. Qed.
Lemma list_pair_fun_app: ∀ {A B C: Type} (f:A→B→C) l1 l2 l3 l4,
length l3 = length l1 →
list_pair_fun f (l1++l2) (l3++l4) = list_pair_fun f l1 l3 ++ list_pair_fun f l2 l4.
Proof.
induction l1; destruct l3; intros; auto; try solve [false; omega].
rewrite list_pair_fun_cons.
simpl.
rewrite list_pair_fun_cons.
f_equal; auto.
Qed.
Lemma list_pair_fun_length: ∀ {A B C: Type} (f: A→B→C) l1 l2,
length (list_pair_fun f l1 l2) = min (length l1) (length l2).
Proof. intros; unfold list_pair_fun; rewrite map_length; apply combine_length. Qed.
Lemma list_pair_fun_nil_r: ∀ {A B C: Type} (f:A→B→C) l,
list_pair_fun f l [] = [].
Proof. induction l; simpl; intros; auto. Qed.
Lemma list_pair_fun_nil_l: ∀ {A B C: Type} (f:A→B→C) l,
list_pair_fun f [] l = [].
Proof. intros; reflexivity. Qed.
End ListPairFun.
Section ListPlus.
Definition list_plus := list_pair_fun plus.
Lemma list_plus_comm: ∀ l1 l2,
list_plus l1 l2 = list_plus l2 l1.
Proof. intros; apply list_pair_fun_comm; intros; omega. Qed.
Lemma list_plus_assoc: ∀ l1 l2 l3,
list_plus l1 (list_plus l2 l3) = list_plus (list_plus l1 l2) l3.
Proof. intros; apply list_pair_fun_assoc; intros; omega. Qed.
Lemma list_plus_app: ∀ l1 l2 l3 l4,
length l3 = length l1 →
list_plus (l1++l2) (l3++l4) = list_plus l1 l3 ++ list_plus l2 l4.
Proof. intros; apply list_pair_fun_app; auto. Qed.
Lemma list_plus_cons: ∀ a1 a2 l1 l2,
list_plus (a1::l1) (a2::l2) = (a1 + a2::list_plus l1 l2)%nat.
Proof. intros; apply list_pair_fun_cons; auto. Qed.
Lemma list_plus_length: ∀ l1 l2,
length (list_plus l1 l2) = min (length l1) (length l2).
Proof. intros; apply list_pair_fun_length. Qed.
Lemma list_plus_nil_r: ∀ l,
list_plus l [] = [].
Proof. intros; apply list_pair_fun_nil_r. Qed.
End ListPlus.
Section ListLE.
Definition list_le l1 l2 := length l2 = length l1 ∧ ∀ a b, In (a,b) (combine l1 l2) → a ≤ b.
Lemma list_le_trans: ∀ l1 l2 l3,
list_le l1 l2 → list_le l2 l3 → list_le l1 l3.
Proof.
unfold list_le; induction l1; destruct l2; destruct l3; simpl; intros; intuition; try solve [false].
inverts H4. inverts H1; inverts H.
transitivity n.
apply H2; auto.
apply H3; auto.
inverts H1; inverts H.
eapply IHl1; eauto.
Qed.
Lemma list_le_app1: ∀ l1 l2 l3 l4,
list_le (l1++l3) (l2++l4) →
length l2=length l1 →
list_le l1 l2 ∧ list_le l3 l4.
Proof.
unfold list_le; intros.
destruct H.
split; split; intros; auto.
apply H1; rewrite combine_app; auto; apply in_or_app. left; auto.
repeat rewrite app_length in ×. omega.
apply H1.
rewrite combine_app; auto.
apply in_or_app. right; auto.
Qed.
Lemma list_le_app2: ∀ l1 l2 l3 l4,
list_le l1 l2 → list_le l3 l4 →
length l2=length l1 →
list_le (l1++l3) (l2++l4).
Proof.
unfold list_le; intros. destruct H; destruct H0.
repeat rewrite app_length.
split; auto.
intros.
rewrite combine_app in H4; auto.
apply in_app_iff in H4.
destruct H4; auto.
Qed.
Lemma list_le_single: ∀ a b,
list_le [a] [b] ↔ a ≤ b.
Proof. unfold list_le; intuition; simpl in *; eauto; destruct H0 as [?|?]; inverts H0; auto. Qed.
Lemma list_le_plus: ∀ l1 l3,
list_le l1 l3 →
∃ l2,
l3 = list_plus l1 l2.
Proof.
unfold list_le; induction l1; destruct l3; simpl; intuition.
∃ (@nil nat); reflexivity.
inverts H0.
edestruct IHl1 as [l2 ?]; eauto.
subst.
specialize (H1 a n).
lapply H1; intros; auto.
∃ (n-a::l2).
rewrite list_plus_cons.
f_equal.
omega.
Qed.
Lemma list_plus_le: ∀ l1 l2,
length l2 ≥ length l1 →
list_le l1 (list_plus l1 l2).
Proof.
unfold list_le; induction l1; destruct l2; simpl; intuition.
rewrite map_length. rewrite combine_length.
rewrite Min.min_l; auto. omega.
inverts H1.
omega.
destruct (IHl1 l2); clear IHl1; auto.
omega.
Qed.
Lemma list_le_refl: ∀ l,
list_le l l.
Proof. unfold list_le; induction l; simpl; intuition; inverts H2; eauto. Qed.
Lemma list_le_cons2: ∀ x y l1 l2,
x ≤ y →
list_le l1 l2 → list_le (x::l1) (y::l2).
Proof. unfold list_le; simpl; intros; intuition; inverts H3; eauto. Qed.
Lemma list_le_cons1: ∀ x y l1 l2,
list_le (x::l1) (y::l2) →
x≤y ∧ list_le l1 l2.
Proof. unfold list_le; simpl; intros; intuition. Qed.
Lemma min_le: ∀ n m,
min n m = n → n ≤ m.
Proof.
induction n; destruct m; simpl; intros; auto.
omega. false.
inverts H.
rewrite H1. apply IHn in H1. omega.
Qed.
End ListLE.
Section ListRep.
Fixpoint list_rep {A:Type} n (x:A) := match n with 0 ⇒ nil | S n ⇒ x::list_rep n x end.
Definition list_zeros n := list_rep n 0.
Lemma list_plus_zeros2: ∀ l,
list_plus l (list_zeros (length l)) = l.
Proof. unfold list_plus, list_zeros, list_rep, list_pair_fun; induction l; simpl; intros; auto; f_equal; auto; omega. Qed.
Lemma list_plus_zeros1: ∀ l,
list_plus (list_zeros (length l)) l = l.
Proof. intros; rewrite list_plus_comm; apply list_plus_zeros2. Qed.
Lemma list_rep_length: ∀ {A:Type} n (x:A),
length (list_rep n x) = n.
Proof. induction n; simpl; intros; auto. Qed.
Lemma list_zeros_length: ∀ n,
length (list_zeros n) = n.
Proof. intros; apply list_rep_length. Qed.
Lemma list_le_zeros: ∀ l,
list_le (list_zeros (length l)) l.
Proof. intros; rewrite<- list_plus_zeros2; rewrite list_plus_comm; apply list_plus_le; rewrite list_zeros_length; auto. Qed.
End ListRep.