From a87c9d012b588c381dc82c53fd0652762a9e50c9 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Fri, 27 Apr 2012 11:46:07 +0000 Subject: [PATCH] Extensions to finset (sum) and auxiliary lemmas. --- matita/matita/lib/basics/bool.ma | 4 ++ matita/matita/lib/basics/deqsets.ma | 45 +++++++++++++++- matita/matita/lib/basics/finset.ma | 71 ++++++++++++++++++------- matita/matita/lib/basics/lists/listb.ma | 24 +++++++++ matita/matita/lib/basics/logic.ma | 6 +-- 5 files changed, 128 insertions(+), 22 deletions(-) diff --git a/matita/matita/lib/basics/bool.ma b/matita/matita/lib/basics/bool.ma index fb0106f12..587ab9ed6 100644 --- a/matita/matita/lib/basics/bool.ma +++ b/matita/matita/lib/basics/bool.ma @@ -54,6 +54,10 @@ theorem andb_elim: ∀ b1,b2:bool. ∀ P:bool → Prop. match b1 with [ true ⇒ P b2 | false ⇒ P false] → P (b1 ∧ b2). #b1 #b2 #P (elim b1) normalize // qed. +theorem true_to_andb_true: ∀b1,b2. b1 = true → b2 = true → (b1 ∧ b2) = true. +#b1 cases b1 normalize // +qed. + theorem andb_true_l: ∀ b1,b2. (b1 ∧ b2) = true → b1 = true. #b1 (cases b1) normalize // qed. diff --git a/matita/matita/lib/basics/deqsets.ma b/matita/matita/lib/basics/deqsets.ma index 4d86c9f6c..2d6434f65 100644 --- a/matita/matita/lib/basics/deqsets.ma +++ b/matita/matita/lib/basics/deqsets.ma @@ -100,4 +100,47 @@ unification hint 0 ≔ T1,T2,p1,p2; example hint2: ∀b1,b2. 〈b1,true〉==〈false,b2〉=true → 〈b1,true〉=〈false,b2〉. -#b1 #b2 #H @(\P H). \ No newline at end of file +#b1 #b2 #H @(\P H) +qed. + +(* sum *) +definition eq_sum ≝ + λA,B:DeqSet.λp1,p2:A+B. + match p1 with + [ inl a1 ⇒ match p2 with + [ inl a2 ⇒ a1 == a2 | inr b2 ⇒ false ] + | inr b1 ⇒ match p2 with + [ inl a2 ⇒ false | inr b2 ⇒ b1 == b2 ] + ]. + +lemma eq_sum_true: ∀A,B:DeqSet.∀p1,p2:A+B. + eq_sum A B p1 p2 = true ↔ p1 = p2. +#A #B * + [#a1 * + [#a2 normalize % + [#eqa >(\P eqa) // | #H destruct @(\b ?) //] + |#b2 normalize % #H destruct + ] + |#b1 * + [#a2 normalize % #H destruct + |#b2 normalize % + [#eqb >(\P eqb) // | #H destruct @(\b ?) //] + ] + ] +qed. + +definition DeqSum ≝ λA,B:DeqSet. + mk_DeqSet (A+B) (eq_sum A B) (eq_sum_true A B). + +unification hint 0 ≔ C1,C2; + T1 ≟ carr C1, + T2 ≟ carr C2, + X ≟ DeqSum C1 C2 +(* ---------------------------------------- *) ⊢ + T1+T2 ≡ carr X. + +unification hint 0 ≔ T1,T2,p1,p2; + X ≟ DeqSum T1 T2 +(* ---------------------------------------- *) ⊢ + eq_sum T1 T2 p1 p2 ≡ eqb X p1 p2. + diff --git a/matita/matita/lib/basics/finset.ma b/matita/matita/lib/basics/finset.ma index 1b972ec06..0f4161997 100644 --- a/matita/matita/lib/basics/finset.ma +++ b/matita/matita/lib/basics/finset.ma @@ -11,18 +11,64 @@ include "basics/lists/listb.ma". -(****** DeqSet: a set with a decidbale equality ******) +(****** DeqSet: a set with a decidable equality ******) record FinSet : Type[1] ≝ -{ carr:> DeqSet; - enum: list carr; - enum_complete: ∀x.memb carr x enum = true; - enum_unique: uniqueb carr enum = true +{ FinSetcarr:> DeqSet; + enum: list FinSetcarr; + enum_unique: uniqueb FinSetcarr enum = true }. -(* -definition DeqBool ≝ mk_DeqSet bool beqb beqb_true. +definition enum_sum ≝ λA,B:DeqSet.λl1.λl2. + (map ?? (inl A B) l1) @ (map ?? (inr A B) l2). + +lemma enumAB_def : ∀A,B:FinSet.∀l1,l2. enum_sum A B l1 l2 = + (map ?? (inl A B) l1) @ (map ?? (inr A B) l2). +// qed. + +axiom unique_map_inj: ∀A,B:DeqSet.∀f:A→B.∀l. injective A B f → + uniqueb A l = true → uniqueb B (map ?? f l) = true . +axiom memb_map_inj: ∀A,B:DeqSet.∀f:A→B.∀l,a. injective A B f → + memb ? (f a) (map ?? f l) = true → memb ? a l = true. + +lemma enumAB_unique: ∀A,B:DeqSet.∀l1,l2. + uniqueb A l1 = true → uniqueb B l2 = true → + uniqueb ? (enum_sum A B l1 l2) = true. +#A #B #l1 #l2 elim l1 + [#_ #ul2 @unique_map_inj // #b1 #b2 #Hinr destruct // + |#a #tl #Hind #uA #uB @true_to_andb_true + [@sym_eq @noteq_to_eqnot % #H + cases (memb_append … (sym_eq … H)) + [#H1 @(absurd (memb ? a tl = true)) + [@(memb_map_inj …H1) #a1 #a2 #Hinl destruct // + |<(andb_true_l … uA) @eqnot_to_noteq // + ] + |elim l2 + [normalize #H destruct + |#b #tlB #Hind #membH cases (orb_true_l … membH) + [#H lapply (\P H) #H1 destruct |@Hind] + ] + ] + |@Hind // @(andb_true_r … uA) + ] + ] +qed. + +definition FinSum ≝ λA,B:FinSet. + mk_FinSet (DeqSum A B) + (enum_sum A B (enum A) (enum B)) + (enumAB_unique … (enum_unique A) (enum_unique B)). + +unification hint 0 ≔ C1,C2; + T1 ≟ FinSetcarr C1, + T2 ≟ FinSetcarr C2, + X ≟ FinSum C1 C2 +(* ---------------------------------------- *) ⊢ + T1+T2 ≡ FinSetcarr X. + + +(* unification hint 0 ≔ ; X ≟ mk_DeqSet bool beqb beqb_true (* ---------------------------------------- *) ⊢ @@ -52,17 +98,6 @@ qed. definition DeqProd ≝ λA,B:DeqSet. mk_DeqSet (A×B) (eq_pairs A B) (eq_pairs_true A B). -unification hint 0 ≔ C1,C2; - T1 ≟ carr C1, - T2 ≟ carr C2, - X ≟ DeqProd C1 C2 -(* ---------------------------------------- *) ⊢ - T1×T2 ≡ carr X. - -unification hint 0 ≔ T1,T2,p1,p2; - X ≟ DeqProd T1 T2 -(* ---------------------------------------- *) ⊢ - eq_pairs T1 T2 p1 p2 ≡ eqb X p1 p2. example hint2: ∀b1,b2. 〈b1,true〉==〈false,b2〉=true → 〈b1,true〉=〈false,b2〉. diff --git a/matita/matita/lib/basics/lists/listb.ma b/matita/matita/lib/basics/lists/listb.ma index b6d5864f8..e46f45f07 100644 --- a/matita/matita/lib/basics/lists/listb.ma +++ b/matita/matita/lib/basics/lists/listb.ma @@ -145,6 +145,30 @@ cases (true_or_false … (memb S a (unique_append S tl l2))) #H >H normalize [@Hind //] >H normalize @Hind // qed. +lemma memb_map_inj: ∀A,B:DeqSet.∀f:A→B.∀l,a. injective A B f → + memb ? (f a) (map ?? f l) = true → memb ? a l = true. +#A #B #f #l #a #injf elim l + [normalize // + |#a1 #tl #Hind #Ha cases (orb_true_l … Ha) + [#eqf @orb_true_r1 @(\b ?) >(injf … (\P eqf)) // + |#membtl @orb_true_r2 /2/ + ] + ] +qed. + +lemma unique_map_inj: ∀A,B:DeqSet.∀f:A→B.∀l. injective A B f → + uniqueb A l = true → uniqueb B (map ?? f l) = true . +#A #B #f #l #injf elim l + [normalize // + |#a #tl #Hind #Htl @true_to_andb_true + [@sym_eq @noteq_to_eqnot @sym_not_eq + @(not_to_not ?? (memb_map_inj … injf …) ) + <(andb_true_l ?? Htl) /2/ + |@Hind @(andb_true_r ?? Htl) + ] + ] +qed. + (******************* sublist *******************) definition sublist ≝ λS,l1,l2.∀a. memb S a l1 = true → memb S a l2 = true. diff --git a/matita/matita/lib/basics/logic.ma b/matita/matita/lib/basics/logic.ma index 8f981d469..70e743e99 100644 --- a/matita/matita/lib/basics/logic.ma +++ b/matita/matita/lib/basics/logic.ma @@ -263,10 +263,10 @@ definition eqProp ≝ λA:Prop.eq A. (* Example to avoid indexing and the consequential creation of ill typed terms during paramodulation *) -example lemmaK : ∀A.∀x:A.∀h:x=x. eqProp ? h (refl A x). +lemma lemmaK : ∀A.∀x:A.∀h:x=x. eqProp ? h (refl A x). #A #x #h @(refl ? h: eqProp ? ? ?). -qed. +qed-. theorem streicherK : ∀T:Type[2].∀t:T.∀P:t = t → Type[3].P (refl ? t) → ∀p.P p. #T #t #P #H #p >(lemmaK T t p) @H -qed. +qed-. -- 2.39.2