Get StrictConstantMapping Arguments that produce a certain Image

We define methods for a StrictConstantMapping to obtain the function arguments that produce a given constant, PreGroundTerm, Fact, etc. The possible arguments take into account a list of candidate constants.

def StrictConstantMapping.arguments_for_constant {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (g : StrictConstantMapping sig) (possible_constants : List sig.C) (c : sig.C) : List sig.C

The arguments for a given constant are simply the constants from the candidate list that map to the target.

Equations

• g.arguments_for_constant possible_constants c = List.filter (fun (d : sig.C) => decide (g d = c)) possible_constants

theorem StrictConstantMapping.apply_to_arguments_yields_original_constant {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (g : StrictConstantMapping sig) (possible_constants : List sig.C) (c arg : sig.C) : arg ∈ g.arguments_for_constant possible_constants c ↔ arg ∈ possible_constants ∧ g arg = c

def StrictConstantMapping.arguments_for_pre_term {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (g : StrictConstantMapping sig) (possible_constants : List sig.C) : PreGroundTerm sig → List (PreGroundTerm sig)

We lift arguments_for_constant to PreGroundTerm considering all possible combinations of arguments.

Equations

• One or more equations did not get rendered due to their size.
• g.arguments_for_pre_term possible_constants (FiniteTree.leaf c) = List.map (fun (arg : sig.C) => FiniteTree.leaf arg) (g.arguments_for_constant possible_constants c)

def StrictConstantMapping.arguments_for_pre_term.arguments_for_pre_term_list {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (g : StrictConstantMapping sig) (possible_constants : List sig.C) : List (PreGroundTerm sig) → List (List (PreGroundTerm sig))

Equations

• One or more equations did not get rendered due to their size.
• StrictConstantMapping.arguments_for_pre_term.arguments_for_pre_term_list g possible_constants [] = [[]]

theorem StrictConstantMapping.arguments_for_pre_term.length_arguments_for_pre_term_list {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {g : StrictConstantMapping sig} {possible_constants : List sig.C} {ts : List (PreGroundTerm sig)} (args : List (PreGroundTerm sig)) : args ∈ arguments_for_pre_term_list g possible_constants ts → args.length = ts.length

theorem StrictConstantMapping.arguments_for_pre_term.mem_arguments_for_pre_term_list {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {g : StrictConstantMapping sig} {possible_constants : List sig.C} {ts args : List (PreGroundTerm sig)} (length_eq : args.length = ts.length) : args ∈ arguments_for_pre_term_list g possible_constants ts ↔ ∀ (i : Nat) (lt : i < ts.length), args[i] ∈ g.arguments_for_pre_term possible_constants ts[i]

theorem StrictConstantMapping.apply_to_arguments_yields_original_pre_term {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {g : StrictConstantMapping sig} {possible_constants : List sig.C} {term : FiniteTree (SkolemFS sig) sig.C} {arg : PreGroundTerm sig} : arg ∈ g.arguments_for_pre_term possible_constants term ↔ (∀ (c : sig.C), c ∈ FiniteTree.leaves arg → c ∈ possible_constants) ∧ g.toConstantMapping.apply_pre_ground_term arg = term

theorem StrictConstantMapping.arguments_for_pre_term_arity_ok {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {g : StrictConstantMapping sig} {possible_constants : List sig.C} {t : FiniteTree (SkolemFS sig) sig.C} (arity_ok : PreGroundTerm.arity_ok t = true) {t' : PreGroundTerm sig} : t' ∈ g.arguments_for_pre_term possible_constants t → PreGroundTerm.arity_ok t' = true

def StrictConstantMapping.arguments_for_term_list {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (g : StrictConstantMapping sig) (possible_constants : List sig.C) (ts : List (GroundTerm sig)) : List (List (GroundTerm sig))

We list arguments_for_pre_term to lists of GroundTerms.

Equations

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

theorem StrictConstantMapping.apply_to_arguments_yields_original_term_list {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {g : StrictConstantMapping sig} {possible_constants : List sig.C} {ts args : List (GroundTerm sig)} : args ∈ g.arguments_for_term_list possible_constants ts ↔ (∀ (c : sig.C), c ∈ List.flatMap GroundTerm.constants args → c ∈ possible_constants) ∧ List.map (fun (arg : GroundTerm sig) => g.toConstantMapping.apply_ground_term arg) args = ts

def StrictConstantMapping.arguments_for_fact {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (g : StrictConstantMapping sig) (possible_constants : List sig.C) (f : Fact sig) : List (Fact sig)

We lift arguments_for_term_list to Fact.

Equations

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

theorem StrictConstantMapping.apply_to_arguments_yields_original_fact {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (g : StrictConstantMapping sig) (possible_constants : List sig.C) (f arg : Fact sig) : arg ∈ g.arguments_for_fact possible_constants f ↔ (∀ (c : sig.C), c ∈ arg.constants → c ∈ possible_constants) ∧ g.toConstantMapping.apply_fact arg = f