Lemmas / proofs about subtyping judgments

Question

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?

Answer 1

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!