我是一名大学讲师,教授一门名为《语言类型系统》的课程。上节课,教授在黑板上使用了以下示例来说明类型理论中归纳证明的概念:
假设我们通过归纳定义了自然数(出于某种原因,他坚持称之为“项”),并且我们对它们进行了递归定义的“大于”函数。我们可以证明对于每个n,都成立(suc n > n)。
我已经准备好了以下Coq代码,用于在课堂上实现这个示例。
这让我想到了下一个目标:
我可以通过重写、展开和/或简化的多种方式来解决这个问题,但我真正想做的是应用一次greaterThan的迭代,将
有没有办法实现这个?
附注:我知道我可以使用
编辑:感谢Théo Winterhalter的回答,我意识到我也可以单独使用
假设我们通过归纳定义了自然数(出于某种原因,他坚持称之为“项”),并且我们对它们进行了递归定义的“大于”函数。我们可以证明对于每个n,都成立(suc n > n)。
我已经准备好了以下Coq代码,用于在课堂上实现这个示例。
Inductive term : Set :=
| zero
| suc (t : term)
.
Fixpoint greaterThan (t t' : term) {struct t} : bool :=
match t, t' with
| zero, _ => false
| suc t, zero => true
| suc t, suc t' => t > t'
end
where "t > t'" := (greaterThan t t').
Lemma successorIsGreater : forall t : term, suc t > t = true.
Proof.
induction t.
(* zero *)
- simpl.
reflexivity.
(* suc t *)
-
这让我想到了下一个目标:
1 subgoal
t : term
IHt : (suc t > t) = true
______________________________________(1/1)
(suc (suc t) > suc t) = true
我可以通过重写、展开和/或简化的多种方式来解决这个问题,但我真正想做的是应用一次greaterThan的迭代,将
(suc (suc t) > suc t) = true
转化为(suc t > t) = true
,然后我可以用exact IHt
完成证明。有没有办法实现这个?
附注:我知道我可以使用
simpl in IHt
然后使用exact
,但它会展开匹配表达式,比在这里需要的更冗长。编辑:感谢Théo Winterhalter的回答,我意识到我也可以单独使用
exact
,因为这些术语是可转换的,但这不会很好地向学生展示过程。(顺便说一句:归纳的两种情况也可以用trivial
解决,但我认为他们从中学到的东西不多。:D)
exact
,这不会向学生展示过程),但改变似乎仍然是我最好的选择,所以非常感谢您提到了这种可能性!如果没有更好的答案出现,我将标记您的答案为被接受的。 - Isti115SCappella
的答案标记为被接受的,因为它似乎更适合我所寻找的(需要较少的解释),但其他提出的想法也很棒,值得记住! - Isti115