Coq просто подразумевает доказательство

Question

Я пытаюсь доказать следующую тривиальную теорему об отмене натуральных чисел:

forall i, j, k in nat . ((i+j) = (i+k)) -> (j = k)

Вот что я написал в Coq:

Theorem cancel : forall (i j k : nat),
  ((add i j) = (add i k)) -> (j = k).
Proof.
intros i j k.
induction i.
simpl.

После чего Coq пытается доказать базис индукции, которая тривиальна:

j = k -> j = k

Почти все учебники Coq начинаются с доказательства A -> A, но когда я пытаюсь использовать такие доказательства, я застреваю. Например, я использую:

Theorem my_first_proof : (forall A : Prop, A -> A).
Proof.
  intros A.
  intros proof_of_A.
  exact proof_of_A.
Qed.

А потом, когда я пытаюсь:

rewrite -> my_first_proof

Я получаю следующую ошибку:

Error: Cannot find a relation to rewrite.

Любая помощь очень ценится, спасибо!

Answer 1

Правильная тактика в этом случае - apply.

apply my_first_proof.

rewrite используется для замены одной подтерии цели другой, обычно с леммой, показывающей, что эти подтермы в некотором смысле равны или эквивалентны. my_first_proof не является доказательством равенства.