Stream: Equations devs & users

Topic: ✔ Coq equation's equivalent of `Set Program Cases`

walker (Jan 11 2023 at 15:31):

I am trying to do pattern matching where cases are not going to be triggered as follows:

Equations multi_reduce_to_univ (fuel: nat) (t: Term) : Result nat :=
multi_reduce_to_univ fuel t with multi_reduce fuel t := {
    multi_reduce_to_univ _ _ (Ok (univ l)) := Ok l;
    multi_reduce_to_univ _ _ (Ok (t)) := Err (ReductionError Univ t);
    multi_reduce_to_univ _ _ (Err (OutOfFuel)) := Err (ReductionError Univ t);
    multi_reduce_to_univ _ _ _ := False_rect _ _;
}.

but the obligations are to week to prove anything:

fuel: nat
t: Term
==========
False

is there a way to make coq-equations maintain information about which path in the pattern matching lead to False ?

walker (Jan 11 2023 at 15:46):

For contrasting this is what I get with Program:

Local Set Program Cases.
Program Fixpoint multi_reduce_to_univ (fuel: nat) (t: Term): Result nat :=
match multi_reduce fuel t with
| Ok (univ l) => Ok l
| Ok (t) => Err (ReductionError Univ t)
| Err (OutOfFuel) => Err (ReductionError Univ t)
| _ => False_rect _ _
end.
Next Obligation.

fuel: nat
t: Term
H1: forall l : nat, Ok (univ l) <> multi_reduce fuel t
H0: Err OutOfFuel <> multi_reduce fuel t
H: forall t0 : Term, Ok t0 <> multi_reduce fuel t
================ Goal
False

Why don't I just use program, well I am trying to be slightly consistent and do as much as possible with the least set of tools.

Meven Lennon-Bertrand (Jan 11 2023 at 16:37):

Are you aware of the Equations devs & users stream? I would move your stream there myself, but it seems I don't have the permissions to do so

Notification Bot (Jan 11 2023 at 16:37):

This topic was moved here from #Coq users > Coq equation's equivalent of Set Program Cases by Karl Palmskog.

walker (Jan 11 2023 at 16:38):

now I am aware that this place exists

Karl Palmskog (Jan 11 2023 at 16:39):

our strategy is to let people discover streams when we move their topics to those streams.

Karl Palmskog (Jan 11 2023 at 16:40):

sometimes it takes a while for a mod to see a topic that needs moving, though.

walker (Jan 11 2023 at 16:44):

Karl Palmskog said:

our strategy is to let people discover streams when we move their topics to those streams.

I think it is working great, I discovered few streams this way.

Paolo Giarrusso (Jan 11 2023 at 18:21):

I think you're looking for the inspect pattern @walker

Paolo Giarrusso (Jan 11 2023 at 18:21):

It exists at least in Agda and in Equations' examples

Paolo Giarrusso (Jan 11 2023 at 18:22):

It's not a flag like Program Cases, it's a programming pattern used on the match itself

Paolo Giarrusso (Jan 11 2023 at 18:23):

The actual details are tricky to explain and I'm in a hurry, but I hope they're googlable

walker (Jan 11 2023 at 18:46):

yeah I think I found it, I guess I was searching in the wrong place

Notification Bot (Jan 12 2023 at 12:15):

walker has marked this topic as resolved.

Matthieu Sozeau (Jan 12 2023 at 12:58):

For reference, it’s explained at the end of http://mattam82.github.io/Coq-Equations/examples/Examples.Basics.html

Matthieu Sozeau (Jan 12 2023 at 13:00):

There’s the issue that the t :eqn H notation conflicts with destruct though. We should find something else…

Matthieu Sozeau (Jan 12 2023 at 13:02):

@Yves Bertot suggests we add a with-eq notation that does inspect too

walker (Jan 12 2023 at 13:05):

yeah I noted the conflict, and I ended up coming with something that just works, [ t | H ], the reason I couldn't find the inspect thing is because I was looking in the wrong place I thought it will be a flag.

Last updated: May 28 2023 at 18:29 UTC