The Coq mailing list

[Pierre Casteran <pierre.casteran AT labri.fr>]

Hi,

 what do you precisely mean by "adding two lists together" ?
 Do you mean "appending" ?
  In this case, it is the "app" function from library List,

Fixpoint app {A:Type}(l l' : list A) : list A :=
match l with nil => l'
            | a::l'' => a::(app l'' l')
end.


If you mean "mapping addition elementwise", it is still a structural
recursion on lists.


 Fixpoint eltwise (l l':list nat) : list nat :=
    match l,l' with
       nil,l' => l'
     | l,nil => l
     | (a::l),(b::l') => (a+b)::(eltwise l l')
    end.


Anyway, as CHA Reeseo says, if you need to use a comparison in an  
if-then-else,
you need either a boolean function or a function returning a value of type
sumbool. For instance, with natural number, you may use :

beq_nat : nat -> nat -> bool

or

eq_nat_dec : forall n m:nat, {n=m}+{n <> m}.

Pierre








Quoting Babak Moazzez 
<babakmoazzez AT yahoo.com>:

> Hi.
>
> I am trying to define a function in Coq that adds two lists  
> together. for this purpose , I need to use a structure which is very  
> familiar in any programming language:
>
> if (p=q) then do ....
>
> but in Coq I cannot use this since (p=q) is not a boolean value but  
> just a proposition which needs to be proved if it is true.
>
> Can anybody tell me what to do?
>
> Thanks.
>  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
>
>
>       New Email names for you!
> Get the Email name you&#39;ve always wanted on the new @ymail and  
> @rocketmail.
> Hurry before someone else does!
> http://mail.promotions.yahoo.com/newdomains/aa/