matitaB/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 (* hint to genereric equality
  59 definition eq_equality: equality ≝
  60  mk_equality eq refl rewrite_l rewrite_r.
  61
  62
  63 unification hint 0 ≔ T,a,b;
  64  X ≟ eq_equality
  65 (*------------------------------------*) ⊢
  66     equal X T a b ≡ eq T a b.
  67 *)
  68
  69 (********** connectives ********)
  70
  71 inductive True: Prop ≝
  72 I : True.
  73
  74 inductive False: Prop ≝ .
  75
  76 (* ndefinition Not: Prop → Prop ≝
  77 λA. A → False. *)
  78
  79 inductive Not (A:Prop): Prop ≝
  80 nmk: (A → False) → Not A.
  81
  82 interpretation "logical not" 'not x = (Not x).
  83
  84 theorem absurd : ∀A:Prop. A → ¬A → False.
  85 #A #H #Hn (elim Hn); /2/; qed.
  86
  87 (*
  88 ntheorem absurd : ∀ A,C:Prop. A → ¬A → C.
  89 #A; #C; #H; #Hn; nelim (Hn H).
  90 nqed. *)
  91
  92 theorem not_to_not : ∀A,B:Prop. (A → B) → ¬B →¬A.
  93 /4/; qed.
  94
  95 (* inequality *)
  96 interpretation "leibnitz's non-equality" 'neq t x y = (Not (eq t x y)).
  97
  98 theorem sym_not_eq: ∀A.∀x,y:A. x ≠ y → y ≠ x.
  99 /3/; qed.
 100
 101 (* and *)
 102 inductive And (A,B:Prop) : Prop ≝
 103     conj : A → B → And A B.
 104
 105 interpretation "logical and" 'and x y = (And x y).
 106
 107 theorem proj1: ∀A,B:Prop. A ∧ B → A.
 108 #A #B #AB (elim AB) //; qed.
 109
 110 theorem proj2: ∀ A,B:Prop. A ∧ B → B.
 111 #A #B #AB (elim AB) //; qed.
 112
 113 (* or *)
 114 inductive Or (A,B:Prop) : Prop ≝
 115      or_introl : A → (Or A B)
 116    | or_intror : B → (Or A B).
 117
 118 interpretation "logical or" 'or x y = (Or x y).
 119
 120 definition decidable : Prop → Prop ≝
 121 λ A:Prop. A ∨ ¬ A.
 122
 123 (* exists *)
 124 inductive ex (A:Type[0]) (P:A → Prop) : Prop ≝
 125     ex_intro: ∀ x:A. P x →  ex A P.
 126
 127 interpretation "exists" 'exists x = (ex ? x).
 128
 129 inductive ex2 (A:Type[0]) (P,Q:A →Prop) : Prop ≝
 130     ex_intro2: ∀ x:A. P x → Q x → ex2 A P Q.
 131
 132 (* iff *)
 133 definition iff :=
 134  λ A,B. (A → B) ∧ (B → A).
 135
 136 interpretation "iff" 'iff a b = (iff a b).
 137
 138 (* cose per destruct: da rivedere *)
 139
 140 definition R0 ≝ λT:Type[0].λt:T.t.
 141
 142 definition R1 ≝ eq_rect_Type0.
 143
 144 (* useless stuff
 145 definition R2 :
 146   ∀T0:Type[0].
 147   ∀a0:T0.
 148   ∀T1:∀x0:T0. a0=x0 → Type[0].
 149   ∀a1:T1 a0 (refl ? a0).
 150   ∀T2:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0. R1 ?? T1 a1 ? p0 = x1 → Type[0].
 151   ∀a2:T2 a0 (refl ? a0) a1 (refl ? a1).
 152   ∀b0:T0.
 153   ∀e0:a0 = b0.
 154   ∀b1: T1 b0 e0.
 155   ∀e1:R1 ?? T1 a1 ? e0 = b1.
 156   T2 b0 e0 b1 e1.
 157 #T0 #a0 #T1 #a1 #T2 #a2 #b0 #e0 #b1 #e1
 158 @(eq_rect_Type0 ????? e1)
 159 @(R1 ?? ? ?? e0)
 160 @a2
 161 qed.
 162
 163 definition R3 :
 164   ∀T0:Type[0].
 165   ∀a0:T0.
 166   ∀T1:∀x0:T0. a0=x0 → Type[0].
 167   ∀a1:T1 a0 (refl ? a0).
 168   ∀T2:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0. R1 ?? T1 a1 ? p0 = x1 → Type[0].
 169   ∀a2:T2 a0 (refl ? a0) a1 (refl ? a1).
 170   ∀T3:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0.∀p1:R1 ?? T1 a1 ? p0 = x1.
 171       ∀x2:T2 x0 p0 x1 p1.R2 ???? T2 a2 x0 p0 ? p1 = x2 → Type[0].
 172   ∀a3:T3 a0 (refl ? a0) a1 (refl ? a1) a2 (refl ? a2).
 173   ∀b0:T0.
 174   ∀e0:a0 = b0.
 175   ∀b1: T1 b0 e0.
 176   ∀e1:R1 ?? T1 a1 ? e0 = b1.
 177   ∀b2: T2 b0 e0 b1 e1.
 178   ∀e2:R2 ???? T2 a2 b0 e0 ? e1 = b2.
 179   T3 b0 e0 b1 e1 b2 e2.
 180 #T0 #a0 #T1 #a1 #T2 #a2 #T3 #a3 #b0 #e0 #b1 #e1 #b2 #e2
 181 @(eq_rect_Type0 ????? e2)
 182 @(R2 ?? ? ???? e0 ? e1)
 183 @a3
 184 qed.
 185
 186 definition R4 :
 187   ∀T0:Type[0].
 188   ∀a0:T0.
 189   ∀T1:∀x0:T0. eq T0 a0 x0 → Type[0].
 190   ∀a1:T1 a0 (refl T0 a0).
 191   ∀T2:∀x0:T0. ∀p0:eq (T0 …) a0 x0. ∀x1:T1 x0 p0.eq (T1 …) (R1 T0 a0 T1 a1 x0 p0) x1 → Type[0].
 192   ∀a2:T2 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1).
 193   ∀T3:∀x0:T0. ∀p0:eq (T0 …) a0 x0. ∀x1:T1 x0 p0.∀p1:eq (T1 …) (R1 T0 a0 T1 a1 x0 p0) x1.
 194       ∀x2:T2 x0 p0 x1 p1.eq (T2 …) (R2 T0 a0 T1 a1 T2 a2 x0 p0 x1 p1) x2 → Type[0].
 195   ∀a3:T3 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1)
 196       a2 (refl (T2 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1)) a2).
 197   ∀T4:∀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.∀p2:eq (T2 …) (R2 T0 a0 T1 a1 T2 a2 x0 p0 x1 p1) x2.
 199       ∀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.
 200       Type[0].
 201   ∀a4:T4 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1)
 202       a2 (refl (T2 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1)) a2)
 203       a3 (refl (T3 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1)
 204                    a2 (refl (T2 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1)) a2))
 205                    a3).
 206   ∀b0:T0.
 207   ∀e0:eq (T0 …) a0 b0.
 208   ∀b1: T1 b0 e0.
 209   ∀e1:eq (T1 …) (R1 T0 a0 T1 a1 b0 e0) b1.
 210   ∀b2: T2 b0 e0 b1 e1.
 211   ∀e2:eq (T2 …) (R2 T0 a0 T1 a1 T2 a2 b0 e0 b1 e1) b2.
 212   ∀b3: T3 b0 e0 b1 e1 b2 e2.
 213   ∀e3:eq (T3 …) (R3 T0 a0 T1 a1 T2 a2 T3 a3 b0 e0 b1 e1 b2 e2) b3.
 214   T4 b0 e0 b1 e1 b2 e2 b3 e3.
 215 #T0 #a0 #T1 #a1 #T2 #a2 #T3 #a3 #T4 #a4 #b0 #e0 #b1 #e1 #b2 #e2 #b3 #e3
 216 @(eq_rect_Type0 ????? e3)
 217 @(R3 ????????? e0 ? e1 ? e2)
 218 @a4
 219 qed. *)
 220
 221 (* TODO concrete definition by means of proof irrelevance *)
 222 axiom streicherK : ∀T:Type[1].∀t:T.∀P:t = t → Type[2].P (refl ? t) → ∀p.P p.