6

考虑以下发展：

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.
4

2 回答 2

6

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

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

这意味着什么？这意味着为了正确地破坏一个 inductive I : Idx -> Prop，你想要得到你的目标形式：I x -> Q x，这样破坏 theI x也将细化xin Q。I term因此，归纳和目标的标准转换Q (f term)是将其重写为I x -> x = term -> Q (f x). 然后，破坏I x将使您x实例化到正确的索引。

case:考虑到这一点，使用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:是，与 destruct 相反，它会试图阻止我们在没有首先将其依赖项纳入范围的情况下破坏一个术语。

于 2017-07-17T19:20:30.693 回答
3

打电话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.

于 2017-07-17T18:45:20.947 回答