勒柯克：毁灭（共）归纳假设，而不会丢失信息

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。