File ContextualImplication

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


(* TODO split this file into syntax / proof system parts*)

Record StructureContext {Σ : Signature} := mkStructureContext {
    sc_ac : Application_context ;
    sc_pred : Pattern ;
}.

Definition sc_valid
    {Σ : Signature}
    {definedness_syntax : Definedness_Syntax.Syntax}
    (Γ : Theory)
    (SC : StructureContext)
    := Γ ⊢ (sc_pred SC)
.

Definition sc_plug
    {Σ : Signature}
    {definedness_syntax : Definedness_Syntax.Syntax}
    (SC : StructureContext)
    (ϕ : Pattern)
    : Pattern
    := patt_and (subst_ctx (sc_ac SC) ϕ) (sc_pred SC)
.

Definition sc2pctx
    {Σ : Signature}
    {definedness_syntax : Definedness_Syntax.Syntax}
    (SC : StructureContext)
    : PatternCtx
    :=
    let boxvar := (evar_fresh_s ((free_evars_ctx (sc_ac SC)) ∪ (free_evars (sc_pred SC)))) in
    {| pcEvar := boxvar ;
       pcPattern := (ApplicationContext2Pattern boxvar (sc_ac SC)) and (sc_pred SC) ;
    |}
.

Definition patt_set_builder
    {Σ : Signature}
    (ψ : Pattern)
    : Pattern
    := patt_exists (patt_and (patt_bound_evar 0) ψ)
.

Lemma set_builder_full_1
    {Σ : Signature}
    {definedness_syntax : Definedness_Syntax.Syntax}
    (Γ : Theory)
    (ϕ : Pattern)
    :
    Definedness_Syntax.theory ⊆ Γ →
    well_formed ϕ →
    Γ ⊢ ϕ ---> (patt_set_builder ((patt_bound_evar 0) ∈ml ϕ))
.

Lemma set_builder_full_2
    {Σ : Signature}
    {definedness_syntax : Definedness_Syntax.Syntax}
    (Γ : Theory)
    (ϕ : Pattern)
    :
    Definedness_Syntax.theory ⊆ Γ →
    well_formed ϕ →
    Γ ⊢ (patt_set_builder ((patt_bound_evar 0) ∈ml ϕ)) ---> ϕ
.

Lemma set_builder_full_iff
    {Σ : Signature}
    {definedness_syntax : Definedness_Syntax.Syntax}
    (Γ : Theory)
    (ϕ : Pattern)
    :
    Definedness_Syntax.theory ⊆ Γ →
    well_formed ϕ →
    Γ ⊢ (ϕ) <---> (patt_set_builder ((patt_bound_evar 0) ∈ml ϕ))
.

(*
  We need recursive symbols here, for which we need product sorts.
*)

Lemma set_builder_full
    {Σ : Signature}
    {definedness_syntax : Definedness_Syntax.Syntax}
    (Γ : Theory)
    (ϕ : Pattern)
    :
    Definedness_Syntax.theory ⊆ Γ →
    well_formed ϕ →
    Γ ⊢ (ϕ) =ml (patt_set_builder ((patt_bound_evar 0) ∈ml ϕ))
.

Definition contextual_implication
    {Σ : Signature}
    {definedness_syntax : Definedness_Syntax.Syntax}
    (SC : StructureContext)
    (ψ : Pattern)
    := patt_set_builder (patt_subseteq (sc_plug SC (patt_bound_evar 0)) ψ)
.

Lemma wrap_unwrap_helper
    {Σ : Signature}
    {definedness_syntax : Definedness_Syntax.Syntax}
    (Γ : Theory)
    (SC : StructureContext)
    :
    Definedness_Syntax.theory ⊆ Γ →
    sc_valid Γ SC →
    (∀ (ϕ ψ : Pattern),
        well_formed ϕ →
        well_formed ψ →
        Γ ⊢ is_predicate_pattern ψ →
        Γ ⊢ (sc_plug SC (ϕ and ψ)) =ml ((sc_plug SC ϕ) and ψ)
    ) →
    (* FIXME I didn't understood from the paper whether ϕ is quantified here,
       or whether it is the same as in the conclusion. *)
    (∀ (ϕ: Pattern),
        well_formed (patt_exists ϕ) →
        Γ ⊢ (sc_plug SC (patt_exists ϕ)) =ml patt_exists (sc_plug SC ϕ)
    ) →
    ∀ (ϕ : Pattern),
        well_formed ϕ →
        Γ ⊢ (sc_plug SC ϕ) =ml (ϕ ---> (contextual_implication SC ϕ))
.