calc mode inside `conv`?

Stream: general

[Scott Morrison]

It would be really useful to be able to use calc inside a conv block, but this currently fails with unknown declaration 'conv.interactive.refine'.

Anyone either want to do this, or could summarise what would be involved to make this work?

[Gabriel Ebner]

Ah, I think this is still fallout from the change where @Johan Commelin modified the tactic-mode calc block so that it uses refine instead of exact.

[Gabriel Ebner]

Now that I look at the lean code, it seems like there is no conv.interactive.exact either.

[Gabriel Ebner]

I think it should be enough to add a conv.interactive.refine function that takes a proof of an equality and then applies it using transitivity:

example (a b c : ℕ) : a = c :=
by conv {
to_lhs,
-- | a
exact show a = b, from sorry,
-- | b
exact show b = c, from sorry
-- | c
}

[Scott Morrison]

Great! I've been missing that anyway.