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: May 28 2023 at 18:29 UTC