Library Facts

Facts about predicates and relations

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

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.

Arguments bot {X} _.
Arguments top {X} _.

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.
Proof. movex. exact: FixI. Qed.

Lemma fix_mono :
  ( P, F P <<= G P) → Fix F <<= Fix G.
Proof. moveh1 x. elim⇒ {x} x P _ h2 /h1. exact: FixI. Qed.

Lemma fix_unfold :
  monotone FFix F <<= F (Fix F).
Proof. movemono x [P Pf]. exact: mono. Qed.

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.
  moveh x. split; by apply: fix_mono ⇒ {x}x P/h.

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.
  moveprefix x [n]. elim: n x ⇒ [|n ih]//= x h.
  apply: prefix. apply: monotonicity x h. exact: ih.

Lemma fixk_fold :
  F fixk <<= fixk.
  movex/continuity; case⇒ [|/=n h]. elim=>//=n ih. exact: monotonicity.
  by n.+1.

Lemma fixk_unfold :
  fixk <<= F fixk.
  apply: fixk_ind. exact/monotonicity/fixk_fold.

Lemma fix_fixk x :
  Fix F x fixk x.
  - elim=>{x}x P _ ih fx. apply: fixk_fold. exact: monotonicity x fx.
  - apply: fixk_ind. exact: fix_fold.

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).
  moveP Q h. apply: fix_monoI. exact: mono.

Lemma chain_le (Q : NPred X) m n :
  chain Qm nQ m <<= Q n.
  movecQ /leP. elim=>//k _ ih x /ih. exact: cQ.

Lemma chain_maxl (Q : NPred X) m n :
  chain QQ m <<= Q (maxn m n).
  move=>/chain_le. apply. exact: leq_maxl.

Lemma chain_maxr (Q : NPred X) m n :
  chain QQ n <<= Q (maxn m n).
  move=>/chain_le. apply. exact: leq_maxr.

Lemma fix_continuous :
  ( P, continuous (F P)) →
  ( Q, continuous (F^~ Q)) →
  continuous (Fix \o F).
  movec1 c2 M cM /= x. elim=>{x}x P _ ih. case/c2=>//=m.
  move=>/mono. case/(_ (M m) _ _ ih)/c1 ⇒ //.
  - moven/=. apply: fix_f_mono. exact: cM.
  - moven /= fmn. (maxn m n) ⇒ /=. apply: fix_fold.
    apply: mono x fmn. exact: chain_maxl. apply: fix_f_mono. exact: chain_maxr.

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.
Proof. exact: starSR. Qed.

Lemma star_trans y x z : star x ystar y zstar x z.
Proof. moveA. elim⇒ //={z} z _. exact: starSR. Qed.

Lemma starRS x y z : R x ystar y zstar x z.
Proof. move/star1. exact: star_trans. Qed.

End Star.

Hint Resolve starxx.
Arguments star_trans {X R} y {x z} A B.