只是CoQ证明中的通用量化假设 [英] Just a universally quantified hypotesis in coq proof

问题描述

另一个硬目标(当然，对我而言)如下:

Goal ~(forall P Q: nat -> Prop,
  (exists x, P x) /\ (exists x, Q x) ->
  (exists x, P x /\ Q x)).
Proof.

我绝对不知道该怎么办.如果我介绍一些东西，我会在假设中得到一个通用量词，然后我就什么也做不了.

我想这是管理这种情况的一种标准方法，但我找不到它.

解决方案

要继续获得证明，您必须展示P的实例和Q的实例，以便您的假设产生矛盾./p>

一种简单的使用方法是:

P : fun x => x = 0
Q : fun x => x = 1

为了使用介绍的假设，您可能要使用战术specialize:

Goal ~(forall P Q : nat -> Prop,
  (exists x, P x) /\ (exists x, Q x) ->
  (exists x, P x /\ Q x)).
Proof.
  intro H.
  specialize (H (fun x => x = 0) (fun x => x = 1)).

它使您可以将假设之一应用于某些输入(假设是函数时).从现在开始，您应该可以轻松得出矛盾.

除了specialize之外，您还可以执行以下操作:

  pose proof (H (fun x => x = 0) (fun x => x = 1)) as Happlied.

这将保留H并为您提供另一个术语Happlied(您选择名称).

Another hard goal (for me, of course) is the following:

Goal ~(forall P Q: nat -> Prop,
  (exists x, P x) /\ (exists x, Q x) ->
  (exists x, P x /\ Q x)).
Proof.

I absolutely have no idea of what could I do. If I introduce something, I get a universal quantifier in the hypotesis, and then I can't do anything with it.

I suppose that it exists a standard way for managing such kind of situations, but I was not able to find it out.

解决方案

To progress in that proof, you will have to exhibit an instance of P and an instance of Q such that your hypothesis produces a contradiction.

A simple way to go is to use:

P : fun x => x = 0
Q : fun x => x = 1

In order to work with the hypothesis introduced, you might want to use the tactic specialize:

Goal ~(forall P Q : nat -> Prop,
  (exists x, P x) /\ (exists x, Q x) ->
  (exists x, P x /\ Q x)).
Proof.
  intro H.
  specialize (H (fun x => x = 0) (fun x => x = 1)).

It allows you to apply one of your hypothesis on some input (when the hypothesis is a function). From now on, you should be able to derive a contradiction easily.

Alternatively to specialize, you can also do:

  pose proof (H (fun x => x = 0) (fun x => x = 1)) as Happlied.

Which will conserve H and give you another term Happlied (you choose the name) for the application.

这篇关于只是CoQ证明中的通用量化假设的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！