## Stream: Equations devs & users

### Topic: `with` on `with`

#### James Wood (Mar 03 2022 at 09:22):

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

#### James Wood (Mar 03 2022 at 09:48):

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.

#### James Wood (Mar 03 2022 at 09:53):

• Defining `view` completely by Equations or completely by Ltac seems to make no difference.

#### Paolo Giarrusso (Mar 03 2022 at 10:10):

given your point about `unfold to. set w := view x.`, you mean you'd want `with` to unfold definitions?

#### James Wood (Mar 03 2022 at 10:11):

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

#### Paolo Giarrusso (Mar 03 2022 at 10:12):

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)

#### James Wood (Mar 03 2022 at 10:13):

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

#### James Wood (Mar 03 2022 at 10:14):

I mean, I could introduce a `where`, but that defeats the point of `with`.

#### Paolo Giarrusso (Mar 03 2022 at 10:16):

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

#### Paolo Giarrusso (Mar 03 2022 at 10:17):

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

#### James Wood (Mar 03 2022 at 10:21):

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

#### Paolo Giarrusso (Mar 03 2022 at 10:23):

arguably, `with` should be equivalent to `destruct` in a reasonable way, so arguably it _is_ metaprogramming

#### James Wood (Mar 03 2022 at 10:24):

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.

#### Paolo Giarrusso (Mar 03 2022 at 10:26):

indeed, so in this case you might need to use `inspect` and `rewrite` to translate the proof, or write it in a different style.

#### James Wood (Mar 03 2022 at 10:28):

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

#### Paolo Giarrusso (Mar 03 2022 at 10:36):

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.

#### James Wood (Mar 03 2022 at 10:39):

Ah, I didn't know that `destruct` would do `with`-like abstraction, so this is a helpful remark!

#### Paolo Giarrusso (Mar 03 2022 at 10:50):

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
*)
``````

#### Paolo Giarrusso (Mar 03 2022 at 10:53):

aaah, we want `funelim` here :-).

#### Paolo Giarrusso (Mar 03 2022 at 10:54):

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

#### Paolo Giarrusso (Mar 03 2022 at 10:55):

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?

#### Paolo Giarrusso (Mar 03 2022 at 10:56):

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

#### James Wood (Mar 03 2022 at 10:57):

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

#### Paolo Giarrusso (Mar 03 2022 at 11:02):

the horrible term for `to`, BTW, is why `Set Equations Transparent.` isn't the default.

#### Paolo Giarrusso (Mar 03 2022 at 11:06):

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

#### Alexander Gryzlov (Mar 03 2022 at 14:27):

Note that `funelim` sometimes acts a bit wonky, there's also `apply_funelim` that keeps all equations in the goal

#### James Wood (Mar 03 2022 at 15:48):

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