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