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 (generalize in match H) (generalize in match 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 (generalize in match H) (generalize in match 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 (generalize in match H) (generalize in match 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 (generalize in match H) (generalize in match 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 (* cose per destruct: da rivedere *)
 159
 160 definition R0 ≝ λT:Type[0].λt:T.t.
 161
 162 definition R1 ≝ eq_rect_Type0.
 163
 164 (* used for lambda-delta *)
 165 definition R2 :
 166   ∀T0:Type[0].
 167   ∀a0:T0.
 168   ∀T1:∀x0:T0. a0=x0 → Type[0].
 169   ∀a1:T1 a0 (refl ? a0).
 170   ∀T2:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0. R1 ?? T1 a1 ? p0 = x1 → Type[0].
 171   ∀a2:T2 a0 (refl ? a0) a1 (refl ? a1).
 172   ∀b0:T0.
 173   ∀e0:a0 = b0.
 174   ∀b1: T1 b0 e0.
 175   ∀e1:R1 ?? T1 a1 ? e0 = b1.
 176   T2 b0 e0 b1 e1.
 177 #T0 #a0 #T1 #a1 #T2 #a2 #b0 #e0 #b1 #e1
 178 @(eq_rect_Type0 ????? e1)
 179 @(R1 ?? ? ?? e0)
 180 @a2
 181 qed.
 182
 183 definition R3 :
 184   ∀T0:Type[0].
 185   ∀a0:T0.
 186   ∀T1:∀x0:T0. a0=x0 → Type[0].
 187   ∀a1:T1 a0 (refl ? a0).
 188   ∀T2:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0. R1 ?? T1 a1 ? p0 = x1 → Type[0].
 189   ∀a2:T2 a0 (refl ? a0) a1 (refl ? a1).
 190   ∀T3:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0.∀p1:R1 ?? T1 a1 ? p0 = x1.
 191       ∀x2:T2 x0 p0 x1 p1.R2 ???? T2 a2 x0 p0 ? p1 = x2 → Type[0].
 192   ∀a3:T3 a0 (refl ? a0) a1 (refl ? a1) a2 (refl ? a2).
 193   ∀b0:T0.
 194   ∀e0:a0 = b0.
 195   ∀b1: T1 b0 e0.
 196   ∀e1:R1 ?? T1 a1 ? e0 = b1.
 197   ∀b2: T2 b0 e0 b1 e1.
 198   ∀e2:R2 ???? T2 a2 b0 e0 ? e1 = b2.
 199   T3 b0 e0 b1 e1 b2 e2.
 200 #T0 #a0 #T1 #a1 #T2 #a2 #T3 #a3 #b0 #e0 #b1 #e1 #b2 #e2
 201 @(eq_rect_Type0 ????? e2)
 202 @(R2 ?? ? ???? e0 ? e1)
 203 @a3
 204 qed.
 205
 206 definition R4 :
 207   ∀T0:Type[0].
 208   ∀a0:T0.
 209   ∀T1:∀x0:T0. eq T0 a0 x0 → Type[0].
 210   ∀a1:T1 a0 (refl T0 a0).
 211   ∀T2:∀x0:T0. ∀p0:eq (T0 …) a0 x0. ∀x1:T1 x0 p0.eq (T1 …) (R1 T0 a0 T1 a1 x0 p0) x1 → Type[0].
 212   ∀a2:T2 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1).
 213   ∀T3:∀x0:T0. ∀p0:eq (T0 …) a0 x0. ∀x1:T1 x0 p0.∀p1:eq (T1 …) (R1 T0 a0 T1 a1 x0 p0) x1.
 214       ∀x2:T2 x0 p0 x1 p1.eq (T2 …) (R2 T0 a0 T1 a1 T2 a2 x0 p0 x1 p1) x2 → Type[0].
 215   ∀a3:T3 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1)
 216       a2 (refl (T2 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1)) a2).
 217   ∀T4:∀x0:T0. ∀p0:eq (T0 …) a0 x0. ∀x1:T1 x0 p0.∀p1:eq (T1 …) (R1 T0 a0 T1 a1 x0 p0) x1.
 218       ∀x2:T2 x0 p0 x1 p1.∀p2:eq (T2 …) (R2 T0 a0 T1 a1 T2 a2 x0 p0 x1 p1) x2.
 219       ∀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.
 220       Type[0].
 221   ∀a4:T4 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1)
 222       a2 (refl (T2 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1)) a2)
 223       a3 (refl (T3 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1)
 224                    a2 (refl (T2 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1)) a2))
 225                    a3).
 226   ∀b0:T0.
 227   ∀e0:eq (T0 …) a0 b0.
 228   ∀b1: T1 b0 e0.
 229   ∀e1:eq (T1 …) (R1 T0 a0 T1 a1 b0 e0) b1.
 230   ∀b2: T2 b0 e0 b1 e1.
 231   ∀e2:eq (T2 …) (R2 T0 a0 T1 a1 T2 a2 b0 e0 b1 e1) b2.
 232   ∀b3: T3 b0 e0 b1 e1 b2 e2.
 233   ∀e3:eq (T3 …) (R3 T0 a0 T1 a1 T2 a2 T3 a3 b0 e0 b1 e1 b2 e2) b3.
 234   T4 b0 e0 b1 e1 b2 e2 b3 e3.
 235 #T0 #a0 #T1 #a1 #T2 #a2 #T3 #a3 #T4 #a4 #b0 #e0 #b1 #e1 #b2 #e2 #b3 #e3
 236 @(eq_rect_Type0 ????? e3)
 237 @(R3 ????????? e0 ? e1 ? e2)
 238 @a4
 239 qed.
 240
 241 definition eqProp ≝ λA:Prop.eq A.
 242
 243 (* Example to avoid indexing and the consequential creation of ill typed
 244    terms during paramodulation *)
 245 example lemmaK : ∀A.∀x:A.∀h:x=x. eqProp ? h (refl A x).
 246 #A #x #h @(refl ? h: eqProp ? ? ?).
 247 qed.
 248
 249 theorem streicherK : ∀T:Type[2].∀t:T.∀P:t = t → Type[3].P (refl ? t) → ∀p.P p.
 250  #T #t #P #H #p >(lemmaK T t p) @H
 251 qed.