1

I'm very new to Coq. Suppose under some hypothesis I want to prove l1 = l2, both of which are lists. I wonder what is a general strategy if I want to prove it inductively.

I don't know of any way to do induction on l1 and l2 at the same time. If I do induction first on l1, then I'll end up having to prove l1 = l2 under hypothesis t1 = l2, where t1 is tail of l1, which is obviously false.

1 Answer 1

3

Usually it depends on what kind of hypothesis you have. However, as a general principle, if you want to synchronise two lists when doing induction on one, you have to generalise over the other.

induction l in l' |- *.

or

revert l'.
induction l.

It might also be that you have some hypothesis on both l and l' on which you can do induction instead. For instance, the Forall2 predicate synchronises the two lists:

Inductive Forall2 (A B : Type) (R : A -> B -> Prop) : list A -> list B -> Prop :=
| Forall2_nil : Forall2 R [] []
| Forall2_cons : forall (x : A) (y : B) (l : list A) (l' : list B), R x y -> Forall2 R l l' -> Forall2 R (x :: l) (y :: l')

If you do induction on this, it will destruct both lists at the same time.

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.