From 347a03a55e60c5a4682e0133454ff87ce21a4e8c Mon Sep 17 00:00:00 2001
From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Mon, 28 May 2012 11:25:09 +0000
Subject: [PATCH] FinOpt

---
 matita/matita/lib/basics/deqsets.ma     |  1 +
 matita/matita/lib/basics/finset.ma      | 40 +++++++++++++++++++++++++
 matita/matita/lib/basics/lists/listb.ma |  9 ++++++
 matita/matita/lib/basics/types.ma       |  2 +-
 4 files changed, 51 insertions(+), 1 deletion(-)

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
   }.
   
-- 
2.39.2