6
$\begingroup$

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.
Improve this question
$\endgroup$
3
  • $\begingroup$ Have you proved that value (bsucc l) = 1 + value l ? $\endgroup$
    – Trebor ♦
    Commented Apr 15, 2022 at 15:11
  • 1
    $\begingroup$ Since the function badd matches on l2 and not l1, the rule of thumb is induction on l2: This "fits" the structure of the function, and is more likely to work. (Don't forget to generalize l1 before you make the induction.) $\endgroup$
    – Trebor ♦
    Commented Apr 15, 2022 at 15:16
  • $\begingroup$ If you want people to easily replay your proofs, you should give your whole context. For instance, here we lack the definition of value to be able to follow. $\endgroup$
    – Meven Lennon-Bertrand ♦
    Commented Apr 15, 2022 at 16:15

2 Answers 2

Reset to default
3
$\begingroup$

If you can change your definition of badd, then you can try swapping l1 and l2, which is in my opinion more natural:

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

But anyway let's use the original badd. The ultimate way to prove anything is to prove it with pen and paper first. After all, if you can't convince a human, you will never convince your computer! So if you do an induction on l2, there will be three cases:

  • l2 is the empty list. In this case you get value l1 = value l1 + O, which you probably already proved.
  • l2 begins with false, say false :: l3. In this case you need to prove value (badd (badd l1 l3) l3) = value l1 + (value l3 + value l3). (You didn't post the definition of value, but it will be similar.) In this case, you already decomposed l2, and therefore you can use the induction hypothesis, which should be value (badd l1 l3) = value l1 + value l3. But now there is a problem applying this hypothesis, because you have value (badd (badd l1 l3) l3), and the first addend is not l1!

This is where the generalization comes in. Since you only matched l2, you should only be doing induction on l2, and the induction hypothesis should range over all l1. This is to say, the induction hypothesis should be IH : forall l, value (badd l l3) = value l + value l3. This would work, because now you can rewrite twice with IH (badd l1 l3) and IH l1, and finish the goal.

Therefore, before performing the tactic induction l2, your goal should be forall l1, value (badd l1 l2) = value l1 + value l2, note the forall! To do this, use the tactic generalize l1 before you do the induction.

Improve this answer
$\endgroup$
2
  • $\begingroup$ @louga31 As I said, there is three cases. I did not write the third, because I trust that you can figure it out if you write down a pen and paper proof. Look at my three cases, can you see what you forgot to do? (Hint: Pen and paper proof is essential.) $\endgroup$
    – Trebor ♦
    Commented Apr 16, 2022 at 15:12
  • $\begingroup$ @louga31 Do you mean unfold? $\endgroup$
    – Trebor ♦
    Commented Apr 17, 2022 at 0:42
2
$\begingroup$

In this case you can use functional induction and automated solvers.

Unfortunately, functional induction doesn't work well over dependent types. The popular Equations plugin works better with dependent types but has its own weirdness.

Also this sort of approach isn't necessarily very edifying unless maybe you write the reflection code yourself.

Certified Programming with Dependent Types gives an introduction to proof by reflection although I don't really feel the approach is very structured. Personally I like to structure proof by reflection around free objects but I still don't really feel I have a fully cohesive grasp of the concept. Unfortunately while the free object for simple cases like monoids is simple and just a list free objects for more complicated cases like rings are more complicated and might require quotients or setoids.

Require Coq.Lists.List.

Require Import FunInd.
Require Import Psatz.
Require Import Coq.Arith.PeanoNat.

Import List.ListNotations.

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

Function bsucc l :=
  match l with
  | [] => [true]
  | false :: t => true :: t
  | true :: t => false :: bsucc t
  end%list.

Function 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 %list.

Lemma bsucc_correct l: value (bsucc l) = 1 + value l.
Proof.
  cbn.
  functional induction (bsucc l).
  all: cbn.
  all: lia.
Qed.

Lemma badd_correct l r: value (badd l r) = value l + value r.
Proof.
  cbn.
  functional induction (badd l r).
  all: cbn.
  all: try rewrite bsucc_correct.
  all: lia.
Qed.
Improve this answer
$\endgroup$