Library ChargeCore.Logics.Pure

From ChargeCore.Logics Require Import ILogic ILInsts BILogic ILEmbed.
Require Import Coq.Setoids.Setoid.
Require Import Coq.Classes.Morphisms.

Set Implicit Arguments.
Unset Strict Implicit.
Set Maximal Implicit Insertion.

Section Pure.

  Context {A : Type} {ILOPs : ILogicOps A} {BILOps : BILogicOps A}.

  Class PureOp := {
    pure : A -> Prop
  }.

  Definition parameter_pure (pure : A -> Prop) (P : A) : Prop :=
    (forall Q, P //\\ Q |-- P ** Q) /\
    (forall Q, pure Q -> P ** Q |-- P //\\ Q) /\
    (forall Q R, (P //\\ Q) ** R -|- P //\\ (Q ** R)) /\
    (forall Q, P -* Q |-- P -->> Q) /\
    (forall Q, pure Q -> P -->> Q |-- P -* Q).

  Class Pure {HP : PureOp} :=
  { pure_axiom : forall p, pure p -> parameter_pure pure p
  ; pure_proper : Proper (lequiv ==> iff) pure
  }.

  Existing Class pure.

  Context (IL : ILogic A) (BIL : BILogic A) (po : PureOp) (p : @Pure po).

  Lemma pureandsc P Q : pure P -> P //\\ Q |-- P ** Q.
  Proof.
    intros. eapply pure_axiom in H. destruct H. intuition.
  Qed.

  Lemma purescand P Q : pure P -> pure Q -> P ** Q |-- P //\\ Q.
  Proof.
    intros. eapply pure_axiom in H. destruct H. intuition.
  Qed.

  Lemma pureandscD P Q R : pure P -> (P //\\ Q) ** R -|- P //\\ (Q ** R).
  Proof.
    intros. eapply pure_axiom in H; destruct H; intuition.
  Qed.

  Lemma puresiimpl P Q : pure P -> P -* Q |-- P -->> Q.
  Proof.
    intros. eapply pure_axiom in H; destruct H; intuition.
  Qed.

  Lemma pureimplsi P Q : pure P -> pure Q -> P -->> Q |-- P -* Q.
  Proof.
    intros. eapply pure_axiom in H; destruct H; intuition.
  Qed.


End Pure.

Arguments Pure {A ILOPs BILOps} HP : rename.
Arguments PureOp _ : rename, clear implicits.