proposition: Lemma soundness_step (bound : nat) (N : term) (v : list nat) : neutral normal_form N -> length v = bound + 1 -> Forall (fun i => type_assignment (Γ_all bound i) N (symbol (nth i v 0))) (seq 0 (bound + 1)) -> multi_step rs v (repeat 1 (bound + 1)).
proof: Proof. elim /(Nat.measure_induction _ term_size): N v. move=> N IH v H0N Hv /[dup] H'v. rewrite seq_app /= => /Forall_app [_] /Forall_cons_iff [+ _]. case: H0N IH H'v. { move=> ?? H /type_assignmentE [>] /In_Γ_allE /[apply] - [] // ? Hx. rewrite (Forall_nth_const v); rewrite Hv; last by apply: rt_refl. apply: Forall_impl H => ? /type_assignmentE [>]. rewrite Hx=> - [<- <-]. by case; case. } move=> ? N1 []. { by move=> ???? /type_assignmentE [>] /type_assignmentE [>] /In_Γ_allE /[apply] - []. } move=> ? N2 /two_params_rule H HN2 HN1 IH IH'. move=> /type_assignmentE [>] /type_assignmentE [>] /[dup] H' /H{H}. move=> [?] [?] [? _]. subst. move: (H') HN2 => /s_rule_spec /[apply] /[apply]. move=> [[[[a0 b0][a1 b1]]]] [Hr] Hx [y] [?] [H1y H2y] H'N2 H1N1 H2N1. subst. have Ha0 : nth_error v y = Some a0. { have : In y (seq 0 (bound + 1)) by apply /in_seq; lia. move: IH' => /Forall_forall /[apply]. move=> /type_assignmentE [>] /type_assignmentE [>] /type_assignmentE [>]. rewrite Hx=> - [<- <-]. move=> H'' /type_assignmentE [>]. rewrite H2y /s_pos Nat.eqb_refl => - [<- <-]. case; last done. move=> ?. subst. move: H'' => /In_s_rule_spec [] //. move=> [] *. subst. apply: nth_error_nth'. lia. } have Hb0 : nth_error v (S y) = Some b0. { have : In (S y) (seq 0 (bound + 1)) by apply /in_seq; lia. move: IH' => /Forall_forall /[apply]. move=> /type_assignmentE [>] /type_assignmentE [>] /type_assignmentE [>]. rewrite Hx=> - [<- <-]. move=> H'' /type_assignmentE [>]. rewrite H2y /s_pos Nat.eqb_refl. have /Nat.eqb_neq -> : S y <> y by lia. move=> [<- <-]. case; last done. move=> ?. subst. move: H'' => /In_s_rule_spec [] //. move=> [] *. subst. apply: nth_error_nth'. lia. } move: Hr Ha0 Hb0 => /step_spec /[apply] /[apply] ?. apply: rt_trans. { apply: rt_step. eassumption. } apply: (IH N1). - move=> /=. lia. - move: H' H1N1 => /type_assignmentE [>] /In_Γ_allE /[apply]. case=> // > [?????] _ _ => [| |_]; subst. all: move=> /nf_hf_atom; by apply. - by rewrite map_length seq_length. - apply /Forall_forall => i /[dup] /in_seq [_ ?]. move: IH' => /Forall_forall /[apply]. move=> /type_assignmentE [>] /type_assignmentE [>] /type_assignmentE [>]. rewrite Hx=> - [<- <-]. move=> H'x /type_assignmentE [>]. rewrite H2y /s_pos. case E1iy: (Nat.eqb i y). { move=> [<- <-]. case; last done. move=> ? _. subst. move: H'x => /In_s_rule_spec [] //. move=> [? -> ??] + _. congr type_assignment. congr symbol. rewrite (map_nth' 0). { by rewrite seq_length Hv. } rewrite seq_nth /= ?E1iy; lia. } case E2iy: (Nat.eqb i (S y)). { move=> [<- <-]. case; last done. move=> ? _. subst. move: H'x => /In_s_rule_spec [] //. move=> [? -> ??] + _. congr type_assignment. congr symbol. rewrite (map_nth' 0). { by rewrite seq_length Hv. } rewrite seq_nth /= ?E1iy ?E2iy; lia. } move=> [<- <-]. case; last done. move=> ? _. subst. move: H'x => /In_s_rule_spec [] //. move=> e [? -> ??] ? + _. congr type_assignment. congr symbol. rewrite (map_nth' 0). { by rewrite seq_length Hv. } rewrite seq_nth /= ?E1iy ?E2iy; lia. Qed.
imports: Undecidability.IntersectionTypes.CD Undecidability.IntersectionTypes.Util.CD_facts Undecidability.StringRewriting.SSTS Undecidability.LambdaCalculus.Util.term_facts Relations List PeanoNat Lia ssreflect ssrfun