Stream: Equations devs & users

Topic: `with` on `with`


view this post on Zulip 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.

view this post on Zulip James Wood (Mar 03 2022 at 09:48):

More observations:

view this post on Zulip James Wood (Mar 03 2022 at 09:53):

view this post on Zulip 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?

view this post on Zulip James Wood (Mar 03 2022 at 10:11):

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

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip James Wood (Mar 03 2022 at 10:14):

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

view this post on Zulip 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 (???)...

view this post on Zulip Paolo Giarrusso (Mar 03 2022 at 10:17):

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

view this post on Zulip 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).

view this post on Zulip Paolo Giarrusso (Mar 03 2022 at 10:23):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip James Wood (Mar 03 2022 at 10:28):

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

view this post on Zulip 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.

view this post on Zulip 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!

view this post on Zulip 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
*)

view this post on Zulip Paolo Giarrusso (Mar 03 2022 at 10:53):

aaah, we want funelim here :-).

view this post on Zulip Paolo Giarrusso (Mar 03 2022 at 10:54):

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

view this post on Zulip 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?

view this post on Zulip 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).

view this post on Zulip 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.

view this post on Zulip Paolo Giarrusso (Mar 03 2022 at 11:02):

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

view this post on Zulip 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 :-|

view this post on Zulip 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

view this post on Zulip 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 28 2024 at 09:01 UTC