有没有办法在 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 的概念，您可能有类似的引理（我不知道它是什么，所以我不能再进一步了。）
【讨论】：
x 和y 是R，您能否在答案中完成最后的Lemma？我做了intros y.，但随后必须飞跃使用exists (y + 1). 我不知道如何进行代数操作，即从两边减去 1，所以 x 是单独的......
R 类型的术语的操作应该留给单独的问题。
R。
solution，因为你已经这样做了。在您的情况下，我们正在处理nat，我认为solution 可以像Compute solution 2. (* yields 3 *) 一样使用。取而代之的是Check solution 2. 产生exists x, x + 1 = 2 + 2，即Prop。我可以对这个结果做些什么吗？
existT，你可以匹配它来获取见证。如果我回答了您的问题，请考虑将其标记为已解决。