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.
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 :=
...
Thanks! Surprisingly only the first one works (unless I'm keying in the second one wrong).
What about the following?
Ltac notac := idtac.
#[tactic=notac] Equations
It might also be that you don't have the latest Equations?
It is described here: https://github.com/mattam82/Coq-Equations/releases/tag/v1.3-8.13
It looks like I'm on version 1.3+8.14, according to opam.
Also, is there any middle ground tactic to use that does all the intros, but doesn't do any equality-based rewriting?
Well then it should work. At least I think it worked for me using the notac
alias.
I don't know. You could replace idtac
by intros
I guess.
I didn't say it explicitly, but the notac
alias didn't work (failed silently). I'll come back to this in a bit...
Can you try it with Equations?
instead of Equations
.
I use it this way here: https://github.com/SSProve/ssprove/blob/main/theories/Crypt/examples/package_usage_example.v#L170
Okay, yeah, #[tactic=idtac] Equations? ...
seems to do exactly what I want. Thanks!
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.
.
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.
James Wood has marked this topic as resolved.
@Matthieu Sozeau Is it expected that the tactic
attribute only works for Equations?
and not Equations
?
@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!
I think they still get run
that's what https://github.com/mattam82/Coq-Equations/blob/a65e6511038bfc33ed87b8526b5a3e4e3041b1a8/src/g_equations.mlg#L404 Doesn'tGuaranteeOpacity
means
Does Equations need to actually pierce through Qed
, or could that be changed?
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).
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.
That's not easy in the current model unfortunately
to clarify the design, I'd want vos
to follow Defined
and Qed
like today
so there's at least no guesswork, tho I'll believe it might be hard to implement today.
Last updated: May 28 2023 at 18:29 UTC