From: Andrea Asperti Date: Fri, 25 May 2012 08:58:36 +0000 (+0000) Subject: New definition of finset. X-Git-Tag: make_still_working~1695 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=30172d86a0cd979e44ae3343655f6ce55043dd52;p=helm.git New definition of finset. --- diff --git a/matita/matita/lib/basics/deqsets.ma b/matita/matita/lib/basics/deqsets.ma index 45afabe59..38c9a1e05 100644 --- a/matita/matita/lib/basics/deqsets.ma +++ b/matita/matita/lib/basics/deqsets.ma @@ -149,3 +149,34 @@ unification hint 0 ≔ T1,T2,p1,p2; (* ---------------------------------------- *) ⊢ eq_sum T1 T2 p1 p2 ≡ eqb X p1 p2. +(* sigma *) +definition eq_sigma ≝ + λA:DeqSet.λP:A→Prop.λp1,p2:Σx:A.P x. + match p1 with + [mk_Sig a1 h1 ⇒ + match p2 with + [mk_Sig a2 h2 ⇒ a1==a2]]. + +(* uses proof irrelevance *) +lemma eq_sigma_true: ∀A:DeqSet.∀P.∀p1,p2:Σx.P x. + eq_sigma A P p1 p2 = true ↔ p1 = p2. +#A #P * #a1 #Ha1 * #a2 #Ha2 % + [normalize #eqa generalize in match Ha1; >(\P eqa) // + |#H >H @(\b ?) // + ] +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 +(* ---------------------------------------- *) ⊢ + Σx:T.P x ≡ carr X. + +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/finset.ma b/matita/matita/lib/basics/finset.ma index 85f4ef3ba..b8f698110 100644 --- a/matita/matita/lib/basics/finset.ma +++ b/matita/matita/lib/basics/finset.ma @@ -16,7 +16,8 @@ include "basics/lists/listb.ma". record FinSet : Type[1] ≝ { FinSetcarr:> DeqSet; enum: list FinSetcarr; - enum_unique: uniqueb FinSetcarr enum = true + enum_unique: uniqueb FinSetcarr enum = true; + enum_complete : ∀x:FinSetcarr. memb ? x enum = true }. notation < "𝐅" non associative with precedence 90 @@ -27,7 +28,11 @@ interpretation "FinSet" 'bigF = (mk_FinSet ???). lemma bool_enum_unique: uniqueb ? [true;false] = true. // qed. -definition FinBool ≝ mk_FinSet DeqBool [true;false] bool_enum_unique. +lemma bool_enum_complete: ∀x:bool. memb ? x [true;false] = true. +* // qed. + +definition FinBool ≝ + mk_FinSet DeqBool [true;false] bool_enum_unique bool_enum_complete. unification hint 0 ≔ ; X ≟ FinBool @@ -42,39 +47,77 @@ qed. definition DeqNat ≝ mk_DeqSet nat eqb eqbnat_true. -let rec enumn n ≝ - match n with [ O ⇒ [ ] | S p ⇒ p::enumn p ]. +lemma lt_to_le : ∀n,m. n < m → n ≤ m. +/2/ qed-. + +let rec enumnaux n m ≝ + match n return (λn.n ≤ m → list (Σx.x < m)) with + [ O ⇒ λh.[ ] | S p ⇒ λh:p < m.(mk_Sig ?? p h)::enumnaux p m (lt_to_le p m h)]. + +definition enumn ≝ λn.enumnaux n n (le_n n). + +definition Nat_to ≝ λn. DeqSig DeqNat (λi.iHfalse @le_n |<(notb_notb (memb …)) >Hind normalize /2/ ] +qed. + + +lemma enumn_unique_aux: ∀n,m. ∀h:n ≤ m. uniqueb (Nat_to m) (enumnaux n m h) = true. +#n elim n -n // #n #Hind #m #h @true_to_andb_true // @memb_enumn // qed. - -lemma enumn_unique: ∀n. uniqueb DeqNat (enumn n) = true. -#n elim n // #m #Hind @true_to_andb_true /2/ + +lemma enumn_unique: ∀n.uniqueb (Nat_to n) (enumn n) = true. +#n @enumn_unique_aux qed. -definition initN ≝ λn.mk_FinSet DeqNat (enumn n) (enumn_unique n). - -example tipa: ∀n.∃x: initN (S n). x = n. -#n @(ex_intro … n) // qed. +(* definition ltb ≝ λn,m.leb (S n) m. *) +lemma enumn_complete_aux: ∀n,m,i.∀h:n ≤m.∀k:iHcut @Hind // + |#eqin cut (eqb (Nat_to m) (mk_Sig ?? i k) (mk_Sig ?? n h) = true) + [normalize @eq_to_eqb_true // + |#Hcut >Hcut % + ] + ] +qed. -example inject : ∃f: initN 2 → initN 4. injective ?? f. -@(ex_intro … S) // +lemma enumn_complete: ∀n.∀i:Nat_to n. memb ? i (enumn n) = true. +#n whd in ⊢ (%→?); * #i #ltin @enumn_complete_aux // qed. +definition initN ≝ λn. + mk_FinSet (Nat_to n) (enumn n) (enumn_unique n) (enumn_complete n). + +example tipa: ∀n.∃x: initN (S n). pi1 … x = n. +#n @ex_intro [whd @mk_Sig [@n | @le_n] | //] qed. + (* sum *) 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 = +lemma enum_sum_def : ∀A,B:FinSet.∀l1,l2. enum_sum A B l1 l2 = (map ?? (inl A B) l1) @ (map ?? (inr A B) l2). // qed. -lemma enumAB_unique: ∀A,B:DeqSet.∀l1,l2. +lemma enum_sum_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 @@ -97,10 +140,21 @@ lemma enumAB_unique: ∀A,B:DeqSet.∀l1,l2. ] qed. +lemma enum_sum_complete: ∀A,B:DeqSet.∀l1,l2. + (∀x:A. memb A x l1 = true) → + (∀x:B. memb B x l2 = true) → + ∀x:DeqSum A B. memb ? x (enum_sum A B l1 l2) = true. +#A #B #l1 #l2 #Hl1 #Hl2 * + [#a @memb_append_l1 @memb_map @Hl1 + |#b @memb_append_l2 @memb_map @Hl2 + ] +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)). + (enum_sum_unique … (enum_unique A) (enum_unique B)) + (enum_sum_complete … (enum_complete A) (enum_complete B)). include alias "basics/types.ma". @@ -120,10 +174,17 @@ axiom enum_prod_unique: ∀A,B,l1,l2. uniqueb A l1 = true → uniqueb B l2 = true → uniqueb ? (enum_prod A B l1 l2) = true. +lemma enum_prod_complete:∀A,B:DeqSet.∀l1,l2. + (∀a. memb A a l1 = true) → (∀b.memb B b l2 = true) → + ∀p. memb ? p (enum_prod A B l1 l2) = true. +#A #B #l1 #l2 #Hl1 #Hl2 * #a #b @memb_compose // +qed. + definition FinProd ≝ λA,B:FinSet.mk_FinSet (DeqProd A B) (enum_prod A B (enum A) (enum B)) - (enum_prod_unique A B (enum A) (enum B) (enum_unique A) (enum_unique B) ). + (enum_prod_unique A B … (enum_unique A) (enum_unique B)) + (enum_prod_complete A B … (enum_complete A) (enum_complete B)). unification hint 0 ≔ C1,C2; T1 ≟ FinSetcarr C1, diff --git a/matita/matita/lib/basics/types.ma b/matita/matita/lib/basics/types.ma index b7a022ad2..94777e071 100644 --- a/matita/matita/lib/basics/types.ma +++ b/matita/matita/lib/basics/types.ma @@ -79,6 +79,9 @@ lemma sub_pi2 : ∀A.∀P,P':A → Prop. (∀x.P x → P' x) → ∀x:Σx:A.P x. #A #P #P' #H1 * #x #H2 @H1 @H2 qed. +lemma inj_mk_Sig: ∀A,P.∀x. x = mk_Sig A P (pi1 A P x) (pi2 A P x). +#A #P #x cases x // +qed-. (* Prod *) record Prod (A,B:Type[0]) : Type[0] ≝ {