From 84ad8d9897278bf64e153a2a5ec848800652890c Mon Sep 17 00:00:00 2001
From: Michael Sippel <micha@fragmental.art>
Date: Wed, 24 Jul 2024 11:20:43 +0200
Subject: [PATCH] coq: add some examples of bb-encoding

---
 coq/bbencode.v | 74 ++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 74 insertions(+)
 create mode 100644 coq/bbencode.v

diff --git a/coq/bbencode.v b/coq/bbencode.v
new file mode 100644
index 0000000..155f605
--- /dev/null
+++ b/coq/bbencode.v
@@ -0,0 +1,74 @@
+
+
+(*  let bb_zero = Λα ↦ λs: α->α ↦ λz: α ↦ z
+ *                ∀α.(α->α)->α->α
+*)
+Definition bb_zero : expr :=
+  (expr_ty_abs "α"
+    (expr_tm_abs "s" (type_fun (type_var "α") (type_var "α"))
+      (expr_tm_abs "z" (type_var "α")
+        (expr_var "z")))).
+
+(*  let bb_one = Λα ↦ λs: α->α ↦ λz: α ↦ s z
+*)
+Definition bb_one : expr :=
+  (expr_ty_abs "α"
+    (expr_tm_abs "s" (type_fun (type_var "α") (type_var "α"))
+      (expr_tm_abs "z" (type_var "α")
+        (expr_tm_app (expr_var "s") (expr_var "z"))))).
+
+(*  let bb_two = Λα ↦ λs: α->α ↦ λz: α ↦ s (s z)
+*)
+Definition bb_two : expr :=
+  (expr_ty_abs "α"
+    (expr_tm_abs "s" (type_fun (type_var "α") (type_var "α"))
+      (expr_tm_abs "z" (type_var "α")
+        (expr_tm_app (expr_var "s") (expr_tm_app (expr_var "s") (expr_var "z")))))).
+
+
+Definition bb_succ : expr :=
+  (expr_tm_abs "n" (type_rung (type_id "ℕ")
+                    (type_rung (type_id "BBNat")
+                     (type_abs "α"
+                      (type_fun (type_fun (type_var "α") (type_var "α"))
+                         (type_fun (type_var "α") (type_var "α"))))))
+
+       (expr_ascend (type_rung (type_id "ℕ") (type_id "BBNat"))
+          (expr_ty_abs "α"
+            (expr_tm_abs "s" (type_fun (type_var "α") (type_var "α"))
+              (expr_tm_abs "z" (type_var "α")
+                (expr_tm_app (expr_var "s")
+                  (expr_tm_app (expr_tm_app
+                      (expr_ty_app (expr_var "n") (type_var "α"))
+                      (expr_var "s"))
+                    (expr_var "z")))))))).
+
+Definition e1 : expr :=
+  (expr_let "bb-zero" (type_rung (type_id "ℕ")
+                        (type_rung (type_id "BBNat")
+                          (type_abs "α"
+                            (type_fun (type_fun (type_var "α") (type_var "α"))
+                              (type_fun (type_var "α") (type_var "α"))))))
+                       bb_zero
+                       (expr_tm_app (expr_tm_app (expr_var "+") (expr_var "bb-zero")) (expr_var "bb-zero"))
+  ).
+
+Definition t1 : expr := (expr_tm_app (expr_var "x") (expr_var "x")).
+
+Compute (expr_subst "x"
+    (expr_ty_abs "α" (expr_tm_abs "a" (type_var "α") (expr_var "a")))
+    bb_one
+).
+
+Example  example_let_reduction :
+    e1 -->β  (expr_tm_app (expr_tm_app (expr_var "+") bb_zero) bb_zero).
+Proof.
+    apply E_AppLet.
+Qed.
+
+Compute     (expr_tm_app bb_succ bb_zero) -->β bb_one.
+
+Example  example_succ :
+    (expr_tm_app bb_succ bb_zero) -->β bb_one.
+Proof.
+Admitted.