More stuff integrated from CerCo on sigma types (that are now a record)

and option.

diff --git a/matita/matita/lib/basics/lists/list.ma b/matita/matita/lib/basics/lists/list.ma
index 01766b9eceaaa6fe032c5cd4afd8f4ced07e71bc..fa9e8bfee3c32290ccf54dcef5f7faca56a53c5b 100644 (file)
--- a/matita/matita/lib/basics/lists/list.ma
+++ b/matita/matita/lib/basics/lists/list.ma
@@ -117,7 +117,7 @@ theorem eq_map : ∀A,B,f,g,l. (∀x.f x = g x) → map A B f l = map A B g l.
 let rec dprodl (A:Type[0]) (f:A→Type[0]) (l1:list A) (g:(∀a:A.list (f a))) on l1 ≝
 match l1 with
   [ nil ⇒ nil ?
-  | cons a tl ⇒ (map ??(dp ?? a) (g a)) @ dprodl A f tl g
+  | cons a tl ⇒ (map ??(mk_Sig ?? a) (g a)) @ dprodl A f tl g
   ].
 
 (**************************** length ******************************)

diff --git a/matita/matita/lib/basics/types.ma b/matita/matita/lib/basics/types.ma
index 060ebb06e84844c5582af4b89b37fb581f7d0ea1..bfcf7731f50d2e2fec9fbce5ab928c7913897d46 100644 (file)
--- a/matita/matita/lib/basics/types.ma
+++ b/matita/matita/lib/basics/types.ma
@@ -29,12 +29,45 @@ 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.
+
 (* 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→Type[0]) : Type[0] ≝ {
+    pi1: A
+  ; pi2: f pi1
+  }.
   
 interpretation "Sigma" 'sigma x = (Sig ? x).
 
+notation "hvbox(« term 19 a, break term 19 b»)" 
+with precedence 90 for @{ 'dp $a $b }.
+
+interpretation "mk_Sig" 'dp x y = (mk_Sig ?? x y).
+
 (* Prod *)
 
 record Prod (A,B:Type[0]) : Type[0] ≝ {