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.