Pattern matching in proof

Stream: general

[Mathias Schack Rabing]

Hi in coq you can in proofs do the following in proofs:
Capture.PNG
Which says if "NearlyRB (if ?k ...)" is the goal then use the tactic "destruct k"
and if there is a hypothesis "H" for "RB ?t Red ?n" and the goal is "RB ?t Black ?n" then do "..." tactic.
Do you know if there are anything equivalent in lean?

[Eric Rodriguez]

do you maybe mean the cases tactic? if you can give a Lean example it'd be nice

[Sebastian Ullrich]

There is no real Ltac equivalent in Lean. Lean tactic metaprogramming is much more low-level and explicit than in Coq.

[Henrik Böving]

Eric Rodriguez said:

do you maybe mean the cases tactic? if you can give a Lean example it'd be nice

No he means something different, what this block does is allow you to inspect your assumptions and proof goal and based on those make a choice for the next tactic you want to apply. This allows you to e.g. write a repeat block with a tactic inside that dynamically changes behaviour depending on how the proof goal looks. But as Sebastian said what Mathias is asking for is rather far away from what's possible right now. Someone would basically have to implement a match statement compiler for tactic mode

[Eric Wieser]

Isn't this basically pattern matching on expr, which we do have?

[Henrik Böving]

It's a bit more elaborate than that:

• it can be just used inline in tactic mode
• match on the high level syntax, for example in the image you can see him doing an if but it can do any sort of syntax
• search for hypothesis like in the second arm, the second arm says if there is a hypothesis H of the desired typed and (after the |-) we have the desired goal then apply...

[Henrik Böving]

and probably a ton of other things I dont know, I just know this syntax from reading and translating CPDT to Lean

[Henrik Böving]

It's sort of an inline tactic macro declaration and in addition integrated to tactic mode with the search for hypothesis stuff etc.

[Henrik Böving]

But yes in the end it does boil down to matching on expr's etc. But as Sebastian said that's much more low level, the difference is mostly in the convenience of usage, not that we cannot do it.