Trying to understand detail about Lemmas from tutorial

[alex4482]

Hi, i was reading tutorial on the proving part, and there was something i did not fully understand about lemmas.

I understood the 'requires' and 'ensures' part, but, in that photo, why is the part encircled with red necessary.

I saw it in multiple Lemma examples, but i dont get why it has to recursively call itself and not directly return ( ), since, in this case at least, any input inevitably will reach the [ ] part.

[nikswamy]

Good question. That part you've highlighted is the proof of the lemma.

See this part of the tutorial for a similar example and an explanation for how proofs of this style work: http://fstar-lang.org/tutorial/book/part1/part1_lemmas.html#a-proof-by-induction-explained-in-detail

Summarizing:

• Yes, indeed, this function always returns a ().

• As such, the return value is not interesting at all. What is interesting is that property that F* can prove every time a call to this function returns. That property is the statement of the lemma and the way it proves the property is a proof by induction, i.e., in the base case, when the list is [], it can prove this property immediately without any further help. In the inductive case, by calling the function recursively on tl, we use the induction hypothesis to prove the property on the tail of the list, and from there, F* + Z3 can complete the proof for hd::tl.

• Another way to interpret your question: F* + Z3 can prove many things automatically, but they cannot do induction automatically. So, by writing this recursive function, one explicitly does the inductive part of the proof that cannot be done automatically.