The Coq mailing list

[AUGER Cédric <sedrikov AT gmail.com>]

Le Mon, 15 Jul 2013 00:44:37 +0200,
Michiel Helvensteijn 
<mhelvens AT gmail.com>
 a écrit :

> Hi all,
> 
> I have two mutually recursive functions with two arguments each
> (simplified example):
> 
> Fixpoint f (a: T) (b: U) : V := ...
> with g (a: T) (b: U) : V := ...
> 
> I know that they terminate because, as a pair, the arguments are
> structurally decreasing. That is to say, in `f`, `a` decreases and `b`
> is passed unchanged, and in `g`, `a` is passed unchanged and `b`
> decreases.
> 
> `Fixpoint` accepts only a single decreasing argument as evidence for
> termination. Apparently the `Function` construct is more flexible
> w.r.t. termination evidence, but not, it seems, for mutual recursion.
> 
> Sure, I could add a third argument to decrease on, such as a `c: nat`
> containing the sum of the structural depths of `a` and `b`. But that
> would involve a lot of tedious boilerplate code, not to mention
> preconditions and proofs of the fact that `c` always remains large
> enough.
> 
> Is there a technique or construct I'm unaware of? Something that will
> make this easier?
> 
> Thanks in advance!
> 
> --
> www.mhelvens.net

→ You can inline f inside of g (or inline g inside of f)
→ You can generalize f in g (Definition g (f:T→U→V) (a:T) (b:U) := …)
  And then define f (Fixpoint f := …) passing itself to g calls.
  (Note that it is rather fragile in Coq, as the system has to be able
  to check that f is really called with smaller arguments; that is if g
  is opaque for example, it won't work)
→ You can also define a well founded relation on pairs, like:
  "Inductive lt_TU : (T * U) → (T * U) → Prop :=
   | LT1 : ∀ t u1 u2, lt_U u1 u2 → lt_TU (t, u1) (t, u2)
   | LT2 : ∀ t1 t2 u, lt_T t1 t2 → lt_TU (t1, u) (t2, u)
   ."
  Then show the following: "∀ p, Acc lt_TU p",
  and define:
  "Fixpoint f (a : T) (b : U) (H : Acc (a, b)) := …
   with g (a : T) (b : U) (H : Acc (a, b)) := …
  " using recursion on H instead of a/b