The Coq mailing list

[Tobias Tebbi <ttebbi AT ps.uni-saarland.de>]

Hi,

I would like to share a little trick to make recursive functions 
structurally recursive.
Consider the gcd function, that ideally, we would like  to write as

Fixpoint gcd (m n : nat) : nat :=
  match m with
    | 0 => n
    | _ => gcd (modulo n m) m
  end.

However, Coq does not accept this definition because the term (modulo n 
m) is not structurally smaller than m, altough it is a smaller number. 
We can circumvent this problem by constructing a term that is equal to 
(mod n m) and and structurally smaller than m. All we need is the 
minimum function, defined as follows.

Definition tmin m n := m - (m - n).

Using the fact that the minus from the standard library is defined in a 
way that the term (m-n) is always structurally smaller or equal than m, 
we have that the term (tmin m n) is strucurally smaller or equal than m.

Now the following definition of gcd works, even if modulo is left 
abstract and cannot be inspected by the type checker.

Variable modulo : nat -> nat -> nat.
Fixpoint gcd (m n : nat) : nat :=
  match m with
    | 0 => n
    | S m' => gcd (tmin m' (modulo n m)) m
  end.

In contrast to this, the structurally recursive versions of gcd in the 
Coq Standard Library (8.4) and SSReflect use special mod functions.

In proofs about functions using tmin, one just has to rewrite with the 
following fact.

Lemma tmin_snd m n : n <= m -> tmin m n = n.
Proof.
  unfold tmin. omega.
Qed.

This trick allows to write any recursive function that decreases a 
natural number argument. It could be extended to tree-like inductive 
types. In this case, instead of the minimum function, one has to search 
for a given subtree in a larger tree and return it.

Please let me know if this trick has been used before.

Best,

Tobias