勒柯克：毀滅（共）歸納假設，而不會丟失信息

Question

考慮以下發展：

Require Import Relation RelationClasses. 

Set Implicit Arguments. 

CoInductive stream (A : Type) : Type := 
| scons : A -> stream A -> stream A. 

CoInductive stream_le (A : Type) {eqA R : relation A} 
         `{PO : PartialOrder A eqA R} : 
         stream A -> stream A -> Prop := 
| le_step : forall h1 h2 t1 t2, R h1 h2 -> 
      (eqA h1 h2 -> stream_le t1 t2) -> 
      stream_le (scons h1 t1) (scons h2 t2). 

如果我有一個假設stream_le (scons h1 t1) (scons h2 t2)，這將是合理的destruct戰術把它變成一對假說R h1 h2的和eqA h1 h2 -> stream_le t1 t2。但這不是什麼情況，因爲destruct每當做任何不重要的事情都會丟失信息。相反，新術語h0,h3,t0,t3被引入到上下文中，但不記得它們分別等於h1,h2,t1，t2。

我想知道是否有快速簡單的方法來做這種「智能destruct」。這是我現在所擁有的：

Theorem stream_le_destruct : forall (A : Type) eqA R 
    `{PO : PartialOrder A eqA R} (h1 h2 : A) (t1 t2 : stream A), 
    stream_le (scons h1 t1) (scons h2 t2) -> 
    R h1 h2 /\ (eqA h1 h2 -> stream_le t1 t2). 
Proof. 
    intros. 
    destruct H eqn:Heq. 
    remember (scons h1 t1) as s1 eqn:Heqs1; 
    remember (scons h2 t2) as s2 eqn:Heqs2; 
    destruct H; 
    inversion Heqs1; subst; clear Heqs1; 
    inversion Heqs2; subst; clear Heqs2. 
    split; assumption. 
Qed. 

Answer 1

事實上，inversion基本上是做你想做的事情，然而就像Arthur指出的那樣，它有點不穩定，主要是由於不同的步驟。

在引擎蓋下，inversion只是調用版本destruct，但首先要記住一些平等。正如你已經發現的那樣，Coq中的模式匹配將會「忘記」構造函數的參數，除非這些變量是變量，那麼將會實例化在destruct的範圍下的所有變量。

這是什麼意思？這意味着爲了正確地摧毀一個歸納的I : Idx -> Prop，您希望獲得以下形式的目標：I x -> Q x，這樣破壞I x也將改進Q中的x。因此，感應I term和目標Q (f term)的標準轉換是將其重寫爲I x -> x = term -> Q (f x)。然後，破壞I x會讓你x實例化爲正確的索引。考慮到這一點，使用Coq 8.7的策略手動實施反演可能是一個很好的練習;

From Coq Require Import ssreflect. 
Theorem stream_le_destruct A eqA R `{PO : PartialOrder A eqA R} (h1 h2 : A) (t1 t2 : stream A) : 
    stream_le (scons h1 t1) (scons h2 t2) -> 
    R h1 h2 /\ (eqA h1 h2 -> stream_le t1 t2). 
Proof. 
move E1: (scons h1 t1) => sc1; move E2: (scons h2 t2) => sc2 H. 
by case: sc1 sc2/H E1 E2 => h1' h2' t1' t2' hr ih [? ?] [? ?]; subst. 
Qed. 

你可以閱讀手冊瞭解更多細節，但基本上用第一行，我們創建我們需要的平等;那麼，在第二個我們可以破壞這個術語並獲得解決目標的恰當實例。 case:策略的好效果是，與破壞相反，它會試圖阻止我們在不首先將其依賴關係納入範圍的情況下破壞術語。

Answer 2

調用destruct不會直接給你你想要的。您需要改用inversion。

Theorem stream_le_destruct : forall h1 h2 t1 t2, 
    stream_le (scons h1 t1) (scons h2 t2) -> 
    h1 <= h2 /\ (h1 = h2 -> stream_le t1 t2). 
Proof. 
    intros. 
    inversion H; subst; clear H. 
    split; assumption. 
Qed. 

不幸的是，inversion戰術是很不舒服的表現，因爲它往往會產生大量的假平等的假設，很難對他們一貫的名字。其中一個（有點重量級，坦率地說）替代方法是僅使用inversion來證明您所做的一個引理，並將這個引理應用於證明中，而不是調用inversion。