Stream: Equations devs & users

Topic: mutual recursion leaving an obligation for _graph_correct


view this post on Zulip 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...

view this post on Zulip 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 }.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Armaël Guéneau (Feb 12 2021 at 17:49):

Thanks for the report on the Coq side

view this post on Zulip 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.

view this post on Zulip Matthieu Sozeau (Feb 12 2021 at 18:12):

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

view this post on Zulip 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(?).

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Armaël Guéneau (Feb 12 2021 at 19:03):

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

view this post on Zulip Matthieu Sozeau (Feb 12 2021 at 19:04):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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)

view this post on Zulip Armaël Guéneau (Feb 12 2021 at 19:08):

ah, I have it here…

view this post on Zulip Armaël Guéneau (Feb 12 2021 at 19:08):

and I get some c_exp_tc_elim after proving it

view this post on Zulip Matthieu Sozeau (Feb 12 2021 at 19:08):

Perfect, almost :)

view this post on Zulip 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?

view this post on Zulip Matthieu Sozeau (Feb 12 2021 at 19:09):

Yes

view this post on Zulip Armaël Guéneau (Feb 12 2021 at 19:09):

excellent!

view this post on Zulip Matthieu Sozeau (Feb 12 2021 at 19:10):

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

view this post on Zulip Armaël Guéneau (Feb 12 2021 at 19:10):

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

view this post on Zulip Armaël Guéneau (Feb 12 2021 at 19:10):

it's Magnus Myreen's CPP proof pearl

view this post on Zulip Armaël Guéneau (Feb 12 2021 at 19:10):

it's a bit complicated because it does tailcall elimination

view this post on Zulip Armaël Guéneau (Feb 12 2021 at 19:11):

hence the tc/notc duplication

view this post on Zulip Matthieu Sozeau (Feb 12 2021 at 19:11):

Ah ok, I wanted to give it a look!

view this post on Zulip Armaël Guéneau (Feb 12 2021 at 19:11):

yeah, it's quite fun

view this post on Zulip 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)

view this post on Zulip Armaël Guéneau (Feb 12 2021 at 19:13):

I think Function does that

view this post on Zulip Matthieu Sozeau (Feb 12 2021 at 19:15):

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

view this post on Zulip Matthieu Sozeau (Feb 12 2021 at 19:16):

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

view this post on Zulip 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

view this post on Zulip Armaël Guéneau (Feb 12 2021 at 19:17):

and doing unfold exposes a fix

view this post on Zulip Armaël Guéneau (Feb 12 2021 at 19:18):

(and working with the explicit fix is annoying)

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Armaël Guéneau (Feb 12 2021 at 19:24):

yes, I think that would work just as well!

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Armaël Guéneau (Feb 13 2021 at 00:48):

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

view this post on Zulip Armaël Guéneau (Feb 13 2021 at 00:49):

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

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip 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?

view this post on Zulip 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