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 ?

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.

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

This topic was moved here from #Coq users > Coq equation's equivalent of `Set Program Cases`

by Karl Palmskog.

now I am aware that this place exists

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

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

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.

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

It exists at least in Agda and in Equations' examples

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

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

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

walker has marked this topic as resolved.

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

There’s the issue that the `t :eqn H`

notation conflicts with destruct though. We should find something else…

@Yves Bertot suggests we add a `with-eq`

notation that does inspect too

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