Stream: Equations devs & users

Topic: ✔ Don't simplify obligations

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.

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 :=
...

James Wood (Mar 01 2022 at 09:59):

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

Théo Winterhalter (Mar 01 2022 at 10:03):

What about the following?

Ltac notac := idtac.

#[tactic=notac] Equations

Théo Winterhalter (Mar 01 2022 at 10:03):

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

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

James Wood (Mar 01 2022 at 10:06):

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

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?

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.

Théo Winterhalter (Mar 01 2022 at 10:09):

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

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...

Théo Winterhalter (Mar 01 2022 at 10:14):

Can you try it with Equations? instead of Equations.

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

James Wood (Mar 01 2022 at 11:01):

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

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..

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.

Notification Bot (Mar 01 2022 at 11:14):

James Wood has marked this topic as resolved.

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?

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!

Gaëtan Gilbert (Mar 01 2022 at 11:19):

I think they still get run

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

Paolo Giarrusso (Mar 01 2022 at 11:27):

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

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).

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.

Matthieu Sozeau (Mar 01 2022 at 13:16):

That's not easy in the current model unfortunately

Paolo Giarrusso (Mar 01 2022 at 13:19):

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

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: Dec 07 2023 at 09:01 UTC