我在一个小项目中工作，目标是给出 Gcd 的定义，它给出两个数字的 gcd 以及结果正确的证明。但我无法给出 Gcd 的完整定义。 Idris 1.3.0 中 Gcd 的定义是完全的，但使用 assert_total 来强制完全，这违背了我项目的目的。有人对 Gcd 有一个不使用 assert_total 的完整定义吗？
附： - 我的代码上传到https://github.com/anotherArka/Idris-Number-Theory.git
【问题讨论】：
标签： idris
我有一个版本，它使用 Accessible 关系来表明您找到的 gcd 的两个数字之和在每次递归调用时都会变小：https://gist.github.com/edwinb/1907723fbcfce2fde43a380b1faa3d2c#file-gcd-idr-L25
它依赖于此，来自Prelude.Wellfounded：
data Accessible : (rel : a -> a -> Type) -> (x : a) -> Type where
Access : (rec : (y : a) -> rel y x -> Accessible rel y) ->
Accessible rel x
一般的想法是，您可以通过明确说明什么变得更小来进行递归调用，并为每个递归调用提供证明，证明它确实变小了。对于gcd，它看起来像这样（gcdt 为总版本，因为gcd 在前奏中）：
gcdt : Nat -> Nat -> Nat
gcdt m n with (sizeAccessible (m + n))
gcdt m Z | acc = m
gcdt Z n | acc = n
gcdt (S m) (S n) | (Access rec)
= if m > n
then gcdt (minus m n) (S n) | rec _ (minusSmaller_1 _ _)
else gcdt (S m) (minus n m) | rec _ (minusSmaller_2 _ _)
sizeAccessible 在前奏中定义，允许您在此处明确声明它是输入的总和越来越小。递归调用小于输入，因为rec 是Access rec 的参数。
如果您想更详细地了解发生了什么，您可以尝试将 minusSmaller_1 和 minusSmaller_2 调用替换为空洞，看看您需要证明什么：
gcdt : Nat -> Nat -> Nat
gcdt m n with (sizeAccessible (m + n))
gcdt m Z | acc = m
gcdt Z n | acc = n
gcdt (S m) (S n) | (Access rec)
= if m > n
then gcdt (minus m n) (S n) | rec _ ?smaller1
else gcdt (S m) (minus n m) | rec _ ?smaller2
例如：
*gcd> :t smaller1
m : Nat
n : Nat
rec : (y : Nat) ->
LTE (S y) (S (plus m (S n))) -> Accessible Smaller y
--------------------------------------
smaller1 : LTE (S (plus (minus m n) (S n))) (S (plus m (S n)))
我不知道任何地方有详细记录 Accessible，至少对于 Idris（您可能会找到 Coq 的示例），但在 Data.List.Views、@987654339 中的 base 库中有更多示例@ 和Data.Nat.Views。
【讨论】：
仅供参考：idris 1.3.0（可能还有 1.2.0）中的实现是完全的，但使用 assert_total 函数来实现这一点。
:printdef gcd
gcd : (a : Nat) ->
(b : Nat) -> {auto ok : NotBothZero a b} -> Nat
gcd a 0 = a
gcd 0 b = b
gcd a (S b) = assert_total (gcd (S b)
(modNatNZ a (S b) SIsNotZ))
【讨论】：