时间戳

首页 > 解决方案 > 在 Coq 中求解一个变量

coq - 在 Coq 中求解一个变量

问题描述

有没有办法解决 Coq 中的变量？鉴于：

From Coq Require Import Reals.Reals. 

Definition f_of_x (x : R) : R := x + 1. 
Definition f_of_y (y : R) : R := y + 2.

我想表达

Definition x_of_y (y : R) : R :=

就像solve for x in f_of_x = f_of_y.我希望使用策略语言然后改组术语一样。我最终想得到正确的可用定义，y + 1.我认为想要使用我的定义：

Compute x_of_y 2. (* This would yield 3 if R was tractable or if I was using nat *)

另一种方法是用铅笔/纸手工完成，然后只用 Coq检查我的工作。这是唯一的方法吗？

标签： coq

解决方案

如果我理解正确，您要表达的是方程的解的存在

x + 3 = x + 2

如果是这样，您可以在 coq 中将其声明为

Lemma solution :
  exists x, x + 3 = x + 2.

如果它是x + 2 = 2 * x可以解决的，那么您可以将其解决为

Lemma solution :
  exists x, x + 2 = 2 * x.
Proof.
  exists 2. reflexivity.
Qed.

但是当然没有解决方案x + 3 = x + 2。如果你想要一个解决方案，y固定为

x + 3 = y + 2

你必须量化y：

Lemma solution :
  forall y, exists x, x + 1 = y + 2.
Proof.
  intro y.
  eexists. (* Here I'm saying I want to prove the equality and fill in the x later *)
  eapply plus_S_inj.
  rewrite plus_0.
  reflexivity.
Defined.

Print solution. (* You will see the y + 1 here *)

在这里，我假设一些可以帮助我操纵数字的引理：

Lemma plus_S_inj :
  forall x y z t,
    x + z = y + t ->
    x + (S z) = y + (S t).
Admitted.

Lemma plus_0 :
  forall x,
    x + 0 = x.
Admitted.

对于您的概念，您可能有类似的引理R（我不知道它是什么，所以我不能再进一步了。）

推荐阅读