First-order logic and model theory in Idris

FOL.idr

module FOL
import Syntax.PreorderReasoning

succAndOne : (n : Nat) -> plus n 1 = S n
succAndOne n = ?succAndOne_rhs

record Language : Type where
  LanguageDef : (funSym : Type)-> (predSym : Type) ->
                (funArity : funSym -> Nat) -> (predArity : predSym -> Nat) -> Language

total NFun : Nat -> Type -> Type
NFun Z     a = a
NFun (S n) a = a -> NFun n a

appNFun : { n : Nat } -> NFun n a -> Vect n a -> a
appNFun x [] = x
appNFun f (y :: xs) = appNFun (f y) xs

mapV : {n : Nat} -> {A, B : Type} -> (A -> B) -> Vect n A -> Vect n B
mapV = map

predFin : Fin n -> Fin n
predFin {n = Z} a = FinZElim a
predFin {n = S _} fZ = fZ
predFin {n = S _} (fS n) = weaken n

total finPlusMinusCancel : {n : Nat} -> (m : Fin n) -> finToNat m + (n - finToNat m) = n
finPlusMinusCancel {n = Z} m = FinZElim m
finPlusMinusCancel {n = (S k)} fZ = refl
finPlusMinusCancel {n = (S k)} (fS x) =
  (finToNat (fS x) + (S k - finToNat (fS x)))
   ={ refl }= (S (finToNat x + (k - finToNat x)))
   ={ cong (finPlusMinusCancel x) }= (S k) QED                  

using (L : Language)
  data Term : Language -> (n : Nat) -> Type where
    Var   : Fin n -> Term L n
    App   : (f : funSym L) -> Vect (funArity L f) (Term L n) -> (Term L n)

  mapVar : (Fin n -> Fin m) -> Term L n -> Term L m
  mapVar f (Var n) = Var (f n)
  mapVar f (App g vs) = App g (mapV (mapVar f) vs)

  liftTerm : {m, n : Nat} -> Fin n -> Fin m -> Term L m -> Term L (m + n)
  liftTerm n k (App f xs) = App f (mapV (liftTerm n k) xs)
  liftTerm {L} {n = n} {m = m} off k (Var i) = 
    if finToNat i < finToNat k 
    then Var (weakenN n i)
    else replace { P = \a => Term L (plus m a)} (finPlusMinusCancel off) $
         replace {P = Term L} (sym $ plusAssociative m (finToNat off) (minus n (finToNat off))) $
         replace {P = \a => Term L (plus a (minus n (finToNat off))) } (plusCommutative (finToNat off) m) $
           Var (weakenN (n - finToNat off) $ shift (finToNat off) i)

  substTerm : {n, m : Nat} -> Fin m -> Term L n -> Term L m -> Term L (m + n)
  substTerm {n = S n} {m = m} k s (Var i) = 
    if finToNat k < finToNat i
    then Var (weakenN (S n) $ predFin i)
    else if i == k
    then replace (plusCommutative (S n) m) $ liftTerm k 0 s
    else Var (weakenN (S n) i)
  substTerm k s (App f xs) = App f (map (substTerm k s) xs)

  infixr 3 ~>
  infixl 4 \/
  infixl 5 /\
  data Formula : Language -> (n : Nat) -> Type where
    Atom : (P : predSym L) -> Vect (predArity L P) (Term L n) -> Formula L n
    (~>) : Formula L n -> Formula L n -> Formula L n
    (/\) : Formula L n -> Formula L n -> Formula L n
    (\/) : Formula L n -> Formula L n -> Formula L n
    Not  : Formula L n -> Formula L n
    Ex   : Formula L (S n) -> Formula L n
    Any  : Formula L (S n) -> Formula L n

  lift : {m, n : Nat} -> Fin n -> Fin m -> Formula L m -> Formula L (m + n)
  lift n k (Atom P vs) = Atom P (mapV (liftTerm n k) vs)
  lift n k (a ~> b)  = lift n k a ~> lift n k b
  lift n k (a /\ b)  = lift n k a /\ lift n k b
  lift n k (a \/ b)  = lift n k a \/ lift n k b
  lift n k (Not a)   = Not $ lift n k a
  lift n k (Ex a)    = Ex $ lift n (shift 1 k) a
  lift n k (Any a)   = Any $ lift n (shift 1 k) a

  subst : {n, m : Nat} -> Fin m -> Term L n -> Formula L m -> Formula L (m + n)
  subst n s (Atom P vs) = Atom P (mapV (substTerm n s) vs)
  subst n s (a ~> b)  = subst n s a ~> subst n s b
  subst n s (a /\ b)  = subst n s a /\ subst n s b
  subst n s (a \/ b)  = subst n s a \/ subst n s b
  subst n s (Not a)   = Not $ subst n s a
  subst n s (Ex a)    = Ex $ subst (shift 1 n) s a
  subst n s (Any a)   = Any $ subst (shift 1 n) s a

  addVarN : (n : Nat) -> Formula L m -> Formula L (m + n)
  addVarN n (Atom P vs) = Atom P (mapV (mapVar (weakenN n)) vs)
  addVarN n (a ~> b)    = addVarN n a ~> addVarN n b
  addVarN n (a /\ b)    = addVarN n a \/ addVarN n b
  addVarN n (a \/ b)    = addVarN n a /\ addVarN n b
  addVarN n (Not a)     = Not $ addVarN n a
  addVarN n (Ex a)      = Ex $ addVarN n a
  addVarN n (Any a)     = Any $ addVarN n a

  addVar : Formula L m -> Formula L (S m)
  addVar {m = m} f = replace (succAndOne m) $ addVarN 1 f

  Sentence : Language -> Type
  Sentence L = Formula L 0

  ClosedTerm : Language -> Type
  ClosedTerm L = Term L 0

  data Structure : Language -> Type where
    MkStructure : (carrier : Type) -> (inhabitant : carrier) ->
                  (interpFun : (f : funSym L) -> NFun (funArity L f) carrier) ->
                  (interpPred : (P : predSym L) -> Vect (predArity L P) carrier -> Type) -> Structure L

  total carrier : Structure L -> Type
  carrier (MkStructure c _ _ _) = c

  total interpFun : (M : Structure L) -> (f : funSym L) -> NFun (funArity L f) (carrier M)
  interpFun (MkStructure _ _ f _) = f

  total interpPred : (M : Structure L) -> (P : predSym L) -> Vect (predArity L P) (carrier M) -> Type
  interpPred (MkStructure _ _ _ f) = f

  interpTermWith : (M : Structure L) -> Vect n (carrier M) -> Term L n -> carrier M
  interpTermWith M vs (Var n) = index n vs
  interpTermWith M vs (App f args) = appNFun (interpFun M f) (map (interpTermWith M vs) args)

  interpClosedTerm : (M : Structure L) -> ClosedTerm L -> carrier M
  interpClosedTerm M = interpTermWith M []

  syntax "[[" [tm] "]]" [M] = interpTerm M tm

  parameters (M : Structure L)
    data ExtendedFunSyms : Type where
      OldSym : funSym L -> ExtendedFunSyms
      ValSym : carrier M -> ExtendedFunSyms
    extendedFunArity : ExtendedFunSyms -> Nat
    extendedFunArity (OldSym ar) = funArity _ ar
    extendedFunArity (ValSym _)  = 0

  ExtLanguage : {L : Language} -> Structure L -> Language
  ExtLanguage {L} M = LanguageDef (ExtendedFunSyms M) (predSym L) (extendedFunArity M) (predArity L)

using (L : Language, M : Structure L, phi : Formula L n, psi : Formula L n, assign : Vect n (carrier M))
  data SatisfiesUnder : (M : Structure L) -> Formula L n -> Vect n (carrier M) -> Type where
      SatAtom : {P : predSym L} -> {args : Vect (predArity L P) (Term L n)} ->
                interpPred M P (map (interpTermWith M assign) args) -> 
                SatisfiesUnder M (Atom P args) assign
      SatAnd : SatisfiesUnder M phi assign -> 
               SatisfiesUnder M psi assign ->
               SatisfiesUnder M (phi /\ psi) assign
      SatOr : SatisfiesUnder M phi assign -> 
              SatisfiesUnder M psi assign ->
              SatisfiesUnder M (phi \/ psi) assign
      SatImply : (SatisfiesUnder M phi assign -> SatisfiesUnder M psi assign) ->
                 SatisfiesUnder M (phi ~> psi) assign
      SatNot : (SatisfiesUnder M phi assign -> _|_) -> SatisfiesUnder M (Not phi) assign
      SatAny : {phi' : Formula L (S n)} ->
               ((z : carrier M) -> SatisfiesUnder M phi'
                   (replace {P = flip Vect (carrier M)} (succAndOne n) $ assign ++ [z])) ->
               SatisfiesUnder M (Any phi') assign
      SatEx : {phi' : Formula L (S n)} ->
               (Exists _ (\ z => SatisfiesUnder M phi'
                   (replace {P = flip Vect (carrier M)} (succAndOne n) $ assign ++ [z]))) ->
               SatisfiesUnder M (Ex phi') assign

  syntax [M] "|=" [f] "[" [s] "]" = SatisfiesUnder M f s

  Satisfies : (M : Structure L) -> Sentence L -> Type
  Satisfies M f = SatisfiesUnder M f []

  infix 2 |=
  (|=) : (M : Structure L) -> Sentence L -> Type
  (|=) = Satisfies

mapL : {a, b : Type} -> (a -> b) -> List a -> List b
mapL = map

using (L : Language)
  infix 2 |-
  data (|-) : List (Formula L n) -> List (Formula L n) -> Type where
    Tauto : {phi : Formula L n} -> [phi] |- [phi]
    Cut   : {phi : Formula L n} -> {G, D, S, P : List (Formula L n)} ->
            (G |- phi :: D) -> (phi :: S |- P) -> G ++ S |- D++ P
    AndL1 : {phi, psi : Formula L n} -> {G, D : List (Formula L n)} ->
            (phi :: G |- D) -> (phi /\ psi) :: G |- D
    AndL2 : {phi, psi : Formula L n} -> {G, D : List (Formula L n)} ->
            (psi :: G |- D) -> (phi /\ psi) :: G |- D
    AndR  : {phi, psi : Formula L n} -> {G, D, S, P : List (Formula L n)} ->
            (G |- phi :: D) -> (S |- psi :: P) -> (G ++ S |- (phi /\ psi) :: D ++ P)
    OrL   : {phi, psi : Formula L n} -> {G, D, S, P : List (Formula L n)} ->
            (phi :: G |- D) -> (psi :: S |- P) -> ((phi \/ psi) :: G ++ S |- D ++ P)
    OrR1  : {phi, psi : Formula L n} -> {G, D : List (Formula L n)} ->
            (G |- phi :: D) -> G |- (phi \/ psi) :: D
    OrR2  : {phi, psi : Formula L n} -> {G, D : List (Formula L n)} ->
            (G |- psi :: D) -> G |- (phi \/ psi) :: D
    NotL  : {phi : Formula L n} -> {G, D : List (Formula L n)} ->
            (G |- phi :: D) -> Not phi :: G |- D
    NotR  : {phi : Formula L n} -> {G, D : List (Formula L n)} ->
            (phi :: G |- D) -> G |- Not phi :: D
    AnyL  : {n, m : Nat} -> {phi : Formula L (S n)} -> {G, D :  List (Formula L n)} -> {t : Term L m}
            -> subst last t phi :: map (addVarN m . addVar) G |- map (addVarN m . addVar) D
            -> Any phi :: G |- D            
    AnyR  : {phi : Formula L (S n)} -> {G, D : List (Formula L n)} ->
            (map addVar G) |- (phi :: map addVar D) -> G |- Any phi :: D
    ExL   : {phi : Formula L (S n)} -> {G, D : List (Formula L n)} ->
            (phi :: map addVar G |- map addVar D) -> Ex phi :: G |- D
    ExR   : {n, m : Nat} -> {phi : Formula L (S n)} -> {G, D :  List (Formula L n)} -> {t : Term L m}
            -> map (addVarN m . addVar) G |- subst last t phi :: map (addVarN m . addVar) D
            -> G |- Any phi :: D
    ImplL : {phi, psi : Formula L n} -> {G, D, S, P : List (Formula L n)} ->
            (G |- phi :: D) -> (psi :: S |- P) -> (phi ~> psi) :: G ++ S |- D ++ P
    ImplR : {phi, psi : Formula L n} -> {G, D : List (Formula L n)} ->
            (phi :: G |- psi :: D) -> G |- (phi ~> psi) :: D
    WeakenL : {phi : Formula L n} -> {G, D : List (Formula L n)} ->
              G |- D -> phi :: G |- D
    WeakenR : {phi : Formula L n} -> {G, D : List (Formula L n)} ->
              G |- D -> G |- phi :: D
    PermL : {phi, psi : Formula L n} -> {G, S, D : List (Formula L n)} ->
            (G ++ (phi :: psi :: S))|- D -> (G ++ (psi :: phi :: S)) |- D
    PermR : {phi, psi : Formula L n} -> {G, P, D : List (Formula L n)} ->
            G |- (P ++ (phi :: psi :: D)) -> G |- (P ++ (psi :: phi :: D))
    ContrL : {phi : Formula L n} -> {G, D : List (Formula L n)} ->
              phi :: phi :: G |- D -> phi :: G |- D
    ContrR : {phi : Formula L n} -> {G, D : List (Formula L n)} ->
              G |- phi :: phi :: D -> G |- phi :: D

  Tauto' : (phi : Formula L n) -> [phi] |- [phi]
  Tauto' _ = Tauto
  AndL1' : {phi : Formula L n} -> {G, D : List (Formula L n)} ->
           (psi : Formula L n) -> (phi :: G |- D) -> (phi /\ psi) :: G |- D
  AndL1' _ = AndL1
  AndL2' : {psi : Formula L n} -> {G, D : List (Formula L n)} ->
           (phi : Formula L n) -> (psi :: G |- D) -> (phi /\ psi) :: G |- D
  AndL2' _ = AndL2
  OrR1'  : {phi : Formula L n} -> {G, D : List (Formula L n)} ->
           (psi : Formula L n) -> (G |- phi :: D) -> G |- (phi \/ psi) :: D
  OrR1' _ = OrR1
  OrR2'  : {psi : Formula L n} -> {G, D : List (Formula L n)} ->
           (phi : Formula L n) -> (G |- psi :: D) -> G |- (phi \/ psi) :: D
  OrR2' _ = OrR2
  WeakenL' : {G, D : List (Formula L n)} ->
             (phi : Formula L n) -> G |- D -> phi :: G |- D
  WeakenL' _ = WeakenL
  WeakenR' : {G, D : List (Formula L n)} ->
             (phi : Formula L n) -> G |- D -> G |- phi :: D
  WeakenR' _ = WeakenR
  PermL' : {phi, psi : Formula L n} -> {S, D : List (Formula L n)} ->
           (G : List (Formula L n)) ->
           (G ++ (phi :: psi :: S)) |- D -> (G ++ (psi :: phi :: S)) |- D
  PermL' _ = PermL
  PermR' : {phi, psi : Formula L n} -> {G, D : List (Formula L n)} ->
           (P : List (Formula L n)) ->
           G |- (P ++ (phi :: psi :: D)) -> G |- (P ++ (psi :: phi :: D))
  PermR' _ = PermR

  Provable : Formula L n -> Type
  Provable f = [] |- [f]

data SetSym = Eps

SetLang : Language
SetLang = LanguageDef _|_ SetSym FalseElim SymArity
  where
    SymArity Eps = 2

data Leq : Nat -> Nat -> Type where
  LeqZero : Leq 0 n
  LeqSucc : Leq n m -> Leq (S n) (S m)

NatOrd : Structure SetLang
NatOrd = MkStructure Nat 0 NatFun NatPred
  where
    total NatFun : (f : _|_) -> NFun (funArity SetLang f) Nat
    NatFun void = FalseElim void
    total NatPred : (P : predSym SetLang) -> Vect (predArity SetLang P) Nat -> Type
    NatPred Eps [x, y] = Leq x y

data Inhabits : (b : a) -> (a : Type) -> Type where
  Inhabitant : {a : Type} -> (b : a) -> Inhabits b a

infix 7 <-
(<-) : Term SetLang n -> Term SetLang n -> Formula SetLang n
(<-) x y = Atom Eps [x, y]

X : Term SetLang 3
X = Var 0

Y : Term SetLang 3
Y = Var 1

W : Term SetLang 3
W = Var 2

Universe : Structure SetLang
Universe = MkStructure Type _|_ TypFun TypPred
  where
    total TypFun : (f : _|_) -> NFun (funArity SetLang f) Type
    TypFun void = FalseElim void
    total TypPred : (P : predSym SetLang) -> Vect (predArity SetLang P) Type -> Type
    TypPred Eps [x, y] = Inhabits x y

---------- Proofs ----------

FOL.succAndOne_rhs = proof
  intros
  rewrite plusSuccRightSucc n 0
  rewrite plusZeroRightNeutral n
  trivial