Terms

We define various kinds of terms that form some of the most basic building blocks of other structures like atoms and rules. In this file we start by introducing a Signature and the VarOrConst as the most basic term type.

structure Signature : Type (max (max (u + 1) (v + 1)) (w + 1))

First of all, almost all of our definitions consider a fixed but arbitrary Signature of predicate symbols P, variables V, and constants C. Also every predicate has a fixed arity. Note that P, V, and C can be arbitrary types so there are no requirements in terms of countability or finiteness. However, intuitively you can consider them to be countably infinite sets. This would allow to pick fresh elements for example. In places where we need this property, we express this through the GetFreshInhabitant type class.

• P : Type u
• V : Type v
• C : Type w
• arity : self.P → Nat

VarOrConst

We introduce VarOrConst as an inductive type representing a term. The term is either a variable or a constant (thus the name). VarOrConst is used to define FunctionFreeAtom later and is thus also the basic building block of (non-Skolemized) Rules.

inductive VarOrConst (sig : Signature) [DecidableEq sig.C] [DecidableEq sig.V] : Type (max u_2 u_3)

As the name suggests, a VarOrConst is either a variable or a constant.

• var {sig : Signature} [DecidableEq sig.C] [DecidableEq sig.V] (v : sig.V) : VarOrConst sig
• const {sig : Signature} [DecidableEq sig.C] [DecidableEq sig.V] (c : sig.C) : VarOrConst sig

def instDecidableEqVarOrConst.decEq {sig✝ : Signature} {inst✝ : DecidableEq sig✝.C} {inst✝¹ : DecidableEq sig✝.V} (x✝ x✝¹ : VarOrConst sig✝) : Decidable (x✝ = x✝¹)

Equations

• instDecidableEqVarOrConst.decEq (VarOrConst.var a) (VarOrConst.var b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• instDecidableEqVarOrConst.decEq (VarOrConst.var v) (VarOrConst.const c) = isFalse ⋯
• instDecidableEqVarOrConst.decEq (VarOrConst.const c) (VarOrConst.var v) = isFalse ⋯
• instDecidableEqVarOrConst.decEq (VarOrConst.const a) (VarOrConst.const b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance instDecidableEqVarOrConst {sig✝ : Signature} {inst✝ : DecidableEq sig✝.C} {inst✝¹ : DecidableEq sig✝.V} : DecidableEq (VarOrConst sig✝)

Equations

• instDecidableEqVarOrConst = instDecidableEqVarOrConst.decEq

def VarOrConst.isVar {sig : Signature} [DecidableEq sig.C] [DecidableEq sig.V] : VarOrConst sig → Bool

A VarOrConst is a variable if it was built using the VarOrConst.var constructor.

Equations

• (VarOrConst.var v).isVar = true
• (VarOrConst.const c).isVar = false

def VarOrConst.filterVars {sig : Signature} [DecidableEq sig.C] [DecidableEq sig.V] : List (VarOrConst sig) → List sig.V

Given a list of VarOrConst, we can filter out all the variables. Note that we do not use List.filter here since we need to change the list type on the way.

Equations

• VarOrConst.filterVars [] = []
• VarOrConst.filterVars (VarOrConst.var v :: vocs) = v :: VarOrConst.filterVars vocs
• VarOrConst.filterVars (VarOrConst.const c :: vocs) = VarOrConst.filterVars vocs

def VarOrConst.filterConsts {sig : Signature} [DecidableEq sig.C] [DecidableEq sig.V] : List (VarOrConst sig) → List sig.C

Analogous to filterVars, we can also filter for constants.

Equations

• VarOrConst.filterConsts [] = []
• VarOrConst.filterConsts (VarOrConst.var v :: vocs) = VarOrConst.filterConsts vocs
• VarOrConst.filterConsts (VarOrConst.const c :: vocs) = c :: VarOrConst.filterConsts vocs

theorem VarOrConst.filterVars_occur_in_original_list {sig : Signature} [DecidableEq sig.C] [DecidableEq sig.V] (l : List (VarOrConst sig)) (v : sig.V) : v ∈ filterVars l → var v ∈ l

Each member of filterVars is in the original list (when applying the VarOrConst.var constructor again.)

theorem VarOrConst.mem_filterVars_of_var {sig : Signature} [DecidableEq sig.C] [DecidableEq sig.V] (l : List (VarOrConst sig)) (v : sig.V) : var v ∈ l → v ∈ filterVars l

If a variable is in a list of VarOrConst, then it occurs in filterVars.

theorem VarOrConst.filterConsts_occur_in_original_list {sig : Signature} [DecidableEq sig.C] [DecidableEq sig.V] (l : List (VarOrConst sig)) (c : sig.C) : c ∈ filterConsts l → const c ∈ l

Each member of filterConsts is in the original list (when applying the VarOrConst.const constructor again.)

theorem VarOrConst.mem_filterConsts_of_const {sig : Signature} [DecidableEq sig.C] [DecidableEq sig.V] (l : List (VarOrConst sig)) (c : sig.C) : const c ∈ l → c ∈ filterConsts l

If a constant is in a list of VarOrConst, then it occurs in filterConsts.