gfp_leq_Chain example

gfp_leq_Chain.v

From Coq Require Import RelationClasses Program.Basics.
From Coinduction Require Import all.
Import CoindNotations.
Lemma gfp_leq_Chain {X} {L : CompleteLattice X} (b : mon X) (R : Chain b) :
  gfp b <= b ` R.
Proof.
  rewrite <- (gfp_fp b).
  apply b.
  eapply gfp_chain.
Qed.
Set Implicit Arguments.
Set Contextual Implicit.
Set Primitive Projections.
Section Trace.
Context {A B : Type}.
Variant traceF (trace : Type) : Type :=
| TnilF (a : A)
| TconsF (a : A) (b : B) (tr : trace).
CoInductive trace : Type := go { _observe : traceF trace }.
End Trace.
Arguments trace _ _ : clear implicits.
Arguments traceF _ _ : clear implicits.
Notation trace' A B := (traceF A B (trace A B)).
Definition observe {A B} (tr : trace A B) : trace' A B :=
@_observe A B tr.
Notation Tnil a := (go (TnilF a)).
Notation Tcons a b tr := (go (TconsF a b tr)).
Section Operations.
Context {A B : Type}.
Definition tr_app' (tr' : trace A B) : trace' A B -> trace A B :=
 cofix _tr_app (tr : trace' A B) :=
 match tr with
  | TnilF a => tr'
  | TconsF a b tr0 => Tcons a b (_tr_app (observe tr0) )
  end.
Definition tr_app : trace A B -> trace A B -> trace A B :=
 fun tr tr' => tr_app' tr' (observe tr).
End Operations.
Module TraceNotations.
Infix "+++" := tr_app (at level 60, right associativity).
End TraceNotations.
Section Eqtr.
Context {A B : Type}.
Variant eqtrb (eq : trace A B -> trace A B -> Prop) :
 trace' A B -> trace' A B -> Prop :=
| Eq_Tnil a : eqtrb eq (TnilF a) (TnilF a)
| Eq_Tcons a b tr1 tr2 (REL : eq tr1 tr2) :
   eqtrb eq (TconsF a b tr1) (TconsF a b tr2).
Hint Constructors eqtrb: core.
Definition eqtrb_ eq : trace A B -> trace A B -> Prop :=
 fun tr1 tr2 => eqtrb eq (observe tr1) (observe tr2).
Program Definition feqtr: mon (trace A B -> trace A B -> Prop) := {| body := eqtrb_ |}.
Next Obligation.
  unfold pointwise_relation, Basics.impl, eqtrb_.
  intros ?? INC ?? EQ. inversion_clear EQ; auto.
Qed.
End Eqtr.
Definition eqtr {A B} := (gfp (@feqtr A B)).
#[export] Hint Unfold eqtr: core.
#[export] Hint Constructors eqtrb: core.
Arguments eqtrb_ _ _/.
#[export] Instance Reflexive_eqtrb {A B : Type} {R} {Hr: Reflexive R} :
 Reflexive (@eqtrb A B R).
Proof. now intros [a|a b tr]; constructor. Qed.
#[export] Instance Reflexive_feqtr {A B : Type} : forall {R: Chain (@feqtr A B)}, Reflexive `R.
Proof. apply Reflexive_chain. now cbn. Qed.
#[export] Instance Symmetric_eqtrb {A B : Type} {R} {Hr: Symmetric R} :
 Symmetric (@eqtrb A B R).
Proof.
intros [a|a b tr]; intros [a'|a' b' tr'] Heq.
- inversion Heq; subst.
  constructor.
- inversion Heq.
- inversion Heq.
- inversion Heq; subst.
  constructor; now symmetry.
Qed.
#[export] Instance Symmetric_feqtr {A B : Type} : forall {R: Chain (@feqtr A B)}, Symmetric `R.
Proof.
apply Symmetric_chain. 
intros R HR.
intros x y xy.
now apply Symmetric_eqtrb.
Qed.
#[export] Instance Transitive_eqtrb {A B : Type} {R} {Hr: Transitive R} :
 Transitive (@eqtrb A B R).
Proof.
intros [xa|xa xb xtr]; intros [ya|ya yb ytr]; intros [za|za zb ztr] Heqx Heqy.
- inversion Heqx; subst.
  inversion Heqy; subst; constructor.
- inversion Heqy; subst.
- inversion Heqx.
- inversion Heqx.
- inversion Heqx.
- inversion Heqx.
- inversion Heqy.
- inversion Heqx; subst.
  inversion Heqy; subst.
  constructor; revert REL REL0; apply Hr.
Qed.
#[export] Instance Transitive_feqtr {A B : Type} : forall {R: Chain (@feqtr A B)}, Transitive `R.
Proof.
apply Transitive_chain. 
intros R HR.
intros x y z.
now apply Transitive_eqtrb.
Qed.
#[export] Instance Equivalence_eqtr {A B}: Equivalence (@eqtr A B).
Proof. split; typeclasses eauto. Qed.
#[export] Instance Proper_eqtr {A B} :
  Proper (eqtr ==> eqtr ==> flip impl) (@eqtr A B).
Proof.
unfold Proper, respectful, flip, impl; cbn.
unfold eqtr; intros.
transitivity y; auto.
symmetry in H0.
transitivity y0; auto.
Qed.
Import TraceNotations.
Lemma tr_app_unfold {A B} :
  forall (tr tr' : trace A B),
    eqtr (tr +++ tr')
      (match observe tr with
       | TnilF a => tr'
       | TconsF a b tr0 => Tcons a b (tr0 +++ tr')
       end).
Proof. intros; now step. Qed.
Lemma eqtr_Tnil_tr_app {A B} : forall a (tr : trace A B), eqtr (Tnil a +++ tr) tr.
Proof.
intros a tr.
rewrite tr_app_unfold.
reflexivity.
Qed.
Section Inftr.
Context {A B : Type}.
Variant inftrb (ifr : trace A B -> Prop) : trace' A B -> Prop :=
| Inf_Tcons a b tr (PRED : ifr tr) : inftrb ifr (TconsF a b tr).
Hint Constructors inftrb: core.
Definition inftrb_ ifr : trace A B -> Prop :=
 fun tr => inftrb ifr (observe tr).
Program Definition finftr: mon (trace A B -> Prop) := {| body := inftrb_ |}.
Next Obligation.
  unfold pointwise_relation, Basics.impl, inftrb_.
  intros PX PY PXY Z INF.
  inversion_clear INF; auto.
Qed.
End Inftr.
Definition inftr {A B} := (gfp (@finftr A B)).
#[export] Hint Unfold inftr: core.
#[export] Hint Constructors inftrb: core.
#[export] Instance inftr_upto_eqtr {A B} {R : Chain (@finftr A B)} :
 Proper (eqtr ==> flip impl) (` R).
Proof.
  apply tower.
  - unfold Proper, respectful.
    apply inf_closed_all; intros ?.
    apply inf_closed_all; intros ?.
    apply inf_closed_impl.
    now intros ???.
    apply inf_closed_impl.
    now intros ???.
    now intros ??.
  - clear R; intros R HP tr tr' EQ INF.
    apply (gfp_fp feqtr) in EQ.
    cbn in *; red in INF |- *.
    inversion EQ.
    + rewrite <- H in INF; inversion INF.
    + constructor.
      rewrite <- H in INF; inversion INF; subst.
      eapply HP; eauto.
Qed.
#[export] Instance Proper_inftr {A B} :
 Proper (eqtr ==> flip impl) (@inftr A B).
Proof. typeclasses eauto. Qed.
Lemma inftr_tr_app {A B} : forall (tr : trace A B),
 inftr tr -> forall tr', inftr (tr' +++ tr).
Proof.
  intros tr INF.
  unfold inftr.
  coinduction R H.
  intros tr'.
  rewrite tr_app_unfold.
  destruct (observe tr') eqn:?.
  - Fail apply (gfp_chain finftr).
    Succeed now eapply (gfp_chain (chain_b R)).
    Succeed now apply (@gfp_chain _ _ finftr).
    now eapply (gfp_leq_Chain finftr).
  - constructor; apply H.
Qed.