代码之家 › 专栏 › 技术社区 › Attila Karoly

如何解决FStar中的这种类型冲突?

fstar

0

Attila Karoly · 技术社区 · 4 年前

下面是一个简单的模式生成器,它返回 1:nat lemma_1 证明了生成的任意长度的表的每个位置都有一个1。这个 lng 争论 nth_1 必须被介绍,否则 n n:nat{n < length lst} 导致类型与 不 引理1 n:nat{n < lng} . 如果没有额外的参数,这个问题怎么解决?

val length: list 'a -> nat
let rec length lst = 
match lst with
  | [] -> 0
  | _ :: t -> 1 + length t

val nth_1 : lst: list nat {length lst > 0} -> (lng: nat) -> n: nat {n < lng} -> nat
let rec nth_1 lst lng n =
  match lst with
  | [h] -> h
  | h :: t -> if n = 0 then h else nth_1 t (lng - 1) (n - 1)

val gen_1 : lng: nat {lng > 0} -> list nat
let rec gen_1 lng =
match lng with 
  | 1 -> [1]
  | _ -> 1 :: gen_1 (lng - 1)

let rec lemma_1 (lng: nat {lng > 0}) (n: nat {n < lng})  : Lemma ((nth_1 (gen_1 lng) lng n) = 1) =
match n with
  | 0 -> ()
  | _ -> lemma_1 (lng - 1) (n - 1)

问题似乎与 gen_1 图案长度不能为零。有没有更好的方法来表达这个标准?

0 回复 | 直到 4 年前

1

Aseem Rastogi 4 年前

以下是避免额外参数的一种方法(请参阅内联注释):

module Test

val length: list Î± â â
let rec length lst =
match lst with
  | [] â 0
  | _ â¸¬ t â 1 + length t

//the refinement on n is not really necessary here, the proofs work even without it
//because as soon as we have [h], irrespective of the value of n, we return h
val nth_1 : lst: list â {length lst > 0} â n: â{n < length lst} â â
let rec nth_1 lst n =
  match lst with
  | [h] â h
  | h â¸¬ t â if n = 0 then h else nth_1 t (n - 1)

//refine the return type to say that it returns a list of length lng
val gen_1 : lng: pos â (l:list â{length l == lng})
let rec gen_1 lng =
match lng with
  | 1 â [1]
  | _ â 1 â¸¬ gen_1 (lng - 1)

let rec lemma_1 (lng: pos) (n: â {n < lng})  : Lemma ((nth_1 (gen_1 lng) n) = 1) =
match n with
  | 0 â ()
  | _ â lemma_1 (lng - 1) (n - 1)