[Merged by Bors] - fix(frontends/lean/elaborator): elaborate structure instances left-to-right #282

gebner · 2020-05-27T15:12:36Z

Fixes #197 and #214.

…-right

gebner · 2020-05-27T15:13:18Z

library/init/data/list/instances.lean

@@ -16,10 +16,10 @@ instance : monad list :=
 { pure := @list.ret, map := @list.map, bind := @list.bind }

 instance : is_lawful_monad list :=
-{ bind_pure_comp_eq_map := by intros; induction x; simp [*, (<$>), pure] at *,
+{ bind_pure_comp_eq_map := by intros; induction x; simp [*, (<$>), (>>=), pure] at *,


The default value is less reduced now.

gebner · 2020-05-27T15:13:49Z

library/init/data/set.lean

-    exact propext ⟨λ ⟨a, ⟨h₁, h₂⟩⟩, ⟨g a, ⟨⟨a, ⟨h₁, rfl⟩⟩, h₂⟩⟩,
-                   λ ⟨b, ⟨⟨a, ⟨h₁, h₂⟩⟩, h₃⟩⟩, ⟨a, ⟨h₁, h₂.symm ▸ h₃⟩⟩⟩
-  end }
+{ id_map := λ _ s, funext $ λ b, propext ⟨λ ⟨_, sb, rfl⟩, sb, λ sb, ⟨_, sb, rfl⟩⟩,


Same issue as in list.monad, and I was in a casual golfing mood.

tests/lean/t10.lean.expected.out

gebner · 2020-05-27T18:01:28Z

I tried building mathlib and found something. This change has a somewhat unintended side-effect.

For example, the le_refl goal now looks like this:

∀ a : α, @has_le.le (has_le.mk α (partial_order.le α)) a a

Unfortunately you can't rw le_refl here because the unifier fails to unify the two (at reducible transparency). This is because projections of constructors are reduced somewhat eagerly and then you have a useless partial_order.le.

kckennylau · 2020-05-28T07:11:58Z

Does this fix #214?

gebner · 2020-05-28T08:19:39Z

@kckennylau This would indeed fix #214 (modulo the has_mul.mk issue I mentioned in the other comment).

This reverts commit 20a5f94.

gebner · 2020-05-28T13:58:02Z

So, I've ported mathlib and the diff isn't too large: https://github.com/leanprover-community/mathlib/compare/si

The workaround for the has_mul.mk issue above is as follows. Consider for example euclidean_domain.integral_domain. This would break:

@[priority 70] -- see Note [lower instance priority]
instance (α : Type*) [e : euclidean_domain α] : integral_domain α :=
by haveI := classical.dec_eq α; exact
{ eq_zero_or_eq_zero_of_mul_eq_zero :=
    λ a b (h : a * b = 0), or_iff_not_and_not.2 $ λ h0 : a ≠ 0 ∧ b ≠ 0,
      h0.1 $ by rw [← mul_div_cancel a h0.2, h, zero_div],
  ..e }

The reason is that the ..e inserts a reference to euclidean_domain.add, which should never be referenced. The workaround is very easy: just specify mul := (*) (etc.) manually:

@[priority 70] -- see Note [lower instance priority]
instance (α : Type*) [e : euclidean_domain α] : integral_domain α :=
by haveI := classical.dec_eq α; exact
{ eq_zero_or_eq_zero_of_mul_eq_zero := by exact
    λ a b h, (or_iff_not_and_not.2 $ λ h0,
      h0.1 $ by rw [← mul_div_cancel a h0.2, h, zero_div]),
  zero := 0, add := (+), mul := (*), ..e }

gebner · 2020-05-28T15:07:05Z

bors merge

…-right (#282) Fixes #197 and #214.

bors · 2020-05-28T15:34:47Z

Pull request successfully merged into master.

Build succeeded:

@eq

The main effect for mathlib comes from leanprover-community/lean#282, which changes the elaboration strategy for structure instance literals (`{ foo := 42 }`). There are two points where we need to pay attention: 1. Avoid sourcing (`{ ..e }` where e.g. `e : euclidean_domain α`) for fields like `add`, `mul`, `zero`, etc. Instead write `{ add := (+), mul := (*), zero := 0, ..e }`. The reason is that `{ ..e }` is equivalent to `{ mul := euclidean_domain.mul, ..e }`. And `euclidean_domain.mul` should never be mentioned. I'm not completely sure if this issue remains visible once the structure literal has been elaborated, but this hasn't changed since 3.14. For now, my advice is: if you get weird errors like "cannot unify `a * b` and `?m_1 * ?m_2` in a structure literal, add `mul := (*)`. 2. `refine { le := (≤), .. }; simp` is slower. This is because references to `(≤)` are no longer reduced to `le` in the subgoals. If a subgoal like `a ≤ b → b ≤ a → a = b` was stated for preorders (because `partial_order` extends `preorder`), then the `(≤)` will contain a `preorder` subterm. This subterm also contains other subgoals (proofs of reflexivity and transitivity). Therefore the goals are larger than you might expect: ``` ∀ (a b : α), @has_le.le.{u} α (@preorder.to_has_le.{u} α (@preorder.mk.{u} α le (@lattice.lt._default.{u} α le) (@conditionally_complete_lattice.copy._aux_1.{u} α c le eq_le sup eq_sup inf eq_inf Sup eq_Sup Inf eq_Inf) (@conditionally_complete_lattice.copy._aux_2.{u} α c le eq_le sup eq_sup inf eq_inf Sup eq_Sup Inf eq_Inf) (λ (a b : α), iff.refl (@has_lt.lt.{u} α (@has_lt.mk.{u} α (@lattice.lt._default.{u} α le)) a b)))) a b → @has_le.le.{u} α (@preorder.to_has_le.{u} α (@preorder.mk.{u} α le (@lattice.lt._default.{u} α le) (@conditionally_complete_lattice.copy._aux_1.{u} α c le eq_le sup eq_sup inf eq_inf Sup eq_Sup Inf eq_Inf) (@conditionally_complete_lattice.copy._aux_2.{u} α c le eq_le sup eq_sup inf eq_inf Sup eq_Sup Inf eq_Inf) (λ (a b : α), iff.refl (@has_lt.lt.{u} α (@has_lt.mk.{u} α (@lattice.lt._default.{u} α le)) a b)))) b a → @eq.{u+1} α a b ``` Advice: in cases such as this, try `refine { le := (≤), .. }; abstract { simp }` to reduce the size of the (dependent) subgoals. Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com> Co-authored-by: Scott Morrison <scott@tqft.net> Co-authored-by: E.W.Ayers <E.W.Ayers@maths.cam.ac.uk>

@eq

The main effect for mathlib comes from leanprover-community/lean#282, which changes the elaboration strategy for structure instance literals (`{ foo := 42 }`). There are two points where we need to pay attention: 1. Avoid sourcing (`{ ..e }` where e.g. `e : euclidean_domain α`) for fields like `add`, `mul`, `zero`, etc. Instead write `{ add := (+), mul := (*), zero := 0, ..e }`. The reason is that `{ ..e }` is equivalent to `{ mul := euclidean_domain.mul, ..e }`. And `euclidean_domain.mul` should never be mentioned. I'm not completely sure if this issue remains visible once the structure literal has been elaborated, but this hasn't changed since 3.14. For now, my advice is: if you get weird errors like "cannot unify `a * b` and `?m_1 * ?m_2` in a structure literal, add `mul := (*)`. 2. `refine { le := (≤), .. }; simp` is slower. This is because references to `(≤)` are no longer reduced to `le` in the subgoals. If a subgoal like `a ≤ b → b ≤ a → a = b` was stated for preorders (because `partial_order` extends `preorder`), then the `(≤)` will contain a `preorder` subterm. This subterm also contains other subgoals (proofs of reflexivity and transitivity). Therefore the goals are larger than you might expect: ``` ∀ (a b : α), @has_le.le.{u} α (@preorder.to_has_le.{u} α (@preorder.mk.{u} α le (@lattice.lt._default.{u} α le) (@conditionally_complete_lattice.copy._aux_1.{u} α c le eq_le sup eq_sup inf eq_inf Sup eq_Sup Inf eq_Inf) (@conditionally_complete_lattice.copy._aux_2.{u} α c le eq_le sup eq_sup inf eq_inf Sup eq_Sup Inf eq_Inf) (λ (a b : α), iff.refl (@has_lt.lt.{u} α (@has_lt.mk.{u} α (@lattice.lt._default.{u} α le)) a b)))) a b → @has_le.le.{u} α (@preorder.to_has_le.{u} α (@preorder.mk.{u} α le (@lattice.lt._default.{u} α le) (@conditionally_complete_lattice.copy._aux_1.{u} α c le eq_le sup eq_sup inf eq_inf Sup eq_Sup Inf eq_Inf) (@conditionally_complete_lattice.copy._aux_2.{u} α c le eq_le sup eq_sup inf eq_inf Sup eq_Sup Inf eq_Inf) (λ (a b : α), iff.refl (@has_lt.lt.{u} α (@has_lt.mk.{u} α (@lattice.lt._default.{u} α le)) a b)))) b a → @eq.{u+1} α a b ``` Advice: in cases such as this, try `refine { le := (≤), .. }; abstract { simp }` to reduce the size of the (dependent) subgoals. Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com> Co-authored-by: Scott Morrison <scott@tqft.net> Co-authored-by: E.W.Ayers <E.W.Ayers@maths.cam.ac.uk>

@eq

The main effect for mathlib comes from leanprover-community/lean#282, which changes the elaboration strategy for structure instance literals (`{ foo := 42 }`). There are two points where we need to pay attention: 1. Avoid sourcing (`{ ..e }` where e.g. `e : euclidean_domain α`) for fields like `add`, `mul`, `zero`, etc. Instead write `{ add := (+), mul := (*), zero := 0, ..e }`. The reason is that `{ ..e }` is equivalent to `{ mul := euclidean_domain.mul, ..e }`. And `euclidean_domain.mul` should never be mentioned. I'm not completely sure if this issue remains visible once the structure literal has been elaborated, but this hasn't changed since 3.14. For now, my advice is: if you get weird errors like "cannot unify `a * b` and `?m_1 * ?m_2` in a structure literal, add `mul := (*)`. 2. `refine { le := (≤), .. }; simp` is slower. This is because references to `(≤)` are no longer reduced to `le` in the subgoals. If a subgoal like `a ≤ b → b ≤ a → a = b` was stated for preorders (because `partial_order` extends `preorder`), then the `(≤)` will contain a `preorder` subterm. This subterm also contains other subgoals (proofs of reflexivity and transitivity). Therefore the goals are larger than you might expect: ``` ∀ (a b : α), @has_le.le.{u} α (@preorder.to_has_le.{u} α (@preorder.mk.{u} α le (@lattice.lt._default.{u} α le) (@conditionally_complete_lattice.copy._aux_1.{u} α c le eq_le sup eq_sup inf eq_inf Sup eq_Sup Inf eq_Inf) (@conditionally_complete_lattice.copy._aux_2.{u} α c le eq_le sup eq_sup inf eq_inf Sup eq_Sup Inf eq_Inf) (λ (a b : α), iff.refl (@has_lt.lt.{u} α (@has_lt.mk.{u} α (@lattice.lt._default.{u} α le)) a b)))) a b → @has_le.le.{u} α (@preorder.to_has_le.{u} α (@preorder.mk.{u} α le (@lattice.lt._default.{u} α le) (@conditionally_complete_lattice.copy._aux_1.{u} α c le eq_le sup eq_sup inf eq_inf Sup eq_Sup Inf eq_Inf) (@conditionally_complete_lattice.copy._aux_2.{u} α c le eq_le sup eq_sup inf eq_inf Sup eq_Sup Inf eq_Inf) (λ (a b : α), iff.refl (@has_lt.lt.{u} α (@has_lt.mk.{u} α (@lattice.lt._default.{u} α le)) a b)))) b a → @eq.{u+1} α a b ``` Advice: in cases such as this, try `refine { le := (≤), .. }; abstract { simp }` to reduce the size of the (dependent) subgoals. Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com> Co-authored-by: Scott Morrison <scott@tqft.net> Co-authored-by: E.W.Ayers <E.W.Ayers@maths.cam.ac.uk>

@eq

The main effect for mathlib comes from leanprover-community/lean#282, which changes the elaboration strategy for structure instance literals (`{ foo := 42 }`). There are two points where we need to pay attention: 1. Avoid sourcing (`{ ..e }` where e.g. `e : euclidean_domain α`) for fields like `add`, `mul`, `zero`, etc. Instead write `{ add := (+), mul := (*), zero := 0, ..e }`. The reason is that `{ ..e }` is equivalent to `{ mul := euclidean_domain.mul, ..e }`. And `euclidean_domain.mul` should never be mentioned. I'm not completely sure if this issue remains visible once the structure literal has been elaborated, but this hasn't changed since 3.14. For now, my advice is: if you get weird errors like "cannot unify `a * b` and `?m_1 * ?m_2` in a structure literal, add `mul := (*)`. 2. `refine { le := (≤), .. }; simp` is slower. This is because references to `(≤)` are no longer reduced to `le` in the subgoals. If a subgoal like `a ≤ b → b ≤ a → a = b` was stated for preorders (because `partial_order` extends `preorder`), then the `(≤)` will contain a `preorder` subterm. This subterm also contains other subgoals (proofs of reflexivity and transitivity). Therefore the goals are larger than you might expect: ``` ∀ (a b : α), @has_le.le.{u} α (@preorder.to_has_le.{u} α (@preorder.mk.{u} α le (@lattice.lt._default.{u} α le) (@conditionally_complete_lattice.copy._aux_1.{u} α c le eq_le sup eq_sup inf eq_inf Sup eq_Sup Inf eq_Inf) (@conditionally_complete_lattice.copy._aux_2.{u} α c le eq_le sup eq_sup inf eq_inf Sup eq_Sup Inf eq_Inf) (λ (a b : α), iff.refl (@has_lt.lt.{u} α (@has_lt.mk.{u} α (@lattice.lt._default.{u} α le)) a b)))) a b → @has_le.le.{u} α (@preorder.to_has_le.{u} α (@preorder.mk.{u} α le (@lattice.lt._default.{u} α le) (@conditionally_complete_lattice.copy._aux_1.{u} α c le eq_le sup eq_sup inf eq_inf Sup eq_Sup Inf eq_Inf) (@conditionally_complete_lattice.copy._aux_2.{u} α c le eq_le sup eq_sup inf eq_inf Sup eq_Sup Inf eq_Inf) (λ (a b : α), iff.refl (@has_lt.lt.{u} α (@has_lt.mk.{u} α (@lattice.lt._default.{u} α le)) a b)))) b a → @eq.{u+1} α a b ``` Advice: in cases such as this, try `refine { le := (≤), .. }; abstract { simp }` to reduce the size of the (dependent) subgoals. [Zulip thread](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Lean.203.2E15.2E0). Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com> Co-authored-by: Scott Morrison <scott@tqft.net> Co-authored-by: E.W.Ayers <E.W.Ayers@maths.cam.ac.uk> Co-authored-by: Chris Hughes <chrishughes24@gmail.com>

@eq

The main effect for mathlib comes from leanprover-community/lean#282, which changes the elaboration strategy for structure instance literals (`{ foo := 42 }`). There are two points where we need to pay attention: 1. Avoid sourcing (`{ ..e }` where e.g. `e : euclidean_domain α`) for fields like `add`, `mul`, `zero`, etc. Instead write `{ add := (+), mul := (*), zero := 0, ..e }`. The reason is that `{ ..e }` is equivalent to `{ mul := euclidean_domain.mul, ..e }`. And `euclidean_domain.mul` should never be mentioned. I'm not completely sure if this issue remains visible once the structure literal has been elaborated, but this hasn't changed since 3.14. For now, my advice is: if you get weird errors like "cannot unify `a * b` and `?m_1 * ?m_2` in a structure literal, add `mul := (*)`. 2. `refine { le := (≤), .. }; simp` is slower. This is because references to `(≤)` are no longer reduced to `le` in the subgoals. If a subgoal like `a ≤ b → b ≤ a → a = b` was stated for preorders (because `partial_order` extends `preorder`), then the `(≤)` will contain a `preorder` subterm. This subterm also contains other subgoals (proofs of reflexivity and transitivity). Therefore the goals are larger than you might expect: ``` ∀ (a b : α), @has_le.le.{u} α (@preorder.to_has_le.{u} α (@preorder.mk.{u} α le (@lattice.lt._default.{u} α le) (@conditionally_complete_lattice.copy._aux_1.{u} α c le eq_le sup eq_sup inf eq_inf Sup eq_Sup Inf eq_Inf) (@conditionally_complete_lattice.copy._aux_2.{u} α c le eq_le sup eq_sup inf eq_inf Sup eq_Sup Inf eq_Inf) (λ (a b : α), iff.refl (@has_lt.lt.{u} α (@has_lt.mk.{u} α (@lattice.lt._default.{u} α le)) a b)))) a b → @has_le.le.{u} α (@preorder.to_has_le.{u} α (@preorder.mk.{u} α le (@lattice.lt._default.{u} α le) (@conditionally_complete_lattice.copy._aux_1.{u} α c le eq_le sup eq_sup inf eq_inf Sup eq_Sup Inf eq_Inf) (@conditionally_complete_lattice.copy._aux_2.{u} α c le eq_le sup eq_sup inf eq_inf Sup eq_Sup Inf eq_Inf) (λ (a b : α), iff.refl (@has_lt.lt.{u} α (@has_lt.mk.{u} α (@lattice.lt._default.{u} α le)) a b)))) b a → @eq.{u+1} α a b ``` Advice: in cases such as this, try `refine { le := (≤), .. }; abstract { simp }` to reduce the size of the (dependent) subgoals. [Zulip thread](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Lean.203.2E15.2E0). Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com> Co-authored-by: Scott Morrison <scott@tqft.net> Co-authored-by: E.W.Ayers <E.W.Ayers@maths.cam.ac.uk> Co-authored-by: Chris Hughes <chrishughes24@gmail.com>

gebner added 2 commits May 27, 2020 17:10

fix(frontends/lean/elaborator): elaborate structure instances left-to…

6c84efd

…-right

Add test.

f9b7307

gebner commented May 27, 2020

View reviewed changes

Style. :-P

3825e41

semorrison mentioned this pull request May 28, 2020

[Merged by Bors] - feat(number_theory/lucas_lehmer): prime (2^127 - 1) leanprover-community/mathlib#2842

Closed

gebner added 3 commits May 28, 2020 13:46

One more test.

20a5f94

Remove field mvars on backtracking.

b918551

Revert "One more test."

3c9e317

This reverts commit 20a5f94.

gebner added 2 commits May 28, 2020 17:02

Merge remote-tracking branch 'origin/master' into structinst

2291974

Fix tests.

32a6652

bors bot pushed a commit that referenced this pull request May 28, 2020

fix(frontends/lean/elaborator): elaborate structure instances left-to…

e06d6f1

…-right (#282) Fixes #197 and #214.

bors bot changed the title ~~fix(frontends/lean/elaborator): elaborate structure instances left-to-right~~ [Merged by Bors] - fix(frontends/lean/elaborator): elaborate structure instances left-to-right May 28, 2020

bors bot closed this May 28, 2020

bors bot deleted the structinst branch May 28, 2020 15:34

gebner mentioned this pull request May 29, 2020

[Merged by Bors] - chore(*): update to lean 3.15.0 leanprover-community/mathlib#2851

Closed

gebner mentioned this pull request Jun 2, 2020

Over-elaboration when using Type* in definitions #214

Closed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - fix(frontends/lean/elaborator): elaborate structure instances left-to-right #282

[Merged by Bors] - fix(frontends/lean/elaborator): elaborate structure instances left-to-right #282

gebner commented May 27, 2020 •

edited

Loading

gebner May 27, 2020

gebner May 27, 2020

gebner commented May 27, 2020

kckennylau commented May 28, 2020

gebner commented May 28, 2020

gebner commented May 28, 2020

gebner commented May 28, 2020

bors bot commented May 28, 2020

[Merged by Bors] - fix(frontends/lean/elaborator): elaborate structure instances left-to-right #282

[Merged by Bors] - fix(frontends/lean/elaborator): elaborate structure instances left-to-right #282

Conversation

gebner commented May 27, 2020 • edited Loading

gebner May 27, 2020

Choose a reason for hiding this comment

gebner May 27, 2020

Choose a reason for hiding this comment

gebner commented May 27, 2020

kckennylau commented May 28, 2020

gebner commented May 28, 2020

gebner commented May 28, 2020

gebner commented May 28, 2020

bors bot commented May 28, 2020

gebner commented May 27, 2020 •

edited

Loading