proposition: Lemma netlist_find_sublist_app {j k} (g : netlist B j k) {i l} (f : netlist B i l) {pre post} : netlist_find_sublist g f = Some (pre, post) → match pre, post with | inright H1, inright H2 => f = rew <- [fun x => netlist B x _] H1 in rew [fun x => netlist B _ x] H2 in g | inleft pre, inright H2 => f = pre ++++ rew [fun x => netlist B _ x] H2 in g | inright H1, inleft post => f = rew <- [fun x => netlist B x _] H1 in g ++++ post | inleft pre, inleft post => f = pre ++++ g ++++ post end.
proof: Proof. intros. generalize dependent k. generalize dependent j. induction f; intros; simpl in H1. - destruct g. + destruct (eq_dec i i0); [|discriminate]; subst. destruct (eq_dec j0 j); [|discriminate]; subst. destruct (eq_dec b0 _); [|discriminate]; subst. inversion H1; now subst. + discriminate. - destruct g. + destruct (eq_dec i i0); subst. * destruct (eq_dec j0 j); subst. ** destruct (eq_dec b0 _); [|discriminate]; subst. inversion H1; now subst. ** destruct (netlist_find_sublist _ _) eqn:?; [|discriminate]. destruct p. destruct s; subst; now cleanup H1 post IHf Heqo. * destruct (netlist_find_sublist _ _) eqn:?; [|discriminate]. destruct p. destruct s; subst; now cleanup H1 post IHf Heqo. + destruct (eq_dec i i0); subst. { destruct (eq_dec j0 j); subst. { destruct (eq_dec b0 _). { subst. destruct (netlist_find_sublist g f) eqn:?. { destruct p. destruct s; subst. - simpl_eq. destruct (netlist_find_sublist (_ :::: g) f) eqn:?; [|discriminate]. destruct p. destruct s; subst; now cleanup H1 post IHf Heqo0. - cleanup H1 post IHf Heqo; auto; simpl_eq; now dependent elimination e. } destruct (netlist_find_sublist (_ :::: g) f) eqn:?; [|discriminate]. destruct p. destruct s; subst; now cleanup H1 post IHf Heqo0; auto. } destruct (netlist_find_sublist (_ :::: g) f) eqn:?; [|discriminate]. destruct p. destruct s; subst; now cleanup H1 post IHf Heqo; auto. } destruct (netlist_find_sublist (_ :::: g) f) eqn:?; [|discriminate]. destruct p. destruct s; subst; now cleanup H1 post IHf Heqo; auto. } destruct (netlist_find_sublist (_ :::: g) f) eqn:?; [|discriminate]. destruct p. destruct s; subst; now cleanup H1 post IHf Heqo; auto. Qed.
imports: Coq.Bool.Bool Coq.Lists.List Equations(Equations) Category.Lib