proposition: Lemma completeness_step (bound : nat) (N : term) (v w : list nat) : step rs v w -> (forall i, In (nth i v 0) symbols) -> neutral normal_form N -> length v = bound + 1 -> type_assignment (Γ_all bound (1 + bound)) N (symbol 1) -> Forall (fun i => type_assignment (Γ_all bound i) N (symbol (nth i w 0))) (seq 0 (bound + 1)) -> exists N', neutral normal_form N' /\ type_assignment (Γ_all bound (1 + bound)) N' (symbol 1) /\ Forall (fun i => type_assignment (Γ_all bound i) N' (symbol (nth i v 0))) (seq 0 (bound + 1)).
proof: Proof. case=> u1 u2 a0 b0 a1 b1. rewrite !app_length /= => + ??? H1N H2N. move=> /(@In_split rule) [rs1] [rs2] Hrs. have ? : length u1 < bound by lia. pose x := bound + (length Γ_init + length rs1). have Hx : forall i, nth_error (Γ_all bound i) x = Some (s_rule ((a0, b0), (a1, b1))). { move=> i. rewrite /x /Γ_all /Γ_step Hrs map_app nth_error_app2 map_length seq_length. { lia. } have -> /= : forall n, bound + n - bound = n by lia. by rewrite nth_error_app2 map_length ?Nat.sub_diag. } exists (app (app (var x) (var (length u1))) N). do ? split. - do ? constructor. by apply: neutral_normal_form. - apply: type_assignment_app; [apply: type_assignment_app| |]. + econstructor; [by rewrite Hx|]. apply: In_s_id_rulesI. apply /in_app_iff. do 2 right. by left. + econstructor; [rewrite nth_Γ_lr; [done|]|by left]. rewrite /s_pos. have /Nat.eqb_neq -> : S bound <> 0 + length u1 by lia. by have /Nat.eqb_neq -> : S bound <> S (0 + length u1) by lia. + done. + done. + done. - apply /Forall_forall => i /[dup] /in_seq [_ ?]. move: H2N => /Forall_forall /[apply]. have [Hi|[Hi|Hi]] : (i < length u1 \/ i >= length u1 + 2) \/ i = length u1 \/ i = S (length u1) by lia. + move=> H'N. apply: type_assignment_app; [apply: type_assignment_app| |]. * econstructor; [by rewrite Hx|]. by apply: In_s_id_rulesI. * econstructor; [rewrite nth_Γ_lr; [done|]| by left]. rewrite /s_pos. have /Nat.eqb_neq -> : i <> length u1 by lia. by have /Nat.eqb_neq -> : i <> S (length u1) by lia. * done. * move: H'N. congr type_assignment. congr symbol. case: Hi => ?. { by do 2 (rewrite (@app_nth1 nat); first done). } do 2 (rewrite (@app_nth2 nat); first lia). by have ->: i - length u1 = S (S (i - length u1 - 2)) by lia. * done. + rewrite Hi (@app_nth2 nat). { done. } rewrite (@app_nth2 nat) ?Nat.sub_diag. { done. } move=> /= H'N. apply: type_assignment_app; [apply: type_assignment_app| |]. * econstructor; [by rewrite Hx|]. by left. * econstructor; [rewrite nth_Γ_lr; [done|]| by left]. by rewrite /s_pos Nat.eqb_refl. * done. * done. * done. + rewrite Hi (@app_nth2 nat). { lia. } rewrite (@app_nth2 nat). { lia. } have -> : S (length u1) - length u1 = 1 by lia. move=> /= H'N. apply: type_assignment_app; [apply: type_assignment_app| |]. * econstructor; [by rewrite Hx|]. right. by left. * econstructor; [rewrite nth_Γ_lr; [done|]| by left]. rewrite /s_pos Nat.eqb_refl. by have /Nat.eqb_neq -> : S (length u1) <> length u1 by lia. * done. * done. * done. Qed.
imports: Undecidability.IntersectionTypes.CD Undecidability.IntersectionTypes.Util.CD_facts Undecidability.StringRewriting.SSTS Undecidability.LambdaCalculus.Util.term_facts Relations List PeanoNat Lia ssreflect ssrfun