Леммы / доказательства о суждениях подтипов

Question

Бывают случаи, когда суждения о подтипах слишком сложны для автоматического определения f-star, и f-star хотела бы, чтобы я изложил свои доказательства более подробно. Я также сталкиваюсь со случаями, когда я хотел бы написать лемму, которая просто доказывает, что f-star может сделать какое-то суждение о типе. делай что хочу Я подозреваю, что неправильно понимаю, что делает этот синтаксис. Здесь я пытаюсь просто доказать, что x имеет тип nat с леммой. Почему это не делает то, что я думаю?

let x: nat = 3
val tj_lem: unit -> Lemma (x: nat)
let tj_lem () = ()

Я также удивлен, что могу написать «x: nat» в этой позиции. Как я могу «доказать, что x - это nat», если мне нужно?

Answer 1

Вы попали в ужасный угол синтаксиса F *. https://github.com/FStarLang/FStar/issues/1905 Мы обсуждали способы его улучшения.

В частности, F * позволяет связывать имена с типами, которые в некоторых случаях не имеют смысла. В вашем примере имя x не имеет смысла в x:nat, который встречается в типе леммы. Он интерпретируется F * как unit -> Lemma nat: это тип доказательства, показывающего, что тип nat заселен ... что не особенно интересно. Для справки, один из способов доказать, что неинтересный тип - это

let nat_is_inhabited () : Lemma nat = FStar.Squash.return_squash #nat 0

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

Допустим, у вас есть тип

let tp = x:t { p }

И в какой-то момент у вас есть

let f (x:t) = … assert (q x); let y : tp = x in …  

, т. Е. Из-за некоторой контекстной информации который дает вам свойство q x, которое вы хотите обработать x:t по типу tp.

Если вы можете доказать лемму вида

val q_implies_p (x:t) : Lemma (requires q x) (ensures p x)

, тогда позвоните лемма в нужной точке вашего кода, вы можете дать F * и SMT solver достаточно информации, чтобы принять подтип от x:t до tp. Например, что-то вроде этого:

let f (x:t) = … assert (q x); q_implies_p x; let y : tp = x in …  

Надеюсь, это поможет. Извините за запутанный синтаксис!