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

feat(frontends/lean): improve calc mode

Browse source 
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
This commit is contained in:
Leonardo de Moura 2015-04-04 08:58:35 -07:00
parent f1b7021ed0
commit 4ec0e1b07c
15 changed files with 92 additions and 122 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

11
hott/init/logic.hlean
View file

@ -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

44
library/algebra/order.lean
View file

@ -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

6
library/data/int/basic.lean
View file

@ -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 -/

4
library/data/int/div.lean
View file

@ -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]

18
library/data/int/order.lean
View file

@ -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 _ _

5
library/data/nat/order.lean
View file

@ -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

8
library/data/perm.lean
View file

@ -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)

29
library/init/logic.lean
View file

@ -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

16
library/init/nat.lean
View file

@ -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

25
src/frontends/lean/calc.cpp
View file

@ -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<calc_step> const & steps, buffer<expr> & 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<calc_step> const & steps1, std::vector<calc_step> const & steps2,
std::vector<calc_step> & res_steps, pos_info const & pos) {
res_steps.clear();
@ -311,11 +316,21 @@ static void join(parser & p, std::vector<calc_step> 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);
}
}
}
}

8
src/library/constants.cpp
View file

@ -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; }

2
src/library/constants.h
View file

@ -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();

2
src/library/constants.txt
View file

@ -103,6 +103,8 @@ tactic.trace
tactic.try_for
tactic.unfold
tactic.whnf
trans_rel_left
trans_rel_right
true
true.intro
is_trunc

18
tests/lean/hott/calc_auto_trans_eq.hlean Normal file
View file

@ -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₃

18
tests/lean/run/calc_auto_trans_eq.lean Normal file
View file

@ -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₃