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...
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 }.
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.
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?
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.
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
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.
Thanks for the report on the Coq side
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.
Apparently the proof tactic in Equations currently does something less clever than Equations itself :)
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(?).
(i.e., what should I put in place of snd r1 + 4
and snd r2
?
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
well nevermind, I made it work. For some reason without calls to simpl in *
in the right places it would fail at Defined
I replaced all the snd r1 + 4
, snd r2
by underscores
Yep, that works too, they are uniquely determined after all
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.
You'll need to use the mutual eliminator that Equations generated, c_exps_graph_mut
I guess
don't I get the nice eliminator, if I use the manual gc_exp definitions to prove the obligation emitted by equations?
If you get the obligation, yes, in my case I don't get it (on Coq master)
ah, I have it here…
and I get some c_exp_tc_elim
after proving it
Perfect, almost :)
nice. So apart from the manual proof, I do get the same eliminator I would've got in the end?
Yes
excellent!
That's a curious program transformation, what does it do?
that's a compiler from first order lisp to assembly :-)
it's Magnus Myreen's CPP proof pearl
it's a bit complicated because it does tailcall elimination
hence the tc/notc duplication
Ah ok, I wanted to give it a look!
yeah, it's quite fun
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)
I think Function does that
Yep, equations does it only for well-founded ones.
But structurally recursive definitions just compute, so why do you want them?
basically I want to unfold the recursive function into its body, as a match, while equations provides lemmas for the branches
and doing unfold
exposes a fix
(and working with the explicit fix is annoying)
Ah I see, you don't want the "pure" unfolding but after one case analysis to unfold the fix, makes sense
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
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
yes, I think that would work just as well!
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.
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
ah but I guess I don't need an induction principle for gc_exp_tc
hmm, looks like there's no way to combine Equations?
and Equations(noind)
?
((nvm, found the correct syntax, i.e. Equations? (noind)
))
@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.
(also I do not know how I would be able to suppress the warning/future error)
Hmm, that's curious. I guess the obligation handling changed in 8.13. Can you try the 1.3~beta version of Equations?
I get the same issue on 1.3~beta+8.13
Last updated: May 28 2023 at 18:29 UTC