Require Import Coq.Bool.Bool.
Require Import Coq.Lists.List.
Import ListNotations.

Local Open Scope list.

CoInductive padic : Type := padic_seq : bool -> padic -> padic.

CoFixpoint map (f: bool -> bool) (p: padic) :=
  match p with
  | padic_seq a b => padic_seq (f a) (map f b)
  end.

CoFixpoint shuffle (a b: padic): padic :=
  match a, b with
    padic_seq ahd atl, padic_seq bhd btl =>
      padic_seq ahd (padic_seq bhd (shuffle atl btl))
  end.

CoFixpoint zip (f: bool -> bool -> bool) (a b: padic): padic :=
  match a, b with
  | padic_seq a' a'', padic_seq b' b'' =>
    padic_seq (f a' b') (zip f a'' b'')
  end.

CoFixpoint zip3 (f: bool -> bool -> bool -> bool) (a b c: padic): padic :=
  match a, b, c with
  | padic_seq a' a'', padic_seq b' b'', padic_seq c' c'' =>
    padic_seq (f a' b' c') (zip3 f a'' b'' c'')
  end.

CoFixpoint zero : padic := padic_seq false zero.

Definition one : padic := padic_seq true zero.

CoFixpoint neg_one : padic := padic_seq true neg_one.

Definition memory (p: padic) := padic_seq false p.

Definition neg (p: padic) : padic := map negb p.

Definition inv_memory p := neg (memory (neg p)).

Definition full_add_s a b c := xorb (xorb a b) c.

Definition full_add_c a b c := (a && b) || (c && (xorb a b)).

Definition full_add (a b c: bool) : bool * bool :=
  (full_add_s a b c, full_add_c a b c).

CoFixpoint full_add_sum (a b c: padic) : padic :=
  match a, b, c with
  | padic_seq ah atl, padic_seq bh btl, padic_seq ch ctl =>
    padic_seq (xorb (xorb ah bh) ch) (full_add_sum atl btl ctl)
  end.

CoFixpoint full_add_carry (a b c: padic) : padic :=
  match a, b, c with
  | padic_seq ah atl, padic_seq bh btl, padic_seq ch ctl =>
    padic_seq ((ah && bh) || (ch && (xorb ah bh))) (full_add_carry atl btl ctl)
  end.

Definition add'' (a b: padic) : padic :=
  zip3 full_add_s a b (memory (zip3 full_add_c a b zero)).

CoFixpoint add' (c: bool) (a b: padic) : padic :=
  match a, b with
    padic_seq ahd atl, padic_seq bhd btl =>
      let (s, c') := full_add ahd bhd c in
      padic_seq s (add' c' atl btl)
  end.

Definition add : padic -> padic -> padic := add' false.

Fixpoint get (n: nat) (p: padic) : list bool :=
  match n, p with
  | S n', padic_seq ahd atl => ahd :: get n' atl
  | O, _ => nil
  end.

Definition negate a := add one (neg a).

Goal add one neg_one = zero.


Compute (get 4 (negate one)).
Compute (get 4 (shuffle neg_one zero)).
Compute (get 10 (add one neg_one)).