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:

Exercise file

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)

Exercise file

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.

Exercise file

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|)
       )