如何解决不能用依赖归纳来重命名事物?
在我的证明中,这有效
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提出了一个问题。
版权声明:本文内容由互联网用户自发贡献,该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容, 请发送邮件至 dio@foxmail.com 举报,一经查实,本站将立刻删除。