如何证明Coq中的引理？ [英] How can I prove following lemma in Coq?

问题描述

我试图为以下引理写一个Coq po：

I am trying to write a Coq poof for the following lemma:

Require Export Coq.Structures.OrderedTypeEx.
Require Import FMapAVL.
Module M := FMapAVL.Make(Nat_as_OT).

Fixpoint cc (n: nat) (c: M.t nat):bool :=
match M.find n c with
| None => false
| _ => true
end.

Lemma l: forall (n: nat) (k:nat) (m: M.t nat), cc n m = true  -> cc n (M.add k k m) = true.

我无法简化（M.add kkm）部分。

推荐答案

首先， cc 中没有递归调用，所以您应该将此定义作为普通定义（使用关键字 Definition 而不是 Fixpoint ）。

First, there is no recursive call in cc, so you should make this definition a plain definition (using keyword Definition instead of Fixpoint).

其次，如果要推理 M.find 和 M.add ，您应该
看一下这些函数的定理：定理
M.find_2 ， M.add_2 ， MEeq_dec 和 M.add_1 会很有用（我通过使用搜索命令）。因此，首先展开 cc ，然后根据情况（ M.find nm ）进行推理，然后使用这些值
定理使语句中出现的功能在逻辑上进行发展。请注意，函数 M.MapsTo 在此问题中起关键作用。

Second, if you want to reason about the behavior of M.find and M.add, you should look at the theorems stating things about these functions: theorems M.find_2, M.add_2, M.E.eq_dec, and M.add_1 will be useful (I found these lemmas by using the Search command). So start by unfolding cc, then reason by cases on the value of (M.find n m), then use these theorems to progress logically about the functions occurring in your statements. Please note that function M.MapsTo plays a key role in this problem.

我宁愿不给您解决方案，因为它看起来像是推理表的基本练习。

I would rather not give you the solution because it looks like an elementary exercise in reasoning about tables.

这篇关于如何证明Coq中的引理？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！