## Stream: Equations devs & users

### Topic: mutual recursion leaving an obligation for _graph_correct

#### Armaël Guéneau (Jan 17 2021 at 12:51):

I'm trying to write a definition with three mutually recursive functions, which Equations manages to define, but then does not manage to solve the obligation for the _graph_correct lemma. I do want an elimination principle for this definition, and I don't know how to prove the obligation manually.

It's a somewhat nontrivial recursive definition, with functions A B C where A sometimes calls B recursively with non-decreasing arguments, but B always calls A with smaller arguments -- so it's well founded at least.

While trying to reproduce/minimize the issue based on the nested_mut_rec example from Equations, I came onto the following degenerate example that also results in _graph_correct not being solved:

``````From Equations Require Import Equations.
From Coq Require Import Program Arith Compare_dec.

Inductive term : Set :=
| Var (n : nat)
| Lam (t : term)
| App (t : term) (l : list term)
| MetaVar (n : nat) (l : list term).

Equations subst_var (k : nat) (u : term) (t : nat) : term :=
subst_var k u n with k ?= n :=
{ | Eq => u;
| Gt => Var n;
| Lt => Var (pred n) }.

Equations subst_term (k : nat) (u : term) (t : term) : term by struct t := {
subst_term k u t := Var 0 }

where subst_term' (k : nat) (u : term) (t : term) : term by struct t := {
subst_term' k u (Var n) := subst_var k u n;
subst_term' k u (Lam t) := Lam (subst_term' (S k) u t);
subst_term' k u (App t l) := App (subst_term' k u t) (subst_tlist k u l);
subst_term' k u (MetaVar t l) := MetaVar t (subst_tlist k u l) }

where subst_tlist (k : nat) (u : term) (t : list term) : list term by struct t := {
subst_tlist k u nil := nil;
subst_tlist k u (cons t ts) := cons (subst_term' k u t) (subst_tlist k u ts) }.
``````

(here, unlike my actual usecase, `subst_term` is isolated and not called by anyone)

Any clues as to what is happening here? I guess an other option would be to rephrase my definition using the "mutual wf" encoding shown in the mutualwfrec example, but I was wondering if there's a way to not do that, since it seems the functions can at least be defined without wf recursion...

#### Armaël Guéneau (Jan 17 2021 at 12:59):

Here's a minimized version of the actual definition I'm trying to do:

``````From Equations Require Import Equations.
From Coq Require Import Program Arith Compare_dec.

Inductive exp :=
| Const : nat -> exp
| Var : nat -> exp
| Op : list exp -> exp
| If : list exp -> exp -> exp -> exp
| Let : nat -> exp -> exp -> exp
| Call : nat -> list exp -> exp.

Equations c_exp_tc (z: exp) : nat by struct z :=
{ c_exp_tc (Let n x y) :=
let r1 := c_exp_notc x in
let r2 := c_exp_tc y in
r1 + r2 ;
c_exp_tc (If xs y z) :=
let r1 := c_exps xs in
let r2 := c_exp_tc z in
let r3 := c_exp_tc y in
r1 + r2 + r3 ;
c_exp_tc (Call n xs) :=
c_exps xs ;
c_exp_tc z :=
c_exp_notc z }
where c_exp_notc (z: exp) : nat by struct z :=
{ c_exp_notc (Let n x y) :=
let r1 := c_exp_notc x in
let r2 := c_exp_notc y in
r1 + r2 ;
c_exp_notc (If xs y z) :=
let r1 := c_exps xs in
let r2 := c_exp_notc z in
let r3 := c_exp_notc y in
r1 + r2 + r3 ;
c_exp_notc (Call n xs) := c_exps xs ;
c_exp_notc (Const n) := n ;
c_exp_notc (Var n) := n ;
c_exp_notc (Op xs) := c_exps xs }
where c_exps (zs: list exp) : nat by struct zs :=
{ c_exps [] := 0 ;
c_exps (x :: xs) :=
let res1 := c_exp_notc x in
let res2 := c_exps xs in
res1 + res2 }.
``````

#### Matthieu Sozeau (Feb 12 2021 at 17:27):

Wow, that's pretty bad, this fails:

``````Inductive exp :=
| If : list exp -> exp.

Fixpoint c_exps (zs : list exp) : nat :=
match zs as l return nat with
| [] => 0
| e :: zs1 =>
(let fix c_exp_notc (z : exp) : nat :=
match z return nat with
| If l0 => (c_exps l0)
end in
c_exp_notc) e
end.
``````

#### Matthieu Sozeau (Feb 12 2021 at 17:28):

So it's not Equations that is at fault here but Coq for not being able to figure out that this is a fine nested fixpoint
@Armaël Guéneau did you find a workaround in the meantime?

#### Matthieu Sozeau (Feb 12 2021 at 17:35):

It can however check that this one is guarded:

``````Fixpoint c_exps_notc (z : exp) : nat :=
match z with
| If l0 =>
let fix c_exps (zs : list exp) : nat :=
match zs with
| nil => 0
| cons e zs1 => c_exps_notc e
end
in c_exps l0
end.
``````

#### Matthieu Sozeau (Feb 12 2021 at 17:47):

I reported the problem on Coq's issue tracker, I'm not sure adapting the guard checker would be easy but it's worth a shot

#### Armaël Guéneau (Feb 12 2021 at 17:49):

I have been working on other things in the meantime, so I didn't look too hard for a workaround.
For my specific usecase, I thought that I could maybe encode everything as a well founded definition, using the gadt-like encoding from one of the equations examples, but I haven't actually tried that yet.

#### Armaël Guéneau (Feb 12 2021 at 17:49):

Thanks for the report on the Coq side

#### Matthieu Sozeau (Feb 12 2021 at 17:58):

A work-around is to prove the elimination principle manually using Equations as well, e.g.:

``````  Obligation Tactic := idtac.
Equations? gc_exp_tc (z: exp) : c_exp_tc_graph z (c_exp_tc z) :=
{ gc_exp_tc (If xs y) :=
let r1 := gc_exps xs in
let r2 := gc_exp_tc y in
_ }
where gc_exp_notc (z: exp) : c_exp_notc_graph z (c_exp_notc z) by struct z :=
{ gc_exp_notc (If xs y) :=
let r1 := c_exps xs in
let r2 := gc_exp_notc y in
_ }
where gc_exps (zs: list exp) : c_exps_graph zs (c_exps zs) by struct zs :=
{ gc_exps [] := _ ;
gc_exps (x :: xs) :=
let res2 := gc_exps xs in
let res1 := gc_exp_notc x in _ }.
Proof.
all:autorewrite with c_exp_tc; simpl; constructor; try assumption.
apply gc_exps.
Defined.
``````

You just mimick the exact same recursive calls to build the graph object.

#### Matthieu Sozeau (Feb 12 2021 at 18:12):

Apparently the proof tactic in Equations currently does something less clever than Equations itself :)

#### Armaël Guéneau (Feb 12 2021 at 18:58):

hmm, interesting. I'm trying that, and here's my actual actual definition:

``````Equations c_exp_tc (l: nat) (vs: list (option vname)) (fs: list (fname * nat)) (z: exp) : (app_list inst * nat) by struct z :=
{ c_exp_tc l vs fs (Let n x y) :=
let r1 := c_exp_notc l vs fs x in
let r2 := c_exp_tc (snd r1) (Some n :: vs) fs y in
((fst r1) +++ (fst r2) +++ List [], snd r2) ;
c_exp_tc l vs fs (If cmp xs y z) :=
let r1 := c_exps l vs fs xs in
let r2 := c_exp_tc (snd r1 + 4) vs fs z in
let r3 := c_exp_tc (snd r2) vs fs y in
c_if true cmp r1 r2 r3 ;
c_exp_tc l vs fs (lang.Call n xs) :=
c_call true vs (lookup_fname n fs) xs (c_exps l vs fs xs) ;
c_exp_tc l vs fs z :=
make_ret vs (c_exp_notc l vs fs z) }
where c_exp_notc (l: nat) (vs: list (option vname)) (fs: list (fname * nat)) (z: exp) : (app_list inst * nat) by struct z :=
{ c_exp_notc l vs fs (Let n x y) :=
let r1 := c_exp_notc l vs fs x in
let r2 := c_exp_notc (snd r1) (Some n :: vs) fs y in
(fst r1 +++ fst r2 +++ List [Add_RSP 1], snd r2 + 1) ;
c_exp_notc l vs fs (If cmp xs y z) :=
let r1 := c_exps l vs fs xs in
let r2 := c_exp_notc (snd r1 + 4) vs fs z in
let r3 := c_exp_notc (snd r2 + 1) vs fs y in
c_if false cmp r1 r2 r3 ;
c_exp_notc l vs fs (lang.Call n xs) :=
c_call false vs (lookup_fname n fs) xs (c_exps l vs fs xs) ;
c_exp_notc l vs fs (lang.Const n) :=
c_const l n vs ;
c_exp_notc l vs fs (Var n) :=
c_var l n vs ;
c_exp_notc l vs fs (Op op xs) :=
let r1 := c_exps l vs fs xs in
let insts := c_op op vs (snd r1) in
(Append (fst r1) (List insts), snd r1 + length insts) }
where c_exps (l: nat) (vs: list (option vname)) (fs: list (fname * nat)) (zs: list exp) : (app_list inst * nat) by struct zs :=
{ c_exps l vs fs [] := (List [], l) ;
c_exps l vs fs (x :: xs) :=
let res1 := c_exp_notc l vs fs x in
let res2 := c_exps (snd res1) (None :: vs) fs xs in
(fst res1 +++ fst res2, snd res2) }.
``````

You can see for instance in the c_exp_tc case for If that I'm using r1 to construct an argument for the next recursive call. But I'm not sure what to do when constructing the elimination principle, since r1 is now an inhabitant of the graph(?).

#### Armaël Guéneau (Feb 12 2021 at 18:59):

(i.e., what should I put in place of `snd r1 + 4` and `snd r2`?

#### Matthieu Sozeau (Feb 12 2021 at 19:03):

In this case it is probably better than you bind `r1` as in the original program and `r1g` as the call to the graph, then leave all final bodies as underscores and then the obligations should easily follow

#### Armaël Guéneau (Feb 12 2021 at 19:03):

well nevermind, I made it work. For some reason without calls to `simpl in *` in the right places it would fail at Defined

#### Armaël Guéneau (Feb 12 2021 at 19:03):

I replaced all the `snd r1 + 4`, `snd r2` by underscores

#### Matthieu Sozeau (Feb 12 2021 at 19:04):

Yep, that works too, they are uniquely determined after all

#### Matthieu Sozeau (Feb 12 2021 at 19:05):

Now the sad thing is that you don't get the nice cleaned up eliminator that Equations produces, but still you can do proofs directly by induction on the graph.

#### Matthieu Sozeau (Feb 12 2021 at 19:07):

You'll need to use the mutual eliminator that Equations generated, `c_exps_graph_mut` I guess

#### Armaël Guéneau (Feb 12 2021 at 19:07):

don't I get the nice eliminator, if I use the manual gc_exp definitions to prove the obligation emitted by equations?

#### Matthieu Sozeau (Feb 12 2021 at 19:08):

If you get the obligation, yes, in my case I don't get it (on Coq master)

#### Armaël Guéneau (Feb 12 2021 at 19:08):

ah, I have it here…

#### Armaël Guéneau (Feb 12 2021 at 19:08):

and I get some `c_exp_tc_elim` after proving it

#### Matthieu Sozeau (Feb 12 2021 at 19:08):

Perfect, almost :)

#### Armaël Guéneau (Feb 12 2021 at 19:09):

nice. So apart from the manual proof, I do get the same eliminator I would've got in the end?

Yes

excellent!

#### Matthieu Sozeau (Feb 12 2021 at 19:10):

That's a curious program transformation, what does it do?

#### Armaël Guéneau (Feb 12 2021 at 19:10):

that's a compiler from first order lisp to assembly :-)

#### Armaël Guéneau (Feb 12 2021 at 19:10):

it's Magnus Myreen's CPP proof pearl

#### Armaël Guéneau (Feb 12 2021 at 19:10):

it's a bit complicated because it does tailcall elimination

#### Armaël Guéneau (Feb 12 2021 at 19:11):

hence the tc/notc duplication

#### Matthieu Sozeau (Feb 12 2021 at 19:11):

Ah ok, I wanted to give it a look!

#### Armaël Guéneau (Feb 12 2021 at 19:11):

yeah, it's quite fun

#### Armaël Guéneau (Feb 12 2021 at 19:13):

btw, since I've got you here: one thing that would be useful but I don't think Equation provides at the moment, is generating unfolding for recursive definitions (including basic primitive recursive fixpoints)

#### Armaël Guéneau (Feb 12 2021 at 19:13):

I think Function does that

#### Matthieu Sozeau (Feb 12 2021 at 19:15):

Yep, equations does it only for well-founded ones.

#### Matthieu Sozeau (Feb 12 2021 at 19:16):

But structurally recursive definitions just compute, so why do you want them?

#### Armaël Guéneau (Feb 12 2021 at 19:17):

basically I want to unfold the recursive function into its body, as a match, while equations provides lemmas for the branches

#### Armaël Guéneau (Feb 12 2021 at 19:17):

and doing `unfold` exposes a fix

#### Armaël Guéneau (Feb 12 2021 at 19:18):

(and working with the explicit fix is annoying)

#### Matthieu Sozeau (Feb 12 2021 at 19:18):

Ah I see, you don't want the "pure" unfolding but after one case analysis to unfold the fix, makes sense

#### Armaël Guéneau (Feb 12 2021 at 19:19):

so for

``````Equations foo (n: nat): nat :=
foo O := O;
foo (S n) := foo n.
``````

the lemma would say

``````forall n, foo n = match n with 0 => 0 | S n => foo n end
``````

#### Matthieu Sozeau (Feb 12 2021 at 19:22):

Hnmm, the thing is, the term on the right could be horrible still. For wf definitions, I generate a `foo_unfold` definition + a proof of `foo n = foo_unfold n` where `foo_unfold` is the non-recursive version calling back to `foo`, would that be enough? You can unfold it of course

#### Armaël Guéneau (Feb 12 2021 at 19:24):

yes, I think that would work just as well!

#### Armaël Guéneau (Feb 12 2021 at 19:26):

in the long run I guess that it would be nice a way to programatically discover the name of foo_unfold and the related lemmas by just knowing `foo`, but I'm not at that level of automation anyway.

#### Armaël Guéneau (Feb 13 2021 at 00:44):

well, looks like I spoke too fast: there's an obligation remaining... `gc_exp_tc_graph_correct` couldn't be proved automatically, and it looks like exactly the obligation that couldn't be solved for c_exp_tc

#### Armaël Guéneau (Feb 13 2021 at 00:46):

ah but I guess I don't need an induction principle for gc_exp_tc

#### Armaël Guéneau (Feb 13 2021 at 00:48):

hmm, looks like there's no way to combine `Equations?` and `Equations(noind)` ?

#### Armaël Guéneau (Feb 13 2021 at 00:49):

((nvm, found the correct syntax, i.e. `Equations? (noind)`))

#### Armaël Guéneau (May 09 2021 at 14:30):

@Matthieu Sozeau coming back to this after upgrading to coq 8.13 and equations 1.2.4, there seems to be a new issue. On the problematic definition (here https://coq.zulipchat.com/#narrow/stream/237659-Equations-devs.20.26.20users/topic/mutual.20recursion.20leaving.20an.20obligation.20for.20_graph_correct/near/223041614) , equations still says that it's not able to prove c_exp_tc_graph_correct automatically:

``````Warning:
Solve Obligations tactic returned error: Recursive definition of c_exps is ill-formed.
[...]
This will become an error in the future [solve_obligation_error,tactics]
1 obligation remaining
Obligation 1 of c_exp_tc_graph_correct:
((∀ z : exp, c_exp_tc_graph z (c_exp_tc z)) *
((∀ z : exp, c_exp_notc_graph z (c_exp_notc z)) * (∀ zs : list exp, c_exps_graph zs (c_exps zs))))%type.
Warning: Functional induction principle could not be proved automatically, it is left as an obligation.
``````

However, now it seems that no obligation is produced! So I'm not able to do `Next Obligation` to complete the proof.

#### Armaël Guéneau (May 09 2021 at 14:33):

(also I do not know how I would be able to suppress the warning/future error)

#### Matthieu Sozeau (May 10 2021 at 07:28):

Hmm, that's curious. I guess the obligation handling changed in 8.13. Can you try the 1.3~beta version of Equations?

#### Armaël Guéneau (May 10 2021 at 12:08):

I get the same issue on 1.3~beta+8.13

Last updated: Jan 29 2023 at 14:02 UTC