基于Dafny实现互质数线性组合GCD引理证明的技术问询

• 核心目标：证明给定两个互质的正整数a和b，存在整数x、y使得1 = ax + by。已从KRML 279复制GCD实现，需编写引理GcdLinearCombination，确保Gcd(a,b)可表示为a、b的线性组合。
• 证明思路参考：采用教材中的标准方法——利用无限集，断言其中最小元d是a、b的线性组合且为GCD，再通过除法余数推导矛盾完成证明，需确认该思路能否在Dafny中实现。
• 当前遇到的问题：已定义有限组合集combinationSet和无限组合集icombinationSet，尝试通过良序原理断言无限集中存在最小元d，但实现无限集的iMin函数时，因无限集大小未递减导致验证失败，询问是否需要自定义公理或有其他可行的推导机制。

引理框架 #

lemma GcdLinearCombination(a: pos, b: pos)
    ensures exists x,y :: Gcd(a,b) == a*x+b*y
{

组合集定义 #

function combinationSet(a: pos, b: pos): set<pos> 
{
    set x: nat,y: nat | 0 <= x <= a && 0 <= y <= b && a*x+b*y > 0 :: a*x+b*y
}

function icombinationSet(a: pos, b: pos): iset<pos> 
{
    iset x: nat,y: nat | a*x+b*y > 0 :: a*x+b*y
}

无限集最小元函数实现 #

function iMin(s: iset<pos>): pos
    requires s != iset{}
    ensures forall x | x in s :: iMin(s) in s && iMin(s) <= x
{
    var x :| x in s;
    if s == iset{x} then
        x
    else
        var y := iMin(s - iset{x}); //infinite set size is not decreasing as expected
        assert forall z | z in s :: z == x || (z in (s - iset{x}) && y <= z);
        if x < y then x else y
}

内容的提问来源于stack exchange，提问作者Hath995