The Coq mailing list

[mukesh tiwari <mukeshtiwari.iiitm AT gmail.com>]

Hello everyone,

I am trying to learn how to represent computations as Inductive data type. I can convert a linear recursion/computation into inductive data type (kindly see if my definitions for remainder and greatest common divisor are correct or not), but I am not able to see how to do this for non linear recursion/computation (breath first search or depth first search ). Any code or literature would be great.

Best regards,

Mukesh Tiwari

Computation of greatest common divisor

function gcd(a, b)
    while a ≠ b 
        if a > b
           a := a − b; 
        else
           b := b − a; 
    return a;

and function gcd in terms of inductive definition

Inductive gcd : nat -> nat -> nat -> Prop :=
|cons_a a b : a = b -> gcd a b b
|cons_b a b c : b > a -> gcd a (b - a) c -> gcd a b c
|cons_c a b c : a > b -> gcd (a - b) b c -> gcd a b c.


Lemma gcd_0 : gcd 10 3 1.
Proof.
  constructor 3. omega. constructor 3. omega. simpl.
  constructor 3. omega. simpl. constructor 2. omega.
  simpl. constructor 2. omega. simpl. constructor 1.
  auto.
Qed.

Print gcd_0.

Lemma gcd_1 : forall n : nat, gcd n n n.
Proof.
  intros. constructor 1. auto.
Qed.

Or remainder of two numbers

function rem(a, b)
    while a >= b
           a := a − b;  
    return a;

and corresponding inductive definition

Inductive rem : nat -> nat -> nat -> Prop :=
| cons_0 n1 n2 : n1 < n2 -> rem n1 n2 n1
| cons_1 n1 n2 n3 : n1 >= n2 -> rem (n1 - n2) n2 n3 -> rem n1 n2 n3.


Lemma rem_3 : forall n : nat, n <> 0 -> rem n n 0.
Proof.
  intros. constructor 2. omega.
  assert (H1 : n - n = 0) by omega.
  rewrite H1. constructor 1. omega.
Qed.

Lemma rem_4 : forall n m p : nat, p <> 0 -> rem n m p -> rem (n + m) m p.
Proof.
  constructor 2. omega.
  assert (H1 : n + m - m = n) by omega.
  rewrite H1. trivial.
Qed.