matita/matita/lib/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 interpretation "logical true" 'true = True.
  95
  96 inductive False: Prop ≝ .
  97
  98 interpretation "logical false" 'false = False.
  99
 100 (* ndefinition Not: Prop → Prop ≝
 101 λA. A → ⊥. *)
 102
 103 inductive Not (A:Prop): Prop ≝
 104 nmk: (A → ⊥) → Not A.
 105
 106 interpretation "logical not" 'not x = (Not x).
 107
 108 theorem absurd : ∀A:Prop. A → ¬A → ⊥.
 109 #A #H #Hn (elim Hn); /2/; qed.
 110
 111 (*
 112 ntheorem absurd : ∀ A,C:Prop. A → ¬A → C.
 113 #A; #C; #H; #Hn; nelim (Hn H).
 114 nqed. *)
 115
 116 theorem not_to_not : ∀A,B:Prop. (A → B) → ¬B →¬A.
 117 /4/; qed.
 118
 119 (* inequality *)
 120 interpretation "leibnitz's non-equality" 'neq t x y = (Not (eq t x y)).
 121
 122 theorem sym_not_eq: ∀A.∀x,y:A. x ≠ y → y ≠ x.
 123 /3/; qed.
 124
 125 (* and *)
 126 inductive And (A,B:Prop) : Prop ≝
 127     conj : A → B → And A B.
 128
 129 interpretation "logical and" 'and x y = (And x y).
 130
 131 theorem proj1: ∀A,B:Prop. A ∧ B → A.
 132 #A #B #AB (elim AB) //; qed.
 133
 134 theorem proj2: ∀ A,B:Prop. A ∧ B → B.
 135 #A #B #AB (elim AB) //; qed.
 136
 137 (* or *)
 138 inductive Or (A,B:Prop) : Prop ≝
 139      or_introl : A → (Or A B)
 140    | or_intror : B → (Or A B).
 141
 142 interpretation "logical or" 'or x y = (Or x y).
 143
 144 definition decidable : Prop → Prop ≝
 145 λ A:Prop. A ∨ ¬ A.
 146
 147 (* exists *)
 148 inductive ex (A:Type[0]) (P:A → Prop) : Prop ≝
 149     ex_intro: ∀ x:A. P x →  ex A P.
 150
 151 interpretation "exists" 'exists x = (ex ? x).
 152
 153 inductive ex2 (A:Type[0]) (P,Q:A →Prop) : Prop ≝
 154     ex_intro2: ∀ x:A. P x → Q x → ex2 A P Q.
 155
 156 (* iff *)
 157 definition iff :=
 158  λ A,B. (A → B) ∧ (B → A).
 159
 160 interpretation "iff" 'iff a b = (iff a b).
 161
 162 lemma iff_sym: ∀A,B. A ↔ B → B ↔ A.
 163 #A #B * /3/ qed.
 164
 165 lemma iff_trans:∀A,B,C. A ↔ B → B ↔ C → A ↔ C.
 166 #A #B #C * #H1 #H2 * #H3 #H4 % /3/ qed.
 167
 168 lemma iff_not: ∀A,B. A ↔ B → ¬A ↔ ¬B.
 169 #A #B * #H1 #H2 % /3/ qed.
 170
 171 lemma iff_and_l: ∀A,B,C. A ↔ B → C ∧ A ↔ C ∧ B.
 172 #A #B #C * #H1 #H2 % * /3/ qed.
 173
 174 lemma iff_and_r: ∀A,B,C. A ↔ B → A ∧ C ↔ B ∧ C.
 175 #A #B #C * #H1 #H2 % * /3/ qed.
 176
 177 lemma iff_or_l: ∀A,B,C. A ↔ B → C ∨ A ↔ C ∨ B.
 178 #A #B #C * #H1 #H2 % * /3/ qed.
 179
 180 lemma iff_or_r: ∀A,B,C. A ↔ B → A ∨ C ↔ B ∨ C.
 181 #A #B #C * #H1 #H2 % * /3/ qed.
 182
 183 (* cose per destruct: da rivedere *)
 184
 185 definition R0 ≝ λT:Type[0].λt:T.t.
 186
 187 definition R1 ≝ eq_rect_Type0.
 188
 189 (* used for lambda-delta *)
 190 definition R2 :
 191   ∀T0:Type[0].
 192   ∀a0:T0.
 193   ∀T1:∀x0:T0. a0=x0 → Type[0].
 194   ∀a1:T1 a0 (refl ? a0).
 195   ∀T2:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0. R1 ?? T1 a1 ? p0 = x1 → Type[0].
 196   ∀a2:T2 a0 (refl ? a0) a1 (refl ? a1).
 197   ∀b0:T0.
 198   ∀e0:a0 = b0.
 199   ∀b1: T1 b0 e0.
 200   ∀e1:R1 ?? T1 a1 ? e0 = b1.
 201   T2 b0 e0 b1 e1.
 202 #T0 #a0 #T1 #a1 #T2 #a2 #b0 #e0 #b1 #e1
 203 @(eq_rect_Type0 ????? e1)
 204 @(R1 ?? ? ?? e0)
 205 @a2
 206 qed.
 207
 208 definition R3 :
 209   ∀T0:Type[0].
 210   ∀a0:T0.
 211   ∀T1:∀x0:T0. a0=x0 → Type[0].
 212   ∀a1:T1 a0 (refl ? a0).
 213   ∀T2:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0. R1 ?? T1 a1 ? p0 = x1 → Type[0].
 214   ∀a2:T2 a0 (refl ? a0) a1 (refl ? a1).
 215   ∀T3:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0.∀p1:R1 ?? T1 a1 ? p0 = x1.
 216       ∀x2:T2 x0 p0 x1 p1.R2 ???? T2 a2 x0 p0 ? p1 = x2 → Type[0].
 217   ∀a3:T3 a0 (refl ? a0) a1 (refl ? a1) a2 (refl ? a2).
 218   ∀b0:T0.
 219   ∀e0:a0 = b0.
 220   ∀b1: T1 b0 e0.
 221   ∀e1:R1 ?? T1 a1 ? e0 = b1.
 222   ∀b2: T2 b0 e0 b1 e1.
 223   ∀e2:R2 ???? T2 a2 b0 e0 ? e1 = b2.
 224   T3 b0 e0 b1 e1 b2 e2.
 225 #T0 #a0 #T1 #a1 #T2 #a2 #T3 #a3 #b0 #e0 #b1 #e1 #b2 #e2
 226 @(eq_rect_Type0 ????? e2)
 227 @(R2 ?? ? ???? e0 ? e1)
 228 @a3
 229 qed.
 230
 231 definition R4 :
 232   ∀T0:Type[0].
 233   ∀a0:T0.
 234   ∀T1:∀x0:T0. eq T0 a0 x0 → Type[0].
 235   ∀a1:T1 a0 (refl T0 a0).
 236   ∀T2:∀x0:T0. ∀p0:eq (T0 …) a0 x0. ∀x1:T1 x0 p0.eq (T1 …) (R1 T0 a0 T1 a1 x0 p0) x1 → Type[0].
 237   ∀a2:T2 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1).
 238   ∀T3:∀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.eq (T2 …) (R2 T0 a0 T1 a1 T2 a2 x0 p0 x1 p1) x2 → Type[0].
 240   ∀a3:T3 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1)
 241       a2 (refl (T2 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1)) a2).
 242   ∀T4:∀x0:T0. ∀p0:eq (T0 …) a0 x0. ∀x1:T1 x0 p0.∀p1:eq (T1 …) (R1 T0 a0 T1 a1 x0 p0) x1.
 243       ∀x2:T2 x0 p0 x1 p1.∀p2:eq (T2 …) (R2 T0 a0 T1 a1 T2 a2 x0 p0 x1 p1) x2.
 244       ∀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.
 245       Type[0].
 246   ∀a4:T4 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1)
 247       a2 (refl (T2 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1)) a2)
 248       a3 (refl (T3 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1)
 249                    a2 (refl (T2 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1)) a2))
 250                    a3).
 251   ∀b0:T0.
 252   ∀e0:eq (T0 …) a0 b0.
 253   ∀b1: T1 b0 e0.
 254   ∀e1:eq (T1 …) (R1 T0 a0 T1 a1 b0 e0) b1.
 255   ∀b2: T2 b0 e0 b1 e1.
 256   ∀e2:eq (T2 …) (R2 T0 a0 T1 a1 T2 a2 b0 e0 b1 e1) b2.
 257   ∀b3: T3 b0 e0 b1 e1 b2 e2.
 258   ∀e3:eq (T3 …) (R3 T0 a0 T1 a1 T2 a2 T3 a3 b0 e0 b1 e1 b2 e2) b3.
 259   T4 b0 e0 b1 e1 b2 e2 b3 e3.
 260 #T0 #a0 #T1 #a1 #T2 #a2 #T3 #a3 #T4 #a4 #b0 #e0 #b1 #e1 #b2 #e2 #b3 #e3
 261 @(eq_rect_Type0 ????? e3)
 262 @(R3 ????????? e0 ? e1 ? e2)
 263 @a4
 264 qed.
 265
 266 definition eqProp ≝ λA:Prop.eq A.
 267
 268 (* Example to avoid indexing and the consequential creation of ill typed
 269    terms during paramodulation *)
 270 lemma lemmaK : ∀A.∀x:A.∀h:x=x. eqProp ? h (refl A x).
 271 #A #x #h @(refl ? h: eqProp ? ? ?).
 272 qed-.
 273
 274 theorem streicherK : ∀T:Type[2].∀t:T.∀P:t = t → Type[3].P (refl ? t) → ∀p.P p.
 275  #T #t #P #H #p >(lemmaK T t p) @H
 276 qed-.