Dafny如何证明映射归纳？同构字符串验证引理解析

我针对同构字符串问题，基于以下TypeScript实现编写了Dafny规范。核心思路是给每个字符分配首次出现的序号，若两个字符串经过该转换后的序列等价，则判定为同构——我将其理解为存在从s到t的单射映射。

function isIsomorphic(s: string, t: string): boolean {

    let sMap = new Map<string, number>();
    let sTransform: number[] = [];
    let tMap = new Map<string, number>();
    let tTransform: number[] = [];
    
    let sIndex = 1;
    let tIndex = 1;
    if(s.length != t.length) return false
    
    for(let i = 0; i < s.length; i++) {
        if(!sMap.has(s[i])) {
            sMap.set(s[i], sIndex++);
        }
        sTransform.push(sMap.get(s[i])); 
    }
    
    for(let i = 0; i < t.length; i++) {
        if(!tMap.has(t[i])) {
            tMap.set(t[i], tIndex++);
        }
        tTransform.push(tMap.get(t[i])); 
    }
    
    return sTransform.every((elem, index) => elem == tTransform[index]);
};

我的验证目标是把直觉明确化、形式化，彻底理解这个解法。目前规范已通过验证，但因为Dafny的归纳能力很强，我还没完全理清其中逻辑，感觉没有充分证明想要形式化的关系。

Dafny辅助函数 #

predicate InjectiveMap<T,U>(f: map<T, U>)
{
    forall x, y :: x in f && y in f && x != y ==> f[x] != f[y]
}

// 将映射应用到序列
function method aps<T,U>(s: seq<T>, smap: map<T,U>): seq<U>
    requires forall x :: x in s ==> x in smap
{
    seq(|s|, i requires 0 <= i < |s| => smap[s[i]])
}


function intsLessThan(n: nat): set<nat>
    ensures intsLessThan(n) == set x | 0 <= x < n
{
    if n == 0 then {} else {n-1} + intsLessThan(n-1)
}

function createMap(lmap: map<char,nat>, rmap: map<char, nat>): map<char, char>
    requires InjectiveMap(lmap)
    requires InjectiveMap(rmap)
    requires rmap.Values == lmap.Values
    ensures forall x :: x in lmap ==> x in createMap(lmap, rmap)
    ensures InjectiveMap(createMap(lmap, rmap))
{
    map xs : char | xs in lmap :: injectiveMapHasKey(rmap, lmap[xs]); var rkey :| rkey in rmap && rmap[rkey] == lmap[xs]; rkey
}

lemma injectiveMapHasKey<T,U>(lmap: map<T, U>, value: U)
    requires InjectiveMap(lmap)
    requires value in lmap.Values
    ensures exists t :: t in lmap && lmap[t] == value
{

}

Dafny主方法 #

当前实现仅断言：若返回true，则存在描述两字符串同构的隐式映射，但我认为这应该是双向条件，却不确定如何证明。

method isIsomorphic(s: string, t: string) returns (answer: bool) 
    requires 1 <= |s|
    requires |t| == |s|
    // ensures answer ==> exists fn: (char) -> char :: Injective(fn) && forall i :: 1 <= i < |s| <= |t| ==> fn(s[i]) == t[i]
    ensures answer ==> exists fn: map<char,char> :: InjectiveMap(fn) && forall i :: 1 <= i < |s| <= |t| ==> s[i] in fn && fn[s[i]] == t[i]
{
    var sMap: map<char, nat> := map[];
    var sTransform: seq<nat> := [];

    var tMap: map<char, nat> := map[];
    var tTransform: seq<nat> := [];

    var sIndex: nat := 0;
    // ghost var gsIndex: nat := 0;
    ghost var sIndices: set<nat> := {};
    var tIndex: nat := 0;
    for i := 0 to |s| 
        invariant forall j :: 0 <= j < i ==> s[j] in sMap
        invariant sIndices == intsLessThan(sIndex)
        invariant sIndex == |sMap|
        invariant sMap.Values == sIndices
        invariant InjectiveMap(sMap)
        invariant sTransform == aps(s[0..i], sMap)
    {
        if s[i] !in sMap {
            ghost var oldsMap := sMap;
            assert sIndex !in sIndices;
            assert sIndex !in sMap.Values;
            sMap := sMap[s[i] := sIndex];
            assert sMap == oldsMap + map[s[i] := sIndex];

            // assert forall z :: z in sMap && z != s[i] ==> sMap[z] != sIndex;
            sIndices := sIndices + {sIndex};
            assert sIndex in sMap.Values && sIndex in sIndices;
            sIndex := sIndex + 1;
        }
        sTransform := sTransform + [sMap[s[i]]];
    }
    
    ghost var tIndices: set<nat> := {};
    for i := 0 to |t| 
        invariant forall j :: 0 <= j < i ==> t[j] in tMap
        invariant tIndices == intsLessThan(tIndex)
        invariant tIndex == |tMap|
        invariant tMap.Values == tIndices
        invariant InjectiveMap(tMap)
        invariant tTransform == aps(t[0..i], tMap)
    {
        if t[i] !in tMap {
            ghost var tOld := tMap;
            assert tIndex !in tIndices;
            assert tIndex !in tMap.Values;
            tMap := tMap[(t[i]) := tIndex];
            assert tMap == tOld + map[t[i] := tIndex];
            tIndices := tIndices + {tIndex};
            assert tIndex in tMap.Values && tIndex in tIndices;
            tIndex := tIndex + 1;
        }
        tTransform := tTransform + [tMap[t[i]]];
    }
    assert sTransform == aps(s, sMap);
    assert tTransform == aps(t, tMap);
    if sMap.Values == tMap.Values && sTransform == tTransform {
        injectiveMapCanBeMade(sMap, tMap, s, t, sTransform, tTransform);
        return true;
    }else{
        return false;
    }
}

核心疑问 #

我的疑问集中在引理部分，尤其是createMapHasAllTheValues。为了证明第一个字符串的映射与第二个字符串的映射的复合可以将s映射为t，我本以为需要更明确地建立s、t与其转换版本smapped、tmapped之间的关系，以此证明对s[i]应用复合映射等于t[i]——毕竟createMap的后置条件里并没有直接断言任何关于s[i]或t[i]位置值的内容。

请问：

1. 该引理实际是在对什么进行归纳？
2. 为什么断言smapped[i] == tmapped[i]就能推导出createMap(lmap, rmap)[s[i]] == t[i]？

lemma injectiveMapCanBeMade(lmap: map<char,nat>, rmap: map<char, nat>, s: string, t: string, smapped: seq<nat>, tmapped: seq<nat>)
    requires InjectiveMap(lmap)
    requires InjectiveMap(rmap)
    requires rmap.Values == lmap.Values
    requires |s| == |t| && |s| >= 1
    requires forall i :: 0 <= i < |s| ==> s[i] in lmap
    requires forall i :: 0 <= i < |t| ==> t[i] in rmap
    requires smapped == aps(s, lmap)
    requires tmapped == aps(t, rmap)
    requires smapped == tmapped
    ensures exists fn: map<char,char> :: InjectiveMap(fn) && forall i :: 1 <= i < |s| <= |t| ==> s[i] in fn && fn[s[i]] == t[i]
{
    var fn := createMap(lmap, rmap);
    assert InjectiveMap(fn);
    createMapHasAllTheValues(lmap, rmap, s, t, smapped, tmapped);
}

lemma createMapHasAllTheValues(lmap: map<char,nat>, rmap: map<char, nat>, s: string, t: string, smapped: seq<nat>, tmapped: seq<nat>)
    requires InjectiveMap(lmap)
    requires InjectiveMap(rmap)
    requires forall j :: 0 <= j < |s| ==> s[j] in lmap
    requires forall j :: 0 <= j < |t| ==> t[j] in rmap
    requires smapped == aps(s, lmap)
    requires tmapped == aps(t, rmap)
    requires smapped == tmapped
    requires rmap.Values == lmap.Values
    ensures createMap(lmap, rmap).Values == rmap.Keys
    ensures forall i :: 0 <= i < |s| ==> createMap(lmap, rmap)[s[i]] == t[i]
{
    var test_map := createMap(lmap, rmap);
    assert createMap(lmap, rmap).Keys == lmap.Keys;
    forall x | x in rmap.Keys 
        ensures x in createMap(lmap, rmap).Values
    {
        assert rmap[x] in lmap.Values;
    }

    forall i | 0 <= i < |s|
        ensures createMap(lmap, rmap)[s[i]] == t[i]
    {
        // Why/How does the following prove the ensure?
        assert smapped[i] == tmapped[i];
    }

}

补充说明：我刚注意到，该方法实际上应断言存在两个映射（一个从s到t，另一个从t到s），才能真正证明存在同构。

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