interpretation "nil" 'nil = (nil ?).
interpretation "cons" 'cons hd tl = (cons ? hd tl).
-definition not_nil: ∀A:Type[0].list A → Prop ≝
+definition is_nil: ∀A:Type[0].list A → Prop ≝
λA.λl.match l with [ nil ⇒ True | cons hd tl ⇒ False ].
theorem nil_cons:
∀A:Type[0].∀l:list A.∀a:A. a::l ≠ [].
- #A #l #a @nmk #Heq (change with (not_nil ? (a::l))) >Heq //
+ #A #l #a @nmk #Heq (change with (is_nil ? (a::l))) >Heq //
qed.
(*
definition tail ≝ λA.λl: list A.
match l with [ nil ⇒ [] | cons hd tl ⇒ tl].
+
+definition option_hd ≝
+ λA.λl:list A. match l with
+ [ nil ⇒ None ?
+ | cons a _ ⇒ Some ? a ].
interpretation "append" 'append l1 l2 = (append ? l1 l2).
∀A.associative (list A) (append A).
#A #l1 #l2 #l3 (elim l1) normalize // qed.
-(* deleterio per auto
-ntheorem cons_append_commute:
- ∀A:Type.∀l1,l2:list A.∀a:A.
- a :: (l1 @ l2) = (a :: l1) @ l2.
-//; nqed. *)
-
theorem append_cons:∀A.∀a:A.∀l,l1.l@(a::l1)=(l@[a])@l1.
#A #a #l #l1 >associative_append // qed.
#A #l1 #l2 #isnil @(nil_append_elim A l1 l2) /2/
qed.
+lemma cons_injective_l : ∀A.∀a1,a2:A.∀l1,l2.a1::l1 = a2::l2 → a1 = a2.
+#A #a1 #a2 #l1 #l2 #Heq destruct //
+qed.
+
+lemma cons_injective_r : ∀A.∀a1,a2:A.∀l1,l2.a1::l1 = a2::l2 → l1 = l2.
+#A #a1 #a2 #l1 #l2 #Heq destruct //
+qed.
+
(**************************** iterators ******************************)
let rec map (A,B:Type[0]) (f: A → B) (l:list A) on l: list B ≝
theorem eq_map : ∀A,B,f,g,l. (∀x.f x = g x) → map A B f l = map A B g l.
#A #B #f #g #l #eqfg (elim l) normalize // qed.
-let rec dprodl (A:Type[0]) (f:A→Type[0]) (l1:list A) (g:(∀a:A.list (f a))) on l1 ≝
-match l1 with
- [ nil ⇒ nil ?
- | cons a tl ⇒ (map ??(mk_Sig ?? a) (g a)) @ dprodl A f tl g
- ].
+(**************************** reverse *****************************)
+let rec rev_append S (l1,l2:list S) on l1 ≝
+ match l1 with
+ [ nil ⇒ l2
+ | cons a tl ⇒ rev_append S tl (a::l2)
+ ]
+.
+
+definition reverse ≝λS.λl.rev_append S l [].
+
+lemma reverse_single : ∀S,a. reverse S [a] = [a].
+// qed.
+
+lemma rev_append_def : ∀S,l1,l2.
+ rev_append S l1 l2 = (reverse S l1) @ l2 .
+#S #l1 elim l1 normalize //
+qed.
+
+lemma reverse_cons : ∀S,a,l. reverse S (a::l) = (reverse S l)@[a].
+#S #a #l whd in ⊢ (??%?); //
+qed.
+
+lemma reverse_append: ∀S,l1,l2.
+ reverse S (l1 @ l2) = (reverse S l2)@(reverse S l1).
+#S #l1 elim l1 [normalize // | #a #tl #Hind #l2 >reverse_cons
+>reverse_cons // qed.
+
+lemma reverse_reverse : ∀S,l. reverse S (reverse S l) = l.
+#S #l elim l // #a #tl #Hind >reverse_cons >reverse_append
+normalize // qed.
+
+(* an elimination principle for lists working on the tail;
+useful for strings *)
+lemma list_elim_left: ∀S.∀P:list S → Prop. P (nil S) →
+(∀a.∀tl.P tl → P (tl@[a])) → ∀l. P l.
+#S #P #Pnil #Pstep #l <(reverse_reverse … l)
+generalize in match (reverse S l); #l elim l //
+#a #tl #H >reverse_cons @Pstep //
+qed.
(**************************** length ******************************)
[ nil ⇒ 0
| cons a tl ⇒ S (length A tl)].
-notation "|M|" non associative with precedence 60 for @{'norm $M}.
-interpretation "norm" 'norm l = (length ? l).
+interpretation "list length" 'card l = (length ? l).
+
+lemma length_tail: ∀A,l. length ? (tail A l) = pred (length ? l).
+#A #l elim l //
+qed.
lemma length_append: ∀A.∀l1,l2:list A.
|l1@l2| = |l1|+|l2|.
#A #l1 elim l1 // normalize /2/
qed.
+lemma length_map: ∀A,B,l.∀f:A→B. length ? (map ?? f l) = length ? l.
+#A #B #l #f elim l // #a #tl #Hind normalize //
+qed.
+
+lemma length_reverse: ∀A.∀l:list A.
+ |reverse A l| = |l|.
+#A #l elim l // #a #l0 #IH >reverse_cons >length_append normalize //
+qed.
+
+lemma lenght_to_nil: ∀A.∀l:list A.
+ |l| = 0 → l = [ ].
+#A * // #a #tl normalize #H destruct
+qed.
+
+(****************** traversing two lists in parallel *****************)
+lemma list_ind2 :
+ ∀T1,T2:Type[0].∀l1:list T1.∀l2:list T2.∀P:list T1 → list T2 → Prop.
+ length ? l1 = length ? l2 →
+ (P [] []) →
+ (∀tl1,tl2,hd1,hd2. P tl1 tl2 → P (hd1::tl1) (hd2::tl2)) →
+ P l1 l2.
+#T1 #T2 #l1 #l2 #P #Hl #Pnil #Pcons
+generalize in match Hl; generalize in match l2;
+elim l1
+[#l2 cases l2 // normalize #t2 #tl2 #H destruct
+|#t1 #tl1 #IH #l2 cases l2
+ [normalize #H destruct
+ |#t2 #tl2 #H @Pcons @IH normalize in H; destruct // ]
+]
+qed.
+
+lemma list_cases2 :
+ ∀T1,T2:Type[0].∀l1:list T1.∀l2:list T2.∀P:Prop.
+ length ? l1 = length ? l2 →
+ (l1 = [] → l2 = [] → P) →
+ (∀hd1,hd2,tl1,tl2.l1 = hd1::tl1 → l2 = hd2::tl2 → P) → P.
+#T1 #T2 #l1 #l2 #P #Hl @(list_ind2 … Hl)
+[ #Pnil #Pcons @Pnil //
+| #tl1 #tl2 #hd1 #hd2 #IH1 #IH2 #Hp @Hp // ]
+qed.
+
+(*********************** properties of append ***********************)
+lemma append_l1_injective :
+ ∀A.∀l1,l2,l3,l4:list A. |l1| = |l2| → l1@l3 = l2@l4 → l1 = l2.
+#a #l1 #l2 #l3 #l4 #Hlen @(list_ind2 … Hlen) //
+#tl1 #tl2 #hd1 #hd2 #IH normalize #Heq destruct @eq_f /2/
+qed.
+
+lemma append_l2_injective :
+ ∀A.∀l1,l2,l3,l4:list A. |l1| = |l2| → l1@l3 = l2@l4 → l3 = l4.
+#a #l1 #l2 #l3 #l4 #Hlen @(list_ind2 … Hlen) normalize //
+#tl1 #tl2 #hd1 #hd2 #IH normalize #Heq destruct /2/
+qed.
+
+lemma append_l1_injective_r :
+ ∀A.∀l1,l2,l3,l4:list A. |l3| = |l4| → l1@l3 = l2@l4 → l1 = l2.
+#a #l1 #l2 #l3 #l4 #Hlen #Heq lapply (eq_f … (reverse ?) … Heq)
+>reverse_append >reverse_append #Heq1
+lapply (append_l2_injective … Heq1) [ // ] #Heq2
+lapply (eq_f … (reverse ?) … Heq2) //
+qed.
+
+lemma append_l2_injective_r :
+ ∀A.∀l1,l2,l3,l4:list A. |l3| = |l4| → l1@l3 = l2@l4 → l3 = l4.
+#a #l1 #l2 #l3 #l4 #Hlen #Heq lapply (eq_f … (reverse ?) … Heq)
+>reverse_append >reverse_append #Heq1
+lapply (append_l1_injective … Heq1) [ // ] #Heq2
+lapply (eq_f … (reverse ?) … Heq2) //
+qed.
+
+lemma length_rev_append: ∀A.∀l,acc:list A.
+ |rev_append ? l acc| = |l|+|acc|.
+#A #l elim l // #a #tl #Hind normalize
+#acc >Hind normalize //
+qed.
+
+(****************************** mem ********************************)
+let rec mem A (a:A) (l:list A) on l ≝
+ match l with
+ [ nil ⇒ False
+ | cons hd tl ⇒ a=hd ∨ mem A a tl
+ ].
+
+lemma mem_map: ∀A,B.∀f:A→B.∀l,b.
+ mem ? b (map … f l) → ∃a. mem ? a l ∧ f a = b.
+#A #B #f #l elim l
+ [#b normalize @False_ind
+ |#a #tl #Hind #b normalize *
+ [#eqb @(ex_intro … a) /3/
+ |#memb cases (Hind … memb) #a * #mema #eqb
+ @(ex_intro … a) /3/
+ ]
+ ]
+qed.
+
+lemma mem_map_forward: ∀A,B.∀f:A→B.∀a,l.
+ mem A a l → mem B (f a) (map ?? f l).
+ #A #B #f #a #l elim l
+ [normalize @False_ind
+ |#b #tl #Hind *
+ [#eqab <eqab normalize %1 % |#memtl normalize %2 @Hind @memtl]
+ ]
+qed.
+
+(***************************** split *******************************)
+let rec split_rev A (l:list A) acc n on n ≝
+ match n with
+ [O ⇒ 〈acc,l〉
+ |S m ⇒ match l with
+ [nil ⇒ 〈acc,[]〉
+ |cons a tl ⇒ split_rev A tl (a::acc) m
+ ]
+ ].
+
+definition split ≝ λA,l,n.
+ let 〈l1,l2〉 ≝ split_rev A l [] n in 〈reverse ? l1,l2〉.
+
+lemma split_rev_len: ∀A,n,l,acc. n ≤ |l| →
+ |\fst (split_rev A l acc n)| = n+|acc|.
+#A #n elim n // #m #Hind *
+ [normalize #acc #Hfalse @False_ind /2/
+ |#a #tl #acc #Hlen normalize >Hind
+ [normalize // |@le_S_S_to_le //]
+ ]
+qed.
+
+lemma split_len: ∀A,n,l. n ≤ |l| →
+ |\fst (split A l n)| = n.
+#A #n #l #Hlen normalize >(eq_pair_fst_snd ?? (split_rev …))
+normalize >length_reverse >(split_rev_len … [ ] Hlen) normalize //
+qed.
+
+lemma split_rev_eq: ∀A,n,l,acc. n ≤ |l| →
+ reverse ? acc@ l =
+ reverse ? (\fst (split_rev A l acc n))@(\snd (split_rev A l acc n)).
+ #A #n elim n //
+ #m #Hind *
+ [#acc whd in ⊢ ((??%)→?); #False_ind /2/
+ |#a #tl #acc #Hlen >append_cons <reverse_single <reverse_append
+ @(Hind tl) @le_S_S_to_le @Hlen
+ ]
+qed.
+
+lemma split_eq: ∀A,n,l. n ≤ |l| →
+ l = (\fst (split A l n))@(\snd (split A l n)).
+#A #n #l #Hlen change with ((reverse ? [ ])@l) in ⊢ (??%?);
+>(split_rev_eq … Hlen) normalize
+>(eq_pair_fst_snd ?? (split_rev A l [] n)) %
+qed.
+
+lemma split_exists: ∀A,n.∀l:list A. n ≤ |l| →
+ ∃l1,l2. l = l1@l2 ∧ |l1| = n.
+#A #n #l #Hlen @(ex_intro … (\fst (split A l n)))
+@(ex_intro … (\snd (split A l n))) % /2/
+qed.
+
+(****************************** flatten ******************************)
+definition flatten ≝ λA.foldr (list A) (list A) (append A) [].
+
+lemma flatten_to_mem: ∀A,n,l,l1,l2.∀a:list A. 0 < n →
+ (∀x. mem ? x l → |x| = n) → |a| = n → flatten ? l = l1@a@l2 →
+ (∃q.|l1| = n*q) → mem ? a l.
+#A #n #l elim l
+ [normalize #l1 #l2 #a #posn #Hlen #Ha #Hnil @False_ind
+ cut (|a|=0) [@sym_eq @le_n_O_to_eq
+ @(transitive_le ? (|nil A|)) // >Hnil >length_append >length_append //] /2/
+ |#hd #tl #Hind #l1 #l2 #a #posn #Hlen #Ha
+ whd in match (flatten ??); #Hflat * #q cases q
+ [<times_n_O #Hl1
+ cut (a = hd) [>(lenght_to_nil… Hl1) in Hflat;
+ whd in ⊢ ((???%)→?); #Hflat @sym_eq @(append_l1_injective … Hflat)
+ >Ha >Hlen // %1 //
+ ] /2/
+ |#q1 #Hl1 lapply (split_exists … n l1 ?) //
+ * #l11 * #l12 * #Heql1 #Hlenl11 %2
+ @(Hind l12 l2 … posn ? Ha)
+ [#x #memx @Hlen %2 //
+ |@(append_l2_injective ? hd l11)
+ [>Hlenl11 @Hlen %1 %
+ |>Hflat >Heql1 >associative_append %
+ ]
+ |@(ex_intro …q1) @(injective_plus_r n)
+ <Hlenl11 in ⊢ (??%?); <length_append <Heql1 >Hl1 //
+ ]
+ ]
+ ]
+qed.
+
(****************************** nth ********************************)
let rec nth n (A:Type[0]) (l:list A) (d:A) ≝
match n with
]
] qed.
+let rec Allr (A:Type[0]) (R:relation A) (l:list A) on l : Prop ≝
+match l with
+[ nil ⇒ True
+| cons a1 l ⇒ match l with [ nil ⇒ True | cons a2 _ ⇒ R a1 a2 ∧ Allr A R l ]
+].
+
(**************************** Exists *******************************)
let rec Exists (A:Type[0]) (P:A → Prop) (l:list A) on l : Prop ≝
qed.
lemma length_ltl: ∀A,n,l. |ltl A l n| = |l| - n.
-#A #n elim n -n /2/
+#A #n elim n -n //
#n #IHn *; normalize /2/
qed.
[ O ⇒ [ ]
| S m ⇒ a::(make_list A a m)
].
+
+(* ******** labelled reflexive and transitive closure ************)
+
+inductive lstar (A:Type[0]) (B:Type[0]) (R: A→relation B): list A → relation B ≝
+| lstar_nil : ∀b. lstar A B R ([]) b b
+| lstar_cons: ∀a,b1,b. R a b1 b →
+ ∀l,b2. lstar A B R l b b2 → lstar A B R (a::l) b1 b2
+.
+
+lemma lstar_step: ∀A,B,R,a,b1,b2. R a b1 b2 → lstar A B R ([a]) b1 b2.
+/2 width=3/
+qed.
+
+lemma lstar_inv_nil: ∀A,B,R,l,b1,b2. lstar A B R l b1 b2 → [] = l → b1 = b2.
+#A #B #R #l #b1 #b2 * -l -b1 -b2 //
+#a #b1 #b #_ #l #b2 #_ #H destruct
+qed-.
+
+lemma lstar_inv_cons: ∀A,B,R,l,b1,b2. lstar A B R l b1 b2 →
+ ∀a0,l0. a0::l0 = l →
+ ∃∃b. R a0 b1 b & lstar A B R l0 b b2.
+#A #B #R #l #b1 #b2 * -l -b1 -b2
+[ #b #a0 #l0 #H destruct
+| #a #b1 #b #Hb1 #l #b2 #Hb2 #a0 #l0 #H destruct /2 width=3/
+]
+qed-.
+
+lemma lstar_inv_step: ∀A,B,R,a,b1,b2. lstar A B R ([a]) b1 b2 → R a b1 b2.
+#A #B #R #a #b1 #b2 #H
+elim (lstar_inv_cons ?????? H ???) -H [4: // |2,3: skip ] #b #Hb1 #H (**) (* simplify line *)
+<(lstar_inv_nil ?????? H ?) -H // (**) (* simplify line *)
+qed-.
+
+theorem lstar_singlevalued: ∀A,B,R. (∀a. singlevalued ?? (R a)) →
+ ∀l. singlevalued … (lstar A B R l).
+#A #B #R #HR #l #b #c1 #H elim H -l -b -c1
+[ /2 width=5 by lstar_inv_nil/
+| #a #b #b1 #Hb1 #l #c1 #_ #IHbc1 #c2 #H
+ elim (lstar_inv_cons ?????? H ???) -H [4: // |2,3: skip ] #b2 #Hb2 #Hbc2 (**) (* simplify line *)
+ lapply (HR … Hb1 … Hb2) -b #H destruct /2 width=1/
+]
+qed-.
+
+theorem lstar_trans: ∀A,B,R,l1,b1,b. lstar A B R l1 b1 b →
+ ∀l2,b2. lstar A B R l2 b b2 → lstar A B R (l1@l2) b1 b2.
+#A #B #R #l1 #b1 #b #H elim H -l1 -b1 -b normalize // /3 width=3/
+qed-.
projects / helm.git / blobdiff