我定义2种几乎相同的语言（foo和bar）： theory SimpTr
imports Main
begin
type_synonym vname = "string"
type_synonym 'a env = "vname ⇒ 'a option"
datatype foo_exp =
FooBConst bool |
FooIConst int |
下面是一个简单的感应关系： datatype t1 = A t1 t1 | B
datatype t2 = C t2 t2 | D
inductive P :: "t1 ⇒ t2 ⇒ bool" where
"P x1 y1 ⟹ P x2 y2 ⟹ P (A x1 x2) (C y1 y2)" |
"P B D"
lemma P_fun:
"P x y ⟹
我试图从chapter 7 of "theorem proving in lean"了解归纳类型。 我给自己设定了证明自然数的是继任者的任务，拥有平等的一个替代性质： inductive natural : Type
| zero : natural
| succ : natural -> natural
lemma succ_over_equality (a b : natural) (
我有一个编程语言AST的数据类型，我想推理一下，但AST的约有10种不同的构造函数。 data Term : Set where
UnitTerm : Term
VarTerm : Var -> Term
...
SeqTerm : Term -> Term -> Term
我想写一个函数，该语言的语法树具有可判定的相等性。理论上，这很简单：没有太复杂的
假设如下： Inductive bin : Set := Z | O.
Fixpoint fib (n : nat) : list bin :=
match n with
| 0 => [Z]
| S k => match k with
| 0 => [O]
| S k' => fib k' ++ fib k
end
我正在研究诸如吸血鬼和E-Prover这样的一阶逻辑定理证明器，并且TPTP语法似乎是要走的路。我对逻辑编程语法比较熟悉，例如Answer Set Programming和Prolog，虽然我尝试引用TPTP syntax的详细描述，但我仍然不明白如何正确区分解释函数和非解释函子（而且我可能使用术语错误）。 本质上，我试图通过证明没有模型作为反例来证明一个定理。我的第一个困难是我没有想到下面的逻辑