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

refactor(builtin): move congruence theorems to kernel/if_then_else modules

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-01-11 13:48:28 -08:00
parent a0a92f11b7
commit a1a467a65f
9 changed files with 137 additions and 109 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/builtin/CMakeLists.txt
View file

@ -94,7 +94,6 @@ add_theory("Int.lean" "${CMAKE_CURRENT_BINARY_DIR}/if_then_else.olean")
add_theory("Real.lean" "${CMAKE_CURRENT_BINARY_DIR}/Int.olean")
add_theory("specialfn.lean" "${CMAKE_CURRENT_BINARY_DIR}/Real.olean")
add_theory("cast.lean" "${CMAKE_CURRENT_BINARY_DIR}/Nat.olean")
add_theory("congr.lean" "${CMAKE_CURRENT_BINARY_DIR}/Nat.olean")
update_interface("kernel.olean" "kernel" "-n")
update_interface("Nat.olean" "library/arith" "-n")

108
src/builtin/congr.lean
View file

@ -1,108 +0,0 @@
-- Congruence theorems for contextual simplification
-- Simplify a → b, by first simplifying a to c using the fact that ¬ b is true, and then
-- b to d using the fact that c is true
theorem imp_congrr {a b c d : Bool} (H_ac : ∀ (H_nb : ¬ b), a = c) (H_bd : ∀ (H_c : c), b = d) : (a → b) = (c → d)
:= or_elim (em b)
(λ H_b : b,
or_elim (em c)
(λ H_c : c,
calc (a → b) = (a → true) : { eqt_intro H_b }
... = true : imp_truer a
... = (c → true) : symm (imp_truer c)
... = (c → b) : { symm (eqt_intro H_b) }
... = (c → d) : { H_bd H_c })
(λ H_nc : ¬ c,
calc (a → b) = (a → true) : { eqt_intro H_b }
... = true : imp_truer a
... = (false → d) : symm (imp_falsel d)
... = (c → d) : { symm (eqf_intro H_nc) }))
(λ H_nb : ¬ b,
or_elim (em c)
(λ H_c : c,
calc (a → b) = (c → b) : { H_ac H_nb }
... = (c → d) : { H_bd H_c })
(λ H_nc : ¬ c,
calc (a → b) = (c → b) : { H_ac H_nb }
... = (false → b) : { eqf_intro H_nc }
... = true : imp_falsel b
... = (false → d) : symm (imp_falsel d)
... = (c → d) : { symm (eqf_intro H_nc) }))
-- Simplify a → b, by first simplifying b to d using the fact that a is true, and then
-- b to d using the fact that ¬ d is true.
-- This kind of congruence seems to be useful in very rare cases.
theorem imp_congrl {a b c d : Bool} (H_ac : ∀ (H_nd : ¬ d), a = c) (H_bd : ∀ (H_a : a), b = d) : (a → b) = (c → d)
:= or_elim (em a)
(λ H_a : a,
or_elim (em d)
(λ H_d : d,
calc (a → b) = (a → d) : { H_bd H_a }
... = (a → true) : { eqt_intro H_d }
... = true : imp_truer a
... = (c → true) : symm (imp_truer c)
... = (c → d) : { symm (eqt_intro H_d) })
(λ H_nd : ¬ d,
calc (a → b) = (c → b) : { H_ac H_nd }
... = (c → d) : { H_bd H_a }))
(λ H_na : ¬ a,
or_elim (em d)
(λ H_d : d,
calc (a → b) = (false → b) : { eqf_intro H_na }
... = true : imp_falsel b
... = (c → true) : symm (imp_truer c)
... = (c → d) : { symm (eqt_intro H_d) })
(λ H_nd : ¬ d,
calc (a → b) = (false → b) : { eqf_intro H_na }
... = true : imp_falsel b
... = (false → d) : symm (imp_falsel d)
... = (a → d) : { symm (eqf_intro H_na) }
... = (c → d) : { H_ac H_nd }))
-- (Common case) simplify a to c, and then b to d using the fact that c is true
theorem imp_congr {a b c d : Bool} (H_ac : a = c) (H_bd : ∀ (H_c : c), b = d) : (a → b) = (c → d)
:= imp_congrr (λ H, H_ac) H_bd
-- In the following theorems we are using the fact that a ∨ b is defined as ¬ a → b
set_opaque or false
theorem or_congrr {a b c d : Bool} (H_ac : ∀ (H_nb : ¬ b), a = c) (H_bd : ∀ (H_nc : ¬ c), b = d) : (a ∨ b) = (c ∨ d)
:= imp_congrr (λ H_nb : ¬ b, congr2 not (H_ac H_nb)) H_bd
theorem or_congrl {a b c d : Bool} (H_ac : ∀ (H_nd : ¬ d), a = c) (H_bd : ∀ (H_na : ¬ a), b = d) : (a ∨ b) = (c ∨ d)
:= imp_congrl (λ H_nd : ¬ d, congr2 not (H_ac H_nd)) H_bd
set_opaque or true
-- (Common case) simplify a to c, and then b to d using the fact that ¬ c is true
theorem or_congr {a b c d : Bool} (H_ac : a = c) (H_bd : ∀ (H_nc : ¬ c), b = d) : (a ∨ b) = (c ∨ d)
:= or_congrr (λ H, H_ac) H_bd
-- In the following theorems we are using the fact hat a ∧ b is defined as ¬ (a → ¬ b)
set_opaque and false
theorem and_congrr {a b c d : Bool} (H_ac : ∀ (H_b : b), a = c) (H_bd : ∀ (H_c : c), b = d) : (a ∧ b) = (c ∧ d)
:= congr2 not (imp_congrr (λ (H_nnb : ¬ ¬ b), H_ac (not_not_elim H_nnb)) (λ H_c : c, congr2 not (H_bd H_c)))
theorem and_congrl {a b c d : Bool} (H_ac : ∀ (H_d : d), a = c) (H_bd : ∀ (H_a : a), b = d) : (a ∧ b) = (c ∧ d)
:= congr2 not (imp_congrl (λ (H_nnd : ¬ ¬ d), H_ac (not_not_elim H_nnd)) (λ H_a : a, congr2 not (H_bd H_a)))
set_opaque and true
-- (Common case) simplify a to c, and then b to d using the fact that c is true
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
-- Perhaps, we should move the following theorem to the if_then_else module
import if_then_else
-- Simplify the then branch using the fact that c is true, and the else branch that c is false
theorem if_congr {A : TypeU} {b c : Bool} {x y u v : A} (H_bc : b = c) (H_xu : ∀ (H_c : c), x = u) (H_yv : ∀ (H_nc : ¬ c), y = v) :
(if b then x else y) = (if c then u else v)
:= or_elim (em c)
(λ H_c : c, calc (if b then x else y) = (if c then x else y) : { H_bc }
... = (if true then x else y) : { eqt_intro H_c }
... = x : if_true _ _
... = u : H_xu H_c
... = (if true then u else v) : symm (if_true _ _)
... = (if c then u else v) : { symm (eqt_intro H_c) })
(λ H_nc : ¬ c, calc (if b then x else y) = (if c then x else y) : { H_bc }
... = (if false then x else y) : { eqf_intro H_nc }
... = y : if_false _ _
... = v : H_yv H_nc
... = (if false then u else v) : symm (if_false _ _)
... = (if c then u else v) : { symm (eqf_intro H_nc) })

17
src/builtin/if_then_else.lean
View file

@ -8,4 +8,21 @@ axiom if_false {A : TypeU} (a b : A) : if false then a else b = b
theorem if_a_a {A : TypeU} (c : Bool) (a : A) : if c then a else a = a
:= case (λ x, if x then a else a = a) (if_true a a) (if_false a a) c
-- Simplify the then branch using the fact that c is true, and the else branch that c is false
theorem if_congr {A : TypeU} {b c : Bool} {x y u v : A} (H_bc : b = c) (H_xu : ∀ (H_c : c), x = u) (H_yv : ∀ (H_nc : ¬ c), y = v) :
(if b then x else y) = (if c then u else v)
:= or_elim (em c)
(λ H_c : c, calc (if b then x else y) = (if c then x else y) : { H_bc }
... = (if true then x else y) : { eqt_intro H_c }
... = x : if_true _ _
... = u : H_xu H_c
... = (if true then u else v) : symm (if_true _ _)
... = (if c then u else v) : { symm (eqt_intro H_c) })
(λ H_nc : ¬ c, calc (if b then x else y) = (if c then x else y) : { H_bc }
... = (if false then x else y) : { eqf_intro H_nc }
... = y : if_false _ _
... = v : H_yv H_nc
... = (if false then u else v) : symm (if_false _ _)
... = (if c then u else v) : { symm (eqf_intro H_nc) })
set_opaque ite true

84
src/builtin/kernel.lean
View file

@ -365,6 +365,90 @@ theorem exists_unfold {A : TypeU} (P : A → Bool) (a : A) : (∃ x : A, P x) =
:= boolext (λ H : (∃ x : A, P x), exists_unfold1 a H)
(λ H : (P a ∨ (∃ x : A, x ≠ a ∧ P x)), exists_unfold2 a H)
-- Congruence theorems for contextual simplification
-- Simplify a → b, by first simplifying a to c using the fact that ¬ b is true, and then
-- b to d using the fact that c is true
theorem imp_congrr {a b c d : Bool} (H_ac : ∀ (H_nb : ¬ b), a = c) (H_bd : ∀ (H_c : c), b = d) : (a → b) = (c → d)
:= or_elim (em b)
(λ H_b : b,
or_elim (em c)
(λ H_c : c,
calc (a → b) = (a → true) : { eqt_intro H_b }
... = true : imp_truer a
... = (c → true) : symm (imp_truer c)
... = (c → b) : { symm (eqt_intro H_b) }
... = (c → d) : { H_bd H_c })
(λ H_nc : ¬ c,
calc (a → b) = (a → true) : { eqt_intro H_b }
... = true : imp_truer a
... = (false → d) : symm (imp_falsel d)
... = (c → d) : { symm (eqf_intro H_nc) }))
(λ H_nb : ¬ b,
or_elim (em c)
(λ H_c : c,
calc (a → b) = (c → b) : { H_ac H_nb }
... = (c → d) : { H_bd H_c })
(λ H_nc : ¬ c,
calc (a → b) = (c → b) : { H_ac H_nb }
... = (false → b) : { eqf_intro H_nc }
... = true : imp_falsel b
... = (false → d) : symm (imp_falsel d)
... = (c → d) : { symm (eqf_intro H_nc) }))
-- Simplify a → b, by first simplifying b to d using the fact that a is true, and then
-- b to d using the fact that ¬ d is true.
-- This kind of congruence seems to be useful in very rare cases.
theorem imp_congrl {a b c d : Bool} (H_ac : ∀ (H_nd : ¬ d), a = c) (H_bd : ∀ (H_a : a), b = d) : (a → b) = (c → d)
:= or_elim (em a)
(λ H_a : a,
or_elim (em d)
(λ H_d : d,
calc (a → b) = (a → d) : { H_bd H_a }
... = (a → true) : { eqt_intro H_d }
... = true : imp_truer a
... = (c → true) : symm (imp_truer c)
... = (c → d) : { symm (eqt_intro H_d) })
(λ H_nd : ¬ d,
calc (a → b) = (c → b) : { H_ac H_nd }
... = (c → d) : { H_bd H_a }))
(λ H_na : ¬ a,
or_elim (em d)
(λ H_d : d,
calc (a → b) = (false → b) : { eqf_intro H_na }
... = true : imp_falsel b
... = (c → true) : symm (imp_truer c)
... = (c → d) : { symm (eqt_intro H_d) })
(λ H_nd : ¬ d,
calc (a → b) = (false → b) : { eqf_intro H_na }
... = true : imp_falsel b
... = (false → d) : symm (imp_falsel d)
... = (a → d) : { symm (eqf_intro H_na) }
... = (c → d) : { H_ac H_nd }))
-- (Common case) simplify a to c, and then b to d using the fact that c is true
theorem imp_congr {a b c d : Bool} (H_ac : a = c) (H_bd : ∀ (H_c : c), b = d) : (a → b) = (c → d)
:= imp_congrr (λ H, H_ac) H_bd
-- In the following theorems we are using the fact that a ∨ b is defined as ¬ a → b
theorem or_congrr {a b c d : Bool} (H_ac : ∀ (H_nb : ¬ b), a = c) (H_bd : ∀ (H_nc : ¬ c), b = d) : (a ∨ b) = (c ∨ d)
:= imp_congrr (λ H_nb : ¬ b, congr2 not (H_ac H_nb)) H_bd
theorem or_congrl {a b c d : Bool} (H_ac : ∀ (H_nd : ¬ d), a = c) (H_bd : ∀ (H_na : ¬ a), b = d) : (a ∨ b) = (c ∨ d)
:= imp_congrl (λ H_nd : ¬ d, congr2 not (H_ac H_nd)) H_bd
-- (Common case) simplify a to c, and then b to d using the fact that ¬ c is true
theorem or_congr {a b c d : Bool} (H_ac : a = c) (H_bd : ∀ (H_nc : ¬ c), b = d) : (a ∨ b) = (c ∨ d)
:= or_congrr (λ H, H_ac) H_bd
-- In the following theorems we are using the fact hat a ∧ b is defined as ¬ (a → ¬ b)
theorem and_congrr {a b c d : Bool} (H_ac : ∀ (H_b : b), a = c) (H_bd : ∀ (H_c : c), b = d) : (a ∧ b) = (c ∧ d)
:= congr2 not (imp_congrr (λ (H_nnb : ¬ ¬ b), H_ac (not_not_elim H_nnb)) (λ H_c : c, congr2 not (H_bd H_c)))
theorem and_congrl {a b c d : Bool} (H_ac : ∀ (H_d : d), a = c) (H_bd : ∀ (H_a : a), b = d) : (a ∧ b) = (c ∧ d)
:= congr2 not (imp_congrl (λ (H_nnd : ¬ ¬ d), H_ac (not_not_elim H_nnd)) (λ H_a : a, congr2 not (H_bd H_a)))
-- (Common case) simplify a to c, and then b to d using the fact that c is true
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
set_opaque exists true
set_opaque not true
set_opaque or true

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

Binary file not shown.

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

Binary file not shown.

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

Binary file not shown.

9
src/kernel/kernel_decls.cpp
View file

@ -100,4 +100,13 @@ MK_CONSTANT(not_exists_elim_fn, name("not_exists_elim"));
MK_CONSTANT(exists_unfold1_fn, name("exists_unfold1"));
MK_CONSTANT(exists_unfold2_fn, name("exists_unfold2"));
MK_CONSTANT(exists_unfold_fn, name("exists_unfold"));
MK_CONSTANT(imp_congrr_fn, name("imp_congrr"));
MK_CONSTANT(imp_congrl_fn, name("imp_congrl"));
MK_CONSTANT(imp_congr_fn, name("imp_congr"));
MK_CONSTANT(or_congrr_fn, name("or_congrr"));
MK_CONSTANT(or_congrl_fn, name("or_congrl"));
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"));
}

27
src/kernel/kernel_decls.h
View file

@ -291,4 +291,31 @@ inline expr mk_exists_unfold2_th(expr const & e1, expr const & e2, expr const &
expr mk_exists_unfold_fn();
bool is_exists_unfold_fn(expr const & e);
inline expr mk_exists_unfold_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_exists_unfold_fn(), e1, e2, e3}); }
expr mk_imp_congrr_fn();
bool is_imp_congrr_fn(expr const & e);
inline expr mk_imp_congrr_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) { return mk_app({mk_imp_congrr_fn(), e1, e2, e3, e4, e5, e6}); }
expr mk_imp_congrl_fn();
bool is_imp_congrl_fn(expr const & e);
inline expr mk_imp_congrl_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) { return mk_app({mk_imp_congrl_fn(), e1, e2, e3, e4, e5, e6}); }
expr mk_imp_congr_fn();
bool is_imp_congr_fn(expr const & e);
inline expr mk_imp_congr_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) { return mk_app({mk_imp_congr_fn(), e1, e2, e3, e4, e5, e6}); }
expr mk_or_congrr_fn();
bool is_or_congrr_fn(expr const & e);
inline expr mk_or_congrr_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) { return mk_app({mk_or_congrr_fn(), e1, e2, e3, e4, e5, e6}); }
expr mk_or_congrl_fn();
bool is_or_congrl_fn(expr const & e);
inline expr mk_or_congrl_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) { return mk_app({mk_or_congrl_fn(), e1, e2, e3, e4, e5, e6}); }
expr mk_or_congr_fn();
bool is_or_congr_fn(expr const & e);
inline expr mk_or_congr_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) { return mk_app({mk_or_congr_fn(), e1, e2, e3, e4, e5, e6}); }
expr mk_and_congrr_fn();
bool is_and_congrr_fn(expr const & e);
inline expr mk_and_congrr_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) { return mk_app({mk_and_congrr_fn(), e1, e2, e3, e4, e5, e6}); }
expr mk_and_congrl_fn();
bool is_and_congrl_fn(expr const & e);
inline expr mk_and_congrl_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) { return mk_app({mk_and_congrl_fn(), e1, e2, e3, e4, e5, e6}); }
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}); }
}