proposition: Theorem pure_typable_intro_prenex M s n : is_simple s -> allfv_poly_type (gt n) s -> { N | forall Gamma, pure_typable (map tidy (many_poly_abs n s :: Gamma)) M <-> pure_typable (map tidy Gamma) N }.
proof: Proof. move=> Hs Hns. pose N0 := many_pure_term_abs n (trace_poly_type n s). pose N1 := pure_abs (K' (many_pure_app (pure_var 0) (repeat (pure_var 2) n)) (many_pure_app (pure_var 0) (repeat (pure_var 3) n))). pose N2 := pure_app (ren_pure_term (Nat.add 4) (pure_abs M)) (pure_app N1 N0). have [N2_1 HN2_1]:= pure_typing_intro_poly_abba N2. have [N2_2 HN2_2] := pure_typable_intro_poly_bot N2_1. have [N2_3 HN2_3] := pure_typable_intro_poly_var_0 N2_2. exists N2_3 => Gamma. constructor. - move=> [tM] HtM. apply /HN2_3 /HN2_2 /HN2_1 => {HN2_3 HN2_2 HN2_1}. eexists. apply: (pure_typing_pure_app_simpleI (s := tidy (many_poly_abs n s))). + move=> /=. apply: pure_typing_pure_abs_simpleI. move: HtM => /(pure_typing_ren_poly_type S) HtM. apply: pure_typing_ren_pure_term; first by eassumption. case. * move=> ? /= <-. rewrite -tidy_ren_poly_type. congr Some. congr tidy. rewrite ren_poly_type_allfv_id ?allfv_poly_type_many_poly_abs; last done. apply: allfv_poly_type_impl Hns => ? ?. rewrite iter_scons_lt; by [lia |]. * move=> ? ? /= <-. congr nth_error. rewrite ?map_map. apply: map_ext => ?. by rewrite tidy_ren_poly_type. + apply: (pure_typing_pure_app_simpleI (s := tidy (Nat.iter n (fun s' => poly_abs (poly_arr (poly_var 0) s')) s))). * rewrite -/(tidy (poly_arr _ _)). apply: pure_typing_tidyI. apply: pure_typing_pure_abs_simpleI. apply: pure_typing_K'I. ** apply: aux_pure_typing_gxs; [done | by apply: pure_typing_pure_var_simpleI]. ** apply: aux_pure_typable_gys; [done | by apply: pure_typing_pure_var_simpleI]. * apply: pure_typing_tidyI. rewrite /N0. have ->: trace_poly_type n = trace_poly_type (n+0) by congr trace_poly_type; lia. apply: aux_pure_typing_N0; [done | by apply: allfv_poly_type_impl Hns; lia | | done]. rewrite allfv_poly_type_many_poly_abs. apply: allfv_poly_type_impl Hns. move=> ? ?. rewrite iter_scons_lt; by [lia|]. - move /HN2_3 /HN2_2 /HN2_1 => {HN2_3 HN2_2 HN2_1}. rewrite /N2 /N1 /N0 /= => {N2_3 N2_2 N2_1}. move=> /pure_typableE [?] [?] []. move=> /pure_typingE' HM. move=> /pure_typingE [n3] [?] [?] [?] [+] [+] [H2C ?]. subst. move=> /pure_typingE'. move=> /pure_typing_K'E [HN1_1] HN1_2. move=> /pure_typing_many_pure_term_absE [nss] [?] [?] [?]. subst. move: HN1_2 => /pure_typable_many_pure_app_repeat_poly_var. evar (r : poly_type) => /(_ (n3 + 0) r). apply: unnest; first by subst r. apply: unnest; first done. move=> Hnss. set Gamma' := (Gamma' in pure_typing Gamma' _ _). have : exists ss Gamma'', length ss = length nss /\ Gamma' = ss ++ poly_abba :: Gamma'' /\ Forall (fun 's => exists n x, s = many_poly_abs n (poly_var (n + x))) ss. { rewrite /Gamma'. elim /rev_ind: (nss) Hnss; first by move=> ?; exists []; eexists. clear=> [[n s]] nss IH /Forall_app [/IH] {}IH /Forall_cons_iff [[n0] [x0] ->] _. rewrite fold_left_app app_length. move: IH => [ss] [Gamma''] [<-] /= [->] Hss. eexists (_ :: map (ren_poly_type (Nat.add n)) ss), (map (ren_poly_type (Nat.add n)) Gamma''). rewrite /= map_length map_app /= Forall_cons_iff Forall_map. constructor; first by lia. constructor; first done. constructor; first by do 2 eexists. apply: Forall_impl Hss => ? [?] [? ->]. rewrite ren_poly_type_many_poly_abs /= iter_up_ren. by do 2 eexists. } move=> [ss] [?] [H1ss] [-> {Gamma'}] H2ss. rewrite -H1ss. move=> /pure_typing_tidyI. rewrite map_app /=. have [ns [H1ns H2ns]] : exists ns, length ss = length ns /\ map tidy ss = map poly_var ns. { elim: (ss) H2ss; first by move=> _; exists []. clear=> s ss IH /Forall_cons_iff [] [?] [n] -> /IH [ns] /= [-> ->]. exists (n :: ns). constructor; first done. rewrite tidy_many_poly_abs_le /=; first by lia. congr cons. congr poly_var. by lia. } rewrite H1ns H2ns. move=> /(pure_typing_trace_poly_typeE (n := 0)). rewrite -H1ns H1ss tidy_tidy => /(_ ltac:(done) ltac:(done)). move: HN1_1 => /pure_typing_fold_right_many_pure_app /= => /(_ _ ltac:(done)). move=> [n6] [ξs] [n7] [?] [? H3C]. subst. move=> H2s. move: HM => /=. set s0 := (s0 in pure_typing (s0 :: _) _ _). set Gamma0 := (Gamma0 in pure_typing (s0 :: _ :: _ :: _ :: _ :: Gamma0) _ _). move=> /(pure_typing_ren_pure_term_allfv_pure_term (scons 0 (scons 0 (scons 0 (scons 0 (scons 0 S))))) (Delta := s0 :: Gamma0)). apply: unnest. { rewrite allfv_pure_term_ren_pure_term /=. apply: allfv_pure_term_TrueI. by case. } rewrite renRen_pure_term /= ren_pure_term_id'; first by case. subst Gamma0. have H4s : allfv_poly_type (fun=> False) (tidy (many_poly_abs (length nss) s)). { rewrite allfv_poly_type_tidy allfv_poly_type_many_poly_abs. apply: allfv_poly_type_impl Hns => ? ?. rewrite iter_scons_lt; by [|lia]. } have : pure_typing [tidy (many_poly_abs (length nss) s)] (pure_var 0) (tidy s0). { have H3s : [tidy (many_poly_abs (length nss) s)] = map tidy [tidy (many_poly_abs (length nss) s)] by rewrite /= tidy_tidy. rewrite /s0 {s0}. rewrite H3s. apply: pure_typing_tidy_many_poly_abs_closed; first done. rewrite H3s. apply: pure_typing_many_poly_abs_contains_tidy_closed; [done | by eassumption |]. rewrite H3s. apply: pure_typing_many_poly_abs_contains_tidy_closed; [done | by eassumption |]. rewrite tidy_ren_poly_type -H2s ?poly_type_norm /=. rewrite -[s in ren_poly_type _ s](tidy_is_simple Hs) -tidy_ren_poly_type -/(map tidy [_]). apply: pure_typing_tidyI. apply: (pure_typing_pure_var 0); first done. rewrite ren_poly_type_id ren_as_subst_poly_type. by apply: contains_many_poly_abs_closedI. } move=> /pure_typing_weaken_closed => /(_ []) H /pure_typing_tidyI /= /H{H} => /(_ ltac:(done)). move=> /(pure_typing_ren_poly_type (fun x => x - 1)) /= /pure_typableI. congr pure_typable. congr cons. + rewrite ren_poly_type_allfv_id; last done. by apply: allfv_poly_type_impl H4s. + rewrite ?map_map. apply: map_ext => ?. rewrite ?tidy_ren_poly_type tidy_tidy ?poly_type_norm /=. apply: ren_poly_type_id'. by lia. Qed.
imports: List Lia Relation_Definitions Relation_Operators Operators_Properties Undecidability.SystemF.SysF Undecidability.SystemF.Autosubst.syntax Undecidability.SystemF.Autosubst.unscoped Undecidability.SystemF.Util(Facts poly_type_facts pure_term_facts term_facts typing_facts iipc2_facts pure_typing_facts) ssreflect ssrbool ssrfun