proposition: Lemma minimize_weight_length {M: SMN} {a r b r' x y} : In (([], a :: r, x), ([], b :: r', y)) M -> weight_Instruction (([], a :: r, x), ([], b :: r', y)) <> 0 -> 1 <= length r -> confluent M -> length_preserving M -> { M' : SMN | weight M' < weight M /\ (confluent M' /\ length_preserving M' /\ ((exists NM, bounded M NM) <-> (exists NM', bounded M' NM'))) }.
proof: Proof. move=> HM Hop Hr confluent_M lp_M. pose z1 := fresh_State M. pose M1 := AddFreshLoop.M' M [] [a] [a] [] x z1. pose z2 := fresh_State M1. pose M2 := AddFreshLoop.M' M1 [] [b] [a] [] y z2. pose M3 := DerivableRule'.M' M2 r r' z1 z2. have : In ([], a :: r, x, ([], b :: r', y)) M3. { rewrite /M3 /M2 /M1 /AddFreshLoop.M' /DerivableRule'.M' ?in_app_iff. move: HM. clear. by firstorder done. } move /in_split_informative => /(_ ltac:(by do 5 (decide equality))) => [[[M31 M32] HM3]]. pose M4 := Reordering.M' M31 M32 [] (a::r) [] (b::r') x y. pose M5 := DerivableRule.M' (M31 ++ M32) [] (a::r) [] (b::r') x y. have ? : x <> z1 by (move: HM => /fresh_StateP; subst z1; lia). have ? : y <> z1 by (move: HM => /fresh_StateP; subst z1; lia). have [? ?] : x <> z2 /\ y <> z2. { have /fresh_StateP : In ([], a :: r, x, ([], b :: r', y)) M1. { rewrite /M1 /AddFreshLoop.M' ?in_app_iff. by right. } unfold z2; lia. } have ? : z1 <> z2. { have /fresh_StateP : In ([], [a], x, ([a], [], z1)) M1. { rewrite /M1 /AddFreshLoop.M' ?in_app_iff. left. by left. } unfold z2; lia. } have ? : reachable M2 ([a], r, z1) ([a], r', z2). { apply: AddFreshLoop.step_fresh_lI; first by (move=> /=; lia). apply: AddFreshLoop.step_fresh_rI; first by (move=> /=; lia). apply: rt_step. move: HM => /transition => /(_ [] []). by rewrite ?app_norm. } have ? : reachable (M31 ++ M32) ([], a::r, x) ([], b :: r', y). { apply: (rt_trans (y := ([a], r, z1))); [| apply: (rt_trans (y := ([a], r', z2)))]; apply: rt_step; (apply: (@DerivableRule.step_neq _ [] (a :: r) [] (b :: r') x y); first by [left | right]); apply /Reordering.simulation_step; rewrite /Reordering.M -HM3 /M3. - apply: (stepI [] r [] [a] [a] [] x z1); [done | done | clear; by firstorder done]. - apply: (stepI [a] [] [] r [] r' z1 z2); [by rewrite ?app_norm | by rewrite ?app_norm | clear; by firstorder done]. - apply: (stepI [] r' [a] [] [] [b] z2 y); [done | done | clear; by firstorder done]. } have ? : forall l'' r'' z , step M2 (l'', r'', z1) z -> l'' = [a] ++ skipn 1 l''. { move=> l'' r'' z. move HZ1: (l'', r'', z1) => Z1 HZ1z. case: HZ1z HZ1. move=> >. rewrite /M2 /AddFreshLoop.M' /M1 /AddFreshLoop.M' ?in_app_iff. case. { case; [by congruence | case; [by congruence | done]]. } case. - case; first by congruence. case; last done. move=> + [] *. move=> [] *. by subst. - move /fresh_StateP=> ? [] *. subst z1. by lia. } have ? : forall l'' r'' z , step M2 z (l'', r'', z1) -> l'' = [a] ++ skipn 1 l''. { move=> l'' r'' z. move HZ1: (l'', r'', z1) => Z1 HZ1z. case: HZ1z HZ1. move=> >. rewrite /M2 /AddFreshLoop.M' /M1 /AddFreshLoop.M' ?in_app_iff. case. { case; [by congruence | case; [by congruence | done]]. } case; [case|]. - move=> + [] * => [[]] *. by subst. - case; [by congruence | done]. - move /fresh_StateP=> ? [] *. subst z1. by lia. } exists (M31 ++ M32). constructor; [| constructor; [| constructor]]. - suff: weight M3 < weight M + (weight_Instruction ([], (a::r), x, ([], (b::r'), y))). { rewrite HM3 weight_split. move: (weight_Instruction _) (weight _). by lia. } move: Hop. rewrite /M3 /DerivableRule.M' /= /weight_Instruction. case: (basic ([], a :: r, x, ([], b :: r', y))); first by lia. move=> _. case: (basic ([], r, z1, ([], r', z2))). { rewrite /= ?app_length. by lia. } rewrite /= ?app_length /= ?app_length. by lia. - apply /DerivableRule.confluence; first by eassumption. apply /Reordering.confluence. rewrite /Reordering.M -HM3. apply /DerivableRule'.confluent_M'; [| by eassumption | done | done | done ]. apply: AddFreshLoop.confluent_M'; [ | done | by apply: fresh_StateP' | by move=> /=; lia ]. apply: AddFreshLoop.confluent_M'; [ done | done | by apply: fresh_StateP' | by move=> /=; lia ]. - apply /DerivableRule.length_preservation; [by eassumption | move=> /=; by lia | ]. apply /Reordering.length_preservation. rewrite /Reordering.M -HM3. apply /DerivableRule'.length_preserving_M'; [| by eassumption | done | done | done | done ]. apply: AddFreshLoop.length_preserving_M'; [ | done | by apply: fresh_StateP' | by move=> /=; lia ]. apply: AddFreshLoop.length_preserving_M'; [ done | done | by apply: fresh_StateP' | by move=> /=; lia ]. - rewrite (DerivableRule.boundedness (M31 ++ M32)); first by eassumption. rewrite -(Reordering.boundedness M31 M32). rewrite /Reordering.M -HM3. rewrite -(DerivableRule'.boundedness); [ by eassumption | done | done | done | done | ]. rewrite -(AddFreshLoop.boundedness); [ done | by apply: fresh_StateP' | by move=> /=; lia | ]. rewrite -(AddFreshLoop.boundedness); [ done | by apply: fresh_StateP' | by move=> /=; lia | done ]. Qed.
imports: Relation_Operators Operators_Properties List Lia PeanoNat Undecidability.StackMachines.SMN Undecidability.StackMachines.Util(List_facts SMN_facts) ssreflect ssrbool ssrfun