michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

refactor(library/logic/core/eq): cleanup

Browse source
This commit is contained in:
Leonardo de Moura 2014-09-09 19:15:11 -07:00
parent b4d765ff2e
commit 9ac5f28b03
1 changed files with 34 additions and 34 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

68
library/logic/core/eq.lean
View file

@ -19,20 +19,20 @@ infix `=` := eq
abbreviation rfl {A : Type} {a : A} := eq.refl a
namespace eq
theorem id_refl {A : Type} {a : A} (H1 : a = a) : H1 = (eq.refl a) :=
rfl
theorem id_refl {A : Type} {a : A} (H1 : a = a) : H1 = (eq.refl a) :=
rfl
theorem irrel {A : Type} {a b : A} (H1 H2 : a = b) : H1 = H2 :=
rfl
theorem irrel {A : Type} {a b : A} (H1 H2 : a = b) : H1 = H2 :=
rfl
theorem subst {A : Type} {a b : A} {P : A → Prop} (H1 : a = b) (H2 : P a) : P b :=
rec H2 H1
theorem subst {A : Type} {a b : A} {P : A → Prop} (H1 : a = b) (H2 : P a) : P b :=
rec H2 H1
theorem trans {A : Type} {a b c : A} (H1 : a = b) (H2 : b = c) : a = c :=
subst H2 H1
theorem trans {A : Type} {a b c : A} (H1 : a = b) (H2 : b = c) : a = c :=
subst H2 H1
theorem symm {A : Type} {a b : A} (H : a = b) : b = a :=
subst H (refl a)
theorem symm {A : Type} {a b : A} (H : a = b) : b = a :=
subst H (refl a)
end eq
calc_subst eq.subst
@ -47,33 +47,33 @@ end eq_ops
open eq_ops
namespace eq
-- eq_rec with arguments swapped, for transporting an element of a dependent type
definition rec_on {A : Type} {a1 a2 : A} {B : A → Type} (H1 : a1 = a2) (H2 : B a1) : B a2 :=
eq.rec H2 H1
-- eq_rec with arguments swapped, for transporting an element of a dependent type
definition rec_on {A : Type} {a1 a2 : A} {B : A → Type} (H1 : a1 = a2) (H2 : B a1) : B a2 :=
eq.rec H2 H1
theorem rec_on_id {A : Type} {a : A} {B : A → Type} (H : a = a) (b : B a) : rec_on H b = b :=
refl (rec_on rfl b)
theorem rec_on_id {A : Type} {a : A} {B : A → Type} (H : a = a) (b : B a) : rec_on H b = b :=
refl (rec_on rfl b)
theorem rec_id {A : Type} {a : A} {B : A → Type} (H : a = a) (b : B a) : rec b H = b :=
rec_on_id H b
theorem rec_id {A : Type} {a : A} {B : A → Type} (H : a = a) (b : B a) : rec b H = b :=
rec_on_id H b
theorem rec_on_compose {A : Type} {a b c : A} {P : A → Type} (H1 : a = b) (H2 : b = c)
(u : P a) :
rec_on H2 (rec_on H1 u) = rec_on (trans H1 H2) u :=
(show ∀(H2 : b = c), rec_on H2 (rec_on H1 u) = rec_on (trans H1 H2) u,
from rec_on H2 (take (H2 : b = b), rec_on_id H2 _))
H2
theorem rec_on_compose {A : Type} {a b c : A} {P : A → Type} (H1 : a = b) (H2 : b = c)
(u : P a) :
rec_on H2 (rec_on H1 u) = rec_on (trans H1 H2) u :=
(show ∀(H2 : b = c), rec_on H2 (rec_on H1 u) = rec_on (trans H1 H2) u,
from rec_on H2 (take (H2 : b = b), rec_on_id H2 _))
H2
end eq
theorem congr_fun {A : Type} {B : A → Type} {f g : Π x, B x} (H : f = g) (a : A) : f a = g a :=
H ▸ eq.refl (f a)
H ▸ rfl
theorem congr_arg {A : Type} {B : Type} {a b : A} (f : A → B) (H : a = b) : f a = f b :=
H ▸ eq.refl (f a)
H ▸ rfl
theorem congr {A : Type} {B : Type} {f g : A → B} {a b : A} (H1 : f = g) (H2 : a = b) :
f a = g b :=
H1 ▸ H2 ▸ eq.refl (f a)
H1 ▸ H2 ▸ rfl
theorem equal_f {A : Type} {B : A → Type} {f g : Π x, B x} (H : f = g) : ∀x, f x = g x :=
take x, congr_fun H x
@ -106,17 +106,17 @@ definition ne [inline] {A : Type} (a b : A) := ¬(a = b)
infix `≠` := ne
namespace ne
theorem intro {A : Type} {a b : A} (H : a = b → false) : a ≠ b :=
H
theorem intro {A : Type} {a b : A} (H : a = b → false) : a ≠ b :=
H
theorem elim {A : Type} {a b : A} (H1 : a ≠ b) (H2 : a = b) : false :=
H1 H2
theorem elim {A : Type} {a b : A} (H1 : a ≠ b) (H2 : a = b) : false :=
H1 H2
theorem irrefl {A : Type} {a : A} (H : a ≠ a) : false :=
H rfl
theorem irrefl {A : Type} {a : A} (H : a ≠ a) : false :=
H rfl
theorem symm {A : Type} {a b : A} (H : a ≠ b) : b ≠ a :=
assume H1 : b = a, H (H1⁻¹)
theorem symm {A : Type} {a b : A} (H : a ≠ b) : b ≠ a :=
assume H1 : b = a, H (H1⁻¹)
end ne
theorem a_neq_a_elim {A : Type} {a : A} (H : a ≠ a) : false :=