# Companions in Classical Type Theory

In classical type theory, we can extend the tower induction principle to all predicates which are closed under infima of chains.

From Companion Require Import prelim companion.

Definition chain {A : proType} I (F : I -> A) :=
forall i j, F i <= F j \/ F j <= F i.

Section ClassicalTowers.
Variables (A : clat) (f : A -> A).
Hypothesis (fP : monotone f).

Local Notation T := (T f).
Local Notation t := (t f).

Section TowerDoubleInd.
Variable R : Rel A.
Hypothesis step : forall x y,
T x -> T y -> R x y -> R y x -> R y (f x).
Hypothesis limit : forall I (F : I -> A) x,
T x -> (forall i, T (F i)) -> (forall i, R x (F i)) -> R x (inf F).

Lemma T_ind2 x y :
T x -> T y -> R x y.
Proof.
move=> tp tq. elim: tq x tp => {y}[x tx ih y ty|I F tF ih x tx].
- apply: step => //; last by exact: ih. elim: ty => {y}; eauto.
- apply: limit => // i. exact: ih.
Qed.
End TowerDoubleInd.

Lemma tower_dec x : T x -> f x <= x.
Proof. move=> /t_img<-. exact: t_fold. Qed.

Hypothesis xm : forall P, P \/ ~P.

Lemma xm_lb I (F : I -> A) x :
is_lb F x \/ exists i, ~x <= F i.
Proof.
case: (xm (exists i, ~x <= F i)) => h. by right. left=> i.
case: (xm (x <= F i)) => g //. case: h. by exists i.
Qed.

Lemma tower_f_linear x y :
T x -> T y -> x <= y \/ y <= f x.
Proof.
move: x y. apply T_ind2 => [x y tx ty ih _|I F x tx tF ih].
- case: ih => le1. right. exact: mono. by left.
- case: (xm_lb F x) => [lb|[i neq]].
+ left. exact: infI.
+ case: (ih i) => le //. right. exact: infE le.
Qed.

Corollary tower_linear x y :
T x -> T y -> x <= y \/ y <= x.
Proof.
move=> tx ty. case: (tower_f_linear tx ty) => h. by left.
right. rewrite h. exact: tower_dec.
Qed.

Corollary tower_ind_classical (P : Pred A) :
(forall I (F : I -> A), chain F -> (forall i, P (F i)) -> P (inf F)) ->
(forall x, P (t x) -> P (f (t x))) ->
forall x, P (t x).
Proof.
move=> h1 h2. suff: forall x, T x -> P x. move=> h x. apply: h. exact: T_t.
move=> x. elim=> {x}[x /t_img tx ih|I F tF ih]. rewrite -tx. apply: h2.
by rewrite tx. apply: h1 ih. move=> i j. apply: tower_linear; exact: tF.
Qed.
End ClassicalTowers.