Carrying over hypothesis

Stream: new members

[Daan van Gent]

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?

[Reid Barton]

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

[Daan van Gent]

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?

[Anatole Dedecker]

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

[Daan van Gent]

Anatole Dedecker said:

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

That changes nothing as far as I can tell.

[Jalex Stark]

how do you expect lean to do the inference?

[Daan van Gent]

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?

[Kenny Lau]

only classes go to the typeclass inference system

[Kenny Lau]

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

[Kenny Lau]

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

[Kenny Lau]

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

[Mario Carneiro]

what? This is silly

[Daan van Gent]

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

[Mario Carneiro]

You could say the same thing about any term at all

[Kevin Buzzard]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Daan van Gent]

(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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Daan van Gent]

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.

[Jalex Stark]

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

[Daan van Gent]

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.

[Jalex Stark]

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