Associate arity with predicates

ProofLibrary.lean

@@ -4,7 +4,8 @@ import ProofLibrary.AlternativeMatches.HomomorphismExtension
 import ProofLibrary.ChaseSequence.Basic
 import ProofLibrary.ChaseSequence.Universality
 import ProofLibrary.ChaseSequence.Deterministic
-import ProofLibrary.ChaseSequence.Termination
+import ProofLibrary.ChaseSequence.Termination.Basic
+import ProofLibrary.ChaseSequence.Termination.MfaLike
 import ProofLibrary.Fin
 import ProofLibrary.FiniteTree
 import ProofLibrary.KnowledgeBaseBasics

ProofLibrary/AlternativeMatches/Chase.lean

@@ -967,7 +967,7 @@ namespace ChaseBranch
             intro t t_mem
             apply each_repeats
             exists f
-          rw [this]
+          simp only [this]
         rw [← this]
         have : (h.repeat_hom j).isHomomorphism fs sub_fs := by
           have : h.repeat_hom j = h.repeat_hom (j-1) ∘ h := by

ProofLibrary/AlternativeMatches/HomomorphismExtension.lean

@@ -42,9 +42,11 @@ namespace ChaseBranch
         have : i = disj_index' := by
           have isLt := i.isLt
           have := det trg'.rule trg.property
+          unfold Rule.isDeterministic at this
           simp [this] at isLt
           have isLt' := disj_index'.isLt
           have := det trg.val.rule trg.property
+          unfold Rule.isDeterministic at this
           simp [this] at isLt'
           rw [Fin.ext_iff]
           rw [isLt, isLt']

ProofLibrary/ChaseSequence/Termination/MfaLike.lean

@@ -0,0 +1,30 @@
+import ProofLibrary.ChaseSequence.Termination.Basic
+
+variable {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V]
+
+def criticalInstance (rs : RuleSet sig) (finite : rs.rules.finite) (special_const : sig.C) : Database sig :=
+  ⟨fun f => f.predicate ∈ rs.predicates ∧ ∀ t, t ∈ f.terms -> t = special_const, by
+    have preds_finite := rs.predicates_finite_of_finite finite
+    rcases preds_finite with ⟨l, nodup, eq⟩
+    exists l.map (fun p => {
+      predicate := p
+      terms := List.repeat special_const (sig.arity p)
+      arity_ok := by rw [List.length_repeat]
+    })
+    constructor
+    . sorry
+    . intro f
+      simp
+      constructor
+      . intro h
+        rcases h with ⟨p, p_mem, f_eq⟩
+        rw [← f_eq]
+        simp [Set.element]
+        rw [eq] at p_mem
+        constructor
+        . exact p_mem
+        . intro t
+          sorry
+      sorry
+  ⟩
+

ProofLibrary/ChaseSequence/Universality.lean

@@ -6,7 +6,7 @@ variable {obs : ObsoletenessCondition sig} {kb : KnowledgeBase sig}
 abbrev InductiveHomomorphismResult (ct : ChaseTree obs kb) (m : FactSet sig) (depth : Nat) := {pair : (List Nat) × (GroundTermMapping sig) // pair.1.length = depth ∧ (ct.tree.get pair.1).is_none_or (fun fs => pair.2.isHomomorphism fs.fact m) }
 
 -- TODO: split up the following definition (rather the proofs inside) to get rid of heartbeat increase
-set_option maxHeartbeats 300000
+set_option maxHeartbeats 400000
 
 noncomputable def inductive_homomorphism_with_prev_node_and_trg (ct : ChaseTree obs kb) (m : FactSet sig) (m_is_model : m.modelsKb kb) (prev_depth : Nat) (prev_result : InductiveHomomorphismResult ct m prev_depth) (prev_node_unwrapped : ChaseNode obs kb.rules) (prev_node_eq : ct.tree.get prev_result.val.fst = some prev_node_unwrapped) (trg_ex : exists_trigger_list obs kb.rules prev_node_unwrapped (ct.tree.children prev_result.val.fst)) : InductiveHomomorphismResult ct m (prev_depth + 1) :=
   let prev_path := prev_result.val.fst

ProofLibrary/KnowledgeBaseBasics.lean

@@ -8,22 +8,26 @@ section StructuralDefs
   structure FunctionFreeFact (sig : Signature) [DecidableEq sig.P] [DecidableEq sig.C] where
     predicate : sig.P
     terms : List sig.C
+    arity_ok : terms.length = sig.arity predicate
     deriving DecidableEq
 
   @[ext]
   structure Fact (sig : Signature) [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] where
     predicate : sig.P
     terms : List (GroundTerm sig)
+    arity_ok : terms.length = sig.arity predicate
     deriving DecidableEq
 
   structure FunctionFreeAtom (sig : Signature) [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] where
     predicate : sig.P
     terms : List (VarOrConst sig)
+    arity_ok : terms.length = sig.arity predicate
     deriving DecidableEq
 
   structure Atom (sig : Signature) [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] where
     predicate : sig.P
     terms : List (SkolemTerm sig)
+    arity_ok : terms.length = sig.arity predicate
     deriving DecidableEq
 
   variable (sig : Signature) [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V]
@@ -57,22 +61,32 @@ namespace FunctionFreeAtom
 
   def variables (a : FunctionFreeAtom sig) : List sig.V := VarOrConst.filterVars a.terms
 
-  def skolemize (ruleId : Nat) (disjunctIndex : Nat) (frontier : List sig.V) (a : FunctionFreeAtom sig) : Atom sig := { predicate := a.predicate, terms := a.terms.map (VarOrConst.skolemize ruleId disjunctIndex frontier) }
+  def skolemize (ruleId : Nat) (disjunctIndex : Nat) (frontier : List sig.V) (a : FunctionFreeAtom sig) : Atom sig := { predicate := a.predicate, terms := a.terms.map (VarOrConst.skolemize ruleId disjunctIndex frontier), arity_ok := by rw [List.length_map, a.arity_ok] }
 
   theorem skolemize_same_length (ruleId : Nat) (disjunctIndex : Nat) (frontier : List sig.V) (a : FunctionFreeAtom sig) : a.terms.length = (a.skolemize ruleId disjunctIndex frontier).terms.length := by
     unfold skolemize
     rw [List.length_map]
 
   theorem skolem_term_in_skolem_atom_if_term_in_atom (ruleId : Nat) (disjunctIndex : Nat) (frontier : List sig.V) (a : FunctionFreeAtom sig) (t : VarOrConst sig) : t ∈ a.terms.toSet -> (↑(t.skolemize ruleId disjunctIndex frontier)) ∈ (a.skolemize ruleId disjunctIndex frontier).terms.toSet := by
     unfold skolemize
-    induction a.terms with
-    | nil => intros; contradiction
-    | cons head tail ih =>
-      simp [Set.element, List.toSet]
-      intro h
-      cases h with
-      | inl hl => apply Or.inl; simp [Set.element] at hl; rw [hl]; simp [Set.element]
-      | inr hr => apply Or.inr; apply ih; apply hr
+
+    have : ∀ (ts : List (VarOrConst sig)), t ∈ ts -> (t.skolemize ruleId disjunctIndex frontier) ∈ ts.map (VarOrConst.skolemize ruleId disjunctIndex frontier) := by
+      intro ts
+      induction ts with
+      | nil => intros; contradiction
+      | cons head tail ih =>
+        intro h
+        rw [List.mem_cons] at h
+        rw [List.map_cons, List.mem_cons]
+        cases h with
+        | inl hl => apply Or.inl; simp [Set.element] at hl; rw [hl]
+        | inr hr => apply Or.inr; apply ih; apply hr
+
+    intro mem
+    rw [← List.inIffInToSet] at mem
+    rw [← List.inIffInToSet]
+    apply this a.terms
+    exact mem
 
 end FunctionFreeAtom
 
@@ -101,6 +115,8 @@ namespace FunctionFreeConjunction
             unfold FunctionFreeAtom.variables at this
             apply this
 
+  def predicates (conj : FunctionFreeConjunction sig) : List sig.P := conj.map FunctionFreeAtom.predicate
+
 end FunctionFreeConjunction
 
 namespace Rule
@@ -119,18 +135,43 @@ namespace Rule
       have exFactInBody := FunctionFreeConjunction.v_in_vars_occurs_in_fact _ v vInBody
       exact exFactInBody
 
-  def Rule.isDatalog (r : Rule sig) : Bool :=
+  def isDatalog (r : Rule sig) : Bool :=
     r.head.all (fun h => h.vars.all (fun v => v ∈ r.body.vars))
 
+  def isDeterministic (r : Rule sig) : Prop := r.head.length = 1
+
+  def predicates (r : Rule sig) : List sig.P := r.body.predicates ++ (r.head.flatMap FunctionFreeConjunction.predicates)
+
 end Rule
 
-def RuleSet.isDeterministic (rs : RuleSet sig) : Prop := ∀ (r : Rule sig), r ∈ rs.rules -> r.head.length = 1
+namespace RuleSet
+
+  def isDeterministic (rs : RuleSet sig) : Prop := ∀ (r : Rule sig), r ∈ rs.rules -> r.isDeterministic
+
+  def predicates (rs : RuleSet sig) : Set sig.P := fun p => ∃ r, r ∈ rs.rules ∧ p ∈ r.predicates
+
+  theorem predicates_finite_of_finite (rs : RuleSet sig) : rs.rules.finite -> rs.predicates.finite := by
+    intro finite
+    rcases finite with ⟨l, nodup, eq⟩
+    exists (l.flatMap Rule.predicates).eraseDupsKeepRight
+    constructor
+    . apply List.nodup_eraseDupsKeepRight
+    . intro p
+      rw [List.mem_eraseDupsKeepRight_iff]
+      unfold predicates
+      simp only [List.mem_flatMap]
+      constructor <;> (intro h; rcases h with ⟨r, h⟩; exists r)
+      . rw [← eq]; assumption
+      . rw [eq]; assumption
+
+end RuleSet
 
 def KnowledgeBase.isDeterministic (kb : KnowledgeBase sig) : Prop := kb.rules.isDeterministic
 
 def FunctionFreeFact.toFact (f : FunctionFreeFact sig) : Fact sig := {
   predicate := f.predicate,
-  terms := f.terms.map GroundTerm.const
+  terms := f.terms.map GroundTerm.const,
+  arity_ok := by rw [List.length_map, f.arity_ok]
 }
 
 def Fact.toFunctionFreeFact (f : Fact sig) : Option (FunctionFreeFact sig) :=
@@ -143,16 +184,19 @@ def Fact.toFunctionFreeFact (f : Fact sig) : Option (FunctionFreeFact sig) :=
       )
     )
   then
-    (Option.some ({ predicate := f.predicate, terms := (f.terms.attach.map (fun ⟨t, t_elem⟩ => match eq : t with
-      | .leaf c => c
-      | .inner _ _ => by
-        -- This cannot happen since we check before that everything is a constant
-        simp at h
-        specialize h t
-        rw [eq] at h
-        specialize h t_elem
-        simp at h
-    )) }))
+    (Option.some ({
+      predicate := f.predicate,
+      terms := (f.terms.attach.map (fun ⟨t, t_elem⟩ => match eq : t with
+        | .leaf c => c
+        | .inner _ _ => by
+          -- This cannot happen since we check before that everything is a constant
+          simp at h
+          specialize h t
+          rw [eq] at h
+          specialize h t_elem
+          simp at h
+      )),
+      arity_ok := by rw [List.length_map, List.length_attach, f.arity_ok] }))
   else
     (Option.none)
 

ProofLibrary/SubstitutionAndHomomorphismBasics.lean

@@ -29,10 +29,10 @@ namespace GroundSubstitution
     | .func fs frontier => FiniteTree.inner fs (FiniteTreeList.fromList (frontier.map (fun fv => σ fv)))
 
   def apply_atom (σ : GroundSubstitution sig) (ϕ : Atom sig) : Fact sig :=
-    { predicate := ϕ.predicate, terms := List.map (apply_skolem_term σ) ϕ.terms }
+    { predicate := ϕ.predicate, terms := List.map (apply_skolem_term σ) ϕ.terms, arity_ok := by rw [List.length_map, ϕ.arity_ok] }
 
   def apply_function_free_atom (σ : GroundSubstitution sig) (ϕ : FunctionFreeAtom sig) : Fact sig :=
-    { predicate := ϕ.predicate, terms := List.map (apply_var_or_const σ) ϕ.terms }
+    { predicate := ϕ.predicate, terms := List.map (apply_var_or_const σ) ϕ.terms, arity_ok := by rw [List.length_map, ϕ.arity_ok] }
 
   def apply_function_free_conj (σ : GroundSubstitution sig) (conj : FunctionFreeConjunction sig) : List (Fact sig) :=
     (List.map (apply_function_free_atom σ)) conj
@@ -98,7 +98,7 @@ namespace GroundTermMapping
       | _ => True
 
   def applyFact (h : GroundTermMapping sig) (f : Fact sig) : Fact sig :=
-    { predicate := f.predicate, terms := List.map h f.terms }
+    { predicate := f.predicate, terms := List.map h f.terms, arity_ok := by rw [List.length_map, f.arity_ok] }
 
   theorem applyFact_compose (g h : GroundTermMapping sig) : applyFact (h ∘ g) = (applyFact h) ∘ (applyFact g) := by
     apply funext

ProofLibrary/TermBasics.lean

@@ -5,6 +5,7 @@ structure Signature where
   P : Type u
   V : Type v
   C : Type w
+  arity : P -> Nat
 
 structure SkolemFS (sig : Signature) [DecidableEq sig.V] where
   ruleId : Nat

ProofLibrary/Trigger.lean

@@ -21,6 +21,7 @@ namespace PreTrigger
     {
       predicate := atom.predicate
       terms := atom.terms.map (trg.apply_to_var_or_const disjunctIndex)
+      arity_ok := by rw [List.length_map, atom.arity_ok]
     }
 
   theorem apply_to_function_free_atom_terms_same_length (trg : PreTrigger sig) (disjunctIndex : Nat) (atom : FunctionFreeAtom sig) : atom.terms.length = (trg.apply_to_function_free_atom disjunctIndex atom).terms.length := by
@@ -197,7 +198,7 @@ def SkolemObsoleteness (sig : Signature) [DecidableEq sig.P] [DecidableEq sig.C]
     constructor
     . intro v v_in_frontier
       simp [PreTrigger.apply_to_var_or_const, PreTrigger.apply_to_skolemized_term, GroundSubstitution.apply_skolem_term, PreTrigger.skolemize_var_or_const, VarOrConst.skolemize, v_in_frontier]
-    . have : trg.mapped_head[i.val] = (trg.rule.head[i]'(by rw [PreTrigger.head_length_eq_mapped_head_length]; exact i.isLt)).map (fun a => { predicate := a.predicate, terms := a.terms.map (trg.apply_to_var_or_const i)}) := by
+    . have : trg.mapped_head[i.val] = (trg.rule.head[i]'(by rw [PreTrigger.head_length_eq_mapped_head_length]; exact i.isLt)).map (fun a => { predicate := a.predicate, terms := a.terms.map (trg.apply_to_var_or_const i), arity_ok := (by rw [List.length_map, a.arity_ok])}) := by
         unfold PreTrigger.mapped_head
         unfold PreTrigger.apply_to_function_free_atom
         simp
@@ -214,8 +215,7 @@ def SkolemObsoleteness (sig : Signature) [DecidableEq sig.P] [DecidableEq sig.C]
         cases x with
         | var => rfl
         | const => simp [PreTrigger.apply_to_var_or_const, PreTrigger.apply_to_skolemized_term, GroundSubstitution.apply_skolem_term, PreTrigger.skolemize_var_or_const, VarOrConst.skolemize]
-      rw [this]
-
+      simp only [this]
       apply h
   contains_trg_result_implies_cond := by
     intro trg F i result_in_F