coq - Isabelle 中带有类型参数的归纳谓词

Question

我开始学习 Isabelle，并想尝试在 Isabelle 中定义幺半群，但不知道如何做。

在 Coq 中，我会做这样的事情:

Inductive monoid (τ : Type) (op: τ -> τ -> τ) (i: τ): Prop :=
| axioms: (forall (e: τ), op e i = e) ->
          (forall (e: τ), op i e = e) ->
          monoid τ op i.

我不知道如何在伊莎贝尔做同样的事情。从概念上讲，我想到了这样的事情:

inductive 'a monoid "('a ⇒ 'a ⇒ 'a) ⇒ 'a ⇒ bool" for f i where
  axioms: "⟦f e i = e; f i e = e⟧ ⇒ monoid f i"

但是，这在伊莎贝尔是无效的。

如何在 Isabelle 中定义带类型参数的归纳谓词？

Answer 1

我对 Coq 不太了解，但 Isabelle 的类型系统非常不同。 Isabelle 值不采用“类型参数”，Isabelle 类型也不采用“值参数”。

在 Isabelle 中，您的示例是一个简单的多态定义，可以像这样完成:

inductive monoid :: "('a ⇒ 'a ⇒ 'a) ⇒ 'a ⇒ bool" for f i where
  axioms: "⟦f e i = e; f i e = e⟧ ⟹ monoid f i"

我必须指出，这意味着如果存在甚至一个 e ，那么您就有了一个幺半群。您可能想写的是

inductive monoid :: "('a ⇒ 'a ⇒ 'a) ⇒ 'a ⇒ bool" for f i where
  axioms: "⟦⋀e. f e i = e; ⋀e. f i e = e⟧ ⟹ monoid f i"

这里，e 在假设中被普遍量化，这意味着定律必须对所有 e 成立才能构成幺半群。

将其作为归纳定义是可能的，并且具有自动生成适当的引入/消除规则的优点(以及使用inducing_cases生成更多规则的能力)，但是，还有其他方法。

使用定义

但是，您也可以将其写为一个简单的定义:

definition monoid :: "('a ⇒ 'a ⇒ 'a) ⇒ 'a ⇒ bool" where
  "monoid f i = ((∀e. f e i = e) ∧ (∀e. f i e = e))"

这为您提供了 monoid 的定义作为引理 monoid_def。如果你想要引入/消除规则，你必须自己推导它们。

使用区域设置

第三个，可能也是最合适的解决方案是区域设置。语言环境是一种将某些固定变量和假设保留在上下文中并在该上下文中进行推理的方法。以下示例演示了如何将幺半群定义为语言环境，在该语言环境中派生引理，然后解释具体示例幺半群(即列表)的语言环境，并使用我们在语言环境中证明的引理。

locale monoid =
  fixes i :: 'a and f :: "'a ⇒ 'a ⇒ 'a"
  assumes left_neutral:  "f i e = e"
      and right_neutral: "f e i = e"
begin
  lemma neutral_unique_left:
    assumes "⋀e. f i' e = e"
    shows   "i' = i"
  proof-
    from right_neutral have "i' = f i' i" by simp
    also from assms have "f i' i = i" by simp
    finally show "i' = i" .
  qed
end

thm monoid.neutral_unique_left
(* Output: monoid i f ⟹ (⋀e. f i' e = e) ⟹ i' = i *)

(* Let's interpret our monoid for the type "'a list", with [] 
   as neutral element and concatenation (_ @ _) as the operation. *)
interpretation list_monoid: monoid "[]" "λxs ys. xs @ ys"
  by default simp_all

thm list_monoid.neutral_unique_left
(* Output: (⋀e. i' @ e = e) ⟹ i' = [] *)

使用类型类

第四种可能性与类型类的区域设置类似。 Isabelle 支持类型类(就像 Haskell 中的类型类，尽管限制更多)，并且您可以创建一个 monoid 类型类，然后将其实例化为具体类型，例如 nat、 int、'a list 等

更多信息

有关归纳谓词、区域设置和类型类的更多信息，请参阅这些工具的文档:http://isabelle.in.tum.de/documentation.html