include "basics/logic.ma".
(* void *)
-inductive void : Type[0] ≝.
+\ 5img class="anchor" src="icons/tick.png" id="void"\ 6inductive void : Type[0] ≝.
(* unit *)
-inductive unit : Type[0] ≝ it: unit.
+\ 5img class="anchor" src="icons/tick.png" id="unit"\ 6inductive unit : Type[0] ≝ it: unit.
(* sum *)
-inductive Sum (A,B:Type[0]) : Type[0] ≝
+\ 5img class="anchor" src="icons/tick.png" id="Sum"\ 6inductive 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] ≝
+\ 5img class="anchor" src="icons/tick.png" id="option"\ 6inductive 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) ].
+\ 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 ≝
+λ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) ].
-lemma option_map_none : ∀A,B,f,x.
- option_map A B f x = None B → x = None A.
+\ 5img class="anchor" src="icons/tick.png" id="option_map_none"\ 6lemma option_map_none : ∀A,B,f,x.
+ \ 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.
#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.
+\ 5img class="anchor" src="icons/tick.png" id="option_map_some"\ 6lemma option_map_some : ∀A,B,f,x,v.
+ \ 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.
#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 ≝
+\ 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 ≝
λ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)).
+\ 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.
+ (∀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)) →
+ 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)).
#A #B #P #Q *
-[ #H cases (H (refl ??))
-| #a #H #p normalize @p @refl
+[ #H cases (H (\ 5a href="cic:/matita/basics/logic/eq.con(0,1,2)"\ 6refl\ 5/a\ 6 ??))
+| #a #H #p normalize @p @\ 5a href="cic:/matita/basics/logic/eq.con(0,1,2)"\ 6refl\ 5/a\ 6
] qed.
(* sigma *)
-record Sig (A:Type[0]) (f:A→Type[0]) : Type[0] ≝ {
+\ 5img class="anchor" src="icons/tick.png" id="Sig"\ 6record Sig (A:Type[0]) (f:A→Type[0]) : Type[0] ≝ {
pi1: A
; pi2: f pi1
}.
(* Prod *)
-record Prod (A,B:Type[0]) : Type[0] ≝ {
+\ 5img class="anchor" src="icons/tick.png" id="Prod"\ 6record Prod (A,B:Type[0]) : Type[0] ≝ {
fst: A
; snd: B
}.
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 〉.
+\ 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.
+ 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.
#A #B #p (cases p) // qed.
-lemma fst_eq : ∀A,B.∀a:A.∀b:B. \fst 〈a,b〉 = a.
+\ 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.
// qed.
-lemma snd_eq : ∀A,B.∀a:A.∀b:B. \snd 〈a,b〉 = b.
+\ 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.
// 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] ≝
+\ 5img class="anchor" src="icons/tick.png" id="PSig"\ 6record 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.
+\ 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.
#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.
+\ 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.
+((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) →
+\ 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.
+#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.
-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/
+\ 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.
+ 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).
+#A #B #C *; normalize /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5/span\ 6\ 5/span\ 6/
qed.
-lemma pair_elim:
+\ 5img class="anchor" src="icons/tick.png" id="pair_elim"\ 6lemma 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: A\ 5a title="Product" href="cic:/fakeuri.def(1)"\ 6×\ 5/a\ 6B → C → Prop.
+ (∀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)) →
+ P p (let 〈lft, rgt〉 ≝ p in T lft rgt).
+ #A #B #C #T * /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5/span\ 6\ 5/span\ 6/
qed.
-lemma pair_elim2:
+\ 5img class="anchor" src="icons/tick.png" id="pair_elim2"\ 6lemma 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: A\ 5a title="Product" href="cic:/fakeuri.def(1)"\ 6×\ 5/a\ 6B → C → C' → Prop.
+ (∀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)) →
+ P p (let 〈lft, rgt〉 ≝ p in T lft rgt) (let 〈lft, rgt〉 ≝ p in T' lft rgt).
+ #A #B #C #C' #T #T' * /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5/span\ 6\ 5/span\ 6/
+qed.
\ No newline at end of file
projects / helm.git / blobdiff