matita/matita/re_complete/basics/logic.ma

   1 include "basics/pts.ma".
   2 include "basics/hints_declaration.ma".
   3
   4 (* propositional equality *)
   5
   6 inductive eq (A:Type[2]) (x:A) : A → Prop ≝
   7     refl: eq A x x.
   8
   9 interpretation "leibnitz's equality" 'eq t x y = (eq t x y).
  10 interpretation "leibniz reflexivity" 'refl = refl.
  11
  12 lemma eq_rect_r:
  13  ∀A.∀a,x.∀p:eq ? x a.∀P: ∀x:A. eq ? x a → Type[3]. P a (refl A a) → P x p.
  14  #A #a #x #p (cases p) // qed.
  15
  16 lemma eq_ind_r :
  17  ∀A.∀a.∀P: ∀x:A. x = a → Prop. P a (refl A a) → ∀x.∀p:eq ? x a.P x p.
  18  #A #a #P #p #x0 #p0; @(eq_rect_r ? ? ? p0) //; qed.
  19
  20 lemma eq_rect_Type0_r:
  21   ∀A.∀a.∀P: ∀x:A. eq ? x a → Type[0]. P a (refl A a) → ∀x.∀p:eq ? x a.P x p.
  22   #A #a #P #H #x #p lapply H lapply P
  23   cases p; //; qed.
  24
  25 lemma eq_rect_Type1_r:
  26   ∀A.∀a.∀P: ∀x:A. eq ? x a → Type[1]. P a (refl A a) → ∀x.∀p:eq ? x a.P x p.
  27   #A #a #P #H #x #p lapply H lapply P
  28   cases p; //; qed.
  29
  30 lemma eq_rect_Type2_r:
  31   ∀A.∀a.∀P: ∀x:A. eq ? x a → Type[2]. P a (refl A a) → ∀x.∀p:eq ? x a.P x p.
  32   #A #a #P #H #x #p lapply H lapply P
  33   cases p; //; qed.
  34
  35 lemma eq_rect_Type3_r:
  36   ∀A.∀a.∀P: ∀x:A. eq ? x a → Type[3]. P a (refl A a) → ∀x.∀p:eq ? x a.P x p.
  37   #A #a #P #H #x #p lapply H lapply P
  38   cases p; //; qed.
  39
  40 theorem rewrite_l: ∀A:Type[2].∀x.∀P:A → Type[2]. P x → ∀y. x = y → P y.
  41 #A #x #P #Hx #y #Heq (cases Heq); //; qed.
  42
  43 theorem sym_eq: ∀A.∀x,y:A. x = y → y = x.
  44 #A #x #y #Heq @(rewrite_l A x (λz.z=x)) // qed.
  45
  46 theorem rewrite_r: ∀A:Type[2].∀x.∀P:A → Type[2]. P x → ∀y. y = x → P y.
  47 #A #x #P #Hx #y #Heq (cases (sym_eq ? ? ? Heq)); //; qed.
  48
  49 theorem eq_coerc: ∀A,B:Type[0].A→(A=B)→B.
  50 #A #B #Ha #Heq (elim Heq); //; qed.
  51
  52 theorem trans_eq : ∀A.∀x,y,z:A. x = y → y = z → x = z.
  53 #A #x #y #z #H1 #H2 >H1; //; qed.
  54
  55 theorem eq_f: ∀A,B.∀f:A→B.∀x,y:A. x=y → f x = f y.
  56 #A #B #f #x #y #H >H; //; qed.
  57
  58 (* deleterio per auto? *)
  59 theorem eq_f2: ∀A,B,C.∀f:A→B→C.
  60 ∀x1,x2:A.∀y1,y2:B. x1=x2 → y1=y2 → f x1 y1 = f x2 y2.
  61 #A #B #C #f #x1 #x2 #y1 #y2 #E1 #E2 >E1; >E2; //; qed.
  62
  63 lemma eq_f3: ∀A,B,C,D.∀f:A→B→C->D.
  64 ∀x1,x2:A.∀y1,y2:B. ∀z1,z2:C. x1=x2 → y1=y2 → z1=z2 → f x1 y1 z1 = f x2 y2 z2.
  65 #A #B #C #D #f #x1 #x2 #y1 #y2 #z1 #z2 #E1 #E2 #E3 >E1; >E2; >E3 //; qed.
  66
  67 (* hint to genereric equality
  68 definition eq_equality: equality ≝
  69  mk_equality eq refl rewrite_l rewrite_r.
  70
  71
  72 unification hint 0 ≔ T,a,b;
  73  X ≟ eq_equality
  74 (*------------------------------------*) ⊢
  75     equal X T a b ≡ eq T a b.
  76 *)
  77
  78 (********** connectives ********)
  79
  80 inductive True: Prop ≝
  81 I : True.
  82
  83 inductive False: Prop ≝ .
  84
  85 (* ndefinition Not: Prop → Prop ≝
  86 λA. A → False. *)
  87
  88 inductive Not (A:Prop): Prop ≝
  89 nmk: (A → False) → Not A.
  90
  91 interpretation "logical not" 'not x = (Not x).
  92
  93 theorem absurd : ∀A:Prop. A → ¬A → False.
  94 #A #H #Hn (elim Hn); /2/; qed.
  95
  96 (*
  97 ntheorem absurd : ∀ A,C:Prop. A → ¬A → C.
  98 #A; #C; #H; #Hn; nelim (Hn H).
  99 nqed. *)
 100
 101 theorem not_to_not : ∀A,B:Prop. (A → B) → ¬B →¬A.
 102 /4/; qed.
 103
 104 (* inequality *)
 105 interpretation "leibnitz's non-equality" 'neq t x y = (Not (eq t x y)).
 106
 107 theorem sym_not_eq: ∀A.∀x,y:A. x ≠ y → y ≠ x.
 108 /3/; qed.
 109
 110 (* and *)
 111 inductive And (A,B:Prop) : Prop ≝
 112     conj : A → B → And A B.
 113
 114 interpretation "logical and" 'and x y = (And x y).
 115
 116 theorem proj1: ∀A,B:Prop. A ∧ B → A.
 117 #A #B #AB (elim AB) //; qed.
 118
 119 theorem proj2: ∀ A,B:Prop. A ∧ B → B.
 120 #A #B #AB (elim AB) //; qed.
 121
 122 (* or *)
 123 inductive Or (A,B:Prop) : Prop ≝
 124      or_introl : A → (Or A B)
 125    | or_intror : B → (Or A B).
 126
 127 interpretation "logical or" 'or x y = (Or x y).
 128
 129 definition decidable : Prop → Prop ≝
 130 λ A:Prop. A ∨ ¬ A.
 131
 132 (* exists *)
 133 inductive ex (A:Type[0]) (P:A → Prop) : Prop ≝
 134     ex_intro: ∀ x:A. P x →  ex A P.
 135
 136 interpretation "exists" 'exists x = (ex ? x).
 137
 138 inductive ex2 (A:Type[0]) (P,Q:A →Prop) : Prop ≝
 139     ex_intro2: ∀ x:A. P x → Q x → ex2 A P Q.
 140
 141 (* iff *)
 142 definition iff :=
 143  λ A,B. (A → B) ∧ (B → A).
 144
 145 interpretation "iff" 'iff a b = (iff a b).
 146
 147 lemma iff_sym: ∀A,B. A ↔ B → B ↔ A.
 148 #A #B * /3/ qed.
 149
 150 lemma iff_trans:∀A,B,C. A ↔ B → B ↔ C → A ↔ C.
 151 #A #B #C * #H1 #H2 * #H3 #H4 % /3/ qed.
 152
 153 lemma iff_not: ∀A,B. A ↔ B → ¬A ↔ ¬B.
 154 #A #B * #H1 #H2 % /3/ qed.
 155
 156 lemma iff_and_l: ∀A,B,C. A ↔ B → C ∧ A ↔ C ∧ B.
 157 #A #B #C * #H1 #H2 % * /3/ qed.
 158
 159 lemma iff_and_r: ∀A,B,C. A ↔ B → A ∧ C ↔ B ∧ C.
 160 #A #B #C * #H1 #H2 % * /3/ qed.
 161
 162 lemma iff_or_l: ∀A,B,C. A ↔ B → C ∨ A ↔ C ∨ B.
 163 #A #B #C * #H1 #H2 % * /3/ qed.
 164
 165 lemma iff_or_r: ∀A,B,C. A ↔ B → A ∨ C ↔ B ∨ C.
 166 #A #B #C * #H1 #H2 % * /3/ qed.
 167
 168 (* cose per destruct: da rivedere *)
 169
 170 definition R0 ≝ λT:Type[0].λt:T.t.
 171
 172 definition R1 ≝ eq_rect_Type0.
 173
 174 (* used for lambda-delta *)
 175 definition R2 :
 176   ∀T0:Type[0].
 177   ∀a0:T0.
 178   ∀T1:∀x0:T0. a0=x0 → Type[0].
 179   ∀a1:T1 a0 (refl ? a0).
 180   ∀T2:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0. R1 ?? T1 a1 ? p0 = x1 → Type[0].
 181   ∀a2:T2 a0 (refl ? a0) a1 (refl ? a1).
 182   ∀b0:T0.
 183   ∀e0:a0 = b0.
 184   ∀b1: T1 b0 e0.
 185   ∀e1:R1 ?? T1 a1 ? e0 = b1.
 186   T2 b0 e0 b1 e1.
 187 #T0 #a0 #T1 #a1 #T2 #a2 #b0 #e0 #b1 #e1
 188 @(eq_rect_Type0 ????? e1)
 189 @(R1 ?? ? ?? e0)
 190 @a2
 191 qed.
 192
 193 definition R3 :
 194   ∀T0:Type[0].
 195   ∀a0:T0.
 196   ∀T1:∀x0:T0. a0=x0 → Type[0].
 197   ∀a1:T1 a0 (refl ? a0).
 198   ∀T2:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0. R1 ?? T1 a1 ? p0 = x1 → Type[0].
 199   ∀a2:T2 a0 (refl ? a0) a1 (refl ? a1).
 200   ∀T3:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0.∀p1:R1 ?? T1 a1 ? p0 = x1.
 201       ∀x2:T2 x0 p0 x1 p1.R2 ???? T2 a2 x0 p0 ? p1 = x2 → Type[0].
 202   ∀a3:T3 a0 (refl ? a0) a1 (refl ? a1) a2 (refl ? a2).
 203   ∀b0:T0.
 204   ∀e0:a0 = b0.
 205   ∀b1: T1 b0 e0.
 206   ∀e1:R1 ?? T1 a1 ? e0 = b1.
 207   ∀b2: T2 b0 e0 b1 e1.
 208   ∀e2:R2 ???? T2 a2 b0 e0 ? e1 = b2.
 209   T3 b0 e0 b1 e1 b2 e2.
 210 #T0 #a0 #T1 #a1 #T2 #a2 #T3 #a3 #b0 #e0 #b1 #e1 #b2 #e2
 211 @(eq_rect_Type0 ????? e2)
 212 @(R2 ?? ? ???? e0 ? e1)
 213 @a3
 214 qed.
 215
 216 definition R4 :
 217   ∀T0:Type[0].
 218   ∀a0:T0.
 219   ∀T1:∀x0:T0. eq T0 a0 x0 → Type[0].
 220   ∀a1:T1 a0 (refl T0 a0).
 221   ∀T2:∀x0:T0. ∀p0:eq (T0 …) a0 x0. ∀x1:T1 x0 p0.eq (T1 …) (R1 T0 a0 T1 a1 x0 p0) x1 → Type[0].
 222   ∀a2:T2 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1).
 223   ∀T3:∀x0:T0. ∀p0:eq (T0 …) a0 x0. ∀x1:T1 x0 p0.∀p1:eq (T1 …) (R1 T0 a0 T1 a1 x0 p0) x1.
 224       ∀x2:T2 x0 p0 x1 p1.eq (T2 …) (R2 T0 a0 T1 a1 T2 a2 x0 p0 x1 p1) x2 → Type[0].
 225   ∀a3:T3 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1)
 226       a2 (refl (T2 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1)) a2).
 227   ∀T4:∀x0:T0. ∀p0:eq (T0 …) a0 x0. ∀x1:T1 x0 p0.∀p1:eq (T1 …) (R1 T0 a0 T1 a1 x0 p0) x1.
 228       ∀x2:T2 x0 p0 x1 p1.∀p2:eq (T2 …) (R2 T0 a0 T1 a1 T2 a2 x0 p0 x1 p1) x2.
 229       ∀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.
 230       Type[0].
 231   ∀a4:T4 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1)
 232       a2 (refl (T2 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1)) a2)
 233       a3 (refl (T3 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1)
 234                    a2 (refl (T2 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1)) a2))
 235                    a3).
 236   ∀b0:T0.
 237   ∀e0:eq (T0 …) a0 b0.
 238   ∀b1: T1 b0 e0.
 239   ∀e1:eq (T1 …) (R1 T0 a0 T1 a1 b0 e0) b1.
 240   ∀b2: T2 b0 e0 b1 e1.
 241   ∀e2:eq (T2 …) (R2 T0 a0 T1 a1 T2 a2 b0 e0 b1 e1) b2.
 242   ∀b3: T3 b0 e0 b1 e1 b2 e2.
 243   ∀e3:eq (T3 …) (R3 T0 a0 T1 a1 T2 a2 T3 a3 b0 e0 b1 e1 b2 e2) b3.
 244   T4 b0 e0 b1 e1 b2 e2 b3 e3.
 245 #T0 #a0 #T1 #a1 #T2 #a2 #T3 #a3 #T4 #a4 #b0 #e0 #b1 #e1 #b2 #e2 #b3 #e3
 246 @(eq_rect_Type0 ????? e3)
 247 @(R3 ????????? e0 ? e1 ? e2)
 248 @a4
 249 qed.
 250
 251 definition eqProp ≝ λA:Prop.eq A.
 252
 253 (* Example to avoid indexing and the consequential creation of ill typed
 254    terms during paramodulation *)
 255 example lemmaK : ∀A.∀x:A.∀h:x=x. eqProp ? h (refl A x).
 256 #A #x #h @(refl ? h: eqProp ? ? ?).
 257 qed.
 258
 259 theorem streicherK : ∀T:Type[2].∀t:T.∀P:t = t → Type[3].P (refl ? t) → ∀p.P p.
 260  #T #t #P #H #p >(lemmaK T t p) @H
 261 qed.