Created
January 12, 2025 22:20
-
-
Save Iainmon/d190a9a07fb82d957a2e779ed059257a to your computer and use it in GitHub Desktop.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
module Prim | |
import Data.Vect | |
import Data.Fin | |
-- import Data.Nat | |
-- import Data.List | |
-- %hide Prelude.cong | |
-- data Bool : Type where | |
-- True : Bool | |
-- False : Bool | |
-- (!!) : {a : Type} -> Nat -> List a -> Maybe a | |
-- _ !! [] = Nothing | |
-- (S n) !! (x :: xs) = n !! xs | |
-- Z !! (x :: xs) = Just x | |
infixl 9 !! | |
(!!) : {a : Type} -> List a -> Nat -> Maybe a | |
[] !! _ = Nothing | |
(x :: xs) !! Z = Just x | |
(x :: xs) !! (S n) = xs !! n | |
-- zip : {a : Type} -> {b : Type} -> List a -> List b -> List (a,b) | |
-- zip [] _ = [] | |
-- zip _ [] = [] | |
-- zip (a :: as) (b :: bs) = (a,b) :: zip as bs | |
zipWith : {a : Type} -> {b : Type} -> {c : Type} -> (a -> b -> c) -> List a -> List b -> List c | |
zipWith f [] _ = [] | |
zipWith f _ [] = [] | |
zipWith f (a :: as) (b :: bs) = (f a b) :: zipWith f as bs | |
zip : {a : Type} -> {b : Type} -> List a -> List b -> List (a,b) | |
zip as bs = zipWith (,) as bs | |
data Cap : Type where | |
Single : Cap | |
Group : Cap | |
Collect : Cap -> Type | |
Collect Single = Nat | |
Collect Group = List Nat | |
create : (c : Cap) -> Nat -> Collect c | |
create Single n = n | |
create Group n = [n] | |
v : Collect Single | |
v = create Single 5 | |
vG : Collect Group | |
vG = create Group 5 | |
-- csum : (c : Cap) -> Collect c -> Nat | |
-- csum Single n = n | |
-- csum Group [] = 0 | |
-- csum Group (n :: ns) = n + csum Group ns | |
-- csum : (c : Cap) -> Collect c -> Nat | |
-- csum Single = id | |
-- csum Group = sum | |
csum : {c : Cap} -> Collect c -> Nat | |
csum {c = Single} n = n | |
csum {c = Group} [] = 0 | |
csum {c = Group} (n :: ns) = n + csum {c = Group} ns | |
inc : (c : Cap) -> Collect c -> Collect c | |
inc Single n = n + 1 | |
inc Group [] = [] | |
inc Group (n :: ns) = (n + 1) :: inc Group ns | |
eqNat : Nat -> Nat -> Bool | |
eqNat Z Z = True | |
eqNat (S n) (S m) = eqNat n m | |
eqNat _ _ = False | |
eqList : {a : Type} -> List a -> List a -> Bool | |
eqList [] [] = True | |
eqList (_ :: xs) (_ :: ys) = eqList xs ys | |
eqList _ _ = False | |
-- foldr' : {a : Type} -> {b : Type} -> (a -> b -> b) -> b -> List a -> b | |
-- foldr' f b [] = b | |
-- foldr' f b (a :: as) = a `f` (foldr' f b as) | |
index' : Fin n -> Vect n a -> a | |
index' FZ (a :: _) = a | |
index' (FS fn) (_ :: as) = index' fn as | |
fiveIsFive : 5 = 5 | |
fiveIsFive = Refl | |
cong' : | |
{A, B : Type} -> | |
{x, y : A} -> | |
(f : A -> B) -> x = y -> f x = f y | |
cong' f Refl = Refl | |
congcong : | |
{A : Type} -> | |
{x, y : A} -> | |
(f : A -> A) -> x = y -> f (f x) = f (f y) | |
congcong f Refl = cong' f Refl | |
cong'' : (f : a -> b) -> x = y -> f x = f y | |
cong'' f Refl = Refl | |
plus_n_0 : (n : Nat) -> n = n + 0 | |
plus_n_0 Z = Refl | |
plus_n_0 (S n) = cong' S (plus_n_0 n) | |
plus_0_l : (n : Nat) -> 0 + n = n | |
plus_0_l n = Refl | |
plus_0_r : (n : Nat) -> n + 0 = n | |
plus_0_r n = sym (plus_n_0 n) | |
plus_n_Sm : (n, m : Nat) -> S (n + m) = n + (S m) | |
-- plus_n_Sm Z Z = Refl | |
-- plus_n_Sm Z (S m) = cong' S Refl | |
-- plus_n_Sm (S n) Z = cong' S (plus_n_Sm n 0) | |
plus_n_Sm Z m = Refl | |
plus_n_Sm (S n) m = cong' S (plus_n_Sm n m) | |
pred_Sn : (n : Nat) -> n = pred (S n) | |
pred_Sn n = Refl | |
-- eq_add_S : (n, m : Nat) -> S n = S m -> n = m | |
-- eq_add_S n m sn_eq_sm = eq_add_S n m sn_eq_sm | |
plus_Sn_m : (n, m : Nat) -> (S n) + m = S (n + m) | |
plus_Sn_m n m = Refl | |
plus_comm : (n, m : Nat) -> n + m = m + n | |
plus_comm Z m = sym $ plus_0_r m -- sym (plus_0_r m) | |
plus_comm (S n) m = trans (cong' S (plus_comm n m)) (plus_n_Sm m n) | |
{- | |
plus_comm (S n) m = | |
let p1 = plus_n_Sm m n | |
in let p2 = plus_comm m (S n) | |
in let p3 = trans p1 p2 | |
in let p4 = trans (sym p3) p1 | |
in let p5 = plus_n_Sm n m in ?help | |
-} | |
plus_Snm_nSm : (n, m : Nat) -> (S n) + m = n + (S m) | |
plus_Snm_nSm n m = plus_n_Sm n m | |
plus_assoc : (n, m, k : Nat) -> n + (m + k) = (n + m) + k | |
plus_assoc Z m k = Refl | |
plus_assoc (S n) m k = cong' S (plus_assoc n m k) | |
plus_permute : (n, m, k : Nat) -> n + (m + k) = m + (n + k) | |
plus_permute Z m k = Refl | |
plus_permute (S n) m k = trans (sym $ cong' S (plus_permute m n k)) (plus_Snm_nSm m (n + k)) | |
append : Vect n a -> Vect m a -> Vect (n + m) a | |
append Nil ms = ms | |
append (n :: ns) ms = n :: append ns ms | |
-- append_nil_id : (n : Nat) -> (v : Vect n a) -> v = (append v []) | |
-- append_nil_id n v = ?h1 | |
-- append_nil_id (a :: as) = ?h1 | |
vsnoc : a -> Vect n a -> Vect (S n) a | |
vsnoc a Nil = a :: Nil | |
vsnoc a (x :: xs) = x :: vsnoc a xs | |
rev : Vect n a -> Vect n a | |
rev Nil = Nil | |
rev (a :: as) = vsnoc a (rev as) | |
cons_vsnoc_rev : (x : a) -> (xs : Vect n a) -> rev (x :: xs) = vsnoc x (rev xs) | |
cons_vsnoc_rev x xs = Refl | |
-- vsnoc_rev_id : (x : a) -> (xs : Vect n a) -> vsnoc x (rev xs) = x :: xs | |
-- vsnoc_rev_id | |
cons_vsnoc : (x : a) -> (xs : Vect n a) -> rev (vsnoc x xs) = x :: rev xs | |
cons_vsnoc {n=Z} x' Nil = Refl | |
cons_vsnoc {n=(S n')} x' (x :: xs) = rewrite cons_vsnoc x' xs in cong'' ((::) x') Refl | |
-- cons_vsnoc {n=(S n')} x' (x :: xs) = rewrite cons_vsnoc x' xs in ?h1 -- (Prelude.cong ((::) x') Refl) | |
-- rev_rev_id : {a : Type} -> {n : Nat} -> (v : Vect n a) -> rev (rev v) = v | |
-- rev_rev_id {a} {n = Z} Nil = Refl | |
-- rev_rev_id {a} {n = S n'} (x :: xs) = ?h2 | |
rev_rev_id : (n : Nat) -> (v : Vect n a) -> rev (rev v) = v | |
rev_rev_id Z Nil = Refl | |
rev_rev_id (S n) (v :: vs) = let p = cons_vsnoc_rev v vs in ?h2 | |
-- case rev vs of | |
-- (x :: xs) => ?h1 -- rev_rev_id (S n') vs | |
-- rev_rev_id Nil = Refl | |
-- rev_rev_id {n = S n'} (x :: xs) = let p = cons_vsnoc_rev x xs in ?h2 | |
-- = case xs of | |
-- Nil => Refl | |
-- (x' :: xs') => ?h2 | |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment