在研究其他作者的Coq证明时,我经常遇到一种策略,让我们说"inv eq Heq"或"intro_b".我想了解这样的策略.
如何在我当前的项目中找到某个Coq策略或战术符号？
第二,有没有办法找到它的定义？
我使用了SearchAbout,Search,Locate和Print但找不到上述问题的答案.
我坚持要证明以下公认的引理。请帮助我如何继续。
函数sumoneseq以相反的顺序添加并返回“true”的重复列表。鉴于 [真;假; 真;真;假; true;true;true ]，它返回 [3;2;1]。该功能sumones在NAT表增加值。给定 [3;2;1]，它返回 6。
Notation "x :: l" := (cons x l) (at level 60, right associativity).
Notation "[ ]" := nil.
Notation "[ x ; .. ; y ]" := (cons x .. (cons y nil) ..).
Fixpoint sumoneseq (lb: list bool) (ln: list nat) : list nat :=
match lb, ln with
| nil, 0::tl'' => tl''
| nil, _ => ln
| true::tl', nil => …