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

feat(builtin/kernel): add new useful theorems for the simplifier

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-01-13 18:21:22 -08:00
parent 4595c50f7e
commit f8eaae7218
5 changed files with 79 additions and 57 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

57
examples/lean/principia.lean
View file

@ -1,57 +0,0 @@
import macros
-- Some theorems from Pricipia Mathematica
theorem p1 {A : TypeU} (p : Bool) (φ : A → Bool) : (∀ x, p ∨ φ x) = (p ∨ ∀ x, φ x)
:= boolext
(assume H : (∀ x, p ∨ φ x),
or_elim (em p)
(λ Hp : p, or_introl Hp (∀ x, φ x))
(λ Hnp : ¬ p, or_intror p (take x,
resolve1 (H x) Hnp)))
(assume H : (p ∨ ∀ x, φ x),
take x,
or_elim H
(λ H1 : p, or_introl H1 (φ x))
(λ H2 : (∀ x, φ x), or_intror p (H2 x)))
theorem p2 {A : TypeU} (p : Bool) (φ : A → Bool) : (∀ x, φ x ∨ p) = ((∀ x, φ x) ∨ p)
:= calc (∀ x, φ x ∨ p) = (∀ x, p ∨ φ x) : allext (λ x, or_comm (φ x) p)
... = (p ∨ ∀ x, φ x) : p1 p φ
... = ((∀ x, φ x) ∨ p) : or_comm p (∀ x, φ x)
theorem p3 {A : TypeU} (φ ψ : A → Bool) : (∀ x, φ x ∧ ψ x) = ((∀ x, φ x) ∧ (∀ x, ψ x))
:= boolext
(assume H : (∀ x, φ x ∧ ψ x),
and_intro (take x, and_eliml (H x)) (take x, and_elimr (H x)))
(assume H : (∀ x, φ x) ∧ (∀ x, ψ x),
take x, and_intro (and_eliml H x) (and_elimr H x))
theorem p4 {A : TypeU} (p : Bool) (φ : A → Bool) : (∃ x, p ∧ φ x) = (p ∧ ∃ x, φ x)
:= boolext
(assume H : (∃ x, p ∧ φ x),
obtain (w : A) (Hw : p ∧ φ w), from H,
and_intro (and_eliml Hw) (exists_intro w (and_elimr Hw)))
(assume H : (p ∧ ∃ x, φ x),
obtain (w : A) (Hw : φ w), from (and_elimr H),
exists_intro w (and_intro (and_eliml H) Hw))
theorem p5 {A : TypeU} (p : Bool) (φ : A → Bool) : (∃ x, φ x ∧ p) = ((∃ x, φ x) ∧ p)
:= calc (∃ x, φ x ∧ p) = (∃ x, p ∧ φ x) : eq_exists_intro (λ x, and_comm (φ x) p)
... = (p ∧ (∃ x, φ x)) : p4 p φ
... = ((∃ x, φ x) ∧ p) : and_comm p (∃ x, φ x)
theorem p6 {A : TypeU} (φ ψ : A → Bool) : (∃ x, φ x ∨ ψ x) = ((∃ x, φ x) ∨ (∃ x, ψ x))
:= boolext
(assume H : (∃ x, φ x ∨ ψ x),
obtain (w : A) (Hw : φ w ∨ ψ w), from H,
or_elim Hw
(λ Hw1 : φ w, or_introl (exists_intro w Hw1) (∃ x, ψ x))
(λ Hw2 : ψ w, or_intror (∃ x, φ x) (exists_intro w Hw2)))
(assume H : (∃ x, φ x) ∨ (∃ x, ψ x),
or_elim H
(λ H1 : (∃ x, φ x),
obtain (w : A) (Hw : φ w), from H1,
exists_intro w (or_introl Hw (ψ w)))
(λ H2 : (∃ x, ψ x),
obtain (w : A) (Hw : ψ w), from H2,
exists_intro w (or_intror (φ w) Hw)))

55
src/builtin/kernel.lean
View file

@ -463,6 +463,61 @@ theorem and_congrl {a b c d : Bool} (H_ac : ∀ (H_d : d), a = c) (H_bd : ∀ (H
theorem and_congr {a b c d : Bool} (H_ac : a = c) (H_bd : ∀ (H_c : c), b = d) : (a ∧ b) = (c ∧ d)
:= and_congrr (λ H, H_ac) H_bd
theorem forall_or_distributer {A : TypeU} (p : Bool) (φ : A → Bool) : (∀ x, p ∨ φ x) = (p ∨ ∀ x, φ x)
:= boolext
(assume H : (∀ x, p ∨ φ x),
or_elim (em p)
(λ Hp : p, or_introl Hp (∀ x, φ x))
(λ Hnp : ¬ p, or_intror p (take x,
resolve1 (H x) Hnp)))
(assume H : (p ∨ ∀ x, φ x),
take x,
or_elim H
(λ H1 : p, or_introl H1 (φ x))
(λ H2 : (∀ x, φ x), or_intror p (H2 x)))
theorem forall_or_distributel {A : TypeU} (p : Bool) (φ : A → Bool) : (∀ x, φ x ∨ p) = ((∀ x, φ x) ∨ p)
:= calc (∀ x, φ x ∨ p) = (∀ x, p ∨ φ x) : allext (λ x, or_comm (φ x) p)
... = (p ∨ ∀ x, φ x) : forall_or_distributer p φ
... = ((∀ x, φ x) ∨ p) : or_comm p (∀ x, φ x)
theorem forall_and_distribute {A : TypeU} (φ ψ : A → Bool) : (∀ x, φ x ∧ ψ x) = ((∀ x, φ x) ∧ (∀ x, ψ x))
:= boolext
(assume H : (∀ x, φ x ∧ ψ x),
and_intro (take x, and_eliml (H x)) (take x, and_elimr (H x)))
(assume H : (∀ x, φ x) ∧ (∀ x, ψ x),
take x, and_intro (and_eliml H x) (and_elimr H x))
theorem exists_and_distributer {A : TypeU} (p : Bool) (φ : A → Bool) : (∃ x, p ∧ φ x) = (p ∧ ∃ x, φ x)
:= boolext
(assume H : (∃ x, p ∧ φ x),
obtain (w : A) (Hw : p ∧ φ w), from H,
and_intro (and_eliml Hw) (exists_intro w (and_elimr Hw)))
(assume H : (p ∧ ∃ x, φ x),
obtain (w : A) (Hw : φ w), from (and_elimr H),
exists_intro w (and_intro (and_eliml H) Hw))
theorem exists_and_distributel {A : TypeU} (p : Bool) (φ : A → Bool) : (∃ x, φ x ∧ p) = ((∃ x, φ x) ∧ p)
:= calc (∃ x, φ x ∧ p) = (∃ x, p ∧ φ x) : eq_exists_intro (λ x, and_comm (φ x) p)
... = (p ∧ (∃ x, φ x)) : exists_and_distributer p φ
... = ((∃ x, φ x) ∧ p) : and_comm p (∃ x, φ x)
theorem exists_or_distribute {A : TypeU} (φ ψ : A → Bool) : (∃ x, φ x ∨ ψ x) = ((∃ x, φ x) ∨ (∃ x, ψ x))
:= boolext
(assume H : (∃ x, φ x ∨ ψ x),
obtain (w : A) (Hw : φ w ∨ ψ w), from H,
or_elim Hw
(λ Hw1 : φ w, or_introl (exists_intro w Hw1) (∃ x, ψ x))
(λ Hw2 : ψ w, or_intror (∃ x, φ x) (exists_intro w Hw2)))
(assume H : (∃ x, φ x) ∨ (∃ x, ψ x),
or_elim H
(λ H1 : (∃ x, φ x),
obtain (w : A) (Hw : φ w), from H1,
exists_intro w (or_introl Hw (ψ w)))
(λ H2 : (∃ x, ψ x),
obtain (w : A) (Hw : ψ w), from H2,
exists_intro w (or_intror (φ w) Hw)))
set_opaque exists true
set_opaque not true
set_opaque or true

BIN
src/builtin/obj/kernel.olean
View file

Binary file not shown.

6
src/kernel/kernel_decls.cpp
View file

@ -112,4 +112,10 @@ MK_CONSTANT(or_congr_fn, name("or_congr"));
MK_CONSTANT(and_congrr_fn, name("and_congrr"));
MK_CONSTANT(and_congrl_fn, name("and_congrl"));
MK_CONSTANT(and_congr_fn, name("and_congr"));
MK_CONSTANT(forall_or_distributer_fn, name("forall_or_distributer"));
MK_CONSTANT(forall_or_distributel_fn, name("forall_or_distributel"));
MK_CONSTANT(forall_and_distribute_fn, name("forall_and_distribute"));
MK_CONSTANT(exists_and_distributer_fn, name("exists_and_distributer"));
MK_CONSTANT(exists_and_distributel_fn, name("exists_and_distributel"));
MK_CONSTANT(exists_or_distribute_fn, name("exists_or_distribute"));
}

18
src/kernel/kernel_decls.h
View file

@ -327,4 +327,22 @@ inline expr mk_and_congrl_th(expr const & e1, expr const & e2, expr const & e3,
expr mk_and_congr_fn();
bool is_and_congr_fn(expr const & e);
inline expr mk_and_congr_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) { return mk_app({mk_and_congr_fn(), e1, e2, e3, e4, e5, e6}); }
expr mk_forall_or_distributer_fn();
bool is_forall_or_distributer_fn(expr const & e);
inline expr mk_forall_or_distributer_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_forall_or_distributer_fn(), e1, e2, e3}); }
expr mk_forall_or_distributel_fn();
bool is_forall_or_distributel_fn(expr const & e);
inline expr mk_forall_or_distributel_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_forall_or_distributel_fn(), e1, e2, e3}); }
expr mk_forall_and_distribute_fn();
bool is_forall_and_distribute_fn(expr const & e);
inline expr mk_forall_and_distribute_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_forall_and_distribute_fn(), e1, e2, e3}); }
expr mk_exists_and_distributer_fn();
bool is_exists_and_distributer_fn(expr const & e);
inline expr mk_exists_and_distributer_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_exists_and_distributer_fn(), e1, e2, e3}); }
expr mk_exists_and_distributel_fn();
bool is_exists_and_distributel_fn(expr const & e);
inline expr mk_exists_and_distributel_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_exists_and_distributel_fn(), e1, e2, e3}); }
expr mk_exists_or_distribute_fn();
bool is_exists_or_distribute_fn(expr const & e);
inline expr mk_exists_or_distribute_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_exists_or_distribute_fn(), e1, e2, e3}); }
}