proposition: Lemma trace_filter_app A (f : A -> Prop) (t t' : trace A) (IMP: trace_length (trace_filter f t) <> NOinfinity -> trace_length t <> NOinfinity) : trace_filter f (trace_app t t') = trace_app (trace_filter f t) (trace_filter f t').
proof: Proof. destruct t; ins; desf; ins; desf. all: try solve [destruct IMP; ins]; clear IMP. all: repeat destruct (constructive_indefinite_description); ins; desf. all: try solve [exfalso; rewrite set_finite_prepend in *; ins]. by rewrite filterP_app in *. { unfold set_map in *. destruct (le_lt_dec (length l) (S x)). - rewrite map_trace_prepend_geq; ins. unfold trace_prepend in *. rewrite filterP_app. do 2 f_equal. eapply filterP_map_seq_eq; simpl; eauto. ins; forward apply (l0 (length l + i)); desf; try lia. by rewrite minus_plus. ins; eapply l1 in H; lia. - eapply map_trace_prepend_lt with (fl := fl) in l2; desf. rewrite l4, filterP_app, appA; clear l4. f_equal. symmetry; rewrite app_eq_prefix, app_eq_nil, ?filterP_eq_nil. remember (a :: l'') as l; clear a l'' Heql. split; ins. apply in_split in IN; desf. forward apply (l0 (length l' + length l2)); try lia. by autorewrite with trace_prepends. in_simp. forward apply (l0 (length l' + (length l + x2))); try lia. by autorewrite with trace_prepends. } { f_equal; extensionality y; ins. destruct (constructive_indefinite_description); ins; desf. erewrite <- length_map, <- filterP_map. destruct (le_lt_dec (length l) x) as [LE|LT]. { rewrite map_trace_prepend_geq; ins. autorewrite with trace_prepends. rewrite filterP_map, length_map. destruct (constructive_indefinite_description); ins; desf. unfold set_map, trace_prepend in *; desf; try lia. destruct (lt_eq_lt_dec (x - length l) x0) as [[LT|]|LT]; desf; apply seq_split0 in LT; rewrite LT in *; exfalso; revert a1; rewrite ?map_app, ?filterP_app, ?length_app; ins; desf; ins; lia. } eapply map_trace_prepend_lt with (fl := fl) in LT; desf. rewrite filterP_app, LT1; red in a. autorewrite with trace_prepends in *; ins; desf. } Qed.
imports: HahnBase HahnList HahnSets HahnRelationsBasic HahnOmega HahnWf Arith micromega.Lia IndefiniteDescription