Coq的不产生归纳假设

我得到的溶液与以下定理，如下所示：Coq的不产生归纳假设

Require Import Coq.Lists.List. 
Import ListNotations. 

Inductive suffix {X : Type} : list X -> list X -> Prop := 
    | suffix_end : forall xs, 
      suffix xs xs 
    | suffix_step : forall x xs ys, 
      suffix xs ys -> 
      suffix (x :: xs) ys. 

Theorem suffix_app (X: Type) (xs ys: list X) : 
    suffix xs ys -> exists ws, xs = ws ++ ys. 
Proof. 
    induction 1 as [|x xsp ysp hs [zs zeq]]. 
    - exists []. reflexivity. 
    - now exists (x :: zs); rewrite zeq. 
Qed.

我试图快速复制到另一台机器上，并试图它因而：

Theorem suffix_app (X: Type) (xs ys: list X) : 
    suffix xs ys -> exists ws, xs = ws ++ ys. 
Proof. 
    induction 1. 
    - exists []. reflexivity. 
    - (* Stuck here! *) 
Abort.

即没有“as”条款。但是，由于自动命名的“zeq”的等价物不是由于我无法解决的原因而生成的，所以我被卡住了。为什么Coq在第二种情况下生成的“zeq”（自动命名）不等于？

来源

2017-05-21 Sean Frötkék

这是对我而言，请注意，在第一个示例中，您在模式中有一个“destruct”。因此'将[IHssuffix]破坏为[zs zeq] .'会让你回到游戏中。 – ejgallego

我很震惊，我从来没有发现，但... c'est la vie。谢谢，这完全回答了我的问题。随意把它作为答案，我会接受它。 –

除了破坏，'intros'也可以重写（' - >'）：'induction 1 as [| x？？？ [zs - >]]; [存在[] |存在（x :: zs）]; trivial.' –

正如评论，这是提及@ejgallego因为as子句允许所谓的前奏图案（即图案，你也可以用intros战术使用，如通过@AntonTrunov在评论中提及）。 [zs zeq]模式表示destruct ... as [zs zeq]。要了解更多关于介绍模式的信息，请参阅https://coq.inria.fr/refman/Reference-Manual010.html#hevea_default564

来源

2017-05-22 12:09:21

Coq的不产生归纳假设

回答

相关问题