CODEWITHSUNDEEP
coq
Marko Grdinić
Marko Grdinić

Reputation: 4062

How to prove binary commutavity with a different definition of bin?

// Collacoq link: https://x80.org/collacoq/qezicaroni.coq

Inductive bin : Type :=
| Zero : bin
| One : bin
| ZeroP : bin -> bin
| OneP : bin -> bin.

Inductive bin_carry : Type :=
| ZeroC : bin_carry
| OneC : bin_carry.

(*returns carry, new_state*)
Fixpoint incr' (x : bin) : bin_carry * bin :=
  match x with
  | Zero => (ZeroC, One)
  | One => (OneC, Zero)
  | ZeroP x =>
    match incr' x with
    | (OneC, x') => (ZeroC, OneP x')
    | (ZeroC, x') => (ZeroC, ZeroP x')
    end
  | OneP x =>
    match incr' x with
    | (OneC, x') => (OneC, ZeroP x')
    | (ZeroC, x') => (ZeroC, OneP x')
    end
  end.


Definition incr (x : bin): bin :=
  match incr' x with
  | (ZeroC,x) => x
  | (OneC,x) => OneP x
  end.

(*index_multiplier * result*)
Fixpoint bin_to_nat' (x : bin): nat * nat :=
  match x with
  | Zero => (2,0)
  | One => (2,1)
  | ZeroP x =>
    match bin_to_nat' x with
    | (multiplier,result) => (multiplier * 2,result)
    end
  | OneP x =>
    match bin_to_nat' x with
    | (multiplier,result) => (multiplier * 2,result + multiplier)
    end
  end.


Definition bin_to_nat (x : bin): nat :=
  match bin_to_nat' x with
  | (_,r) => r
  end.

Example bin_test1: bin_to_nat Zero = 0.
Proof. reflexivity. Qed.
Example bin_test2: bin_to_nat (incr Zero) = 1.
Proof. reflexivity. Qed.
Example bin_test3: bin_to_nat (incr (incr Zero)) = 2.
Proof. reflexivity. Qed.
Example bin_test4: bin_to_nat (incr (incr (incr Zero))) = 3.
Proof. reflexivity. Qed.
Example bin_test5: bin_to_nat (incr (incr (incr (incr Zero)))) = 4.
Proof. reflexivity. Qed.

Theorem binary_commute :
  forall (x: bin),
    bin_to_nat(incr x) = S (bin_to_nat x).
Proof. induction x.
       - reflexivity.
       - reflexivity.
       - replace (ZeroP x) with x.
         + rewrite -> IHx. reflexivity.
         + induction x.
           * Abort.

I am going through the Software Foundations book and am stumped on the above. I looked around on the net and found the solution for a different kind of bin formulation, but I do not think the solution there applies here.

The trouble is that in the third - bullet bin_to_nat (incr (ZeroP x)) = S (bin_to_nat (ZeroP x) will not simplify and neither it can be rewritten directly. So after learning about replace I thought that might work, but then I get stuck trying to prove Zero = ZeroP Zero.

I know the problem states that I am free to change the formulation of bin to make proving its commutativity easier, but my hunch is that I am not going to get far with Coq if I get stuck at the above definition. Though unlike the past few times, I do not think I have the tools to get past this yet.

What am I missing here?

Upvotes: 2

Views: 188

Answers (1)

gallais
gallais

Reputation: 12093

replace (ZeroP x) with x. cannot succeed: for such an equation to hold x would need to be an infinite term equal to ZeroP (ZeroP (ZeroP (...))). What you may want to prove first is that incr is extensional semantically. i.e.

Theorem incr_ext : forall (x y : bin),
  bin_to_nat x = bin_to_nat y -> bin_to_nat (incr x) = bin_to_nat (incr y).

Upvotes: 3

Related Questions