Stream: general

Topic: cc failure

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


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)

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.

Kenny Lau (May 16 2018 at 17:09):

subst h

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.

Kenny Lau (May 16 2018 at 17:11):

try set_option pp.all true

Chris Hughes (May 16 2018 at 17:11):

subst h

rw h

stop!

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.

Kenny Lau (May 16 2018 at 17:13):

by cc

Reid Barton (May 16 2018 at 17:13):

Yeah, changing cc to exact by cc works also

Reid Barton (May 16 2018 at 17:14):

(And also in my real code.)

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

Kenny Lau (May 16 2018 at 17:14):

I thought exact hp unified the metavariable

Reid Barton (May 16 2018 at 17:14):

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

Reid Barton (May 16 2018 at 17:15):

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

Reid Barton (May 16 2018 at 17:16):

but cc only works in the second case

Last updated: Aug 03 2023 at 10:10 UTC