## Stream: Equations devs & users

### Topic: Accessing where clauses as independent functions

#### 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. *)
``````

#### Karl Palmskog (Dec 07 2022 at 21:08):

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).
``````

#### Sébastien Michelland (Dec 07 2022 at 21:22):

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.
``````

#### Sébastien Michelland (Dec 08 2022 at 10:01):

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)).
``````

#### Matthieu Sozeau (Dec 08 2022 at 10:31):

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: Jan 29 2023 at 14:02 UTC