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

refactor(library): replace 'calc_trans', 'calc_symm', 'calc_refl' and 'calc_subst' commands with attributes '[symm]', '[refl]', '[trans]' and '[subst]'

Browse source 
These attributes are used by the calc command.
They will also be used by tactics such as 'reflexivity', 'symmetry' and
'transitivity'.

See issue #500
This commit is contained in:
Leonardo de Moura 2015-05-02 15:15:35 -07:00
parent efc33a2f1d
commit cd17618f4a
27 changed files with 381 additions and 307 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
hott/init/equiv.hlean
View file

@ -270,10 +270,10 @@ namespace equiv
definition equiv_of_equiv_of_eq {A B C : Type} (p : A = B) (q : B ≃ C) : A ≃ C := p⁻¹ ▹ q
definition equiv_of_eq_of_equiv {A B C : Type} (p : A ≃ B) (q : B = C) : A ≃ C := q ▹ p
calc_trans equiv.trans
calc_refl equiv.refl
calc_symm equiv.symm
calc_trans equiv_of_equiv_of_eq
calc_trans equiv_of_eq_of_equiv
attribute equiv.trans [trans]
attribute equiv.refl [refl]
attribute equiv.symm [symm]
attribute equiv_of_equiv_of_eq [trans]
attribute equiv_of_eq_of_equiv [trans]
end equiv

17
hott/init/logic.hlean
View file

@ -75,10 +75,10 @@ section
H₁⁻¹ ▸ H₂
end
calc_subst eq.subst
calc_refl eq.refl
calc_trans eq.trans
calc_symm eq.symm
attribute eq.subst [subst]
attribute eq.refl [refl]
attribute eq.trans [trans]
attribute eq.symm [symm]
namespace lift
definition down_up.{l₁ l₂} {A : Type.{l₁}} (a : A) : down (up.{l₁ l₂} a) = a :=
@ -125,8 +125,8 @@ section
assume H₁ H₂, H₂ ▸ H₁
end
calc_trans ne.of_eq_of_ne
calc_trans ne.of_ne_of_eq
attribute ne.of_eq_of_ne [trans]
attribute ne.of_ne_of_eq [trans]
/- iff -/
@ -187,8 +187,9 @@ namespace iff
iff.intro (λ Ha, H ▸ Ha) (λ Hb, H⁻¹ ▸ Hb)
end iff
calc_refl iff.refl
calc_trans iff.trans
attribute iff.refl [refl]
attribute iff.trans [trans]
attribute iff.symm [symm]
/- inhabited -/

29
hott/init/nat.hlean
View file

@ -88,7 +88,7 @@ namespace nat
(lt.base zero)
(λ a (hlt : zero < succ a), lt.step hlt)
definition lt.trans {a b c : nat} (H₁ : a < b) (H₂ : b < c) : a < c :=
definition lt.trans [trans] {a b c : nat} (H₁ : a < b) (H₂ : b < c) : a < c :=
have aux : ∀ {d}, d < c → b = d → a < b → a < c, from
(λ d H, lt.rec_on H
(λ h₁ h₂, lt.step (eq.rec_on h₁ h₂))
@ -199,48 +199,27 @@ namespace nat
definition succ_le_of_lt {a b : nat} (h : a < b) : succ a ≤ b :=
lt.succ_of_lt h
definition le.trans {a b c : nat} (h₁ : a ≤ b) (h₂ : b ≤ c) : a ≤ c :=
definition le.trans [trans] {a b c : nat} (h₁ : a ≤ b) (h₂ : b ≤ c) : a ≤ c :=
begin
cases h₁ with b' hlt,
apply h₂,
apply lt.trans hlt h₂
end
definition lt.of_le_of_lt {a b c : nat} (h₁ : a ≤ b) (h₂ : b < c) : a < c :=
definition lt.of_le_of_lt [trans] {a b c : nat} (h₁ : a ≤ b) (h₂ : b < c) : a < c :=
begin
cases h₁ with b' hlt,
apply h₂,
apply lt.trans hlt h₂
end
definition lt.of_lt_of_le {a b c : nat} (h₁ : a < b) (h₂ : b ≤ c) : a < c :=
definition lt.of_lt_of_le [trans] {a b c : nat} (h₁ : a < b) (h₂ : b ≤ c) : a < c :=
begin
cases h₁ with b' hlt,
apply lt.of_succ_lt_succ h₂,
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

17
hott/init/path.hlean
View file

@ -201,18 +201,14 @@ namespace eq
notation f ∼ g := homotopy f g
namespace homotopy
protected definition refl [reducible] (f : Πx, P x) : f ∼ f :=
protected definition refl [refl] [reducible] (f : Πx, P x) : f ∼ f :=
λ x, idp
protected definition symm [reducible] {f g : Πx, P x} (H : f ∼ g) : g ∼ f :=
protected definition symm [symm] [reducible] {f g : Πx, P x} (H : f ∼ g) : g ∼ f :=
λ x, (H x)⁻¹
protected definition trans [reducible] {f g h : Πx, P x} (H1 : f ∼ g) (H2 : g ∼ h) : f ∼ h :=
protected definition trans [trans] [reducible] {f g h : Πx, P x} (H1 : f ∼ g) (H2 : g ∼ h) : f ∼ h :=
λ x, H1 x ⬝ H2 x
calc_refl refl
calc_symm symm
calc_trans trans
end homotopy
definition apd10 {f g : Πx, P x} (H : f = g) : f ∼ g :=
@ -232,10 +228,9 @@ namespace eq
/- calc enviroment -/
calc_subst transport
calc_trans concat
calc_refl refl
calc_symm inverse
attribute transport [subst]
attribute concat [trans]
attribute inverse [symm]
/- More theorems for moving things around in equations -/

3
hott/init/ua.hlean
View file

@ -53,12 +53,11 @@ left_inv equiv_of_eq p
namespace equiv
universe variable l
protected definition transport_of_equiv (P : Type → Type) {A B : Type.{l}} (H : A ≃ B)
protected definition transport_of_equiv [subst] (P : Type → Type) {A B : Type.{l}} (H : A ≃ B)
: P A → P B :=
eq.transport P (ua H)
-- We can use this for calculation evironments
calc_subst transport_of_equiv
definition rec_on_of_equiv_of_eq {A B : Type} {P : (A ≃ B) → Type}
(p : A ≃ B) (H : Π(q : A = B), P (equiv_of_eq q)) : P p :=

25
library/algebra/order.lean
View file

@ -54,11 +54,9 @@ section
theorem le.refl (a : A) : a ≤ a := !weak_order.le_refl
theorem le.trans {a b c : A} : a ≤ b → b ≤ c → a ≤ c := !weak_order.le_trans
calc_trans le.trans
theorem le.trans [trans] {a b c : A} : a ≤ b → b ≤ c → a ≤ c := !weak_order.le_trans
theorem ge.trans {a b c : A} (H1 : a ≥ b) (H2: b ≥ c) : a ≥ c := le.trans H2 H1
calc_trans ge.trans
theorem ge.trans [trans] {a b c : A} (H1 : a ≥ b) (H2: b ≥ c) : a ≥ c := le.trans H2 H1
theorem le.antisymm {a b : A} : a ≤ b → b ≤ a → a = b := !weak_order.le_antisymm
end
@ -81,11 +79,9 @@ section
theorem lt.irrefl (a : A) : ¬ a < a := !strict_order.lt_irrefl
theorem lt.trans {a b c : A} : a < b → b < c → a < c := !strict_order.lt_trans
calc_trans lt.trans
theorem lt.trans [trans] {a b c : A} : a < b → b < c → a < c := !strict_order.lt_trans
theorem gt.trans {a b c : A} (H1 : a > b) (H2: b > c) : a > c := lt.trans H2 H1
calc_trans gt.trans
theorem gt.trans [trans] {a b c : A} (H1 : a > b) (H2: b > c) : a > c := lt.trans H2 H1
theorem ne_of_lt {a b : A} (lt_ab : a < b) : a ≠ b :=
assume eq_ab : a = b,
@ -152,7 +148,7 @@ section
definition order_pair.to_strict_order [instance] [coercion] [reducible] : strict_order A :=
⦃ strict_order, s, lt_irrefl := lt_irrefl s, lt_trans := lt_trans s ⦄
theorem lt_of_lt_of_le : a < b → b ≤ c → a < c :=
theorem lt_of_lt_of_le [trans] : a < b → b ≤ c → a < c :=
assume lt_ab : a < b,
assume le_bc : b ≤ c,
have le_ac : a ≤ c, from le.trans (le_of_lt lt_ab) le_bc,
@ -163,7 +159,7 @@ section
show false, from ne_of_lt lt_ab eq_ab,
show a < c, from lt_of_le_of_ne le_ac ne_ac
theorem lt_of_le_of_lt : a ≤ b → b < c → a < c :=
theorem lt_of_le_of_lt [trans] : a ≤ b → b < c → a < c :=
assume le_ab : a ≤ b,
assume lt_bc : b < c,
have le_ac : a ≤ c, from le.trans le_ab (le_of_lt lt_bc),
@ -174,14 +170,9 @@ section
show false, from ne_of_lt lt_bc eq_bc,
show a < c, from lt_of_le_of_ne le_ac ne_ac
theorem gt_of_gt_of_ge (H1 : a > b) (H2 : b ≥ c) : a > c := lt_of_le_of_lt H2 H1
theorem gt_of_gt_of_ge [trans] (H1 : a > b) (H2 : b ≥ c) : a > c := lt_of_le_of_lt H2 H1
theorem gt_of_ge_of_gt (H1 : a ≥ b) (H2 : b > c) : a > c := lt_of_lt_of_le H2 H1
calc_trans lt_of_lt_of_le
calc_trans lt_of_le_of_lt
calc_trans gt_of_gt_of_ge
calc_trans gt_of_ge_of_gt
theorem gt_of_ge_of_gt [trans] (H1 : a ≥ b) (H2 : b > c) : a > c := lt_of_lt_of_le H2 H1
theorem not_le_of_lt (H : a < b) : ¬ b ≤ a :=
assume H1 : b ≤ a,

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

@ -154,15 +154,15 @@ protected definition equiv (p q : ℕ × ℕ) : Prop := pr1 p + pr2 q = pr2 p +
local notation p `≡` q := equiv p q
protected theorem equiv.refl {p : ℕ × ℕ} : p ≡ p := !add.comm
protected theorem equiv.refl [refl] {p : ℕ × ℕ} : p ≡ p := !add.comm
protected theorem equiv.symm {p q : ℕ × ℕ} (H : p ≡ q) : q ≡ p :=
protected theorem equiv.symm [symm] {p q : ℕ × ℕ} (H : p ≡ q) : q ≡ p :=
calc
pr1 q + pr2 p = pr2 p + pr1 q : !add.comm
... = pr1 p + pr2 q : H⁻¹
... = pr2 q + pr1 p : !add.comm
protected theorem equiv.trans {p q r : ℕ × ℕ} (H1 : p ≡ q) (H2 : q ≡ r) : p ≡ r :=
protected theorem equiv.trans [trans] {p q r : ℕ × ℕ} (H1 : p ≡ q) (H2 : q ≡ r) : p ≡ r :=
have H3 : pr1 p + pr2 r + pr2 q = pr2 p + pr1 r + pr2 q, from
calc
pr1 p + pr2 r + pr2 q = pr1 p + pr2 q + pr2 r : by simp
@ -187,10 +187,6 @@ or.elim (@le_or_gt (pr2 p) (pr1 p))
protected theorem equiv_of_eq {p q : ℕ × ℕ} (H : p = q) : p ≡ q := H ▸ equiv.refl
calc_trans equiv.trans
calc_refl equiv.refl
calc_symm equiv.symm
/- the representation and abstraction functions -/
definition abstr (a : ℕ × ℕ) : ℤ := sub_nat_nat (pr1 a) (pr2 a)

10
library/data/list/perm.lean
View file

@ -43,27 +43,25 @@ have gen : ∀ (l₁ l₂ : list A) (p : l₁ ~ l₂), l₁ = [] → l₂ = (x::
end),
assume p, gen [] (x::l) p rfl rfl
protected theorem refl : ∀ (l : list A), l ~ l
protected theorem refl [refl] : ∀ (l : list A), l ~ l
| [] := nil
| (x::xs) := skip x (refl xs)
protected theorem symm : ∀ {l₁ l₂ : list A}, l₁ ~ l₂ → l₂ ~ l₁ :=
protected theorem symm [symm] : ∀ {l₁ l₂ : list A}, l₁ ~ l₂ → l₂ ~ l₁ :=
take l₁ l₂ p, perm.induction_on p
nil
(λ x l₁ l₂ p₁ r₁, skip x r₁)
(λ x y l, swap y x l)
(λ l₁ l₂ l₃ p₁ p₂ r₁ r₂, trans r₂ r₁)
attribute perm.trans [trans]
theorem eqv (A : Type) : equivalence (@perm A) :=
mk_equivalence (@perm A) (@perm.refl A) (@perm.symm A) (@perm.trans A)
protected definition is_setoid [instance] (A : Type) : setoid (list A) :=
setoid.mk (@perm A) (perm.eqv A)
calc_refl perm.refl
calc_symm perm.symm
calc_trans perm.trans
theorem mem_perm {a : A} {l₁ l₂ : list A} : l₁ ~ l₂ → a ∈ l₁ → a ∈ l₂ :=
assume p, perm.induction_on p
(λ h, h)

13
library/data/rat/basic.lean
View file

@ -26,12 +26,9 @@ definition equiv (a b : prerat) : Prop := num a * denom b = num b * denom a
infix `≡` := equiv
theorem equiv.refl (a : prerat) : a ≡ a := rfl
theorem equiv.refl [refl] (a : prerat) : a ≡ a := rfl
theorem equiv.symm {a b : prerat} (H : a ≡ b) : b ≡ a := !eq.symm H
calc_refl equiv.refl
calc_symm equiv.symm
theorem equiv.symm [symm] {a b : prerat} (H : a ≡ b) : b ≡ a := !eq.symm H
theorem num_eq_zero_of_equiv {a b : prerat} (H : a ≡ b) (na_zero : num a = 0) : num b = 0 :=
have H1 : num a * denom b = 0, from !zero_mul ▸ na_zero ▸ rfl,
@ -52,7 +49,7 @@ neg_of_neg_pos H3
theorem equiv_of_num_eq_zero {a b : prerat} (H1 : num a = 0) (H2 : num b = 0) : a ≡ b :=
by rewrite [↑equiv, H1, H2, *zero_mul]
theorem equiv.trans {a b c : prerat} (H1 : a ≡ b) (H2 : b ≡ c) : a ≡ c :=
theorem equiv.trans [trans] {a b c : prerat} (H1 : a ≡ b) (H2 : b ≡ c) : a ≡ c :=
decidable.by_cases
(assume b0 : num b = 0,
have a0 : num a = 0, from num_eq_zero_of_equiv (equiv.symm H1) b0,
@ -71,10 +68,6 @@ decidable.by_cases
*mul.left_comm (denom b), mul.comm (denom a)],
mul.cancel_left H3 H4)
calc_refl equiv.refl
calc_symm equiv.symm
calc_trans equiv.trans
theorem equiv.is_equivalence : equivalence equiv :=
mk_equivalence equiv equiv.refl @equiv.symm @equiv.trans

21
library/init/logic.lean
View file

@ -82,10 +82,10 @@ section
assume Hp, H ▸ Hp
end
calc_subst eq.subst
calc_refl eq.refl
calc_trans eq.trans
calc_symm eq.symm
attribute eq.subst [subst]
attribute eq.refl [refl]
attribute eq.trans [trans]
attribute eq.symm [symm]
/- ne -/
@ -154,10 +154,10 @@ end heq
theorem of_heq_true {a : Prop} (H : a == true) : a :=
of_eq_true (heq.to_eq H)
calc_trans heq.trans
calc_trans heq.of_heq_of_eq
calc_trans heq.of_eq_of_heq
calc_symm heq.symm
attribute heq.trans [trans]
attribute heq.of_heq_of_eq [trans]
attribute heq.of_eq_of_heq [trans]
attribute heq.symm [symm]
/- and -/
@ -258,8 +258,9 @@ iff.intro
(assume Hr : ¬a,
assume Hnna : ¬¬a, absurd Hr Hnna)
calc_refl iff.refl
calc_trans iff.trans
attribute iff.refl [refl]
attribute iff.symm [symm]
attribute iff.trans [trans]
inductive Exists {A : Type} (P : A → Prop) : Prop :=
intro : ∀ (a : A), P a → Exists P

13
library/init/nat.lean
View file

@ -76,7 +76,7 @@ namespace nat
(lt.base zero)
(λ a (hlt : zero < succ a), lt.step hlt)
definition lt.trans {a b c : nat} (H₁ : a < b) (H₂ : b < c) : a < c :=
definition lt.trans [trans] {a b c : nat} (H₁ : a < b) (H₂ : b < c) : a < c :=
have aux : a < b → a < c, from
lt.rec_on H₂
(λ h₁, lt.step h₁)
@ -185,32 +185,27 @@ namespace nat
definition succ_le_of_lt {a b : nat} (h : a < b) : succ a ≤ b :=
succ_lt_succ h
definition le.trans {a b c : nat} (h₁ : a ≤ b) (h₂ : b ≤ c) : a ≤ c :=
definition le.trans [trans] {a b c : nat} (h₁ : a ≤ b) (h₂ : b ≤ c) : a ≤ c :=
begin
cases h₁ with b' hlt,
apply h₂,
apply lt.trans hlt h₂
end
definition lt_of_le_of_lt {a b c : nat} (h₁ : a ≤ b) (h₂ : b < c) : a < c :=
definition lt_of_le_of_lt [trans] {a b c : nat} (h₁ : a ≤ b) (h₂ : b < c) : a < c :=
begin
cases h₁ with b' hlt,
apply h₂,
apply lt.trans hlt h₂
end
definition lt_of_lt_of_le {a b c : nat} (h₁ : a < b) (h₂ : b ≤ c) : a < c :=
definition lt_of_lt_of_le [trans] {a b c : nat} (h₁ : a < b) (h₂ : b ≤ c) : a < c :=
begin
cases h₁ with b' hlt,
apply lt_of_succ_lt_succ h₂,
apply lt.trans hlt (lt_of_succ_lt_succ h₂)
end
calc_trans lt.trans
calc_trans lt_of_le_of_lt
calc_trans lt_of_lt_of_le
calc_trans le.trans
definition max (a b : nat) : nat :=
if a < b then b else a

2
library/logic/instances.lean
View file

@ -87,7 +87,7 @@ namespace iff
@general_subst.subst Prop iff P C a b H H1
end iff
calc_subst iff.subst
attribute iff.subst [subst]
namespace iff_ops
notation H ⁻¹ := iff.symm H

4
src/emacs/lean-syntax.el
View file

@ -14,8 +14,7 @@
"print" "theorem" "example" "abbreviation"
"open" "as" "export" "axiom" "axioms" "inductive" "with" "structure" "record" "universe" "universes"
"alias" "help" "environment" "options" "precedence" "reserve"
"calc_trans" "calc_subst" "calc_refl" "calc_symm" "match"
"infix" "infixl" "infixr" "notation" "postfix" "prefix"
"match" "infix" "infixl" "infixr" "notation" "postfix" "prefix"
"tactic_infix" "tactic_infixl" "tactic_infixr" "tactic_notation" "tactic_postfix" "tactic_prefix"
"eval" "check" "coercion" "end"
"using" "namespace" "section" "fields" "find_decl"
@ -123,6 +122,7 @@
"\[coercion\]" "\[unfold-f\]" "\[reducible\]" "\[irreducible\]" "\[semireducible\]" "\[quasireducible\]" "\[wf\]"
"\[whnf\]" "\[multiple-instances\]" "\[none\]"
"\[decls\]" "\[declarations\]" "\[all-transparent\]" "\[coercions\]" "\[classes\]"
"\[symm\]" "\[subst\]" "\[refl\]" "\[trans\]"
"\[notations\]" "\[abbreviations\]" "\[begin-end-hints\]" "\[tactic-hints\]" "\[reduce-hints\]"))
. 'font-lock-doc-face)
(,(rx "\[priority" (zero-or-more (not (any "\]"))) "\]") . font-lock-doc-face)

1
src/frontends/lean/builtin_cmds.cpp
View file

@ -860,7 +860,6 @@ void init_cmd_table(cmd_table & r) {
register_structure_cmd(r);
register_migrate_cmd(r);
register_notation_cmds(r);
register_calc_cmds(r);
register_begin_end_cmds(r);
register_tactic_hint_cmd(r);
}

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

@ -14,6 +14,7 @@ Author: Leonardo de Moura
#include "util/buffer.h"
#include "util/interrupt.h"
#include "kernel/environment.h"
#include "library/equivalence_manager.h"
#include "library/module.h"
#include "library/constants.h"
#include "library/choice.h"
@ -30,180 +31,18 @@ Author: Leonardo de Moura
#include "frontends/lean/begin_end_ext.h"
namespace lean {
// Check whether e is of the form (f ...) where f is a constant. If it is return f.
static name const & get_fn_const(expr const & e, char const * msg) {
expr const & fn = get_app_fn(e);
if (!is_constant(fn))
throw exception(msg);
return const_name(fn);
}
static pair<expr, unsigned> extract_arg_types_core(environment const & env, name const & f, buffer<expr> & arg_types) {
declaration d = env.get(f);
expr f_type = d.get_type();
while (is_pi(f_type)) {
arg_types.push_back(binding_domain(f_type));
f_type = binding_body(f_type);
}
return mk_pair(f_type, d.get_num_univ_params());
}
static expr extract_arg_types(environment const & env, name const & f, buffer<expr> & arg_types) {
return extract_arg_types_core(env, f, arg_types).first;
}
enum class calc_cmd { Subst, Trans, Refl, Symm };
struct calc_entry {
calc_cmd m_cmd;
name m_name;
calc_entry() {}
calc_entry(calc_cmd c, name const & n):m_cmd(c), m_name(n) {}
};
struct calc_state {
typedef name_map<std::tuple<name, unsigned, unsigned>> refl_table;
typedef name_map<std::tuple<name, unsigned, unsigned>> subst_table;
typedef name_map<std::tuple<name, unsigned, unsigned>> symm_table;
typedef rb_map<name_pair, std::tuple<name, name, unsigned>, name_pair_quick_cmp> trans_table;
trans_table m_trans_table;
refl_table m_refl_table;
subst_table m_subst_table;
symm_table m_symm_table;
calc_state() {}
void add_calc_subst(environment const & env, name const & subst) {
buffer<expr> arg_types;
auto p = extract_arg_types_core(env, subst, arg_types);
expr r_type = p.first;
unsigned nunivs = p.second;
unsigned nargs = arg_types.size();
if (nargs < 2)
throw exception("invalid calc substitution theorem, it must have at least 2 arguments");
name const & rop = get_fn_const(arg_types[nargs-2], "invalid calc substitution theorem, argument penultimate argument must be an operator application");
m_subst_table.insert(rop, std::make_tuple(subst, nargs, nunivs));
}
void add_calc_refl(environment const & env, name const & refl) {
buffer<expr> arg_types;
auto p = extract_arg_types_core(env, refl, arg_types);
expr r_type = p.first;
unsigned nunivs = p.second;
unsigned nargs = arg_types.size();
if (nargs < 1)
throw exception("invalid calc reflexivity rule, it must have at least 1 argument");
name const & rop = get_fn_const(r_type, "invalid calc reflexivity rule, result type must be an operator application");
m_refl_table.insert(rop, std::make_tuple(refl, nargs, nunivs));
}
void add_calc_trans(environment const & env, name const & trans) {
buffer<expr> arg_types;
expr r_type = extract_arg_types(env, trans, arg_types);
unsigned nargs = arg_types.size();
if (nargs < 5)
throw exception("invalid calc transitivity rule, it must have at least 5 arguments");
name const & rop = get_fn_const(r_type, "invalid calc transitivity rule, result type must be an operator application");
name const & op1 = get_fn_const(arg_types[nargs-2], "invalid calc transitivity rule, penultimate argument must be an operator application");
name const & op2 = get_fn_const(arg_types[nargs-1], "invalid calc transitivity rule, last argument must be an operator application");
m_trans_table.insert(name_pair(op1, op2), std::make_tuple(trans, rop, nargs));
}
void add_calc_symm(environment const & env, name const & symm) {
buffer<expr> arg_types;
auto p = extract_arg_types_core(env, symm, arg_types);
expr r_type = p.first;
unsigned nunivs = p.second;
unsigned nargs = arg_types.size();
if (nargs < 1)
throw exception("invalid calc symmetry rule, it must have at least 1 argument");
name const & rop = get_fn_const(r_type, "invalid calc symmetry rule, result type must be an operator application");
m_symm_table.insert(rop, std::make_tuple(symm, nargs, nunivs));
}
};
static name * g_calc_name = nullptr;
static std::string * g_key = nullptr;
struct calc_config {
typedef calc_state state;
typedef calc_entry entry;
static void add_entry(environment const & env, io_state const &, state & s, entry const & e) {
switch (e.m_cmd) {
case calc_cmd::Refl: s.add_calc_refl(env, e.m_name); break;
case calc_cmd::Subst: s.add_calc_subst(env, e.m_name); break;
case calc_cmd::Trans: s.add_calc_trans(env, e.m_name); break;
case calc_cmd::Symm: s.add_calc_symm(env, e.m_name); break;
}
}
static name const & get_class_name() {
return *g_calc_name;
}
static std::string const & get_serialization_key() {
return *g_key;
}
static void write_entry(serializer & s, entry const & e) {
s << static_cast<char>(e.m_cmd) << e.m_name;
}
static entry read_entry(deserializer & d) {
entry e;
char cmd;
d >> cmd >> e.m_name;
e.m_cmd = static_cast<calc_cmd>(cmd);
return e;
}
static optional<unsigned> get_fingerprint(entry const &) {
return optional<unsigned>();
}
};
template class scoped_ext<calc_config>;
typedef scoped_ext<calc_config> calc_ext;
environment calc_subst_cmd(parser & p) {
name id = p.check_constant_next("invalid 'calc_subst' command, constant expected");
return calc_ext::add_entry(p.env(), get_dummy_ios(), calc_entry(calc_cmd::Subst, id));
}
environment calc_refl_cmd(parser & p) {
name id = p.check_constant_next("invalid 'calc_refl' command, constant expected");
return calc_ext::add_entry(p.env(), get_dummy_ios(), calc_entry(calc_cmd::Refl, id));
}
environment calc_trans_cmd(parser & p) {
name id = p.check_constant_next("invalid 'calc_trans' command, constant expected");
return calc_ext::add_entry(p.env(), get_dummy_ios(), calc_entry(calc_cmd::Trans, id));
}
environment calc_symm_cmd(parser & p) {
name id = p.check_constant_next("invalid 'calc_symm' command, constant expected");
return calc_ext::add_entry(p.env(), get_dummy_ios(), calc_entry(calc_cmd::Symm, id));
}
void register_calc_cmds(cmd_table & r) {
add_cmd(r, cmd_info("calc_subst", "set the substitution rule that is used by the calculational proof '{...}' notation", calc_subst_cmd));
add_cmd(r, cmd_info("calc_refl", "set the reflexivity rule for an operator, this command is relevant for the calculational proof '{...}' notation", calc_refl_cmd));
add_cmd(r, cmd_info("calc_trans", "set the transitivity rule for a pair of operators, this command is relevant for the calculational proof '{...}' notation", calc_trans_cmd));
add_cmd(r, cmd_info("calc_symm", "set the symmetry rule for an operator, this command is relevant for the calculational proof '{...}' notation", calc_symm_cmd));
}
static optional<std::tuple<name, unsigned, unsigned>> get_info(name_map<std::tuple<name, unsigned, unsigned>> const & table, name const & op) {
if (auto it = table.find(op)) {
return optional<std::tuple<name, unsigned, unsigned>>(*it);
} else {
return optional<std::tuple<name, unsigned, unsigned>>();
}
}
optional<std::tuple<name, unsigned, unsigned>> get_calc_refl_info(environment const & env, name const & op) {
return get_info(calc_ext::get_state(env).m_refl_table, op);
return get_refl_extra_info(env, op);
}
optional<std::tuple<name, unsigned, unsigned>> get_calc_subst_info(environment const & env, name const & op) {
return get_info(calc_ext::get_state(env).m_subst_table, op);
return get_subst_extra_info(env, op);
}
optional<std::tuple<name, unsigned, unsigned>> get_calc_symm_info(environment const & env, name const & op) {
return get_info(calc_ext::get_state(env).m_symm_table, op);
return get_symm_extra_info(env, op);
}
static name * g_calc_name = nullptr;
static expr mk_calc_annotation_core(expr const & e) { return mk_annotation(*g_calc_name, e); }
static expr mk_calc_annotation(expr const & pr) {
if (is_by(pr) || is_begin_end_annotation(pr) || is_sorry(pr)) {
@ -263,12 +102,12 @@ static void parse_calc_proof(parser & p, buffer<calc_pred> const & preds, std::v
p.check_token_next(get_colon_tk(), "invalid 'calc' expression, ':' expected");
if (p.curr_is_token(get_lcurly_tk())) {
p.next();
environment const & env = p.env();
expr pr = p.parse_expr();
p.check_token_next(get_rcurly_tk(), "invalid 'calc' expression, '}' expected");
calc_state const & state = calc_ext::get_state(p.env());
for (auto const & pred : preds) {
if (auto refl_it = state.m_refl_table.find(pred_op(pred))) {
if (auto subst_it = state.m_subst_table.find(pred_op(pred))) {
if (auto refl_it = get_refl_extra_info(env, pred_op(pred))) {
if (auto subst_it = get_subst_extra_info(env, pred_op(pred))) {
expr refl = mk_op_fn(p, std::get<0>(*refl_it), std::get<1>(*refl_it)-1, pos);
expr refl_pr = p.mk_app(refl, pred_lhs(pred), pos);
expr subst = mk_op_fn(p, std::get<0>(*subst_it), std::get<1>(*subst_it)-2, pos);
@ -304,8 +143,8 @@ static unsigned get_arity_of(parser & p, name const & op) {
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) {
environment const & env = p.env();
res_steps.clear();
calc_state const & state = calc_ext::get_state(p.env());
for (calc_step const & s1 : steps1) {
check_interrupted();
calc_pred const & pred1 = step_pred(s1);
@ -315,7 +154,7 @@ static void join(parser & p, std::vector<calc_step> const & steps1, std::vector<
expr const & pr2 = step_proof(s2);
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)));
auto trans_it = get_trans_extra_info(env, pred_op(pred1), pred_op(pred2));
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);
@ -380,14 +219,9 @@ expr parse_calc(parser & p) {
void initialize_calc() {
g_calc_name = new name("calc");
g_key = new std::string("calc");
calc_ext::initialize();
register_annotation(*g_calc_name);
}
void finalize_calc() {
calc_ext::finalize();
delete g_key;
delete g_calc_name;
}
}

1
src/frontends/lean/calc.h
View file

@ -8,7 +8,6 @@ Author: Leonardo de Moura
#include "frontends/lean/cmd_table.h"
namespace lean {
class parser;
void register_calc_cmds(cmd_table & r);
expr parse_calc(parser & p);
bool is_calc_annotation(expr const & e);
/** \brief Given an operator name \c op, return the symmetry rule associated with, number of arguments, and universe parameters.

29
src/frontends/lean/decl_cmds.cpp
View file

@ -27,6 +27,7 @@ Author: Leonardo de Moura
#include "library/replace_visitor.h"
#include "library/class.h"
#include "library/abbreviation.h"
#include "library/equivalence_manager.h"
#include "library/unfold_macros.h"
#include "library/definitional/equations.h"
#include "library/error_handling/error_handling.h"
@ -353,6 +354,10 @@ struct decl_attributes {
bool m_is_parsing_only;
bool m_has_multiple_instances;
bool m_unfold_f_hint;
bool m_symm;
bool m_trans;
bool m_refl;
bool m_subst;
optional<unsigned> m_priority;
optional<unsigned> m_unfold_c_hint;
@ -371,6 +376,10 @@ struct decl_attributes {
m_is_parsing_only = false;
m_has_multiple_instances = false;
m_unfold_f_hint = false;
m_symm = false;
m_trans = false;
m_refl = false;
m_subst = false;
}
struct elim_choice_fn : public replace_visitor {
@ -482,6 +491,18 @@ struct decl_attributes {
throw parser_error("invalid '[unfold-c]' attribute, value must be greater than 0", pos);
m_unfold_c_hint = r - 1;
p.check_token_next(get_rbracket_tk(), "invalid 'unfold-c', ']' expected");
} else if (p.curr_is_token(get_symm_tk())) {
p.next();
m_symm = true;
} else if (p.curr_is_token(get_refl_tk())) {
p.next();
m_refl = true;
} else if (p.curr_is_token(get_trans_tk())) {
p.next();
m_trans = true;
} else if (p.curr_is_token(get_subst_tk())) {
p.next();
m_subst = true;
} else {
break;
}
@ -527,6 +548,14 @@ struct decl_attributes {
if (m_unfold_f_hint)
env = add_unfold_f_hint(env, d, m_persistent);
}
if (m_symm)
env = add_symm(env, d, m_persistent);
if (m_refl)
env = add_refl(env, d, m_persistent);
if (m_trans)
env = add_trans(env, d, m_persistent);
if (m_subst)
env = add_subst(env, d, m_persistent);
if (m_is_class)
env = add_class(env, d, m_persistent);
if (m_has_multiple_instances)

2
src/frontends/lean/token_table.cpp
View file

@ -107,7 +107,7 @@ void init_token_table(token_table & t) {
"definition", "example", "coercion", "abbreviation",
"variables", "parameter", "parameters", "constant", "constants", "[persistent]", "[visible]", "[instance]",
"[none]", "[class]", "[coercion]", "[reducible]", "[irreducible]", "[semireducible]", "[quasireducible]",
"[parsing-only]", "[multiple-instances]",
"[parsing-only]", "[multiple-instances]", "[symm]", "[trans]", "[refl]", "[subst]",
"evaluate", "check", "eval", "[wf]", "[whnf]", "[all-transparent]", "[priority", "[unfold-f]", "[unfold-c", "print",
"end", "namespace", "section", "prelude", "help",
"import", "inductive", "record", "structure", "module", "universe", "universes", "local",

16
src/frontends/lean/tokens.cpp
View file

@ -134,6 +134,10 @@ static name * g_fields = nullptr;
static name * g_trust = nullptr;
static name * g_metaclasses = nullptr;
static name * g_inductive = nullptr;
static name * g_symm = nullptr;
static name * g_trans = nullptr;
static name * g_refl = nullptr;
static name * g_subst = nullptr;
void initialize_tokens() {
g_period = new name(".");
@ -240,6 +244,10 @@ void initialize_tokens() {
g_semireducible = new name("[semireducible]");
g_irreducible = new name("[irreducible]");
g_parsing_only = new name("[parsing-only]");
g_symm = new name("[symm]");
g_trans = new name("[trans]");
g_refl = new name("[refl]");
g_subst = new name("[subst]");
g_attribute = new name("attribute");
g_with = new name("with");
g_class = new name("[class]");
@ -303,6 +311,10 @@ void finalize_tokens() {
delete g_unfold_c;
delete g_unfold_f;
delete g_coercion;
delete g_symm;
delete g_refl;
delete g_trans;
delete g_subst;
delete g_reducible;
delete g_quasireducible;
delete g_semireducible;
@ -496,6 +508,10 @@ name const & get_priority_tk() { return *g_priority; }
name const & get_unfold_c_tk() { return *g_unfold_c; }
name const & get_unfold_f_tk() { return *g_unfold_f; }
name const & get_coercion_tk() { return *g_coercion; }
name const & get_symm_tk() { return *g_symm; }
name const & get_trans_tk() { return *g_trans; }
name const & get_refl_tk() { return *g_refl; }
name const & get_subst_tk() { return *g_subst; }
name const & get_reducible_tk() { return *g_reducible; }
name const & get_quasireducible_tk() { return *g_quasireducible; }
name const & get_semireducible_tk() { return *g_semireducible; }

4
src/frontends/lean/tokens.h
View file

@ -136,4 +136,8 @@ name const & get_fields_tk();
name const & get_trust_tk();
name const & get_metaclasses_tk();
name const & get_inductive_tk();
name const & get_symm_tk();
name const & get_trans_tk();
name const & get_refl_tk();
name const & get_subst_tk();
}

2
src/library/CMakeLists.txt
View file

@ -12,6 +12,6 @@ add_library(library deep_copy.cpp expr_lt.cpp io_state.cpp occurs.cpp
metavar_closure.cpp reducible.cpp init_module.cpp
generic_exception.cpp fingerprint.cpp flycheck.cpp hott_kernel.cpp
local_context.cpp choice_iterator.cpp pp_options.cpp unfold_macros.cpp
app_builder.cpp projection.cpp abbreviation.cpp)
app_builder.cpp projection.cpp abbreviation.cpp equivalence_manager.cpp)
target_link_libraries(library ${LEAN_LIBS})

218
src/library/equivalence_manager.cpp Normal file
View file

@ -0,0 +1,218 @@
/*
Copyright (c) 2015 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#include <string>
#include "util/optional.h"
#include "util/name.h"
#include "util/rb_map.h"
#include "library/constants.h"
#include "library/scoped_ext.h"
namespace lean {
// Check whether e is of the form (f ...) where f is a constant. If it is return f.
static name const & get_fn_const(expr const & e, char const * msg) {
expr const & fn = get_app_fn(e);
if (!is_constant(fn))
throw exception(msg);
return const_name(fn);
}
static pair<expr, unsigned> extract_arg_types_core(environment const & env, name const & f, buffer<expr> & arg_types) {
declaration d = env.get(f);
expr f_type = d.get_type();
while (is_pi(f_type)) {
arg_types.push_back(binding_domain(f_type));
f_type = binding_body(f_type);
}
return mk_pair(f_type, d.get_num_univ_params());
}
static expr extract_arg_types(environment const & env, name const & f, buffer<expr> & arg_types) {
return extract_arg_types_core(env, f, arg_types).first;
}
enum class op_kind { Subst, Trans, Refl, Symm };
struct eqv_entry {
op_kind m_kind;
name m_name;
eqv_entry() {}
eqv_entry(op_kind k, name const & n):m_kind(k), m_name(n) {}
};
struct eqv_state {
typedef name_map<std::tuple<name, unsigned, unsigned>> refl_table;
typedef name_map<std::tuple<name, unsigned, unsigned>> subst_table;
typedef name_map<std::tuple<name, unsigned, unsigned>> symm_table;
typedef rb_map<name_pair, std::tuple<name, name, unsigned>, name_pair_quick_cmp> trans_table;
trans_table m_trans_table;
refl_table m_refl_table;
subst_table m_subst_table;
symm_table m_symm_table;
eqv_state() {}
void add_subst(environment const & env, name const & subst) {
buffer<expr> arg_types;
auto p = extract_arg_types_core(env, subst, arg_types);
expr r_type = p.first;
unsigned nunivs = p.second;
unsigned nargs = arg_types.size();
if (nargs < 2)
throw exception("invalid substitution theorem, it must have at least 2 arguments");
name const & rop = get_fn_const(arg_types[nargs-2], "invalid substitution theorem, penultimate argument must be an operator application");
m_subst_table.insert(rop, std::make_tuple(subst, nargs, nunivs));
}
void add_refl(environment const & env, name const & refl) {
buffer<expr> arg_types;
auto p = extract_arg_types_core(env, refl, arg_types);
expr r_type = p.first;
unsigned nunivs = p.second;
unsigned nargs = arg_types.size();
if (nargs < 1)
throw exception("invalid reflexivity rule, it must have at least 1 argument");
name const & rop = get_fn_const(r_type, "invalid reflexivity rule, result type must be an operator application");
m_refl_table.insert(rop, std::make_tuple(refl, nargs, nunivs));
}
void add_trans(environment const & env, name const & trans) {
buffer<expr> arg_types;
expr r_type = extract_arg_types(env, trans, arg_types);
unsigned nargs = arg_types.size();
if (nargs < 5)
throw exception("invalid transitivity rule, it must have at least 5 arguments");
name const & rop = get_fn_const(r_type, "invalid transitivity rule, result type must be an operator application");
name const & op1 = get_fn_const(arg_types[nargs-2], "invalid transitivity rule, penultimate argument must be an operator application");
name const & op2 = get_fn_const(arg_types[nargs-1], "invalid transitivity rule, last argument must be an operator application");
m_trans_table.insert(name_pair(op1, op2), std::make_tuple(trans, rop, nargs));
}
void add_symm(environment const & env, name const & symm) {
buffer<expr> arg_types;
auto p = extract_arg_types_core(env, symm, arg_types);
expr r_type = p.first;
unsigned nunivs = p.second;
unsigned nargs = arg_types.size();
if (nargs < 1)
throw exception("invalid symmetry rule, it must have at least 1 argument");
name const & rop = get_fn_const(r_type, "invalid symmetry rule, result type must be an operator application");
m_symm_table.insert(rop, std::make_tuple(symm, nargs, nunivs));
}
};
static name * g_eqv_name = nullptr;
static std::string * g_key = nullptr;
struct eqv_config {
typedef eqv_state state;
typedef eqv_entry entry;
static void add_entry(environment const & env, io_state const &, state & s, entry const & e) {
switch (e.m_kind) {
case op_kind::Refl: s.add_refl(env, e.m_name); break;
case op_kind::Subst: s.add_subst(env, e.m_name); break;
case op_kind::Trans: s.add_trans(env, e.m_name); break;
case op_kind::Symm: s.add_symm(env, e.m_name); break;
}
}
static name const & get_class_name() {
return *g_eqv_name;
}
static std::string const & get_serialization_key() {
return *g_key;
}
static void write_entry(serializer & s, entry const & e) {
s << static_cast<char>(e.m_kind) << e.m_name;
}
static entry read_entry(deserializer & d) {
entry e;
char cmd;
d >> cmd >> e.m_name;
e.m_kind = static_cast<op_kind>(cmd);
return e;
}
static optional<unsigned> get_fingerprint(entry const &) {
return optional<unsigned>();
}
};
template class scoped_ext<eqv_config>;
typedef scoped_ext<eqv_config> eqv_ext;
environment add_subst(environment const & env, name const & n, bool persistent) {
return eqv_ext::add_entry(env, get_dummy_ios(), eqv_entry(op_kind::Subst, n), persistent);
}
environment add_refl(environment const & env, name const & n, bool persistent) {
return eqv_ext::add_entry(env, get_dummy_ios(), eqv_entry(op_kind::Refl, n), persistent);
}
environment add_symm(environment const & env, name const & n, bool persistent) {
return eqv_ext::add_entry(env, get_dummy_ios(), eqv_entry(op_kind::Symm, n), persistent);
}
environment add_trans(environment const & env, name const & n, bool persistent) {
return eqv_ext::add_entry(env, get_dummy_ios(), eqv_entry(op_kind::Trans, n), persistent);
}
static optional<std::tuple<name, unsigned, unsigned>> get_info(name_map<std::tuple<name, unsigned, unsigned>> const & table, name const & op) {
if (auto it = table.find(op)) {
return optional<std::tuple<name, unsigned, unsigned>>(*it);
} else {
return optional<std::tuple<name, unsigned, unsigned>>();
}
}
optional<std::tuple<name, unsigned, unsigned>> get_refl_extra_info(environment const & env, name const & op) {
return get_info(eqv_ext::get_state(env).m_refl_table, op);
}
optional<std::tuple<name, unsigned, unsigned>> get_subst_extra_info(environment const & env, name const & op) {
return get_info(eqv_ext::get_state(env).m_subst_table, op);
}
optional<std::tuple<name, unsigned, unsigned>> get_symm_extra_info(environment const & env, name const & op) {
return get_info(eqv_ext::get_state(env).m_symm_table, op);
}
optional<std::tuple<name, name, unsigned>> get_trans_extra_info(environment const & env, name const & op1, name const & op2) {
if (auto it = eqv_ext::get_state(env).m_trans_table.find(mk_pair(op1, op2))) {
return optional<std::tuple<name, name, unsigned>>(*it);
} else {
return optional<std::tuple<name, name, unsigned>>();
}
}
optional<name> get_refl_info(environment const & env, name const & op) {
if (auto it = get_refl_extra_info(env, op))
return optional<name>(std::get<0>(*it));
else
return optional<name>();
}
optional<name> get_symm_info(environment const & env, name const & op) {
if (auto it = get_symm_extra_info(env, op))
return optional<name>(std::get<0>(*it));
else
return optional<name>();
}
optional<name> get_trans_info(environment const & env, name const & op) {
if (auto it = get_trans_extra_info(env, op, op))
return optional<name>(std::get<0>(*it));
else
return optional<name>();
}
void initialize_equivalence_manager() {
g_eqv_name = new name("eqv");
g_key = new std::string("eqv");
eqv_ext::initialize();
}
void finalize_equivalence_manager() {
eqv_ext::finalize();
delete g_key;
delete g_eqv_name;
}
}

24
src/library/equivalence_manager.h Normal file
View file

@ -0,0 +1,24 @@
/*
Copyright (c) 2015 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#pragma once
#include "kernel/environment.h"
namespace lean {
environment add_subst(environment const & env, name const & n, bool persistent = true);
environment add_refl(environment const & env, name const & n, bool persistent = true);
environment add_symm(environment const & env, name const & n, bool persistent = true);
environment add_trans(environment const & env, name const & n, bool persistent = true);
optional<std::tuple<name, unsigned, unsigned>> get_refl_extra_info(environment const & env, name const & op);
optional<std::tuple<name, unsigned, unsigned>> get_subst_extra_info(environment const & env, name const & op);
optional<std::tuple<name, unsigned, unsigned>> get_symm_extra_info(environment const & env, name const & op);
optional<std::tuple<name, name, unsigned>> get_trans_extra_info(environment const & env, name const & op1, name const & op2);
optional<name> get_refl_info(environment const & env, name const & op);
optional<name> get_symm_info(environment const & env, name const & op);
optional<name> get_trans_info(environment const & env, name const & op);
void initialize_equivalence_manager();
void finalize_equivalence_manager();
}

3
src/library/init_module.cpp
View file

@ -36,6 +36,7 @@ Author: Leonardo de Moura
#include "library/projection.h"
#include "library/normalize.h"
#include "library/abbreviation.h"
#include "library/equivalence_manager.h"
namespace lean {
void initialize_library_module() {
@ -71,9 +72,11 @@ void initialize_library_module() {
initialize_projection();
initialize_normalize();
initialize_abbreviation();
initialize_equivalence_manager();
}
void finalize_library_module() {
finalize_equivalence_manager();
finalize_abbreviation();
finalize_normalize();
finalize_projection();

18
tests/lean/calc1.lean
View file

@ -11,13 +11,13 @@ axiom le_trans (a b c : A) (H1 : a ≤ b) (H2 : b ≤ c) : a ≤ c
axiom le_refl (a : A) : a ≤ a
axiom eq_le_trans (a b c : A) (H1 : a = b) (H2 : b ≤ c) : a ≤ c
axiom le_eq_trans (a b c : A) (H1 : a ≤ b) (H2 : b = c) : a ≤ c
calc_subst subst
calc_refl eq_refl
calc_refl le_refl
calc_trans eq_trans
calc_trans le_trans
calc_trans eq_le_trans
calc_trans le_eq_trans
attribute subst [subst]
attribute eq_refl [refl]
attribute le_refl [refl]
attribute eq_trans [trans]
attribute le_trans [trans]
attribute eq_le_trans [trans]
attribute le_eq_trans [trans]
constants a b c d e f : A
axiom H1 : a = b
axiom H2 : b ≤ c
@ -36,14 +36,14 @@ axiom lt_le_trans (a b c : A) (H1 : a < b) (H2 : b ≤ c) : a < c
axiom H5 : c < d
check calc b ≤ c : H2
... < d : H5 -- Error le_lt_trans was not registered yet
calc_trans le_lt_trans
attribute le_lt_trans [trans]
check calc b ≤ c : H2
... < d : H5
constant le2 : A → A → bool
infixl `≤`:50 := le2
constant le2_trans (a b c : A) (H1 : le2 a b) (H2 : le2 b c) : le2 a c
calc_trans le2_trans
attribute le2_trans [trans]
print raw calc b ≤ c : H2
... ≤ d : H3
... ≤ e : H4

6
tests/lean/interactive/eq2.lean
View file

@ -37,9 +37,9 @@ namespace eq
subst H (refl a)
end eq
calc_subst eq.subst
calc_refl eq.refl
calc_trans eq.trans
attribute eq.subst [subst]
attribute eq.refl [refl]
attribute eq.trans [trans]
namespace eq_ops
postfix `⁻¹`:1024 := eq.symm

2
tests/lean/run/calc.lean
View file

@ -4,7 +4,7 @@ import data.num
namespace foo
constant le : num → num → Prop
axiom le_trans {a b c : num} : le a b → le b c → le a c
calc_trans le_trans
attribute le_trans [trans]
infix `≤` := le
end foo