## Stream: new members

### Topic: Carrying over hypothesis

#### 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?

#### Reid Barton (Aug 01 2020 at 15:02):

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

#### 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?

#### Anatole Dedecker (Aug 01 2020 at 15:08):

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

#### 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.

#### Jalex Stark (Aug 01 2020 at 15:10):

how do you expect lean to do the inference?

#### 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?

#### Kenny Lau (Aug 01 2020 at 15:14):

only classes go to the typeclass inference system

#### Kenny Lau (Aug 01 2020 at 15:15):

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

#### 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


#### Kenny Lau (Aug 01 2020 at 15:16):

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

#### Mario Carneiro (Aug 01 2020 at 15:18):

what? This is silly

#### 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.

#### Mario Carneiro (Aug 01 2020 at 15:18):

You could say the same thing about any term at all

#### Kevin Buzzard (Aug 01 2020 at 15:18):

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

#### Mario Carneiro (Aug 01 2020 at 15:19):

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

#### 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

#### 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


#### 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.

#### 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


#### 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.

#### 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

#### 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.

#### 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