Stream: Coq users

Topic: forward reasoning


view this post on Zulip 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.

view this post on Zulip Karl Palmskog (Nov 20 2022 at 13:22):

why wouldn't tactics like assert, pose proof, SSReflect's have, etc., count as forward reasoning?

view this post on Zulip Robert Watson (Nov 20 2022 at 14:11):

They do. I'm not sure what SSReflect is yet. More or less what is it?

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Paolo Giarrusso (Nov 20 2022 at 22:05):

but to me "forward proof" is a way to write _manual_ proof steps :-)

view this post on Zulip 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.

view this post on Zulip Karl Palmskog (Nov 21 2022 at 10:35):

also specialize

view this post on Zulip 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

view this post on Zulip Théo Winterhalter (Nov 22 2022 at 09:36):

You can also specialize as.


Last updated: Feb 06 2023 at 12:04 UTC