# Coq Induction on Hypothesis destroys the Hypothesis

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.
- rewrite IHin_order_merge. reflexivity.


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.

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).

• Instead of reverting and reintroducing ys, Coq provides the equivalent but slighthly nicer syntax induction xs in ys |- *. Mar 7 at 16:04