helm/software/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 ninductive 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 nlemma eq_rect_r:
  23  ∀A.∀a,x.∀p:eq ? x a.∀P: ∀x:A. eq ? x a → Type. P a (refl A a) → P x p.
  24  #A; #a; #x; #p; ncases p; #P; #H; nassumption.
  25 nqed.
  26
  27 nlemma 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; napply (eq_rect_r ? ? ? p0); nassumption.
  30 nqed.
  31
  32 nlemma eq_rect_Type2_r :
  33   ∀A:Type.∀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;ngeneralize in match H;ngeneralize in match P;
  35   ncases p;//;
  36 nqed.
  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 ntheorem rewrite_l: ∀A:Type[2].∀x.∀P:A → Prop. P x → ∀y. x = y → P y.
  47 #A; #x; #P; #Hx; #y; #Heq;ncases Heq;nassumption.
  48 nqed.
  49
  50 ntheorem sym_eq: ∀A:Type[2].∀x,y:A. x = y → y = x.
  51 #A; #x; #y; #Heq; napply (rewrite_l A x (λz.z=x));
  52 ##[ @; ##| nassumption; ##]
  53 nqed.
  54
  55 ntheorem rewrite_r: ∀A:Type[2].∀x.∀P:A → Prop. P x → ∀y. y = x → P y.
  56 #A; #x; #P; #Hx; #y; #Heq;ncases (sym_eq ? ? ?Heq);nassumption.
  57 nqed.
  58
  59 ntheorem eq_coerc: ∀A,B:Type[1].A→(A=B)→B.
  60 #A; #B; #Ha; #Heq;nelim Heq; nassumption.
  61 nqed.
  62
  63 ndefinition R0 ≝ λT:Type[0].λt:T.t.
  64
  65 ndefinition R1 ≝ eq_rect_Type0.
  66
  67 ndefinition 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 napply (eq_rect_Type0 ????? e1);
  81 napply (R1 ?? ? ?? e0);
  82 napply a2;
  83 nqed.
  84
  85 ndefinition 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 napply (eq_rect_Type0 ????? e2);
 104 napply (R2 ?? ? ???? e0 ? e1);
 105 napply a3;
 106 nqed.
 107
 108 ndefinition 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 napply (eq_rect_Type0 ????? e3);
 139 napply (R3 ????????? e0 ? e1 ? e2);
 140 napply a4;
 141 nqed.
 142
 143 naxiom streicherK : ∀T:Type[2].∀t:T.∀P:t = t → Type[2].P (refl ? t) → ∀p.P p.