证明如果 string_is_prefix returns 为真，则字符串的长度与前缀一样大

Question

我正在尝试创建 string_is_prefix 的一个版本，如果 returns 为真，则证明字符串比前缀长。这是我目前的代码：

#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(n54(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

如果使用证明，您需要如下所示的数据属性：

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

证明如果 string_is_prefix returns 为真，则字符串的长度与前缀一样大

Prove that if string_is_prefix returns true, then the string has a length as big as the prefix

ats