Coq：如何证明语句是否涉及字符串？ [英] Coq: How to prove if statements involving strings?

问题描述

我有一个字符串a ，并且与字符串b 进行比较，如果相等则有一个字符串c ，否则具有字符串x 。我在假设中知道 fun x< = fun c 。我如何证明以下陈述？ fun 是一些函数，它接受 string 并返回 nat 。

I have a string a and on comparison with string b, if equals has an string c, else has string x. I know in the hypothesis that fun x <= fun c. How do I prove this below statement? fun is some function which takes in string and returns nat.

fun (if a == b then c else x) <= S (fun c)

逻辑似乎很明显，但是我无法在coq中拆分if语句。

The logic seems obvious but I am unable to split the if statements in coq. Any help would be appreciated.

谢谢！

推荐答案

可以写一条if-then-else语句，这意味着测试表达式 a == b 的类型具有两个构造函数（例如 bool ）或（ sumbool ）。我将首先假定类型为 bool 。在那种情况下，在证明过程中最好的方法是输入以下命令。

If you can write an if-then-else statement, it means that the test expression a == b is in a type with two constructors (like bool) or (sumbool). I will first assume the type is bool. In that case, the best approach during a proof is to enter the following command.

case_eq (a == b); intros hyp_ab.

这将产生两个目标。在第一个假设中，您将有一个假设

This will generate two goals. In the first one, you will have an hypothesis

hyp_ab : a == b = true

断言测试成功，目标结论具有以下形状（ if-then-else 为替换为 then 分支）：

that asserts that the test succeeds and the goal conclusion has the following shape (the if-then-else is replaced by the then branch):

fun c< = S（fun c）

fun c <= S (fun c)

在第二个目标中，您将有一个假设

In the second goal, you will have an hypothesis

hyp_ab : a == b = false

目标结论具有以下形状（ if-then-else 替换为 else 分支）。

and the goal conclusion has the following shape (the if-then-else is replaced by the else branch).

fun x <= S (fun c)

您应该能够从那里继续。

You should be able to carry on from there.

另一方面，来自Coq的 String 库具有函数 string_dec ，返回类型为 { a = b} + {a<> b} 。如果您的符号 a == b 是 string_dec ab 的漂亮符号，则最好使用以下策略：

On the other hand, the String library from Coq has a function string_dec with return type {a = b}+{a <> b}. If your notation a == b is a pretty notation for string_dec a b, it is better to use the following tactic:

destruct (a == b) as [hyp_ab | hyp_ab].

该行为将与我上面描述的非常接近，只是更易于使用。

The behavior will be quite close to what I described above, only easier to use.

直觉上，当您在 if-then-else 语句中进行推理时，可以使用类似 case_eq ，破坏或案例，它们会导致您分别研究两条执行路径，请记住一个假设，为什么您采取每个执行路径。

Intuitively, when you reason on an if-then-else statement, you use a command like case_eq, destruct, or case that leads you to studying separately the two executions paths, remember in an hypothesis why you took each of these executions paths.

这篇关于Coq：如何证明语句是否涉及字符串？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！