From fd916dda04f46e02f2f2b5541a9e162d5c8761a8 Mon Sep 17 00:00:00 2001
From: Michael Zhang <mail@mzhang.io>
Date: Tue, 22 Nov 2022 01:45:39 -0600
Subject: [PATCH] frap

---
 .gitignore     |   2 +
 frap.agda-lib  |   2 +
 src/Pset1.agda | 213 +++++++++++++++++++++++++++++++++++++++++++++++++
 src/Pset2.agda |  30 +++++++
 src/Pset3.agda |  38 +++++++++
 5 files changed, 285 insertions(+)
 create mode 100644 .gitignore
 create mode 100644 frap.agda-lib
 create mode 100644 src/Pset1.agda
 create mode 100644 src/Pset2.agda
 create mode 100644 src/Pset3.agda

diff --git a/.gitignore b/.gitignore
new file mode 100644
index 0000000..73cf8bf
--- /dev/null
+++ b/.gitignore
@@ -0,0 +1,2 @@
+*.agdai
+
diff --git a/frap.agda-lib b/frap.agda-lib
new file mode 100644
index 0000000..53c7164
--- /dev/null
+++ b/frap.agda-lib
@@ -0,0 +1,2 @@
+include: src
+depend: standard-library cubical
diff --git a/src/Pset1.agda b/src/Pset1.agda
new file mode 100644
index 0000000..f7f9c92
--- /dev/null
+++ b/src/Pset1.agda
@@ -0,0 +1,213 @@
+{-# OPTIONS --cubical #-}
+
+module Pset1 where
+
+open import Cubical.Foundations.Prelude
+open import Data.Bool
+open import Data.Nat
+open import Data.Empty
+open import Data.Product
+open import Relation.Nullary
+
+data Prog : Set where
+  Done : Prog
+  AddThen : ℕ → Prog → Prog
+  MulThen : ℕ → Prog → Prog
+  DivThen : ℕ → Prog → Prog
+  VidThen : ℕ → Prog → Prog
+  SetToThen : ℕ → Prog → Prog
+
+divmod : ℕ → ℕ → ℕ → ℕ → ℕ × ℕ
+divmod zero y q u = q ,′ u
+divmod (suc x) y q zero = divmod x y (suc q) y
+divmod (suc x) y q (suc u) = divmod x y q u
+
+_/_ : ℕ → ℕ → ℕ
+x / zero = zero
+x / (suc y) = proj₁ (divmod x y 0 y)
+
+neg : Bool → Bool
+neg true = false
+neg false = true
+
+neg-true : neg true ≡ false
+neg-true = refl
+
+neg-involutive : (b : Bool) → neg (neg b) ≡ b
+neg-involutive true = refl
+neg-involutive false = refl
+
+and : Bool → Bool → Bool
+and true true = true
+and _ _ = false
+
+and-comm : (x y : Bool) → and x y ≡ and y x
+and-comm true true = refl
+and-comm true false = refl
+and-comm false true = refl
+and-comm false false = refl
+
+and-true-r : (x : Bool) → and x true ≡ x
+and-true-r true = refl
+and-true-r false = refl
+
+run : Prog → ℕ → ℕ
+run Done state = state
+run (AddThen n prog) state = run prog (n + state)
+run (MulThen n prog) state = run prog (n * state)
+run (DivThen n prog) state = run prog (state / n)
+run (VidThen n prog) state = run prog (n / state)
+run (SetToThen n prog) _ = run prog n
+
+run-example-1 : run Done 0 ≡ 0
+run-example-1 = refl
+
+run-example-2 : run (MulThen 5 (AddThen 2 Done)) 1 ≡ 7
+run-example-2 = refl
+
+run-example-3 : run (SetToThen 3 (MulThen 2 Done)) 10 ≡ 6
+run-example-3 = refl
+
+num-instructions : Prog → ℕ
+num-instructions Done = 0
+num-instructions (AddThen x prog) = suc (num-instructions prog)
+num-instructions (MulThen x prog) = suc (num-instructions prog)
+num-instructions (DivThen x prog) = suc (num-instructions prog)
+num-instructions (VidThen x prog) = suc (num-instructions prog)
+num-instructions (SetToThen x prog) = suc (num-instructions prog)
+
+num-instructions-example : num-instructions (MulThen 5 (AddThen 2 Done)) ≡ 2
+num-instructions-example = refl
+
+concat-prog : Prog → Prog → Prog
+concat-prog Done q = q
+concat-prog (AddThen x p) q = AddThen x (concat-prog p q)
+concat-prog (MulThen x p) q = MulThen x (concat-prog p q)
+concat-prog (DivThen x p) q = DivThen x (concat-prog p q)
+concat-prog (VidThen x p) q = VidThen x (concat-prog p q)
+concat-prog (SetToThen x p) q = SetToThen x (concat-prog p q)
+
+concat-prog-example : concat-prog (AddThen 1 Done) (MulThen 2 Done) ≡ AddThen 1 (MulThen 2 Done)
+concat-prog-example = refl
+
+concat-prog-num-instructions : (p1 p2 : Prog) →
+  num-instructions (concat-prog p1 p2) ≡ num-instructions p1 + num-instructions p2
+concat-prog-num-instructions Done p2 = refl
+concat-prog-num-instructions (AddThen x p1) p2 = cong suc (concat-prog-num-instructions p1 p2)
+concat-prog-num-instructions (MulThen x p1) p2 = cong suc (concat-prog-num-instructions p1 p2)
+concat-prog-num-instructions (DivThen x p1) p2 = cong suc (concat-prog-num-instructions p1 p2)
+concat-prog-num-instructions (VidThen x p1) p2 = cong suc (concat-prog-num-instructions p1 p2)
+concat-prog-num-instructions (SetToThen x p1) p2 = cong suc (concat-prog-num-instructions p1 p2)
+
+concat-prog-run : (p1 p2 : Prog) (init : ℕ) → run (concat-prog p1 p2) init ≡ run p2 (run p1 init)
+concat-prog-run Done p2 init = refl
+concat-prog-run (AddThen x p1) p2 init = 
+  concat-prog-run p1 p2 (x + init) ∙ cong (run p2) (sym (λ c → run (AddThen x p1) init))
+  --   run (concat-prog (AddThen x p1) p2) init
+  -- ≡⟨ refl ⟩
+  --   run (concat-prog p1 p2) (x + init)
+  -- ≡⟨ concat-prog-run p1 p2 (x + init) ⟩
+  --   run p2 (run p1 (x + init))
+  -- ≡⟨ cong (run p2) (sym (λ c → run (AddThen x p1) init)) ⟩
+  --   run p2 (run (AddThen x p1) init)
+  -- ∎
+concat-prog-run (MulThen x p1) p2 init =
+  concat-prog-run p1 p2 (x * init) ∙ cong (run p2) (sym (λ c → run (MulThen x p1) init))
+concat-prog-run (DivThen x p1) p2 init =
+  concat-prog-run p1 p2 (init / x) ∙ cong (run p2) (sym (λ c → run (DivThen x p1) init))
+concat-prog-run (VidThen x p1) p2 init =
+  concat-prog-run p1 p2 (x / init) ∙ cong (run p2) (sym (λ c → run (VidThen x p1) init))
+concat-prog-run (SetToThen x p1) p2 init =
+  concat-prog-run p1 p2 x ∙ cong (run p2) (sym (λ c → run (SetToThen x p1) init))
+
+run-portable : Prog → ℕ → Bool × ℕ
+run-portable Done state = true ,′ state
+run-portable (AddThen x prog) state = run-portable prog (x + state)
+run-portable (MulThen x prog) state = run-portable prog (x * state)
+run-portable (DivThen zero prog) state = false ,′ state
+run-portable (DivThen (suc x) prog) state = run-portable prog (state / x)
+run-portable (VidThen x prog) zero = false ,′ 0
+run-portable (VidThen x prog) (suc state) = run-portable prog (x / state)
+run-portable (SetToThen x prog) state = run-portable prog x
+
+fuck : {A B : Set} {a₁ a₂ : A} {b₁ b₂ : B} → (a₁ ,′ b₁) ≡ (a₂ ,′ b₂) → a₁ ≡ a₂
+fuck {A} {B} {a₁} {a₂} {b₁} {b₂} prf i = proj₁ (prf i)
+
+run-portable-run : (p : Prog) → (s0 s1 : ℕ) → run-portable p s0 ≡ (true ,′ s1) → run p s0 ≡ s1
+run-portable-run Done s0 s1 prf = cong proj₂ refl
+run-portable-run (AddThen x p) s0 s1 prf = run-portable-run p (x + s0) s1 prf
+run-portable-run (MulThen x p) s0 s1 prf = run-portable-run p (x * s0) s1 prf
+run-portable-run (DivThen zero p) s0 s1 prf = ?
+  where
+    prf2 : run-portable (DivThen zero p) s0 ≡ (true ,′ s1)
+    prf2 = prf
+
+    prf3 : (false ,′ s0) ≡ (true ,′ s1)
+    prf3 = prf
+
+    prf4 : false ≡ true
+    prf4 i = proj₁ (prf3 i)
+
+    prf5 : (false ≡ true) → ⊥
+    prf5 x = ?
+run-portable-run (DivThen (suc x) p) s0 s1 prf = {! !}
+run-portable-run (VidThen x p) s0 s1 prf = ?
+run-portable-run (SetToThen x p) s0 s1 prf = run-portable-run p x s1 prf
+
+validate' : Bool → Prog → Bool
+validate' _ Done = true
+validate' could-be-zero (AddThen zero prog) = validate' could-be-zero prog
+validate' _ (AddThen (suc x) prog) = validate' false prog
+validate' _ (MulThen zero prog) = validate' true prog
+validate' could-be-zero (MulThen (suc x) prog) = validate' could-be-zero prog
+validate' could-be-zero (MulThen x prog) = validate' could-be-zero prog
+validate' could-be-zero (DivThen zero prog) = false
+validate' could-be-zero (DivThen (suc x) prog) = validate' could-be-zero prog
+validate' false (VidThen x prog) = validate' false prog
+validate' true (VidThen x prog) = false
+validate' could-be-zero (SetToThen zero prog) = validate' could-be-zero prog
+validate' could-be-zero (SetToThen (suc x) prog) = true
+
+validate : Prog → Bool
+validate prog = validate' true prog
+
+goodProgram1 = AddThen 1 (VidThen 10 Done)
+goodProgram2 = AddThen 0 (MulThen 10 (AddThen 0 (DivThen 1 Done)))
+goodProgram3 = AddThen 1 (MulThen 10 (AddThen 0 (VidThen 1 Done)))
+goodProgram4 = Done
+goodProgram5 = SetToThen 0 (DivThen 1 Done)
+goodProgram6 = SetToThen 1 (VidThen 1 Done)
+goodProgram7 = AddThen 1 (DivThen 1 (DivThen 1 (VidThen 1 Done)))
+
+validate1 : validate goodProgram1 ≡ true
+validate1 = refl
+
+validate2 : validate goodProgram2 ≡ true
+validate2 = refl
+
+validate3 : validate goodProgram3 ≡ true
+validate3 = refl
+
+validate4 : validate goodProgram4 ≡ true
+validate4 = refl
+
+validate5 : validate goodProgram5 ≡ true
+validate5 = refl
+
+validate6 : validate goodProgram6 ≡ true
+validate6 = refl
+
+validate7 : validate goodProgram7 ≡ true
+validate7 = refl
+
+badProgram1 = AddThen 0 (VidThen 10 Done)
+badProgram2 = AddThen 1 (DivThen 0 Done)
+
+validateb1 : validate badProgram1 ≡ false
+validateb1 = refl
+
+validateb2 : validate badProgram2 ≡ false
+validateb2 = refl
+
+validate-sound : (p : Prog) → validate p ≡ true → (s : ℕ) → run-portable p s ≡ (true ,′ run p s)
+validate-sound p prf s = ?
diff --git a/src/Pset2.agda b/src/Pset2.agda
new file mode 100644
index 0000000..12294b2
--- /dev/null
+++ b/src/Pset2.agda
@@ -0,0 +1,30 @@
+{-# OPTIONS --cubical #-}
+
+module Pset2 where
+
+open import Cubical.Foundations.Prelude
+open import Data.Nat
+
+fact : ℕ → ℕ
+fact 0 = 1
+fact (suc n) = (suc n) * (fact n)
+
+exp : ℕ → ℕ → ℕ
+exp b zero = 1
+exp b (suc p) = b * (exp b p)
+
+test-exp-2-3 : exp 2 3 ≡ 8
+test-exp-2-3 = refl
+
+test-exp-3-2 : exp 3 2 ≡ 9
+test-exp-3-2 = refl
+
+test-exp-4-1 : exp 4 1 ≡ 4
+test-exp-4-1 = refl
+
+test-exp-5-0 : exp 5 0 ≡ 1
+test-exp-5-0 = refl
+
+test-exp-1-3 : exp 1 3 ≡ 1
+test-exp-1-3 = refl
+
diff --git a/src/Pset3.agda b/src/Pset3.agda
new file mode 100644
index 0000000..4c6d30f
--- /dev/null
+++ b/src/Pset3.agda
@@ -0,0 +1,38 @@
+{-# OPTIONS --cubical #-}
+
+module Pset3 where
+
+open import Cubical.Foundations.Prelude
+open import Data.Nat
+open import Data.List
+open import Relation.Nullary
+
+data Tree (A : Set) : Set where
+  Leaf : Tree A
+  Node : (l : Tree A) → A → (r : Tree A) → Tree A
+
+flatten : {A : Set} → Tree A → List A
+flatten Leaf = []
+flatten (Node l x r) = flatten l ++ (x ∷ []) ++ flatten r
+
+id : {A : Set} → A → A
+id x = x
+
+compose : {A B C : Set} (g : B → C) → (f : A → B) → A → C
+compose g f x = g (f x)
+
+compose-id-l : {A B : Set} → (f : A → B) → compose id f ≡ f
+compose-id-l f = refl
+
+compose-id-r : {A B : Set} → (f : A → B) → compose f id ≡ f
+compose-id-r f = refl
+
+compose-assoc : {A B C D : Set} (f : A → B) (g : B → C) (h : C → D) →
+  compose h (compose g f) ≡ compose (compose h g) f
+compose-assoc f g h = refl
+
+-- 2d. Binary search trees
+
+bst : Tree ℕ → (ℕ → Set) → Set
+bst Leaf s = ?
+bst (Node l d r) s = {! !}