CODEWITHSUNDEEP
coq
Tom And.
Tom And.

Reputation: 125

How to prove a theorem on natural numbers using Coq list

I'm new in Coq. To do practice on list and list of pairs, I used Coq list library to prove a simple theorem of natural numbers. I try to prove the simple property of natural numbers:

forall n, multiplier, a0....an, d1...dn: 
((a0*multiplier)=d1)+((a1*multiplier)=d2)+((a2*multiplier)=d3)+...+((an*multiplier)=dn) = result 
        ->    (a0+a1+a2+...+an) * multiplier = d1+d2+...+dn = result

((3*2)=6)+((5*2)=10)+((9*2)=18) = 34 -> (3+5+9)*2 = 6+10+18 = 34 can be an example of this property(i.e. n=3 and multiplier = 2).

I use list of pairs (storing a's in one list and d's in another list) to code this property in Coq as: 

Require Import List.

Fixpoint addnumbers (L : list nat) : nat :=
  match L with
      | nil    => 0
      | H::tail => H + addnumbers tail
  end.

Theorem resultAreEqual : forall (natListofpair :list (nat * nat)) 
(multiplier : nat) (result : nat),
Forall (fun '(a,d) => a * multiplier = d ) natListofpair ->  
 addnumbers(List.map (@fst nat  nat) natListofpair) * multiplier = result   ->
  addnumbers (List.map (@snd nat  nat) natListofpair) = result.

Proof.
intros.
destruct natListofpair.
subst. simpl. reflexivity.
rewrite <- H0.
inversion H.
destruct p. simpl.

But I don't know how I should continue this prove. I'm stuck in this proving for one week. I'd be thankful for your help.

Upvotes: 0

Views: 921

Answers (1)

Arthur Azevedo De Amorim
Arthur Azevedo De Amorim

Reputation: 23592

One reason you are having difficulty is that you have stated your lemma in an indirect way. When proving something in Coq, it is very important that you state it as simple as possible, as this often leads to easier proofs. In this case, the statement can become much simpler by using higher-order functions on lists.

Require Import Coq.Arith.PeanoNat.
Require Import Coq.Lists.List.

Definition sum (l : list nat) := fold_right Nat.add 0 l.

Lemma my_lemma l m : sum (map (Nat.mul m) l) = m * sum l.

The sum function is the equivalent of your addnumbers. The lemma says "the result of multiplying all numbers in l by m and adding them is the same as the result of adding them up first and multiplying by m later".

To prove this result, we need a crucial ingredient that your proof was missing: induction. This is often needed in Coq when we want to reason about objects of unbounded size, such as lists. Here is one possible proof.

Proof.
  unfold sum.
  induction l as [|x l IH]; simpl.
  - (* Nil case *)
    now rewrite Nat.mul_0_r.
  - (* Cons case *)
    now rewrite IH, Nat.mul_add_distr_l.
Qed.

Upvotes: 4

Related Questions