ats

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


I'm trying to create a version of string_is_prefix that prove that a string is longer than the prefix if it returns true. Here's the code I have so far:

#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
}

Unfortunately, the call to func(string) does not compile as if this proof was not working:

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

How can I make this proof work?


Solution

  • The type you used is incorrect.

    The type for what you want can be given as follows:

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