File Sorts_Semantics

From Coq Require Import Classes.Morphisms_Prop.
From MatchingLogic Require Export Definedness_Semantics
                                  Sorts_Syntax.
Import MatchingLogic.Logic.Notations
       MatchingLogic.Theories.Definedness_Syntax.Notations
       MatchingLogic.Theories.Sorts_Syntax.Notations.


Section with_model.
    Context
      {Σ : Signature}
      {syntax : Sorts_Syntax.Syntax}
      {M : Model}.
    Hypothesis M_satisfies_theory : M ⊨ᵀ Definedness_Syntax.theory.

    Definition Mpatt_inhabitant_set m := app_ext (sym_interp M (sym_inj sym_inh)) {[m]}.

    (* ϕ is expected to be a sort pattern *)
    Definition Minterp_inhabitant (ϕ : Pattern) (ρ : Valuation)
      := @eval Σ M ρ (patt_app inhabitant ϕ).

    Lemma eval_forall_of_sort_predicate s ϕ ρ:
      let x := fresh_evar ϕ in
      M_predicate M (ϕ^{evar: 0 ↦ x}) →
      eval ρ (patt_sorted_forall s ϕ) = ⊤
      ↔ (∀ m : Domain M, m ∈ Minterp_inhabitant s ρ →
                           eval (update_evar_val x m ρ) (ϕ^{evar: 0 ↦ x}) = ⊤).

    Lemma eval_exists_of_sort_predicate s ϕ ρ:
      let x := fresh_evar ϕ in
      M_predicate M (ϕ^{evar: 0 ↦ x}) →
      eval ρ (patt_sorted_exists s ϕ) = ⊤
      ↔ (∃ m : Domain M, m ∈ Minterp_inhabitant s ρ ∧
                           eval (update_evar_val x m ρ) (ϕ^{evar: 0 ↦ x}) = ⊤).

    Lemma M_predicate_exists_of_sort s ϕ :
      let x := fresh_evar ϕ in
      M_predicate M (ϕ^{evar: 0 ↦ x}) → M_predicate M (patt_sorted_exists s ϕ).

    Hint Resolve M_predicate_exists_of_sort : core.

    Lemma M_predicate_forall_of_sort s ϕ :
      let x := fresh_evar ϕ in
      M_predicate M (ϕ^{evar: 0 ↦ x}) → M_predicate M (patt_sorted_forall s ϕ).

    Hint Resolve M_predicate_forall_of_sort : core.

    Lemma interp_total_function f s₁ s₂ ρ :
      @eval Σ M ρ (patt_total_function f s₁ s₂) = ⊤ ↔
      is_total_function f (Minterp_inhabitant s₁ ρ) (Minterp_inhabitant s₂ ρ) ρ.

    Lemma interp_partial_function f s₁ s₂ ρ :
      @eval Σ M ρ (patt_partial_function f s₁ s₂) = ⊤ ↔
      ∀ (m₁ : Domain M),
        m₁ ∈ Minterp_inhabitant s₁ ρ →
        ∃ (m₂ : Domain M),
          m₂ ∈ Minterp_inhabitant s₂ ρ ∧
          (app_ext (@eval Σ M ρ f) {[m₁]})
            ⊆ {[m₂]}.

    Lemma Minterp_inhabitant_evar_open_update_evar_val ρ x e s m:
      evar_is_fresh_in x s →
      m ∈ Minterp_inhabitant ((nest_ex s)^{evar: 0 ↦ x}) (update_evar_val x e ρ)
      ↔ m ∈ Minterp_inhabitant s ρ.

    Lemma interp_partial_function_injective f s ρ :
      @eval Σ M ρ (patt_partial_function_injective f s) = ⊤ ↔
      ∀ (m₁ : Domain M),
        m₁ ∈ Minterp_inhabitant s ρ →
        ∀ (m₂ : Domain M),
          m₂ ∈ Minterp_inhabitant s ρ →
          (rel_of ρ f) m₁ ≠ ∅ →
          (rel_of ρ f) m₁ = (rel_of ρ f) m₂ →
          m₁ = m₂.

    Lemma interp_total_function_injective f s ρ :
      @eval Σ M ρ (patt_total_function_injective f s) = ⊤ ↔
      total_function_is_injective f (Minterp_inhabitant s ρ) ρ.

    Lemma eval_exists_of_sort
      (s : Pattern)
      (ρ : Valuation)
      (indec : ∀ (m : Domain M), Decision (m ∈ Minterp_inhabitant s ρ))
      (ϕ : Pattern):
    eval ρ (patt_sorted_exists s ϕ)
    = stdpp_ext.propset_fa_union (λ (m : Domain M),
      match (indec m) with
      | left _ ⇒ eval (update_evar_val (fresh_evar ϕ) m ρ) (ϕ^{evar: 0 ↦ (fresh_evar ϕ)})
      | right _ ⇒ ∅
      end
    ).

    Lemma eval_forall_of_sort
      (s : Pattern)
      (ρ : Valuation)
      (indec : ∀ (m : Domain M), Decision (m ∈ Minterp_inhabitant s ρ))
      (ϕ : Pattern):
    eval ρ (patt_sorted_forall s ϕ)
    = stdpp_ext.propset_fa_intersection (λ (m : Domain M),
      match (indec m) with
      | left _ ⇒ eval (update_evar_val (fresh_evar ϕ) m ρ) (ϕ^{evar: 0 ↦ (fresh_evar ϕ)})
      | right _ ⇒ ⊤
      end
    ).

  End with_model.

#[export]
Hint Resolve M_predicate_exists_of_sort : core.

#[export]
Hint Resolve M_predicate_forall_of_sort : core.