Zulip Chat Archive

Stream: new members

Topic: have giving error


view this post on Zulip 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?

view this post on Zulip Johan Commelin (May 26 2020 at 21:13):

What's the error?

view this post on Zulip Johan Commelin (May 26 2020 at 21:13):

Probably adding parentheses will help

view this post on Zulip Johan Commelin (May 26 2020 at 21:14):

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

view this post on Zulip 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 ?

view this post on Zulip Reid Barton (May 26 2020 at 21:16):

Aha, the "a" bug

view this post on Zulip 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

view this post on Zulip Patrick Massot (May 26 2020 at 21:17):

The a bug! Long time no see

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Patrick Lutz (May 26 2020 at 21:18):

this is pretty wild

view this post on Zulip Patrick Massot (May 26 2020 at 21:18):

Gaabrieeeel?

view this post on Zulip 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.

view this post on Zulip Johan Commelin (May 26 2020 at 21:19):

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

view this post on Zulip Pedro Minicz (May 26 2020 at 21:19):

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

view this post on Zulip Thomas Browning (May 26 2020 at 21:20):

so I guess I'll just do

rename a c

weird

view this post on Zulip Bryan Gin-ge Chen (May 26 2020 at 21:21):

Is it the same as lean#130?

view this post on Zulip Patrick Massot (May 26 2020 at 21:21):

This won't let you prove false however

view this post on Zulip Patrick Massot (May 26 2020 at 21:21):

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

view this post on Zulip Reid Barton (May 26 2020 at 21:21):

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

view this post on Zulip Patrick Massot (May 26 2020 at 21:22):

Soon Sebastian will come here and tell us everything about hygiene

view this post on Zulip 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

view this post on Zulip 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".

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Mario Carneiro (May 27 2020 at 04:03):

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

view this post on Zulip Yury G. Kudryashov (May 27 2020 at 04:06):

AFAIR coq takes the next unused name from the sequence.

view this post on Zulip Yury G. Kudryashov (May 27 2020 at 04:06):

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

view this post on Zulip 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