-
Notifications
You must be signed in to change notification settings - Fork 80
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Merged by Bors] - fix(frontends/lean/elaborator): elaborate structure instances left-to-right #282
Conversation
@@ -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 *, |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
The default value is less reduced now.
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⟩⟩, |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Same issue as in list.monad
, and I was in a casual golfing mood.
I tried building mathlib and found something. This change has a somewhat unintended side-effect. For example, the ∀ a : α, @has_le.le (has_le.mk α (partial_order.le α)) a a Unfortunately you can't |
Does this fix #214? |
@kckennylau This would indeed fix #214 (modulo the |
This reverts commit 20a5f94.
So, I've ported mathlib and the diff isn't too large: https://github.com/leanprover-community/mathlib/compare/si The workaround for the @[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 @[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 } |
bors merge |
Pull request successfully merged into master. Build succeeded: |
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>
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>
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>
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>
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>
Fixes #197 and #214.