## Stream: new members

### Topic: have giving error

#### Thomas Browning (May 26 2020 at 21:11):

the expression

have h : a * b = a * b → a = a,


introduces a weird forall, and the expression

have h' : a * b = a * b → a * b = a * b,


gives an error at the third multiplication symbol. Why is this happening and how can it be avoided?

#### Johan Commelin (May 26 2020 at 21:13):

What's the error?

#### Johan Commelin (May 26 2020 at 21:14):

I don't know how *, → and = bind... but I guess not the way we're hoping (-;

#### Thomas Browning (May 26 2020 at 21:14):

parentheses don't seem to change anything:

example (a b : ℕ) : a * b = a * b → a * b = a * b :=
begin
have h : a * b = a * b → a = a,
have h' : (((a * b) = (a * b)) → ((a * b) = (a * b))),
end


this still gives the error
type mismatch at application
has_mul.mul a
term
a
has type
a * b = a * b : Prop
but is expected to have type
?m_1 : Type ?

Aha, the "a" bug

#### Patrick Lutz (May 26 2020 at 21:16):

For reference,

  let a := 0,
let b := 1,
have h : ((a = b) →  (a = a)),


gives a state with the goal

a : ℕ := 0,
b : ℕ := 1
⊢ ∀ (a_1 : a = b), a_1 = a_1


#### Patrick Massot (May 26 2020 at 21:17):

The a bug! Long time no see

#### Johan Commelin (May 26 2020 at 21:17):

example (c b : ℕ) : (c * b = c * b) → (c * b = c * b) :=
begin
have h : (c * b = c * b) → c = c,
have h' : (((c * b) = (c * b)) → ((c * b) = (c * b))),
end


#### Reid Barton (May 26 2020 at 21:18):

For some reason, only in tactic mode, have h : a * b = a * b → a = a means have h : \Pi (a : a * b = a * b), a = a

#### Patrick Lutz (May 26 2020 at 21:18):

this is pretty wild

Gaabrieeeel?

#### Reid Barton (May 26 2020 at 21:18):

I've been meaning to change the implicit H to _H or something, but I totally forgot about this one.

#### Johan Commelin (May 26 2020 at 21:19):

I think it should be renamed to \Pi (a_bug : etc...)

#### Pedro Minicz (May 26 2020 at 21:19):

Wow, so is this only a problem because a is the default name? Funny (and horrifying).

#### Thomas Browning (May 26 2020 at 21:20):

so I guess I'll just do

rename a c


weird

#### Bryan Gin-ge Chen (May 26 2020 at 21:21):

Is it the same as lean#130?

#### Patrick Massot (May 26 2020 at 21:21):

This won't let you prove false however

#### Patrick Massot (May 26 2020 at 21:21):

I'm writing this because Pedro comes from Coq where bugs usually let you prove false.

#### Reid Barton (May 26 2020 at 21:21):

Does this variable even get a name at all when in term mode?

#### Patrick Massot (May 26 2020 at 21:22):

Soon Sebastian will come here and tell us everything about hygiene

#### Kevin Buzzard (May 26 2020 at 23:27):

Bryan Gin-ge Chen said:

Is it the same as lean#130?

No, that's the H bug :-) The a bug is #1285

#### Bryan Gin-ge Chen (May 26 2020 at 23:59):

:joy: I meant "the same" in a very loose sense, of course. Definitely much looser than "the mathematician's equals".

#### Yury G. Kudryashov (May 27 2020 at 00:45):

Coq adds some numeric suffix to the name of the new variable in cases like these two.

#### Patrick Stevens (May 27 2020 at 03:31):

Amusingly, if I recall correctly, Agda sometimes disambiguates by incrementing numbers at the end of identifiers - can lead to confusion with terms called a=1 and that kind of thing

#### Mario Carneiro (May 27 2020 at 04:03):

Lean does this too, but the sequence is something like a a_2 a_3 ...

#### Yury G. Kudryashov (May 27 2020 at 04:06):

AFAIR coq takes the next unused name from the sequence.

#### Yury G. Kudryashov (May 27 2020 at 04:06):

It has something like mk_fresh_name prefix (not sure about name).

#### Mario Carneiro (May 27 2020 at 04:07):

I think lean also has something like this, but it isn't used in all circumstances, and this is one of them

Last updated: May 11 2021 at 00:31 UTC