## 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: Jun 23 2024 at 01:02 UTC