weblib/basics/logic.ma

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