# The Companion for Typing in System F Corresponds to Size Induction

More formally, using the companion is approximately the same thing as complete induction on the depth of a derivation.
From Companion Require Import prelim companion companion_mu.
Require Import sysf.

Definition TyN n := iter n Fty bot.
Definition STy R := \sup_(n | TyN n <= R) TyN n.

Lemma T_TyN n :
T (Fty : _^r -> _^r) (TyN n).
Proof.
elim: n => /=[|n ih]. rewrite suplat_bot. exact: T_lim. exact: T_step.
Qed.

Lemma TyN_inc n :
TyN n <= Fty (TyN n).
Proof.
elim: n => [|n ih] /=. exact: botE. exact: mono.
Qed.

Global Instance TyN_mono : monotone TyN.
Proof.
move=> m n /leP. elim=> // k _ -> /=. exact: TyN_inc.
Qed.

Global Instance STy_mono : monotone STy.
Proof.
move=> R S le_r_s. apply: supEc => n h. apply: supIc _ le_refl. by rewrite h.
Qed.

Lemma ty_sty :
Ty <= STy.
Proof.
apply: ind_upto_above => /= R. apply: ind_upto R => /= R ih.
rewrite {1}ih => {ih}. move=> Gamma s A []{s A}.
- move=> x ltn. exists 1. split. apply: Fty_mono. exact: botE.
rewrite/=. by constructor.
- move=> A B s [n [p q]]. exists n.+1. split. by rewrite -p.
move=> /=. by constructor.
- move=> A B s t [m [p1 q1]] [n [p2 q2]]. case/orP: (leq_total m n) => h.
+ exists n.+1; split. exact: Fty_mono. apply: Fty_app q2. exact: (TyN_mono h).
+ exists m.+1; split. exact: Fty_mono. apply: Fty_app q1 _. exact: (TyN_mono h).
- move=> A s [m [p q]]. exists m.+1; split. exact: Fty_mono. by constructor.
- move=> A B s [m [p q]]. exists m.+1; split. exact: Fty_mono. by constructor.
Qed.

Lemma sty_ty :
STy <= Ty.
Proof.
move=>/=R. apply: supEc => i h. apply: supIc (TyN i) _ _. split.
- exact: T_TyN.
- exact: h.
- reflexivity.
Qed.

Theorem correspondence :
Ty = STy.
Proof.
apply: le_eq. exact: ty_sty. exact: sty_ty.
Qed.