diff --git a/src/builtin/CMakeLists.txt b/src/builtin/CMakeLists.txt index ff700ebe18..2670aca666 100644 --- a/src/builtin/CMakeLists.txt +++ b/src/builtin/CMakeLists.txt @@ -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") diff --git a/src/builtin/congr.lean b/src/builtin/congr.lean deleted file mode 100644 index 5987cfc82d..0000000000 --- a/src/builtin/congr.lean +++ /dev/null @@ -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) }) diff --git a/src/builtin/if_then_else.lean b/src/builtin/if_then_else.lean index 4f023c92bd..ad5f768531 100644 --- a/src/builtin/if_then_else.lean +++ b/src/builtin/if_then_else.lean @@ -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 \ No newline at end of file diff --git a/src/builtin/kernel.lean b/src/builtin/kernel.lean index 3c3a6120be..94241390e7 100644 --- a/src/builtin/kernel.lean +++ b/src/builtin/kernel.lean @@ -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 diff --git a/src/builtin/obj/congr.olean b/src/builtin/obj/congr.olean deleted file mode 100644 index 14efc8c492..0000000000 Binary files a/src/builtin/obj/congr.olean and /dev/null differ diff --git a/src/builtin/obj/if_then_else.olean b/src/builtin/obj/if_then_else.olean index dde4ccabbd..438a5a495b 100644 Binary files a/src/builtin/obj/if_then_else.olean and b/src/builtin/obj/if_then_else.olean differ diff --git a/src/builtin/obj/kernel.olean b/src/builtin/obj/kernel.olean index f6bc2514c5..6f07d32bcb 100644 Binary files a/src/builtin/obj/kernel.olean and b/src/builtin/obj/kernel.olean differ diff --git a/src/kernel/kernel_decls.cpp b/src/kernel/kernel_decls.cpp index f4101dfb03..70b5aa39d1 100644 --- a/src/kernel/kernel_decls.cpp +++ b/src/kernel/kernel_decls.cpp @@ -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")); } diff --git a/src/kernel/kernel_decls.h b/src/kernel/kernel_decls.h index 8e9768323f..69a031edb2 100644 --- a/src/kernel/kernel_decls.h +++ b/src/kernel/kernel_decls.h @@ -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}); } }