]> matita.cs.unibo.it Git - helm.git/blob - weblib/basics/jmeq.ma
universary milestone in basic_2
[helm.git] / weblib / basics / jmeq.ma
1 (*
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.                     
5     ||I||                                                                 
6     ||T||  
7     ||A||  This file is distributed under the terms of the 
8     \   /  GNU General Public License Version 2        
9      \ /      
10       V_______________________________________________________________ *)
11
12 include "basics/logic.ma".
13
14 \ 5img class="anchor" src="icons/tick.png" id="Sigma"\ 6inductive Sigma: Type[1] ≝
15  mk_Sigma: ∀p1: Type[0]. p1 → Sigma.
16
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].
18  #S cases S #Y #_ @Y
19 qed.
20
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.
22  #S cases S #Y #x @x
23 qed.
24
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.
27
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.
29
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 ? ? ?).
32 qed.
33
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
37 qed.
38
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.
42  [2: >E %
43  | #Aa #Bb #E >E cases Bb #B #b normalize % ]
44 qed.
45  
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
51  #H @H
52 qed.
53
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.
55
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 ⊢ (???%); %
59 qed.
60
61 \ 5img class="anchor" src="icons/tick.png" id="curry"\ 6definition curry:
62  ∀A,x.
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) %
66 qed.
67
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.
70   P y h.
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;
72  @(match G
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
74    with
75     [refl ⇒ ?])
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
77 qed.
78
79 \ 5img class="anchor" src="icons/tick.png" id="PP"\ 6definition PP: ∀A:Prop.∀P:A → Type[0]. A → Type[0].
80  #A #P #a @(P a)
81 qed.
82
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)
87   [ normalize //
88   | #H whd in H; @(H : \ 5a href="cic:/matita/basics/jmeq/PP.def(1)"\ 6PP\ 5/a\ 6 ? (P b) ?) ]
89 qed.
90
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.