X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Fbasics%2Fdeqsets.ma;h=fb6ad5be4fe3f11a678f11e62cea79b14ba8cfb6;hb=2f8eacc69333b13fe143cc007681f21464e06529;hp=4d86c9f6caada32726c9153fffc8ea40b5b5b7a7;hpb=dec09d382f401b62b3ee183c9b60b883d0d33255;p=helm.git

diff --git a/matita/matita/lib/basics/deqsets.ma b/matita/matita/lib/basics/deqsets.ma
index 4d86c9f6c..fb6ad5be4 100644
--- a/matita/matita/lib/basics/deqsets.ma
+++ b/matita/matita/lib/basics/deqsets.ma
@@ -28,6 +28,10 @@ notation "\P H" non associative with precedence 90
 notation "\b H" non associative with precedence 90 
   for @{(proj2 … (eqb_true ???) $H)}. 
   
+notation < "𝐃" non associative with precedence 90 
+ for @{'bigD}.
+interpretation "DeqSet" 'bigD = (mk_DeqSet ???).
+  
 lemma eqb_false: ∀S:DeqSet.∀a,b:S. 
   (eqb ? a b) = false ↔ a ≠ b.
 #S #a #b % #H 
@@ -57,6 +61,7 @@ qed.
 
 definition DeqBool ≝ mk_DeqSet bool beqb beqb_true.
 
+alias symbol "hint_decl" (instance 1) = "hint_decl_Type1".
 unification hint  0 ≔ ; 
     X ≟ mk_DeqSet bool beqb beqb_true
 (* ---------------------------------------- *) ⊢ 
@@ -71,6 +76,45 @@ example exhint: ∀b:bool. (b == false) = true → b = false.
 #b #H @(\P H).
 qed.
 
+(* option *)
+
+definition eq_option ≝
+  λA:DeqSet.λa1,a2:option A.
+    match a1 with 
+    [ None ⇒ match a2 with [None ⇒ true | _ ⇒ false]
+    | Some a1' ⇒ match a2 with [None ⇒ false | Some a2' ⇒ a1'==a2']].
+
+lemma eq_option_true: ∀A:DeqSet.∀a1,a2:option A.
+  eq_option A a1 a2 = true ↔ a1 = a2.
+#A *
+  [* 
+    [% //
+    |#a1 % normalize #H destruct 
+    ]
+  |#a1 *  
+    [normalize % #H destruct
+    |#a2 normalize %
+      [#Heq >(\P Heq) //
+      |#H destruct @(\b ?) //
+      ]
+  ]
+qed.
+
+definition DeqOption ≝ λA:DeqSet.
+  mk_DeqSet (option A) (eq_option A) (eq_option_true A).
+  
+unification hint  0 ≔ C; 
+    T ≟ carr C,
+    X ≟ DeqOption C
+(* ---------------------------------------- *) ⊢ 
+    option T ≡ carr X.
+
+unification hint  0 ≔ T,a1,a2; 
+    X ≟ DeqOption T
+(* ---------------------------------------- *) ⊢ 
+    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).
@@ -100,4 +144,79 @@ 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.
+
+(* 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.
+*)