File DeductionTheorem

From MatchingLogic Require Export Definedness_ProofSystem.
Import MatchingLogic.Logic.Notations
       MatchingLogic.Theories.Definedness_Syntax.Notations.


Open Scope list_scope.

(* TODO: These 3 lemmas are used only here as is, but maybe it should be somewhere else? *)
Local Lemma impl_ctx_impl {Σ : Signature} Γ ctx ϕ ψ i :
  well_formed ϕ →
  well_formed ψ →
  well_formed (pcPattern ctx) →
  ProofInfoLe AnyReasoning i →
  Γ ⊢i ϕ ---> ψ using i →
  (is_positive_context ctx →
  Γ ⊢i (emplace ctx ϕ) ---> (emplace ctx ψ) using i)
  ×
  (is_negative_context ctx →
  Γ ⊢i (emplace ctx ψ) ---> (emplace ctx ϕ) using i).
Lemma impl_ctx_impl_pos {Σ : Signature} Γ ctx ϕ ψ i :
  well_formed ϕ →
  well_formed ψ →
  well_formed (pcPattern ctx) →
  is_positive_context ctx →
  ProofInfoLe AnyReasoning i →
  Γ ⊢i ϕ ---> ψ using i →
  Γ ⊢i (emplace ctx ϕ) ---> (emplace ctx ψ) using i.

Lemma impl_ctx_impl_neg {Σ : Signature} Γ ctx ϕ ψ i :
  well_formed ϕ →
  well_formed ψ →
  well_formed (pcPattern ctx) →
  is_negative_context ctx →
  ProofInfoLe AnyReasoning i →
  Γ ⊢i ϕ ---> ψ using i →
  Γ ⊢i (emplace ctx ψ) ---> (emplace ctx ϕ) using i.

(* Lemma 88 in in the matching mu logic paper.*)
Lemma pred_and_ctx_and {Σ : Signature} {syntax : Syntax} Γ ctx ϕ ψ:
  Definedness_Syntax.theory ⊆ Γ →
  well_formed ϕ →
  well_formed ψ →
  well_formed (pcPattern ctx) →
  mu_in_evar_path (pcEvar ctx) (pcPattern ctx) 0 = false →
  Γ ⊢ is_predicate_pattern ψ →
  Γ ⊢ ψ and (emplace ctx ϕ) <---> ψ and (emplace ctx (ψ and ϕ)).

(* Lemma 89 *)
(* TODO: it is worth splitting this theorem, since the ---> direction requires
         fewer side conditions *)
Lemma mu_and_predicate_propagation {Σ : Signature} {syntax : Syntax} Γ ϕ ψ :
  Definedness_Syntax.theory ⊆ Γ →
  well_formed (mu, ϕ) →
  well_formed ψ →
  (* "Let X be a set variable that does not occur under any µ-binder in ϕ" *)
  bound_svar_is_banned_under_mus ϕ 0 0 →
  Γ ⊢ is_predicate_pattern ψ →
  Γ ⊢ (mu, (ψ and ϕ)) <---> (ψ and (mu, ϕ)).

Theorem deduction_theorem {Σ : Signature} {syntax : Syntax} Γ ϕ ψ
  (gpi : ProofInfo)
  (pf : Γ ∪ {[ ψ ]} ⊢i ϕ using gpi) :
  well_formed ϕ →
  well_formed ψ →
  theory ⊆ Γ →
  pi_generalized_evars gpi ## (gset_to_coGset (free_evars ψ)) →
  pi_substituted_svars gpi ## (gset_to_coGset (free_svars ψ)) →
  pi_uses_advanced_kt gpi = false →
  Γ ⊢i ⌊ ψ ⌋ ---> ϕ
  using AnyReasoning.

Lemma MLGoal_deduct'
  {Σ : Signature}
  {syntax : Syntax}
  (Γ : Theory)
  (l : hypotheses)
  name
  (ψ g : Pattern)
  (C : PatternCtx)
  (i : ProofInfo)
  :
  theory ⊆ Γ →
  pi_generalized_evars i ## gset_to_coGset (free_evars ψ) →
  pi_substituted_svars i ## gset_to_coGset (free_svars ψ) →
  pi_uses_advanced_kt i = false →
  mkMLGoal Σ (Γ ∪ {[ψ]}) l g i →
  mkMLGoal Σ Γ ((mkNH _ name ⌊ ψ ⌋) :: l) g AnyReasoning .
Lemma MLGoal_deduct
  {Σ : Signature}
  {syntax : Syntax}
  (Γ : Theory)
  (l₁ l₂ : hypotheses)
  name
  (ψ g : Pattern)
  :
  theory ⊆ Γ →
  mkMLGoal Σ (Γ ∪ {[ψ]}) (l₁ ++ l₂) g
    ((ExGen := ⊤ ∖ gset_to_coGset (free_evars ψ), SVSubst := ⊤ ∖ gset_to_coGset (free_svars ψ), KT := true, AKT := false)) →
  mkMLGoal Σ Γ (l₁ ++ (mkNH _ name ⌊ ψ ⌋) :: l₂) g AnyReasoning .

Tactic Notation "mlDeduct" constr(name) :=
  _ensureProofMode;
  _mlReshapeHypsByName name;
  apply MLGoal_deduct;
  [try assumption|_mlReshapeHypsBack]
.

#[local]
Example ex_deduct
  {Σ : Signature} {syntax : Syntax} (Γ : Theory) (ϕ₁ ϕ₂ ϕ₃ : Pattern)
  :
  well_formed ϕ₁ →
  well_formed ϕ₂ →
  well_formed ϕ₃ →
  theory ⊆ Γ →
  Γ ⊢ ϕ₁ ---> ⌊ ϕ₂ ⌋ ---> ϕ₃ ---> ϕ₂
.
Lemma equality_elimination
  {Σ : Signature}
  {sy : Definedness_Syntax.Syntax}
  Γ φ1 φ2 C
  (HΓ : theory ⊆ Γ)
  (WF1 : well_formed φ1)
  (WF2 : well_formed φ2)
  (WFC : PC_wf C)
  (Hmu : pattern_kt_well_formed (pcPattern C))
  
:
  Γ ⊢i (φ1 =ml φ2) --->
    (emplace C φ1) ---> (emplace C φ2)
  using AnyReasoning.