X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=weblib%2Fbasics%2Ftypes.ma;h=17c211675eb1d9b3c21fa573e4446d7f60c7ebc9;hb=c0ac63fead67ea1902e3d923ce877a2779cf501e;hp=ed324db0e3fb12ab52b118ef99b85fd8a163469a;hpb=7f6235dca57343e63217316b6415599daef7d4aa;p=helm.git

diff --git a/weblib/basics/types.ma b/weblib/basics/types.ma
index ed324db0e..17c211675 100644
--- a/weblib/basics/types.ma
+++ b/weblib/basics/types.ma
@@ -12,51 +12,51 @@
 include "basics/logic.ma".
 
 (* void *)
-inductive void : Type[0] ≝.
+img class="anchor" src="icons/tick.png" id="void"inductive void : Type[0] ≝.
 
 (* unit *)
-inductive unit : Type[0] ≝ it: unit.
+img class="anchor" src="icons/tick.png" id="unit"inductive unit : Type[0] ≝ it: unit.
 
 (* sum *)
-inductive Sum (A,B:Type[0]) : Type[0] ≝
+img class="anchor" src="icons/tick.png" id="Sum"inductive Sum (A,B:Type[0]) : Type[0] ≝
   inl : A → Sum A B
 | inr : B → Sum A B.
 
 interpretation "Disjoint union" 'plus A B = (Sum A B).
 
 (* option *)
-inductive option (A:Type[0]) : Type[0] ≝
+img class="anchor" src="icons/tick.png" id="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) ].
+img class="anchor" src="icons/tick.png" id="option_map"definition option_map : ∀A,B:Type[0]. (A → B) → a href="cic:/matita/basics/types/option.ind(1,0,1)"option/a A → a href="cic:/matita/basics/types/option.ind(1,0,1)"option/a B ≝
+λA,B,f,o. match o with [ None ⇒ a href="cic:/matita/basics/types/option.con(0,1,1)"None/a B | Some a ⇒ a href="cic:/matita/basics/types/option.con(0,2,1)"Some/a B (f a) ].
 
-lemma option_map_none : ∀A,B,f,x.
-  option_map A B f x = None B → x = None A.
+img class="anchor" src="icons/tick.png" id="option_map_none"lemma option_map_none : ∀A,B,f,x.
+  a href="cic:/matita/basics/types/option_map.def(1)"option_map/a A B f x a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/types/option.con(0,1,1)"None/a B → x a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/types/option.con(0,1,1)"None/a 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.
+img class="anchor" src="icons/tick.png" id="option_map_some"lemma option_map_some : ∀A,B,f,x,v.
+  a href="cic:/matita/basics/types/option_map.def(1)"option_map/a A B f x a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/types/option.con(0,2,1)"Some/a B v → a title="exists" href="cic:/fakeuri.def(1)"∃/ay. x a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/types/option.con(0,2,1)"Some/a ? y a title="logical and" href="cic:/fakeuri.def(1)"∧/a f y a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a 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 ≝
+img class="anchor" src="icons/tick.png" id="option_map_def"definition option_map_def : ∀A,B:Type[0]. (A → B) → B → a href="cic:/matita/basics/types/option.ind(1,0,1)"option/a 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)).
+img class="anchor" src="icons/tick.png" id="refute_none_by_refl"lemma refute_none_by_refl : ∀A,B:Type[0]. ∀P:A → B. ∀Q:B → Type[0]. ∀x:a href="cic:/matita/basics/types/option.ind(1,0,1)"option/a A. ∀H:x a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/types/option.con(0,1,1)"None/a ? → a href="cic:/matita/basics/logic/False.ind(1,0,0)"False/a.
+  (∀v. x a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/types/option.con(0,2,1)"Some/a ? v → Q (P v)) →
+  Q (match x return λy.x a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a y → ? with [ Some v ⇒ λ_. P v | None ⇒ λE. match H E in False with [ ] ] (a href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/a ? x)).
 #A #B #P #Q *
-[ #H cases (H (refl ??))
-| #a #H #p normalize @p @refl
+[ #H cases (H (a href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/a ??))
+| #a #H #p normalize @p @a href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/a
 ] qed.
 
 (* sigma *)
-record Sig (A:Type[0]) (f:A→Type[0]) : Type[0] ≝ {
+img class="anchor" src="icons/tick.png" id="Sig"record Sig (A:Type[0]) (f:A→Type[0]) : Type[0] ≝ {
     pi1: A
   ; pi2: f pi1
   }.
@@ -70,7 +70,7 @@ interpretation "mk_Sig" 'dp x y = (mk_Sig ?? x y).
 
 (* Prod *)
 
-record Prod (A,B:Type[0]) : Type[0] ≝ {
+img class="anchor" src="icons/tick.png" id="Prod"record Prod (A,B:Type[0]) : Type[0] ≝ {
    fst: A
  ; snd: B
  }.
@@ -99,94 +99,94 @@ 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 〉.
+img class="anchor" src="icons/tick.png" id="eq_pair_fst_snd"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 a title="Pair construction" href="cic:/fakeuri.def(1)"〉/a.
 #A #B #p (cases p) // qed.
 
-lemma fst_eq : ∀A,B.∀a:A.∀b:B. \fst 〈a,b〉 = a.
+img class="anchor" src="icons/tick.png" id="fst_eq"lemma fst_eq : ∀A,B.∀a:A.∀b:B. a title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aa,ba title="Pair construction" href="cic:/fakeuri.def(1)"〉/a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a.
 // qed.
 
-lemma snd_eq : ∀A,B.∀a:A.∀b:B. \snd 〈a,b〉 = b.
+img class="anchor" src="icons/tick.png" id="snd_eq"lemma snd_eq : ∀A,B.∀a:A.∀b:B. a title="pair pi2" href="cic:/fakeuri.def(1)"\snd/a a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aa,ba title="Pair construction" href="cic:/fakeuri.def(1)"〉/a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a b.
 // qed.
 
-notation > "hvbox('let' 〈ident x,ident y〉 ≝ t 'in' s)"
+notation > "hvbox('let' 〈ident x,ident y〉 ≝ t 'in' s)"
  with precedence 10
 for @{ match $t with [ mk_Prod ${ident x} ${ident y} ⇒ $s ] }.
 
-notation < "hvbox('let' \nbsp hvbox(〈ident x,ident y〉 \nbsp≝ break t \nbsp 'in' \nbsp) break s)"
+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)"
+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] ≝
+img class="anchor" src="icons/tick.png" id="PSig"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)"
+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)"
+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)"
+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)"
+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)"
+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.
+img class="anchor" src="icons/tick.png" id="contract_pair"example contract_pair : ∀A,B.∀e:Aa title="Product" href="cic:/fakeuri.def(1)"×/aB. (let 〈a,b〉 ≝ e in a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aa,ba title="Pair construction" href="cic:/fakeuri.def(1)"〉/a) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a 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.
+img class="anchor" src="icons/tick.png" id="extract_pair"lemma extract_pair : ∀A,B,C,D.  ∀u:Aa title="Product" href="cic:/fakeuri.def(1)"×/aB. ∀Q:A → B → Ca title="Product" href="cic:/fakeuri.def(1)"×/aD. ∀x,y.
+((let 〈a,b〉 ≝ u in Q a b) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="Pair construction" href="cic:/fakeuri.def(1)"〈/ax,ya title="Pair construction" href="cic:/fakeuri.def(1)"〉/a) →
+a title="exists" href="cic:/fakeuri.def(1)"∃/aa,ba title="exists" href="cic:/fakeuri.def(1)"./a a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aa,ba title="Pair construction" href="cic:/fakeuri.def(1)"〉/a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a u a title="logical and" href="cic:/fakeuri.def(1)"∧/a Q a b a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="Pair construction" href="cic:/fakeuri.def(1)"〈/ax,ya title="Pair construction" href="cic:/fakeuri.def(1)"〉/a.
+#A #B #C #D * #a #b #Q #x #y normalize #E1 %{a} %{b} % try @a href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/a @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/
+img class="anchor" src="icons/tick.png" id="breakup_pair"lemma breakup_pair : ∀A,B,C:Type[0].∀x. ∀R:C → Prop. ∀P:A → B → C.
+  R (P (a title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a x) (a title="pair pi2" href="cic:/fakeuri.def(1)"\snd/a x)) → R (let 〈a,b〉 ≝ x in P a b).
+#A #B #C *; normalize /span class="autotactic"2span class="autotrace" trace /span/span/
 qed.
 
-lemma pair_elim:
+img class="anchor" src="icons/tick.png" id="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/
+  ∀P: Aa title="Product" href="cic:/fakeuri.def(1)"×/aB → C → Prop.
+    (∀lft, rgt. p a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="Pair construction" href="cic:/fakeuri.def(1)"〈/alft,rgta title="Pair construction" href="cic:/fakeuri.def(1)"〉/a → P a title="Pair construction" href="cic:/fakeuri.def(1)"〈/alft,rgta title="Pair construction" href="cic:/fakeuri.def(1)"〉/a (T lft rgt)) →
+      P p (let 〈lft, rgt〉 ≝ p in T lft rgt).
+ #A #B #C #T * /span class="autotactic"2span class="autotrace" trace /span/span/
 qed.
 
-lemma pair_elim2:
+img class="anchor" src="icons/tick.png" id="pair_elim2"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.
+  ∀P: Aa title="Product" href="cic:/fakeuri.def(1)"×/aB → C → C' → Prop.
+    (∀lft, rgt. p a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="Pair construction" href="cic:/fakeuri.def(1)"〈/alft,rgta title="Pair construction" href="cic:/fakeuri.def(1)"〉/a → P a title="Pair construction" href="cic:/fakeuri.def(1)"〈/alft,rgta title="Pair construction" href="cic:/fakeuri.def(1)"〉/a (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' * /span class="autotactic"2span class="autotrace" trace /span/span/
+qed.
\ No newline at end of file