coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Dirk Pattinson <dirk.pattinson AT anu.edu.au>
- To: <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] Non linear recursion
- Date: Wed, 27 Jul 2016 09:23:40 +1000
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=dirk.pattinson AT anu.edu.au; spf=Pass smtp.mailfrom=dirk.pattinson AT anu.edu.au; spf=Pass smtp.helo=postmaster AT APC01-SG2-obe.outbound.protection.outlook.com
- Ironport-phdr: 9a23:ZrmClBJ4HtbOHIZMiNmcpTZWNBhigK39O0sv0rFitYgUKfXxwZ3uMQTl6Ol3ixeRBMOAuqoC1bad6vyocFdDyK7JiGoFfp1IWk1NouQttCtkPvS4D1bmJuXhdS0wEZcKflZk+3amLRodQ56mNBXsq3G/pQQfBg/4fVIsYL+kQsiM04/ui6ibwN76W01wnj2zYLd/fl2djD76kY0ou7ZkMbs70RDTo3FFKKx8zGJsIk+PzV6nvp/jtM0rzyMF7/km7otLVbjwV6U+V71RSjo8ZTMb/sru4DXCVwjH3nIATmQQiR1OS1zJ7Qv5GI/4rjf7sPF63gGTO9CwQLwpHz2/ufQ4ACT0gTsKYmZquFrcjdZ92fpW
- Spamdiagnosticmetadata: NSPM
- Spamdiagnosticoutput: 1:99
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.
- [Coq-Club] Non linear recursion, mukesh tiwari, 07/26/2016
- Re: [Coq-Club] Non linear recursion, Dirk Pattinson, 07/27/2016
Archive powered by MHonArc 2.6.18.