Тактика, чтобы доказать логическое значение

Question

Есть ли тактика, похожая на intros чтобы доказать логическое значение, такое как

f : nat -> bool
g : nat -> bool
Lemma f_implies_g : forall n : nat, eq_true(implb (f n) (g n)).

Эта тактика потянет eq_true(f n) в контекст и требуют доказать eq_true(g n),

Answer 1

Позвольте мне предложить использовать SSReflect в этом случае. Потому что там уже есть машина, которая вам нужна. Не использует eq_true встраивать bool в Prop, скорее is_true, который является альтернативным способом сделать это.

From Coq Require Import ssreflect ssrbool.
Variables f g : nat -> bool.
Lemma f_implies_g n : (f n) ==> (g n).
Proof.
apply/implyP => Hfn.
Abort.

Фрагмент выше делает то, что вы хотите, неявно принуждая f n а также g n в Prop, Выполнив фрагмент, вы видите это

  n : nat
  Hfn : f n
  ============================
  g n

но Set Printing Coercions. показывает, что это действительно

  n : nat
  Hfn : is_true (f n)
  ============================
  is_true (g n)

что у вас есть.