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

考虑以下发展:

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。

我想知道是否有一种快速简便的方法来执行这种“smart 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.

最佳答案

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

在幕后，inversion只是调用destruct的一个版本，但首先要记住一些相等性。如您所知，Coq中的模式匹配将“忘记”构造函数的参数，除非它们是变量，否则，将实例化销毁范围内的所有变量。

这意味着什么？这意味着，为了正确地破坏归纳式I : Idx -> Prop，您希望获得以下形式的目标:I x -> Q x，以便破坏I x还将优化x中的Q。因此，归纳I term和目标Q (f term)的标准转换是将其重写为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:策略的一个很好的效果是，与破坏相反，它会试图阻止我们在不首先将其依赖项纳入范围的情况下破坏一个术语。

关于coq - Coq:在不丢失信息的情况下破坏(共)归纳假设，我们在Stack Overflow上找到一个类似的问题：https://stackoverflow.com/questions/45151308/