File DerivedOperators_Semantics

From Coq Require Import Logic.Classical_Prop.
From MatchingLogic Require Export PrePredicate.

Import MatchingLogic.Syntax.Notations.
Import MatchingLogic.Substitution.Notations.
Import MatchingLogic.DerivedOperators_Syntax.Notations.

Section with_signature.
  Context {Σ : Signature}.
  Open Scope ml_scope.

  Section with_model.
    Context {M : Model}.

    Lemma eval_not_simpl : ∀ (ρ : Valuation) (phi : Pattern),
        @eval Σ M ρ (patt_not phi) = ⊤ ∖ (eval ρ phi).

    Lemma eval_or_simpl : ∀ (ρ : Valuation) (phi1 phi2 : Pattern),
        eval ρ (patt_or phi1 phi2)
        = (eval ρ phi1) ∪ (@eval _ M ρ phi2).

    Lemma eval_or_comm : ∀ (ρ : Valuation) (phi1 phi2 : Pattern),
        @eval Σ M ρ (patt_or phi1 phi2)
        = eval ρ (patt_or phi2 phi1).

    Lemma eval_and_simpl : ∀ (ρ : Valuation)
                                                    (phi1 phi2 : Pattern),
        eval ρ (patt_and phi1 phi2)
        = (eval ρ phi1) ∩ (@eval _ M ρ phi2).

    Lemma eval_and_comm : ∀ (ρ : Valuation)
                                                   (phi1 phi2 : Pattern),
        @eval Σ M ρ (patt_and phi1 phi2)
        = eval ρ (patt_and phi2 phi1).

    Lemma eval_top_simpl : ∀ (ρ : Valuation),
        @eval Σ M ρ patt_top = ⊤.

    (* TODO prove. Maybe some de-morgan laws could be helpful in proving this? *)
    Lemma eval_iff_or : ∀ (ρ : Valuation)
                                                 (phi1 phi2 : Pattern),
        @eval Σ M ρ (patt_iff phi1 phi2)
        = eval ρ (patt_or (patt_and phi1 phi2) (patt_and (patt_not phi1) (patt_not phi2))).

    Lemma eval_iff_comm : ∀ (ρ : Valuation)
                                                   (phi1 phi2 : Pattern),
        @eval Σ M ρ (patt_iff phi1 phi2)
        = eval ρ (patt_iff phi2 phi1).

    (* TODO: forall, nu *)

  Lemma eval_iff_simpl ρ phi1 phi2:
    @eval Σ M ρ (patt_iff phi1 phi2)
    = (⊤ ∖ eval ρ phi1 ∪ eval ρ phi2) ∩ (⊤ ∖ eval ρ phi2 ∪ eval ρ phi1).

        (* if eval (phi1 ---> phi2) = Full_set,
           then eval phi1 subset eval phi2
        *)
    Lemma eval_iff_subset (ρ : Valuation)
          (phi1 : Pattern) (phi2 : Pattern) :
      eval ρ (phi1 ---> phi2)%ml = ⊤ ↔
      (eval ρ phi1) ⊆
               (@eval _ M ρ phi2).

    Lemma M_predicate_not ϕ : M_predicate M ϕ → M_predicate M (patt_not ϕ).

    Hint Resolve M_predicate_not : core.

    Lemma M_predicate_or ϕ₁ ϕ₂ : M_predicate M ϕ₁ → M_predicate M ϕ₂ → M_predicate M (patt_or ϕ₁ ϕ₂).

    Hint Resolve M_predicate_or : core.

    Lemma M_predicate_and ϕ₁ ϕ₂ : M_predicate M ϕ₁ → M_predicate M ϕ₂ → M_predicate M (patt_and ϕ₁ ϕ₂).

    Hint Resolve M_predicate_and : core.

    Lemma M_predicate_top : M_predicate M patt_top.

    Hint Resolve M_predicate_top : core.

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

    Hint Resolve M_predicate_forall : core.

    Lemma M_predicate_iff ϕ₁ ϕ₂ :
      M_predicate M ϕ₁ →
      M_predicate M ϕ₂ →
      M_predicate M (patt_iff ϕ₁ ϕ₂).

    Hint Resolve M_predicate_iff : core.

    Lemma M_pre_predicate_not ϕ :
      M_pre_predicate M ϕ →
      M_pre_predicate M (patt_not ϕ).
    Lemma M_pre_predicate_or ϕ₁ ϕ₂ :
      M_pre_predicate M ϕ₁ →
      M_pre_predicate M ϕ₂ →
      M_pre_predicate M (patt_or ϕ₁ ϕ₂).
    Lemma M_pre_predicate_and ϕ₁ ϕ₂ :
      M_pre_predicate M ϕ₁ →
      M_pre_predicate M ϕ₂ →
      M_pre_predicate M (patt_and ϕ₁ ϕ₂).
    Lemma eval_set_builder ϕ ρ :
      let x := fresh_evar ϕ in
      M_predicate M (ϕ^{evar: 0 ↦ x}) →
      (eval ρ (patt_exists (patt_and (patt_bound_evar 0) ϕ)))
      = PropSet
          (fun m : (Domain M) ⇒ eval (update_evar_val x m ρ) (ϕ^{evar: 0 ↦ x}) = ⊤).

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

    Lemma eval_and_full ρ ϕ₁ ϕ₂:
      @eval Σ M ρ (patt_and ϕ₁ ϕ₂) = ⊤
      ↔ (@eval Σ M ρ ϕ₁ = ⊤
           ∧ @eval Σ M ρ ϕ₂ = ⊤).

    Lemma eval_predicate_not ρ ϕ :
      M_predicate M ϕ →
      eval ρ (patt_not ϕ) = ⊤
      ↔ @eval Σ M ρ ϕ ≠ ⊤.

  End with_model.

  Lemma T_predicate_not Γ ϕ : T_predicate Γ ϕ → T_predicate Γ (patt_not ϕ).

  Hint Resolve T_predicate_not : core.

  Lemma T_predicate_or Γ ϕ₁ ϕ₂ : T_predicate Γ ϕ₁ → T_predicate Γ ϕ₂ → T_predicate Γ (patt_or ϕ₁ ϕ₂).

  Hint Resolve T_predicate_or : core.

  Lemma T_predicate_and Γ ϕ₁ ϕ₂ : T_predicate Γ ϕ₁ → T_predicate Γ ϕ₂ → T_predicate Γ (patt_and ϕ₁ ϕ₂).

  Hint Resolve T_predicate_or : core.

  Lemma bcmcloseex_not (l : list (db_index × evar)) (p : Pattern):
    bcmcloseex l (patt_not p) = patt_not (bcmcloseex l p).

  Lemma bcmcloseex_all (l : list (db_index × evar)) (q : Pattern) :
    bcmcloseex l (all , q)%ml =
    (all , bcmcloseex (map (λ p : nat × evar, (S p.1, p.2)) l) q)%ml.

  Lemma M_pre_pre_predicate_forall (k : db_index) M ϕ :
    M_pre_pre_predicate (S k) M ϕ →
    M_pre_pre_predicate k M (patt_forall ϕ).
  Lemma M_pre_predicate_forall M ϕ :
    M_pre_predicate M ϕ →
    M_pre_predicate M (patt_forall ϕ).

  Lemma eval_all_simpl
    (M : Model)
    (ρ : Valuation)
    (ϕ : Pattern)
    :
    eval ρ (patt_forall ϕ) =
    (let x := fresh_evar ϕ in
     propset_fa_intersection (λ e : Domain M,
      @eval _ M (update_evar_val x e ρ) (ϕ^{evar: 0 ↦ x})
     )
    ).

  Lemma exists_singleton_is_top : ∀ (M : Model) ρ φ,
      @eval _ M ρ (patt_exists (patt_and (patt_bound_evar 0) φ) --->
                  (patt_forall ((patt_bound_evar 0) ---> φ))) = ⊤.

End with_signature.

(* TODO make these a separate hintdb. *)
#[export]
Hint Resolve M_predicate_not : core.
#[export]
Hint Resolve M_predicate_or : core.
#[export]
Hint Resolve M_predicate_and : core.
#[export]
Hint Resolve M_predicate_top : core.
#[export]
Hint Resolve M_predicate_forall : core.
#[export]
Hint Resolve M_predicate_iff : core.
#[export]
Hint Resolve T_predicate_not : core.
#[export]
Hint Resolve T_predicate_or : core.
#[export]
Hint Resolve T_predicate_or : core.