proposition: Lemma construct_h10cs_solution {xs tSs tPs P}: normal_form P -> Forall encodes_sum tSs -> Forall encodes_prod tPs -> typing (Gamma0 ++ (map Ut (map (fun x => poly_var (x + zt)) xs)) ++ (map St tSs) ++ (map Pt tPs)) P (poly_var tt) -> H10C_SAT h10cs.
proof: Proof. Proof using h10cs. elim /(Nat.measure_induction _ term_size): P xs tSs tPs => P IH xs tSs tPs + HtSs HtPs. move=> /[dup] [HP] /typing_is_safe_environment H /H{H}. apply: unnest. { apply: Forall_appI; first by apply: is_safe_environment_Gamma0. apply: Forall_appI; first by apply: is_safe_environment_Ut. apply: Forall_appI; [by apply: is_safe_environment_St | by apply: is_safe_environment_Pt]. } move=> [ss] [?] [ts] [Qs] [?] [/nth_error_In]. subst P. case /in_app_iff. { case; [|case; [|case; [|case]]]; last done. - move: IH HP. case ts; first by case: ss. move=> s. case; last by case ss. move=> IH HQs [] /(congr1 parameters_poly_arr). rewrite ?parameters_many_poly_arr. move=> <- HQsss. move: (HQsss) => /Forall2_length /=. move HQs': (Qs) => Qs'. move: Qs' HQs' => [|]; first done. move=> Q1 [|]; first done. move=> Q1' [|]; first done. move=> Q1'' [|]; first done. move=> Q1''' [|]; first done. move=> Q2 [|]; last done. move=> ? _. subst Qs. move: HQs => /normal_form_many_app [_ +]. do 4 (move=> /Forall_inv_tail). move=> /Forall_inv HQ2. move: HQsss => /Forall2_cons_iff [/iipc2I HQ1] /Forall2_cons_iff [_] /Forall2_cons_iff [_] /Forall2_cons_iff [_] /Forall2_cons_iff [+ _]. have [n Hsn] : exists n, encodes_nat s n by apply: iipc2_Ut_unique; eassumption. rewrite [poly_arr _ _]lock [Gamma0]lock /=. move: HQ2 => /typing_normal_form_poly_absE H /H{H} => /(_ (1+n+zt)) => [[Q2']]. rewrite poly_type_norm. set f := (f in subst_poly_type f _). have Hf : forall x, f x = fold_right scons poly_var [poly_var (1 + n + zt); s] x. { rewrite /f /funcomp. case; first done. case; last done. by rewrite ?poly_type_norm -[RHS]ren_poly_type_id. } under ext_poly_type => ? do rewrite Hf. set σ := (fold_right _ _ _). rewrite -?lock [Gamma0]lock [Ut']lock [St']lock [Pt']lock /= -?lock [Gamma0]lock. rewrite subst_poly_type_Ut' ?subst_poly_type_St' ?subst_poly_type_Pt' /σ /=. move=> [+] [HQ2']. move=> /typing_normal_form_poly_arrE H /H{H} [Q2'2] [+] [?]. move=> /typing_normal_form_poly_arrE H /H{H} [Q2'3] [+] [?]. move=> /typing_normal_form_poly_arrE H /H{H} [Q2'4] [+] [?]. move=> /typing_normal_form_poly_arrE H /H{H} [Q2'5] [HQ2'5] [?]. move=> /(typing_weakening (Gamma' := locked Gamma0 ++ (map Ut (map (fun x => poly_var (x + zt)) (1+n :: xs))) ++ (map St ((s, poly_var (1+zt), poly_var (1+n+zt)) :: (poly_var (1+n+zt), poly_var zt, poly_var (1+n+zt)) :: tSs)) ++ (map Pt ((poly_var (1+n+zt), poly_var zt, poly_var zt) :: tPs)))). apply: unnest. { move=> ?. rewrite /= ?app_comm_cons ?in_app_iff /=. clear. by tauto. } unlock. move=> [?] /IH. apply. + rewrite term_size_ren_term /=. rewrite [_ Q1]term_size_pos [_ Q1']term_size_pos [_ Q1'']term_size_pos [_ Q1''']term_size_pos. by lia. + by apply: normal_form_ren_term. + constructor; [| constructor]; last done. * exists n, 1, (1+n). constructor; first done. do 2 (constructor; first by apply: encodes_natI). by lia. * exists (1+n), 0, (1+n). do 3 (constructor; first by apply: encodes_natI). by lia. + constructor; last done. exists (1+n), 0, 0. do 3 (constructor; first by apply: encodes_natI). by lia. - rewrite /t_s. rewrite [Gamma0]lock. move=> /safe_poly_type_eqE [+ [<- _]]. move: ts HP IH. do 5 (move=> [|?]; first done). case; last done. set σ := fold_right scons poly_var _. move=> /normal_form_many_app [_ HQs] IH _. rewrite [Ut']lock [St']lock /= -[locked Ut']lock -[locked St']lock ?subst_poly_type_Ut' ?subst_poly_type_St' /= -lock. move=> /[dup] [/Forall2_typing_Forall_iipc2 /Forall_cons_iff [_]]. move=> /Forall_cons_iff [/iipc2_Ut_unique [n5 ?]]. move=> /Forall_cons_iff [/iipc2_Ut_unique [n4 ?]]. move=> /Forall_cons_iff [/iipc2_Ut_unique [n3 ?]]. move=> /Forall_cons_iff [/iipc2_Ut_unique [n2 ?]]. move=> /Forall_cons_iff [/iipc2_Ut_unique [n1 ?]]. have ? := encodes_natI 1. move=> /Forall_cons_iff [/iipc2_St_soundness {}H]. have ?: n5 + n4 = n3 by apply: H; eassumption. move=> /Forall_cons_iff [/iipc2_St_soundness {}H]. have ?: n4 + 1 = n2 by apply: H; eassumption. move=> /Forall_cons_iff [/iipc2_St_soundness {}H]. have ?: n3 + 1 = n1 by apply: H; eassumption. move=> _ {H} /[dup] [/Forall2_length]. move: Qs HQs IH. move=> [|Q9]; first done. move=> Qs /Forall_inv HQ9 IH _ /Forall2_cons_iff [+ _]. move: HQ9 => /typing_normal_form_poly_arrE H /H{H} [Q] [H1Q] [?]. set tS := (tS in St tS). move=> /(typing_weakening (Gamma' := Gamma0 ++ (map Ut (map (fun x => poly_var (x + zt)) xs)) ++ (map St (tS :: tSs)) ++ (map Pt tPs))). apply: unnest. { move: (Gamma0) => ? ?. rewrite /= ?app_comm_cons ?in_app_iff /=. clear. by tauto. } move=> [?] /IH. apply. + rewrite term_size_ren_term /=. set P := (P in many_app P _). have := term_size_many_app_le P Qs. rewrite /P /=. by lia. + by apply: normal_form_ren_term. + constructor; last done. exists n5, n2, n1. do 3 (constructor; first done). by lia. + done. - rewrite /t_p. rewrite [Gamma0]lock. move=> /safe_poly_type_eqE [+ [<- _]]. move: ts HP IH. do 5 (move=> [|?]; first done). case; last done. set σ := fold_right scons poly_var _. move=> /normal_form_many_app [_ HQs] IH _. rewrite [Ut']lock [St']lock [Pt']lock /= -[locked Ut']lock -[locked St']lock -[locked Pt']lock ?subst_poly_type_Ut' ?subst_poly_type_St' ?subst_poly_type_Pt' /= -lock. move=> /[dup] [/Forall2_typing_Forall_iipc2 /Forall_cons_iff [_]]. move=> /Forall_cons_iff [/iipc2_Ut_unique [n5 ?]]. move=> /Forall_cons_iff [/iipc2_Ut_unique [n4 ?]]. move=> /Forall_cons_iff [/iipc2_Ut_unique [n3 ?]]. move=> /Forall_cons_iff [/iipc2_Ut_unique [n2 ?]]. move=> /Forall_cons_iff [/iipc2_Ut_unique [n1 ?]]. have ? := encodes_natI 1. move=> /Forall_cons_iff [/iipc2_Pt_soundness {}H]. have ?: n5 * n4 = n3 by apply: H; eassumption. move=> /Forall_cons_iff [/iipc2_St_soundness {}H]. have ?: n4 + 1 = n2 by apply: H; eassumption. move=> /Forall_cons_iff [/iipc2_St_soundness {}H]. have ?: n3 + n5 = n1 by apply: H; eassumption. move=> _ {H} /[dup] [/Forall2_length]. move: Qs HQs IH. move=> [|Q9]; first done. move=> Qs /Forall_inv HQ9 IH _ /Forall2_cons_iff [+ _]. move: HQ9 => /typing_normal_form_poly_arrE H /H{H} [Q] [H1Q] [?]. set tP := (tP in Pt tP). move=> /(typing_weakening (Gamma' := Gamma0 ++ (map Ut (map (fun x => poly_var (x + zt)) xs)) ++ (map St tSs) ++ (map Pt (tP :: tPs)))). apply: unnest. { move: (Gamma0) => ? ?. rewrite /= ?in_app_iff /=. clear. by tauto. } move=> [?] /IH. apply. + rewrite term_size_ren_term /=. set P := (P in many_app P _). have := term_size_many_app_le P Qs. rewrite /P /=. by lia. + by apply: normal_form_ren_term. + done. + constructor; last done. exists n5, n2, n1. do 3 (constructor; first done). by lia. - move=> /safe_poly_type_eqE [Hts] [<-] _ /Forall2_typing_Forall_iipc2. rewrite map_app ?[map (subst_poly_type _) (map _ _)]map_map. under [map _ (seq _ _)]map_ext => x do rewrite Hts -rev_length subst_poly_type_Ut'. under [map _ h10cs]map_ext => c do (rewrite subst_poly_type_h10c_poly_type; first done). set σ := (fold_right _ _ (rev ts)). move=> /Forall_app [Hδ Hh10cs]. have /list_choice [φ Hφ] : Forall (fun i => exists n, encodes_nat (σ i) n) (seq 0 δ). { move: Hδ => /Forall_map. apply: Forall_impl => ?. by apply: iipc2_Ut_unique. } exists φ => c. move: Hh10cs δP Hφ => /Forall_map /Forall_forall H1 /Forall_forall H2 /Forall_forall Hφ. move=> /[dup] [/H1{H1} + /H2{H2}]. case: c. + move=> x /iipc2_St_soundness + ? /=. move=> /(_ (φ x) 0 1). have -> : φ x + 0 = φ x by lia. apply; [done | | by apply: encodes_natI | by apply: encodes_natI]. apply /Hφ /in_seq. by lia. + move=> x y z /iipc2_St_soundness + ? /=. apply; first done. all: apply /Hφ /in_seq; by lia. + move=> x y z /iipc2_Pt_soundness + ? /=. apply; first done. all: apply /Hφ /in_seq; by lia. } case /in_app_iff; first by move=> /in_map_iff [?] [/last_poly_var_safe_poly_type]. case /in_app_iff; first by move=> /in_map_iff [[[? ?] ?]] [/last_poly_var_safe_poly_type]. by move=> /in_map_iff [[[? ?] ?]] [/last_poly_var_safe_poly_type]. Qed.
imports: PeanoNat List Lia Undecidability.SystemF.SysF Undecidability.SystemF.Autosubst.syntax Undecidability.SystemF.Util(Facts poly_type_facts term_facts typing_facts iipc2_facts sn_facts) Undecidability.DiophantineConstraints.H10C ssreflect ssrbool ssrfun