I have just started learning F*, going through the tutorial. One of the exercises there is to prove that the reverse function on lists is injective.
Since this follows from the fact that involutions are injective I would like to express that fact as a lemma in F*. To do that I define
let is_involutive f = forall x. (f (f x) == x)
let is_injective f = forall x y. (f x == f y) ==> x == y
Is this the right way to define the notion of f being involutive or injective in F*?
Then I state the lemma
val inv_is_inj: #a:eqtype -> a -> f:(a->a) ->
Lemma (requires (is_involutive f)) (ensures(is_injective f))
Informally the proof can be written as
{ fix (x:a) (y:a)
assume (f x == f y)
then have (f (f x) == f (f y))
with (is_involutive f) have (x == y)
} hence (forall (x:a) (y:a). f x == f y ==> x == y)
then have (is_injective f)
How do I express such proof in F*?
In general, what F* language constructs can be used to prove statements of the form forall (x:a). phi x, where phi is a predicate on a type a?