From: Andrea Asperti Date: Mon, 28 May 2012 11:25:09 +0000 (+0000) Subject: FinOpt X-Git-Tag: make_still_working~1687 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=347a03a55e60c5a4682e0133454ff87ce21a4e8c;p=helm.git FinOpt --- diff --git a/matita/matita/lib/basics/deqsets.ma b/matita/matita/lib/basics/deqsets.ma index dc0044edc..fcc89f312 100644 --- a/matita/matita/lib/basics/deqsets.ma +++ b/matita/matita/lib/basics/deqsets.ma @@ -114,6 +114,7 @@ unification hint 0 ≔ T,a1,a2; (* ---------------------------------------- *) ⊢ eq_option T a1 a2 ≡ eqb X a1 a2. + (* pairs *) definition eq_pairs ≝ λA,B:DeqSet.λp1,p2:A×B.(\fst p1 == \fst p2) ∧ (\snd p1 == \snd p2). diff --git a/matita/matita/lib/basics/finset.ma b/matita/matita/lib/basics/finset.ma index b8f698110..babbf997c 100644 --- a/matita/matita/lib/basics/finset.ma +++ b/matita/matita/lib/basics/finset.ma @@ -109,6 +109,46 @@ definition initN ≝ λn. example tipa: ∀n.∃x: initN (S n). pi1 … x = n. #n @ex_intro [whd @mk_Sig [@n | @le_n] | //] qed. +(* option *) +definition enum_option ≝ λA:DeqSet.λl. + None A::(map ?? (Some A) l). + +lemma enum_option_def : ∀A:FinSet.∀l. + enum_option A l = None A :: (map ?? (Some A) l). +// qed. + +lemma enum_option_unique: ∀A:DeqSet.∀l. + uniqueb A l = true → + uniqueb ? (enum_option A l) = true. +#A #l #uA @true_to_andb_true + [generalize in match uA; -uA #_ elim l [%] + #a #tl #Hind @sym_eq @noteq_to_eqnot % #H + cases (orb_true_l … (sym_eq … H)) + [#H1 @(absurd (None A = Some A a)) [@(\P H1) | % #H2 destruct] + |-H #H >H in Hind; normalize /2/ + ] + |@unique_map_inj // #a #a1 #H destruct % + ] +qed. + +lemma enum_option_complete: ∀A:DeqSet.∀l. + (∀x:A. memb A x l = true) → + ∀x:DeqOption A. memb ? x (enum_option A l) = true. +#A #l #Hl * // #a @memb_cons @memb_map @Hl +qed. + +definition FinOption ≝ λA:FinSet. + mk_FinSet (DeqOption A) + (enum_option A (enum A)) + (enum_option_unique … (enum_unique A)) + (enum_option_complete … (enum_complete A)). + +unification hint 0 ≔ C; + T ≟ FinSetcarr C, + X ≟ FinOption C +(* ---------------------------------------- *) ⊢ + option T ≡ FinSetcarr X. + (* sum *) definition enum_sum ≝ λA,B:DeqSet.λl1.λl2. (map ?? (inl A B) l1) @ (map ?? (inr A B) l2). diff --git a/matita/matita/lib/basics/lists/listb.ma b/matita/matita/lib/basics/lists/listb.ma index 640f1391c..ac72b008b 100644 --- a/matita/matita/lib/basics/lists/listb.ma +++ b/matita/matita/lib/basics/lists/listb.ma @@ -103,6 +103,15 @@ lemma memb_compose: ∀S1,S2,S3,op,a1,a2,l1,l2. ] qed. +lemma mem_to_memb: ∀S:DeqSet.∀a,l. mem S a l → memb S a l = true. +#S #a #l elim l normalize + [@False_ind + |#hd #tl #Hind * + [#eqa >(\b eqa) % + |#Hmem cases (a==hd) // normalize /2/ + ] + ] +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 94777e071..b319b5bd0 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 ; pi2: f pi1 }.