小编kai*_*wen的帖子

更新:在Arthur Azevedo De Amorim的帮助下,我终于完成了它.代码附在问题的末尾.

我正在阅读"类型和编程语言"一书,我试图用coq来证明本书中的每个定理(引理).当谈到定理3.5.4时,我试过并且无法管理它.这是问题描述.

AST的一种小语言:

t = :: true
    :: false
    :: if t then t else t

评估规则是:

1. if true then t2 else t3 -> t2 (eval_if_true)
2. if false then t2 else t3 -> t3 (eval_if_false)
3.             t1 -> t1'
         ------------------------  (eval_if)
         if t1 then t2 else t3 -> 
           if t1' then t2 else t3

我要证明的定理是:对于任何t1 t2 t3,给定t1 - > t2和t1 - > t3,则t2 = t3.

我在Coq中构建类型和命题如下:

Inductive t : Type :=
| zhen (* represent …

当在纸上推理时,我经常通过归纳使用一些列表的长度.我想在Coq中形式化这些参数,但似乎没有任何内置的方法来对列表的长度进行归纳.

我该如何进行这样的归纳？

更具体地说,我试图证明这个定理.在纸面上,我通过归纳证明了它的长度w.我的目标是在Coq中形式化这个证明.