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