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

Section Definitions.
Variable (X : Type).

Definition Pred := X → Prop.
Definition NPred := nat → X → Prop.

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 x ⇒ P x ∨ Q x.
Definition cap (P Q : Pred) : Pred := fun x ⇒ P x ∧ Q x.
End Definitions.


Notation "F <<= G" := (∀ x, F x → G 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 X → Pred X.

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

Inductive Fix {X} (F : PredT X) (x : X) : Prop :=
| FixI (P : Pred X) : P <<= Fix F → F P x → Fix 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 F → Fix 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.

Section OmegaIteration.

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

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

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

Lemma fixk_fold :
  F fixk <<= fixk.

Lemma fixk_unfold :
  fixk <<= F fixk.

Lemma fix_fixk x :
  Fix F x ↔ fixk x.

End OmegaIteration.

Section FixContinuity.

Variable X : Type.
Variable F : Pred X → PredT X.
Variable mono : ∀ (P1 P2 Q1 Q2 : Pred X),
    P1 <<= P2 → Q1 <<= Q2 → F P1 Q1 <<= F P2 Q2.

Lemma fix_f_mono :
  monotone (Fix \o F).

Lemma chain_le (Q : NPred X) m n :
  chain Q → m ≤ n → Q m <<= Q n.

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

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

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

End FixContinuity.

Section Star.

Variables (X : Type) (R : X → X → Prop).
Implicit Types (R S : X → X → Prop).

Inductive star (x : X) : Pred X :=
| starxx : star x x
| starSR y z : star x y → R y z → star x z.

Hint Resolve starxx.

Lemma star1 x y : R x y → star x y.

Lemma star_trans y x z : star x y → star y z → star x z.

Lemma starRS x y z : R x y → star y z → star x z.

End Star.

Hint Resolve starxx.