Library div2

Set Implicit Arguments.

Require Import Notations.
Require Import Logic.
Require Import Datatypes.

Require Import Omega.

A Bruno mentioned in this email, the divide-by-two function can be expressed in a very readable way below.

Fixpoint div2_guarded (n:nat) : nat :=
match n with
| S (S k) => S (div2_guarded k)
| _ => 0
end.

If we limit ourself to the recursor for nat, which is nat_rect, the result does not look that readable. To begin with, here is the type of nat_rect.

Check nat_rect.

nat_rect
: forall P : nat -> Type,
P 0 -> (forall n : nat, P n -> P (S n)) -> forall n : nat, P n

Bruno mentions the following 2 translations in the email above.

Definition div2_recursor1 (n:nat) : nat :=
  fst (nat_rect
            (fun _ => nat *bool)
            (0, true )
            (fun _ r => let (d,b) := r in
                if b
                then
                    (d , false )
                else
                    (S d , true ))
            n).

Bruno says that the following one generalizes better by simultaneously computing the result for the input and its successor.

Definition div2_recursor2 (n:nat) : nat :=
  fst (nat_rect
            (fun _ => nat *nat)
            (0, 0)
            (fun _ r => let (dk,dn) := r in (dn , S dk ))
            n).

Just to be sure that I didn't make a mistake, I prove that the 3 versions are equivalent. First I prove my favourite induction principle on numbers.

Theorem comp_ind:
  forall P: nat -> Prop,
    (forall n: nat, (forall m: nat, m < n -> P m) -> P n)
    -> forall n:nat, P n.
Proof.
     intros P H n.
     assert (forall n:nat , forall m:nat, m < n -> P m).
     intro n0. induction n0 as [| n']; intros.
     inversion H0.
     assert (m < n' \/ m = n') by omega.
     destruct H1; subst; auto.
     apply H0 with (n := S n); omega.
Qed.

Lemma equiv_div2 :
    forall (n:nat),
        div2_guarded n = div2_recursor1 n
        /\ div2_guarded n = div2_recursor2 n.
Proof.
    induction n as [n Hind] using comp_ind.
    unfold div2_recursor1, div2_recursor2, nat_rect.

the cases for n=0 and n=1 are easy

    destruct n; simpl; [auto; fail|].
    destruct n; simpl; [auto; fail|].
    assert (n< S (S n)) as Hn by omega.
    pose proof (Hind _ Hn) as Hindn.
    clear Hind Hn.
    destruct Hindn as [Hindn1 Hindn2].
    split; [rewrite Hindn1 | rewrite Hindn2];
    unfold div2_recursor1, div2_recursor2, nat_rect;
    match goal with
    [ |- S (fst (?rr)) = _ ] => remember rr as r
    end; destruct r as [rf rs]; simpl; auto;
    destruct rs; auto.
Qed.

Coq also provides the Function mechanism to write down recursive functions. This seems to be a very general mechanism. We will illustrate the 4^th variant mentioned in Sec 2.3 of the link above. The user needs to provide a well founded relation and prove that all recursive calls are performed on arguments that are "less" according to that well founded relation. Behind the scenes, Coq is just translating user's code to something much more complicated. Let us write down the div2 function above using the Function mechanism.

Require Import Recdef.

Function div2_Fun (n:nat)
{wf lt }
: nat :=
match n with
| S (S k) => S (div2_Fun k)
| _ => 0
end.
Proof.
-

recursive calls are on "lesser" arguments w.r.t to the supplied w.f. relation

intros; omega.
-

well foundedness of the supplied relation

exact lt_wf.
Qed.

Even though code part of the definition is exactly same as div2_guarded above, the actual definition that goes into the Coq kernel is much more complicated, as shown by the result of the Print query below.

Print div2_Fun.

div2_Fun =
fun x : nat => let (v, _) := div2_Fun_terminate x in v
: nat -> nat

The body of div2_Fun_terminate runs into 100s of lines. However, the good news is that the extracted code looks pretty much like the original code that we wrote down. Presumably, the extra stuff was in Prop and got thrown out.

Extraction div2_Fun.

let rec div2_Fun = function
| O -> O
| S n0 ->
  (match n0 with
   | O -> O
   | S k -> S (div2_Fun k))

Try replacing the proofs of both the subgoals by admit. The result of Extraction will remain unchanged. Hence, as Matthieu suggested in this email, one can use classical axioms to prove termination. The Ocaml extract should not get stuck in such cases/

Even though div2_Fun is more complicated than whath we wrote, one can use div2_Fun_equation to get it to behave (in proofs) exactly like what we wrote

Check div2_Fun_equation.

div2_Fun_equation
     : forall n : nat,
       div2_Fun n =
       match n with
       | 0 => 0
       | 1 => 0
       | S (S k) => S (div2_Fun k)
       end

Finally, lets see another example of this method.

Require Import NPeano.

Print gcd.

Function Gcd (a b : nat) {wf lt a} : nat :=
match a with
| O => b
| S k => Gcd (b mod S k) (S k)
end
.
Proof.
- intros m n k Heq. subst. apply Nat.mod_upper_bound.
omega.
- exact lt_wf.
Qed.

Check Gcd_equation.