# Inf-closed co-induction and sup-closed induction

## Directed and codirected families.

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.

## Inf-closed induction through closure operators.

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.

## Pataraia's fixed point theorem as an induction principle for greatest-fixed points.

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.

## Direct (co)induction

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.*)