frap
This commit is contained in:
commit
fd916dda04
GPG key ID:
BDA47A31A3C8EE6B
5 changed files with 285 additions and 0 deletions
2
.gitignore
vendored
Normal file
2
.gitignore
vendored
Normal file
|
|
@ -0,0 +1,2 @@
|
|||
*.agdai
|
||||
|
||||
2
frap.agda-lib
Normal file
2
frap.agda-lib
Normal file
|
|
@ -0,0 +1,2 @@
|
|||
include: src
|
||||
depend: standard-library cubical
|
||||
213
src/Pset1.agda
Normal file
213
src/Pset1.agda
Normal file
|
|
@ -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 = ?
|
||||
30
src/Pset2.agda
Normal file
30
src/Pset2.agda
Normal file
|
|
@ -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
|
||||
|
||||
38
src/Pset3.agda
Normal file
38
src/Pset3.agda
Normal file
|
|
@ -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 = {! !}
|
||||
Loading…
Reference in a new issue