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[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 lemma jm_to_eq_sigma:
  55  ∀A,x,y. jmeq A x A y → mk_Sigma A x = mk_Sigma A y.
  56  #A #x #y #E cases E in ⊢ (???%); %
  57 qed.
  58
  59 definition curry:
  60  ∀A,x.
  61   (∀y. jmeq A x A y → Type[0]) →
  62    (∀y. mk_Sigma A x = mk_Sigma A y → Type[0]).
  63  #A #x #f #y #E @(f y) >(gral ??? E) %
  64 qed.
  65
  66 lemma G : ∀A.∀x:A.∀P:∀y:A.mk_Sigma A x = mk_Sigma A y →Type[0].
  67  P x (refl ? (mk_Sigma A x)) → ∀y.∀h:mk_Sigma A x = mk_Sigma A y.
  68   P y h.
  69  #A #x #P #H #y #E lapply (gral ??? E) #G generalize in match E;
  70  @(match G
  71     return λy.λ_. ∀e:mk_Sigma A x = mk_Sigma A y. P y e
  72    with
  73     [refl ⇒ ?])
  74  #E <(sym_eq ??? (K ?? E)) @H
  75 qed.
  76
  77 definition PP: ∀A:Prop.∀P:A → Type[0]. A → Type[0].
  78  #A #P #a @(P a)
  79 qed.
  80
  81 lemma E : ∀A.∀x:A.∀P:∀y:A.jmeq A x A y→Type[0].
  82  PP ? (P x) (jmrefl A x) → ∀y.∀h:jmeq A x A y.PP ? (P y) h.
  83  #A #a #P #H #b #E letin F ≝ (jm_to_eq_sigma ??? E)
  84  lapply (G ?? (curry ?? P) ?? F)
  85   [ normalize //
  86   | #H whd in H; @(H : PP ? (P b) ?) ]
  87 qed.
  88
  89 lemma jmeq_elim : ∀A.∀x:A.∀P:∀y:A.jmeq A x A y→Type[0].
  90  P x (jmrefl A x) → ∀y.∀h:jmeq A x A y.P y h ≝ E.