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的不產生歸納假設

回答

相關問題