CODEWITHSUNDEEP
coqcoq-tactic
Felipe Balbi
Felipe Balbi

Reputation: 157

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

Upvotes: 0

Views: 94

Answers (1)

Ana Borges
Ana Borges

Reputation: 1376

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.

Upvotes: 2

Related Questions