有没有可能表达一个定理,说明应用了哪些构造函数?

您不能直接表示使用了哪个构造函数,但您可以从构造函数的类型反向工作,以确定您知道是否使用了该构造函数。这正是反转策略所做的。你需要做的是手动陈述你所知道的 e1 和 e2 既然你有 eval (add ..) .. . 例如:

Theorem appplied_constructor: forall e1 e2, (exists e, eval (add e1 e2) e) ->
                                      (e1 = lit 0) \/
                                      (~e1 = lit 0 /\
                                        exists n1 n2, eval e1 n1 /\
                                                eval e2 n2).
Proof.
  intros.
  destruct H as [e ?].
  inversion H; subst; eauto 10.
Qed.

你用 exists e ,所以我遵循了这个模式,没有提到 e 在结论中。然而,不是假设 exists e, ... ,你可以说 forall e 然后再回头看看 e :

Theorem appplied_constructor': forall e1 e2 e, eval (add e1 e2) e ->
                                      (eval e2 e /\ e1 = lit 0) \/
                                      (~e1 = lit 0 /\
                                        exists n1 n2, eval e1 n1 /\
                                                 eval e2 n2 /\
                                                 n1 + n2 = e).
Proof.
  intros.
  inversion H; subst; eauto 10.
Qed.