I 'd like to know if there is a good way to do forward reasoning in tactics mode, maybe if there is a tactics language written for that or whether metacoq can be used for that purpose. Also whether what looks to me like a nice piece of work -Mtac2- can be used for forward reasoning, as well as the advertised backwards monadic reasoning.
why wouldn't tactics like
pose proof, SSReflect's
have, etc., count as forward reasoning?
They do. I'm not sure what SSReflect is yet. More or less what is it?
I guess forward reasoning is just manipulating the context instead of the goal...so any tactic language can be used? Is that correct?
yes, that's my intuition at least: forward reasoning occurs if you add or change something in context. Here is SSReflect's
have tactic, which is probably one of the most sophisticated ways to do this in Coq (it can also change the goal): https://coq.inria.fr/refman/proof-engine/ssreflect-proof-language.html#coq:tacn.have
That's where I'll start then Ltac+SSReflect. Thanks. The messiness of 'a few' compatibility issues with Ltac seems to be no big cost as Ltac seems messy enough already! And from what you've said I guess after that I could eventually start on Mtac2 and write my own forward tactics in an SSReflect style in Mtac2. Whilst this is down road for me, it would be useful to know if Mtac 2 is sufficient for that (in the most generic sense of doing whatever I want with a context), or whether I need to go the extra mile and learn MetaCoq? I think the latter would be hard for a newcomer to Coq - so just in terms of time commitments and expectations I'd like to know ahead of time.
If a newcomer asks about "how do I do forward reasoning" I'd typically recommend plain ltac or ltac + ssreflect; the other options seem overkill for that goal
yes, plain old
assert works well for a lot of stuff. The reference to
have is just to illustrate that there are options.
... conversely, the other options can make sense if you have _additional_ goals — say, develop fancy proof automation
but to me "forward proof" is a way to write _manual_ proof steps :-)
My first thought of a forward reasoning tactic would be
apply M in x, and similar tactics containing
my preference is using
have over specialize, especially if you (like me) don't know exactly what you are doing, the idea is that specialize discards the old hypothesis, while have preserves the old hypothesis.
so you would usually do:
have := M x
You can also
Last updated: Feb 06 2023 at 12:04 UTC