Zulip Chat Archive

Stream: new members

Topic: Carrying over hypothesis


view this post on Zulip Daan van Gent (Aug 01 2020 at 14:59):

I have two definitions

section
variables (α : Type*) (a b : α)
def f [h : a  b] :  := 0
def g [h : a  b] :  := f
end

This fails, because in the definition of g it does not know that a\ne b, which is required for f, even though it is a hypothesis to g. We can fix this with defining g as @f α a b h . However, in the actual context we are working in @f α a b h is very long and has to be written fairly often with different parameters. What can we do?

view this post on Zulip Reid Barton (Aug 01 2020 at 15:02):

[h : a ≠ b] is strange: is not a class

view this post on Zulip Daan van Gent (Aug 01 2020 at 15:06):

I am not sure why that is an objection? How do you suggest that we define f such that it tries to derive a\ne b from the context instead of having to explicitly give it as an argument?

view this post on Zulip Anatole Dedecker (Aug 01 2020 at 15:08):

I think you want to use {} instead of []

view this post on Zulip Daan van Gent (Aug 01 2020 at 15:10):

Anatole Dedecker said:

I think you want to use {} instead of []

That changes nothing as far as I can tell.

view this post on Zulip Jalex Stark (Aug 01 2020 at 15:10):

how do you expect lean to do the inference?

view this post on Zulip Daan van Gent (Aug 01 2020 at 15:13):

I mean it wants me to prove this:

failed to synthesize type class instance for
α : Type u_2,
a b : α,
h : a  b
 a  b

Don't you think that is rather silly?

view this post on Zulip Kenny Lau (Aug 01 2020 at 15:14):

only classes go to the typeclass inference system

view this post on Zulip Kenny Lau (Aug 01 2020 at 15:15):

maybe you can try attribute [class] ne at the beginning

view this post on Zulip Kenny Lau (Aug 01 2020 at 15:15):

i.e.:

section
attribute [class] ne
variables (α : Type*) (a b : α)
def f [h : a  b] :  := 0
def g [h : a  b] :  := f α a b
end

view this post on Zulip Kenny Lau (Aug 01 2020 at 15:16):

@Mario Carneiro so why don't we make ne a class?

view this post on Zulip Mario Carneiro (Aug 01 2020 at 15:18):

what? This is silly

view this post on Zulip Daan van Gent (Aug 01 2020 at 15:18):

I can confirm attribute [class] ne fixes the problem. I see variables was supposed to be parameters for my mwe to make sense.

view this post on Zulip Mario Carneiro (Aug 01 2020 at 15:18):

You could say the same thing about any term at all

view this post on Zulip Kevin Buzzard (Aug 01 2020 at 15:18):

only props, or else you'd get diamonds ;-)

view this post on Zulip Mario Carneiro (Aug 01 2020 at 15:19):

maybe a better choice is (h : a ≠ b . tactic.assumption)

view this post on Zulip Mario Carneiro (Aug 01 2020 at 15:21):

If you are using parameters for a and b, you may as well use it for (h : a ≠ b) too and then you won't have this problem

view this post on Zulip Daan van Gent (Aug 01 2020 at 15:33):

(h : a ≠ b . tactic.assumption) works for the mwe but somehow fails in our actual problem. That a and b are both parameters is only for the mwe. Maybe a more faithfull mwe would be

section
attribute [class] ne
parameters (α : Type*) (a : α)
def f (b:\alpha) [h : a  b] :  := 0
def g (b:\alpha) [h : a  b] :  := f b
end

view this post on Zulip Kevin Buzzard (Aug 01 2020 at 15:40):

Why not just make a and b implicit but ask for h explicitly? It seems like by far the easiest method.

view this post on Zulip Kevin Buzzard (Aug 01 2020 at 15:42):

section
variables {α : Type*} {a b : α}
def f (h : a  b) :  := 0
def g (h : a  b) :  := f h
end

view this post on Zulip Daan van Gent (Aug 01 2020 at 15:56):

Kevin Buzzard said:

Why not just make a and b implicit but ask for h explicitly? It seems like by far the easiest method.

This works quite well. It feels a bit wrong somehow, but not as wrong as making \ne a class.

view this post on Zulip Jalex Stark (Aug 01 2020 at 15:57):

I typically do things similar to kevin's suggestion. I think of it as a function that takes in "two distinct elements" as an argument, and I forget the "implementation detail" that the one argument is literally a proof of \ne

view this post on Zulip Daan van Gent (Aug 01 2020 at 16:26):

Thank you all for the interesting discussion. I still have a long way to go before I get a feel of what the canonical way to do things is in Lean.

view this post on Zulip Jalex Stark (Aug 01 2020 at 16:35):

to the extent that the canon exists, it's forged by seeing what works and what doesn't at the mathlib scale; in particular the canon is still very much evolving


Last updated: May 15 2021 at 00:39 UTC