不能用依赖归纳来重命名事物？

问题描述

在我的证明中，这有效

induction H1 as [ | | | | | | | | | ].

但是，当我换成

dependent induction H1 as [ | | | | | | | | | ].

我收到“错误： 语法错误：在[tactic：tactic]之后出现[tactic：ltac_use_default]（在[vernac：tactic_command]中）。 “

在进行依赖归纳时，您可以认真地不选择变量名吗？那太疯狂了；我真的希望我只是因为某种原因而语法错误。

谢谢。

解决方法

在阅读Equality.v的代码之后，这是尝试为支持as子句的从属归纳定义一种表示法。

From Coq Require Import Program.

Ltac elim_ind_as p pat := elim_tac ltac:(fun p el => induction p as pat using el) p.
Ltac do_ind_as p pat := introduce p ; (induction p as pat || elim_ind_as p pat).

Tactic Notation "dependent" "induction" ident(H) "as" simple_intropattern(pat) :=
  do_depind ltac:(fun hyp => do_ind_as hyp pat) H.


(*Example:*)
From Coq Require Vector.

Definition head : forall {A} (n:nat),Vector.t A (S n) -> A.
Proof.
  intros A n v.
  (* induction v. Would not discard the case t A 0 *)
  dependent induction v as [|a z v IH]. (* For some reason the `z` is renamed to `n`... *)
  exact a.
Defined.

请注意，它有一些警告：此表示法使用simple_intropattern，而标准归纳策略使用的or_and_intropattern_loc似乎无法从Ltac访问。 我在#12840提出了一个问题。