The Coq mailing list

[Dirk Pattinson <dirk.pattinson AT anu.edu.au>]

Hi Mukesh,

I think you are looking for derivation trees in operational semantics. 
In Coq specifically, see for instance the chapter on the Imp toy 
language in Software Foundations:

  https://www.cis.upenn.edu/~bcpierce/sf/current/Imp.html

The inference rules are presented under the heading 'Operational 
Semantics' and there's an inductive definition of the evaluation 
relation just below.

All the best,

Dirk.


On 07/26/2016 04:16 PM, mukesh tiwari wrote:
> 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.