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 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     ex2_intro: ∀ x:A. P x → Q x → ex2 A P Q.
 151
 152 interpretation "exists on two predicates" 'exists2 x1 x2 = (ex2 ? x1 x2).
 153
 154 lemma ex2_commute: ∀A0. ∀P0,P1:A0→Prop. (∃∃x0. P0 x0 & P1 x0) → ∃∃x0. P1 x0 & P0 x0.
 155 #A0 #P0 #P1 * /2 width=3/
 156 qed-.
 157
 158 (* iff *)
 159 definition iff :=
 160  λ A,B. (A → B) ∧ (B → A).
 161
 162 interpretation "iff" 'iff a b = (iff a b).
 163
 164 lemma iff_sym: ∀A,B. A ↔ B → B ↔ A.
 165 #A #B * /3/ qed.
 166
 167 lemma iff_trans:∀A,B,C. A ↔ B → B ↔ C → A ↔ C.
 168 #A #B #C * #H1 #H2 * #H3 #H4 % /3/ qed.
 169
 170 lemma iff_not: ∀A,B. A ↔ B → ¬A ↔ ¬B.
 171 #A #B * #H1 #H2 % /3/ qed.
 172
 173 lemma iff_and_l: ∀A,B,C. A ↔ B → C ∧ A ↔ C ∧ B.
 174 #A #B #C * #H1 #H2 % * /3/ qed.
 175
 176 lemma iff_and_r: ∀A,B,C. A ↔ B → A ∧ C ↔ B ∧ C.
 177 #A #B #C * #H1 #H2 % * /3/ qed.
 178
 179 lemma iff_or_l: ∀A,B,C. A ↔ B → C ∨ A ↔ C ∨ B.
 180 #A #B #C * #H1 #H2 % * /3/ qed.
 181
 182 lemma iff_or_r: ∀A,B,C. A ↔ B → A ∨ C ↔ B ∨ C.
 183 #A #B #C * #H1 #H2 % * /3/ qed.
 184
 185 (* cose per destruct: da rivedere *)
 186
 187 definition R0 ≝ λT:Type[0].λt:T.t.
 188
 189 definition R1 ≝ eq_rect_Type0.
 190
 191 (* used for lambda-delta *)
 192 definition R2 :
 193   ∀T0:Type[0].
 194   ∀a0:T0.
 195   ∀T1:∀x0:T0. a0=x0 → Type[0].
 196   ∀a1:T1 a0 (refl ? a0).
 197   ∀T2:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0. R1 ?? T1 a1 ? p0 = x1 → Type[0].
 198   ∀a2:T2 a0 (refl ? a0) a1 (refl ? a1).
 199   ∀b0:T0.
 200   ∀e0:a0 = b0.
 201   ∀b1: T1 b0 e0.
 202   ∀e1:R1 ?? T1 a1 ? e0 = b1.
 203   T2 b0 e0 b1 e1.
 204 #T0 #a0 #T1 #a1 #T2 #a2 #b0 #e0 #b1 #e1
 205 @(eq_rect_Type0 ????? e1)
 206 @(R1 ?? ? ?? e0)
 207 @a2
 208 qed.
 209
 210 definition R3 :
 211   ∀T0:Type[0].
 212   ∀a0:T0.
 213   ∀T1:∀x0:T0. a0=x0 → Type[0].
 214   ∀a1:T1 a0 (refl ? a0).
 215   ∀T2:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0. R1 ?? T1 a1 ? p0 = x1 → Type[0].
 216   ∀a2:T2 a0 (refl ? a0) a1 (refl ? a1).
 217   ∀T3:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0.∀p1:R1 ?? T1 a1 ? p0 = x1.
 218       ∀x2:T2 x0 p0 x1 p1.R2 ???? T2 a2 x0 p0 ? p1 = x2 → Type[0].
 219   ∀a3:T3 a0 (refl ? a0) a1 (refl ? a1) a2 (refl ? a2).
 220   ∀b0:T0.
 221   ∀e0:a0 = b0.
 222   ∀b1: T1 b0 e0.
 223   ∀e1:R1 ?? T1 a1 ? e0 = b1.
 224   ∀b2: T2 b0 e0 b1 e1.
 225   ∀e2:R2 ???? T2 a2 b0 e0 ? e1 = b2.
 226   T3 b0 e0 b1 e1 b2 e2.
 227 #T0 #a0 #T1 #a1 #T2 #a2 #T3 #a3 #b0 #e0 #b1 #e1 #b2 #e2
 228 @(eq_rect_Type0 ????? e2)
 229 @(R2 ?? ? ???? e0 ? e1)
 230 @a3
 231 qed.
 232
 233 definition R4 :
 234   ∀T0:Type[0].
 235   ∀a0:T0.
 236   ∀T1:∀x0:T0. eq T0 a0 x0 → Type[0].
 237   ∀a1:T1 a0 (refl T0 a0).
 238   ∀T2:∀x0:T0. ∀p0:eq (T0 …) a0 x0. ∀x1:T1 x0 p0.eq (T1 …) (R1 T0 a0 T1 a1 x0 p0) x1 → Type[0].
 239   ∀a2:T2 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1).
 240   ∀T3:∀x0:T0. ∀p0:eq (T0 …) a0 x0. ∀x1:T1 x0 p0.∀p1:eq (T1 …) (R1 T0 a0 T1 a1 x0 p0) x1.
 241       ∀x2:T2 x0 p0 x1 p1.eq (T2 …) (R2 T0 a0 T1 a1 T2 a2 x0 p0 x1 p1) x2 → Type[0].
 242   ∀a3:T3 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   ∀T4:∀x0:T0. ∀p0:eq (T0 …) a0 x0. ∀x1:T1 x0 p0.∀p1:eq (T1 …) (R1 T0 a0 T1 a1 x0 p0) x1.
 245       ∀x2:T2 x0 p0 x1 p1.∀p2:eq (T2 …) (R2 T0 a0 T1 a1 T2 a2 x0 p0 x1 p1) x2.
 246       ∀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.
 247       Type[0].
 248   ∀a4:T4 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 (refl (T3 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1)
 251                    a2 (refl (T2 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1)) a2))
 252                    a3).
 253   ∀b0:T0.
 254   ∀e0:eq (T0 …) a0 b0.
 255   ∀b1: T1 b0 e0.
 256   ∀e1:eq (T1 …) (R1 T0 a0 T1 a1 b0 e0) b1.
 257   ∀b2: T2 b0 e0 b1 e1.
 258   ∀e2:eq (T2 …) (R2 T0 a0 T1 a1 T2 a2 b0 e0 b1 e1) b2.
 259   ∀b3: T3 b0 e0 b1 e1 b2 e2.
 260   ∀e3:eq (T3 …) (R3 T0 a0 T1 a1 T2 a2 T3 a3 b0 e0 b1 e1 b2 e2) b3.
 261   T4 b0 e0 b1 e1 b2 e2 b3 e3.
 262 #T0 #a0 #T1 #a1 #T2 #a2 #T3 #a3 #T4 #a4 #b0 #e0 #b1 #e1 #b2 #e2 #b3 #e3
 263 @(eq_rect_Type0 ????? e3)
 264 @(R3 ????????? e0 ? e1 ? e2)
 265 @a4
 266 qed.
 267
 268 definition eqProp ≝ λA:Prop.eq A.
 269
 270 (* Example to avoid indexing and the consequential creation of ill typed
 271    terms during paramodulation *)
 272 lemma lemmaK : ∀A.∀x:A.∀h:x=x. eqProp ? h (refl A x).
 273 #A #x #h @(refl ? h: eqProp ? ? ?).
 274 qed-.
 275
 276 theorem streicherK : ∀T:Type[2].∀t:T.∀P:t = t → Type[3].P (refl ? t) → ∀p.P p.
 277  #T #t #P #H #p >(lemmaK T t p) @H
 278 qed-.