The Coq mailing list

[Andreas Abel <andreas.abel AT ifi.lmu.de>]

Hi Tobias,

to me, this trick was new.

In Agda, one can put the height of a data structure as size index into 
its type, so one can make the reasoning about "structurally smaller" 
explicit.  Here is gcd in Agda, using a symmetric difference:

{-# OPTIONS --sized-types #-}
module Gcd where

postulate
  Size : Set
  ↑_   : Size → Size
  ∞    : Size
  Size< : ..(_ : Size) → Set
  max   : Size → Size → Size

{-# BUILTIN SIZE    Size  #-}
{-# BUILTIN SIZESUC ↑_    #-}
{-# BUILTIN SIZEINF ∞    #-}
{-# BUILTIN SIZELT  Size< #-}
{-# BUILTIN SIZEMAX max   #-}

data Nat {size : Size} : Set where
  zero : Nat
  suc  : {size' : Size< size} → Nat {size'} → Nat

data Either (A B : Set) : Set where
  left  : A → Either A B
  right : B → Either A B

-- symmetric difference: returns which number was bigger, plus the 
difference
diff : {i j : Size} → Nat {i} → Nat {j} → Either (Nat {i}) (Nat {j})
diff zero    m       = right m
diff (suc n) zero    = left (suc n)
diff (suc n) (suc m) = diff n m

gcd : {i j : Size} → Nat {i} → Nat {j} → Nat {max i j}
gcd         zero    m            = m
gcd         (suc n) zero         = suc n
gcd {j = j} (suc n) (suc {j'} m) with diff {j = j'} n m
... | left n'  = gcd {j = j} n' (suc m)
... | right m' = gcd {j = j'} (suc n) m'

(Agda development version only.)

Cheers,
Andreas

On 22.03.13 8:26 PM, Tobias Tebbi wrote:
> 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

--
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel AT ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/