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