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 ?

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

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)).
```

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

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

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).
```

What I'm doing is what `Fixpoint`

will define anyway.

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

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`

Théo Winterhalter said:

What I'm doing is what

`Fixpoint`

will define anyway.

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

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.

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
}.
```

```
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

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`

?

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

Last updated: Oct 13 2024 at 01:02 UTC