标签: proof

我们有2种语言(非正式地)在语义上等同但在语法上不同.一个是xml,另一个是基于脚本.我怎样才能正式证明这两种语言实际上是等价的.脚本方法只是一种编写相同程序的便捷方式,在xml中编写这些程序会很繁琐.

谢谢Ketan

我开始学习Coq,并试图证明一些看似相当简单的东西:如果列表包含x,那么该列表中x的实例数将> 0.

我已经定义了contains和count函数,如下所示:

Fixpoint contains (n: nat) (l: list nat) : Prop :=
  match l with
  | nil => False
  | h :: t => if beq_nat h n then True else contains n t
  end.

Fixpoint count (n acc: nat) (l: list nat) : nat :=
  match l with
  | nil => acc
  | h :: t => if beq_nat h n then count n (acc + 1) t else count n acc t
  end.

我试图证明:

Lemma contains_count_ge1 : …

Haskell 经常被吹捧为进行证明的语言。（在他们开始推荐 Agda、Idris 或 Coq 之前）。但是，这段代码没有潜在问题还是我对这个概念的理解错误？

x :: Int -> Int
x n
 | x == 0 = error "Error"
 | otherwise = n + 1

据我了解，这对于检查证明不太好（因为Int这里不强制返回。）
有没有办法解决这个问题？

据我了解，上述其他语言都避免了这种情况。[1] 我不明白怎么办。仅仅是因为更严格的类型系统还是该语言提供的其他一些保证？

到目前为止，我已经仔细查看了语言文档，但什么也没找到。

[1] = https://www.reddit.com/r/haskell/comments/9toh6b/comment/e8y4gzi/?utm_source=share&utm_medium=web2x&context=3

我需要证明

f (g xs) == g (f xs)

当 xs 是 Int 的有限列表时。

假设 f 和 g 都是 [Int]->[Int] 类型