我定義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的詳細描述，但我仍然不明白如何正確區分解釋函數和非解釋函子（而且我可能使用術語錯誤）。 本質上，我試圖通過證明沒有模型作爲反例來證明一個定理。我的第一個困難是我沒有想到下面的邏輯