proposition: Lemma soundness_expand (bound : nat) (N : term) : neutral normal_form N -> Forall (fun Γi => type_assignment Γi N star) (map (Γ_all bound) (seq 1 bound)) -> type_assignment (Γ_all bound 0) N hash -> type_assignment (Γ_all bound (1+bound)) N dollar -> exists bound' N', neutral normal_form N' /\ Forall (fun Γi => type_assignment Γi N' (symbol 0)) (map (Γ_all bound') (seq 0 (1+bound'))).
proof: Proof. elim /(Nat.measure_induction _ term_size): N bound. move=> ? + bound Hx. case: Hx. { move=> ? IH ? /type_assignmentE [>] /In_Γ_allE /[apply]. by case. } move=> M N []; first last. { move=> > /two_params_rule H ???? /type_assignmentE [>] /type_assignmentE [>]. by move=> /H [?] [?] []. } move=> ? H0N IH IH' /type_assignmentE [>] /type_assignmentE [>]. move=> /In_Γ_allE /[apply]. case=> //. - move=> [-> ->] Hx H1N _. move: H0N IH IH' H1N => /normal_form_neutral []. { move=> []. - move=> ??? /type_assignmentE [>] /In_Γ_allE /[apply]. by case. - by move=> > /two_params_rule H ??? /type_assignmentE [>] /H [?] [?] []. } move=> [] N' [->] H0N' IH IH' /type_assignmentE H1N'. move=> /type_assignmentE [>] /type_assignmentE [>]. rewrite Hx=> - [<- <-]. case; [done|case;[done|case;[|done]]]. move=> [<- <-]/type_assignmentE H2N' /Forall_cons_iff [/type_assignmentE H3N' _]. apply: (IH N' _ (S bound)). + move=> /=. lia. + by apply: nf_hf_atom; eassumption. + move=> /=. constructor. { move: H1N'. by rewrite /Γ_all /= -seq_shift map_map. } move: IH'. rewrite -!seq_shift !map_map. move=> /Forall_map IH'. apply /Forall_map. apply: Forall_impl IH'. move=> ? /type_assignmentE [>] /type_assignmentE [>]. rewrite Hx=> - [<- <-]. case; [|case;[done|by case]]. move=> [<- <-] /type_assignmentE + _. by rewrite /Γ_all /= -seq_shift map_map. + move: H2N'. congr type_assignment. rewrite /Γ_all /=. congr cons. congr List.app. rewrite -seq_shift map_map. apply: map_ext_in => j /in_seq ?. rewrite /s_pos. have /Nat.eqb_neq -> : S bound <> j by lia. by have /Nat.eqb_neq -> : S bound <> S j by lia. + move: H3N'. by rewrite /Γ_all /= -seq_shift map_map. - move=> [-> ->] Hx ? _ /type_assignmentE [>] /type_assignmentE [>]. rewrite Hx=> - [<- <-]. case; [done|case;[done|case;[|done]]]. move=> [<- <-] ? _. exists bound, N. split. { by apply: nf_hf_atom; eassumption. } move=> /=. constructor; [done|]. apply /Forall_forall => ? /[dup] /in_map_iff [?] [<-] ?. move: IH' => /Forall_forall /[apply]. move=> /type_assignmentE [>] /type_assignmentE [>]. rewrite Hx=> - [<- <-]. case; [|case;[done|by case]]. by move=> [<- <-]. Qed.
imports: Undecidability.IntersectionTypes.CD Undecidability.IntersectionTypes.Util.CD_facts Undecidability.StringRewriting.SSTS Undecidability.LambdaCalculus.Util.term_facts Relations List PeanoNat Lia ssreflect ssrfun