Coq Induction on Hypothesis destroys the Hypothesis

Question

I'm trying to prove something in coq
I have and Inductive prop type named in_order_merge which is a relation between three lists that shows third one is in_order merge of first two, here is the definition.

Inductive in_order_merge {X : Type} : list X -> list X -> list X -> Prop :=
  | iom_nil : in_order_merge [ ] [ ] [ ]
  | iom_merge_l x l1 l2 l (H: in_order_merge l1 l2 l) :
  in_order_merge (x :: l1) l2 (x :: l)
  | iom_merge_r x l1 l2 l (H: in_order_merge l1 l2 l) :
  in_order_merge l1 (x :: l2) (x :: l).

I want to prove that if one of the lists is empty then this preposition means the non-empty one equals the third list. clearly induction on hypothesis (constructors) is the way to go but my problem comes when i get to second constructor and the fact that one of the lists is empty is completely demolished.
here is the lemma and it's proof:

Lemma iom_l_nil: forall X : Type, forall l2 l : list X, in_order_merge [ ] l2 l -> l2 = l.
Proof. intros. induction H. 
  - reflexivity.
  - admit.
  - rewrite IHin_order_merge. reflexivity.
Admitted. 

and this is my proof-view on second branch:

X: Type
x: X
l1, l2, l: list X
H: in_order_merge l1 l2 l
IHin_order_merge: l2 = l

---

1/1
l2 = x :: l

can anyone help me with what i can do to avoid this issue.

Answer 1

The induction tactic tends to forget about the values of concrete arguments (e.g., nil on in_order_merge.) One possible fix is to use remember to convert the nil argument to a variable:

Lemma iom_l_nil {X} (xs ys : list X) : in_order_merge nil xs ys -> xs = ys.
  intros H.
  remember nil as l.
  (* now, H as type in_order_merge l xs ys; this is good for induction *)
  induction H.
  - auto. (* base case *)
  - discriminate Heql. (* left case:  l <> nil *)
  - rewrite IHin_order_merge; auto. (* right case *)  
Qed.

Alternatively, you can structure the proof as inductive on the second argument itself, rather than on the proof of in_order_merge:

Lemma iom_l_nil {X} (xs ys : list X) : in_order_merge nil xs ys -> xs = ys.
  revert ys. (* generalize the induction hypothesis over ys *)
  induction xs; intros ys Hys. (* Hys is the proof of in_order_merge *)
  - inversion Hys; subst; auto. (* case xs = nil *)
  - inversion Hys; subst; rewrite (IHxs _ H3); auto. (* case xs not nil *)
Qed.

The inversion tactic is very useful here, since the branch of in_order_merge is uniquely determined by whether xs is nil or a cons (since the first argument is nil).