Блог

У меня есть следующая цель и контекст:

   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'
 

Есть ли тактика, которая позволяет мне применить H0 H1 и завершить это доказательство?

Спасибо

Да, это называется rewrite (см. рефман). Вы можете сделать

 rewrite H0, H1.
 

или альтернативно

 rewrite H0.
rewrite H1.
 

РЕДАКТИРОВАТЬ: Вы также можете использовать f_equal (doc), который должен немедленно выполнить вашу цель.