Stream: Equations devs & users

Topic: Case splitting trouble


view this post on Zulip 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 ?

view this post on Zulip Théo Winterhalter (Nov 29 2020 at 10:36):

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

view this post on Zulip 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)).

view this post on Zulip Kenji Maillard (Nov 29 2020 at 10:36):

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

view this post on Zulip 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

view this post on Zulip 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).

view this post on Zulip Théo Winterhalter (Nov 29 2020 at 10:42):

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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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...

view this post on Zulip 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.

view this post on Zulip 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
  }.

view this post on Zulip 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

view this post on Zulip 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 ?

view this post on Zulip Matthieu Sozeau (Nov 30 2020 at 12:33):

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


Last updated: Jan 29 2023 at 15:02 UTC