From: Andrea Asperti Date: Fri, 8 Jun 2012 10:46:29 +0000 (+0000) Subject: Dropping a coercion and some hints due to conflicts with CerCo X-Git-Tag: make_still_working~1647 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=5d54a6d3a0f22bb8784387c491de7bb66e67b625;p=helm.git Dropping a coercion and some hints due to conflicts with CerCo --- diff --git a/matita/matita/lib/basics/deqsets.ma b/matita/matita/lib/basics/deqsets.ma index fcc89f312..fb6ad5be4 100644 --- a/matita/matita/lib/basics/deqsets.ma +++ b/matita/matita/lib/basics/deqsets.ma @@ -207,7 +207,8 @@ qed. definition DeqSig ≝ λA:DeqSet.λP:A→Prop. mk_DeqSet (Σx:A.P x) (eq_sigma A P) (eq_sigma_true A P). - + +(* unification hint 0 ≔ C,P; T ≟ carr C, X ≟ DeqSig C P @@ -218,4 +219,4 @@ unification hint 0 ≔ T,P,p1,p2; X ≟ DeqSig T P (* ---------------------------------------- *) ⊢ eq_sigma T P p1 p2 ≡ eqb X p1 p2. - +*) diff --git a/matita/matita/lib/basics/lists/list.ma b/matita/matita/lib/basics/lists/list.ma index a20a89108..a330f6224 100644 --- a/matita/matita/lib/basics/lists/list.ma +++ b/matita/matita/lib/basics/lists/list.ma @@ -196,6 +196,11 @@ lemma length_reverse: ∀A.∀l:list A. #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. @@ -265,6 +270,27 @@ let rec mem A (a:A) (l:list A) on l ≝ | 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 Hnil >length_append >length_append //] /2/ + |#hd #tl #Hind #l1 #l2 #a #posn #Hlen #Ha + whd in match (flatten ??); #Hflat * #q cases q + [(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) + Hl1 // + ] + ] + ] +qed. + (****************************** nth ********************************) let rec nth n (A:Type[0]) (l:list A) (d:A) ≝ match n with diff --git a/matita/matita/lib/basics/lists/listb.ma b/matita/matita/lib/basics/lists/listb.ma index 438f3b497..a95d8a05a 100644 --- a/matita/matita/lib/basics/lists/listb.ma +++ b/matita/matita/lib/basics/lists/listb.ma @@ -122,6 +122,15 @@ lemma mem_to_memb: ∀S:DeqSet.∀a,l. mem S a l → memb S a l = true. ] ] qed. + +lemma memb_to_mem: ∀S:DeqSet.∀l,a. memb S a l =true → mem S a l. +#S #l #a elim l + [normalize #H destruct + |#b #tl #Hind #mema cases (orb_true_l … mema) + [#eqab >(\P eqab) %1 % |#memtl %2 @Hind @memtl] + ] +qed. + (**************** unicity test *****************) let rec uniqueb (S:DeqSet) l on l : bool ≝ diff --git a/matita/matita/lib/basics/types.ma b/matita/matita/lib/basics/types.ma index b319b5bd0..a5e35c9d2 100644 --- a/matita/matita/lib/basics/types.ma +++ b/matita/matita/lib/basics/types.ma @@ -67,7 +67,7 @@ interpretation "mk_DPair" 'mk_DPair x y = (mk_DPair ?? x y). (* sigma *) record Sig (A:Type[0]) (f:A→Prop) : Type[0] ≝ { - pi1:> A + pi1: A (* not a coercion due to problems with Cerco *) ; pi2: f pi1 }.