matita/matita/nlibrary/Plogic/equality.ma

   1 (**************************************************************************)
   2 (*       ___                                                                *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||       A.Asperti, C.Sacerdoti Coen,                          *)
   8 (*      ||A||       E.Tassi, S.Zacchiroli                                 *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU Lesser General Public License Version 2.1         *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 include "logic/pts.ma".
  16
  17 inductive eq (A:Type[2]) (x:A) : A → Prop ≝
  18     refl: eq A x x.
  19
  20 interpretation "leibnitz's equality" 'eq t x y = (eq t x y).
  21
  22 lemma eq_rect_r:
  23  ∀A.∀a,x.∀p:eq ? x a.∀P: ∀x:A. eq ? x a → Type[0]. P a (refl A a) → P x p.
  24  #A  #a  #x  #p  cases p  #P  #H  assumption.
  25 qed.
  26
  27 lemma eq_ind_r :
  28  ∀A.∀a.∀P: ∀x:A. x = a → Prop. P a (refl A a) → ∀x.∀p:eq ? x a.P x p.
  29  #A #a #P #p #x0 #p0 apply (eq_rect_r ? ? ? p0) assumption.
  30 qed.
  31
  32 lemma eq_rect_Type2_r :
  33   ∀A:Type[0].∀a.∀P: ∀x:A. eq ? x a → Type[2]. P a (refl A a) → ∀x.∀p:eq ? x a.P x p.
  34   #A #a #P #H #x #p generalize in match H generalize in match P
  35   cases p //
  36 qed.
  37
  38 (*
  39 nlemma eq_ind_r :
  40  ∀A.∀a.∀P: ∀x:A. x = a → Prop. P a (refl_eq A a) → ∀x.∀p:eq ? x a.P x p.
  41  #A  #a  #P  #p  #x0  #p0  ngeneralize in match p
  42 ncases p0  #Heq  nassumption.
  43 nqed.
  44 *)
  45
  46 theorem rewrite_l: ∀A:Type[2].∀x.∀P:A → Prop. P x → ∀y. x = y → P y.
  47 #A  #x  #P  #Hx  #y  #Heq cases Heq assumption.
  48 qed.
  49
  50 theorem sym_eq: ∀A:Type[2].∀x,y:A. x = y → y = x.
  51 #A  #x  #y  #Heq  apply (rewrite_l A x (λz.z=x))
  52 [ % | assumption ]
  53 qed.
  54
  55 theorem rewrite_r: ∀A:Type[2].∀x.∀P:A → Prop. P x → ∀y. y = x → P y.
  56 #A  #x  #P  #Hx  #y  #Heq  cases (sym_eq ? ? ?Heq)  assumption.
  57 qed.
  58
  59 theorem eq_coerc: ∀A,B:Type[1].A→(A=B)→B.
  60 #A  #B  #Ha  #Heq elim Heq  assumption.
  61 qed.
  62
  63 definition R0 ≝ λT:Type[0].λt:T.t.
  64
  65 definition R1 ≝ eq_rect_Type0.
  66
  67 definition R2 :
  68   ∀T0:Type[0].
  69   ∀a0:T0.
  70   ∀T1:∀x0:T0. a0=x0 → Type[0].
  71   ∀a1:T1 a0 (refl ? a0).
  72   ∀T2:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0. R1 ?? T1 a1 ? p0 = x1 → Type[0].
  73   ∀a2:T2 a0 (refl ? a0) a1 (refl ? a1).
  74   ∀b0:T0.
  75   ∀e0:a0 = b0.
  76   ∀b1: T1 b0 e0.
  77   ∀e1:R1 ?? T1 a1 ? e0 = b1.
  78   T2 b0 e0 b1 e1.
  79 #T0 #a0 #T1 #a1 #T2 #a2 #b0 #e0 #b1 #e1
  80 apply (eq_rect_Type0 ????? e1)
  81 apply (R1 ?? ? ?? e0)
  82 apply a2
  83 qed.
  84
  85 definition R3 :
  86   ∀T0:Type[0].
  87   ∀a0:T0.
  88   ∀T1:∀x0:T0. a0=x0 → Type[0].
  89   ∀a1:T1 a0 (refl ? a0).
  90   ∀T2:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0. R1 ?? T1 a1 ? p0 = x1 → Type[0].
  91   ∀a2:T2 a0 (refl ? a0) a1 (refl ? a1).
  92   ∀T3:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0.∀p1:R1 ?? T1 a1 ? p0 = x1.
  93       ∀x2:T2 x0 p0 x1 p1.R2 ???? T2 a2 x0 p0 ? p1 = x2 → Type[0].
  94   ∀a3:T3 a0 (refl ? a0) a1 (refl ? a1) a2 (refl ? a2).
  95   ∀b0:T0.
  96   ∀e0:a0 = b0.
  97   ∀b1: T1 b0 e0.
  98   ∀e1:R1 ?? T1 a1 ? e0 = b1.
  99   ∀b2: T2 b0 e0 b1 e1.
 100   ∀e2:R2 ???? T2 a2 b0 e0 ? e1 = b2.
 101   T3 b0 e0 b1 e1 b2 e2.
 102 #T0 #a0 #T1 #a1 #T2 #a2 #T3 #a3 #b0 #e0 #b1 #e1 #b2 #e2
 103 apply (eq_rect_Type0 ????? e2)
 104 apply (R2 ?? ? ???? e0 ? e1)
 105 apply a3
 106 qed.
 107
 108 definition R4 :
 109   ∀T0:Type[0].
 110   ∀a0:T0.
 111   ∀T1:∀x0:T0. eq T0 a0 x0 → Type[0].
 112   ∀a1:T1 a0 (refl T0 a0).
 113   ∀T2:∀x0:T0. ∀p0:eq (T0 …) a0 x0. ∀x1:T1 x0 p0.eq (T1 …) (R1 T0 a0 T1 a1 x0 p0) x1 → Type[0].
 114   ∀a2:T2 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1).
 115   ∀T3:∀x0:T0. ∀p0:eq (T0 …) a0 x0. ∀x1:T1 x0 p0.∀p1:eq (T1 …) (R1 T0 a0 T1 a1 x0 p0) x1.
 116       ∀x2:T2 x0 p0 x1 p1.eq (T2 …) (R2 T0 a0 T1 a1 T2 a2 x0 p0 x1 p1) x2 → Type[0].
 117   ∀a3:T3 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1)
 118       a2 (refl (T2 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1)) a2).
 119   ∀T4:∀x0:T0. ∀p0:eq (T0 …) a0 x0. ∀x1:T1 x0 p0.∀p1:eq (T1 …) (R1 T0 a0 T1 a1 x0 p0) x1.
 120       ∀x2:T2 x0 p0 x1 p1.∀p2:eq (T2 …) (R2 T0 a0 T1 a1 T2 a2 x0 p0 x1 p1) x2.
 121       ∀x3:T3 x0 p0 x1 p1 x2 p2.∀p3:eq (T3 …) (R3 T0 a0 T1 a1 T2 a2 T3 a3 x0 p0 x1 p1 x2 p2) x3.
 122       Type[0].
 123   ∀a4:T4 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1)
 124       a2 (refl (T2 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1)) a2)
 125       a3 (refl (T3 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1)
 126                    a2 (refl (T2 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1)) a2))
 127                    a3).
 128   ∀b0:T0.
 129   ∀e0:eq (T0 …) a0 b0.
 130   ∀b1: T1 b0 e0.
 131   ∀e1:eq (T1 …) (R1 T0 a0 T1 a1 b0 e0) b1.
 132   ∀b2: T2 b0 e0 b1 e1.
 133   ∀e2:eq (T2 …) (R2 T0 a0 T1 a1 T2 a2 b0 e0 b1 e1) b2.
 134   ∀b3: T3 b0 e0 b1 e1 b2 e2.
 135   ∀e3:eq (T3 …) (R3 T0 a0 T1 a1 T2 a2 T3 a3 b0 e0 b1 e1 b2 e2) b3.
 136   T4 b0 e0 b1 e1 b2 e2 b3 e3.
 137 #T0 #a0 #T1 #a1 #T2 #a2 #T3 #a3 #T4 #a4 #b0 #e0 #b1 #e1 #b2 #e2 #b3 #e3
 138 apply (eq_rect_Type0 ????? e3)
 139 apply (R3 ????????? e0 ? e1 ? e2)
 140 apply a4
 141 qed.
 142
 143 axiom streicherK : ∀T:Type[2].∀t:T.∀P:t = t → Type[2].P (refl ? t) → ∀p.P p.