structure equality

Stream: general

[Patrick Massot]

How do we prove equality of two terms whose type is a structure mixing data and Prop? I would like to prove each data holding field matches. I thought this has something to do with no_confusion but I can't get it to work.

[Patrick Massot]

Hum, it seems I can uses cases to access stuff here again.

[Chris Hughes]

structure thing := (a : ℕ) (b : ℕ)

example (a b c d : ℕ) : thing.mk a b = thing.mk c d :=
begin
   rw thing.mk.inj_eq,
end

simp also works.

[Chris Hughes]

I'm not sure what to do if you haven't done cases.

[Simon Hudon]

You can also use congr or congr'

[Chris Hughes]

What's the difference between congr and congr'?

[Simon Hudon]

congr' takes an argument like congr' 3 to ask for three iterations of congruence. congr just keeps going until it can't anymore. Often, congr goes too far

[Patrick Massot]

Thanks Chris and Simon. congr and simp do nothing, cases both sides and rw pequiv.mk.inj_eq ; cc did the trick

[Simon Hudon]

Sorry, I didn't mention, in either case, you need to cases both sides

[Patrick Massot]

Correction, after cases both sides, congr ; cc also works

[Patrick Massot]

and congr ; tauto of course

[Simon Hudon]

I'm wrapping up a round of optimization of tauto. When it works, it should be faster than cc

[Simon Hudon]

(and now, it should work more often than before)

[Patrick Massot]

Great!