Robert Watson (Nov 20 2022 at 13:09): Robert Watson (Nov 20 2022 at 13:09):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.
Karl Palmskog (Nov 20 2022 at 13:22):why wouldn't tactics like assert, pose proof, SSReflect's have, etc., count as forward reasoning?
Robert Watson (Nov 20 2022 at 14:11):They do. I'm not sure what SSReflect is yet. More or less what is it?
Robert Watson (Nov 20 2022 at 15:18):I guess forward reasoning is just manipulating the context instead of the goal...so any tactic language can be used? Is that correct?
Karl Palmskog (Nov 20 2022 at 15:20):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
Robert Watson (Nov 20 2022 at 16:16):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.
Paolo Giarrusso (Nov 20 2022 at 17:18):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
Karl Palmskog (Nov 20 2022 at 19:02):yes, plain old assert works well for a lot of stuff. The reference to have is just to illustrate that there are options.
Paolo Giarrusso (Nov 20 2022 at 22:04):... conversely, the other options can make sense if you have _additional_ goals — say, develop fancy proof automation
Paolo Giarrusso (Nov 20 2022 at 22:05):but to me "forward proof" is a way to write _manual_ proof steps :-)
James Wood (Nov 21 2022 at 10:21):My first thought of a forward reasoning tactic would be apply M in x, and similar tactics containing in.
Karl Palmskog (Nov 21 2022 at 10:35):also specialize
walker (Nov 22 2022 at 08:45):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
Théo Winterhalter (Nov 22 2022 at 09:36):You can also specialize as.
Last updated: Oct 03 2023 at 04:02 UTC