在Coq中使用匹配表达式分解构造函数的相等性 [英] Decomposing equality of constructors with match expressions in Coq

问题描述

我有一个类似于分解构造函数相等性coq的问题，但是，我的相等性包含匹配表达式。考虑示例（这是荒谬的，但仅用于澄清）：

I have a question similar to Decomposing equality of constructors coq, however, my equality contains a match expression. Consider the example (which is nonsensical, but just used for clarification):

Fixpoint positive (n : nat) :=
  match n with
  | O => Some O
  | S n => match positive n with
    | Some n => Some (S n)
    | None => None (* Note that this never happens *)
    end
  end.

Lemma positiveness : forall n : nat, Some (S n) = positive (S n).
Proof.
intro.
simpl.

此时， n：nat 在环境中，目标是：

At this point, with n : nat in the environment, the goal is:

Some (S n) =
match positive n with
| Some n0 => Some (S n0)
| None => None
end

我想将其转换为环境<$ c $中的两个子目标c> n，n0：nat ：

positive n = Some n0  (* Verifying the match *)
S n = S n0            (* Verifying the result *)

我希望如果 match 证明相等存在多个可能有效的情况，那么新目标就是将所有可能性分离开，例如

And I would expect that if the match to prove equality on has multiple cases that might work, the new goal is a disjunction of all possibilities, so e.g. for

Some (S n) =
match positive n with
| Some (S n0) => Some (S (S n0))
| Some O => Some (S O)
| None => None
end

我希望

   (positive n = Some (S n0) /\ S n = S (S n0))  (* First alternative *)
\/ (positive n = Some O      /\ S n = S O)       (* Second alternative *)

是否有Coq策略

推荐答案

是否有Coq策略可以做到这一点或类似的目的？ ？

Is there a Coq tactic which does this or something similar?

如果运行 destruct（positive n）eqn：H ，则表示将获得两个子目标。在第一个子目标中，您将得到：

If you run destruct (positive n) eqn:H, you will get two subgoals. In the first subgoal, you get:

  n, n0 : nat
  H : positive n = Some n0
  ============================
  Some (S n) = Some (S n0)

，在第二个子目标中，您将得到

and in the second subgoal you get

  n : nat
  H : positive n = None
  ============================
  Some (S n) = None

这并非您所要的，但是在第二个子目标中，您可以编写 assert（存在n0，正n =某个n0）；这将为您提供您想要的目标，并且可以通过存在破坏破坏并使用 congruence 或 discriminate 表示 n正值不能为没有和有些。

This is not exactly what you asked for, but in the second subgoal, you can write assert (exists n0, positive n = Some n0); this will give you the goal you seek, and you can discharge the remaining goal by destructing the exists and using congruence or discriminate to show that positive n cannot be None and Some at the same time.

这篇关于在Coq中使用匹配表达式分解构造函数的相等性的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！