coq-club AT inria.fr
Subject: The Coq mailing list
List archive
Re: [Coq-Club] Mutually recursive function with structurally decreasing argument pair?
Chronological Thread
- From: AUGER Cédric <sedrikov AT gmail.com>
- To: Michiel Helvensteijn <mhelvens AT gmail.com>
- Cc: coq-club <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] Mutually recursive function with structurally decreasing argument pair?
- Date: Mon, 15 Jul 2013 01:59:32 +0200
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
- [Coq-Club] Mutually recursive function with structurally decreasing argument pair?, Michiel Helvensteijn, 07/15/2013
- Re: [Coq-Club] Mutually recursive function with structurally decreasing argument pair?, t x, 07/15/2013
- Re: [Coq-Club] Mutually recursive function with structurally decreasing argument pair?, Michiel Helvensteijn, 07/15/2013
- Re: [Coq-Club] Mutually recursive function with structurally decreasing argument pair?, Adam Chlipala, 07/15/2013
- Re: [Coq-Club] Mutually recursive function with structurally decreasing argument pair?, Michiel Helvensteijn, 07/15/2013
- Re: [Coq-Club] Mutually recursive function with structurally decreasing argument pair?, AUGER Cédric, 07/15/2013
- Re: [Coq-Club] Mutually recursive function with structurally decreasing argument pair?, Jacques-Henri Jourdan, 07/15/2013
- Re: [Coq-Club] Mutually recursive function with structurally decreasing argument pair?, Adam Chlipala, 07/15/2013
- Re: [Coq-Club] Mutually recursive function with structurally decreasing argument pair?, t x, 07/15/2013
Archive powered by MHonArc 2.6.18.