Rename field of Obsoleteness Condition

monsterkrampe · Jul 11, 2024 · 1ff0582 · 1ff0582
1 parent 2be3778
commit 1ff0582
Show file tree

Hide file tree

Showing 2 changed files with 6 additions and 7 deletions.
diff --git a/ProofLibrary/ChaseSequence.lean b/ProofLibrary/ChaseSequence.lean
@@ -398,8 +398,8 @@ noncomputable def inductive_homomorphism (cs : ChaseSequence obs kb) (m : FactSe
       rfl 
       apply trg_variant_loaded_for_m
 
-    let obs_for_m_subs := Classical.choose (obs.implies_subs trg_variant_obsolete_on_m)
-    let h_obs_for_m_subs := Classical.choose_spec (obs.implies_subs trg_variant_obsolete_on_m)
+    let obs_for_m_subs := Classical.choose (obs.cond_implies_trg_is_satisfied trg_variant_obsolete_on_m)
+    let h_obs_for_m_subs := Classical.choose_spec (obs.cond_implies_trg_is_satisfied trg_variant_obsolete_on_m)
 
     let next_hom : GroundTermMapping := fun t =>
       match t with 

diff --git a/ProofLibrary/Trigger.lean b/ProofLibrary/Trigger.lean
@@ -110,8 +110,7 @@ end PreTrigger
 structure ObsoletenessCondition where 
   cond : PreTrigger -> FactSet -> Prop
   monotone : ∀ trg (A B : FactSet), A ⊆ B -> cond trg A -> cond trg B
-  implies_subs : cond trg F -> 
-    -- TODO: this is robsoleteness right now, maybe this should be different?
+  cond_implies_trg_is_satisfied : cond trg F -> 
     ∃ s : GroundSubstitution,
       (∀ v, v ∈ (Rule.frontier trg.rule) → s v = trg.subs v) ∧
       ((s.apply_function_free_conj trg.rule.head).toSet ⊆ F)
@@ -137,7 +136,7 @@ def SkolemObsoleteness : ObsoletenessCondition := {
     constructor
     . apply head_sub_A
     . apply A_sub_B
-  implies_subs := by 
+  cond_implies_trg_is_satisfied := by 
     intro trg F h
     exists (fun v => trg.apply_to_var_or_const (VarOrConst.var v))
     constructor
@@ -180,7 +179,7 @@ def RestrictedObsoleteness : ObsoletenessCondition := {
       constructor
       . apply applied_head_sub_A
       . apply A_sub_B
-  implies_subs := by intro _ _ h; exact h 
+  cond_implies_trg_is_satisfied := by intro _ _ h; exact h 
   contained_in_trg_result_implies_cond := by 
     intro trg F result_in_F
     let obs_subs := fun v : Variable => trg.apply_to_var_or_const (VarOrConst.var v)
@@ -222,7 +221,7 @@ namespace FactSet
   def modelsRule (fs : FactSet) (rule : Rule) : Prop :=
     ∀ (trg : Trigger obs),
       (trg.rule = rule ∧ trg.loaded fs)
-      -> obs.cond trg fs -- the rule is ractive iff it is not satisfied under FOL semantics
+      -> obs.cond trg fs 
 
   def modelsRules (fs : FactSet) (rules : RuleSet) : Prop :=
     ∀ r, r ∈ rules.rules -> fs.modelsRule obs r