File monotonic

From Coq Require Import Ensembles.
From MatchingLogic Require Export Semantics.

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

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

  (* Definitions and lemmas inside this section are useful for proving `is_monotonic`,
   but they are probably not usefull for any other purpose. *)
  Section respects_blacklist.
    (* Bp - Blacklist of Positive Occurrence - these variables can occur only negatively.
     Bn - Blacklist of Negative Occurrence - these variables can occur only positively *)
    Definition respects_blacklist (phi : Pattern) (Bp Bn : Ensemble svar) : Prop :=
      ∀ (var : svar),
        (Bp var → svar_has_positive_occurrence var phi = false) ∧ (Bn var → @svar_has_negative_occurrence Σ var phi = false).

    Lemma respects_blacklist_app : ∀ (phi1 phi2 : Pattern) (Bp Bn : Ensemble svar),
        respects_blacklist phi1 Bp Bn → respects_blacklist phi2 Bp Bn →
        respects_blacklist (phi1 ⋅ phi2)%ml Bp Bn.

    Lemma respects_blacklist_app_1 : ∀ (phi1 phi2 : Pattern) (Bp Bn : Ensemble svar),
        respects_blacklist (phi1 ⋅ phi2)%ml Bp Bn → respects_blacklist phi1 Bp Bn.

    (* This proof is the same as for app_1 *)
    Lemma respects_blacklist_app_2 : ∀ (phi1 phi2 : Pattern) (Bp Bn : Ensemble svar),
        respects_blacklist (phi1 ⋅ phi2) Bp Bn → respects_blacklist phi2 Bp Bn.

    Lemma respects_blacklist_impl : ∀ (phi1 phi2 : Pattern) (Bp Bn : Ensemble svar),
        respects_blacklist phi1 Bn Bp → respects_blacklist phi2 Bp Bn →
        respects_blacklist (phi1 ---> phi2) Bp Bn.

    Lemma respects_blacklist_impl_1 : ∀ (phi1 phi2 : Pattern) (Bp Bn : Ensemble svar),
        respects_blacklist (phi1 ---> phi2) Bp Bn → respects_blacklist phi1 Bn Bp.

    Lemma respects_blacklist_impl_2 : ∀ (phi1 phi2 : Pattern) (Bp Bn : Ensemble svar),
        respects_blacklist (phi1 ---> phi2) Bp Bn → respects_blacklist phi2 Bp Bn.

    Lemma respects_blacklist_ex : ∀ (phi : Pattern) (Bp Bn : Ensemble svar),
        respects_blacklist (patt_exists phi) Bp Bn → respects_blacklist phi Bp Bn.

    Lemma respects_blacklist_ex' : ∀ (phi : Pattern) (Bp Bn : Ensemble svar),
        respects_blacklist phi Bp Bn → respects_blacklist (patt_exists phi) Bp Bn.

    Lemma respects_blacklist_mu : ∀ (phi : Pattern) (Bp Bn : Ensemble svar),
        respects_blacklist (patt_mu phi) Bp Bn → respects_blacklist phi Bp Bn.

    Lemma respects_blacklist_mu' : ∀ (phi : Pattern) (Bp Bn : Ensemble svar),
        respects_blacklist phi Bp Bn → respects_blacklist (patt_mu phi) Bp Bn.

    Lemma respects_blacklist_union : ∀ (phi : Pattern) (Bp1 Bn1 Bp2 Bn2 : Ensemble svar),
        respects_blacklist phi Bp1 Bn1 →
        respects_blacklist phi Bp2 Bn2 →
        respects_blacklist phi (Ensembles.Union svar Bp1 Bp2) (Ensembles.Union svar Bn1 Bn2).

    Lemma positive_occurrence_respects_blacklist_svar_open :
      ∀ (phi : Pattern) (dbi : db_index) (X : svar),
        no_negative_occurrence_db_b dbi phi →
        X ∉ (free_svars phi) →
        respects_blacklist (phi^{svar: dbi ↦ X}) (Empty_set svar) (Ensembles.Singleton svar X).

    Lemma mu_wellformed_respects_blacklist : ∀ (phi : Pattern) (X : svar),
        well_formed_positive (patt_mu phi) →
        svar_is_fresh_in X phi →
        respects_blacklist (phi^{svar: 0 ↦ X}) (Empty_set svar) (Ensembles.Singleton svar X).

    (*
Lemma respects_blacklist_ex' : forall (phi : Pattern) (Bp Bn : Ensemble svar),
    respects_blacklist ()
respects_blacklist (evar_open 0 (evar_fresh variables (free_evars phi)) phi) Bp B
     *)

    Lemma evar_open_respects_blacklist :
      ∀ (phi : Pattern) (Bp Bn : Ensemble svar) (x : evar) (n : nat),
        respects_blacklist phi Bp Bn →
        respects_blacklist (phi^{evar: n ↦ x}) Bp Bn.
  End respects_blacklist.

  (* From the following section, `update_svar_val_comm`, `update_svar_shadow`
   and `is_monotonic` may be generally useful.
   The lemma `respects_blacklist_implies_monotonic` is only a technical lemma for proving `is_monotonic`,
   which is the main lemma of the section.
   *)
  Section with_model.

    Context {M : Model}.
    Let A := propset (Domain M).
    Let OS := PropsetOrderedSet (Domain M).
    Let L := PowersetLattice (Domain M).

    Lemma respects_blacklist_implies_monotonic :
      ∀ (n : nat) (phi : Pattern),
        le (pat_size phi) n → well_formed_positive phi →
        ∀ (Bp Bn : Ensemble svar),
          respects_blacklist phi Bp Bn →
          ∀ (ρ : @Valuation _ M)
                 (X : svar),
            (Bp X →
             @AntiMonotonicFunction A OS (fun (S : propset (Domain M)) ⇒
                                            (@eval Σ M (update_svar_val X S ρ) phi)
                                         )
            ) ∧
            (Bn X →
             @MonotonicFunction A OS (fun S : propset (Domain M) ⇒
                                        (@eval Σ M (update_svar_val X S ρ) phi))
            )
    .
          Arguments LeastFixpointOf : simpl never.
          Arguments leq : simpl never.
          Arguments LeastFixpointOf : simpl never.
          Arguments leq : simpl never.
          Arguments LeastFixpointOf : simpl never.
          Arguments leq : simpl never.
          Arguments LeastFixpointOf : simpl never.
          Arguments leq : simpl never.

    Lemma is_monotonic : ∀ (phi : Pattern)
                                (X : svar)
                                (ρ : Valuation),
        well_formed_positive (mu, phi) →
        svar_is_fresh_in X phi →
        @MonotonicFunction A OS
                           (fun S : propset (Domain M) ⇒
                              (@eval Σ M (update_svar_val X S ρ)
                                                       (phi^{svar: 0 ↦ X}))).
  End with_model.

End monotonic.