Тактика: застрял в eqb_trans

Question

Пытаясь решить eqb_trans, я застрял:

Theorem eqb_trans : forall n m p,
  n =? m = true ->
  m =? p = true ->
  n =? p = true.

Очевидно, что мы должны использовать eqb_true для его решения:

Theorem eqb_true : forall n m,
    n =? m = true -> n = m.
--------------------------------------------
Proof.
  intros n m p H1 H2. apply eqb_true in H1.
  apply eqb_true with (n:=m)(m:=p) in H2.

На данный момент мы имеем:

n, m, p : nat
H1 : n = m
H2 : m = p
============================
(n =? p) = true

Теперь я хотел использовать eqb_true для достижения цели:

apply eqb_true with (m:=p).

Но здесь мы получаем ошибку:

Unable to unify "?M1056 = p" with "(n =? p) = true".

Почему это не работает? Как исправить?

Answer 1

Когда вы применяете лемму к цели, это вывод леммы, который должен объединяться с целью, а не с ее предпосылкой. Заключение этой леммы имеет вид _ = _в то время как ваша цель (_ =? _) = true, Эти два не могут быть объединены, что приводит к ошибке, которую вы видите.

Чтобы доказать eqb_transвам нужно обратное eqb_trueа именно

forall n m, n = m -> (n =? m) = true,

что после некоторого упрощения эквивалентно

forall n, (n =? n) = true.

Answer 2

Theorem eqb_trans : forall n m p,
    n =? m = true ->
    m =? p = true ->
    n =? p = true.
Proof.
  intros n m p.
  repeat rewrite  Nat.eqb_eq.
  intros.
  rewrite H.
  exact H0.
Qed.

- Проверьте Nat.eqb_eq.

Nat.eqb_eq                                                                                          
 : forall n m : nat, (n =? m) = true <-> n = m