propagating the arithmetics library, partial commit

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

diff --git a/matita/matita/lib/basics/types.ma b/matita/matita/lib/basics/types.ma
index 0cf9aeadda497de167dfff2413e6981dee39c9bb..efc213f95da759cb305ef3d1522ee13691de78e0 100644 (file)
--- a/matita/matita/lib/basics/types.ma
+++ b/matita/matita/lib/basics/types.ma
@@ -9,6 +9,7 @@
      \ /   GNU General Public License Version 2   
       V_______________________________________________________________ *)
 
+include "basics/core_notation/pair_2.ma".
 include "basics/logic.ma".
 
 (* void *)
@@ -29,12 +30,59 @@ inductive option (A:Type[0]) : Type[0] ≝
    None : option A
  | Some : A → option A.
 
+definition option_map : ∀A,B:Type[0]. (A → B) → option A → option B ≝
+λA,B,f,o. match o with [ None ⇒ None B | Some a ⇒ Some B (f a) ].
+
+lemma option_map_none : ∀A,B,f,x.
+  option_map A B f x = None B → x = None A.
+#A #B #f * [ // | #a #E whd in E:(??%?); destruct ]
+qed.
+
+lemma option_map_some : ∀A,B,f,x,v.
+  option_map A B f x = Some B v → ∃y. x = Some ? y ∧ f y = v.
+#A #B #f *
+[ #v normalize #E destruct
+| #y #v normalize #E %{y} destruct % //
+] qed.
+
+definition option_map_def : ∀A,B:Type[0]. (A → B) → B → option A → B ≝
+λA,B,f,d,o. match o with [ None ⇒ d | Some a ⇒ f a ].
+
+lemma refute_none_by_refl : ∀A,B:Type[0]. ∀P:A → B. ∀Q:B → Type[0]. ∀x:option A. ∀H:x = None ? → False.
+  (∀v. x = Some ? v → Q (P v)) →
+  Q (match x return λy.x = y → ? with [ Some v ⇒ λ_. P v | None ⇒ λE. match H E in False with [ ] ] (refl ? x)).
+#A #B #P #Q *
+[ #H cases (H (refl ??))
+| #a #H #p normalize @p @refl
+] qed.
+
+(* dependent pair *)
+record DPair (A:Type[0]) (f:A→Type[0]) : Type[0] ≝ {
+    dpi1:> A
+  ; dpi2: f dpi1
+  }.
+
+interpretation "DPair" 'dpair x = (DPair ? x).
+
+interpretation "mk_DPair" 'mk_DPair x y = (mk_DPair ?? x y).
+
 (* sigma *)
-inductive Sig (A:Type[0]) (f:A→Type[0]) : Type[0] ≝
-  dp: ∀a:A.(f a)→Sig A f.
+record Sig (A:Type[0]) (f:A→Prop) : Type[0] ≝ {
+    pi1: A  (* not a coercion due to problems with Cerco *)
+  ; pi2: f pi1
+  }.
   
 interpretation "Sigma" 'sigma x = (Sig ? x).
 
+interpretation "mk_Sig" 'dp x y = (mk_Sig ?? x y).
+
+lemma sub_pi2 : ∀A.∀P,P':A → Prop. (∀x.P x → P' x) → ∀x:Σx:A.P x. P' (pi1 … 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] ≝ {
@@ -101,15 +149,15 @@ for @{ match $t return λx.x = $t → ? with [ mk_Prod ${fresh xy} ${ident z} 
        match ${fresh xy} return λx. ? = $t → ? with [ mk_Prod ${ident x} ${ident y} ⇒
         λ${ident E}.$s ] ] (refl ? $t) }.
 
-notation < "hvbox('let' \nbsp hvbox(〈ident x,ident y,ident z〉 \nbsp'as'\nbsp ident E\nbsp ≝ break t \nbsp 'in' \nbsp) break s)"
+notation < "hvbox('let' \nbsp hvbox(〈ident x,ident y,ident z〉 \nbsp 'as' \nbsp ident E\nbsp ≝ break t \nbsp 'in' \nbsp) break s)"
  with precedence 10
-for @{ match $t return λ${ident x}.$eq $T $x $t → $U with [ mk_Prod (${fresh xy}:$V) (${ident z}:$Z) ⇒
-       match ${fresh xy} return λ${ident y}. $eq $R $r $t → ? with [ mk_Prod (${ident x}:$L) (${ident y}:$I) ⇒
+for @{ match $t return λ${ident k}:$X.$eq $T $k $t → $U with [ mk_Prod (${ident xy}:$V) (${ident z}:$Z) ⇒
+       match $xy return λ${ident a}. $eq $R $r $t → ? with [ mk_Prod (${ident x}:$L) (${ident y}:$I) ⇒
         λ${ident E}:$J.$s ] ] ($refl $A $t) }.
 
 notation > "hvbox('let' 〈ident w,ident x,ident y,ident z〉 ≝ t 'in' s)"
  with precedence 10
-for @{ match $t with [ mk_Prod ${fresh wx} ${fresh yz} ⇒ match ${fresh wx} with [ mk_Prod ${ident w} ${ident x} ⇒ match ${fresh yz} with [ pair ${ident y} ${ident z} ⇒ $s ] ] ] }.
+for @{ match $t with [ mk_Prod ${fresh wx} ${fresh yz} ⇒ match ${fresh wx} with [ mk_Prod ${ident w} ${ident x} ⇒ match ${fresh yz} with [ mk_Prod ${ident y} ${ident z} ⇒ $s ] ] ] }.
 
 notation > "hvbox('let' 〈ident x,ident y,ident z〉 ≝ t 'in' s)"
  with precedence 10
@@ -131,8 +179,17 @@ lemma breakup_pair : ∀A,B,C:Type[0].∀x. ∀R:C → Prop. ∀P:A → B → C.
 #A #B #C *; normalize /2/
 qed.
 
-(* Is this necessary?
-axiom pair_elim'':
+lemma pair_elim:
+  ∀A,B,C: Type[0].
+  ∀T: A → B → C.
+  ∀p.
+  ∀P: A×B → C → Prop.
+    (∀lft, rgt. p = 〈lft,rgt〉 → P 〈lft,rgt〉 (T lft rgt)) →
+      P p (let 〈lft, rgt〉 ≝ p in T lft rgt).
+ #A #B #C #T * /2/
+qed.
+
+lemma pair_elim2:
   ∀A,B,C,C': Type[0].
   ∀T: A → B → C.
   ∀T': A → B → C'.
@@ -140,7 +197,8 @@ axiom pair_elim'':
   ∀P: A×B → C → C' → Prop.
     (∀lft, rgt. p = 〈lft,rgt〉 → P 〈lft,rgt〉 (T lft rgt) (T' lft rgt)) →
       P p (let 〈lft, rgt〉 ≝ p in T lft rgt) (let 〈lft, rgt〉 ≝ p in T' lft rgt).
-*)
+ #A #B #C #C' #T #T' * /2/
+qed.
 
 (* Useful for avoiding destruct's full normalization. *)
 lemma pair_eq1: ∀A,B. ∀a1,a2:A. ∀b1,b2:B. 〈a1,b1〉 = 〈a2,b2〉 → a1 = a2.
@@ -159,4 +217,11 @@ qed.
 lemma pair_destruct_2:
  ∀A,B.∀a:A.∀b:B.∀c. 〈a,b〉 = c → b = \snd c.
  #A #B #a #b *; /2/
-qed.
\ No newline at end of file
+qed.
+
+lemma coerc_pair_sigma:
+ ∀A,B,P. ∀p:A × B. P (\snd p) → A × (Σx:B.P x).
+#A #B #P * #a #b #p % [@a | /2/]
+qed.
+coercion coerc_pair_sigma:∀A,B,P. ∀p:A × B. P (\snd p) → A × (Σx:B.P x)
+≝ coerc_pair_sigma on p: (? × ?) to (? × (Sig ??)).