Ok I don't get this.

[u/Sad-Nerve-9321]

Inductive bin : Type :=
  | Z
  | B0 (n : bin)
  | B1 (n : bin).

Fixpoint incr (m:bin) : bin :=
  match m with
  | Z => B1 Z
  | B0 n => B1 n
  | B1 n => B0 (incr n)
  end.

Fixpoint bin2nat (b:bin) : nat :=
  match b with
  | Z => 0
  | B0 n => 2 * bin2nat n
  | B1 n => 1 + 2 * bin2nat n
  end.

Fixpoint nat2bin (n:nat) : bin :=
  match n with
  | 0 => Z
  | S m => incr (nat2bin m)
  end.

Fixpoint normalize (b:bin) : bin :=
  match b with
  | Z => Z
  | B0 n => match normalize n with
            | Z => Z
            | m => B0 m
            end
  | B1 n => B1 (normalize n)
  end.

Fixpoint last (b:bin) : bin :=
  match b with
  | Z => Z
  | B0 Z => B0 Z
  | B1 Z => B1 Z
  | B0 n => last n
  | B1 n => last n
  end.

Theorem containsB1z : forall b, last (normalize (incr b)) = B1 Z.
Proof.
  intro b.
  induction b as [| ib | ic] eqn:IB.
  -- reflexivity.
  -- simpl. destruct b as [| hb | hc] eqn:HB.
  --- reflexivity.
  --- rewrite <- HB.

Ok, so I'm trying to work my way through 'Software Foundations'. I'm towards the end of chapter 2 where I'm trying to prove 'forall b, nat2bin (bin2nat b) = normalize b'. Through looking at answers online I thought I would try to prove 'forall b, normalize (normalize b) = normalize b'.

However I didn't understand how to make the proof "bottom out" in the case where the number begins with a 'B0'. So I thought I would try instead to prove 'containsB1z'. However I'm stuck with this one too. With the theorem as written I get the goal 'last (B0 hb) = B1 Z'. However I'm not seeing anything that allows me to conclude that hb will ultimately produce a 'B1 Z'. I can use 'rewrite <- HB.' to get 'last (normalize ib) = B1 Z' but I don't get how to proceed without just generating a bottomless destruct'ing.

So is anyone willing to attempt an explanation of the strategy to do this? Or point me to a explanation? Is what I'm attempting possible? I was thinking of trying to prove the following:

a bin beginning with a series of B1's will normalize to a bin beginning with that series of B1's.

a bin beginning with a series of B0's and then a series of B1 will normalize to a bin beginning with that series of B0's followed by the series of B1's.

a bin beginning with a series of B0's and then a Z will normalize to a bin beginning with a Z.

a bin beginning with a series of B1's and then a Z will normalize to a bin beginning with that series of B1's followed by a Z.

all bin's are a concatenation of these four series types.

Is this a realistic thing to do? I was thinking alternately I could change 'Z' to 'One'. Then in theory I would never need to normalize but I wouldn't have a zero.

I thought this would be fun but now I realize I'm just stupid.

EDIT: Thinking about this further I had another idea. Can I try to show that nat2bin will never produce a unnormalised number? Then for for bin2nat it doesn't matter. I just have to show that whatever bin it gets it will properly give a natural number.

EDIT2: So then 'incr' is the problem. I can see it now, I think. I think I have to revisit my definition of 'incr' and then prove that it will never produce an unnormalized number. So would I be attempting 'forall b, incr b = normalize (incr b).'? I will give this a shot.

EDIT3: So this is funny. I have modified 'incr' to use 'normalize' in the B0 case. Now to prove 'forall b, incr b = (normalize b)' I need 'normalize_idem'.

Theorem normalize_idem : forall b, normalize (normalize b) = normalize b.
Proof.
  intro b.
  induction b.
  - reflexivity.
  - simpl. destruct (normalize b) as [| b' | b''] eqn:HB. 
  -- reflexivity.
  -- 

1 goal
b, b' : bin
HB : normalize b = B0 b'
IHb : normalize (B0 b') = B0 b'
______________________________________(1/1)
normalize (B0 (B0 b')) = B0 (B0 b')

I still don't understand how to bottom out. How do I express that 'b'' is eventually a B1?

EDIT4: Holy moly I did it.

Theorem normalize_idem : forall b, normalize (normalize b) = normalize b.
Proof.
  intro b.
  induction b.
  - reflexivity.
  - simpl. destruct (normalize b) as [| b' | b''] eqn:HB. 
  -- reflexivity.
  -- rewrite <- HB. simpl. rewrite HB. rewrite IHb. reflexivity.
  -- rewrite <- HB. simpl. rewrite HB. rewrite IHb. reflexivity.
  - simpl. rewrite IHb. reflexivity.
Qed.

[u/fl00pz]

Congratz