playground/coq/nat2listbool.v

Require List.

Fixpoint nat2bin_aux (n pw:nat): list bool :=
  match pw with
  | O =>
      match n with
      | O => List.cons false List.nil
      | _ => List.cons true List.nil
      end
  | S pw' =>
      let pwr := Nat.pow 2 pw in
      let qnt := Nat.div n pwr in
      let nxt := Nat.modulo n pwr in
      List.cons
        (if Nat.eqb qnt 0 then false
         else true)
        (nat2bin_aux nxt pw')
  end.
Definition nat2bin (n:nat): list bool := nat2bin_aux n (Nat.log2 n).


Fixpoint nat2bin_aux' (n pw:nat): list bool :=
  match pw with
  | O =>
      match n with
      | O => List.cons false List.nil
      | _ => List.cons true List.nil
      end
  | S pw' =>
      let pwr := Nat.pow 2 pw in
      let qnt := Nat.div n pwr in
      let nxt := Nat.modulo n pwr in
      List.app
        (nat2bin_aux' nxt pw')
        (if Nat.eqb qnt 0 then List.cons false List.nil
         else List.cons true List.nil)
  end.
Definition nat2bin' (n:nat): list bool := nat2bin_aux' n (Nat.log2 n).

Fixpoint bin2nat_aux (l:list bool) (pw:nat): nat :=
  match pw with
  | O =>
      match l with
      | List.cons true nil => 1
      | _ => 0
      end
  | S pw' =>
      let pwr := Nat.pow 2 pw in
      match l with
      | List.cons true xs => pwr + (bin2nat_aux xs pw')
      | List.cons false xs => bin2nat_aux xs pw'
      | _ => 0
      end
  end.
Definition bin2nat (l:list bool): nat := bin2nat_aux l ((List.length l)-1).

Fixpoint bin2nat_aux' (l:list bool) (pw:nat): nat :=
  match l with
  | List.cons true xs => Nat.pow 2 pw + (bin2nat_aux' xs (S pw))
  | List.cons false xs => bin2nat_aux' xs (S pw)
  | _ => 0
  end.
Definition bin2nat' (l:list bool): nat := bin2nat_aux' l 0.

Definition padList (n:nat) (l:list bool): list bool :=
  let sz := List.length l in
  if Nat.leb n sz then l
  else
    List.app (List.repeat false (n-sz)) l.

Definition padList' (n:nat) (l:list bool): list bool :=
  let sz := List.length l in
  if Nat.leb n sz then l
  else
    List.app l (List.repeat false (n-sz)).

Definition shiftl (n:nat) (l:list bool): list bool :=
  List.app (List.skipn n l) (List.repeat false n).
(*
Definition shiftr (l:list bool): list bool :=
  List.cons false ().
 *)

Compute shiftl 2 (List.cons true List.nil).

Compute shiftl 0 (nat2bin 10).
Compute shiftl 1 (nat2bin 10).
Compute shiftl 2 (nat2bin 10).
Compute shiftl 3 (nat2bin 10).

(****************** Trying out... ***************)

Compute nat2bin 0.
Compute nat2bin 1.
Compute nat2bin 2.
Compute nat2bin 3.
Compute nat2bin 4.
Compute nat2bin 5.
Compute nat2bin 6.
Compute nat2bin 7.
Compute nat2bin 8.
Compute nat2bin 9.
Compute nat2bin 10.
(* = (true :: false :: true :: false :: nil)%list *)

Compute padList 4 (nat2bin 0).
Compute padList 4 (nat2bin 1).
Compute padList 4 (nat2bin 2).
Compute padList 4 (nat2bin 3).
Compute padList 4 (nat2bin 4).
Compute padList 4 (nat2bin 5).
Compute padList 4 (nat2bin 6).
Compute padList 4 (nat2bin 7).
Compute padList 4 (nat2bin 8).
Compute padList 4 (nat2bin 9).
Compute padList 4 (nat2bin 10).
(* = (true :: false :: true :: false :: nil)%list *)

Compute bin2nat (nat2bin 0).
Compute bin2nat (nat2bin 1).
Compute bin2nat (nat2bin 2).
Compute bin2nat (nat2bin 3).
Compute bin2nat (nat2bin 4).
Compute bin2nat (nat2bin 5).
Compute bin2nat (nat2bin 6).
Compute bin2nat (nat2bin 7).
Compute bin2nat (nat2bin 8).
Compute bin2nat (nat2bin 9).
Compute bin2nat (nat2bin 10).
(* = 10 : nat *)

Compute bin2nat (padList 4 (nat2bin 0)).
Compute bin2nat (padList 4 (nat2bin 1)).
Compute bin2nat (padList 4 (nat2bin 2)).
Compute bin2nat (padList 4 (nat2bin 3)).
Compute bin2nat (padList 4 (nat2bin 4)).
Compute bin2nat (padList 4 (nat2bin 5)).
Compute bin2nat (padList 4 (nat2bin 6)).
Compute bin2nat (padList 4 (nat2bin 7)).
Compute bin2nat (padList 4 (nat2bin 8)).
Compute bin2nat (padList 4 (nat2bin 9)).
Compute bin2nat (padList 4 (nat2bin 10)).
(* = 10 : nat *)


Compute nat2bin' 0.
Compute nat2bin' 1.
Compute nat2bin' 2.
Compute nat2bin' 3.
Compute nat2bin' 4.
Compute nat2bin' 5.
Compute nat2bin' 6.
Compute nat2bin' 7.
Compute nat2bin' 8.
Compute nat2bin' 9.
Compute nat2bin' 10.
(* = (false :: true :: false :: true :: nil)%list *)

Compute bin2nat' (nat2bin' 0).
Compute bin2nat' (nat2bin' 1).
Compute bin2nat' (nat2bin' 2).
Compute bin2nat' (nat2bin' 3).
Compute bin2nat' (nat2bin' 4).
Compute bin2nat' (nat2bin' 5).
Compute bin2nat' (nat2bin' 6).
Compute bin2nat' (nat2bin' 7).
Compute bin2nat' (nat2bin' 8).
Compute bin2nat' (nat2bin' 9).
Compute bin2nat' (nat2bin' 10).
(* = 10 : nat *)

Compute bin2nat' (padList' 4 (nat2bin' 0)).
Compute bin2nat' (padList' 4 (nat2bin' 1)).
Compute bin2nat' (padList' 4 (nat2bin' 2)).
Compute bin2nat' (padList' 4 (nat2bin' 3)).
Compute bin2nat' (padList' 4 (nat2bin' 4)).
Compute bin2nat' (padList' 4 (nat2bin' 5)).
Compute bin2nat' (padList' 4 (nat2bin' 6)).
Compute bin2nat' (padList' 4 (nat2bin' 7)).
Compute bin2nat' (padList' 4 (nat2bin' 8)).
Compute bin2nat' (padList' 4 (nat2bin' 9)).
Compute bin2nat' (padList' 4 (nat2bin' 10)).