File ProofSystemSoundness

From Coq Require Import Logic.Classical_Prop.
From MatchingLogic Require Export DerivedOperators_Semantics
                                  ProofSystem
                                  monotonic.

Import MatchingLogic.Syntax.Notations.
Import MatchingLogic.Substitution.Notations.
Import MatchingLogic.Semantics.Notations.
Import MatchingLogic.DerivedOperators_Syntax.Notations.
Import MatchingLogic.ProofSystem.Notations_private.

Section soundness.
  Open Scope ml_scope.

  Context {Σ : Signature}.

  (* soundness for prop_ex_right *)
  Lemma proof_rule_prop_ex_right_sound {m : Model} (theory : Theory) (phi psi : Pattern)
        (ρ : @Valuation Σ m):
    (well_formed (patt_imp (patt_app (patt_exists phi) psi) (patt_exists (patt_app phi psi)))) →
    (well_formed (ex, phi)%ml) → (@well_formed Σ psi) →
    (∀ axiom : Pattern,
        axiom ∈ theory
        → ∀ (ρ : @Valuation Σ m),
          eval ρ axiom = ⊤) →
    eval ρ ((ex , phi) ⋅ psi ---> ex , phi ⋅ psi)%ml = ⊤.

(* soundness for prop_ex_left *)
  Lemma proof_rule_prop_ex_left_sound {m : Model} (theory : Theory) (phi psi : Pattern)
        (ρ : @Valuation Σ m):
    (well_formed (patt_imp (patt_app psi (patt_exists phi)) (patt_exists (patt_app psi phi)))) →
    (well_formed (ex, phi)%ml) → (@well_formed Σ psi) →
    (∀ axiom : Pattern,
        axiom ∈ theory
        → ∀ (ρ : @Valuation Σ m),
          eval ρ axiom = ⊤) →
    eval ρ (psi ⋅ (ex , phi) ---> ex , psi ⋅ phi)%ml = ⊤.

(* free_svar_subst maintains soundness *)
Lemma proof_rule_set_var_subst_sound {m : Model}: ∀ phi psi,
  well_formed_closed phi → well_formed psi →
  (∀ (ρ : @Valuation Σ m),
      eval ρ phi = ⊤)
  →
  ∀ X ρ,
    @eval Σ m ρ (phi^[[svar: X ↦ psi]]) = ⊤.

(* Soundness theorem *)
Theorem Soundness :
  ∀ phi : Pattern, ∀ theory : Theory,
  well_formed phi → (theory ⊢H phi) → (theory ⊨ phi).

End soundness.