binary number stuff

gistfile1.coq

(* Exercise: 4 stars, recommended (binary)                                                                                                                              
Consider a different, more efficient representation of natural numbers using a binary                                                                                   
rather than unary system. That is, instead of saying that each natural number is either                                                                                 
zero or the successor of a natural number, we can say that each binary number is either                                                                                 
                                                                                                                                                                        
    zero,                                                                                                                                                               
    twice a binary number, or                                                                                                                                           
    one more than twice a binary number.                                                                                                                                
                                                                                                                                                                        
(a) First, write an inductive definition of the type bin corresponding to this                                                                                          
description of binary numbers.                                                                                                                                          
(Hint: recall that the definition of nat from class,                                                                                                                    
    Inductive nat : Type :=                                                                                                                                             
      | O : nat                                                                                                                                                         
      | S : nat → nat.                                                                                                                                                  
says nothing about what O and S "mean". It just says "O is a nat (whatever that is),                                                                                    
and if n is a nat then so is S n". The interpretation of O as zero and S as                                                                                             
successor/plus one comes from the way that we use nat values, by writing functions to                                                                                   
do things with them, proving things about them, and so on. Your definition of bin should                                                                                
be correspondingly simple; it is the functions you will write next that will give it                                                                                    
mathematical meaning.) *)

Inductive bin : Type :=
| inf : bin
| zero : bin -> bin
| one : bin -> bin.

(* (b) Next, write an increment function for binary numbers, and a function to convert                                                                                  
binary numbers to unary numbers. *)

(* inf                                                                                                                                                                  
   zero inf : 0                                                                                                                                                         
   one inf : 1                                                                                                                                                          
   one (zero inf) : 2                                                                                                                                                   
   one (one inf) : 3                                                                                                                                                    
one (one inf) -> one (inc (one inf)) -> one (one (inc inf)) -> one (one (zero inf))                                                                                     
odd (odd O) -> even                                                                                                                                                     
   one (zero (zero inf)) : 4                                                                                                                                            
*)

Fixpoint incbin (n : bin) : bin :=
match n with
| inf => one inf
| zero nn => one nn
| one nn => zero (incbin nn)
end.

Example incbin_test : incbin (one (one inf)) = zero (zero (one inf)).
Proof. reflexivity. Qed.

Definition incnat (n : nat) : nat := S n.

Fixpoint bin_to_un (n : bin) : nat :=
match n with
| inf => O
| zero nn => mult 2 (bin_to_un nn)
| one nn => plus 1 (mult 2 (bin_to_un nn))
end.

Example test_bin_un1 : bin_to_un (zero (one (zero (one inf)))) = 10.
Proof. reflexivity. Qed.

Example test_bin_un2 : un_to_bin 14 = zero (one (one (one inf))).
Proof. simpl. reflexivity. Qed.

(* (c) Finally, prove that your increment and binary-to-unary functions commute: that is, incrementing a binary number and then converting it to unary yields the same \
result as first converting it to unary and then incrementing. *)

Theorem inc_un_comm : forall (m : bin),
                        bin_to_un (incbin m) = incnat (bin_to_un m).
Proof.
  intro m. induction m as [|m1 |m2].
  reflexivity.
  simpl. reflexivity.
  simpl. rewrite -> IHm2. unfold incnat. rewrite <- plus_n_Sm.
  assert (H : S (bin_to_un m2) + bin_to_un m2 = bin_to_un m2 + S (bin_to_un m2)).
   apply plus_comm.
  rewrite -> H. rewrite <- plus_n_Sm. reflexivity.
Qed.

(* Exercise: 5 stars, advanced (binary_inverse) *)                                                                                                                      
(* This exercise is a continuation of the previous exercise about binary numbers. You will need your definitions and theorems from the previous exercise to complete th\
is one.                                                                                                                                                                 
(a) First, write a function to convert natural numbers to binary numbers. Then prove that starting with any natural number, converting to binary, then converting back \
yields the same natural number you started with. *)                                                                                                                     
                                                                                                                                                                        
Check un_to_bin.                                                                                                                                                        
                                                                                                                                                                        
Theorem incbin_un : forall b, bin_to_un (incbin b) = S (bin_to_un b).                                                                                                   
Proof.                                                                                                                                                                  
  intros b. induction b as [|zero|one].                                                                                                                                 
  simpl. reflexivity.                                                                                                                                                   
  simpl. reflexivity.                                                                                                                                                   
  simpl. rewrite -> IHone. simpl. rewrite <- plus_n_Sm. reflexivity.                                                                                                    
Qed.                                                                                                                                                                    
                                                                                                                                                                        
Theorem nat_to_bin_back : forall n : nat,                                                                                                                               
                            bin_to_un (un_to_bin n) = n.                                                                                                                
Proof.                                                                                                                                                                  
  intro n. induction n as [|nn].                                                                                                                                        
  simpl. reflexivity.                                                                                                                                                   
  simpl. rewrite -> incbin_un. rewrite -> IHnn. reflexivity.                                                                                                            
Qed.   


(* (b) You might naturally think that we should also prove the opposite direction: that starting with a binary number, converting to a natural, and then back to binary\
 yields the same number we started with. However, it is not true! Explain what the problem is. *)                                                                       
                                                                                                                                                                        
Fixpoint plus_bin (b1 : bin) (b2 : bin) (carry : bool) : bin :=                                                                                                         
  match b1 with                                                                                                                                                         
    | inf => match b2 with                                                                                                                                              
               | inf => if carry then one inf else zero inf                                                                                                             
               | _ => if carry then one b2 else b2                                                                                                                      
             end                                                                                                                                                        
    | zero n => match b2 with                                                                                                                                           
                  | inf => b1                                                                                                                                           
                  | zero m => if carry then one (plus_bin n m false) else zero (plus_bin n m true)                                                                      
                  | one m => if carry then zero (plus_bin n m true) else one (plus_bin n m false)                                                                       
                end                                                                                                                                                     
    | one n => match b2 with                                                                                                                                            
                 | inf => if carry then one b1 else b1                                                                                                                  
                 | zero m => if carry then zero (plus_bin n m true) else one (plus_bin n m false)                                                                       
                 | one m => if carry then one (plus_bin n m true) else zero (plus_bin n m true)                                                                         
               end                                                                                                                                                      
  end.                                                                                                                                                                  
                                                                                                                                                                        
Notation "x +b y" := (plus_bin x y false) (at level 50, left associativity) : nat_scope.                                                                                
                                                                                                                                                                        
Example plus_bin_test1 : (un_to_bin 5) +b (un_to_bin 7) = (un_to_bin 12).                                                                                               
Proof. simpl. reflexivity. Qed.                                                                                                                                         
Example plus_bin_test2 : (un_to_bin 8) +b (un_to_bin 3) = (un_to_bin 11).                                                                                               
Proof. simpl. reflexivity. Qed.                                                                                                                                         
                                                                                                                                                                        
Theorem remove_zero_bin : forall p q,                                                                                                                                   
                            p = q -> zero p = zero q.                                                                                                                   
Proof. intros p q H.                                                                                                                                                    
  rewrite -> H. reflexivity.                                                                                                                                            
Qed.    

Theorem bin_double_zero : forall m,                                                                                                                                     
                              zero m = m +b m.                                                                                                                          
Proof. intro m. induction m as [|p|q].                                                                                                                                  
  Case "inf". simpl. reflexivity.                                                                                                                                       
  Case "zero". simpl. rewrite -> IHp. apply remove_zero_bin. symmetry.                                                                                                  
Admitted.


=>eorem bin_to_nat_back : forall b : bin,                                                                                                                               
                            un_to_bin (bin_to_un b) = b.
Proof.
  intro b. induction b as [|n|m].
  Case "inf". simpl. reflexivity.
  Case "zero". simpl.
Admitted.
(* I'm going to guess that this has something to do with how you don't know where the zero in a binary                                                                  
number comes from? Like, it could come from adding two zeros or it could come from adding two ones?                                                                     
Maybe this makes the structure difficult for using induction? *)

(* (c) Define a function normalize from binary numbers to binary numbers such that for any binary number b, converting to a natural and then back to binary yields (nor\
malize b). Prove it.                                                                                                                                                    
Again, feel free to change your earlier definitions if this helps here. *)