initial commit

.gitignore

@@ -0,0 +1,2 @@
+build/
+*.*~

fol.ipkg

@@ -0,0 +1,47 @@
+package fol
+version = 0.1.0
+authors = "William Ball"
+-- maintainers =
+-- license =
+-- brief =
+-- readme =
+-- homepage =
+-- sourceloc =
+-- bugtracker =
+
+-- the Idris2 version required (e.g. langversion >= 0.5.1)
+-- langversion
+
+-- packages to add to search path
+-- depends =
+
+-- modules to install
+-- modules =
+
+-- main file (i.e. file to load at REPL)
+main = Main
+
+-- name of executable
+executable = "fol"
+-- opts =
+sourcedir = "src"
+-- builddir =
+-- outputdir =
+
+-- script to run before building
+-- prebuild =
+
+-- script to run after building
+-- postbuild =
+
+-- script to run after building, before installing
+-- preinstall =
+
+-- script to run after installing
+-- postinstall =
+
+-- script to run before cleaning
+-- preclean =
+
+-- script to run after cleaning
+-- postclean =

pack.toml

@@ -0,0 +1,10 @@
+[custom.all.fol]
+type = "local"
+path = "."
+ipkg = "fol.ipkg"
+test = "test/test.ipkg"
+
+[custom.all.fol-test]
+type = "local"
+path = "test"
+ipkg = "test.ipkg"

src/Context.idr

@@ -0,0 +1,30 @@
+module Context
+
+import Signature
+import Term
+import Formula
+
+import Data.Fin
+
+%default total
+
+public export
+data Context : Signature nFuncs nRels -> Nat -> Type where
+  Nil  : Context sig 0
+  (::) : {d : Nat} -> Formula sig d -> Context sig n -> Context sig (S n)
+  
+public export
+index : Fin n -> Context sig n -> (d ** Formula sig d)
+index FZ (x :: _) = (depth x ** x)
+index (FS k) (_ :: xs) = index k xs
+
+public export
+data Subset : Context sig n -> Context sig m -> Type where
+  Empty   : Subset [] c
+  Missing : Subset c1 c2 -> Subset c1 (a :: c2)
+  There   : Subset c1 c2 -> Subset (a :: c1) (a :: c2)
+  
+export
+SameSubset : {c : Context sig n} -> Subset c c
+SameSubset {c = []} = Empty
+SameSubset {c = (x :: y)} = There SameSubset

src/Formula.idr

@@ -0,0 +1,38 @@
+module Formula
+
+import Data.Vect
+import Data.Fin
+import Signature
+import Term
+
+public export
+data Formula : Signature nFuncs nRels -> Nat -> Type where
+  Equal  : Term sig n -> Term sig n -> Formula sig n
+  Rel    : (i : Fin nRels) -> Vect (relArity sig i) (Term sig n) -> Formula sig n
+  Imp    : Formula sig n -> Formula sig n -> Formula sig n
+  Bot    : Formula sig n
+  Forall : Formula sig (S n) -> Formula sig n
+
+public export
+sub : Fin n -> Term sig n -> Formula sig n -> Formula sig n
+sub k t (Equal x y) = Equal (sub k t x) (sub k t y)
+sub k t (Rel i xs)  = Rel i (map (sub k t) xs)
+sub k t (Imp x y)   = Imp (sub k t x) (sub k t y)
+sub k t Bot         = Bot
+sub k t (Forall x)  = Forall (sub (FS k) (inc t) x)
+
+public export
+depth : {d : Nat} -> Formula sig d -> Nat
+depth {d = d} phi = d
+
+public export
+elimBinder : {n : Nat} -> Term sig n -> Formula sig (S n) -> Formula sig n
+elimBinder t (Equal x y) = Equal (elimBinder t x) (elimBinder t y)
+elimBinder t (Rel i xs)  = Rel i (map (elimBinder t) xs)
+elimBinder t (Imp x y)   = Imp (elimBinder t x) (elimBinder t y)
+elimBinder t Bot     = Bot
+elimBinder t (Forall x)  = Forall (elimBinder (inc t) x)
+
+public export
+Sentence : Signature nFuncs nRels -> Type
+Sentence sig = Formula sig 0

src/Main.idr

@@ -0,0 +1,4 @@
+module Main
+
+main : IO ()
+main = putStrLn "Hello from Idris2!"

src/Proof.idr

@@ -0,0 +1,25 @@
+module Proof
+
+import Data.Vect
+
+import Signature
+import Term
+import Formula
+import Context
+
+%default total
+
+public export
+data Proof : Context sig g -> Formula sig n -> Type where
+  Hyp     : {c : Context sig g} -> (i : Fin g) -> Proof c (snd $ index i c)
+  EqRefl  : (t : Term sig k) -> Proof c (Equal t t)
+  EqSym   : Proof c (Equal s t) -> Proof c (Equal t s)
+  EqTrans : Proof c (Equal s t) -> Proof c (Equal t u) -> Proof c (Equal s u)
+  EqE     : {phi : Formula sig (S n)} -> Proof c (Equal s t) -> Proof c (elimBinder s phi) -> Proof c (elimBinder t phi)
+  BotE    : Proof c Bot -> Proof c phi
+  Contra  : Proof (Imp phi Bot :: c) Bot -> Proof c phi
+  ImpI    : Proof (phi :: c) psi -> Proof c (Imp phi psi)
+  ImpE    : Proof c (Imp phi psi) -> Proof c phi -> Proof c psi
+  ForallI : Proof c phi -> Proof c (Forall phi)
+  ForallE : Proof c (Forall phi) -> Proof c (elimBinder t phi)
+  Weaken  : Proof c1 phi -> Subset c1 c2 -> Proof c2 phi

src/Signature.idr

@@ -0,0 +1,31 @@
+module Signature
+
+import Data.Vect
+
+%default total
+
+public export
+record FuncSym where
+  constructor MkFuncSym
+  name  : String
+  arity : Nat
+
+public export
+record RelSym where
+  constructor MkRelSym
+  name  : String
+  arity : Nat
+
+public export
+record Signature (n, m : Nat) where
+  constructor MkSignature
+  funcs : Vect n FuncSym
+  rels  : Vect m RelSym
+  
+public export
+funcArity : Signature n _ -> Fin n -> Nat
+funcArity (MkSignature funcs rels) i = (index i funcs).arity
+
+public export
+relArity : Signature _ m -> Fin m -> Nat
+relArity (MkSignature funcs rels) i = (index i rels).arity

src/Term.idr

@@ -0,0 +1,69 @@
+module Term
+
+import Data.Vect
+import Data.Fin
+import Decidable.Equality
+
+import Signature
+
+%default total
+
+public export
+data Term : Signature nFuncs nRels -> Nat -> Type where
+  Bound : Fin n -> Term sig n
+  Free  : String -> Term sig n
+  Func  : (i : Fin nFuncs) -> Vect (funcArity sig i) (Term sig n) -> Term sig n
+  
+public export  
+sub : Fin n -> Term sig n -> Term sig n -> Term sig n  
+sub k t (Bound x) = if k == x then t else Bound x
+sub k t (Free str) = Free str
+sub k t (Func i xs) = Func i (subVec xs t k)
+  where
+    subVec : Vect d (Term sig n) -> Term sig n -> Fin n -> Vect d (Term sig n)
+    subVec [] _ _ = []
+    subVec (x :: xs) t k = sub k t x :: subVec xs t k
+
+public export        
+prev : {n : Nat} -> Fin (S n) -> Maybe (Fin n)    
+prev {n = 0} x = Nothing
+prev {n = S k} FZ = Just FZ
+prev {n = S k} (FS x) =
+  case prev x of
+       Nothing => Nothing
+       Just y => Just (FS y)
+
+public export
+elimBinder : {n : Nat} -> Term sig n -> Term sig (S n) -> Term sig n    
+elimBinder t (Bound x) =
+  case prev x of
+    Just x => Bound x
+    Nothing => t
+elimBinder t (Free str) = Free str
+elimBinder t (Func i xs) = Func i (elimVec t xs)
+  where
+    elimVec : Term sig n -> Vect k (Term sig (S n)) -> Vect k (Term sig n)
+    elimVec t [] = []
+    elimVec t (x :: xs) = elimBinder t x :: elimVec t xs
+
+public export
+inc : Term sig n -> Term sig (S n)
+inc (Bound x) = Bound (FS x)
+inc (Free str) = Free str
+inc (Func i xs) = Func i (incVec xs)
+  where
+    incVec : Vect k (Term sig n) -> Vect k (Term sig (S n))
+    incVec [] = []
+    incVec (x :: xs) = inc x :: incVec xs
+    
+Eq (Term sig n) where
+  (Bound x) == (Bound y) = x == y
+  (Free str1) == (Free str2) = str1 == str2
+  (Func i xs) == (Func j ys) with (decEq i j)
+    (Func i xs) == (Func i ys) | Yes Refl = eqVec xs ys
+    where
+      eqVec : Vect k (Term sig n) -> Vect k (Term sig n) -> Bool
+      eqVec [] [] = True
+      eqVec (x :: xs) (y :: ys) = x == y && eqVec xs ys
+    (Func i xs) == (Func j ys) | No _ = False
+  _ == _ = False