2 ||M|| This file is part of HELM, an Hypertextual, Electronic
3 ||A|| Library of Mathematics, developed at the Computer Science
4 ||T|| Department of the University of Bologna, Italy.
8 \ / This file is distributed under the terms of the
9 \ / GNU General Public License Version 2
10 V_______________________________________________________________ *)
12 include "basics/logic.ma".
15 \ 5img class="anchor" src="icons/tick.png" id="void"
\ 6inductive void : Type[0] ≝.
18 \ 5img class="anchor" src="icons/tick.png" id="unit"
\ 6inductive unit : Type[0] ≝ it: unit.
21 \ 5img class="anchor" src="icons/tick.png" id="Sum"
\ 6inductive Sum (A,B:Type[0]) : Type[0] ≝
25 interpretation "Disjoint union" 'plus A B = (Sum A B).
28 \ 5img class="anchor" src="icons/tick.png" id="option"
\ 6inductive option (A:Type[0]) : Type[0] ≝
30 | Some : A → option A.
32 \ 5img class="anchor" src="icons/tick.png" id="option_map"
\ 6definition option_map : ∀A,B:Type[0]. (A → B) →
\ 5a href="cic:/matita/basics/types/option.ind(1,0,1)"
\ 6option
\ 5/a
\ 6 A →
\ 5a href="cic:/matita/basics/types/option.ind(1,0,1)"
\ 6option
\ 5/a
\ 6 B ≝
33 λA,B,f,o. match o with [ None ⇒
\ 5a href="cic:/matita/basics/types/option.con(0,1,1)"
\ 6None
\ 5/a
\ 6 B | Some a ⇒
\ 5a href="cic:/matita/basics/types/option.con(0,2,1)"
\ 6Some
\ 5/a
\ 6 B (f a) ].
35 \ 5img class="anchor" src="icons/tick.png" id="option_map_none"
\ 6lemma option_map_none : ∀A,B,f,x.
36 \ 5a href="cic:/matita/basics/types/option_map.def(1)"
\ 6option_map
\ 5/a
\ 6 A B f x
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 \ 5a href="cic:/matita/basics/types/option.con(0,1,1)"
\ 6None
\ 5/a
\ 6 B → x
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 \ 5a href="cic:/matita/basics/types/option.con(0,1,1)"
\ 6None
\ 5/a
\ 6 A.
37 #A #B #f * [ // | #a #E whd in E:(??%?); destruct ]
40 \ 5img class="anchor" src="icons/tick.png" id="option_map_some"
\ 6lemma option_map_some : ∀A,B,f,x,v.
41 \ 5a href="cic:/matita/basics/types/option_map.def(1)"
\ 6option_map
\ 5/a
\ 6 A B f x
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 \ 5a href="cic:/matita/basics/types/option.con(0,2,1)"
\ 6Some
\ 5/a
\ 6 B v →
\ 5a title="exists" href="cic:/fakeuri.def(1)"
\ 6∃
\ 5/a
\ 6y. x
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 \ 5a href="cic:/matita/basics/types/option.con(0,2,1)"
\ 6Some
\ 5/a
\ 6 ? y
\ 5a title="logical and" href="cic:/fakeuri.def(1)"
\ 6∧
\ 5/a
\ 6 f y
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 v.
43 [ #v normalize #E destruct
44 | #y #v normalize #E %{y} destruct % //
47 \ 5img class="anchor" src="icons/tick.png" id="option_map_def"
\ 6definition option_map_def : ∀A,B:Type[0]. (A → B) → B →
\ 5a href="cic:/matita/basics/types/option.ind(1,0,1)"
\ 6option
\ 5/a
\ 6 A → B ≝
48 λA,B,f,d,o. match o with [ None ⇒ d | Some a ⇒ f a ].
50 \ 5img class="anchor" src="icons/tick.png" id="refute_none_by_refl"
\ 6lemma refute_none_by_refl : ∀A,B:Type[0]. ∀P:A → B. ∀Q:B → Type[0]. ∀x:
\ 5a href="cic:/matita/basics/types/option.ind(1,0,1)"
\ 6option
\ 5/a
\ 6 A. ∀H:x
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 \ 5a href="cic:/matita/basics/types/option.con(0,1,1)"
\ 6None
\ 5/a
\ 6 ? →
\ 5a href="cic:/matita/basics/logic/False.ind(1,0,0)"
\ 6False
\ 5/a
\ 6.
51 (∀v. x
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 \ 5a href="cic:/matita/basics/types/option.con(0,2,1)"
\ 6Some
\ 5/a
\ 6 ? v → Q (P v)) →
52 Q (match x return λy.x
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 y → ? with [ Some v ⇒ λ_. P v | None ⇒ λE. match H E in False with [ ] ] (
\ 5a href="cic:/matita/basics/logic/eq.con(0,1,2)"
\ 6refl
\ 5/a
\ 6 ? x)).
54 [ #H cases (H (
\ 5a href="cic:/matita/basics/logic/eq.con(0,1,2)"
\ 6refl
\ 5/a
\ 6 ??))
55 | #a #H #p normalize @p @
\ 5a href="cic:/matita/basics/logic/eq.con(0,1,2)"
\ 6refl
\ 5/a
\ 6
59 \ 5img class="anchor" src="icons/tick.png" id="Sig"
\ 6record Sig (A:Type[0]) (f:A→Type[0]) : Type[0] ≝ {
64 interpretation "Sigma" 'sigma x = (Sig ? x).
66 notation "hvbox(« term 19 a, break term 19 b»)"
67 with precedence 90 for @{ 'dp $a $b }.
69 interpretation "mk_Sig" 'dp x y = (mk_Sig ?? x y).
73 \ 5img class="anchor" src="icons/tick.png" id="Prod"
\ 6record Prod (A,B:Type[0]) : Type[0] ≝ {
78 interpretation "Pair construction" 'pair x y = (mk_Prod ? ? x y).
80 interpretation "Product" 'product x y = (Prod x y).
82 interpretation "pair pi1" 'pi1 = (fst ? ?).
83 interpretation "pair pi2" 'pi2 = (snd ? ?).
84 interpretation "pair pi1" 'pi1a x = (fst ? ? x).
85 interpretation "pair pi2" 'pi2a x = (snd ? ? x).
86 interpretation "pair pi1" 'pi1b x y = (fst ? ? x y).
87 interpretation "pair pi2" 'pi2b x y = (snd ? ? x y).
89 notation "π1" with precedence 10 for @{ (proj1 ??) }.
90 notation "π2" with precedence 10 for @{ (proj2 ??) }.
92 (* Yeah, I probably ought to do something more general... *)
93 notation "hvbox(\langle term 19 a, break term 19 b, break term 19 c\rangle)"
94 with precedence 90 for @{ 'triple $a $b $c}.
95 interpretation "Triple construction" 'triple x y z = (mk_Prod ? ? (mk_Prod ? ? x y) z).
97 notation "hvbox(\langle term 19 a, break term 19 b, break term 19 c, break term 19 d\rangle)"
98 with precedence 90 for @{ 'quadruple $a $b $c $d}.
99 interpretation "Quadruple construction" 'quadruple w x y z = (mk_Prod ? ? (mk_Prod ? ? w x) (mk_Prod ? ? y z)).
102 \ 5img class="anchor" src="icons/tick.png" id="eq_pair_fst_snd"
\ 6theorem eq_pair_fst_snd: ∀A,B.∀p:A
\ 5a title="Product" href="cic:/fakeuri.def(1)"
\ 6×
\ 5/a
\ 6 B.
103 p
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"
\ 6〈
\ 5/a
\ 6 \ 5a title="pair pi1" href="cic:/fakeuri.def(1)"
\ 6\fst
\ 5/a
\ 6 p,
\ 5a title="pair pi2" href="cic:/fakeuri.def(1)"
\ 6\snd
\ 5/a
\ 6 p
\ 5a title="Pair construction" href="cic:/fakeuri.def(1)"
\ 6〉
\ 5/a
\ 6.
104 #A #B #p (cases p) // qed.
106 \ 5img class="anchor" src="icons/tick.png" id="fst_eq"
\ 6lemma fst_eq : ∀A,B.∀a:A.∀b:B.
\ 5a title="pair pi1" href="cic:/fakeuri.def(1)"
\ 6\fst
\ 5/a
\ 6 \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"
\ 6〈
\ 5/a
\ 6a,b
\ 5a title="Pair construction" href="cic:/fakeuri.def(1)"
\ 6〉
\ 5/a
\ 6 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 a.
109 \ 5img class="anchor" src="icons/tick.png" id="snd_eq"
\ 6lemma snd_eq : ∀A,B.∀a:A.∀b:B.
\ 5a title="pair pi2" href="cic:/fakeuri.def(1)"
\ 6\snd
\ 5/a
\ 6 \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"
\ 6〈
\ 5/a
\ 6a,b
\ 5a title="Pair construction" href="cic:/fakeuri.def(1)"
\ 6〉
\ 5/a
\ 6 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 b.
112 notation > "hvbox('let' 〈ident x,ident y〉 ≝ t 'in' s)"
114 for @{ match $t with [ mk_Prod ${ident x} ${ident y} ⇒ $s ] }.
116 notation < "hvbox('let' \nbsp hvbox(〈ident x,ident y〉 \nbsp≝ break t \nbsp 'in' \nbsp) break s)"
118 for @{ match $t with [ mk_Prod (${ident x}:$X) (${ident y}:$Y) ⇒ $s ] }.
120 (* Also extracts an equality proof (useful when not using Russell). *)
121 notation > "hvbox('let' 〈ident x,ident y〉 'as' ident E ≝ t 'in' s)"
123 for @{ match $t return λx.x = $t → ? with [ mk_Prod ${ident x} ${ident y} ⇒
124 λ${ident E}.$s ] (refl ? $t) }.
127 \ 5img class="anchor" src="icons/tick.png" id="PSig"
\ 6record PSig (A:Type[0]) (P:A→Prop) : Type[0] ≝
128 {elem:>A; eproof: P elem}.
130 interpretation "subset type" 'sigma x = (PSig ? x).
132 notation < "hvbox('let' \nbsp hvbox(〈ident x,ident y〉 \nbsp 'as'\nbsp ident E\nbsp ≝ break t \nbsp 'in' \nbsp) break s)"
134 for @{ match $t return λ${ident k}:$X.$eq $T $k $t → ? with [ mk_Prod (${ident x}:$U) (${ident y}:$W) ⇒
135 λ${ident E}:$e.$s ] ($refl $T $t) }.
137 notation > "hvbox('let' 〈ident x,ident y,ident z〉 'as' ident E ≝ t 'in' s)"
139 for @{ match $t return λx.x = $t → ? with [ mk_Prod ${fresh xy} ${ident z} ⇒
140 match ${fresh xy} return λx. ? = $t → ? with [ mk_Prod ${ident x} ${ident y} ⇒
141 λ${ident E}.$s ] ] (refl ? $t) }.
143 notation < "hvbox('let' \nbsp hvbox(〈ident x,ident y,ident z〉 \nbsp'as'\nbsp ident E\nbsp ≝ break t \nbsp 'in' \nbsp) break s)"
145 for @{ match $t return λ${ident x}.$eq $T $x $t → $U with [ mk_Prod (${fresh xy}:$V) (${ident z}:$Z) ⇒
146 match ${fresh xy} return λ${ident y}. $eq $R $r $t → ? with [ mk_Prod (${ident x}:$L) (${ident y}:$I) ⇒
147 λ${ident E}:$J.$s ] ] ($refl $A $t) }.
149 notation > "hvbox('let' 〈ident w,ident x,ident y,ident z〉 ≝ t 'in' s)"
151 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 ] ] ] }.
153 notation > "hvbox('let' 〈ident x,ident y,ident z〉 ≝ t 'in' s)"
155 for @{ match $t with [ mk_Prod ${fresh xy} ${ident z} ⇒ match ${fresh xy} with [ mk_Prod ${ident x} ${ident y} ⇒ $s ] ] }.
157 (* This appears to upset automation (previously provable results require greater
158 depth or just don't work), so use example rather than lemma to prevent it
160 \ 5img class="anchor" src="icons/tick.png" id="contract_pair"
\ 6example contract_pair : ∀A,B.∀e:A
\ 5a title="Product" href="cic:/fakeuri.def(1)"
\ 6×
\ 5/a
\ 6B. (let 〈a,b〉 ≝ e in
\ 5a title="Pair construction" href="cic:/fakeuri.def(1)"
\ 6〈
\ 5/a
\ 6a,b
\ 5a title="Pair construction" href="cic:/fakeuri.def(1)"
\ 6〉
\ 5/a
\ 6)
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 e.
163 \ 5img class="anchor" src="icons/tick.png" id="extract_pair"
\ 6lemma extract_pair : ∀A,B,C,D. ∀u:A
\ 5a title="Product" href="cic:/fakeuri.def(1)"
\ 6×
\ 5/a
\ 6B. ∀Q:A → B → C
\ 5a title="Product" href="cic:/fakeuri.def(1)"
\ 6×
\ 5/a
\ 6D. ∀x,y.
164 ((let 〈a,b〉 ≝ u in Q a b)
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"
\ 6〈
\ 5/a
\ 6x,y
\ 5a title="Pair construction" href="cic:/fakeuri.def(1)"
\ 6〉
\ 5/a
\ 6) →
165 \ 5a title="exists" href="cic:/fakeuri.def(1)"
\ 6∃
\ 5/a
\ 6a,b
\ 5a title="exists" href="cic:/fakeuri.def(1)"
\ 6.
\ 5/a
\ 6 \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"
\ 6〈
\ 5/a
\ 6a,b
\ 5a title="Pair construction" href="cic:/fakeuri.def(1)"
\ 6〉
\ 5/a
\ 6 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 u
\ 5a title="logical and" href="cic:/fakeuri.def(1)"
\ 6∧
\ 5/a
\ 6 Q a b
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"
\ 6〈
\ 5/a
\ 6x,y
\ 5a title="Pair construction" href="cic:/fakeuri.def(1)"
\ 6〉
\ 5/a
\ 6.
166 #A #B #C #D * #a #b #Q #x #y normalize #E1 %{a} %{b} % try @
\ 5a href="cic:/matita/basics/logic/eq.con(0,1,2)"
\ 6refl
\ 5/a
\ 6 @E1 qed.
168 \ 5img class="anchor" src="icons/tick.png" id="breakup_pair"
\ 6lemma breakup_pair : ∀A,B,C:Type[0].∀x. ∀R:C → Prop. ∀P:A → B → C.
169 R (P (
\ 5a title="pair pi1" href="cic:/fakeuri.def(1)"
\ 6\fst
\ 5/a
\ 6 x) (
\ 5a title="pair pi2" href="cic:/fakeuri.def(1)"
\ 6\snd
\ 5/a
\ 6 x)) → R (let 〈a,b〉 ≝ x in P a b).
170 #A #B #C *; normalize /
\ 5span class="autotactic"
\ 62
\ 5span class="autotrace"
\ 6 trace
\ 5/span
\ 6\ 5/span
\ 6/
173 \ 5img class="anchor" src="icons/tick.png" id="pair_elim"
\ 6lemma pair_elim:
177 ∀P: A
\ 5a title="Product" href="cic:/fakeuri.def(1)"
\ 6×
\ 5/a
\ 6B → C → Prop.
178 (∀lft, rgt. p
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"
\ 6〈
\ 5/a
\ 6lft,rgt
\ 5a title="Pair construction" href="cic:/fakeuri.def(1)"
\ 6〉
\ 5/a
\ 6 → P
\ 5a title="Pair construction" href="cic:/fakeuri.def(1)"
\ 6〈
\ 5/a
\ 6lft,rgt
\ 5a title="Pair construction" href="cic:/fakeuri.def(1)"
\ 6〉
\ 5/a
\ 6 (T lft rgt)) →
179 P p (let 〈lft, rgt〉 ≝ p in T lft rgt).
180 #A #B #C #T * /
\ 5span class="autotactic"
\ 62
\ 5span class="autotrace"
\ 6 trace
\ 5/span
\ 6\ 5/span
\ 6/
183 \ 5img class="anchor" src="icons/tick.png" id="pair_elim2"
\ 6lemma pair_elim2:
188 ∀P: A
\ 5a title="Product" href="cic:/fakeuri.def(1)"
\ 6×
\ 5/a
\ 6B → C → C' → Prop.
189 (∀lft, rgt. p
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"
\ 6〈
\ 5/a
\ 6lft,rgt
\ 5a title="Pair construction" href="cic:/fakeuri.def(1)"
\ 6〉
\ 5/a
\ 6 → P
\ 5a title="Pair construction" href="cic:/fakeuri.def(1)"
\ 6〈
\ 5/a
\ 6lft,rgt
\ 5a title="Pair construction" href="cic:/fakeuri.def(1)"
\ 6〉
\ 5/a
\ 6 (T lft rgt) (T' lft rgt)) →
190 P p (let 〈lft, rgt〉 ≝ p in T lft rgt) (let 〈lft, rgt〉 ≝ p in T' lft rgt).
191 #A #B #C #C' #T #T' * /
\ 5span class="autotactic"
\ 62
\ 5span class="autotrace"
\ 6 trace
\ 5/span
\ 6\ 5/span
\ 6/