主页 / coding / 问题 / 79266019
Accepted
Mohamed Elsheikh
Asked: 2024-12-10 02:05:54 +0800 CST

Coq 重复使用了归纳假设中的一个术语，而不是创建一个新的术语

  • 772

我有这个目标，我想证明这一点。

1 goal
t1, t2 : FCPLang
H : evalS t1 = Some t2
______________________________________(1/1)
evalBS t1 = evalBS t2

为了证明这一点，我使用了induction t1.，但这些是引入的归纳假设：

1 goal
t1_1, t1_2, t1_3, t2 : FCPLang
H : evalS (if_then_else t1_1 t1_2 t1_3) = Some t2
IHt1_1 : evalS t1_1 = Some t2 -> evalBS t1_1 = evalBS t2
IHt1_2 : evalS t1_2 = Some t2 -> evalBS t1_2 = evalBS t2
IHt1_3 : evalS t1_3 = Some t2 -> evalBS t1_3 = evalBS t2
______________________________________(1/1)
evalBS (if_then_else t1_1 t1_2 t1_3) = evalBS t2

我认为这毫无用处，因为t2再次使用它们，而不是引入一个新术语，例如： IHt1_1 : evalS t1_1 = Some t2_1 -> evalBS t1_1 = evalBS t2_1 我该如何解决这个问题？

coq

1 个回答

  1. Best Answer

    您要做的就是“t2在归纳假设中量化”。正如您所指出的，t2在整个归纳过程中是固定的，但您希望它发生变化。为了实现这一点，您需要对其进行量化，以便您通过归纳证明的陈述对所有都t2成立。

    有两种方法可以实现这一点。“更原始”的方法是告诉你发生了什么（因此对学习者有好处），即

    revert t2. induction t1; intros t2.

    您会注意到，现在所有归纳假设都以 开头forall t2, ...，因此您可以任意更改t2s 来使用它们。

    由于一直打字revert很intros烦人，所以有一个更高级的技巧

    induction t1 in t2|-*.

    这可以概括为例如 induction t1 in t2,t3,Ht23|-*。|-*需要在那里，如果你忽略它，事情就不会起作用。

    • 1

相关问题