Search code examples
coqcoq-tactic

How to split equality of two lists?

I have the following goal and context:

  A : Type
  eqb : A -> A -> bool
  H : forall a1 a2 : A, eqb a1 a2 = true <-> a1 = a2
  x : A
  l1' : list A
  IHl1' : forall l2 : list A, eqb_list eqb l1' l2 = true <-> l1' = l2
  y : A
  l2' : list A
  IHl2' : eqb_list eqb (x :: l1') l2' = true <-> x :: l1' = l2'
  H0 : x = y
  H1 : l1' = l2'
  ============================
  x :: l1' = y :: l2'

Is there a tactic that allows me to apply H0 and H1 and complete this proof?

Thanks

Solution

  • Yes, it's called rewrite (see the refman). You can do

    rewrite H0, H1.

    or alternatively

    rewrite H0.
rewrite H1.

    EDIT: You can also use f_equal (doc), which should immediately discharge your goal.