From: matitaweb <claudio.sacerdoticoen@unibo.it>
Date: Fri, 2 Mar 2012 15:02:54 +0000 (+0000)
Subject: commit by user andrea
X-Git-Tag: make_still_working~1916
X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=fc43587e06d59afb5b1c65904372843d928fdfe5

commit by user andrea
---

diff --git a/weblib/basics/types.ma b/weblib/basics/types.ma
index a07cf29ea..ed324db0e 100644
--- a/weblib/basics/types.ma
+++ b/weblib/basics/types.ma
@@ -17,19 +17,67 @@ inductive void : Type[0] ≝.
 (* unit *)
 inductive unit : Type[0] ≝ it: unit.
 
-(* Prod *)
-inductive Prod (A,B:Type[0]) : Type[0] ≝
-pair : A → B → Prod A B.
+(* sum *)
+inductive Sum (A,B:Type[0]) : Type[0] ≝
+  inl : A → Sum A B
+| inr : B → Sum A B.
 
-interpretation "Pair construction" 'pair x y = (pair ? ? x y).
+interpretation "Disjoint union" 'plus A B = (Sum A B).
 
-interpretation "Product" 'product x y = (Prod x y).
+(* option *)
+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.
 
-definition fst ≝ λA,B.λp:A a title="Product" href="cic:/fakeuri.def(1)"×/a B.
-  match p with [pair a b ⇒ a]. 
+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 snd ≝ λA,B.λp:A a title="Product" href="cic:/fakeuri.def(1)"×/a B.
-  match p with [pair a b ⇒ b].
+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 *)
+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] ≝ {
+   fst: A
+ ; snd: B
+ }.
+
+interpretation "Pair construction" 'pair x y = (mk_Prod ? ? x y).
+
+interpretation "Product" 'product x y = (Prod x y).
 
 interpretation "pair pi1" 'pi1 = (fst ? ?).
 interpretation "pair pi2" 'pi2 = (snd ? ?).
@@ -38,24 +86,107 @@ interpretation "pair pi2" 'pi2a x = (snd ? ? x).
 interpretation "pair pi1" 'pi1b x y = (fst ? ? x y).
 interpretation "pair pi2" 'pi2b x y = (snd ? ? x y).
 
-theorem eq_pair_fst_snd: ∀A,B.∀p:A a title="Product" href="cic:/fakeuri.def(1)"×/a B.
-  p a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="Pair construction" href="cic:/fakeuri.def(1)"〈/a a title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a p, a title="pair pi2" href="cic:/fakeuri.def(1)"\snd/a p 〉.
+notation "π1" with precedence 10 for @{ (proj1 ??) }.
+notation "π2" with precedence 10 for @{ (proj2 ??) }.
+
+(* Yeah, I probably ought to do something more general... *)
+notation "hvbox(\langle term 19 a, break term 19 b, break term 19 c\rangle)"
+with precedence 90 for @{ 'triple $a $b $c}.
+interpretation "Triple construction" 'triple x y z = (mk_Prod ? ? (mk_Prod ? ? x y) z).
+
+notation "hvbox(\langle term 19 a, break term 19 b, break term 19 c, break term 19 d\rangle)"
+with precedence 90 for @{ 'quadruple $a $b $c $d}.
+interpretation "Quadruple construction" 'quadruple w x y z = (mk_Prod ? ? (mk_Prod ? ? w x) (mk_Prod ? ? y z)).
+
+
+theorem eq_pair_fst_snd: ∀A,B.∀p:A × B.
+  p = 〈 \fst p, \snd p 〉.
 #A #B #p (cases p) // qed.
 
-(* sum *)
-inductive Sum (A,B:Type[0]) : Type[0] ≝
-  inl : A → Sum A B
-| inr : B → Sum A B.
+lemma fst_eq : ∀A,B.∀a:A.∀b:B. \fst 〈a,b〉 = a.
+// qed.
 
-interpretation "Disjoint union" 'plus A B = (Sum A B).
+lemma snd_eq : ∀A,B.∀a:A.∀b:B. \snd 〈a,b〉 = b.
+// qed.
 
-(* option *)
-inductive option (A:Type[0]) : Type[0] ≝
-   None : option A
- | Some : A → option A.
+notation > "hvbox('let' 〈ident x,ident y〉 ≝ t 'in' s)"
+ with precedence 10
+for @{ match $t with [ mk_Prod ${ident x} ${ident y} ⇒ $s ] }.
 
-(* sigma *)
-inductive Sig (A:Type[0]) (f:A→Type[0]) : Type[0] ≝
-  dp: ∀a:A.(f a)→Sig A f.
+notation < "hvbox('let' \nbsp hvbox(〈ident x,ident y〉 \nbsp≝ break t \nbsp 'in' \nbsp) break s)"
+ with precedence 10
+for @{ match $t with [ mk_Prod (${ident x}:$X) (${ident y}:$Y) ⇒ $s ] }.
+
+(* Also extracts an equality proof (useful when not using Russell). *)
+notation > "hvbox('let' 〈ident x,ident y〉 'as' ident E ≝ t 'in' s)"
+ with precedence 10
+for @{ match $t return λx.x = $t → ? with [ mk_Prod ${ident x} ${ident y} ⇒
+        λ${ident E}.$s ] (refl ? $t) }.
+
+(* Prop sigma *)
+record PSig (A:Type[0]) (P:A→Prop) : Type[0] ≝
+  {elem:>A; eproof: P elem}.
+  
+interpretation "subset type" 'sigma x = (PSig ? x).
+
+notation < "hvbox('let' \nbsp hvbox(〈ident x,ident y〉 \nbsp 'as'\nbsp ident E\nbsp ≝ break t \nbsp 'in' \nbsp) break s)"
+ with precedence 10
+for @{ match $t return λ${ident k}:$X.$eq $T $k $t → ? with [ mk_Prod (${ident x}:$U) (${ident y}:$W) ⇒
+        λ${ident E}:$e.$s ] ($refl $T $t) }.
+
+notation > "hvbox('let' 〈ident x,ident y,ident z〉 'as' ident E ≝ t 'in' s)"
+ with precedence 10
+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)"
+ 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) ⇒
+        λ${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 [ mk_Prod ${ident y} ${ident z} ⇒ $s ] ] ] }.
+
+notation > "hvbox('let' 〈ident x,ident y,ident z〉 ≝ t 'in' s)"
+ with precedence 10
+for @{ match $t with [ mk_Prod ${fresh xy} ${ident z} ⇒ match ${fresh xy} with [ mk_Prod ${ident x} ${ident y} ⇒ $s ] ] }.
+
+(* This appears to upset automation (previously provable results require greater
+   depth or just don't work), so use example rather than lemma to prevent it
+   being indexed. *)
+example contract_pair : ∀A,B.∀e:A×B. (let 〈a,b〉 ≝ e in 〈a,b〉) = e.
+#A #B * // qed.
+
+lemma extract_pair : ∀A,B,C,D.  ∀u:A×B. ∀Q:A → B → C×D. ∀x,y.
+((let 〈a,b〉 ≝ u in Q a b) = 〈x,y〉) →
+∃a,b. 〈a,b〉 = u ∧ Q a b = 〈x,y〉.
+#A #B #C #D * #a #b #Q #x #y normalize #E1 %{a} %{b} % try @refl @E1 qed.
+
+lemma breakup_pair : ∀A,B,C:Type[0].∀x. ∀R:C → Prop. ∀P:A → B → C.
+  R (P (\fst x) (\snd x)) → R (let 〈a,b〉 ≝ x in P a b).
+#A #B #C *; normalize /2/
+qed.
+
+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.
 
-interpretation "Sigma" 'sigma x = (Sig ? x).
\ No newline at end of file
+lemma pair_elim2:
+  ∀A,B,C,C': Type[0].
+  ∀T: A → B → C.
+  ∀T': A → B → C'.
+  ∀p.
+  ∀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.
diff --git a/weblib/tutorial/chapter7.ma b/weblib/tutorial/chapter7.ma
index 2b3df9064..a4e3a8614 100644
--- a/weblib/tutorial/chapter7.ma
+++ b/weblib/tutorial/chapter7.ma
@@ -202,7 +202,7 @@ unification hint  0 a href="cic:/fakeuri.def(1)" title="hint_decl_Type0"≔/a
     a href="cic:/matita/tutorial/chapter7/beqitem.fix(0,1,4)"beqitem/a S i1 i2 ≡ a href="cic:/matita/tutorial/chapter4/eqb.fix(0,0,3)"eqb/a X i1 i2.
 
 (* 
-h2Semantics of pointed regular expression/h2
+h2Semantics of pointed regular expressions/h2
 The intuitive semantic of a point is to mark the position where
 we should start reading the regular expression. The language associated
 to a pre is the union of the languages associated with its points. *)
diff --git a/weblib/tutorial/chapter8.ma b/weblib/tutorial/chapter8.ma
index 7aac6fabc..c0d4d91dc 100644
--- a/weblib/tutorial/chapter8.ma
+++ b/weblib/tutorial/chapter8.ma
@@ -1,3 +1,22 @@
+(*
+h1Broadcasting points/h1
+Intuitively, a regular expression e must be understood as a pointed expression with a single 
+point in front of it. Since however we only allow points before symbols, we must broadcast 
+this initial point inside e traversing all nullable subexpressions, that essentially corresponds 
+to the ϵ-closure operation on automata. We use the notation •(_) to denote such an operation;
+its definition is the expected one: let us start discussing an example.
+
+bExample/b
+Let us broadcast a point inside (a + ϵ)(b*a + b)b. We start working in parallel on the 
+first occurrence of a (where the point stops), and on ϵ that gets traversed. We have hence 
+reached the end of a + ϵ and we must pursue broadcasting inside (b*a + b)b. Again, we work in 
+parallel on the two additive subterms b^*a and b; the first point is allowed to both enter the 
+star, and to traverse it, stopping in front of a; the second point just stops in front of b. 
+No point reached that end of b^*a + b hence no further propagation is possible. In conclusion: 
+               •((a + ϵ)(b^*a + b)b) = 〈(•a + ϵ)((•b)^*•a + •b)b, false〉
+*)
+
+
 include "tutorial/chapter7.ma".
 
 definition lo ≝ λS:DeqSet.λa,b:pre S.〈\fst a + \fst b,\snd a ∨ \snd b〉.