Coq:在不丢失信息的情况下破坏(共)归纳假设

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

确实，反转基本上可以满足您的要求，但是正如 Arthur 指出的那样，它有点不稳定，主要是由于同余步骤不同。

在底层，inversion 只是调用 destruct 的一个版本，但首先要记住一些等式。正如您所发现的，Coq 中的模式匹配将“忘记”构造函数的参数，除非这些参数是变量，那么，析构作用域下的所有变量都将被实例化。

这是什么意思？这意味着，为了正确地破坏归纳 I : Idx -> Prop，您需要获得以下形式的目标:I x -> Q x，这样破坏I x也会优化Q中的x。因此，归纳 I 项 和目标 Q (f 项) 的标准转换是将其重写为 I x -> x = term -> Q ( f x) 。然后，析构 I x 将使您的 x 实例化到正确的索引。

考虑到这一点，使用 Coq 8.7 的 case: 策略手动实现反转可能是一个很好的练习；

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: 策略的一个很好的效果是，与 destruct 相反，它会尝试阻止我们在不首先将其依赖项纳入范围的情况下破坏术语。