helm/software/matita/nlibrary/logic/equality.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 include "logic/connectives.ma".
  16 include "properties/relations.ma".
  17
  18 ninductive eq (A: Type[0]) (a: A) : A → CProp[0] ≝
  19  refl: eq A a a.
  20
  21 nlemma eq_rect_Type0_r':
  22  ∀A.∀a,x.∀p:eq ? x a.∀P: ∀x:A. eq ? x a → Type[0]. P a (refl A a) → P x p.
  23  #A; #a; #x; #p; ncases p; #P; #H; nassumption.
  24 nqed.
  25
  26 nlemma eq_rect_Type0_r:
  27  ∀A.∀a.∀P: ∀x:A. eq ? x a → Type[0]. P a (refl A a) → ∀x.∀p:eq ? x a.P x p.
  28  #A; #a; #P; #p; #x0; #p0; napply (eq_rect_Type0_r' ??? p0); nassumption.
  29 nqed.
  30
  31 nlemma eq_rect_CProp0_r':
  32  ∀A.∀a,x.∀p:eq ? x a.∀P: ∀x:A. eq ? x a → CProp[0]. P a (refl A a) → P x p.
  33  #A; #a; #x; #p; ncases p; #P; #H; nassumption.
  34 nqed.
  35
  36 nlemma eq_rect_CProp0_r:
  37  ∀A.∀a.∀P: ∀x:A. eq ? x a → CProp[0]. P a (refl A a) → ∀x.∀p:eq ? x a.P x p.
  38  #A; #a; #P; #p; #x0; #p0; napply (eq_rect_CProp0_r' ??? p0); nassumption.
  39 nqed.
  40
  41 nlemma eq_ind_r :
  42  ∀A.∀a.∀P: ∀x:A. eq ? x a → Prop. P a (refl A a) → ∀x.∀p:eq ? x a.P x p.
  43  #A; #a; #P; #p; #x0; #p0; napply (eq_rect_CProp0_r' ??? p0); nassumption.
  44 nqed.
  45
  46 interpretation "leibnitz's equality" 'eq t x y = (eq t x y).
  47
  48 interpretation "leibnitz's non-equality" 'neq t x y = (Not (eq t x y)).
  49
  50 ndefinition R0 ≝ λT:Type[0].λt:T.t.
  51
  52 ndefinition R1 ≝ eq_rect_Type0.
  53
  54 ndefinition R2 :
  55   ∀T0:Type[0].
  56   ∀a0:T0.
  57   ∀T1:∀x0:T0. a0=x0 → Type[0].
  58   ∀a1:T1 a0 (refl ? a0).
  59   ∀T2:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0. R1 ?? T1 a1 ? p0 = x1 → Type[0].
  60   ∀a2:T2 a0 (refl ? a0) a1 (refl ? a1).
  61   ∀b0:T0.
  62   ∀e0:a0 = b0.
  63   ∀b1: T1 b0 e0.
  64   ∀e1:R1 ?? T1 a1 ? e0 = b1.
  65   T2 b0 e0 b1 e1.
  66 #T0;#a0;#T1;#a1;#T2;#a2;#b0;#e0;#b1;#e1;
  67 napply (eq_rect_Type0 ????? e1);
  68 napply (R1 ?? ? ?? e0);
  69 napply a2;
  70 nqed.
  71
  72 ndefinition R3 :
  73   ∀T0:Type[0].
  74   ∀a0:T0.
  75   ∀T1:∀x0:T0. a0=x0 → Type[0].
  76   ∀a1:T1 a0 (refl ? a0).
  77   ∀T2:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0. R1 ?? T1 a1 ? p0 = x1 → Type[0].
  78   ∀a2:T2 a0 (refl ? a0) a1 (refl ? a1).
  79   ∀T3:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0.∀p1:R1 ?? T1 a1 ? p0 = x1.
  80       ∀x2:T2 x0 p0 x1 p1.R2 ???? T2 a2 x0 p0 ? p1 = x2 → Type[0].
  81   ∀a3:T3 a0 (refl ? a0) a1 (refl ? a1) a2 (refl ? a2).
  82   ∀b0:T0.
  83   ∀e0:a0 = b0.
  84   ∀b1: T1 b0 e0.
  85   ∀e1:R1 ?? T1 a1 ? e0 = b1.
  86   ∀b2: T2 b0 e0 b1 e1.
  87   ∀e2:R2 ???? T2 a2 b0 e0 ? e1 = b2.
  88   T3 b0 e0 b1 e1 b2 e2.
  89 #T0;#a0;#T1;#a1;#T2;#a2;#T3;#a3;#b0;#e0;#b1;#e1;#b2;#e2;
  90 napply (eq_rect_Type0 ????? e2);
  91 napply (R2 ?? ? ???? e0 ? e1);
  92 napply a3;
  93 nqed.
  94
  95 ndefinition R4 :
  96   ∀T0:Type[0].
  97   ∀a0:T0.
  98   ∀T1:∀x0:T0. eq T0 a0 x0 → Type[0].
  99   ∀a1:T1 a0 (refl T0 a0).
 100   ∀T2:∀x0:T0. ∀p0:eq (T0 …) a0 x0. ∀x1:T1 x0 p0.eq (T1 …) (R1 T0 a0 T1 a1 x0 p0) x1 → Type[0].
 101   ∀a2:T2 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1).
 102   ∀T3:∀x0:T0. ∀p0:eq (T0 …) a0 x0. ∀x1:T1 x0 p0.∀p1:eq (T1 …) (R1 T0 a0 T1 a1 x0 p0) x1.
 103       ∀x2:T2 x0 p0 x1 p1.eq (T2 …) (R2 T0 a0 T1 a1 T2 a2 x0 p0 x1 p1) x2 → Type[0].
 104   ∀a3:T3 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1)
 105       a2 (refl (T2 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1)) a2).
 106   ∀T4:∀x0:T0. ∀p0:eq (T0 …) a0 x0. ∀x1:T1 x0 p0.∀p1:eq (T1 …) (R1 T0 a0 T1 a1 x0 p0) x1.
 107       ∀x2:T2 x0 p0 x1 p1.∀p2:eq (T2 …) (R2 T0 a0 T1 a1 T2 a2 x0 p0 x1 p1) x2.
 108       ∀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.
 109       Type[0].
 110   ∀a4:T4 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1)
 111       a2 (refl (T2 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1)) a2)
 112       a3 (refl (T3 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1)
 113                    a2 (refl (T2 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1)) a2))
 114                    a3).
 115   ∀b0:T0.
 116   ∀e0:eq (T0 …) a0 b0.
 117   ∀b1: T1 b0 e0.
 118   ∀e1:eq (T1 …) (R1 T0 a0 T1 a1 b0 e0) b1.
 119   ∀b2: T2 b0 e0 b1 e1.
 120   ∀e2:eq (T2 …) (R2 T0 a0 T1 a1 T2 a2 b0 e0 b1 e1) b2.
 121   ∀b3: T3 b0 e0 b1 e1 b2 e2.
 122   ∀e3:eq (T3 …) (R3 T0 a0 T1 a1 T2 a2 T3 a3 b0 e0 b1 e1 b2 e2) b3.
 123   T4 b0 e0 b1 e1 b2 e2 b3 e3.
 124 #T0;#a0;#T1;#a1;#T2;#a2;#T3;#a3;#T4;#a4;#b0;#e0;#b1;#e1;#b2;#e2;#b3;#e3;
 125 napply (eq_rect_Type0 ????? e3);
 126 napply (R3 ????????? e0 ? e1 ? e2);
 127 napply a4;
 128 nqed.
 129
 130 naxiom streicherK : ∀T:Type[0].∀t:T.∀P:t = t → Type[2].P (refl ? t) → ∀p.P p.
 131
 132 ndefinition EQ: ∀A:Type[0]. equivalence_relation A.
 133  #A; napply mk_equivalence_relation
 134   [ napply eq
 135   | napply refl
 136   | #x; #y; #H; nrewrite < H; napply refl
 137   | #x; #y; #z; #Hyx; #Hxz; nrewrite < Hxz; nassumption]
 138 nqed.
 139
 140 naxiom T1 : Type[0].
 141 naxiom T2 : T1 → Type[0].
 142 naxiom t1 : T1.
 143 naxiom t2 : ∀x:T1. T2 x.
 144
 145 ninductive I2 : ∀r1:T1.T2 r1 → Type[0] ≝
 146 | i2c1 : ∀x1:T1.∀x2:T2 x1. I2 x1 x2
 147 | i2c2 : I2 t1 (t2 t1).
 148
 149 (* nlemma i2d : ∀a,b.∀x,y:I2 a b.
 150              ∀e1:a = a.∀e2:R1 T1 a (λz,p.T2 z) b a e1 = b.
 151              ∀e: R2 T1 a (λz,p.T2 z) b (λz1,p1,z2,p2.I2 z1 z2) x a e1 b e2 = y.
 152              Type[2].
 153 #a;#b;#x;#y;
 154 napply (
 155 match x return (λr1,r2,r.
 156                  ∀e1:r1 = a. ∀e2:R1 T1 r1 (λz,p. T2 z) r2 a e1 = b.
 157                  ∀e :R2 T1 r1 (λz,p. T2 z) r2 (λz1,p1,z2,p2. I2 z1 z2) r a e1 b e2 = y. Type[2]) with
 158   [ i2c1 x1 x2 ⇒ ?
 159   | i2c2 ⇒ ?]
 160 )
 161 [napply (match y return (λr1,r2,r.
 162                      ∀e1: x1 = r1. ∀e2: R1 T1 x1 (λz,p. T2 z) x2 r1 e1 = r2.
 163                      ∀e : R2 T1 x1 (λz,p.T2 z) x2 (λz1,p1,z2,p2. I2 z1 z2) (i2c1 x1 x2) r1 e1 r2 e2 = r. Type[2]) with
 164     [ i2c1 y1 y2 ⇒ ?
 165     | i2c2 ⇒ ? ])
 166  [#e1; #e2; #e;
 167   napply (∀P:Type[1].
 168                      (∀f1:x1 = y1. ∀f2: R1 T1 x1 (λz,p.T2 z) x2 y1 f1 = y2.
 169                       ∀f: R2 T1 x1 (λz,p.T2 z) x2
 170                           (λz1,p1,z2,p2.eq ?
 171                               (i2c1 (R1 ??? z1 ? (R1 ?? (λm,n.m = y1) f1 ? p1)) ?)
 172                                (*       (R2 ???? (λm1,n1,m2,n2.R1 ?? (λm,n.T2 m) ? ? f1 = y2) f2 ?
 173                                        p1 ? p2)))*)
 174 (*                            (R2 ???? (λw1,q1,w2,q2.I2 w1 w2) (i2c1 z1 z2)
 175                                 ? (R1 ?? (λw,q.w = y1) e1 z1 p1)
 176                                 ? (R2 ????
 177                                       (λw1,q1,w2,q2.R1 ?? (λm,n.T2 m) w2 ? q1 = y2)
 178                                       e2 z1 p1 (R1 T1 x1 (λw,q.w = y1) e1 z1 p1) p2))
 179   *)                          (i2c1 y1 y2))
 180                           ? y1 f1 y2 f2 = refl (I2 y1 y2) (i2c1 y1 y2).P)
 181                    → P);
 182   napply (∀P:Type[1].
 183                      (∀f1:x1 = y1. ∀f2: R1 T1 x1 (λz,p.T2 z) x2 y1 f1 = y2.
 184                       ∀f: R2 T1 x1 (λz,p.T2 z) x2
 185                           (λz1,p1,z2,p2.eq (I2 y1 y2)
 186                             (R2 T1 z1 (λw,q.T2 w) z2 (λw1,q1,w2,q2.I2 w1 w2) (i2c1 z1 z2)
 187                                 y1 (R1 T1 x1 (λw,q.w = y1) e1 z1 p1)
 188                                 y2 (R2 T1 x1 (λw,q.w = y1) e1
 189                                              (λw1,q1,w2,q2.R1 ??? w2 w1 q1 = y2) e2 z1 p1 (R1 T1 x1 (λw,q.w = y1) e1 z1 p1) p2))
 190                             (i2c1 y1 y2))
 191                           e y1 f1 y2 f2 = refl (I2 y1 y2) (i2c1 y1 y2).P)
 192                    → P);
 193
 194
 195
 196 ndefinition i2d : ∀a,b.∀x,y:I2 a b.
 197                   ∀e1:a = a.∀e2:R1 T1 a (λz,p.T2 z) b a e1 = b.
 198                   ∀e: R2 T1 a (λz,p.T2 z) b (λz1,p1,z2,p2.I2 z1 z2) x a e1 b e2 = y.Type[2] ≝
 199 λa,b,x,y.
 200 match x return (λr1,r2,r.
 201                  ∀e1:r1 = a. ∀e2:R1 T1 r1 (λz,p. T2 z) r2 a e1 = b.
 202                  ∀e :R2 T1 r1 (λz,p. T2 z) r2 (λz1,p1,z2,p2. I2 z1 z2) r a e1 b e2 = y. Type[2]) with
 203   [ i2c1 x1 x2 ⇒
 204     match y return (λr1,r2,r.
 205                      ∀e1: x1 = r1. ∀e2: R1 T1 x1 (λz,p. T2 z) x2 r1 e1 = r2.
 206                      ∀e : R2 T1 x1 (λz,p.T2 z) x2 (λz1,p1,z2,p2. I2 z1 z2) (i2c1 x1 x2) r1 e1 r2 e2 = r. Type[2]) with
 207     [ i2c1 y1 y2 ⇒ λe1,e2,e.∀P:Type[1].
 208                      (∀f1:x1 = y1. ∀f2: R1 T1 x1 (λz,p.T2 z) x2 y1 f1 = y2.
 209                       ∀f: R2 T1 x1 (λz,p.T2 z) x2
 210                           (λz1,p1,z2,p2.eq (I2 y1 y2)
 211                             (R2 T1 z1 (λw,q.T2 w) z2 (λw1,q1,w2,q2.I2 w1 w2) (i2c1 z1 z2)
 212                                 y1 (R1 T1 x1 (λw,q.w = y1) e1 z1 p1)
 213                                 y2 (R2 T1 x1 (λw,q.w = y1) e1
 214                                              (λw1,q1,w2,q2.R1 ??? w2 w1 q1 = y2) e2 z1 p1 (R1 T1 x1 (λw,q.w = y1) e1 z1 p1) p2))
 215                             (i2c1 y1 y2))
 216                           e y1 f1 y2 f2 = refl (I2 y1 y2) (i2c1 y1 y2).P)
 217                    → P
 218     | i2c2 ⇒ λe1,e2,e.∀P:Type[1].P ]
 219   | i2c2 ⇒
 220     match y return (λr1,r2,r.
 221                      ∀e1: x1 = r1. ∀e2: R1 ?? (λz,p. T2 z) x2 ? e1 = r2.
 222                      ∀e : R2 ???? (λz1,p1,z2,p2. I2 z1 z2) i2c2 ? e1 ? e2 = r. Type[2]) with
 223     [ i2c1 _ _ ⇒ λe1,e2,e.∀P:Type[1].P
 224     | i2c2 ⇒ λe1,e2,e.∀P:Type[1].
 225                (∀f: R2 ????
 226                     (λz1,p1,z2,p2.eq ? i2c2 i2c2)
 227                     e ? e1 ? e2 = refl ? i2c2.P) → P ] ].
 228
 229 *)