Library Facts

Facts about predicates and relations

Require Export ssreflect ssrfun ssrbool eqtype ssrnat seq.
Require Export AutosubstSsr.
Set Implicit Arguments.

Predicates and predicate transformers

Section Definitions.
Variable (X : Type).

Definition Pred := XProp.
Definition NPred := natXProp.

Definition top : Pred := fun _True.
Definition bot : Pred := fun _False.

Definition Top : NPred := fun _top.
Definition Bot : NPred := fun _bot.

Definition cup (P Q : Pred) : Pred := fun xP x Q x.
Definition cap (P Q : Pred) : Pred := fun xP x Q x.
End Definitions.

Notation "F <<= G" := ( x, F xG x) (at level 70, no associativity).

Definition sup {X} (Q : NPred X) (x : X) := n, Q n x.
Definition chain {X} (Q : NPred X) := n, Q n <<= Q n.+1.

Definition PredT (X : Type) := Pred XPred X.

Definition continuous {X} (F : PredT X) :=
   (Q : NPred X), chain QF (sup Q) <<= sup (F \o Q).
Definition monotone {X} (F : PredT X) :=
   (P Q : Pred X), P <<= QF P <<= F Q.

Fixpoint of monotone predicate transformers

Inductive Fix {X} (F : PredT X) (x : X) : Prop :=
| FixI (P : Pred X) : P <<= Fix FF P xFix F x.

Section Fixpoints.
Variable (X : Type).
Variable (F G : PredT X).
Implicit Types (P Q : Pred X).

Lemma fix_fold : F (Fix F) <<= Fix F.

Lemma fix_mono :
  ( P, F P <<= G P) → Fix F <<= Fix G.

Lemma fix_unfold :
  monotone FFix F <<= F (Fix F).

End Fixpoints.

Lemma fix_ext X (F G : PredT X) :
  ( P x, F P x G P x) → x, Fix F x Fix G x.

Fixpoints of continuous predicate transformers

Section OmegaIteration.

Variables (X : Type) (F : PredT X).
Hypothesis continuity : continuous F.
Hypothesis monotonicity : monotone F.

Definition fixk := sup (fun niter n F bot).

Lemma fixk_ind (P : Pred X) :
  F P <<= Pfixk <<= P.

Lemma fixk_fold :
  F fixk <<= fixk.

Lemma fixk_unfold :
  fixk <<= F fixk.

Lemma fix_fixk x :
  Fix F x fixk x.

End OmegaIteration.

Least fixed points of continuous predicate transformers are continuous.

Section FixContinuity.

Variable X : Type.
Variable F : Pred XPredT X.
Variable mono : (P1 P2 Q1 Q2 : Pred X),
    P1 <<= P2Q1 <<= Q2F P1 Q1 <<= F P2 Q2.

Lemma fix_f_mono :
  monotone (Fix \o F).

Lemma chain_le (Q : NPred X) m n :
  chain Qm nQ m <<= Q n.

Lemma chain_maxl (Q : NPred X) m n :
  chain QQ m <<= Q (maxn m n).

Lemma chain_maxr (Q : NPred X) m n :
  chain QQ n <<= Q (maxn m n).

Lemma fix_continuous :
  ( P, continuous (F P)) →
  ( Q, continuous (F^~ Q)) →
  continuous (Fix \o F).

End FixContinuity.

Reflexive, transitive closure

Section Star.

Variables (X : Type) (R : XXProp).
Implicit Types (R S : XXProp).

Inductive star (x : X) : Pred X :=
| starxx : star x x
| starSR y z : star x yR y zstar x z.

Hint Resolve starxx.

Lemma star1 x y : R x ystar x y.

Lemma star_trans y x z : star x ystar y zstar x z.

Lemma starRS x y z : R x ystar y zstar x z.

End Star.

Hint Resolve starxx.