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.
7 ||A|| This file is distributed under the terms of the
8 \ / GNU General Public License Version 2
10 V_______________________________________________________________ *)
12 include "basics/logic.ma".
14 \ 5img class="anchor" src="icons/tick.png" id="Sigma"
\ 6inductive Sigma: Type[1] ≝
15 mk_Sigma: ∀p1: Type[0]. p1 → Sigma.
17 \ 5img class="anchor" src="icons/tick.png" id="p1"
\ 6definition p1:
\ 5a href="cic:/matita/basics/jmeq/Sigma.ind(1,0,0)"
\ 6Sigma
\ 5/a
\ 6 → Type[0].
21 \ 5img class="anchor" src="icons/tick.png" id="p2"
\ 6definition p2: ∀S:
\ 5a href="cic:/matita/basics/jmeq/Sigma.ind(1,0,0)"
\ 6Sigma
\ 5/a
\ 6.
\ 5a href="cic:/matita/basics/jmeq/p1.def(1)"
\ 6p1
\ 5/a
\ 6 S.
25 \ 5img class="anchor" src="icons/tick.png" id="jmeq"
\ 6inductive jmeq (A:Type[0]) (x:A) : ∀B:Type[0]. B →Prop ≝
26 jmrefl : jmeq A x A x.
28 \ 5img class="anchor" src="icons/tick.png" id="eqProp"
\ 6definition eqProp ≝ λA:Prop.
\ 5a href="cic:/matita/basics/logic/eq.ind(1,0,2)"
\ 6eq
\ 5/a
\ 6 A.
30 \ 5img class="anchor" src="icons/tick.png" id="K"
\ 6lemma K : ∀A.∀x:A.∀h:x
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6x.
\ 5a href="cic:/matita/basics/jmeq/eqProp.def(1)" title="null"
\ 6eqProp
\ 5/a
\ 6 ? h (
\ 5a href="cic:/matita/basics/logic/eq.con(0,1,2)"
\ 6refl
\ 5/a
\ 6 A x).
31 #A #x #h @(
\ 5a href="cic:/matita/basics/logic/eq.con(0,1,2)"
\ 6refl
\ 5/a
\ 6 ? h:
\ 5a href="cic:/matita/basics/jmeq/eqProp.def(1)"
\ 6eqProp
\ 5/a
\ 6 ? ? ?).
34 \ 5img class="anchor" src="icons/tick.png" id="cast"
\ 6definition cast:
35 ∀A,B:Type[0].∀E:A
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6B. A → B.
36 #A #B #E cases E #X @X
39 \ 5img class="anchor" src="icons/tick.png" id="tech1"
\ 6lemma tech1:
40 ∀Aa,Bb:
\ 5a href="cic:/matita/basics/jmeq/Sigma.ind(1,0,0)"
\ 6Sigma
\ 5/a
\ 6.∀E:Aa
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6Bb.
41 \ 5a href="cic:/matita/basics/jmeq/cast.def(1)"
\ 6cast
\ 5/a
\ 6 (
\ 5a href="cic:/matita/basics/jmeq/p1.def(1)"
\ 6p1
\ 5/a
\ 6 Aa) (
\ 5a href="cic:/matita/basics/jmeq/p1.def(1)"
\ 6p1
\ 5/a
\ 6 Bb) ? (
\ 5a href="cic:/matita/basics/jmeq/p2.def(2)"
\ 6p2
\ 5/a
\ 6 Aa)
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 \ 5a href="cic:/matita/basics/jmeq/p2.def(2)"
\ 6p2
\ 5/a
\ 6 Bb.
43 | #Aa #Bb #E >E cases Bb #B #b normalize % ]
46 \ 5img class="anchor" src="icons/tick.png" id="gral"
\ 6lemma gral: ∀A.∀x,y:A.
47 \ 5a href="cic:/matita/basics/jmeq/Sigma.con(0,1,0)"
\ 6mk_Sigma
\ 5/a
\ 6 A x
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 \ 5a href="cic:/matita/basics/jmeq/Sigma.con(0,1,0)"
\ 6mk_Sigma
\ 5/a
\ 6 A y → x
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6y.
48 #A #x #y #E lapply (
\ 5a href="cic:/matita/basics/jmeq/tech1.def(3)"
\ 6tech1
\ 5/a
\ 6 ?? E)
49 generalize in ⊢ (??(???%?)? → ?); #E1
50 normalize in E1; >(
\ 5a href="cic:/matita/basics/jmeq/K.def(2)"
\ 6K
\ 5/a
\ 6 ?? E1) normalize
54 \ 5img class="anchor" src="icons/tick.png" id="daemon"
\ 6axiom daemon:
\ 5a href="cic:/matita/basics/logic/False.ind(1,0,0)"
\ 6False
\ 5/a
\ 6.
56 \ 5img class="anchor" src="icons/tick.png" id="jm_to_eq_sigma"
\ 6lemma jm_to_eq_sigma:
57 ∀A,x,y.
\ 5a href="cic:/matita/basics/jmeq/jmeq.ind(1,0,2)"
\ 6jmeq
\ 5/a
\ 6 A x A y →
\ 5a href="cic:/matita/basics/jmeq/Sigma.con(0,1,0)"
\ 6mk_Sigma
\ 5/a
\ 6 A x
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 \ 5a href="cic:/matita/basics/jmeq/Sigma.con(0,1,0)"
\ 6mk_Sigma
\ 5/a
\ 6 A y.
58 #A #x #y #E cases E in ⊢ (???%); %
61 \ 5img class="anchor" src="icons/tick.png" id="curry"
\ 6definition curry:
63 (∀y.
\ 5a href="cic:/matita/basics/jmeq/jmeq.ind(1,0,2)"
\ 6jmeq
\ 5/a
\ 6 A x A y → Type[0]) →
64 (∀y.
\ 5a href="cic:/matita/basics/jmeq/Sigma.con(0,1,0)"
\ 6mk_Sigma
\ 5/a
\ 6 A x
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 \ 5a href="cic:/matita/basics/jmeq/Sigma.con(0,1,0)"
\ 6mk_Sigma
\ 5/a
\ 6 A y → Type[0]).
65 #A #x #f #y #E @(f y) >(
\ 5a href="cic:/matita/basics/jmeq/gral.def(4)"
\ 6gral
\ 5/a
\ 6 ??? E) %
68 \ 5img class="anchor" src="icons/tick.png" id="G"
\ 6lemma G : ∀A.∀x:A.∀P:∀y:A.
\ 5a href="cic:/matita/basics/jmeq/Sigma.con(0,1,0)"
\ 6mk_Sigma
\ 5/a
\ 6 A x
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 \ 5a href="cic:/matita/basics/jmeq/Sigma.con(0,1,0)"
\ 6mk_Sigma
\ 5/a
\ 6 A y →Type[0].
69 P x (
\ 5a href="cic:/matita/basics/logic/eq.con(0,1,2)"
\ 6refl
\ 5/a
\ 6 ? (
\ 5a href="cic:/matita/basics/jmeq/Sigma.con(0,1,0)"
\ 6mk_Sigma
\ 5/a
\ 6 A x)) → ∀y.∀h:
\ 5a href="cic:/matita/basics/jmeq/Sigma.con(0,1,0)"
\ 6mk_Sigma
\ 5/a
\ 6 A x
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 \ 5a href="cic:/matita/basics/jmeq/Sigma.con(0,1,0)"
\ 6mk_Sigma
\ 5/a
\ 6 A y.
71 #A #x #P #H #y #E lapply (
\ 5a href="cic:/matita/basics/jmeq/gral.def(4)"
\ 6gral
\ 5/a
\ 6 ??? E) #G generalize in match E;
73 return λy.λ_. ∀e:
\ 5a href="cic:/matita/basics/jmeq/Sigma.con(0,1,0)"
\ 6mk_Sigma
\ 5/a
\ 6 A x
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 \ 5a href="cic:/matita/basics/jmeq/Sigma.con(0,1,0)"
\ 6mk_Sigma
\ 5/a
\ 6 A y. P y e
76 #E <(
\ 5a href="cic:/matita/basics/logic/sym_eq.def(2)"
\ 6sym_eq
\ 5/a
\ 6 ??? (
\ 5a href="cic:/matita/basics/jmeq/K.def(2)"
\ 6K
\ 5/a
\ 6 ?? E)) @H
79 \ 5img class="anchor" src="icons/tick.png" id="PP"
\ 6definition PP: ∀A:Prop.∀P:A → Type[0]. A → Type[0].
83 \ 5img class="anchor" src="icons/tick.png" id="E"
\ 6lemma E : ∀A.∀x:A.∀P:∀y:A.
\ 5a href="cic:/matita/basics/jmeq/jmeq.ind(1,0,2)"
\ 6jmeq
\ 5/a
\ 6 A x A y→Type[0].
84 \ 5a href="cic:/matita/basics/jmeq/PP.def(1)"
\ 6PP
\ 5/a
\ 6 ? (P x) (
\ 5a href="cic:/matita/basics/jmeq/jmeq.con(0,1,2)"
\ 6jmrefl
\ 5/a
\ 6 A x) → ∀y.∀h:
\ 5a href="cic:/matita/basics/jmeq/jmeq.ind(1,0,2)"
\ 6jmeq
\ 5/a
\ 6 A x A y.
\ 5a href="cic:/matita/basics/jmeq/PP.def(1)"
\ 6PP
\ 5/a
\ 6 ? (P y) h.
85 #A #a #P #H #b #E letin F ≝ (
\ 5a href="cic:/matita/basics/jmeq/jm_to_eq_sigma.def(1)"
\ 6jm_to_eq_sigma
\ 5/a
\ 6 ??? E)
86 lapply (
\ 5a href="cic:/matita/basics/jmeq/G.def(5)"
\ 6G
\ 5/a
\ 6 ?? (
\ 5a href="cic:/matita/basics/jmeq/curry.def(5)"
\ 6curry
\ 5/a
\ 6 ?? P) ?? F)
88 | #H whd in H; @(H :
\ 5a href="cic:/matita/basics/jmeq/PP.def(1)"
\ 6PP
\ 5/a
\ 6 ? (P b) ?) ]
91 \ 5img class="anchor" src="icons/tick.png" id="jmeq_elim"
\ 6lemma jmeq_elim : ∀A.∀x:A.∀P:∀y:A.
\ 5a href="cic:/matita/basics/jmeq/jmeq.ind(1,0,2)"
\ 6jmeq
\ 5/a
\ 6 A x A y→Type[0].
92 P x (
\ 5a href="cic:/matita/basics/jmeq/jmeq.con(0,1,2)"
\ 6jmrefl
\ 5/a
\ 6 A x) → ∀y.∀h:
\ 5a href="cic:/matita/basics/jmeq/jmeq.ind(1,0,2)"
\ 6jmeq
\ 5/a
\ 6 A x A y.P y h ≝
\ 5a href="cic:/matita/basics/jmeq/E.def(6)"
\ 6E
\ 5/a
\ 6.