1 files changed, 88 insertions, 0 deletions
diff --git a/coq/padic.v b/coq/padic.v
new file mode 100644
index 0000000..af28184
--- /dev/null
+++ b/coq/padic.v
@@ -0,0 +1,88 @@
+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)).