我在Coq的SSReflect扩展中找到了两个公约,这些公约看起来特别有用,但我还没有看到在新的依赖类型语言(Lean,Agda,Idris)中广泛采用的公约.
首先,可能的谓词表示为布尔返回函数,而不是归纳定义的数据类型.这默认带来可判定性,通过计算开辟了更多的证明机会,并通过避免校对引擎携带大量证明条件来提高检查性能.我看到的主要缺点是需要使用反射词来在证明时操纵这些布尔谓词.
其次,具有不变量的数据类型被定义为包含简单数据类型和不变量证明的从属记录.例如,固定长度序列在SSReflect中定义,如:
Structure tuple_of : Type := Tuple {tval :> seq T; _ : size tval == n}.
A seq和证明该序列的长度是一定值.这与Idris如何定义此类型相反:
data Vect : (len : Nat) -> (elem : Type) -> Type
一种依赖类型的数据结构,其中不变量是其类型的一部分.SSReflect方法的一个优点是它允许重用,因此例如许多定义的函数seq和关于它们的证明仍然可以使用tuple(通过对底层操作seq),而使用Idris的方法函数reverse,append等等需要被重写Vect.Lean实际上在其标准库中具有等效的SSReflect样式vector,但它也具有Idris样式array,似乎在运行时具有优化的实现.
一本面向SSReflect的书甚至声称Vect n A风格方法是反模式:
依赖类型语言和Coq中的常见反模式特别是将这样的代数属性编码到数据类型和函数本身的定义中(这种方法的规范示例是长度索引列表).虽然这种方法看起来很吸引人,因为它展示了依赖类型捕获它们的数据类型和函数的某些属性的能力,但它本质上是不可扩展的,因为总会有另一个感兴趣的属性,这是设计者没有预见到的.数据类型/函数的数据,因此它必须被编码为外部事实.这就是为什么我们提倡这种方法,其中数据类型和函数被定义为尽可能接近程序员定义的方式,并且它们的所有必要属性都是分开证明的.
因此,我的问题是,为什么没有更广泛地采用这些方法.我缺少哪些缺点,或者它们的优势在具有比Coq更好支持依赖模式匹配的语言中不那么重要？
他们来自微软,看起来像是助理？除了语法差异之外,还有哪些实际方面使它们彼此不同(比如说能够做自动化,表达能力等)？我是正式验证的新手.
编辑:我不是要求哪一个更好,我只是对这些工具提供的不同功能之间的技术比较感兴趣.我正在寻找像这样
有人发现 Setoids 被广泛用于 Agda、Coq 等语言中……事实上，Lean 等语言认为它们可以帮助避免“Setoid Hell”。首先使用 Setoids 的原因是什么？转向基于 HoTT（如立方体 Agda）的外延类型理论是否减少了对 Setoids 的需求？
我试图从"精益证明中的证据"第7章中理解归纳类型.
我为自己设定了一个任务,证明自然数的继承者有平等的替代属性:
inductive natural : Type
| zero : natural
| succ : natural -> natural
lemma succ_over_equality (a b : natural) (H : a = b) :
(natural.succ a) = (natural.succ b) := sorry
经过一些猜测和相当详尽的搜索后,我能够满足编译器的几种可能性:
lemma succ_over_equality (a b : natural) (H : a = b) :
(natural.succ a) = (natural.succ b) :=
eq.rec_on H (eq.refl (natural.succ a))
--eq.rec_on H rfl
--eq.subst H rfl
--eq.subst H (eq.refl (natural.succ a))
--congr_arg (? (n : natural), (natural.succ n)) H …在精益中，我有时想将一种rw策略应用于多个相同术语中的一个。例如我有一个目标
\xe2\x8a\xa2 0 = 0\n我想要rw它
\xe2\x8a\xa2 a * 0 = 0\n我也有
\nmul_zero (a : mynat) :\n a * 0 = 0\n现在我应该能够重写0to a * 0。然而尝试
rw \xe2\x86\x90 zero_mul a,\n给我
\n\xe2\x8a\xa2 a * 0 = a * 0\n这不是我想要的！
\n精益这样做有什么原因吗？是否有某种方法可以将重写仅应用于一个术语？
\nLean 4 是一种纯粹的函数式编程语言，但它是惰性的（如 Haskell）还是严格的（如 Idris）？这意味着什么？有没有办法选择加入（或选择退出）懒惰？
我尝试使用归纳数据类型的语法,但它得到一条错误消息"互感类型必须编译为具有依赖消除的基本归纳类型".
下面是我尝试定义命题even和odd自然数的一个例子
mutual inductive even, odd
with even: ? ? Prop
| z: even 0
| n: ? n, odd n ? even (n + 1)
with odd: ? ? Prop
| z: odd 1
| n: ? n, even n ? odd (n + 1)
还有一个相关的问题:定义相互递归函数的语法是什么？我似乎无法在任何地方找到它.
我正在学习精益教程的第 4 章。
我希望能够证明简单的等式，例如a = b ? a + 1 = b + 1 无需使用 calc 环境。换句话说，我想明确构建以下证明项：
example (a b : nat) (H1 : a = b) : a + 1 = b + 1 := sorry
我最好的猜测是我需要使用eq.subst标准库中关于自然数相等的一些相关引理，但我不知所措。我能找到的最接近的精益例子是这样的：
example (A : Type) (a b : A) (P : A ? Prop) (H1 : a = b) (H2 : P a) : P b :=
eq.subst H1 H2
为什么 mathlib 对 UFD 的定义是这样的：
class unique_factorization_domain (? : Type*) [integral_domain ?] :=
(factors : ? ? multiset ?)
(factors_prod : ?{a : ?}, a ? 0 ? (factors a).prod ~? a)
(prime_factors : ?{a : ?}, a ? 0 ? ?x?factors a, prime x)
（要求通过类型类推断来推断整数域结构）但它对 PID 的定义是这样的：
class principal_ideal_domain (? : Type*) extends integral_domain ? :=
(principal : ? (S : ideal ?), S.is_principal)
扩展整体域结构？有什么不同？旧的结构命令与它有关吗？
我在 macOS Catalina 下使用美式键盘在 VS Code 中使用 Lean。如何输入符号，例如暗示箭头、联合、交集、子集？
是否有一些内置或附加调色板来促进这一点？或者我是否必须使用 Option 键组合，如果是这样，我在哪里可以找到合适的代码？