为映射和函数定义满射谓词答案

【问题标题】：Defining a surjective predicate for maps and functions为映射和函数定义满射谓词
【发布时间】：2022-12-01 04:06:34
【问题描述】：

我在为映射和函数定义满射谓词时遇到了一些问题。

predicate isTotal<G(!new), B(!new)>(f:G -> B)
    reads f.reads;
{
     forall g:G :: f.requires(g)
}

predicate Surjective<A(!new), B(!new)>(f: A -> B) 
    requires isTotal(f)
{
    forall b: B :: exists a: A :: f(a) == b 
}

predicate isTotalMap<G(!new), B(!new)>(m:map<G,B>)
{
     forall g:G :: g in m
}

predicate mapSurjective<U(!new), V(!new)>(m: map<U,V>)
    requires forall u: U :: u in m.Keys
{
    forall x: V :: exists a: U :: m[a] == x
}

这些定义似乎有些作用。但是，他们无法验证以下设置。

datatype Color = Blue | Yellow | Green | Red

function toRed(x: Color): Color {
    Red
}

function shiftColor(x: Color): Color {
    match x {
        case Red => Blue
        case Blue => Yellow
        case Yellow => Green
        case Green => Red
    }
}

lemma TestSurjective() {
    assert isTotal(toRed);
    assert isTotal(shiftColor);
    var toRedm := map[Red := Red, Blue := Red, Yellow := Red, Green := Red];
    var toShiftm := map[Red := Blue, Blue := Yellow, Yellow := Green, Green := Red];
    // assert Surjective(toRed); //should fail
    // assert Surjective(shiftColor); //should succeed
    // assert mapSurjective(toRedm); //should fail
    // assert forall u: Color :: u in toShiftm.Keys;
    assert isTotalMap(toShiftm); //also fails
    assume forall u: Color :: u in toShiftm.Keys;
    assert mapSurjective(toShiftm); // should succeed
}

我假设地图不符合 mapSurjective 中定义的整体性要求的原因是因为地图可能是堆对象，而 Dafny 没有费心去跟踪其中的内容？即使我假设前提条件，即使它应该通过，谓词仍然失败。
对于功能案例assert Surjective(shiftColor) 也失败了。对于具有无限基数的类型，我可以理解它会失败，但我觉得应该可以评估有限类型。

【问题讨论】：

标签： dafny

【解决方案1】：

我想出了以下内容。对于地图，我定义了这两个引理。

lemma TotalColorMapIsTotal<B>(m: map<Color, B>) 
    requires m.Keys == {Red, Blue, Green, Yellow}
    // ensures forall u: Color :: u in m
    ensures isTotalMap(m)
{
    forall u: Color | true
        ensures u in m
    {
        if u.Red? {
            assert u in m;
        }
    }
}

lemma ColorMapIsOnto<A>(m: map<A, Color>) 
    requires m.Values == {Red, Blue, Green, Yellow}
    ensures forall u: Color :: u in m.Values
{

    forall u: Color | true
        ensures u in m.Values
    {
        if u.Red? {
            assert u in m.Values;
        }
    }
}

其中有一些断言，当应用于示例总图和满射图时已验证。

    assert toShiftm[Red] == Blue;
    assert toShiftm[Blue] == Yellow;
    assert toShiftm[Yellow] == Green;
    assert toShiftm[Green] == Red;

    TotalColorMapIsTotal(toShiftm);
    ColorMapIsOnto(toShiftm);
    assert mapSurjective(toShiftm);

当我为功能版本提供以下断言时，也进行了验证。

    assert shiftColor(Green) == Red;
    assert shiftColor(Red) == Blue;
    assert shiftColor(Blue) == Yellow;
    assert shiftColor(Yellow) == Green;
    assert Surjective(shiftColor); //should succeed

所以我猜他们工作，但感觉有点动力不足。这是可以做到的最好的吗？

【讨论】：