1

在证明中，如果我对非最终论证进行归纳，我会得到普遍量化的归纳假设。我发现自己反复写这样的策略：

match goal with
        | [H : forall (esub : expr) (x : exprvar) (tsub t : T) (Gamma_ : Gamma),
             (internalType Gamma_ ?Theta_ ?d esub tsub) ->
                        (internalType (gamma_evar x tsub :: ?Gamma_) ?Theta_ ?d ?e t)->
                        internalType Gamma_ ?Theta_ ?d (esubst_expr esub x ?e) t,
             esub : expr,
             xvar : exprvar,
             tsub : T,
             t : T,
             Gamma_ : Gamma,
             H1 : internalType ?Gamma_ ?Theta ?d ?esub ?xsub,
             H2 : internalType (gamma_evar ?xvar ?tsub :: ?Gamma_) ?Theta ?d ?e ?t
             |- _]

也就是说，我寻找一个归纳假设，并寻找与它统一的论点来专门化它。然后我做specialize (Hypothesis Arg1 Arg2...)

这感觉就像样板，但我一直不得不为我使用它的每个引理编写不同的版本。有没有办法：

  1. 自动执行此操作？
  2. 自动执行此操作，仅针对归纳假设？（这样我们就不会陷入将每个参数应用于每个可能的函数的无限循环中）
4

0 回答 0