Zulip Chat Archive

Stream: general

Topic: cc failure


view this post on Zulip Reid Barton (May 16 2018 at 17:03):

Is this a bug?

example {α β : Type} (x1 x2 : α) (y : β) (h : x1 = x2)
  {p : β  Prop} (hp : p y) :
   y', p y'  (x2, y') = (x1, y) :=
begin
  existsi _, split, exact hp, -- ⊢ (x2, y) = (x1, y)
  cc                          -- cc tactic failed
end

view this post on Zulip Reid Barton (May 16 2018 at 17:06):

(I know the lemma and proof are strange, this is a minimized version of some real code)

view this post on Zulip Reid Barton (May 16 2018 at 17:08):

It seems that cc doesn't recognize that the ys are equal because one of them was created by substituting for a metavariable, or something.

view this post on Zulip Kenny Lau (May 16 2018 at 17:09):

subst h

view this post on Zulip Reid Barton (May 16 2018 at 17:10):

I observed this a few days ago as well, but in a setting which was too hard to minimize.

view this post on Zulip Kenny Lau (May 16 2018 at 17:11):

try set_option pp.all true

view this post on Zulip Chris Hughes (May 16 2018 at 17:11):

subst h

rw h

view this post on Zulip Reid Barton (May 16 2018 at 17:11):

stop!

view this post on Zulip Chris Hughes (May 16 2018 at 17:13):

this works

example {α β : Type} (x1 x2 : α) (y : β) (h : x1 = x2)
  {p : β  Prop} (hp : p y) :
   y', p y'  (x2, y') = (x1, y) := ⟨_, hp, begin
    cc,
  end

So it seems like a bug.

view this post on Zulip Kenny Lau (May 16 2018 at 17:13):

by cc

view this post on Zulip Reid Barton (May 16 2018 at 17:13):

Yeah, changing cc to exact by cc works also

view this post on Zulip Reid Barton (May 16 2018 at 17:14):

(And also in my real code.)

view this post on Zulip Chris Hughes (May 16 2018 at 17:14):

It's to do with the metavariable

example {α β : Type} (x1 x2 : α) (y : β) (h : x1 = x2)
  {p : β  Prop} (hp : p y) :
   y', p y'  (x2, y') = (x1, y) :=
begin
  existsi y, split, exact hp, -- ⊢ (x2, y) = (x1, y)
  cc                          -- cc tactic failed
end

works

view this post on Zulip Kenny Lau (May 16 2018 at 17:14):

I thought exact hp unified the metavariable

view this post on Zulip Reid Barton (May 16 2018 at 17:14):

It does. That's what makes this so confusing.

view this post on Zulip Reid Barton (May 16 2018 at 17:15):

The displayed proof state is exactly the same whether you write existsi _ or existsi y

view this post on Zulip Reid Barton (May 16 2018 at 17:16):

but cc only works in the second case


Last updated: May 08 2021 at 19:11 UTC