diff --git a/ProofLibrary.lean b/ProofLibrary.lean index 19f80a0..e0cc6e1 100644 --- a/ProofLibrary.lean +++ b/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 diff --git a/ProofLibrary/AlternativeMatches/Chase.lean b/ProofLibrary/AlternativeMatches/Chase.lean index 65e53f5..ee4b808 100644 --- a/ProofLibrary/AlternativeMatches/Chase.lean +++ b/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 diff --git a/ProofLibrary/AlternativeMatches/HomomorphismExtension.lean b/ProofLibrary/AlternativeMatches/HomomorphismExtension.lean index 75f0d3d..506867b 100644 --- a/ProofLibrary/AlternativeMatches/HomomorphismExtension.lean +++ b/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'] diff --git a/ProofLibrary/ChaseSequence/Termination.lean b/ProofLibrary/ChaseSequence/Termination/Basic.lean similarity index 100% rename from ProofLibrary/ChaseSequence/Termination.lean rename to ProofLibrary/ChaseSequence/Termination/Basic.lean diff --git a/ProofLibrary/ChaseSequence/Termination/MfaLike.lean b/ProofLibrary/ChaseSequence/Termination/MfaLike.lean new file mode 100644 index 0000000..4193229 --- /dev/null +++ b/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 + ⟩ + diff --git a/ProofLibrary/ChaseSequence/Universality.lean b/ProofLibrary/ChaseSequence/Universality.lean index 9ba3d7f..f45fcb6 100644 --- a/ProofLibrary/ChaseSequence/Universality.lean +++ b/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 diff --git a/ProofLibrary/KnowledgeBaseBasics.lean b/ProofLibrary/KnowledgeBaseBasics.lean index 1d82a29..10efa6d 100644 --- a/ProofLibrary/KnowledgeBaseBasics.lean +++ b/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,7 +61,7 @@ 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 @@ -65,14 +69,24 @@ namespace FunctionFreeAtom 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) diff --git a/ProofLibrary/SubstitutionAndHomomorphismBasics.lean b/ProofLibrary/SubstitutionAndHomomorphismBasics.lean index e15ecd6..ec48835 100644 --- a/ProofLibrary/SubstitutionAndHomomorphismBasics.lean +++ b/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 diff --git a/ProofLibrary/TermBasics.lean b/ProofLibrary/TermBasics.lean index 573f98c..dd0966d 100644 --- a/ProofLibrary/TermBasics.lean +++ b/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 diff --git a/ProofLibrary/Trigger.lean b/ProofLibrary/Trigger.lean index 146556e..48563f6 100644 --- a/ProofLibrary/Trigger.lean +++ b/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