Stream: Equations devs & users

Topic: ✔ Don't simplify obligations


view this post on Zulip James Wood (Mar 01 2022 at 09:42):

In the following code, the displayed context is m, n : nat, with identification q seemingly having been simplified away automatically. How can I avoid this simplification and keep access to q?

From Equations Require Import Equations.

Definition inspect {A B} (f : A -> B) (x : A) : { y | f x = y } :=
  exist _ _ eq_refl.
Notation "'eqn:' p" := (exist _ _ p) (only parsing, at level 20).

Equations foo : nat -> nat :=
| n with pred n, inspect pred n => {
  | m, eqn: q => _
  }.
Next Obligation.

view this post on Zulip Théo Winterhalter (Mar 01 2022 at 09:50):

This is the obligation tactic doing its work. You can change the obligation tactic globally using

Obligation Tactic := idtac.

or locally to Equations using

#[tactic="idtac"] Equations foo : nat -> nat :=
...

view this post on Zulip James Wood (Mar 01 2022 at 09:59):

Thanks! Surprisingly only the first one works (unless I'm keying in the second one wrong).

view this post on Zulip Théo Winterhalter (Mar 01 2022 at 10:03):

What about the following?

Ltac notac := idtac.

#[tactic=notac] Equations

view this post on Zulip Théo Winterhalter (Mar 01 2022 at 10:03):

It might also be that you don't have the latest Equations?

view this post on Zulip Théo Winterhalter (Mar 01 2022 at 10:04):

It is described here: https://github.com/mattam82/Coq-Equations/releases/tag/v1.3-8.13

view this post on Zulip James Wood (Mar 01 2022 at 10:06):

It looks like I'm on version 1.3+8.14, according to opam.

view this post on Zulip James Wood (Mar 01 2022 at 10:07):

Also, is there any middle ground tactic to use that does all the intros, but doesn't do any equality-based rewriting?

view this post on Zulip Théo Winterhalter (Mar 01 2022 at 10:08):

Well then it should work. At least I think it worked for me using the notac alias.

view this post on Zulip Théo Winterhalter (Mar 01 2022 at 10:09):

I don't know. You could replace idtac by intros I guess.

view this post on Zulip James Wood (Mar 01 2022 at 10:13):

I didn't say it explicitly, but the notac alias didn't work (failed silently). I'll come back to this in a bit...

view this post on Zulip Théo Winterhalter (Mar 01 2022 at 10:14):

Can you try it with Equations? instead of Equations.

view this post on Zulip Théo Winterhalter (Mar 01 2022 at 10:15):

I use it this way here: https://github.com/SSProve/ssprove/blob/main/theories/Crypt/examples/package_usage_example.v#L170

view this post on Zulip James Wood (Mar 01 2022 at 11:01):

Okay, yeah, #[tactic=idtac] Equations? ... seems to do exactly what I want. Thanks!

view this post on Zulip James Wood (Mar 01 2022 at 11:04):

Are there any other reasons why I should prefer Equations? over Equations when dealing with remaining obligations? The only differences I've come across are this and writing Proof. instead of Next Obligation..

view this post on Zulip Théo Winterhalter (Mar 01 2022 at 11:13):

I personally like it more because then you can use the proper proof mode and you can see all you need to prove at once. Whereas with Next Obligation you might have to use the command several times (once for each obligation) so from the file alone you cannot see if an obligation has been forgotten.

view this post on Zulip Notification Bot (Mar 01 2022 at 11:14):

James Wood has marked this topic as resolved.

view this post on Zulip Théo Winterhalter (Mar 01 2022 at 11:15):

@Matthieu Sozeau Is it expected that the tactic attribute only works for Equations? and not Equations?

view this post on Zulip Paolo Giarrusso (Mar 01 2022 at 11:17):

@Théo Winterhalter Equations? might also work better with vos builds then? Next Obligation.scripts are unfortunately still run when building interfaces, but Proof. ... Qed. scripts aren't!

view this post on Zulip Gaëtan Gilbert (Mar 01 2022 at 11:19):

I think they still get run

view this post on Zulip Gaëtan Gilbert (Mar 01 2022 at 11:21):

that's what https://github.com/mattam82/Coq-Equations/blob/a65e6511038bfc33ed87b8526b5a3e4e3041b1a8/src/g_equations.mlg#L404 Doesn'tGuaranteeOpacity means

view this post on Zulip Paolo Giarrusso (Mar 01 2022 at 11:27):

Does Equations need to actually pierce through Qed, or could that be changed?

view this post on Zulip Matthieu Sozeau (Mar 01 2022 at 12:45):

It could be changed but not so easily, we’d have to project out each goal from one big proof. The problem is, the definition itself cannot be seen as finished (if it is transparent) until the obligations are proven. Also, we could guarantee opacity if Equations Transparent is false, but you wouldn’t get the equations lemma and eliminator until after it is actually defined, so I think there is not much to gain. A mode where we treat Proof/Qed for Equations? As Admitted could be useful though, albeit fragile (no guarantee that you get the same behaviors).

view this post on Zulip Paolo Giarrusso (Mar 01 2022 at 13:11):

all I'd want is to Qed proof obligations but not the body, and have them processed asynchronously, for the cases where it makes sense.

view this post on Zulip Matthieu Sozeau (Mar 01 2022 at 13:16):

That's not easy in the current model unfortunately

view this post on Zulip Paolo Giarrusso (Mar 01 2022 at 13:19):

to clarify the design, I'd want vos to follow Defined and Qed like today

view this post on Zulip Paolo Giarrusso (Mar 01 2022 at 13:19):

so there's at least no guesswork, tho I'll believe it might be hard to implement today.


Last updated: Jan 29 2023 at 16:02 UTC