is_in_order_merge

is_in_order_merge.v

Inductive in_order_merge {X : Type} : (list X) -> (list X) -> (list X) -> Prop :=
  | iom_nil : forall (xs : list X),
                in_order_merge [] xs xs
  | iom_seq_l : forall (x : X) (xs ys zs : list X),
                  in_order_merge xs ys zs -> in_order_merge (x::xs) ys (x::zs)
  | iom_seq_r : forall (y : X) (xs ys zs : list X),
                  in_order_merge xs ys zs -> in_order_merge xs (y::ys) (y::zs).

Theorem iom_seq_l_inverse  :
  forall {X : Type} (x : X) (xs ys zs : list X),
    in_order_merge (x :: xs) ys (x::zs) ->
    in_order_merge xs ys zs.
Proof.
  intros.
  inversion H.
  apply H3.
(* 1 subgoals, subgoal 1 (ID 2079) *)
  
(*   X : Type *)
(*   x : X *)
(*   xs : list X *)
(*   ys : list X *)
(*   zs : list X *)
(*   H : in_order_merge (x :: xs) ys (x :: zs) *)
(*   y : X *)
(*   xs0 : list X *)
(*   ys0 : list X *)
(*   zs0 : list X *)
(*   H3 : in_order_merge (x :: xs) ys0 zs *)
(*   H1 : xs0 = x :: xs *)
(*   H2 : y :: ys0 = ys *)
(*   H0 : y = x *)
(*   H4 : zs0 = zs *)
(*   ============================ *)
(*    in_order_merge xs (x :: ys0) zs *)
Abort.