From 4ec0e1b07c6a76bf461edee143e93073cba6625b Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 4 Apr 2015 08:58:35 -0700 Subject: [PATCH] feat(frontends/lean): improve calc mode Now, it automatically supports transitivity of the form (R a b) -> (b = c) -> R a c (a = b) -> (R b c) -> R a c closes #507 --- hott/init/logic.hlean | 11 ++++++ library/algebra/order.lean | 44 ------------------------ library/data/int/basic.lean | 6 ---- library/data/int/div.lean | 4 +-- library/data/int/order.lean | 18 ---------- library/data/nat/order.lean | 5 --- library/data/perm.lean | 8 ----- library/init/logic.lean | 29 ++++++---------- library/init/nat.lean | 16 --------- src/frontends/lean/calc.cpp | 25 +++++++++++--- src/library/constants.cpp | 8 +++++ src/library/constants.h | 2 ++ src/library/constants.txt | 2 ++ tests/lean/hott/calc_auto_trans_eq.hlean | 18 ++++++++++ tests/lean/run/calc_auto_trans_eq.lean | 18 ++++++++++ 15 files changed, 92 insertions(+), 122 deletions(-) create mode 100644 tests/lean/hott/calc_auto_trans_eq.hlean create mode 100644 tests/lean/run/calc_auto_trans_eq.lean diff --git a/hott/init/logic.hlean b/hott/init/logic.hlean index 994801ab0a..fc3a7c5aa5 100644 --- a/hott/init/logic.hlean +++ b/hott/init/logic.hlean @@ -61,6 +61,17 @@ namespace eq end ops end eq +section + variables {A : Type} {a b c: A} + open eq.ops + + definition trans_rel_left (R : A → A → Type) (H₁ : R a b) (H₂ : b = c) : R a c := + H₂ ▸ H₁ + + definition trans_rel_right (R : A → A → Type) (H₁ : a = b) (H₂ : R b c) : R a c := + H₁⁻¹ ▸ H₂ +end + calc_subst eq.subst calc_refl eq.refl calc_trans eq.trans diff --git a/library/algebra/order.lean b/library/algebra/order.lean index 95f7b9ad98..b5716241dd 100644 --- a/library/algebra/order.lean +++ b/library/algebra/order.lean @@ -41,39 +41,6 @@ notation a >= b := has_le.ge a b definition has_lt.gt [reducible] {A : Type} [s : has_lt A] (a b : A) := b < a notation a > b := has_lt.gt a b -theorem le_of_eq_of_le {A : Type} [s : has_le A] {a b c : A} (H1 : a = b) (H2 : b ≤ c) : a ≤ c := - H1⁻¹ ▸ H2 - -theorem le_of_le_of_eq {A : Type} [s : has_le A] {a b c : A} (H1 : a ≤ b) (H2 : b = c) : a ≤ c := - H2 ▸ H1 - -theorem lt_of_eq_of_lt {A : Type} [s : has_lt A] {a b c : A} (H1 : a = b) (H2 : b < c) : a < c := - H1⁻¹ ▸ H2 - -theorem lt_of_lt_of_eq {A : Type} [s : has_lt A] {a b c : A} (H1 : a < b) (H2 : b = c) : a < c := - H2 ▸ H1 - -theorem ge_of_eq_of_ge {A : Type} [s : has_le A] {a b c : A} (H1 : a = b) (H2 : b ≥ c) : a ≥ c := - H1⁻¹ ▸ H2 - -theorem ge_of_ge_of_eq {A : Type} [s : has_le A] {a b c : A} (H1 : a ≥ b) (H2 : b = c) : a ≥ c := - H2 ▸ H1 - -theorem gt_of_eq_of_gt {A : Type} [s : has_lt A] {a b c : A} (H1 : a = b) (H2 : b > c) : a > c := - H1⁻¹ ▸ H2 - -theorem gt_of_gt_of_eq {A : Type} [s : has_lt A] {a b c : A} (H1 : a > b) (H2 : b = c) : a > c := - H2 ▸ H1 - -calc_trans le_of_eq_of_le -calc_trans le_of_le_of_eq -calc_trans lt_of_eq_of_lt -calc_trans lt_of_lt_of_eq -calc_trans ge_of_eq_of_ge -calc_trans ge_of_ge_of_eq -calc_trans gt_of_eq_of_gt -calc_trans gt_of_gt_of_eq - /- weak orders -/ structure weak_order [class] (A : Type) extends has_le A := @@ -381,23 +348,12 @@ end algebra /- For reference, these are all the transitivity rules defined in this file: - -calc_trans le_of_eq_of_le -calc_trans le_of_le_of_eq -calc_trans lt_of_eq_of_lt -calc_trans lt_of_lt_of_eq - calc_trans le.trans calc_trans lt.trans calc_trans lt_of_lt_of_le calc_trans lt_of_le_of_lt -calc_trans ge_of_eq_of_ge -calc_trans ge_of_ge_of_eq -calc_trans gt_of_eq_of_gt -calc_trans gt_of_gt_of_eq - calc_trans ge.trans calc_trans gt.trans diff --git a/library/data/int/basic.lean b/library/data/int/basic.lean index 9c4db64f16..01868e2b81 100644 --- a/library/data/int/basic.lean +++ b/library/data/int/basic.lean @@ -187,15 +187,9 @@ or.elim (@le_or_gt (pr2 p) (pr1 p)) theorem equiv_of_eq {p q : ℕ × ℕ} (H : p = q) : p ≡ q := H ▸ equiv.refl -theorem equiv_of_eq_of_equiv {p q r : ℕ × ℕ} (H1 : p = q) (H2 : q ≡ r) : p ≡ r := H1⁻¹ ▸ H2 - -theorem equiv_of_equiv_of_eq {p q r : ℕ × ℕ} (H1 : p ≡ q) (H2 : q = r) : p ≡ r := H2 ▸ H1 - calc_trans equiv.trans calc_refl equiv.refl calc_symm equiv.symm -calc_trans equiv_of_eq_of_equiv -calc_trans equiv_of_equiv_of_eq /- the representation and abstraction functions -/ diff --git a/library/data/int/div.lean b/library/data/int/div.lean index 3b81cd61b0..112a6b83c9 100644 --- a/library/data/int/div.lean +++ b/library/data/int/div.lean @@ -66,7 +66,7 @@ obtain (m : ℕ) (Hm : a = m), from exists_eq_of_nat Ha, obtain (n : ℕ) (Hn : b = n), from exists_eq_of_nat Hb, calc a div b = (#nat m div n) : by rewrite [Hm, Hn, of_nat_div_of_nat] - ... ≥ 0 : trivial + ... ≥ 0 : begin change (0 ≤ #nat m div n), apply trivial end theorem div_nonpos {a b : ℤ} (Ha : a ≥ 0) (Hb : b ≤ 0) : a div b ≤ 0 := calc @@ -396,7 +396,7 @@ have H : ∀a b, b > 0 → abs (a div b) ≤ abs a, from ... = abs a : abs_of_nonneg H2) (assume H2 : a < 0, have H3 : -a - 1 ≥ 0, from le_sub_one_of_lt (neg_pos_of_neg H2), - have H4 : (-a - 1) div b + 1 ≥ 0, from add_nonneg (div_nonneg H3 (le_of_lt H1)) trivial, + have H4 : (-a - 1) div b + 1 ≥ 0, from add_nonneg (div_nonneg H3 (le_of_lt H1)) (of_nat_le_of_nat !nat.zero_le), have H5 : (-a - 1) div b ≤ -a - 1, from div_le_of_nonneg_of_nonneg H3 (le_of_lt H1), calc abs (a div b) = abs ((-a - 1) div b + 1) : by rewrite [div_of_neg_of_pos H2 H1, abs_neg] diff --git a/library/data/int/order.lean b/library/data/int/order.lean index 6d0cd604d7..d4686ba2de 100644 --- a/library/data/int/order.lean +++ b/library/data/int/order.lean @@ -258,28 +258,10 @@ section port_algebra definition decidable_gt [instance] (a b : ℤ) : decidable (a > b) := show decidable (b < a), from _ - theorem le_of_eq_of_le : ∀{a b c : ℤ}, a = b → b ≤ c → a ≤ c := @algebra.le_of_eq_of_le _ _ - theorem le_of_le_of_eq : ∀{a b c : ℤ}, a ≤ b → b = c → a ≤ c := @algebra.le_of_le_of_eq _ _ - theorem lt_of_eq_of_lt : ∀{a b c : ℤ}, a = b → b < c → a < c := @algebra.lt_of_eq_of_lt _ _ - theorem lt_of_lt_of_eq : ∀{a b c : ℤ}, a < b → b = c → a < c := @algebra.lt_of_lt_of_eq _ _ - calc_trans int.le_of_eq_of_le - calc_trans int.le_of_le_of_eq - calc_trans int.lt_of_eq_of_lt - calc_trans int.lt_of_lt_of_eq - - theorem ge_of_eq_of_ge : ∀{a b c : ℤ}, a = b → b ≥ c → a ≥ c := @algebra.ge_of_eq_of_ge _ _ - theorem ge_of_ge_of_eq : ∀{a b c : ℤ}, a ≥ b → b = c → a ≥ c := @algebra.ge_of_ge_of_eq _ _ - theorem gt_of_eq_of_gt : ∀{a b c : ℤ}, a = b → b > c → a > c := @algebra.gt_of_eq_of_gt _ _ - theorem gt_of_gt_of_eq : ∀{a b c : ℤ}, a > b → b = c → a > c := @algebra.gt_of_gt_of_eq _ _ theorem ge.trans: ∀{a b c : ℤ}, a ≥ b → b ≥ c → a ≥ c := @algebra.ge.trans _ _ theorem gt.trans: ∀{a b c : ℤ}, a ≥ b → b ≥ c → a ≥ c := @algebra.ge.trans _ _ theorem gt_of_gt_of_ge : ∀{a b c : ℤ}, a > b → b ≥ c → a > c := @algebra.gt_of_gt_of_ge _ _ theorem gt_of_ge_of_gt : ∀{a b c : ℤ}, a ≥ b → b > c → a > c := @algebra.gt_of_ge_of_gt _ _ - calc_trans int.ge_of_eq_of_ge - calc_trans int.ge_of_ge_of_eq - calc_trans int.gt_of_eq_of_gt - calc_trans int.gt_of_gt_of_eq - theorem lt.asymm : ∀{a b : ℤ}, a < b → ¬ b < a := @algebra.lt.asymm _ _ theorem lt_of_le_of_ne : ∀{a b : ℤ}, a ≤ b → a ≠ b → a < b := @algebra.lt_of_le_of_ne _ _ theorem lt_of_lt_of_le : ∀{a b c : ℤ}, a < b → b ≤ c → a < c := @algebra.lt_of_lt_of_le _ _ diff --git a/library/data/nat/order.lean b/library/data/nat/order.lean index df5ecc7508..3e115ab9c9 100644 --- a/library/data/nat/order.lean +++ b/library/data/nat/order.lean @@ -172,11 +172,6 @@ section hiding pos_of_mul_pos_left, pos_of_mul_pos_right, lt_of_mul_lt_mul_left, lt_of_mul_lt_mul_right end -calc_trans ge_of_eq_of_ge -calc_trans ge_of_ge_of_eq -calc_trans gt_of_eq_of_gt -calc_trans gt_of_gt_of_eq - section port_algebra theorem add_pos_left : ∀{a : ℕ}, 0 < a → ∀b : ℕ, 0 < a + b := take a H b, @algebra.add_pos_of_pos_of_nonneg _ _ a b H !zero_le diff --git a/library/data/perm.lean b/library/data/perm.lean index e57cc275d9..8b2d50e281 100644 --- a/library/data/perm.lean +++ b/library/data/perm.lean @@ -64,14 +64,6 @@ calc_refl perm.refl calc_symm perm.symm calc_trans perm.trans --- TODO: remove this theorems after we improve calc -theorem perm_of_eq_of_perm (l₁ l₂ l₃ : list A) : l₁ = l₂ → l₂ ~ l₃ → l₁ ~ l₃ := -assume e p, eq.rec_on (eq.symm e) p -theorem perm_of_perm_of_eq (l₁ l₂ l₃ : list A) : l₁ ~ l₂ → l₂ = l₃ → l₁ ~ l₃ := -assume p e, eq.rec_on e p -calc_trans perm_of_perm_of_eq -calc_trans perm_of_eq_of_perm - theorem mem_perm (a : A) (l₁ l₂ : list A) : l₁ ~ l₂ → a ∈ l₁ → a ∈ l₂ := assume p, perm.induction_on p (λ h, h) diff --git a/library/init/logic.lean b/library/init/logic.lean index 0f6ca0863e..ea5ac417fe 100644 --- a/library/init/logic.lean +++ b/library/init/logic.lean @@ -50,9 +50,19 @@ namespace eq notation H1 ⬝ H2 := trans H1 H2 notation H1 ▸ H2 := subst H1 H2 end ops - end eq +section + variables {A : Type} {a b c: A} + open eq.ops + + definition trans_rel_left (R : A → A → Prop) (H₁ : R a b) (H₂ : b = c) : R a c := + H₂ ▸ H₁ + + definition trans_rel_right (R : A → A → Prop) (H₁ : a = b) (H₂ : R b c) : R a c := + H₁⁻¹ ▸ H₂ +end + section variable {p : Prop} open eq.ops @@ -98,17 +108,8 @@ section theorem false.of_ne : a ≠ a → false := assume H, H rfl - - theorem ne.of_eq_of_ne : a = b → b ≠ c → a ≠ c := - assume H₁ H₂, H₁⁻¹ ▸ H₂ - - theorem ne.of_ne_of_eq : a ≠ b → b = c → a ≠ c := - assume H₁ H₂, H₂ ▸ H₁ end -calc_trans ne.of_eq_of_ne -calc_trans ne.of_ne_of_eq - infixl `==`:50 := heq namespace heq @@ -226,16 +227,8 @@ iff.mp (iff.symm H) trivial theorem not_of_iff_false (H : a ↔ false) : ¬a := assume Ha : a, iff.mp H Ha -theorem iff_of_eq_of_iff (H₁ : a = b) (H₂ : b ↔ c) : a ↔ c := -H₁⁻¹ ▸ H₂ - -theorem iff_of_iff_of_eq (H₁ : a ↔ b) (H₂ : b = c) : a ↔ c := -H₂ ▸ H₁ - calc_refl iff.refl calc_trans iff.trans -calc_trans iff_of_eq_of_iff -calc_trans iff_of_iff_of_eq inductive Exists {A : Type} (P : A → Prop) : Prop := intro : ∀ (a : A), P a → Exists P diff --git a/library/init/nat.lean b/library/init/nat.lean index a6cb271a47..1e18f1adc1 100644 --- a/library/init/nat.lean +++ b/library/init/nat.lean @@ -209,26 +209,10 @@ namespace nat apply (lt.trans hlt (lt_of_succ_lt_succ h₂)) end - definition lt_of_lt_of_eq {a b c : nat} (h₁ : a < b) (h₂ : b = c) : a < c := - eq.rec_on h₂ h₁ - - definition le_of_le_of_eq {a b c : nat} (h₁ : a ≤ b) (h₂ : b = c) : a ≤ c := - eq.rec_on h₂ h₁ - - definition lt_of_eq_of_lt {a b c : nat} (h₁ : a = b) (h₂ : b < c) : a < c := - eq.rec_on (eq.rec_on h₁ rfl) h₂ - - definition le_of_eq_of_le {a b c : nat} (h₁ : a = b) (h₂ : b ≤ c) : a ≤ c := - eq.rec_on (eq.rec_on h₁ rfl) h₂ - calc_trans lt.trans calc_trans lt_of_le_of_lt calc_trans lt_of_lt_of_le - calc_trans lt_of_lt_of_eq - calc_trans lt_of_eq_of_lt calc_trans le.trans - calc_trans le_of_le_of_eq - calc_trans le_of_eq_of_le definition max (a b : nat) : nat := if a < b then b else a diff --git a/src/frontends/lean/calc.cpp b/src/frontends/lean/calc.cpp index e3cece64f9..4f2b525260 100644 --- a/src/frontends/lean/calc.cpp +++ b/src/frontends/lean/calc.cpp @@ -15,6 +15,7 @@ Author: Leonardo de Moura #include "util/interrupt.h" #include "kernel/environment.h" #include "library/module.h" +#include "library/constants.h" #include "library/choice.h" #include "library/placeholder.h" #include "library/explicit.h" @@ -297,6 +298,10 @@ static void collect_rhss(std::vector const & steps, buffer & rh lean_assert(!rhss.empty()); } +static unsigned get_arity_of(parser & p, name const & op) { + return get_arity(p.env().get(op).get_type()); +} + static void join(parser & p, std::vector const & steps1, std::vector const & steps2, std::vector & res_steps, pos_info const & pos) { res_steps.clear(); @@ -311,11 +316,21 @@ static void join(parser & p, std::vector const & steps1, std::vector< if (!is_eqp(pred_rhs(pred1), pred_lhs(pred2))) continue; auto trans_it = state.m_trans_table.find(name_pair(pred_op(pred1), pred_op(pred2))); - if (!trans_it) - continue; - expr trans = mk_op_fn(p, std::get<0>(*trans_it), std::get<2>(*trans_it)-5, pos); - expr trans_pr = p.mk_app({trans, pred_lhs(pred1), pred_rhs(pred1), pred_rhs(pred2), pr1, pr2}, pos); - res_steps.emplace_back(calc_pred(std::get<1>(*trans_it), pred_lhs(pred1), pred_rhs(pred2)), trans_pr); + if (trans_it) { + expr trans = mk_op_fn(p, std::get<0>(*trans_it), std::get<2>(*trans_it)-5, pos); + expr trans_pr = p.mk_app({trans, pred_lhs(pred1), pred_rhs(pred1), pred_rhs(pred2), pr1, pr2}, pos); + res_steps.emplace_back(calc_pred(std::get<1>(*trans_it), pred_lhs(pred1), pred_rhs(pred2)), trans_pr); + } else if (pred_op(pred1) == get_eq_name()) { + expr trans_right = mk_op_fn(p, get_trans_rel_right_name(), 1, pos); + expr R = mk_op_fn(p, pred_op(pred2), get_arity_of(p, pred_op(pred2))-2, pos); + expr trans_pr = p.mk_app({trans_right, pred_lhs(pred1), pred_rhs(pred1), pred_rhs(pred2), R, pr1, pr2}, pos); + res_steps.emplace_back(calc_pred(pred_op(pred2), pred_lhs(pred1), pred_rhs(pred2)), trans_pr); + } else if (pred_op(pred2) == get_eq_name()) { + expr trans_left = mk_op_fn(p, get_trans_rel_left_name(), 1, pos); + expr R = mk_op_fn(p, pred_op(pred1), get_arity_of(p, pred_op(pred1))-2, pos); + expr trans_pr = p.mk_app({trans_left, pred_lhs(pred1), pred_rhs(pred1), pred_rhs(pred2), R, pr1, pr2}, pos); + res_steps.emplace_back(calc_pred(pred_op(pred1), pred_lhs(pred1), pred_rhs(pred2)), trans_pr); + } } } } diff --git a/src/library/constants.cpp b/src/library/constants.cpp index 2b123c462a..b216270d27 100644 --- a/src/library/constants.cpp +++ b/src/library/constants.cpp @@ -108,6 +108,8 @@ name const * g_tactic_trace = nullptr; name const * g_tactic_try_for = nullptr; name const * g_tactic_unfold = nullptr; name const * g_tactic_whnf = nullptr; +name const * g_trans_rel_left = nullptr; +name const * g_trans_rel_right = nullptr; name const * g_true = nullptr; name const * g_true_intro = nullptr; name const * g_is_trunc = nullptr; @@ -221,6 +223,8 @@ void initialize_constants() { g_tactic_try_for = new name{"tactic", "try_for"}; g_tactic_unfold = new name{"tactic", "unfold"}; g_tactic_whnf = new name{"tactic", "whnf"}; + g_trans_rel_left = new name{"trans_rel_left"}; + g_trans_rel_right = new name{"trans_rel_right"}; g_true = new name{"true"}; g_true_intro = new name{"true", "intro"}; g_is_trunc = new name{"is_trunc"}; @@ -335,6 +339,8 @@ void finalize_constants() { delete g_tactic_try_for; delete g_tactic_unfold; delete g_tactic_whnf; + delete g_trans_rel_left; + delete g_trans_rel_right; delete g_true; delete g_true_intro; delete g_is_trunc; @@ -448,6 +454,8 @@ name const & get_tactic_trace_name() { return *g_tactic_trace; } name const & get_tactic_try_for_name() { return *g_tactic_try_for; } name const & get_tactic_unfold_name() { return *g_tactic_unfold; } name const & get_tactic_whnf_name() { return *g_tactic_whnf; } +name const & get_trans_rel_left_name() { return *g_trans_rel_left; } +name const & get_trans_rel_right_name() { return *g_trans_rel_right; } name const & get_true_name() { return *g_true; } name const & get_true_intro_name() { return *g_true_intro; } name const & get_is_trunc_name() { return *g_is_trunc; } diff --git a/src/library/constants.h b/src/library/constants.h index 506749bfa3..8c4b50f3c7 100644 --- a/src/library/constants.h +++ b/src/library/constants.h @@ -110,6 +110,8 @@ name const & get_tactic_trace_name(); name const & get_tactic_try_for_name(); name const & get_tactic_unfold_name(); name const & get_tactic_whnf_name(); +name const & get_trans_rel_left_name(); +name const & get_trans_rel_right_name(); name const & get_true_name(); name const & get_true_intro_name(); name const & get_is_trunc_name(); diff --git a/src/library/constants.txt b/src/library/constants.txt index 3331e2fcec..67b32a2b47 100644 --- a/src/library/constants.txt +++ b/src/library/constants.txt @@ -103,6 +103,8 @@ tactic.trace tactic.try_for tactic.unfold tactic.whnf +trans_rel_left +trans_rel_right true true.intro is_trunc diff --git a/tests/lean/hott/calc_auto_trans_eq.hlean b/tests/lean/hott/calc_auto_trans_eq.hlean new file mode 100644 index 0000000000..205c439277 --- /dev/null +++ b/tests/lean/hott/calc_auto_trans_eq.hlean @@ -0,0 +1,18 @@ +constant list : Type → Type +constant R.{l} : Π {A : Type.{l}}, A → A → Type.{l} +infix `~`:50 := R + +example {A : Type} {a b c d : list nat} (H₁ : a ~ b) (H₂ : b = c) (H₃ : c = d) : a ~ d := +calc a ~ b : H₁ + ... = c : H₂ + ... = d : H₃ + +example {A : Type} {a b c d : list nat} (H₁ : a = b) (H₂ : b = c) (H₃ : c ~ d) : a ~ d := +calc a = b : H₁ + ... = c : H₂ + ... ~ d : H₃ + +example {A : Type} {a b c d : list nat} (H₁ : a = b) (H₂ : b ~ c) (H₃ : c = d) : a ~ d := +calc a = b : H₁ + ... ~ c : H₂ + ... = d : H₃ diff --git a/tests/lean/run/calc_auto_trans_eq.lean b/tests/lean/run/calc_auto_trans_eq.lean new file mode 100644 index 0000000000..e2036aeb46 --- /dev/null +++ b/tests/lean/run/calc_auto_trans_eq.lean @@ -0,0 +1,18 @@ +import data.list +constant R : Π {A : Type}, A → A → Prop +infix `~`:50 := R + +example {A : Type} {a b c d : list nat} (H₁ : a ~ b) (H₂ : b = c) (H₃ : c = d) : a ~ d := +calc a ~ b : H₁ + ... = c : H₂ + ... = d : H₃ + +example {A : Type} {a b c d : list nat} (H₁ : a = b) (H₂ : b = c) (H₃ : c ~ d) : a ~ d := +calc a = b : H₁ + ... = c : H₂ + ... ~ d : H₃ + +example {A : Type} {a b c d : list nat} (H₁ : a = b) (H₂ : b ~ c) (H₃ : c = d) : a ~ d := +calc a = b : H₁ + ... ~ c : H₂ + ... = d : H₃