# Constructive & Classical Connectives

In an earlier chapter, we learned about the propositional connectives \(\forall, \exists, \Rightarrow, \iff, \wedge, \vee, \neg\), etc. Whereas in other logical frameworks these connectives are primitive, in a type theory like F* these connectives are defined notions, built from inductive type definitions and function types. In this section, we take a closer look at these logical connectives, show their definitions, and present some utilities to manipulate them in proofs.

Every logical connective comes in two flavors. First, in its most
primitive form, it is defined as an inductive or arrow type, giving a
constructive interpretation to the connective. Second, and more
commonly used in F*, is a *squashed*, or proof-irrelevant, variant of
the same connective—the squashed variant is classical rather than
constructive and its proofs are typically derived by writing partial
proof terms with the SMT filling in the missing parts.

Each connective has an *introduction* principle (which describes how
to build proofs of that connective) and an *elimination* principle
(which describes how to use a proof of that connective to build other
proofs). Example uses of introduction and elimination principles for
all the connectives can be found in ClassicalSugar.fst

All these types are defined in `Prims`

, the very first module in all
F* programs.

## Falsehood

The `empty`

inductive type is the proposition that has no
proofs. The logical consistency of F* depends on there being no closed
terms whose type is `empty`

.

```
type empty =
```

This definition might look odd at first: it defines an inductive type
with *zero* constructors. This is perfectly legal in F*, unlike in
languages like OCaml or F#.

The squashed variant of `empty`

is called `False`

and is defined
as shown below:

```
let False = squash empty
```

### Introduction

The `False`

proposition has no introduction form, since it has no proofs.

### Elimination

From a (hypothetical) proof of `False`

, one can build a proof of any
other type.

```
let empty_elim (#a:Type) (x:empty) : a = match x with
```

This body of `elim_false`

is a `match`

expression with no branches,
which suffices to match all the zero cases of the `empty`

type.

`FStar.Pervasives.false_elim`

provides an analogous elimination rule
for `False`

, as shown below, where the termination check for the
recursive call succeeds trivially in a context with `x:False`

.

```
let rec false_elim (#a:Type) (x:False) : a = false_elim x
```

## Truth

The `trivial`

inductive type has just a single proof, `T`

.

```
type trivial = T
```

Note

Although isomorphic to the `unit`

type with its single element
`()`

, for historic reasons, F* uses the `trivial`

type to
represent trivial proofs. In the future, it is likely that
`trivial`

will just be replaced by `unit`

.

The squashed form of `trivial`

is written `True`

and is defined as:

```
let True = squash trivial
```

### Introduction

The introduction forms for both the constructive and squashed variants are trivial.

```
let _ : trivial = T
let _ : True = ()
```

### Elimination

There is no elimination form, since proofs of `trivial`

are vacuous
and cannot be used to derive any other proofs.

## Conjunction

A constructive proof of `p`

and `q`

is just a pair containing
proofs of `p`

and `q`

, respectively.

```
type pair (p q:Type) = | Pair : _1:p -> _2:q -> pair p q
```

Note

This type is isomorphic to the tuple type `p & q`

that we
encountered previously here. F* currently
uses a separate type for pairs used in proofs and those used to
pair data, though there is no fundamental reason for this. In the
future, it is likely that `pair`

will just be replaced by the
regular tuple type.

The squashed form of conjunction is written `/\`

and is defined as
follows:

```
let ( /\ ) (p q:Type) = squash (pair p q)
```

### Introduction

Introducing a conjunction simply involves constructing a pair.

```
let and_intro #p #q (pf_p:p) (pf_q:q)
: pair p q
= Pair pf_p pf_q
```

To introduce the squashed version, there are two options. One can
either rely entirely on the SMT solver to discover a proof of ```
p /\
q
```

from proofs of `p`

and `q`

, which it is usually very capable
of doing.

```
let conj_intro #p #q (pf_p:squash p) (pf_q: squash q)
: Lemma (p /\ q)
= ()
```

Or, if one needs finer control, F* offers specialized syntax
(defined in `FStar.Classical.Sugar`

) to manipulate each of the
non-trivial logical connectives, as shown below.

```
let conj_intro_sugar #p #q (pf_p:squash p) (pf_q: squash q)
: squash (p /\ q)
= introduce p /\ q
with pf_p
and pf_q
```

The sugared introduction form for conjunction is, in general, as follows:

```
introduce p /\ q //Term whose top-level connective is /\
with proof_of_p //proof_of_p : squash p
and proof_of_q //proof_of_q : squash q
```

### Elimination

Eliminating a conjunction comes in two forms, corresponding to projecting each component of the pair.

```
let and_elim_1 #p #q (pf_pq:p & q)
: p
= pf_pq._1
let and_elim_2 #p #q (pf_pq:p & q)
: q
= pf_pq._2
```

For the squashed version, we again have two styles, the first relying on the SMT solver.

```
let conj_elim_1 #p #q (pf_pq:squash (p /\ q))
: squash p
= ()
let conj_elim_2 #p #q (pf_pq:squash (p /\ q))
: squash q
= ()
```

And a style using syntactic sugar:

```
let conj_elim_sugar_1 #p #q (pf_pq:squash (p /\ q))
: squash p
= eliminate p /\ q
returns p
with pf_p pf_q. pf_p
let conj_elim_sugar_2 #p #q (pf_pq:squash (p /\ q))
: squash p
= eliminate p /\ q
returns q
with pf_p pf_q. pf_q
```

## Disjunction

A constructive proof of `p`

or `q`

is represented by the following
inductive type:

```
type sum (p q:Type) =
| Left : p -> sum p q
| Right : q -> sum p q
```

The constructors `Left`

and `Right`

inject proofs of `p`

or
`q`

into a proof of `sum p q`

.

Note

Just like before, this type is isomorphic to the type `either p q`

from `FStar.Pervasives`

.

The classical connective `\/`

described previously is just a
squashed version of `sum`

.

```
let ( \/ ) (p q: Type) = squash (sum p q)
```

### Introduction

As with the other connectives, introducing a constructive disjunction
is just a matter of using the `Left`

or `Right`

constructor.

To introduce the squashed version `\/`

, one can either rely on the
SMT solver, as shown below.

```
let or_intro_left #p #q (pf_p:squash p)
: squash (p \/ q)
= ()
let or_intro_right #p #q (pf_q:squash q)
: squash (p \/ q)
= ()
```

Or, using the following syntactic sugar, one can specifically provide
a proof for either the `Left`

or `Right`

disjunct.

```
let or_intro_sugar_left #p #q (pf_p:squash p)
: squash (p \/ q)
= introduce p \/ q
with Left pf_p
let or_intro_sugar_right #p #q (pf_q:squash q)
: squash (p \/ q)
= introduce p \/ q
with Right pf_q
```

### Elimination

Eliminating a disjunction requires a *motive*, a goal proposition to
be derived from a proof of `sum p q`

or `p \/ q`

.

In constructive style, eliminating `sum p q`

amounts to just
pattern matching on the cases and constructing a proof of the goal
by applying a suitable goal-producing hypothesis.

```
let sum_elim #p #q #r (p_or_q: sum p q)
(pr: p -> r)
(qr: q -> r)
: r
= match p_or_q with
| Left p -> pr p
| Right q -> qr q
```

The squashed version is similar, except the case analysis can either be automated by SMT or explicitly handled using the syntactic sugar.

```
let or_elim #p #q #r (pf_p:squash (p \/ q))
(pf_pr:squash (p ==> r))
(pf_qr:squash (q ==> r))
: squash r
= ()
```

```
let or_elim_sugar #p #q #r
(pf_p:squash (p \/ q))
(pf_pr:unit -> Lemma (requires p) (ensures r))
(pf_qr:unit -> Lemma (requires q) (ensures r))
: squash r
= eliminate p \/ q
returns r
with pf_p. pf_pr () //pf_p : squash p
and pf_q. pf_qr () //pf_q : squash q
```

## Implication

One of the elimination principles for disjunction used the implication
connective `==>`

. Its definition is shown below:

```
let ( ==> ) (p q : Type) = squash (p -> q)
```

That is, `==>`

is just the squashed version of the non-dependent
arrow type `->`

.

Note

In `Prims`

, the definition of `p ==> q`

is actually ```
squash (p
-> GTot q)
```

, a **ghost** function from `p`

to `q`

. We’ll learn
about this more when we encounter effects.

### Introduction

Introducing a constructive arrow `p -> q`

just involves constructing
a \(\lambda\)-literal of the appropriate type.

One can turn several kinds of arrows into implications, as shown below.

One option is to directly use a function from the `FStar.Classical`

library, as shown below:

```
val impl_intro_tot (#p #q: Type) (f: (p -> q)) : (p ==> q)
```

However, this form is seldom used in F*. Instead, one often works with functions between squashed propositions, or Lemmas, turning them into implications when needed. We show a few styles below.

```
let implies_intro_1 #p #q (pq: squash p -> squash q)
: squash (p ==> q)
= introduce p ==> q
with pf_p. pq pf_p
let implies_intro_2 #p #q (pq: unit -> Lemma (requires p) (ensures q))
: squash (p ==> q)
= introduce p ==> q
with pf_p. pq pf_p
let implies_intro_3 #p #q (pq: unit -> Lemma (requires p) (ensures q))
: Lemma (p ==> q)
= introduce p ==> q
with pf_p. pq pf_p
```

Unlike the other connectives, there is no fully automated SMT-enabled way to turn an arrow type into an implication. Of course, the form shown above remains just sugar: it may be instructive to look at its desugaring, shown below.

```
let implies_intro_1 (#p #q:Type) (pq: (squash p -> squash q))
: squash (p ==> q)
= FStar.Classical.Sugar.implies_intro
p
(fun (_: squash p) -> q)
(fun (pf_p: squash p) -> pq pf_p)
```

`FStar.Squash`

and `FStar.Classical`

provide the basic building
blocks and the sugar packages it into a more convenient form for use.

### Elimination

Of course, the elimination form for a constructive implication, i.e.,
`p -> q`

is just function application.

```
let arrow_elim #p #q (f:p -> q) (x:p) : q = f x
```

The elimination rule for the squashed form is the classical logical
rule *modus ponens*, which is usually very well automated by SMT, as
shown in `implies_elim`

below. We also provide syntactic sugar for
it, for completeness, though it is seldom used in practice.

```
let implies_elim #p #q (pq:squash (p ==> q)) (pf_p: squash p)
: squash q
= ()
let implies_elim_sugar #p #q (pq:squash (p ==> q)) (pf_p: squash p)
: squash q
= eliminate p ==> q
with pf_p
```

## Negation

Negation is just a special case of implication.

In its constructive form, it corresponds to `p -> empty`

.

In `Prims`

, we define `~p`

as `p ==> False`

.

Being just an abbreviation for an implication to `False`

, negation
has no particular introduction or elimination forms of its
own. However, the following forms are easily derivable.

### Introduction (Exercise)

Prove the following introduction rule for negation:

```
val neg_intro #p (f:squash p -> squash False)
: squash (~p)
```

**Answer**

```
let neg_intro #p (f:squash p -> squash False)
: squash (~p)
= introduce p ==> False
with pf_p. f pf_p
```

### Elimination (Exercise)

Prove the following elimination rule for negation using the sugar rather than just SMT only.

```
val neg_elim #p #q (f:squash (~p)) (x:unit -> Lemma p)
: squash (~q)
```

**Answer**

```
let neg_elim #p #q (f:squash (~p)) (lem:unit -> Lemma p)
: squash q
= eliminate p ==> False
with lem()
```

## Universal Quantification

Whereas implication is represented by the non-dependent arrow ```
p ->
q
```

, universal quantification corresponds to the dependent arrow ```
x:t
-> q x
```

. Its classical form in `forall (x:t). q x`

, and is defined
in as shown below:

```
let ( forall ) #t (q:t -> Type) = squash (x:t -> q x)
```

Note

As with `==>`

, in `Prims`

uses `x:t -> GTot (q x)`

, a ghost
arrow, though the difference is not yet significant.

### Introduction

Introducing a dependent function type `x:t -> p x`

is just like
introducing a non-dependent one: use a lambda literal.

For the squashed form, F* provides sugar for use with several styles,
where names corresponding to each of the `forall`

-bound variables on
the `introduce`

line are in scope for the proof term on the `with`

line.

```
let forall_intro_1 (#t:Type)
(#q:t -> Type)
(f : (x:t -> squash (q x)))
: squash (forall (x:t). q x)
= introduce forall (x:t). q x
with f x
let forall_intro_2 (#t:Type)
(#q:t -> Type)
(f : (x:t -> Lemma (q x)))
: squash (forall (x:t). q x)
= introduce forall (x:t). q x
with f x
let forall_intro_3 (#t0:Type)
(#t1:t0 -> Type)
(#q: (x0:t0 -> x1:t1 x0 -> Type))
(f : (x0:t0 -> x1:t1 x0 -> Lemma (q x0 x1)))
: squash (forall (x0:t0) (x1:t1 x0). q x0 x1)
= introduce forall (x0:t0) (x1:t1 x0). q x0 x1
with f x0 x1
```

Note, as `forall_intro_3`

shows, the sugar also works for `forall`

quantifiers of arities greater than 1.

### Elimination

Eliminating a dependent function corresponds to dependent function application.

```
let dep_arrow_elim #t #q (f:(x:t -> q x)) (x:t) : q x = f x
```

For the squashed version, eliminating a `forall`

quantifier amounts
to instantiating the quantifier for a given term. Automating proofs
that require quantifier instantiation is a large topic in its own
right, as we’ll cover in a later section—this wiki page
provides some hints.

Often, eliminating a universal quantifier is automated by the SMT
solver, as shown below, where the SMT solver easily instantiates the
quantified hypothesis `f`

with `a`

.

```
let forall_elim_1 (#t:Type)
(#q:t -> Type)
(f : squash (forall (x:t). q x))
(a:t)
: squash (q a)
= ()
```

But, F* also provides syntactic sugar to explicitly trigger quantifier
insantiation (as shown below), where the terms provided on the
`with`

line are instantiations for each of the binders on the
`eliminate`

line.

```
let forall_elim_2 (#t0:Type)
(#t1:t0 -> Type)
(#q: (x0:t0 -> x1:t1 x0 -> Type))
(f : squash (forall x0 x1. q x0 x1))
(v0: t0)
(v1: t1 v0)
: squash (q v0 v1)
= eliminate forall x0 x1. q x0 x1
with v0 v1
```

Its desugaring may be illuminating:

```
FStar.Classical.Sugar.forall_elim
#(t1 v0)
#(fun x1 -> q v0 x1)
v1
(FStar.Classical.Sugar.forall_elim
#t0
#(fun x0 -> forall (x1: t1 x0). q x0 x1)
v0
())
```

## Existential Quantification

Finally, we come to existential quantification. Its constructive form
is a dependent pair, a dependent version of the pair used to represent
conjunctions. The following inductive type is defined in `Prims`

.

```
type dtuple2 (a:Type) (b: a -> Type) =
| Mkdtuple2 : x:a -> y:b x -> dtuple2 a b
```

As with `tuple2`

, F* offers specialized syntax for `dtuple2`

:

Instead of

`dtuple2 a (fun (x:a) -> b x)`

, one writes`x:a & b x`

.Instead of writing

`Mkdtuple2 x y`

, one writes`(| x, y |)`

.

The existential quantifier `exists (x:t). p x`

is a squashed version
of the dependent pair:

```
let ( exists ) (#a:Type) (#b:a -> Type) = squash (x:a & b x)
```

### Introduction

Introducing a constructive proof of `x:a & b x`

is just a question
of using the constructor—we show a concrete instance below.

```
let dtuple2_intro (x:int) (y:int { y > x })
: (a:int & b:int{b > a})
= (| x, y |)
```

For the squashed version, introducing an `exists (x:t). p x`

automatically using the SMT solver requires finding an instance `a`

for the quantifier such that `p a`

is derivable—this is the dual
problem of quantifier instantiation mentioned with universal

In the first example below, the SMT solver finds the instantiation and proof automatically, while in the latter two, the user picks which instantiation and proof to provide.

```
let exists_intro_1 (#t:Type)
(#q:t -> Type)
(a:t) (b:t)
(f : squash (q a /\ q b))
: squash (exists x. q x)
= () //instantiation found by SMT, it chose a or b, unclear/irrelevant which
let exists_intro_2 (#t:Type)
(#q:t -> Type)
(a:t) (b:t)
(f : squash (q a))
(g : squash (q b))
: squash (exists x. q x)
= introduce exists x. q x
with a //witness
and f //proof term of q applied to witness
let exists_intro_3 (#t:Type)
(#q:t -> Type)
(a:t) (b:t)
(f : squash (q a /\ q b))
: squash (exists x. q x)
= introduce exists x. q x
with a
and f // f: squash (q a /\ q b) implicitly eliminated to squash (q a) by SMT
```

### Elimination

Just as with disjunction and conjunction, eliminating `dtuple2`

or
`exists`

requires a motive, a goal proposition that *does not
mention* the bound variable of the quantifier.

For constructive proofs, this is just a pattern match:

```
let dtuple2_elim (#t:Type) (#p:t -> Type) (#q:Type)
(pf: (x:t & p x))
(k : (x:t -> p x -> q))
: q
= let (| x, pf_p |) = pf in
k x pf_p
```

For the `exists`

, the following sugar provides an elimination
principle:

```
let exists_elim (#t:Type) (#p:t -> Type) (#q:Type)
(pf: squash (exists (x:t). p x))
(k : (x:t -> squash (p x) -> squash q))
: squash q
= eliminate exists (x:t). p x
returns q
with pf_p. k x pf_p
let exists_elim_alt (#t:Type) (#p:t -> Type) (#q:Type)
(pf: squash (exists (x:t). p x))
(k : (x:t -> Lemma (requires p x)
(ensures q)))
: Lemma q
= eliminate exists (x:t). p x
returns q
with pf_p. k x
```

Names corresponding to the binders on the `eliminate`

line are in
scope in the `with`

line, which additionally binds a name for a
proof term corresponding to the body of the existential formula. That
is, in the examples above, `x:t`

is implicitly in scope for the proof
term, while `pf_p: squash p`

.

### Exercise

In a previous exercise, we defined a function to insert an element in a Merkle tree and had it return a new root hash and an updated Merkle tree. Our solution had the following signature:

```
type mtree' (n:nat) =
| MTree : h:hash_t -> mtree n h -> mtree' n
val update_mtree' (#h:hash_t)
(rid:resource_id)
(res:resource)
(tree:mtree (L.length rid) h)
: mtree' (L.length rid)
```

Revise the solution so that it instead returns a dependent
pair. `dtuple2`

is already defined in `Prims`

, so you don’t have
to define it again.

**Answer**

```
let rec update #h
(rid:resource_id)
(res:resource)
(tree:mtree (L.length rid) h)
: Tot (h':_ & mtree (L.length rid) h')
(decreases rid)
= match rid with
| [] -> (| _, L res |)
| hd :: rid' ->
if hd
then (
let (| _, t |) = update rid' res (N?.left tree) in
(| _, N t (N?.right tree) |)
)
else (
let (| _, t |) = update rid' res (N?.right tree) in
(| _, N (N?.left tree) t|)
)
```