Port of Rocq's Deriving such that tactic

Stream: Program verification

[Kiran]

Hihi, just wanted to share a small little lean plugin I'd made recently, that implements Rocq's Deriving Such That mechanism in Lean: https://github.com/Gopiandcode/deriving-such-that

The idea is that you can construct a term and a proof that some property holds on that term simultaneously:

variable (k n m : nat)
derive p such that (k * n) + (k * m) = p as h := by
   instantiate ?p := k * (n + m)
   simp [p, Nat.mul_add]

#eval (p 1 2 3)
-- produces 9

(Lean doesn't seem to have tactics for instantiating MVars directly so I added one in this library)

The corresponding page on Rocq's deriving mechanism: https://coq.inria.fr/doc/V8.18.0/refman/addendum/miscellaneous-extensions.html

[Eric Wieser]

Is case p => exact k * (n + m) the same as your instantiate tactic?

[Kiran]

Ah, almost, the p is an mvar so case wouldn't work (unbound id p), so I wrote a tactic to allow instantiating mvars directly

[Timo Carlin-Burns]

Kiran Gopinathan said:

the p is an mvar so case wouldn't work (unbound id p)

I'm pretty sure case usually operates on mvars. Are you confusing it with cases? Here is some tactic documentation for case..

[Mario Carneiro]

I think Kiran is right that this syntax won't work if it's an mvar which is not a goal

[Mario Carneiro]

although that's pretty rare

[Kiran]

Mario Carneiro said:

I think Kiran is right that this syntax won't work if it's an mvar which is not a goal

Okay, so I've updated the plugin so that the mvar is added to the goals, and so that case is supported!

Thanks @Eric Wieser for the suggestion.

Actually adding the generated mvar was a little bit of a challenge and took a couple of tries, @Mario Carneiro could I ask if there was an easier way of doing this?

[Mario Carneiro]

I'm not sure what you did, the usual thing is to just call setGoals [mvar] or otherwise add it to the list of goals in some way

[Kiran]

I was adding the mvar to the list of goals, but case p would still not work and complain that the identifier was not found

[Eric Wieser]

(to be clear, I think your instantiate notation is quite nice despite the fact we have an existing spelling, similar to how we have both obtain pat := val as well as rcases val with pat)

[Kiran]

My command was expanding into a definition of the form

def ...: by
    add_to_goal $id -- (adds mvar with matching name to goals)
     exact $proof

Where $proof is a term containing the proof, maybe case-ing on id

[Kiran]

Eric Wieser said:

(to be clear, I think your instantiate notation is quite nice despite the fact we have an existing spelling, similar to how we have both obtain pat := val as well as rcases val with pat)

Mhh yes, thanks! I wanted to get rid of it though as it seems like people don't instantiate mvars directly, but now that you mention it, it might be a nice tactic by itself.

[Johan Commelin]

Could where be a tactic?

refine myLemma arg1 arg2 _ ?x arg3 ?y
where x := some longish expr
where y := some thing else

[Kyle Miller]

For that you should be able to do case x => exact some longish expr in place of where x := ...

[Johan Commelin]

Right, but I like the look of where. It is closer to what you would say informally

[Eric Wieser]

I think this is closely related to the on_sides discussion about side-goals