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 (*
  33 nlemma eq_ind_r :
  34  ∀A.∀a.∀P: ∀x:A. x = a → Prop. P a (refl_eq A a) → ∀x.∀p:eq ? x a.P x p.
  35  #A; #a; #P; #p; #x0; #p0; ngeneralize in match p;
  36 ncases p0; #Heq; nassumption.
  37 nqed.
  38 *)
  39
  40 ntheorem rewrite_l: ∀A:Type[2].∀x.∀P:A → Prop. P x → ∀y. x = y → P y.
  41 #A; #x; #P; #Hx; #y; #Heq;ncases Heq;nassumption.
  42 nqed.
  43
  44 ntheorem sym_eq: ∀A:Type[2].∀x,y:A. x = y → y = x.
  45 #A; #x; #y; #Heq; napply (rewrite_l A x (λz.z=x));
  46 ##[ @; ##| nassumption; ##]
  47 nqed.
  48
  49 ntheorem rewrite_r: ∀A:Type[2].∀x.∀P:A → Prop. P x → ∀y. y = x → P y.
  50 #A; #x; #P; #Hx; #y; #Heq;ncases (sym_eq ? ? ?Heq);nassumption.
  51 nqed.
  52
  53 ntheorem eq_coerc: ∀A,B:Type[1].A→(A=B)→B.
  54 #A; #B; #Ha; #Heq;nelim Heq; nassumption.
  55 nqed.
  56
  57 ndefinition R0 ≝ λT:Type[0].λt:T.t.
  58
  59 ndefinition R1 ≝ eq_rect_Type0.
  60
  61 ndefinition R2 :
  62   ∀T0:Type[0].
  63   ∀a0:T0.
  64   ∀T1:∀x0:T0. a0=x0 → Type[0].
  65   ∀a1:T1 a0 (refl ? a0).
  66   ∀T2:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0. R1 ?? T1 a1 ? p0 = x1 → Type[0].
  67   ∀a2:T2 a0 (refl ? a0) a1 (refl ? a1).
  68   ∀b0:T0.
  69   ∀e0:a0 = b0.
  70   ∀b1: T1 b0 e0.
  71   ∀e1:R1 ?? T1 a1 ? e0 = b1.
  72   T2 b0 e0 b1 e1.
  73 #T0;#a0;#T1;#a1;#T2;#a2;#b0;#e0;#b1;#e1;
  74 napply (eq_rect_Type0 ????? e1);
  75 napply (R1 ?? ? ?? e0);
  76 napply a2;
  77 nqed.
  78
  79 ndefinition R3 :
  80   ∀T0:Type[0].
  81   ∀a0:T0.
  82   ∀T1:∀x0:T0. a0=x0 → Type[0].
  83   ∀a1:T1 a0 (refl ? a0).
  84   ∀T2:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0. R1 ?? T1 a1 ? p0 = x1 → Type[0].
  85   ∀a2:T2 a0 (refl ? a0) a1 (refl ? a1).
  86   ∀T3:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0.∀p1:R1 ?? T1 a1 ? p0 = x1.
  87       ∀x2:T2 x0 p0 x1 p1.R2 ???? T2 a2 x0 p0 ? p1 = x2 → Type[0].
  88   ∀a3:T3 a0 (refl ? a0) a1 (refl ? a1) a2 (refl ? a2).
  89   ∀b0:T0.
  90   ∀e0:a0 = b0.
  91   ∀b1: T1 b0 e0.
  92   ∀e1:R1 ?? T1 a1 ? e0 = b1.
  93   ∀b2: T2 b0 e0 b1 e1.
  94   ∀e2:R2 ???? T2 a2 b0 e0 ? e1 = b2.
  95   T3 b0 e0 b1 e1 b2 e2.
  96 #T0;#a0;#T1;#a1;#T2;#a2;#T3;#a3;#b0;#e0;#b1;#e1;#b2;#e2;
  97 napply (eq_rect_Type0 ????? e2);
  98 napply (R2 ?? ? ???? e0 ? e1);
  99 napply a3;
 100 nqed.
 101
 102 ndefinition R4 :
 103   ∀T0:Type[0].
 104   ∀a0:T0.
 105   ∀T1:∀x0:T0. eq T0 a0 x0 → Type[0].
 106   ∀a1:T1 a0 (refl T0 a0).
 107   ∀T2:∀x0:T0. ∀p0:eq (T0 …) a0 x0. ∀x1:T1 x0 p0.eq (T1 …) (R1 T0 a0 T1 a1 x0 p0) x1 → Type[0].
 108   ∀a2:T2 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1).
 109   ∀T3:∀x0:T0. ∀p0:eq (T0 …) a0 x0. ∀x1:T1 x0 p0.∀p1:eq (T1 …) (R1 T0 a0 T1 a1 x0 p0) x1.
 110       ∀x2:T2 x0 p0 x1 p1.eq (T2 …) (R2 T0 a0 T1 a1 T2 a2 x0 p0 x1 p1) x2 → Type[0].
 111   ∀a3:T3 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1)
 112       a2 (refl (T2 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1)) a2).
 113   ∀T4:∀x0:T0. ∀p0:eq (T0 …) a0 x0. ∀x1:T1 x0 p0.∀p1:eq (T1 …) (R1 T0 a0 T1 a1 x0 p0) x1.
 114       ∀x2:T2 x0 p0 x1 p1.∀p2:eq (T2 …) (R2 T0 a0 T1 a1 T2 a2 x0 p0 x1 p1) x2.
 115       ∀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.
 116       Type[0].
 117   ∀a4:T4 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       a3 (refl (T3 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1)
 120                    a2 (refl (T2 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1)) a2))
 121                    a3).
 122   ∀b0:T0.
 123   ∀e0:eq (T0 …) a0 b0.
 124   ∀b1: T1 b0 e0.
 125   ∀e1:eq (T1 …) (R1 T0 a0 T1 a1 b0 e0) b1.
 126   ∀b2: T2 b0 e0 b1 e1.
 127   ∀e2:eq (T2 …) (R2 T0 a0 T1 a1 T2 a2 b0 e0 b1 e1) b2.
 128   ∀b3: T3 b0 e0 b1 e1 b2 e2.
 129   ∀e3:eq (T3 …) (R3 T0 a0 T1 a1 T2 a2 T3 a3 b0 e0 b1 e1 b2 e2) b3.
 130   T4 b0 e0 b1 e1 b2 e2 b3 e3.
 131 #T0;#a0;#T1;#a1;#T2;#a2;#T3;#a3;#T4;#a4;#b0;#e0;#b1;#e1;#b2;#e2;#b3;#e3;
 132 napply (eq_rect_Type0 ????? e3);
 133 napply (R3 ????????? e0 ? e1 ? e2);
 134 napply a4;
 135 nqed.
 136
 137 naxiom streicherK : ∀T:Type[0].∀t:T.∀P:t = t → Type[2].P (refl ? t) → ∀p.P p.