]> matita.cs.unibo.it Git - helm.git/blob - matitaB/matita/lib/basics/jmeq.ma
advances non lfsx ...
[helm.git] / matitaB / matita / lib / 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 inductive Sigma: Type[1] ≝
15  mk_Sigma: ∀p1: Type[0]. p1 → Sigma.
16
17 definition p1: Sigma → Type[0].
18  #S cases S #Y #_ @Y
19 qed.
20
21 definition p2: ∀S:Sigma. p1 S.
22  #S cases S #Y #x @x
23 qed.
24
25 inductive jmeq (A:Type[0]) (x:A) : ∀B:Type[0]. B →Prop ≝
26 jmrefl : jmeq A x A x.
27
28 definition eqProp ≝ λA:Prop.eq A.
29
30 lemma K : ∀A.∀x:A.∀h:x=x. eqProp ? h (refl A x).
31 #A #x #h @(refl ? h: eqProp ? ? ?).
32 qed.
33
34 definition cast:
35  ∀A,B:Type[0].∀E:A=B. A → B.
36  #A #B #E cases E #X @X
37 qed.
38
39 lemma tech1:
40  ∀Aa,Bb:Sigma.∀E:Aa=Bb.
41   cast (p1 Aa) (p1 Bb) ? (p2 Aa) = p2 Bb.
42  [2: >E %
43  | #Aa #Bb #E >E cases Bb #B #b normalize % ]
44 qed.
45  
46 lemma gral: ∀A.∀x,y:A.
47  mk_Sigma A x = mk_Sigma A y → x=y.
48  #A #x #y #E lapply (tech1 ?? E)
49  generalize in ⊢ (??(???%?)? → ?) #E1
50  normalize in E1; >(K ?? E1) normalize
51  #H @H
52 qed.
53
54 axiom daemon: False.
55
56 lemma jm_to_eq_sigma:
57  ∀A,x,y. jmeq A x A y → mk_Sigma A x = mk_Sigma A y.
58  #A #x #y #E cases E in ⊢ (???%); %
59 qed.
60
61 definition curry:
62  ∀A,x.
63   (∀y. jmeq A x A y → Type[0]) →
64    (∀y. mk_Sigma A x = mk_Sigma A y → Type[0]).
65  #A #x #f #y #E @(f y) >(gral ??? E) %
66 qed.
67
68 lemma G : ∀A.∀x:A.∀P:∀y:A.mk_Sigma A x = mk_Sigma A y →Type[0].
69  P x (refl ? (mk_Sigma A x)) → ∀y.∀h:mk_Sigma A x = mk_Sigma A y.
70   P y h.
71  #A #x #P #H #y #E lapply (gral ??? E) #G generalize in match E;
72  @(match G
73     return λy.λ_. ∀e:mk_Sigma A x = mk_Sigma A y. P y e
74    with
75     [refl ⇒ ?])
76  #E <(sym_eq ??? (K ?? E)) @H
77 qed.
78
79 definition PP: ∀A:Prop.∀P:A → Type[0]. A → Type[0].
80  #A #P #a @(P a)
81 qed.
82
83 lemma E : ∀A.∀x:A.∀P:∀y:A.jmeq A x A y→Type[0].
84  PP ? (P x) (jmrefl A x) → ∀y.∀h:jmeq A x A y.PP ? (P y) h.
85  #A #a #P #H #b #E letin F ≝ (jm_to_eq_sigma ??? E)
86  lapply (G ?? (curry ?? P) ?? F)
87   [ normalize //
88   | #H whd in H; @(H : PP ? (P b) ?) ]
89 qed.
90
91 lemma jmeq_elim : ∀A.∀x:A.∀P:∀y:A.jmeq A x A y→Type[0].
92  P x (jmrefl A x) → ∀y.∀h:jmeq A x A y.P y h ≝ E.