# FStar.Classical

``````module FStar.Classical
``````

This module contains the standard primitives to manipulate proof goals containing classical logic. The proof goals manipulated are values of type `Type` or `Type0`. One can go from a goal of type `Type` to `Type0` by “squashing” it into an F* value of type unit having a refinmnent corresponding to the original goal.

To produce a value of type `squash a`, the general method is to let-bind a unit value and annotate it with the type `squash a`, for instance:

``````let pf : squash (1 <> 0) = () in ...
``````

The F* typechecker will then proceed to proved the squashed property by typechecking the squashed value. To apply most of the lemmas here, you will have to let-bind or create auxiliary lemmas matching what the function expects to make F*’s unification mechanism work

## Witnesses

#### give_witness

Demonstrate the existence of a type from a value of that type.

``````val give_witness (#a:Type) (_:a) : Lemma (ensures a)
``````

Example:

``````let x : n:nat{n <> 0} = 1 in
give_witness x
``````

#### give_witness_from_squash

Demonstrate the existence of a type from a squashed value. See `give_witness`.

``````val give_witness_from_squash (#a:Type) (_:squash a) : Lemma (ensures a)
``````

Example:

``````let pf : squash(1+1 = 2) = () in
give_witness pf
``````

#### get_equality

Produce equality as a `Type` if provable from context.

``````val get_equality
(#t:Type)
(a b: t)
: Pure (a == b)
(requires (a == b))
(ensures (fun _ -> True))
``````

#### get_forall

Produce a `forall` property as a `Type` if provable from context.

``````val get_forall
(#a:Type)
(p: a -> GTot Type0)
: Pure (forall (x: a). p x)
(requires (forall (x: a). p x))
(ensures (fun _ -> True))
``````

#### impl_to_arrow

Get an arrow from an implication. Converse is `arrow_to_impl`.

``````val impl_to_arrow (#a:Type0) (#b:Type0) (_:(a ==> b)) (_:squash a) :GTot (squash b)
``````

#### arrow_to_impl

Get an implication from an arrow. Converse is `impl_to_arrow`.

``````val arrow_to_impl (#a:Type0) (#b:Type0) (_:(squash a -> GTot (squash b))) : GTot (a ==> b)
``````

Example:

``````arrow_to_impl #(foo) #(bar) (fun _ ->
// proof of "bar", but now we have "foo" in context
)
``````

can be used to prove `foo ==> bar`.

## Universal quantification

#### gtot_to_lemma

Introduce a property `p x` from a `GTot` function.

``````val gtot_to_lemma (#a:Type) (#p:(a -> GTot Type)) (\$_:(x:a -> GTot (p x))) (x:a) : Lemma (p x)
``````

#### lemma_to_squash_gtot

Produce a squashed property as a `Type` from a lemma.

``````val lemma_to_squash_gtot
(#a:Type)
(#p:(a -> GTot Type))
(\$_:(x:a -> Lemma (p x)))
(x:a)
: GTot (squash (p x))
``````

The following values are all variations on a same theme: proving a proposition `p` true for all `x` of type `a`.

#### forall_intro_gtot

Produce `forall` property as a `Type` from a `GTot` function. See `lemma_forall_intro_gtot`.

``````val forall_intro_gtot
(#a:Type)
(#p:(a -> GTot Type))
(\$_:(x:a -> GTot (p x)))
: Tot (squash (forall (x:a). p x))
``````

#### lemma_forall_intro_gtot

Introduce a `forall` property into context from a `GTot` function.

``````val lemma_forall_intro_gtot
(#a:Type)
(#p:(a -> GTot Type))
(\$_:(x:a -> GTot (p x)))
: Lemma (forall (x:a). p x)
``````

#### forall_intro_squash_gtot

Produce a squashed `forall` property as a `Type` from a `GTot` function. See `forall_intro_squash_gtot_join`.

``````val forall_intro_squash_gtot
(#a:Type)
(#p:(a -> GTot Type))
(\$_:(x:a -> GTot (squash (p x))))
: Tot (squash (forall (x:a). p x))
``````

Produce a `forall` property as a `Type` from a `GTot` function.

This one seems more generally useful than the one above

``````val forall_intro_squash_gtot_join
(#a:Type)
(#p:(a -> GTot Type))
(\$_:(x:a -> GTot (squash (p x))))
: Tot (forall (x:a). p x)
``````

#### forall_intro

Introduce a `forall` property into context from a lemma. See relevant useful `move_requires` to make this even more useful.

``````val forall_intro (#a:Type) (#p:(a -> GTot Type)) (\$_:(x:a -> Lemma (p x))) : Lemma (forall (x:a). p x)
``````

Example:

``````let aux x : Lemma (p x) =
// proof of `p x`
in
forall_intro aux // and now we have `forall x. p x`
``````

Example:

``````let aux x : Lemma (requires (p x)) (ensures (q x)) =
// proof of `q x` under assumption of `q x`
in
forall_intro (move_requires aux) // and now we have `forall x. p x ==> q x`
``````

#### forall_intro_with_pat

Introduce a `forall` property with a pattern. See `forall_intro`.

``````val forall_intro_with_pat (#a:Type) (#c: (x:a -> Type)) (#p:(x:a -> GTot Type0))
(\$pat: (x:a -> Tot (c x)))
(\$_: (x:a -> Lemma (p x)))
: Lemma (forall (x:a).{:pattern (pat x)} p x)
``````

#### forall_intro_sub

Introduce a `forall` property. Equivalent to `forall_intro` except for lack of exact unification requirement `\$`.

``````val forall_intro_sub (#a:Type) (#p:(a -> GTot Type)) (_:(x:a -> Lemma (p x))) : Lemma (forall (x:a). p x)
``````

#### forall_intro_2

Introduce a `forall` property over 2 variables. Similar to `forall_intro`.

``````val forall_intro_2
(#a:Type)
(#b:(a -> Type))
(#p:(x:a -> b x -> GTot Type0))
(\$_: (x:a -> y:b x -> Lemma (p x y)))
: Lemma (forall (x:a) (y:b x). p x y)
``````

Example: A useful way to use it with a lemma that has a non-trivial `requires` clause:

``````let aux x y : Lemma (requires (p x y)) (ensures (q x y)) =
// proof of `q x y` under assumption of `p x y`
in
let aux x = move_requires (aux x) in // notice only 1 argument (last argument is pointfree)
forall_intro aux // and now we have `forall x. p x y ==> q x y`
``````

#### forall_intro_2_with_pat

`forall_intro_2` with pattern.

``````val forall_intro_2_with_pat
(#a:Type)
(#b:(a -> Type))
(#c: (x:a -> y:b x -> Type))
(#p:(x:a -> b x -> GTot Type0))
(\$pat: (x:a -> y:b x -> Tot (c x y)))
(\$_: (x:a -> y:b x -> Lemma (p x y)))
: Lemma (forall (x:a) (y:b x).{:pattern (pat x y)} p x y)
``````

#### forall_intro_3

`forall_intro` for 3 variables.

``````val forall_intro_3
(#a:Type)
(#b:(a -> Type))
(#c:(x:a -> y:b x -> Type))
(#p:(x:a -> y:b x -> z:c x y -> Type0))
(\$_: (x:a -> y:b x -> z:c x y -> Lemma (p x y z)))
: Lemma (forall (x:a) (y:b x) (z:c x y). p x y z)
``````

Example: Similar to `forall_intro_2`, we can use it for non-trivial `requires` clauses:

``````let aux x y z : Lemma (requires (p x y z)) (ensures (q x y z)) =
// proof of `q x y z` under assumption of `p x y z`
in
let aux x y = move_requires (aux x y) in
// notice only 2 arguments (last argument is pointfree)
forall_intro aux // and now we have `forall x. p x y z ==> q x y z`
``````

#### forall_intro_3_with_pat

`forall_intro_3` with pattern.

``````val forall_intro_3_with_pat
(#a:Type)
(#b:(a -> Type))
(#c: (x:a -> y:b x -> Type))
(#d: (x:a -> y:b x -> z:c x y -> Type))
(#p:(x:a -> y:b x -> z:c x y -> GTot Type0))
(\$pat: (x:a -> y:b x -> z:c x y -> Tot (d x y z)))
(\$_: (x:a -> y:b x -> z:c x y -> Lemma (p x y z)))
: Lemma (forall (x:a) (y:b x) (z:c x y).{:pattern (pat x y z)} p x y z)
``````

#### forall_intro_4

`forall_intro` for 4 variables.

``````val forall_intro_4
(#a:Type)
(#b:(a -> Type))
(#c:(x:a -> y:b x -> Type))
(#d:(x:a -> y:b x -> z:c x y -> Type))
(#p:(x:a -> y:b x -> z:c x y -> w:d x y z -> Type0))
(\$_: (x:a -> y:b x -> z:c x y -> w:d x y z -> Lemma (p x y z w)))
: Lemma (forall (x:a) (y:b x) (z:c x y) (w:d x y z). p x y z w)
``````

## Existential quantification

#### exists_intro

Introduce `exists x. p x`, given `p` and a `witness`.

``````val exists_intro (#a:Type) (p:(a -> Type)) (witness:a)
: Lemma (requires (p witness)) (ensures (exists (x:a). p x))
``````

#### forall_to_exists

Given a lemma `x:_ -> (p x ==> r)`, show that `(exists x. p x) ==> r`.

``````val forall_to_exists (#a:Type) (#p:(a -> Type)) (#r:Type) (\$_:(x:a -> Lemma (p x ==> r)))
: Lemma ((exists (x:a). p x) ==> r)
``````

#### forall_to_exists_2

`forall_to_exists` for two variables.

``````val forall_to_exists_2 (#a:Type) (#p:(a -> Type)) (#b:Type) (#q:(b -> Type)) (#r:Type)
(\$f:(x:a -> y:b -> Lemma ((p x /\ q y) ==> r)))
: Lemma (((exists (x:a). p x) /\ (exists (y:b). q y)) ==> r)
``````

#### exists_elim

Introduce a (scoped) witness of an existential.

``````val exists_elim (goal:Type) (#a:Type) (#p:(a -> Type)) (_:squash (exists (x:a). p x))
(_:(x:a{p x} -> GTot (squash goal))) : Lemma goal
``````

Example:

``````// if `exists x. p x` is in context, and we are proving `goal`
exists_elim goal (fun (x:_{p x}) ->
// we now have a witness `x` in context here that we can use to prove `goal`
)
``````

## Implications

The two next functions introduce implications in the context. Since they expect `Type0`, you have to provide them squashed values. For instance:

``````let aux (_ : squash p) : Lemma q = ... in
impl_intro aux
``````

#### impl_intro_gtot

Introduce an implication using a `GTot` function. `arrow_to_impl` without explicit squash.

``````val impl_intro_gtot (#p:Type0) (#q:Type0) (\$_:p -> GTot q) : GTot (p ==> q)
``````

#### impl_intro

Introduce an implication using a lemma.

``````val impl_intro (#p:Type0) (#q:Type0) (\$_: p -> Lemma q) : Lemma (p ==> q)
``````

#### move_requires

Convert a requires/ensures lemma into an implication lemma.

``````val move_requires
(#a:Type)
(#p:a -> Type)
(#q:a -> Type)
(\$_:(x:a -> Lemma (requires (p x)) (ensures (q x)))) (x:a)
: Lemma (p x ==> q x)
``````

Note: Works only on lemmas with a single argument, but can be made to work with lemmas with more arguments by using the following “trick”:

If we have ```FStar val foo x y z : Lemma (requires (p x y z)) (ensures (q x y z)) ``` and want ```FStar val bar x y z : Lemma (p x y z ==> q x y z) ``` then we can simply use ```FStar let bar x y z = move_requires (foo x y) z

``````
#### impl_intro_gen

A generative version of [`impl_intro`](#impl_intro).

```FStar
val impl_intro_gen (#p:Type0) (#q:squash p -> Tot Type0) (_:squash p -> Lemma (q ()))
: Lemma (p ==> q ())
``````

#### forall_impl_intro

Both `impl_intro` and `forall_intro` at once.

``````val forall_impl_intro
(#a:Type)
(#p:(a -> GTot Type))
(#q:(a -> GTot Type))
(\$_:(x:a -> (squash(p x)) -> Lemma (q x)))
: Lemma (forall x. p x ==> q x)
``````

#### ghost_lemma

Given a `Ghost unit` function with pre/post conditions, convert it into a lemma with `forall` and implication.

``````val ghost_lemma (#a:Type) (#p:(a -> GTot Type0)) (#q:(a -> unit -> GTot Type0))
(\$_:(x:a -> Ghost unit (p x) (q x)))
: Lemma (forall (x:a). p x ==> q x ())
``````

## Disjunctions

#### or_elim

Eliminate a disjunction. Useful for splitting proof of goal under two assumptions separately.

``````val or_elim (#l #r:Type0) (#goal:(squash (l \/ r) -> Tot Type0))
(hl:squash l -> Lemma (goal ()))
(hr:squash r -> Lemma (goal ()))
: Lemma ((l \/ r) ==> goal ())
``````

Example:

``````// assuming we want to prove `goal` under `l \/ r`.
let goal (_ : squash (l \/ r)) = ... in
or_elim #l #r #goal
(fun _ ->
// prove `goal` assuming `l`
)
(fun _ ->
// prove `goal` assuming `r`
)
// and now we've proven `goal` under `l \/ r`.
``````

Example:

``````// assuming we want to prove `goal`.
or_elim #_ #_ #(fun () -> goal)
(fun (_:squash p) ->
// prove `goal` assuming `p`
)
(fun (_:squash (~p)) ->
// prove `goal` assuming `~p`
)
// and now we've proven `goal`.
``````

#### excluded_middle

Introduce `p \/ ~p` – a classic of classical logic.

``````val excluded_middle (p:Type) :Lemma (requires (True)) (ensures (p \/ ~p))
``````