Sébastien Michelland (Dec 07 2022 at 18:43): Sébastien Michelland (Dec 07 2022 at 18:43):I have a nested inductive type along with a recursive program on it, defined using a where clause and a subprogram to handle the nesting. Now I'm trying to prove some theorem on it, but for the nested object that theorem is expressed using the subprogram's return value. The subprogram appears to be hidden, and according to the documentation where clauses are elaborated as let bindings inside the main function. How should I go to reason about that subprogram?
Silly example:
From Coq Require Import List.
From Equations Require Import Equations.
Import ListNotations.
Inductive NaryTree (α: Type): Type :=
| Leaf
| Node (children: list (NaryTree α)).
Arguments Leaf {α}.
Arguments Node {α} (_).
Equations NaryTree_map {α β} (f: α -> β) (t: NaryTree α): NaryTree β :=
NaryTree_map f Leaf := Leaf;
NaryTree_map f (Node children) := Node (NaryTree_mapchildren children)
where NaryTree_mapchildren (l: list (NaryTree α)): list (NaryTree β) :=
NaryTree_mapchildren [] := [];
NaryTree_mapchildren (t::l) := NaryTree_map f t :: NaryTree_mapchildren l.
Check NaryTree_mapchildren.
(* Error: The reference NaryTree_mapchildren was not found in the current environment. *)
pretty much every functional programming language semantics I've seen defines the meaning of a let binding via substitution. This means the let binding basically can't be called a subprogram in any meaningful sense, and can't be reasoned about separately
Karl Palmskog (Dec 07 2022 at 21:10):to my knowledge the bottom line is: reasoning in isolation about let bindings in Coq can't be done
Sébastien Michelland (Dec 07 2022 at 21:10):Right, seems reasonable. Can I define NaryTree_map and NaryTree_mapchildren in any other way with equations so that they're two separate functions?
Karl Palmskog (Dec 07 2022 at 21:15):Why not just use regular map?
Equations NaryTree_map {α β} (f: α -> β) (t: NaryTree α): NaryTree β :=
NaryTree_map f Leaf := Leaf;
NaryTree_map f (Node children) := Node (map (NaryTree_map f) children).
That would be ideal. My particular use case is with different higher-order functions on a dependent vector type though, and the recursive calls do not seem to be recognized, leading to usual "cannot guess the decreasing argument of fix messages". Are there any tricks to improve my chances here? I can make a MWE if needed.
Karl Palmskog (Dec 07 2022 at 21:25):"cannot guess decreasing arg" is usually a hint to switch to using explicit well-founded relations with Equations (Equations ... by wf <expression> <rel> := ...)
Karl Palmskog (Dec 07 2022 at 21:26):doesn't sound like you would gain anything by defining the vector map together with other function
Sébastien Michelland (Dec 07 2022 at 21:45):Right, inlining the nested type is my gut reaction, but it is quite unsatisfying. Let me see if I can get the wf option to work. I've tried to use the subterm relation as a first test below (not sure if it's good enough):
Inductive vec (α: Type): nat -> Type :=
| vec_nil: vec α 0
| vec_cons {N} (a: α) (u: vec α N): vec α (S N).
Arguments vec_nil {α}.
Arguments vec_cons {α N}.
Equations Derive NoConfusion Subterm for vec.
Equations vec_map {N α β} (f: α -> β) (v: vec α N): vec β N :=
vec_map f vec_nil := vec_nil;
vec_map f (vec_cons a u) := vec_cons (f a) (vec_map f u).
Inductive M: Type -> Type :=
| Ret {R} (r: R): M R
| Blocks {R T} {N: nat} (blocks: vec (T -> M T) N) (k: T -> M R): M R.
Equations Derive NoConfusion Subterm for M.
Equations identity {R} (m: M R): M R by wf m M_subterm :=
identity (Ret r) := Ret r;
identity (Blocks blocks k) :=
Blocks (vec_map (fun b t => identity (b t)) blocks) (fun t => identity (k t)).
I get "The carrier type of the recursion order cannot depend on the arguments" though, and judging from the manual which has this example
Equations unzip {n} (v : vector (A × B) n) : vector A n × vector B n
by wf (signature pack v ) (@t subterm (A × B)) :=
It does seem on the surface that using m could be legal. :thinking:
Paolo Giarrusso (Dec 08 2022 at 05:39):"signature pack v" isn't syntax I've seen (got a link?); but that + your error suggests the following trick: to ensure the carrier doesn't depend on earlier arguments, maybe the well-founded recursion could be defined on { R & M R }? "Signature pack" might be syntax to ask Equations to do this internally?
Paolo Giarrusso (Dec 08 2022 at 05:42):OTOH, if R is constant throughout the recursion, maybe you could declare it as a section parameter:
Section foo.
Context {R : Type}.
Equations identity (m : M R) ...
End foo.
Ok, I'm making progress. For "signature pack v", some underscores actually disappeared when I copied from the manual. The example reads
Equations unzip {n} (v : vector (A × B) n) : vector A n × vector B n
by wf (signature_pack v) (@t_subterm (A × B)) :=
where t_subterm is from Derive Subterm and signature_pack is a generic Equations function which connects to the signature obtained from Derive Signature, and does what you suggested with the index. In my case R isn't constant so the signature pack feels like the correct approach.
I've been trying to build a subterm relation, which seems to me like it should be straightforward by inlining the nested inductive. However deriving Subterm leaves me with a basic M_direct_subterm which ignores the sub-terms in the vector.
Inductive vec (α: Type): nat -> Type :=
| vec_nil: vec α 0
| vec_cons {N} (a: α) (u: vec α N): vec α (S N).
Inductive M: Type -> Type :=
| Ret {R} (r: R): M R
| Blocks {R T} {N: nat} (blocks: vec (T -> M T) N) (k: T -> M R): M R.
Equations Derive NoConfusion NoConfusionHom Subterm Signature for M vec.
Print M_direct_subterm. (* only one case for k *)
Can I get such a subterm relation automatically, or do I have to build it?
Matthieu Sozeau (Dec 08 2022 at 10:18):Indeed, Equations does not yet generate automatically the subterm relation for nested inductive types like M. You could either derive it yourself or write a size function like the last example here http://mattam82.github.io/Coq-Equations/examples/Examples.mutualwfrec.html
Matthieu Sozeau (Dec 08 2022 at 10:20):However your definition of identity is fine using structural recursion, you only need to define vec_map in a section with f : alpha -> beta as a parameter, so that the syntactic guard checking can recognize it.
Matthieu Sozeau (Dec 08 2022 at 10:21):This is a common problem, already with list
Sébastien Michelland (Dec 08 2022 at 10:24):Thanks, this is exactly what I'd like to know more about. Could you elaborate just a bit? Setting f as a Variable in a section for vec_map yields the same result, while setting it as a Parameter makes it a free variable of vec_map even outside the section (!).
Matthieu Sozeau (Dec 08 2022 at 10:28):Right, I should have said Variable indeed. Once you have that the structural definition should go through
Sébastien Michelland (Dec 08 2022 at 10:30):Cool, I should be close then. I do get obligations about the subterms in the vector though. Is that what you mean?
Inductive vec (α: Type): nat -> Type :=
| vec_nil: vec α 0
| vec_cons {N} (a: α) (u: vec α N): vec α (S N).
Arguments vec_nil {α}.
Arguments vec_cons {α N}.
Inductive M: Type -> Type :=
| Ret {R} (r: R): M R
| Blocks {R T} {N: nat} (blocks: vec (T -> M T) N) (k: T -> M R): M R.
Equations Derive NoConfusion NoConfusionHom Subterm Signature for vec M.
Section VecMap.
Variables (α β: Type) (f: α -> β).
Equations vec_map {N} (v: vec α N): vec β N :=
vec_map vec_nil := vec_nil;
vec_map (vec_cons a u) := vec_cons (f a) (vec_map u).
End VecMap.
Arguments vec_map {α β} (f) {N}.
Equations? identity {R} (m: M R): M R by wf (signature_pack m) M_subterm :=
identity (Ret r) := Ret r;
identity (Blocks blocks k) :=
Blocks (vec_map (fun b t => identity (b t)) blocks) (fun t => identity (k t)).
Try without the wf annotation?
Sébastien Michelland (Dec 08 2022 at 10:32):It appears to work with Equations?. Great! Strangely with Equations I get the following message
Obligation 1 of identity_graph_correct:
(forall (R : Type) (m : M R), identity_graph R m (identity m)).
Functional induction principle could not be proved automatically, it is left as an obligation.
But there is no obligation. :sweat_smile:
Matthieu Sozeau (Dec 08 2022 at 10:37):Ah yes, it's another limitation when working with nested inductive types, the elimination principle generation doesn't catch recursive calls under vec_map
Matthieu Sozeau (Dec 08 2022 at 10:43):You can use #[derive(eliminator=no)] Equations to a avoid the generation and error
Sébastien Michelland (Dec 08 2022 at 11:01):Right, I had to prove the induction principle manually in some other case. Well this is all very helpful, I think I can now go back to my code and make some progress. Thanks for the help!
Last updated: May 28 2023 at 18:29 UTC