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
to my knowledge the bottom line is: reasoning in isolation about let bindings in Coq can't be done
Right, seems reasonable. Can I define NaryTree_map
and NaryTree_mapchildren
in any other way with equations so that they're two separate functions?
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.
"cannot guess decreasing arg" is usually a hint to switch to using explicit well-founded relations with Equations (Equations ... by wf <expression> <rel> := ...
)
doesn't sound like you would gain anything by defining the vector map
together with other function
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:
"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?
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?
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
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.
This is a common problem, already with list
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 (!).
Right, I should have said Variable
indeed. Once you have that the structural definition should go through
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?
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:
Ah yes, it's another limitation when working with nested inductive types, the elimination principle generation doesn't catch recursive calls under vec_map
You can use #[derive(eliminator=no)] Equations
to a avoid the generation and error
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