matitaB/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 inductive eq (A: Type[0]) (a: A) : A → CProp[0] ≝
  19  refl: eq A a a.
  20
  21 lemma 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; cases p; #P; #H; assumption.
  24 qed.
  25
  26 lemma 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; apply (eq_rect_Type0_r' ??? p0); assumption.
  29 qed.
  30
  31 lemma 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; cases p; #P; #H; assumption.
  34 qed.
  35
  36 lemma 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; apply (eq_rect_CProp0_r' ??? p0); assumption.
  39 qed.
  40
  41 lemma 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; apply (eq_rect_CProp0_r' ??? p0); assumption.
  44 qed.
  45
  46 interpretation "leibnitz's equality" 'eq t x y = (eq t x y).
  47
  48 interpretation "leibnitz's on-equality" 'neq t x y = (Not (eq t x y)).
  49
  50 definition R0 ≝ λT:Type[0].λt:T.t.
  51
  52 definition R1 ≝ eq_rect_Type0.
  53
  54 definition 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 apply (eq_rect_Type0 ????? e1);
  68 apply (R1 ?? ? ?? e0);
  69 apply a2;
  70 qed.
  71
  72 definition 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 apply (eq_rect_Type0 ????? e2);
  91 apply (R2 ?? ? ???? e0 ? e1);
  92 apply a3;
  93 qed.
  94
  95 definition 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 apply (eq_rect_Type0 ????? e3);
 126 apply (R3 ????????? e0 ? e1 ? e2);
 127 apply a4;
 128 qed.
 129
 130 axiom streicherK : ∀T:Type[0].∀t:T.∀P:t = t → Type[2].P (refl ? t) → ∀p.P p.
 131
 132 definition EQ: ∀A:Type[0]. equivalence_relation A.
 133  #A; apply mk_equivalence_relation
 134   [ apply eq
 135   | apply refl
 136   | #x; #y; #H; rewrite < H; apply refl
 137   | #x; #y; #z; #Hyx; #Hxz; rewrite < Hxz; assumption]
 138 qed.
 139
 140 axiom T1 : Type[0].
 141 axiom T2 : T1 → Type[0].
 142 axiom t1 : T1.
 143 axiom t2 : ∀x:T1. T2 x.
 144
 145 inductive 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 (* lemma 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 apply (
 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   apply (∀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   apply (∀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 definition 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 *)