## Stream: Equations devs & users

### Topic: Case splitting trouble

#### Kenji Maillard (Nov 29 2020 at 10:32):

I have an annoyingly simple functions that I can define easily with Fixpoint but does not seem to be accepted by Equations:

``````Fail Equations myid (n : nat) : nat by struct n :=
myid 0 := 0 ;
myid 1 := 1 ;
myid (S n) := S (myid n). (* Problematic recursive call *)
(* The command has indeed failed with message: *)
(* Error: *)
(* Recursive definition of myid is ill-formed. *)
(* In environment *)
(* myid : nat -> nat *)
(* n : nat *)
(* n0 : nat *)
(* n1 : nat *)
(* Recursive call to myid has principal argument equal to  *)
(* "S n1" instead of one of the following variables:  *)
(* "n0" "n1". *)
(* Recursive definition is: *)
(* "fun n : nat => *)
(*  match n with *)
(*  | 0 => 0 *)
(*  | 1 => 1 *)
(*  | S (S n1) => S (myid (S n1)) *)
(*  end". *)

(* works without trouble *)
Fixpoint myid (n : nat) {struct n} : nat :=
match n with
| 0 => 0
| 1 => 1
| S n => S (myid n)
end.
``````

Is there a reasonable way to keep using Equations and bypass this issue with case-splitting ?

#### Théo Winterhalter (Nov 29 2020 at 10:36):

Ah indeed, it accepts it if you remove the second clause.

#### Théo Winterhalter (Nov 29 2020 at 10:36):

Or if you explicitly state that the last case has two constructors:

``````Equations myid (n : nat) : nat :=
myid 0 := 0 ;
myid 1 := 1 ;
myid (S (S m)) := S (S (myid m)).
``````

#### Kenji Maillard (Nov 29 2020 at 10:36):

yes, but I want to keep this second clause ^^'

#### Kenji Maillard (Nov 29 2020 at 10:37):

Théo Winterhalter said:

Or if you explicitly state that the last case has two constructors:

``````Equations myid (n : nat) : nat :=
myid 0 := 0 ;
myid 1 := 1 ;
myid (S (S m)) := S (S (myid m)).
``````

ok, but that's a simplified example that do not apply to the slightly more complex one I have

#### Kenji Maillard (Nov 29 2020 at 10:38):

the actual code I want is:

``````Equations idn (n : nat) : string_diagram :=
idn 0 := empty ;
idn 1 := id ;
idn (S n) := tensor id (idn n).
``````

#### Théo Winterhalter (Nov 29 2020 at 10:42):

What I'm doing is what `Fixpoint` will define anyway.

#### Théo Winterhalter (Nov 29 2020 at 10:42):

If you don't like it, you probably will not like unfolding your function. Maybe you should use a view instead?

#### Kenji Maillard (Nov 29 2020 at 10:47):

Théo Winterhalter said:

If you don't like it, you probably will not like unfolding your function. Maybe you should use a view instead?

Yea, I'm complaining that the trivial view that I'm expecting here is not inferred/accepted by Equations, whereas it is accepted structurally by `Fixpoint`

#### Kenji Maillard (Nov 29 2020 at 10:48):

Théo Winterhalter said:

What I'm doing is what `Fixpoint` will define anyway.

not exactly, the successor is inside the recursive call...

#### Théo Winterhalter (Nov 29 2020 at 10:50):

Kenji Maillard said:

Théo Winterhalter said:

What I'm doing is what `Fixpoint` will define anyway.

not exactly, the successor is inside the recursive call...

Ah true.

#### Théo Winterhalter (Nov 29 2020 at 10:51):

Kenji Maillard said:

Théo Winterhalter said:

If you don't like it, you probably will not like unfolding your function. Maybe you should use a view instead?

Yea, I'm complaining that the trivial view that I'm expecting here is not inferred/accepted by Equations, whereas it is accepted structurally by `Fixpoint`

Yeah I understand, I actually tried to define a view and got the same error message.

``````Inductive nat_view : nat → Type :=
| nat_0 : nat_view 0
| nat_1 : nat_view 1
| nat_S n : nat_view (S n).

Equations nat_viewc (n : nat) : nat_view n :=
nat_viewc 0 := nat_0 ;
nat_viewc 1 := nat_1 ;
nat_viewc (S (S n)) := nat_S (S n).

Equations myid (n : nat) : nat :=
myid n with nat_viewc n => {
| nat_0 => 0 ;
| nat_1 => 1 ;
| nat_S m => myid m
}.
``````

#### Matthieu Sozeau (Nov 30 2020 at 11:49):

``````Equations myid (n : nat) : nat :=
myid 0 := 0 ;
myid (S n) with n :=
{ | 0 := 1 ;
| _ := myid n }.
``````

is the best we can do for now. Coq is "clever" not to unfold `n` to `S n` to please the guard checker, but that requires quite some hacks

#### Kenji Maillard (Nov 30 2020 at 12:09):

It's good to know that there is a way around. Could we improve the error message to make this method discoverable ? like try to add a suggestion `you may want to bind "foo" with a "with foo => { | ... }" construct` ?

#### Matthieu Sozeau (Nov 30 2020 at 12:33):

That might be possible indeed, or at least put in in a FAQ

Last updated: Sep 30 2023 at 16:01 UTC