From cd17618f4a32bea8a8765db41fea56f33e895134 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 2 May 2015 15:15:35 -0700 Subject: [PATCH] refactor(library): replace 'calc_trans', 'calc_symm', 'calc_refl' and 'calc_subst' commands with attributes '[symm]', '[refl]', '[trans]' and '[subst]' These attributes are used by the calc command. They will also be used by tactics such as 'reflexivity', 'symmetry' and 'transitivity'. See issue #500 --- hott/init/equiv.hlean | 10 +- hott/init/logic.hlean | 17 ++- hott/init/nat.hlean | 29 +--- hott/init/path.hlean | 17 +-- hott/init/ua.hlean | 3 +- library/algebra/order.lean | 25 +--- library/data/int/basic.lean | 10 +- library/data/list/perm.lean | 10 +- library/data/rat/basic.lean | 13 +- library/init/logic.lean | 21 +-- library/init/nat.lean | 13 +- library/logic/instances.lean | 2 +- src/emacs/lean-syntax.el | 4 +- src/frontends/lean/builtin_cmds.cpp | 1 - src/frontends/lean/calc.cpp | 188 ++---------------------- src/frontends/lean/calc.h | 1 - src/frontends/lean/decl_cmds.cpp | 29 ++++ src/frontends/lean/token_table.cpp | 2 +- src/frontends/lean/tokens.cpp | 16 ++ src/frontends/lean/tokens.h | 4 + src/library/CMakeLists.txt | 2 +- src/library/equivalence_manager.cpp | 218 ++++++++++++++++++++++++++++ src/library/equivalence_manager.h | 24 +++ src/library/init_module.cpp | 3 + tests/lean/calc1.lean | 18 +-- tests/lean/interactive/eq2.lean | 6 +- tests/lean/run/calc.lean | 2 +- 27 files changed, 381 insertions(+), 307 deletions(-) create mode 100644 src/library/equivalence_manager.cpp create mode 100644 src/library/equivalence_manager.h diff --git a/hott/init/equiv.hlean b/hott/init/equiv.hlean index d440312a71..bb428f74ed 100644 --- a/hott/init/equiv.hlean +++ b/hott/init/equiv.hlean @@ -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 diff --git a/hott/init/logic.hlean b/hott/init/logic.hlean index a9ce529ce9..984b503ff7 100644 --- a/hott/init/logic.hlean +++ b/hott/init/logic.hlean @@ -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 -/ diff --git a/hott/init/nat.hlean b/hott/init/nat.hlean index 13c4977654..7f92cd5f5f 100644 --- a/hott/init/nat.hlean +++ b/hott/init/nat.hlean @@ -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 diff --git a/hott/init/path.hlean b/hott/init/path.hlean index 18eedc72cf..282aef3454 100644 --- a/hott/init/path.hlean +++ b/hott/init/path.hlean @@ -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 -/ diff --git a/hott/init/ua.hlean b/hott/init/ua.hlean index e5fe8bd960..7312a67597 100644 --- a/hott/init/ua.hlean +++ b/hott/init/ua.hlean @@ -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 := diff --git a/library/algebra/order.lean b/library/algebra/order.lean index 506a14dc4b..2d92171120 100644 --- a/library/algebra/order.lean +++ b/library/algebra/order.lean @@ -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, diff --git a/library/data/int/basic.lean b/library/data/int/basic.lean index 34fbcf995a..5393469b26 100644 --- a/library/data/int/basic.lean +++ b/library/data/int/basic.lean @@ -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) diff --git a/library/data/list/perm.lean b/library/data/list/perm.lean index 6fbce67e1e..32176a6478 100644 --- a/library/data/list/perm.lean +++ b/library/data/list/perm.lean @@ -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) diff --git a/library/data/rat/basic.lean b/library/data/rat/basic.lean index 3a652b2c97..6b4e2a4386 100644 --- a/library/data/rat/basic.lean +++ b/library/data/rat/basic.lean @@ -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 diff --git a/library/init/logic.lean b/library/init/logic.lean index 6da90b0ad9..5381988282 100644 --- a/library/init/logic.lean +++ b/library/init/logic.lean @@ -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 diff --git a/library/init/nat.lean b/library/init/nat.lean index 7ace6b2a74..d4c0cf6a6f 100644 --- a/library/init/nat.lean +++ b/library/init/nat.lean @@ -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 diff --git a/library/logic/instances.lean b/library/logic/instances.lean index f5da26e7ac..42e10b7e4d 100644 --- a/library/logic/instances.lean +++ b/library/logic/instances.lean @@ -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 diff --git a/src/emacs/lean-syntax.el b/src/emacs/lean-syntax.el index d2236ef1ef..892eb0aa65 100644 --- a/src/emacs/lean-syntax.el +++ b/src/emacs/lean-syntax.el @@ -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) diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp index e08c62900d..73619ae8c5 100644 --- a/src/frontends/lean/builtin_cmds.cpp +++ b/src/frontends/lean/builtin_cmds.cpp @@ -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); } diff --git a/src/frontends/lean/calc.cpp b/src/frontends/lean/calc.cpp index 4f2b525260..d4718641c8 100644 --- a/src/frontends/lean/calc.cpp +++ b/src/frontends/lean/calc.cpp @@ -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 extract_arg_types_core(environment const & env, name const & f, buffer & 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 & 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> refl_table; - typedef name_map> subst_table; - typedef name_map> symm_table; - typedef rb_map, 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 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 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 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 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(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(cmd); - return e; - } - static optional get_fingerprint(entry const &) { - return optional(); - } -}; - -template class scoped_ext; -typedef scoped_ext 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> get_info(name_map> const & table, name const & op) { - if (auto it = table.find(op)) { - return optional>(*it); - } else { - return optional>(); - } -} - optional> 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> 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> 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 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 const & steps1, std::vector const & steps2, std::vector & 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 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; } } diff --git a/src/frontends/lean/calc.h b/src/frontends/lean/calc.h index 4df3c0d50f..15df441285 100644 --- a/src/frontends/lean/calc.h +++ b/src/frontends/lean/calc.h @@ -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. diff --git a/src/frontends/lean/decl_cmds.cpp b/src/frontends/lean/decl_cmds.cpp index f8c79ff428..bb2c775bf6 100644 --- a/src/frontends/lean/decl_cmds.cpp +++ b/src/frontends/lean/decl_cmds.cpp @@ -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 m_priority; optional 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) diff --git a/src/frontends/lean/token_table.cpp b/src/frontends/lean/token_table.cpp index f7f48c4a82..d764ef67e4 100644 --- a/src/frontends/lean/token_table.cpp +++ b/src/frontends/lean/token_table.cpp @@ -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", diff --git a/src/frontends/lean/tokens.cpp b/src/frontends/lean/tokens.cpp index 2c5f6f6283..316d64a6db 100644 --- a/src/frontends/lean/tokens.cpp +++ b/src/frontends/lean/tokens.cpp @@ -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; } diff --git a/src/frontends/lean/tokens.h b/src/frontends/lean/tokens.h index 168f68fe0c..6ca75a8b41 100644 --- a/src/frontends/lean/tokens.h +++ b/src/frontends/lean/tokens.h @@ -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(); } diff --git a/src/library/CMakeLists.txt b/src/library/CMakeLists.txt index 2f3318942c..a46a0939c2 100644 --- a/src/library/CMakeLists.txt +++ b/src/library/CMakeLists.txt @@ -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}) diff --git a/src/library/equivalence_manager.cpp b/src/library/equivalence_manager.cpp new file mode 100644 index 0000000000..76121291da --- /dev/null +++ b/src/library/equivalence_manager.cpp @@ -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 +#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 extract_arg_types_core(environment const & env, name const & f, buffer & 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 & 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> refl_table; + typedef name_map> subst_table; + typedef name_map> symm_table; + typedef rb_map, 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 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 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 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 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(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(cmd); + return e; + } + static optional get_fingerprint(entry const &) { + return optional(); + } +}; + +template class scoped_ext; +typedef scoped_ext 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> get_info(name_map> const & table, name const & op) { + if (auto it = table.find(op)) { + return optional>(*it); + } else { + return optional>(); + } +} + +optional> get_refl_extra_info(environment const & env, name const & op) { + return get_info(eqv_ext::get_state(env).m_refl_table, op); +} +optional> get_subst_extra_info(environment const & env, name const & op) { + return get_info(eqv_ext::get_state(env).m_subst_table, op); +} +optional> get_symm_extra_info(environment const & env, name const & op) { + return get_info(eqv_ext::get_state(env).m_symm_table, op); +} + +optional> 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>(*it); + } else { + return optional>(); + } +} + +optional get_refl_info(environment const & env, name const & op) { + if (auto it = get_refl_extra_info(env, op)) + return optional(std::get<0>(*it)); + else + return optional(); +} + +optional get_symm_info(environment const & env, name const & op) { + if (auto it = get_symm_extra_info(env, op)) + return optional(std::get<0>(*it)); + else + return optional(); +} + +optional get_trans_info(environment const & env, name const & op) { + if (auto it = get_trans_extra_info(env, op, op)) + return optional(std::get<0>(*it)); + else + return optional(); +} + +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; +} +} diff --git a/src/library/equivalence_manager.h b/src/library/equivalence_manager.h new file mode 100644 index 0000000000..4552d33e78 --- /dev/null +++ b/src/library/equivalence_manager.h @@ -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> get_refl_extra_info(environment const & env, name const & op); +optional> get_subst_extra_info(environment const & env, name const & op); +optional> get_symm_extra_info(environment const & env, name const & op); +optional> get_trans_extra_info(environment const & env, name const & op1, name const & op2); +optional get_refl_info(environment const & env, name const & op); +optional get_symm_info(environment const & env, name const & op); +optional get_trans_info(environment const & env, name const & op); +void initialize_equivalence_manager(); +void finalize_equivalence_manager(); +} diff --git a/src/library/init_module.cpp b/src/library/init_module.cpp index 5b67d37136..c27768a73a 100644 --- a/src/library/init_module.cpp +++ b/src/library/init_module.cpp @@ -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(); diff --git a/tests/lean/calc1.lean b/tests/lean/calc1.lean index 28a3986f80..521e440f17 100644 --- a/tests/lean/calc1.lean +++ b/tests/lean/calc1.lean @@ -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 diff --git a/tests/lean/interactive/eq2.lean b/tests/lean/interactive/eq2.lean index 282bbfeb97..6d969814ec 100644 --- a/tests/lean/interactive/eq2.lean +++ b/tests/lean/interactive/eq2.lean @@ -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 diff --git a/tests/lean/run/calc.lean b/tests/lean/run/calc.lean index 0a312687d2..d7760aca85 100644 --- a/tests/lean/run/calc.lean +++ b/tests/lean/run/calc.lean @@ -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