coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] A Question on Recursive Functions.

chronological Thread

From: Babak Moazzez <babakmoazzez AT yahoo.com>
To: coq-club AT inria.fr
Subject: [Coq-Club] A Question on Recursive Functions.
Date: Thu, 7 Jan 2010 18:15:10 -0800 (PST)
Domainkey-signature: a=rsa-sha1; q=dns; c=nofws; s=s1024; d=yahoo.com; h=Message-ID:X-YMail-OSG:Received:X-Mailer:Date:From:Subject:To:MIME-Version:Content-Type; b=LFQIPQDG6t1i+D7qAji6g8aI2G8SeGEUXy9PIxP/c+PWuGm+axwABeUoc6Mhh0ogsuNochcuGp3+QBAmgm1/XObT2TI74cSme/4FZLulTC7MfuZYPdLZrdv9XxQKIPASLWycgKobGpNV9cFNO+qWoGrBfVWVVlttNtRbbX0TGr8=;

Hi.

I have defined two functions in Coq: "add" and "mult" recursively.

they are functions for lists of pairs. a pair is like (a,b), and a list of pairs is like

(a_1,b_1)::(a_2,b_2):: ... ::(a_n, b_n)::nil

mult function multiplies each b_i by a constant m.

(a_1,m*b_1)::(a_2,m*b_2):: ... ::(a_n, m*b_n)::nil

add function adds two lists in this way:

suppose we have

l1 = (a_1,b_1)::(a_2,b_2):: ... ::(a_n, b_n)::nil

l2 = (a_1,b'_1)::(a'_2,b'_2):: ... ::(a'_n, b'_n)::nil

add function adds b_i's with a special rule and gives a new list of pairs.

now I want to prove that

mult m (add l1 l2) = add (mult m l1) (mult m l2)

but since both of my functions are recursively defined, I cannot prove it. Is there a special tactic for this?

Babak Moazzez
School of Mathematics and Statistics
Carleton University

Address:
Room 4356, Herzberg Building
Carleton University
1125 Colonel By Drive
Ottawa, ON K1S 5B6
Canada

Web: www.math.carleton.ca/~bmoazzez

Tel: 613 520 2600 Ext. 8789
Email: bmoazzez AT math.carleton.ca or babakmoazzez AT yahoo.com

Get your new Email address!
Grab the Email name you've always wanted before someone else does!

[Coq-Club] A Question on Recursive Functions., Babak Moazzez
- Re: [Coq-Club] A Question on Recursive Functions., Matthew Brecknell