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

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.

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

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.
Proof. move⇒ x. exact: FixI. Qed.

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

Lemma fix_unfold :
  monotone F → Fix F <<= F (Fix F).
Proof. move⇒ mono 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.
Proof.
  move⇒ h x. split; by apply: fix_mono ⇒ {x}x P/h.
Qed.

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

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

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

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

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).
Proof.
  move⇒ P Q h. apply: fix_mono ⇒ I. exact: mono.
Qed.

Lemma chain_le (Q : NPred X) m n :
  chain Q → m ≤ n → Q m <<= Q n.
Proof.
  move⇒ cQ /leP. elim=>//k _ ih x /ih. exact: cQ.
Qed.

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

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

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

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

Lemma star_trans y x z : star x y → star y z → star x z.
Proof. move⇒ A. elim⇒ //={z} y´ z _. exact: starSR. Qed.

Lemma starRS x y z : R x y → star y z → star x z.
Proof. move/star1. exact: star_trans. Qed.

End Star.

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