请证明，如果String_is_prefix返回true，则字符串的长度与前缀一样大

Question

我正在尝试创建一个string_is_prefix的版本，该版本证明字符串返回true（如果返回true）长。这是我到目前为止的代码：

#include "share/atspre_staload.hats"
dataprop StringLen(bool) =
    | LessThan(false)
    | {m,n:nat | m >= n} GreaterThanEqual(true)
fun string_is_prefix {m, n: nat} (string_prefix: string(m), string: string(n)): [b:bool] (StringLen(b) | bool(b)) =
    let val prefix_len = string_length(string_prefix)
        val string_len = string_length(string)
        fun is_prefix {i: nat | m <= n; i < m} (index: size_t(i)): [b:bool] bool(b) =
            let val equal = g1ofg0(string_get_at(string, index) = string_get_at(string_prefix, index))
            in
                if index + 1 >= prefix_len then
                    equal
                else
                    equal * is_prefix(index + 1)
            end
    in
        if prefix_len > string_len then
            (LessThan() | false)
        else if prefix_len > 0 then
            let val result = is_prefix(i2sz(0))
            in
                if result then
                    (GreaterThanEqual{n, m}() | result)
                else
                    (LessThan() | result)
            end
        else
            (GreaterThanEqual{n, m}() | true)
    end
fun func(string: stringGte(1)) =
    ()
implement main0(argc, argv) = {
    val prefix_string: string(1) = "t"
    val string: [n:nat] string(n) = g1ofg0(argv[0])
    val (pf | is_prefix) = string_is_prefix(prefix_string, string)
    val () =
        if is_prefix then
            let prval GreaterThanEqual{n, m}() = pf
            in
                func(string)
            end
}

不幸的是，对func(string)的呼叫不会汇编，好像此证明不起作用：

unsolved constraint: C3NSTRprop(C3TKmain(); S2Eapp(S2Ecst(>=); S2EVar(5277->S2Evar(n$8654(14309))), S2Eintinf(1)))

如何使此证明工作？

Answer 1

您使用的类型不正确。

可以给出的类型如下：

extern
fun
string_is_prefix
{m,n: nat}
( prfix: string(m)
, strng: string(n)): [b:bool | ~b || m <= n ] bool(b)

Answer 2

如果使用证明，则需要一个数据plop，如以下一个：

dataprop
StringLen(int, int, bool) =
| {m,n:int} StringLenFalse(m, n, false)
| {m,n:int | m <= n} StringLenTrue(m, n, true)