There are times when subtyping judgments are too difficult for f-star to figure out automatically, and f-star would like me to spell out my proofs in more detail. I am also running into cases where I would like to write a lemma that just proves f-star can make some type judgment.
A piece of syntax that looks like it does this does parse, but it seems to not do what I want. I suspect I misunderstand what this syntax does. Here I am trying to just prove that x has type nat with a Lemma. Why doesn't this do what I think it does?
let x: nat = 3
val tj_lem: unit -> Lemma (x: nat)
let tj_lem () = ()
I am also surprised that I can write "x: nat" in that position. How can I "prove that x is a nat" if I needed to?
You've hit an ugly corner of F*'s syntax. https://github.com/FStarLang/FStar/issues/1905 We've been discussing ways to improve it.
In particular, F* allows you to associate names with types that are in some cases meaningless. In your example the name x
is meaningless in the x:nat
that appears in the type of Lemma. It is interpreted by F* as unit -> Lemma nat
: this is the type of a proof that shows that the nat
type is inhabited … which isn't particularly interesting. For the record, one way to prove that uninteresting type is
let nat_is_inhabited () : Lemma nat = FStar.Squash.return_squash #nat 0
Now, to your actual question of how to spell out a proof of subtyping. There are many ways. One common way is as follows:
Let's say you have the type
let tp = x:t { p }
And at some point you have
let f (x:t) = … assert (q x); let y : tp = x in …
i.e., because of some contextual information that gives you the property q x
, you want to treat x:t
at the type tp
.
If you can prove a lemma of the form
val q_implies_p (x:t) : Lemma (requires q x) (ensures p x)
then by calling the lemma at the right point in your code, you can give F* and the SMT solver enough information to accept the subtyping of x:t
to tp
. For example, something like this:
let f (x:t) = … assert (q x); q_implies_p x; let y : tp = x in …
Hope that helps. Sorry about the confusing syntax!