Докажите, что если string_is_prefix возвращает true, длина строки равна префиксу - PullRequest
Новая
       8

Докажите, что если string_is_prefix возвращает true, длина строки равна префиксу

0 голосов
/ 22 марта 2019

Я пытаюсь создать версию string_is_prefix, которая доказывает, что строка длиннее префикса, если она возвращает 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)))

Как я могу это сделатьдоказательство работы?

Ответы [ 2 ]

1 голос
/ 23 марта 2019

Если вы используете доказательство, вам нужен такой датапроп: 

dataprop
StringLen(int, int, bool) =
| {m,n:int} StringLenFalse(m, n, false)
| {m,n:int | m <= n} StringLenTrue(m, n, true)
1 голос
/ 23 марта 2019

Неправильный тип, который вы использовали.

Тип того, что вы хотите, можно указать следующим образом: 

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