1
$\begingroup$

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.

$\endgroup$

1 Answer 1

2
$\begingroup$

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

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

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.