have giving error

Stream: new members

[Thomas Browning]

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]

What's the error?

[Johan Commelin]

Probably adding parentheses will help

[Johan Commelin]

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

[Thomas Browning]

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 ?

[Reid Barton]

Aha, the "a" bug

[Patrick Lutz]

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]

The a bug! Long time no see

[Johan Commelin]

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]

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]

this is pretty wild

[Patrick Massot]

Gaabrieeeel?

[Reid Barton]

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

[Johan Commelin]

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

[Pedro Minicz]

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

[Thomas Browning]

so I guess I'll just do

rename a c

weird

[Bryan Gin-ge Chen]

Is it the same as lean#130?

[Patrick Massot]

This won't let you prove false however

[Patrick Massot]

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

[Reid Barton]

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

[Patrick Massot]

Soon Sebastian will come here and tell us everything about hygiene

[Kevin Buzzard]

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]

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

[Yury G. Kudryashov]

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

[Patrick Stevens]

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]

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

[Yury G. Kudryashov]

AFAIR coq takes the next unused name from the sequence.

[Yury G. Kudryashov]

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

[Mario Carneiro]

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