`with` on `with` · Equations devs & users

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

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

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

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

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

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

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

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:

Stream: Equations devs & users

Topic: `with` on `with`

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