matita/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[2] ≝
  15  mk_Sigma: ∀p1: Type[1]. p1 → Sigma.
  16
  17 definition p1: Sigma → Type[1].
  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[1]) (x:A) : ∀B:Type[1]. B →Prop ≝
  26 refl_jmeq : jmeq A x A x.
  27
  28 notation < "hvbox(term 46 a break maction (≃) (≃\sub(t,u)) term 46 b)"
  29   non associative with precedence 45
  30 for @{ 'jmsimeq $t $a $u $b }.
  31
  32 notation > "hvbox(n break ≃ m)"
  33   non associative with precedence 45
  34 for @{ 'jmsimeq ? $n ? $m }.
  35
  36 interpretation "john major's equality" 'jmsimeq t x u y = (jmeq t x u y).
  37 interpretation "john major's reflexivity" 'refl = refl_jmeq.
  38
  39 definition eqProp ≝ λA:Prop.eq A.
  40
  41 lemma K : ∀A.∀x:A.∀h:x=x. eqProp ? h (refl A x).
  42 #A #x #h @(refl ? h: eqProp ? ? ?).
  43 qed.
  44
  45 definition cast:
  46  ∀A,B:Type[1].∀E:A=B. A → B.
  47  #A #B #E cases E #X @X
  48 qed.
  49
  50 lemma tech1:
  51  ∀Aa,Bb:Sigma.∀E:Aa=Bb.
  52   cast (p1 Aa) (p1 Bb) ? (p2 Aa) = p2 Bb.
  53  [2: >E %
  54  | #Aa #Bb #E >E cases Bb #B #b normalize % ]
  55 qed.
  56
  57 lemma gral: ∀A.∀x,y:A.
  58  mk_Sigma A x = mk_Sigma A y → x=y.
  59  #A #x #y #E lapply (tech1 ?? E)
  60  generalize in ⊢ (??(???%?)? → ?); #E1
  61  normalize in E1; >(K ?? E1) normalize
  62  #H @H
  63 qed.
  64
  65 lemma jm_to_eq_sigma:
  66  ∀A,x,y. jmeq A x A y → mk_Sigma A x = mk_Sigma A y.
  67  #A #x #y #E cases E in ⊢ (???%); %
  68 qed.
  69
  70 definition curry:
  71  ∀A,x.
  72   (∀y. jmeq A x A y → Type[0]) →
  73    (∀y. mk_Sigma A x = mk_Sigma A y → Type[0]).
  74  #A #x #f #y #E @(f y) >(gral ??? E) %
  75 qed.
  76
  77 lemma G : ∀A.∀x:A.∀P:∀y:A.mk_Sigma A x = mk_Sigma A y →Type[0].
  78  P x (refl ? (mk_Sigma A x)) → ∀y.∀h:mk_Sigma A x = mk_Sigma A y.
  79   P y h.
  80  #A #x #P #H #y #E lapply (gral ??? E) #G generalize in match E;
  81  @(match G
  82     return λy.λ_. ∀e:mk_Sigma A x = mk_Sigma A y. P y e
  83    with
  84     [refl ⇒ ?])
  85  #E <(sym_eq ??? (K ?? E)) @H
  86 qed.
  87
  88 definition PP: ∀A:Prop.∀P:A → Type[0]. A → Type[0].
  89  #A #P #a @(P a)
  90 qed.
  91
  92 lemma E : ∀A.∀x:A.∀P:∀y:A.jmeq A x A y→Type[0].
  93  PP ? (P x) (refl_jmeq A x) → ∀y.∀h:jmeq A x A y.PP ? (P y) h.
  94  #A #a #P #H #b #E letin F ≝ (jm_to_eq_sigma ??? E)
  95  lapply (G ?? (curry ?? P) ?? F)
  96   [ normalize //
  97   | #H whd in H; @(H : PP ? (P b) ?) ]
  98 qed.
  99
 100 lemma jmeq_elim : ∀A.∀x:A.∀P:∀y:A.jmeq A x A y→Type[0].
 101  P x (refl_jmeq A x) → ∀y.∀h:jmeq A x A y.P y h ≝ E.
 102
 103 lemma jmeq_to_eq: ∀A:Type[1]. ∀x,y:A. x≃y → x=y.
 104  #A #x #y #JMEQ @(jmeq_elim ? x … JMEQ) %
 105 qed.
 106
 107 coercion jmeq_to_eq: ∀A:Type[1]. ∀x,y:A. ∀p:x≃y.x=y ≝ jmeq_to_eq on _p:?≃? to ?=?.
 108
 109 lemma eq_to_jmeq:
 110   ∀A: Type[1].
 111   ∀x, y: A.
 112     x = y → x ≃ y.
 113   //
 114 qed.