cc failure

Stream: general

[Reid Barton]

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

[Reid Barton]

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

[Reid Barton]

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.

[Kenny Lau]

subst h

[Reid Barton]

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

[Kenny Lau]

try set_option pp.all true

[Chris Hughes]

subst h

rw h

[Reid Barton]

stop!

[Chris Hughes]

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.

[Kenny Lau]

by cc

[Reid Barton]

Yeah, changing cc to exact by cc works also

[Reid Barton]

(And also in my real code.)

[Chris Hughes]

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

[Kenny Lau]

I thought exact hp unified the metavariable

[Reid Barton]

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

[Reid Barton]

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

[Reid Barton]

but cc only works in the second case