In the following definition `lemma`

, `view x`

is not being abstracted in the goal. Why would that be? (Apologies for the somewhat long example, though it's conceptually simple: I have a view `View`

of type `foo`

, a definition `to`

via the view, and then an attempted proof via that same view.)

```
Require Import ssreflect.
From Equations Require Import Equations.
Set Equations Transparent.
Variant foo : Type := aa | bb | cc.
Variant View_true : foo -> Type :=
| view_aa : View_true aa
| view_cc : View_true cc.
Variant View_false : foo -> Type :=
| view_bb : View_false bb.
Variant View {x : foo} : Type :=
| view_true : View_true x -> View
| view_false : View_false x -> View.
Arguments View x : clear implicits.
Equations? view x : View x :=
| aa => _
| bb => _
| cc => _.
Proof.
all: by first [ constructor 1; constructor | constructor 2; constructor ].
Defined.
Equations to : foo -> bool :=
| x with view x =>
| view_true v => true
| view_false v => false.
Equations from : bool -> foo :=
| true => aa
| false => bb.
Equations? lemma x : to (from (to x)) = to x :=
| x with view x =>
| view_true v => _
| view_false v => _.
Proof.
```

More observations:

- Setting
`view`

as opaque does not help. - Defining
`to`

via a`match`

(rather than`with`

) does not help (whether the`match`

is inside`Equations`

or`Definition`

). - Doing
`set w := view x.`

has no effect, but`unfold to. set w := view x.`

does the intended abstraction.

- Defining
`view`

completely by Equations or completely by Ltac seems to make no difference.

given your point about `unfold to. set w := view x.`

, you mean you'd want `with`

to unfold definitions?

I suppose so, yeah. That's what Agda does.

well, I'm not sure how `with`

works exactly here, but in _goals_ Coq will NEVER do unfoldings you didn't ask. (Now, `Equations`

has a nontrivial `Obligation Tactic`

, but I set that to `idtac`

because it violates expectations elsewhere)

If there's a way to do such an unfolding *within* Equations, I'd be happy to do it explicitly.

I mean, I could introduce a `where`

, but that defeats the point of `with`

.

well I understand why you'd want it here, and that in Agda you'd probably get it automatically because Agda does more unfolding (???)...

BTW what are the Agda's semantics in goal normalization?

In Agda, β-equivalent terms are indistinguishable to everything but metaprogramming. βη-equivalent terms are mostly indistinguishable, but `with`

-abstraction is actually one of the counterexamples (fully β-reducing the goal and context is seen as a reasonable thing to do, but η-expansion on top of that is seen as a bridge too far).

arguably, `with`

should be equivalent to `destruct`

in a reasonable way, so arguably it _is_ metaprogramming

With all that said, I guess it'd be good around `with`

to be able to explain exactly what normalisation should be done before matching and abstraction. As far as I'm aware, neither Agda nor Equations offers that, though.

indeed, so in this case you might need to use `inspect`

and `rewrite`

to translate the proof, or write it in a different style.

Is this a concrete suggestion? I don't understand what you're suggesting.

no it's not that concrete sorry — I was thinking of `unfold to; destruct (view x)`

(or a dependent `destruct`

variant from Equations), but you probably don't want to ever unfold Equations-generated definitions since the proof terms are horrible.

Ah, I didn't know that `destruct`

would do `with`

-like abstraction, so this is a helpful remark!

so the output of `unfold to`

is horrible but overall the results here are reasonable:

```
Lemma lemma x : to (from (to x)) = to x.
Proof. unfold to; destruct (view x); simpl.
(*
true = true
false = false
*)
```

aaah, we want `funelim`

here :-).

```
Lemma lemma x : to (from (to x)) = to x.
Proof. by funelim (to x). Qed.
```

arguably, this proof is even nicer than Agda in its own way, since `funelim`

automates (robustly) the pattern of "perform the same splits as the original call" which Agda programmers learn. @James Wood how do you like this?

sorry for the bad suggestion. And as another correction: `destruct`

is pretty weak and will struggle with slightly fancy dependent types; `dependent elimination ident as [ up | .. | up ].`

from the manual does better, but you need an identifier. Here, `unfold to; set v := view xl dependent elimination v; simpl.`

would work (but again, `funelim`

is better).

Thanks, this looks good! (It sounds like you're my barber. :laughing:) I'd stumbled on the first proof you gave, but now I'll learn about `funelim`

.

the horrible term for `to`

, BTW, is why `Set Equations Transparent.`

isn't the default.

Not all code is designed for longer-term maintenance, but for the one that is, as a rule of thumb, depending on the details of any generated proof term is too fragile — where "generated proof term" includes compilation to eliminators :-|

Note that `funelim`

sometimes acts a bit wonky, there's also `apply_funelim`

that keeps all equations in the goal

Yeah, I've noticed that in my actual use case, it's not quite as easy to use. But then, neither is anything else, in a way that's hard to minify to ask another question. :neutral:

Last updated: Mar 03 2024 at 15:01 UTC