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:<A href="cic:/matita/basics/logic/eq.ind(1,0,2)">eq</A> ? x a.∀P:
  24  ∀x:A. x <A title="leibnitz's equality" href="cic:/fakeuri.def(1)">=</A> 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 title="leibnitz's equality" href="cic:/fakeuri.def(1)">=</A> a → Prop. P a (<A href="cic:/matita/basics/logic/eq.con(0,1,2)">refl</A> A a) →
  29    ∀x.∀p:<A href="cic:/matita/basics/logic/eq.ind(1,0,2)">eq</A> ? x a.P x p.
  30  #A #a #P #p #x0 #p0; @(<A href="cic:/matita/basics/logic/eq_rect_r.def(1)">eq_rect_r</A> ? ? ? p0) //; qed.
  31
  32 lemma eq_rect_Type2_r:
  33   ∀A.∀a.∀P: ∀x:A. <A href="cic:/matita/basics/logic/eq.ind(1,0,2)">eq</A> ? x a → Type[2]. P a (<A href="cic:/matita/basics/logic/eq.con(0,1,2)">refl</A> A a) →
  34     ∀x.∀p:<A href="cic:/matita/basics/logic/eq.ind(1,0,2)">eq</A> ? 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 <A title="leibnitz's equality" href="cic:/fakeuri.def(1)">=</A> y → P y.
  39 #A #x #P #Hx #y #Heq (cases Heq); //; qed.
  40
  41 theorem sym_eq: ∀A.∀x,y:A. x <A title="leibnitz's equality" href="cic:/fakeuri.def(1)">=</A> y → y <A title="leibnitz's equality" href="cic:/fakeuri.def(1)">=</A> x.
  42 #A #x #y #Heq @(<A href="cic:/matita/basics/logic/rewrite_l.def(1)">rewrite_l</A> A x (λz.z<A title="leibnitz's equality" href="cic:/fakeuri.def(1)">=</A>x)); //; qed.
  43
  44 theorem rewrite_r: ∀A:Type[1].∀x.∀P:A → Type[1]. P x → ∀y. y <A title="leibnitz's equality" href="cic:/fakeuri.def(1)">=</A> x → P y.
  45 #A #x #P #Hx #y #Heq (cases (<A href="cic:/matita/basics/logic/sym_eq.def(2)">sym_eq</A> ? ? ? Heq)); //; qed.
  46
  47 theorem eq_coerc: ∀A,B:Type[0].A→(A<A title="leibnitz's equality" href="cic:/fakeuri.def(1)">=</A>B)→B.
  48 #A #B #Ha #Heq (elim Heq); //; qed.
  49
  50 theorem trans_eq : ∀A.∀x,y,z:A. x <A title="leibnitz's equality" href="cic:/fakeuri.def(1)">=</A> y → y <A title="leibnitz's equality" href="cic:/fakeuri.def(1)">=</A> z → x <A title="leibnitz's equality" href="cic:/fakeuri.def(1)">=</A> z.
  51 #A #x #y #z #H1 #H2 >H1; //; qed.
  52
  53 theorem eq_f: ∀A,B.∀f:A→B.∀x,y:A. x<A title="leibnitz's equality" href="cic:/fakeuri.def(1)">=</A>y → f x <A title="leibnitz's equality" href="cic:/fakeuri.def(1)">=</A> 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<A title="leibnitz's equality" href="cic:/fakeuri.def(1)">=</A>x2 → y1<A title="leibnitz's equality" href="cic:/fakeuri.def(1)">=</A>y2 → f x1 y1 <A title="leibnitz's equality" href="cic:/fakeuri.def(1)">=</A> 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 → <A href="cic:/matita/basics/logic/False.ind(1,0,0)">False</A>) → Not A.
  84
  85
  86 interpretation "logical not" 'not x = (Not x).
  87
  88 theorem absurd : ∀A:Prop. A → <A title="logical not" href="cic:/fakeuri.def(1)">¬</A>A → <A href="cic:/matita/basics/logic/False.ind(1,0,0)">False</A>.
  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) → <A title="logical not" href="cic:/fakeuri.def(1)">¬</A>B →<A title="logical not" href="cic:/fakeuri.def(1)">¬</A>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 <A title="leibnitz's non-equality" href="cic:/fakeuri.def(1)">≠</A> y → y <A title="leibnitz's non-equality" href="cic:/fakeuri.def(1)">≠</A> 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 <A title="logical and" href="cic:/fakeuri.def(1)">∧</A> B → A.
 112 #A #B #AB (elim AB) //; qed.
 113
 114 theorem proj2: ∀ A,B:Prop. A <A title="logical and" href="cic:/fakeuri.def(1)">∧</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 title="logical or" href="cic:/fakeuri.def(1)">∨</A> <A title="logical not" href="cic:/fakeuri.def(1)">¬</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) <A title="logical and" href="cic:/fakeuri.def(1)">∧</A> (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 ≝ <A href="cic:/matita/basics/logic/eq_rect_Type0.fix(0,5,1)">eq_rect_Type0</A>.
 147
 148 (* useless stuff *)
 149 definition R2 :
 150   ∀T0:Type[0].
 151   ∀a0:T0.
 152   ∀T1:∀x0:T0. a0<A title="leibnitz's equality" href="cic:/fakeuri.def(1)">=</A>x0 → Type[0].
 153   ∀a1:T1 a0 (<A href="cic:/matita/basics/logic/eq.con(0,1,2)">refl</A> ? a0).
 154   ∀T2:∀x0:T0. ∀p0:a0<A title="leibnitz's equality" href="cic:/fakeuri.def(1)">=</A>x0. ∀x1:T1 x0 p0. <A href="cic:/matita/basics/logic/R1.def(2)">R1</A> ?? T1 a1 ? p0 <A title="leibnitz's equality" href="cic:/fakeuri.def(1)">=</A> x1 → Type[0].
 155   ∀a2:T2 a0 (<A href="cic:/matita/basics/logic/eq.con(0,1,2)">refl</A> ? a0) a1 (<A href="cic:/matita/basics/logic/eq.con(0,1,2)">refl</A> ? a1).
 156   ∀b0:T0.
 157   ∀e0:a0 <A title="leibnitz's equality" href="cic:/fakeuri.def(1)">=</A> b0.
 158   ∀b1: T1 b0 e0.
 159   ∀e1:<A href="cic:/matita/basics/logic/R1.def(2)">R1</A> ?? T1 a1 ? e0 <A title="leibnitz's equality" href="cic:/fakeuri.def(1)">=</A> b1.
 160   T2 b0 e0 b1 e1.
 161 #T0 #a0 #T1 #a1 #T2 #a2 #b0 #e0 #b1 #e1
 162 @(<A href="cic:/matita/basics/logic/eq_rect_Type0.fix(0,5,1)">eq_rect_Type0</A> ????? e1)
 163 @(<A href="cic:/matita/basics/logic/R1.def(2)">R1</A> ?? ? ?? e0)
 164 @a2
 165 qed.
 166
 167 definition R3 :
 168   ∀T0:Type[0].
 169   ∀a0:T0.
 170   ∀T1:∀x0:T0. a0<A title="leibnitz's equality" href="cic:/fakeuri.def(1)">=</A>x0 → Type[0].
 171   ∀a1:T1 a0 (<A href="cic:/matita/basics/logic/eq.con(0,1,2)">refl</A> ? a0).
 172   ∀T2:∀x0:T0. ∀p0:a0<A title="leibnitz's equality" href="cic:/fakeuri.def(1)">=</A>x0. ∀x1:T1 x0 p0. <A href="cic:/matita/basics/logic/R1.def(2)">R1</A> ?? T1 a1 ? p0 <A title="leibnitz's equality" href="cic:/fakeuri.def(1)">=</A> x1 → Type[0].
 173   ∀a2:T2 a0 (<A href="cic:/matita/basics/logic/eq.con(0,1,2)">refl</A> ? a0) a1 (<A href="cic:/matita/basics/logic/eq.con(0,1,2)">refl</A> ? a1).
 174   ∀T3:∀x0:T0. ∀p0:a0<A title="leibnitz's equality" href="cic:/fakeuri.def(1)">=</A>x0. ∀x1:T1 x0 p0.∀p1:<A href="cic:/matita/basics/logic/R1.def(2)">R1</A> ?? T1 a1 ? p0 <A title="leibnitz's equality" href="cic:/fakeuri.def(1)">=</A> x1.
 175       ∀x2:T2 x0 p0 x1 p1.<A href="cic:/matita/basics/logic/R2.def(3)">R2</A> ???? T2 a2 x0 p0 ? p1 <A title="leibnitz's equality" href="cic:/fakeuri.def(1)">=</A> x2 → Type[0].
 176   ∀a3:T3 a0 (<A href="cic:/matita/basics/logic/eq.con(0,1,2)">refl</A> ? a0) a1 (<A href="cic:/matita/basics/logic/eq.con(0,1,2)">refl</A> ? a1) a2 (<A href="cic:/matita/basics/logic/eq.con(0,1,2)">refl</A> ? a2).
 177   ∀b0:T0.
 178   ∀e0:a0 <A title="leibnitz's equality" href="cic:/fakeuri.def(1)">=</A> b0.
 179   ∀b1: T1 b0 e0.
 180   ∀e1:<A href="cic:/matita/basics/logic/R1.def(2)">R1</A> ?? T1 a1 ? e0 <A title="leibnitz's equality" href="cic:/fakeuri.def(1)">=</A> b1.
 181   ∀b2: T2 b0 e0 b1 e1.
 182   ∀e2:<A href="cic:/matita/basics/logic/R2.def(3)">R2</A> ???? T2 a2 b0 e0 ? e1 <A title="leibnitz's equality" href="cic:/fakeuri.def(1)">=</A> 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 @(<A href="cic:/matita/basics/logic/eq_rect_Type0.fix(0,5,1)">eq_rect_Type0</A> ????? e2)
 186 @(<A href="cic:/matita/basics/logic/R2.def(3)">R2</A> ?? ? ???? e0 ? e1)
 187 @a3
 188 qed.
 189
 190 definition R4 :
 191   ∀T0:Type[0].
 192   ∀a0:T0.
 193   ∀T1:∀x0:T0. <A href="cic:/matita/basics/logic/eq.ind(1,0,2)">eq</A> T0 a0 x0 → Type[0].
 194   ∀a1:T1 a0 (<A href="cic:/matita/basics/logic/eq.con(0,1,2)">refl</A> T0 a0).
 195   ∀T2:∀x0:T0. ∀p0:<A href="cic:/matita/basics/logic/eq.ind(1,0,2)">eq</A> (T0 …) a0 x0. ∀x1:T1 x0 p0.<A href="cic:/matita/basics/logic/eq.ind(1,0,2)">eq</A> (T1 …) (<A href="cic:/matita/basics/logic/R1.def(2)">R1</A> T0 a0 T1 a1 x0 p0) x1 → Type[0].
 196   ∀a2:T2 a0 (<A href="cic:/matita/basics/logic/eq.con(0,1,2)">refl</A> T0 a0) a1 (<A href="cic:/matita/basics/logic/eq.con(0,1,2)">refl</A> (T1 a0 (<A href="cic:/matita/basics/logic/eq.con(0,1,2)">refl</A> T0 a0)) a1).
 197   ∀T3:∀x0:T0. ∀p0:<A href="cic:/matita/basics/logic/eq.ind(1,0,2)">eq</A> (T0 …) a0 x0. ∀x1:T1 x0 p0.∀p1:<A href="cic:/matita/basics/logic/eq.ind(1,0,2)">eq</A> (T1 …) (<A href="cic:/matita/basics/logic/R1.def(2)">R1</A> T0 a0 T1 a1 x0 p0) x1.
 198       ∀x2:T2 x0 p0 x1 p1.<A href="cic:/matita/basics/logic/eq.ind(1,0,2)">eq</A> (T2 …) (<A href="cic:/matita/basics/logic/R2.def(3)">R2</A> T0 a0 T1 a1 T2 a2 x0 p0 x1 p1) x2 → Type[0].
 199   ∀a3:T3 a0 (<A href="cic:/matita/basics/logic/eq.con(0,1,2)">refl</A> T0 a0) a1 (<A href="cic:/matita/basics/logic/eq.con(0,1,2)">refl</A> (T1 a0 (<A href="cic:/matita/basics/logic/eq.con(0,1,2)">refl</A> T0 a0)) a1)
 200       a2 (<A href="cic:/matita/basics/logic/eq.con(0,1,2)">refl</A> (T2 a0 (<A href="cic:/matita/basics/logic/eq.con(0,1,2)">refl</A> T0 a0) a1 (<A href="cic:/matita/basics/logic/eq.con(0,1,2)">refl</A> (T1 a0 (<A href="cic:/matita/basics/logic/eq.con(0,1,2)">refl</A> T0 a0)) a1)) a2).
 201   ∀T4:∀x0:T0. ∀p0:<A href="cic:/matita/basics/logic/eq.ind(1,0,2)">eq</A> (T0 …) a0 x0. ∀x1:T1 x0 p0.∀p1:<A href="cic:/matita/basics/logic/eq.ind(1,0,2)">eq</A> (T1 …) (<A href="cic:/matita/basics/logic/R1.def(2)">R1</A> T0 a0 T1 a1 x0 p0) x1.
 202       ∀x2:T2 x0 p0 x1 p1.∀p2:<A href="cic:/matita/basics/logic/eq.ind(1,0,2)">eq</A> (T2 …) (<A href="cic:/matita/basics/logic/R2.def(3)">R2</A> T0 a0 T1 a1 T2 a2 x0 p0 x1 p1) x2.
 203       ∀x3:T3 x0 p0 x1 p1 x2 p2.∀p3:<A href="cic:/matita/basics/logic/eq.ind(1,0,2)">eq</A> (T3 …) (<A href="cic:/matita/basics/logic/R3.def(4)">R3</A> T0 a0 T1 a1 T2 a2 T3 a3 x0 p0 x1 p1 x2 p2) x3.
 204       Type[0].
 205   ∀a4:T4 a0 (<A href="cic:/matita/basics/logic/eq.con(0,1,2)">refl</A> T0 a0) a1 (<A href="cic:/matita/basics/logic/eq.con(0,1,2)">refl</A> (T1 a0 (<A href="cic:/matita/basics/logic/eq.con(0,1,2)">refl</A> T0 a0)) a1)
 206       a2 (<A href="cic:/matita/basics/logic/eq.con(0,1,2)">refl</A> (T2 a0 (<A href="cic:/matita/basics/logic/eq.con(0,1,2)">refl</A> T0 a0) a1 (<A href="cic:/matita/basics/logic/eq.con(0,1,2)">refl</A> (T1 a0 (<A href="cic:/matita/basics/logic/eq.con(0,1,2)">refl</A> T0 a0)) a1)) a2)
 207       a3 (<A href="cic:/matita/basics/logic/eq.con(0,1,2)">refl</A> (T3 a0 (<A href="cic:/matita/basics/logic/eq.con(0,1,2)">refl</A> T0 a0) a1 (<A href="cic:/matita/basics/logic/eq.con(0,1,2)">refl</A> (T1 a0 (<A href="cic:/matita/basics/logic/eq.con(0,1,2)">refl</A> T0 a0)) a1)
 208                    a2 (<A href="cic:/matita/basics/logic/eq.con(0,1,2)">refl</A> (T2 a0 (<A href="cic:/matita/basics/logic/eq.con(0,1,2)">refl</A> T0 a0) a1 (<A href="cic:/matita/basics/logic/eq.con(0,1,2)">refl</A> (T1 a0 (<A href="cic:/matita/basics/logic/eq.con(0,1,2)">refl</A> T0 a0)) a1)) a2))
 209                    a3).
 210   ∀b0:T0.
 211   ∀e0:<A href="cic:/matita/basics/logic/eq.ind(1,0,2)">eq</A> (T0 …) a0 b0.
 212   ∀b1: T1 b0 e0.
 213   ∀e1:<A href="cic:/matita/basics/logic/eq.ind(1,0,2)">eq</A> (T1 …) (<A href="cic:/matita/basics/logic/R1.def(2)">R1</A> T0 a0 T1 a1 b0 e0) b1.
 214   ∀b2: T2 b0 e0 b1 e1.
 215   ∀e2:<A href="cic:/matita/basics/logic/eq.ind(1,0,2)">eq</A> (T2 …) (<A href="cic:/matita/basics/logic/R2.def(3)">R2</A> T0 a0 T1 a1 T2 a2 b0 e0 b1 e1) b2.
 216   ∀b3: T3 b0 e0 b1 e1 b2 e2.
 217   ∀e3:<A href="cic:/matita/basics/logic/eq.ind(1,0,2)">eq</A> (T3 …) (<A href="cic:/matita/basics/logic/R3.def(4)">R3</A> 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 @(<A href="cic:/matita/basics/logic/eq_rect_Type0.fix(0,5,1)">eq_rect_Type0</A> ????? e3)
 221 @(<A href="cic:/matita/basics/logic/R3.def(4)">R3</A> ????????? 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 <A title="leibnitz's equality" href="cic:/fakeuri.def(1)">=</A> t → Type[2].P (<A href="cic:/matita/basics/logic/eq.con(0,1,2)">refl</A> ? t) → ∀p.P p.