Require Import List Lia.
Require Import Undecidability.SystemF.SysF Undecidability.SystemF.Autosubst.syntax.
From Undecidability.SystemF.Util Require Import Facts poly_type_facts typing_facts.
Require Import ssreflect ssrbool ssrfun.
Set Default Goal Selector "!".
Local Arguments nth_error_In {A l n x}.
Local Arguments In_nth_error {A l x}.
Definition iipc2 (Gamma: environment) (t: poly_type) := exists P, typing Gamma P t.
Arguments iipc2 : simpl never.
Lemma iipc2I {Gamma P t} : typing Gamma P t -> iipc2 Gamma t.
Proof. move=> ?. eexists. by eassumption. Qed.
Lemma iipc2_weakening {Gamma Gamma' t} :
incl Gamma Gamma' -> iipc2 Gamma t -> iipc2 Gamma' t.
Proof. by move=> /incl_nth_error [?] /typing_ren_term' H [?] /H /iipc2I. Qed.
Lemma iipc2_generalization {Gamma Gamma' t} :
Forall (iipc2 Gamma') Gamma -> iipc2 Gamma t -> iipc2 Gamma' t.
Proof.
move=> H [P HP]. elim: P Gamma Gamma' t HP H.
- move=> > /typingE /nth_error_In. rewrite Forall_forall.
by move=> + H => /H.
- move=> ? IH1 ? IH2 > /typingE [?] [/IH1{}IH1 /IH2{}IH2].
move=> /copy [/IH1 [? ?] /IH2 [? ?]]. eexists. apply: typing_app; by eassumption.
- move=> s > IH Gamma Gamma' > /typingE [?] [->] /IH.
move=> /(_ (s :: Gamma')) + HG. apply: unnest.
{
constructor.
- exists (var 0). by apply: typing_var.
- move: HG. apply: Forall_impl. move=> ?.
apply: iipc2_weakening => ? /=. clear. by firstorder done.
}
move=> [? ?]. eexists. apply: typing_abs. by eassumption.
- move=> ? IH > /typingE [?] [->] /IH{}IH /IH [? ?].
eexists. apply: typing_ty_app. by eassumption.
- move=> > IH Gamma Gamma' > /typingE [?] [->] /IH.
move=> /(_ (map (ren_poly_type S) Gamma')) + HG. apply: unnest.
{
rewrite Forall_mapP. apply: Forall_impl HG.
move=> ? [Q]. eexists. apply: typing_ren_poly_type. by eassumption.
}
move=> [? ?]. eexists. apply: typing_ty_abs. by eassumption.
Qed.
Lemma iipc2_poly_arrE {Gamma s t}: iipc2 Gamma (poly_arr s t) -> iipc2 (s :: Gamma) t.
Proof.
move=> [?] /(@typing_ren_term' S) => /(_ (s :: Gamma) ltac:(done)).
move=> /typing_app => /(_ (var 0)) H. eexists. apply: H. by apply: typing_var.
Qed.
Corollary last_poly_var_typingI {t Gamma}:
(if last_poly_var t is Some x then In (poly_var x) Gamma else False) -> iipc2 Gamma t.
Proof.
move Hox: (last_poly_var t) => ox Hx. case: ox Hox Hx; last done.
move=> x. elim: t x Gamma.
- move=> /= > [->] /In_nth_error [? ?]. eexists. apply: typing_var. by eassumption.
- move=> ? _ ? IH > /= /IH H /H [P]. move=> /(@typing_ren_term' S) HP. eexists.
apply: typing_abs. by apply: HP.
- move=> s + x Gamma /= => /(_ (S x) (map (ren_poly_type S) Gamma)).
case: (last_poly_var s); last done. move=> [|y]; first done.
move=> + [?] ?. subst y. rewrite in_map_iff.
apply: unnest; first done. apply: unnest.
{ eexists. constructor; last by eassumption. done. }
move=> [?] /typing_ty_abs ?. eexists. by eassumption.
Qed.
Lemma iipc2_poly_arr_comp {Gamma s r t} : iipc2 Gamma (poly_arr s r) -> iipc2 Gamma (poly_arr r t) ->
iipc2 Gamma (poly_arr s t).
Proof.
move=> [?] /(@typing_ren_term' S) HP1 [?] /(@typing_ren_term' S) HP2.
eexists. apply: typing_abs. apply: typing_app; first by apply: HP2.
apply: typing_app; first by apply: HP1.
by apply: (typing_var (x := 0)).
Qed.
Lemma Forall2_typing_Forall_iipc2 {Gamma Ps ts} : Forall2 (typing Gamma) Ps ts -> Forall (iipc2 Gamma) ts.
Proof. elim; [by constructor | by move=> > /iipc2I; constructor]. Qed.
Lemma iipc2_ren_poly_type {Gamma t} ξ : iipc2 Gamma t ->
iipc2 (map (ren_poly_type ξ) Gamma) (ren_poly_type ξ t).
Proof. by move=> [?] /(typing_ren_poly_type ξ) /iipc2I. Qed.
Lemma iipc2_var_InI {Gamma t} : In t Gamma -> iipc2 Gamma t.
Proof. move=> /In_nth_error [?] /typing_var ?. eexists. by eassumption. Qed.
Lemma iipc2_poly_arrI {Gamma s t} : iipc2 (s :: Gamma) t -> iipc2 Gamma (poly_arr s t).
Proof. move=> [?] /typing_abs ?. eexists. by eassumption. Qed.
Lemma iipc2_poly_absI (x: nat) {Gamma t} :
Forall (fresh_in x) Gamma -> fresh_in (S x) t ->
iipc2 Gamma (ren_poly_type (scons x id) t) ->
iipc2 Gamma (poly_abs t).
Proof.
pose ξ := fun y => if PeanoNat.Nat.eq_dec x y then 0 else S y.
move=> HG Ht /(iipc2_ren_poly_type ξ).
have -> : map (ren_poly_type ξ) Gamma = (map (ren_poly_type S) Gamma).
{
elim: Gamma HG; first done.
move=> s Gamma H /Forall_consP [Hx /H{H} /= ->].
congr cons. apply: ext_ren_poly_type_allfv_poly_type.
apply: allfv_poly_type_impl Hx => ? ?. rewrite /ξ. by case: (PeanoNat.Nat.eq_dec _ _).
}
move=> [?] /typing_ty_abs /iipc2I. congr iipc2. congr poly_abs.
rewrite poly_type_norm /ξ /= ren_poly_type_allfv_id; last done.
apply: allfv_poly_type_impl Ht. clear.
move=> [|y]; case: (PeanoNat.Nat.eq_dec _ _); move=> /=; by lia.
Qed.
Lemma iipc2_poly_varI x {Gamma ts ss y} :
nth_error Gamma x = Some (many_poly_abs (length ts) (many_poly_arr ss (poly_var (length ts + y)))) ->
Forall (iipc2 Gamma) (map (subst_poly_type (fold_right scons poly_var (rev ts))) ss) ->
iipc2 Gamma (poly_var y).
Proof.
move=> /typing_var /typing_many_ty_appI => /(_ ts ltac:(done)).
rewrite subst_poly_type_many_poly_arr /subst_poly_type -rev_length fold_right_length_ts -/subst_poly_type.
move=> /iipc2I. move: (map _ ss) => {}ss. move: (poly_var y) => t.
elim: ss t; first done.
by move=> s ss IH t /= [?] /typing_app H /Forall_consP [[?] /H{H} /iipc2I /IH].
Qed.