isabelle - Isabelle/Isar 中的仿函子构造
问题描述
这是数学中的一个小定理:
假设 u 不是 A 的元素,v 不是 B 的元素,f 是从 A 到 B 的单射函数。令 A' = A union {u} 和 B' = B union {v},并定义g: A' -> B' by g(x) = f(x) 如果 x 在 A 中,并且 g(u) = v。那么 g 也是单射的。
如果我正在编写类似 OCaml 的代码,我会将 A 和 B 表示为类型,并将 f 表示为 A->B 函数,例如
module type Q =
sig
type 'a
type 'b
val f: 'a -> 'b
end
然后定义一个函子
module Extend (M : Q) : Q =
struct
type a = OrdinaryA of M.a | ExoticA
type b = OrdinaryB of M.b | ExoticB
let f x = match x with
OrdinaryA t -> OrdinaryB ( M.f t)
| Exotic A -> ExoticB
end;;
我的定理是 ifQ.f
是单射的,那么 也是(Extend Q).f
,我希望我的语法或多或少是正确的。
我想在 Isabelle/Isar 做同样的事情。通常,这意味着写类似
definition injective :: "('a ⇒ 'b) ⇒ bool"
where "injective f ⟷ ( ∀ P Q. (f(P) = f(Q)) ⟷ (P = Q))"
proposition: "injective f ⟹ injective (Q(f))"
并且Q
是……某事。我不知道如何在 Isabelle 中创建一个类似于Q
OCaml 中的仿函数的单个操作,它创建两个新的数据类型和它们之间的函数。单射性的证明似乎相当简单——只是一个四例拆分。但是我想要帮助定义我调用的新函数Q f
,给定函数f
。
解决方案
这是一个解决方案。我试图为函数做一个“定义” Q
,但做不到;相反,创建一个常数Q
(与 强烈类比map
)让我陈述并证明定理:
theory Extensions
imports Main
begin
text ‹We show that if we have f: 'a → 'b that's injective, and we extend
both the domain and codomain types by a new element, and extend f in the
obvious way, then the resulting function is still injective.›
definition injective :: "('a ⇒ 'b) ⇒ bool"
where "injective f ⟷ ( ∀ P Q. (f(P) = f(Q)) ⟷ (P = Q))"
datatype 'a extension = Ordinary 'a | Exotic
fun Q :: "('a ⇒ 'b) ⇒ (('a extension) ⇒ ('b extension))" where
"Q f (Ordinary u) = Ordinary (f u)" |
"Q f (Exotic) = Exotic"
lemma "⟦injective f⟧ ⟹ injective (Q f)"
by (smt Q.elims extension.distinct(1) extension.inject injective_def)
end
推荐阅读
- java - Apache Common Mails:异常:将电子邮件发送到以下服务器失败:smtp.gmail.com:587
- python-3.x - 启动 Django 服务时如何修复此错误?-- 启动的线程中出现未处理的异常
- python-3.x - 如何在python类中对同质属性进行分组
- python - 在 Sql Alchemy 的 add_columns 中格式化列
- javascript - 无法在 chrome v.71 ios 12+ 上打开 blob 文件
- javascript - localeCompare 方法行为不明确
- xamarin - 如何解决在尝试获取令牌时获得 401 Unauthorized 的问题?
- firebase - BigQuery 会向我收取从 Firebase Analytic 导出数据的费用吗
- ssh - Ansible 变得无密码
- payment-gateway - Flutterwave Rave Inline Checkout 集成错误