Return to Question

I'm fairly new to the Coq language and I want to prove a function that does an binary add from numbers represented as a list (least significant bit upfront).

I have created this badd function that does that and now I want to prove it

Fixpoint badd (l1 l2: list bool): list bool := 
  match l1,l2 with
    | [],_ => l2
    | _,[] => l1
    | x :: l1', y :: l2' => 
         match x,y with
          | true,true => false :: badd l1' (bsucc l2')
          | true,false => true :: badd l1' l2'
          | false,true => true :: badd l1' l2'
          | false,false => false :: badd l1' l2'
        end
end.

I'm fairly new to the Coq language and I want to prove a function that does an binary add from numbers represented as a list (least significant bit upfront).

I have created this badd function that does that and now I want to prove it

Fixpoint badd (l1 l2: list bool): list bool := 
  match l2 with
  | [] => l1
  | true :: l2 =>  bsucc (badd (badd l1 l2) l2)
  | false :: l2 => badd (badd l1 l2) l2
  end.

Here is my proof so far (value give the decimal value of the binary number) :

Lemma baddOK: forall l1 l2, value (badd l1 l2) = value l1 + value l2.
Proof.
  intros l1 l2.
  generalize dependent l1.
  induction l2; auto.
  rewrite IHl2. (* this fail *)


Admitted.

The problem I have now is that I have IHl2 that correspond to

IHl2: forall l1 : list bool, value (badd l1 l2) = value l1 + value l2

And my goal is :

forall l1 : list bool, value (badd l1 (a :: l2)) = value l1 + value (a :: l2)

The problem is that I can't rewrite using IHl2 as the generic part of it (i.e. l1) does not match with l3 (i.e. a::l2) but with l1 itself.

Here is the value function to be able to follow the proof:

Fixpoint value (l: list bool) :=
  match l with
  | [] => 0
  | true :: l => 2 * (value l) + 1
  | false :: l => 2 * (value l)
  end.

I'm fairly new to the Coq language and I want to prove a function that does an binary add from numbers represented as a list (least significant bit upfront).

I have created this badd function that does that and now I want to prove it

Fixpoint badd (l1 l2: list bool): list bool := 
  match l2 with
  | [] => l1
  | true :: l2 =>  bsucc (badd (badd l1 l2) l2)
  | false :: l2 => badd (badd l1 l2) l2
  end.

Here is my proof so far (value give the decimal value of the binary number) :

Lemma baddOK: forall l1 l2, value (badd l1 l2) = value l1 + value l2.
Proof.
  intros l1 l2.
  generalize dependent l1.
  induction l2; auto.
  rewrite IHl2. (* this fail *)


Admitted.

The problem I have now is that I have IHl2 that correspond to

IHl2: forall l1 : list bool, value (badd l1 l2) = value l1 + value l2

And my goal is :

forall l1 : list bool, value (badd l1 (a :: l2)) = value l1 + value (a :: l2)

The problem is that I can't rewrite using IHl2 as the generic part of it (i.e. l1) does not match with l3 (i.e. a::l2) but with l1 itself.

Here is the value function to be able to follow the proof:

Fixpoint value (l: list bool) :=
  match l with
  | [] => 0
  | true :: l => 2 * (value l) + 1
  | false :: l => 2 * (value l)
  end.

I'm fairly new to the Coq language and I want to prove a function that does an binary add from numbers represented as a list (least significant bit upfront).

I have created this badd function that does that and now I want to prove it

Fixpoint badd (l1 l2: list bool): list bool := 
  match l1,l2 with
    | [],_ => l2
    | _,[] => l1
    | x :: l1', y :: l2' =>  
        match x,y with
          | true,true => false :: badd l1' (bsucc l2')
          | true,false => true :: badd l1' l2'
          | false,true => true :: badd l1' l2'
          | false,false => false :: badd l1' l2'
        end
end.

I'm fairly new to the Coq language and I want to prove a function that does an binary add from numbers represented as a list (least significant bit upfront).

I have created this badd function that does that and now I want to prove it

Fixpoint badd (l1 l2: list bool): list bool := 
  match l2 with
  | [] => l1
  | true :: l2 =>  bsucc (badd (badd l1 l2) l2)
  | false :: l2 => badd (badd l1 l2) l2
  end.

Here is my proof so far (value give the decimal value of the binary number) :

Lemma baddOK: forall l1 l2, value (badd l1 l2) = value l1 + value l2.
Proof.
  intros l1 l2.
  generalize dependent l1.
  induction l2; auto.
  rewrite IHl2.


Admitted.

Here is the value function to be able to follow the proof:

Fixpoint value (l: list bool) :=
  match l with
  | [] => 0
  | true :: l => 2 * (value l) + 1
  | false :: l => 2 * (value l)
  end.
```

I'm fairly new to the Coq language and I want to prove a function that does an binary add from numbers represented as a list (least significant bit upfront).

I have created this badd function that does that and now I want to prove it

Fixpoint badd (l1 l2: list bool): list bool := 
  match l2 with
  | [] => l1
  | true :: l2 =>  bsucc (badd (badd l1 l2) l2)
  | false :: l2 => badd (badd l1 l2) l2
  end.

Here is my proof so far (value give the decimal value of the binary number) :

Lemma baddOK: forall l1 l2, value (badd l1 l2) = value l1 + value l2.
Proof.
  intros l1 l2.
  generalize dependent l1.
  induction l2; auto.
  rewrite IHl2. (* this fail *)


Admitted.

The problem I have now is that I have IHl2 that correspond to

IHl2: forall l1 : list bool, value (badd l1 l2) = value l1 + value l2

And my goal is :

forall l1 : list bool, value (badd l1 (a :: l2)) = value l1 + value (a :: l2)

The problem is that I can't rewrite using IHl2 as the generic part of it (i.e. l1) does not match with l3 (i.e. a::l2) but with l1 itself.

Here is the value function to be able to follow the proof:

Fixpoint value (l: list bool) :=
  match l with
  | [] => 0
  | true :: l => 2 * (value l) + 1
  | false :: l => 2 * (value l)
  end.