Require Import base ord tower.tarski tower.associated_closure.

Definition directed {X : clat} {I} (F : I -> X) :=
  forall i j : I, exists2 k : I, F i ≤ F k & F j ≤ F k.

Definition codirected {X : clat} {I} (F : I -> X) :=
  forall i j : I, exists2 k : I, F k ≤ F i & F k ≤ F j.

Section InfClosedCoinduction.
  Variable X : clat.
  Variable f : X -> X.
  Hypothesis fP : monotone f.
  Variable P : X -> Prop.
  Hypothesis H : inf_closed P.

  Lemma inf_closed_coind :
    (forall x, P x -> P (f x)) -> P (gfp f).
  Proof.
    move=> pf. apply/closure_of_image. exact H. apply: gfp_below_coind. exact: topI.
    rewrite {1}/closure_of. apply: allEc le_refl. split.
    - apply: pf. exact: closure_of_stable.
    - rewrite -{1}gfpE. apply: mono. exact/closure_of_is_closure.
  Qed.
End InfClosedCoinduction.

Module Pataraia.
  Section WithFunction.
  Variable A : clat.
  Variable f : A -> A.
  Hypothesis f_mono : monotone f.

  Inductive T : Pred A :=
  | T_step x : T x -> T (f x)
  | T_limit I (F : I -> A) :
      codirected F ->
      (forall i, T (F i)) ->
      T (inf F).

  Lemma T_top : T ⊤.
  Proof. exact: T_limit. Qed.

  Lemma T_dec x : T x -> f x ≤ x.
  Proof.
    elim=> {x} [x _ ih|I F _ _ ih]. exact: mono.
    focus=> i. rewrite -ih. apply: mono. exact: allE.
  Qed.

  Structure infl (g : A -> A) :=
    { infl_mono :> monotone g
    ; infl_dec : forall x, T x -> g x ≤ x
    ; infl_T : forall x, T x -> T (g x)
    }.

  Lemma infl_f : infl f.
  Proof. constructor=> //. exact: @T_dec. exact: @T_step. Qed.

  Lemma infl_id : infl id.
  Proof. by constructor. Qed.

  Lemma infl_comp g1 g2 : infl g1 -> infl g2 -> infl (g1 \o g2).
  Proof.
    move=> h1 h2. constructor=> [x y le_x_y|x tx|x tx]/=.
    - apply: infl_mono => //. exact: infl_mono.
    - rewrite -{2}[x](infl_dec h2) //. apply: (infl_dec h1). exact: infl_T.
    - apply: infl_T => //. exact: infl_T.
  Qed.

  Definition infl_null (x : A) := inf (fun p : sig infl => p.1 x).

  Lemma infl_codirected x :
    T x -> codirected (fun p : {x : A -> A | infl x} => p.1 x).
  Proof.
    move=> tx [g1 gP1] [g2 gP2]. exists (exist _ (g1 \o g2) (infl_comp gP1 gP2)) => /=.
    - apply: infl_mono => //. exact: infl_dec.
    - apply: infl_dec => //. exact: infl_T.
  Qed.

  Lemma infl_null_T x : T x -> T (infl_null x).
  Proof.
    move=> tx. apply: T_limit => [|[g gP]]/=.
    exact: infl_codirected. exact: infl_T.
  Qed.

  Lemma infl_nullP : infl infl_null.
  Proof.
    constructor=> [x y le_x_y|x tx|x tx]/=.
    - rewrite/infl_null. focus=> p /=. apply: allE (p) _. case: p => g h /=. exact: infl_mono.
    - exact: allE (exist _ id infl_id) le_refl.
    - exact: infl_null_T.
  Qed.

  Definition ν : A := infl_null ⊤.

  Lemma ν_tower : T ν.
  Proof. apply: infl_null_T. exact: T_top. Qed.

  Lemma ν_inc : ν ≤ f ν.
  Proof.
    apply: allE (exist _ (f \o infl_null) _) _ => //=.
    apply: infl_comp. exact: infl_f. exact: infl_nullP.
  Qed.

  Lemma ν_min x : T x -> ν ≤ x.
  Proof.
    elim=> {x} [x _ ih|I F _ _ ih]/=.
    - rewrite ν_inc. exact: mono.
    - focus=> i. exact: ih.
  Qed.

  Lemma ν_coind (P : Pred A) :
    (forall I (F : I -> A), codirected F -> (forall i, P (F i)) -> P (inf F)) ->
    (forall x, P x -> P (f x)) ->
    P ν.
  Proof.
    move=> h1 h2. apply: (h1).
    - apply: infl_codirected. exact: T_top.
    - case=> g gP /=. suff: forall x, T x -> P x. apply. apply: infl_T => //. exact: T_top.
      move=> {g gP} x. elim=> {x}[x _ ih|I F dF _ ih].
      exact: h2. exact: h1.
  Qed.

  Lemma ν_gfp : ν = gfp f.
  Proof.
    apply: le_eq.
    - apply: gfp_below_coind => //. exact: ν_inc.
    - apply ν_coind. move=> I F _ ih. focus. exact: ih. move=> x ih. rewrite -gfpE. exact: mono.
  Qed.
  End WithFunction.
End Pataraia.

Notation T f := (@Pataraia.T _ f).

Lemma T_gfp {A : clat} (f : A -> A) (a : A) :
  monotone f -> T f a -> gfp f ≤ a.
Proof.
  move=> h1 h2. rewrite -Pataraia.ν_gfp. exact: Pataraia.ν_min.
Qed.

Lemma T_dec {A : clat} (f : A -> A) (a : A) :
  monotone f -> T f a -> f a ≤ a.
Proof.
  move=> h1 h2. exact: Pataraia.T_dec.
Qed.

Inductive C {A : clat} (f : A -> A) : Pred A :=
| C_step (a : A) : C f a -> C f (f a)
| C_limit (I : Type) (F : I -> A) :
    directed F -> (forall i, C f (F i)) -> C f (sup F).

Fact T_C {A : clat} (f : A -> A) :
  @C A f = @Pataraia.T [clat of A^r] f.
Proof with eauto using @C, @Pataraia.T.
  apply: le_eq; hnf=> a; hnf; elim...
  - move=> I F dF _ ih. rewrite -rev_allE...
  - move=> I F dF _ ih. rewrite rev_allE...
Qed.

Lemma rev_lfp {A : clat} (f : A -> A) :
  @lfp A f = @gfp [clat of A^r] f.
Proof. by rewrite lfp_def gfp_def rev_exEc. Qed.

Lemma C_lfp {A : clat} (f : A -> A) (a : A) :
  monotone f -> C f a -> a ≤ lfp f.
Proof.
  move=> h1. rewrite T_C => /T_gfp. rewrite -rev_lfp. apply.
  move=> x y h2. apply: h1. exact: h2.
Qed.

Lemma C_inc {A : clat} (f : A -> A) (a : A) :
  monotone f -> C f a -> a ≤ f a.
Proof.
  rewrite T_C => h1 /T_dec. apply=> x y h2. apply: h1. exact: h2.
Qed.

Theorem direct_coinduction {X : clat} (f : X -> X) `{monotone X X f} (P : Pred X) :
  (forall I (F : I -> X), codirected F -> (forall i, P (F i)) -> P (inf F)) ->
  (forall x, T f x -> P x -> P (f x)) ->
  P (gfp f).
Proof.
  move=> h1 h2. rewrite -(Pataraia.ν_gfp). elim: (Pataraia.ν_tower); last first.
  - move=> I F cF _ ih. exact: h1.
  - move=> x px. exact: h2.
Qed.

Theorem direct_induction {X : clat} (f : X -> X) `{monotone X X f} (P : Pred X) :
  (forall I (F : I -> X), directed F -> (forall i, P (F i)) -> P (sup F)) ->
  (forall x, C f x -> P x -> P (f x)) ->
  P (lfp f).
Proof.
  rewrite T_C. move=> h1 h2. case/(_ _ _)/Wrap: (@direct_coinduction [clat of X^r] f _ P _ h2).
  - move=> x y. exact: H.
  - move=> I F cF. exact: h1.
  - by rewrite rev_lfp.
Qed.

(*Section SupClosedInduction.
  Variable X : clat.
  Variable f : X -> X.
  Hypothesis fP : monotone f.
  Variable P : X -> Prop.
  Hypothesis H : sup_closed P.

  Lemma sup_closed_ind :
    (forall x, P x -> P (f x)) -> P (lfp f).
  Proof.
    move=> pf. case/(_ _ _)/Wrap: (@inf_closed_coind (reverse_clat X) f _ P _ pf).
    - move=> /= x y. rewrite !rev_leE. exact: mono.
    - move=> I F /H. exact.
    - suff: @gfp (reverse_clat X) f = lfp f by move->.
      by rewrite gfp_def lfp_def rev_exEc.
  Qed.
End SupClosedInduction.*)

(*Section Pataraia.
  Variable A : clat.
  Variable f : A -> A.
  Hypothesis f_mono : monotone f.

  Inductive T : Pred A :=
  | Tf x : T x -> T (f x)
  | Tsup I (F : I -> A) :
      directed F ->
      (forall i, T (F i)) ->
      T (sup F).

  Lemma T_bot : T ⊥.
  Proof.
    have->: ⊥ = sup (fun b : False => match b with end).
    - move=> t. apply: bot_def. by focus.
    - exact: Tsup.
  Qed.

  Lemma T_inc x :
    T x -> x ≤ f x.
  Proof.
    elim=> {x} x _ ih|I F _ _ ih. exact: mono.
    focus=> i. rewrite ih. apply: mono. exact: exI.
  Qed.

  Structure infl (g : A -> A) :=
    { infl_mono :> monotone g
    ; infl_inc : forall x, T x -> x ≤ g x
    ; infl_T : forall x, T x -> T (g x)
    }.

  Lemma infl_f : infl f.
  Proof.
    constructor=> //. exact: @T_inc. exact: @Tf.
  Qed.

  Lemma infl_id : infl id.
  Proof. by constructor. Qed.

  Lemma infl_comp g1 g2 : infl g1 -> infl g2 -> infl (g1 \o g2).
  Proof.
    move=> h1 h2. constructor=> x y le_x_y|x tx|x tx/=.
    - apply: infl_mono => //. exact: infl_mono.
    - rewrite {1}x(infl_inc h1) //. apply: infl_mono => //. exact: infl_inc.
    - apply: infl_T => //. exact: infl_T.
  Qed.

  Definition infl_max (x : A) := sup (fun p : sig infl => p.1 x).

  Lemma infl_max_directed x :
    T x -> directed (fun p : {x : A -> A | infl x} => p.1 x).
  Proof.
    move=> tx g1 gP1 g2 gP2. exists (exist _ (g1 \o g2) (infl_comp gP1 gP2)) => /=.
    - apply: infl_mono => //. exact: infl_inc.
    - apply: infl_inc => //. exact: infl_T.
  Qed.

  Lemma infl_max_T x : T x -> T (infl_max x).
  Proof.
    move=> tx. apply: Tsup => |[g gP]/=.
    exact: infl_max_directed. exact: infl_T.
  Qed.

  Lemma infl_infl_max : infl infl_max.
  Proof.
    constructor=> x y le_x_y|x tx|x tx/=.
    - rewrite/infl_max. focus=> p /=. apply: exI (p) _. case: p => g h /=. exact: infl_mono.
    - exact: exI (exist _ id infl_id) le_refl.
    - exact: infl_max_T.
  Qed.

  Definition μ : A := infl_max ⊥. (*sup (fun p : sig infl => p.1 ⊥).*)

  Lemma μ_tower : T μ.
  Proof. apply: infl_max_T. exact: T_bot. Qed.

  Lemma μ_fp :
    f μ = μ.
  Proof.
    apply: le_eq.
    - apply: exI (exist _ (f \o infl_max) _) _ => //=.
      apply: infl_comp. exact: infl_f. exact: infl_infl_max.
    - apply: T_inc. exact: μ_tower.
  Qed.

  Lemma μ_max x : T x -> x ≤ μ.
  Proof.
    elim=> {x} x _ ih|I F _ _ ih/=.
    - rewrite -μ_fp. exact: mono.
    - focus=> i. exact: ih.
  Qed.

  Lemma μ_ind (P : Pred A) :
    (forall I (F : I -> A), directed F -> (forall i, P (F i)) -> P (sup F)) ->
    (forall x, P x -> P (f x)) ->
    P μ.
  Proof.
    move=> h1 h2. apply: (h1).
    - apply: infl_max_directed. exact: T_bot.
    - case=> g gP /=. suff: forall x, T x -> P x. apply. apply: infl_T => //. exact: T_bot.
      move=> {g gP} x. elim=> {x}x _ ih|I F dF _ ih.
      exact: h2. exact: h1.
  Qed.

  Lemma μ_lfp : μ = lfp f.
  Proof.
    apply: le_eq.
    - apply μ_ind. move=> I F _ ih. focus. exact: ih. move=> x ih. rewrite -lfpE. exact: mono.
    - apply: lfp_above_ind => //. by rewrite μ_fp.
  Qed.
End Pataraia.*)

(*Section Determinism.
  Variable X : Type.
  Variable F : (X -> Prop) -> X -> Prop.
  Hypothesis F_mono : monotone F.
  Hypothesis F_det : forall (P : Pred X), (forall x y, P x -> P y -> x = y) -> forall x y, F P x -> F P y -> x = y.

  Lemma lfp_F_det :
    forall x y, μ F x -> μ F y -> x = y.
  Proof.
    apply μ_ind.
    - move=> I G dG ih x y. rewrite !prod_exE !prop_exE => -i hi j hj.
      case: (dG i j) => k /(_ _ hi) gkx /(_ _ hj) gky. exact: ih gkx gky.
    - move=> /= P ih. exact: F_det.
  Qed.

Section DirectedSupClosedInduction.
  Variable X : clat.
  Variable f : X -> X.
  Hypothesis fP : monotone f.
  Variable P : X -> Prop.

  Hypothesis H : forall I (F : I -> X), (forall i j, exists2 k, F i ≤ F k & F j ≤ F k) -> (forall i, P (F i)) -> P (sup F).

  Let t y := sup (fun (p : { x : X | (x ≤ y) /\ P x}) => p.1).
  (*Let t y := ∃ x | (x ≤ y) /\ P x, x.*)

  Lemma directed_sup_closed_stable y :
    P (t y).
  Proof.
    apply: H; last by case=> x  //=.
    case=> x0 le_x0_y px0 x1 [le_x1_y px1] /=.
  Qed.
End DirectedSupClosedInduction.*)

(*Lemma gfp_upto {X : clat} (f g : X -> X) :
  monotone f -> monotone g ->
  (forall x, g x ≤ x -> g (f x) ≤ f x) ->
  g (gfp f) ≤ gfp f.
Proof.
  move=> fP gP p. apply: (@inf_closed_coind X f fP (fun x => g x ≤ x)).
  - move=> I F h. focus=> i. rewrite -(h i). apply: mono. exact: allE.
  - exact: p.
Qed.*)