File TEST_ProofMode_relative_completeness

From MatchingLogic Require Import Logic ProofMode.MLPM.

Import
  MatchingLogic.Logic.Notations
  MatchingLogic.DerivedOperators_Syntax.Notations
.


Section with_signature.

Context {Σ : Signature}.

Local Lemma P1_complete (Γ : Theory) (ϕ ψ : Pattern):
  well_formed ϕ → well_formed ψ →
  mkMLGoal _ Γ [] (ϕ ---> ψ ---> ϕ) BasicReasoning.

Local Lemma P2_complete (Γ : Theory) (ϕ ψ ξ : Pattern):
  well_formed ϕ → well_formed ψ → well_formed ξ →
  mkMLGoal _ Γ [] ((ϕ ---> ψ ---> ξ) ---> (ϕ ---> ψ) ---> ϕ ---> ξ) BasicReasoning.

Local Lemma P3_complete Γ ϕ :
  well_formed ϕ →
  mkMLGoal _ Γ [] (! ! ϕ ---> ϕ) BasicReasoning.

Local Lemma MP_complete Γ ϕ ψ i:
  well_formed ϕ → well_formed ψ →
  mkMLGoal _ Γ [] ϕ i → mkMLGoal _ Γ [] (ϕ ---> ψ) i →
  mkMLGoal _ Γ [] ψ i.

Local Lemma Ex_quan_complete (Γ : Theory) (ϕ : Pattern) (y : evar):
  well_formed (ex , ϕ) →
  mkMLGoal _ Γ [] ((ex , ϕ)^[patt_free_evar y] ---> (ex , ϕ)) BasicReasoning.

Local Lemma Ex_gen_complete (Γ : Theory) (ϕ₁ ϕ₂ : Pattern) (x : evar) (i : ProofInfo):
  well_formed ϕ₁ → well_formed ϕ₂ →
  ProofInfoLe (ExGen := {[x]}, SVSubst := ∅, KT := false, AKT := false) i →
  x ∉ free_evars ϕ₂ →
  mkMLGoal _ Γ [] (ϕ₁ ---> ϕ₂) i →
  mkMLGoal _ Γ [] (exists_quantify x ϕ₁ ---> ϕ₂) i.

End with_signature.