Progress

[helm.git] / matita / matita / lib / basics / deqsets.ma

diff --git a/matita/matita/lib/basics/deqsets.ma b/matita/matita/lib/basics/deqsets.ma
index 4d86c9f6caada32726c9153fffc8ea40b5b5b7a7..45afabe59ad9555e55f863c8b9e3a584c5ac5963 100644 (file)
--- 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
 (* ---------------------------------------- *) ⊢ 
@@ -100,4 +105,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.
+