Skip to content

Instantly share code, notes, and snippets.

@Iainmon
Created January 12, 2025 22:20
Show Gist options
  • Save Iainmon/d190a9a07fb82d957a2e779ed059257a to your computer and use it in GitHub Desktop.
Save Iainmon/d190a9a07fb82d957a2e779ed059257a to your computer and use it in GitHub Desktop.
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