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: Sep 30 2023 at 16:01 UTC