Ground Terms

A GroundTerm is a constant or a functional term with arbitrary nesting of function symbols (SkolemFS). Aiming to define GroundTerm, we need to define a more basic structure first, where we do not demand yet that function symbol arities are respected. PreGroundTerms need to be able to model Skolem terms, i.e. function terms. We can represent those conveniently using inductively defined FiniteTrees.

With PreGroundTerms in place, we merely define GroundTerms to be the PreGroundTerms where arity_ok holds. We then define appropriate constructors and recursion principles on the GroundTerm to make it behave almost like an inductive type with a GroundTerm.const and GroundTerm.func constructor.

@[reducible, inline]

abbrev PreGroundTerm (sig : Signature) [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] : Type (max (max (max u_3 u_2) u_1) u_3)

The PreGroundTerm is simply a FiniteTree (SkolemFS sig) sig.C. That is a tree that features Skolem function symbols in its inner nodes and constants in its leaf nodes.

Equations

• PreGroundTerm sig = FiniteTree (SkolemFS sig) sig.C

@[irreducible]

def PreGroundTerm.arity_ok {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] : FiniteTree (SkolemFS sig) sig.C → Bool

The arity of a functional term is ok if the defined arity of its function symbol matches its number of children and arity_ok also holds for each child. For constants, i.e. the leaf nodes, the arity is trivially ok.

Equations

• One or more equations did not get rendered due to their size.
• PreGroundTerm.arity_ok (FiniteTree.leaf a) = true

@[reducible, inline]

abbrev GroundTerm (sig : Signature) [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] : Type (max 0 (max u_3 u_2) u_1)

As mentioned above, a GroundTerm is simply a PreGroundTerm subtype where arity_ok holds.

Equations

• GroundTerm sig = { t : PreGroundTerm sig // PreGroundTerm.arity_ok t = true }

def GroundTerm.const {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (c : sig.C) : GroundTerm sig

A GroundTerm can be direclty constructed from a constant.

Equations

• GroundTerm.const c = ⟨FiniteTree.leaf c, ⋯⟩

theorem GroundTerm.const.inj {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] : Function.Injective const

The GroundTerm.const constructor is injective.

@[simp]

theorem GroundTerm.const.injEq {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {c d : sig.C} : const c = const d ↔ c = d

def GroundTerm.func {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (func : SkolemFS sig) (ts : List (GroundTerm sig)) (arity_ok : ts.length = func.arity) : GroundTerm sig

Also, a GroundTerm can be constructed from a SkolemFS and a list of GroundTerms as long as the length of the list matches the function symbol's arity.

Equations

• GroundTerm.func func ts arity_ok = ⟨FiniteTree.inner func ts.unattach, ⋯⟩

theorem GroundTerm.func.inj {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {func1 func2 : SkolemFS sig} {ts1 ts2 : List (GroundTerm sig)} {arity_ok1 : ts1.length = func1.arity} {arity_ok2 : ts2.length = func2.arity} : func func1 ts1 arity_ok1 = func func2 ts2 arity_ok2 → func1 = func2 ∧ ts1 = ts2

The GroundTerm.func constructor is injective.

@[simp]

theorem GroundTerm.func.injEq {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {func1 func2 : SkolemFS sig} {ts1 ts2 : List (GroundTerm sig)} {arity_ok1 : ts1.length = func1.arity} {arity_ok2 : ts2.length = func2.arity} : func func1 ts1 arity_ok1 = func func2 ts2 arity_ok2 ↔ func1 = func2 ∧ ts1 = ts2

theorem GroundTerm.func_neq_const {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {func : SkolemFS sig} {ts : List (GroundTerm sig)} {arity_ok : ts.length = func.arity} {c : sig.C} : GroundTerm.func func ts arity_ok ≠ const c

GroundTerm.func can never be equal to GroundTerm.const.

theorem GroundTerm.eq_while_contained_is_impossible {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {func : SkolemFS sig} {ts : List (GroundTerm sig)} {arity_ok : ts.length = func.arity} : ¬GroundTerm.func func ts arity_ok ∈ ts

A term cannot occur in its own child.

def GroundTerm.cases {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {motive : GroundTerm sig → Sort u} (t : GroundTerm sig) (const : (c : sig.C) → motive (const c)) (func : (func : SkolemFS sig) → (ts : List (GroundTerm sig)) → (arity_ok : ts.length = func.arity) → motive (GroundTerm.func func ts arity_ok)) : motive t

We define a cases eliminator for the GroundTerm having a case for each constructor. This allows to use the cases tactic direcly on GroundTerms.

Equations

• One or more equations did not get rendered due to their size.

@[irreducible]

def GroundTerm.rec {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {motive : GroundTerm sig → Sort u} (const : (c : sig.C) → motive (const c)) (func : (func : SkolemFS sig) → (ts : List (GroundTerm sig)) → (arity_ok : ts.length = func.arity) → ((t : GroundTerm sig) → t ∈ ts → motive t) → motive (GroundTerm.func func ts arity_ok)) (t : GroundTerm sig) : motive t

We define an induction eliminator for the GroundTerm having a case for each constructor. This allows to use the induction tactic direcly on GroundTerms.

Equations

• One or more equations did not get rendered due to their size.

def GroundTerm.toConst {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (t : GroundTerm sig) (isConst : ∃ (c : sig.C), t = const c) : sig.C

A GroundTerm that has been constructed from a constant can be converted into this constants again.

Equations

• t.toConst isConst = match eq : t.val with | FiniteTree.leaf c => c | FiniteTree.inner a a_1 => ⋯.elim

def GroundTerm.functionSymbol {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (t : GroundTerm sig) (isFunc : ∃ (func : SkolemFS sig), ∃ (ts : List (GroundTerm sig)), ∃ (arity_ok : ts.length = func.arity), t = GroundTerm.func func ts arity_ok) : SkolemFS sig

For a GroundTerm that has been constructed as a functional term, we can obtain the function symbol.

Equations

• t.functionSymbol isFunc = match eq : t.val with | FiniteTree.leaf a => ⋯.elim | FiniteTree.inner func a => func

def GroundTerm.depth {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (t : GroundTerm sig) : Nat

The depth of a GroundTerm is the depth of the underlying FiniteTree, i.e. the deepest nesting of function symbols (+1).

Equations

• t.depth = FiniteTree.depth t.val

def GroundTerm.constants {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (t : GroundTerm sig) : List sig.C

The constants occurring in a GroundTerm are exactly the leaves of the underlying FiniteTree.

Equations

• t.constants = FiniteTree.leaves t.val

def GroundTerm.functions {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (t : GroundTerm sig) : List (SkolemFS sig)

The functions (i.e. function symbols SkolemFS) occurring in a GroundTerm are exactly the inner labels of the underlying FiniteTree.

Equations

• t.functions = FiniteTree.innerLabels t.val

def GroundTerm.rules {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (t : GroundTerm sig) : List (Rule sig)

The rules that occur in the Skolem symbols of a GroundTerm.

Equations

• t.rules = List.map SkolemFS.rule t.functions

@[simp]

theorem GroundTerm.toConst_const {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {c : sig.C} : (const c).toConst ⋯ = c

Applying toConst to a GroundTerm.const yields exactly the contained constant.

@[simp]

theorem GroundTerm.functionSymbol_func {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {func : SkolemFS sig} {ts : List (GroundTerm sig)} {arity_ok : ts.length = func.arity} : (GroundTerm.func func ts arity_ok).functionSymbol ⋯ = func

Applying functionSymbol to a GroundTerm.func yields exactly the contained function symbol.

@[simp]

theorem GroundTerm.depth_const {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {c : sig.C} : (const c).depth = 1

Constants have depth 1.

@[simp]

theorem GroundTerm.depth_func {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {f : SkolemFS sig} {ts : List (GroundTerm sig)} {arity_ok : ts.length = f.arity} : (func f ts arity_ok).depth = 1 + (List.map depth ts).max?.getD 1

The depth of a function term is the maximum depth of its children + 1.

theorem GroundTerm.depth_gt_zero {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {t : GroundTerm sig} : 0 < t.depth

Every term has a depth greater zero since constants already have depth 1.

@[simp]

theorem GroundTerm.constants_const {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {c : sig.C} : (const c).constants = [c]

The constants of a constant are the singleton list with the constant itself.

@[simp]

theorem GroundTerm.constants_func {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {f : SkolemFS sig} {ts : List (GroundTerm sig)} {arity_ok : ts.length = f.arity} : (func f ts arity_ok).constants = List.flatMap constants ts

The constants of a function term are the constants of its children.

@[simp]

theorem GroundTerm.functions_const {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {c : sig.C} : (const c).functions = []

A constant has no functions.

@[simp]

theorem GroundTerm.functions_func {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {f : SkolemFS sig} {ts : List (GroundTerm sig)} {arity_ok : ts.length = f.arity} : (func f ts arity_ok).functions = f :: List.flatMap functions ts

The functions of a function term consist of the function symbol of the current term and the function symbols of all its children.

@[simp]

theorem GroundTerm.rules_const {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {c : sig.C} : (const c).rules = []

A constant has no rules.

@[simp]

theorem GroundTerm.rules_func {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {f : SkolemFS sig} {ts : List (GroundTerm sig)} {arity_ok : ts.length = f.arity} : (func f ts arity_ok).rules = f.rule :: List.flatMap rules ts

The rules of a function term consist of the rules of the current term and the rules of all its children.