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