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