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