Skip to content

Sugar for manipulating connectives in classical logic

Jump to bottom Edit New page
Théophile Wallez edited this page Aug 10, 2022 · 8 revisions

Table of contents

Introduction

Working directly with FStar.Squash and FStar.Classical is tedious. Instead, F* provides syntactic sugar to manipulate the five main connectives used in the classical logic fragment of F*. These connectives are:

  1. forall
  2. exists
  3. implies
  4. and
  5. or

The syntactic sugar encapsulates the main proof rules for these connectives. As is traditional, the proof rules for each connective come in two flavors.

  • Introduction rules: These are rules that allow you to prove a formula beginning with a given connective. Sugar for the introduction rules begin with the introduce keyword. The rough syntactic form of an introduction rule is
introduce <some formula>
with <some arguments>
and <some more arguments or proof terms>

The shape of the rule varies depending on the head constructor of the introduced formula.

  • Elimination rules: These are rules that allow you to make use of an already proven formula of a given connective, and to derive another formula from it. Sugar for the elimination rules begin with the eliminate keyword.

The rough syntactic form of an elimination rule is

eliminate <some formula>
returns <some other formula>
with <some arguments>
and <some more arguments or proof terms>

Again, the shape of the rule varies depending on the head constructor of the eliminated formula.

See this file for examples.

Universal quantifier: forall

Universally quantified formulas have the shape forall x1...xn. p.

This formula is itself sugar for a more basic type defined in prims.fst.

forall (x:t). p = squash (x:t -> GTot (p x))

That is, a forall x. p is a squashed ghost function, returning a proof of p x for every x.

However, proving forall x. t by directly building a term of this type, while possible, is very cumbersome. This is particularly true when quantifying over multiple arguments. For instance, forall x y. p would be squash (x:t -> GTot (squash (y:t' -> GTot (p x y))).

Likewise, given a proof of forall x. p x, apply it to a particular v and obtaining p v is also cumbersome.

Instead of building these proof terms directly, a typical usage in F* is to rely on the SMT solver to reason with this connective. However, one often needs more control. For the most precise control one can use a tactic, though that requires a different level of expertise. The sugar described below is a middle ground---it allows one to more carefully control how these connectives are manipulated, while still staying within F* rather than stepping to the meta level with a tactic.

Introducing a universal quantifier

Given a lemma proving x:a -> y:b -> z:c -> squash (p x y z), one can turn it into a squash (forall x y z. p x y z) by doing:

let test_forall_intro_1 #a #b #c (p: a -> b -> c -> Type)
                      (f:(x:a -> y:b -> z:c -> squash (p x y z)))
  : squash (forall x y z. p x y z)
  = introduce forall x y z. p x y z
         with f x y z

Alternatively, working only with Lemma rather than squash (which is often more idiomatic), one can write:

let test_forall_intro_2 #a #b #c (p: a -> b -> c -> Type)
                      (f:(x:a -> y:b -> z:c -> Lemma (p x y z)))
  : Lemma (forall x y z. p x y z)
  = introduce forall x y z. p x y z
        with f x y z

In the syntax

introduce forall x1 .. xn. p
with proof

The binders x1...xn are in scope for both p and proof, where proof : squash p or, equivalently, proof : Lemma p.

How it is desugared

You can mostly ignore this, but in case you're wondering how this sugar is implemented, in fstar-mode.el, the emacs mode, you can inspect a term after it has been desugared (using C-c C-s C-p). For test_forall_intro_2 the desugaring is:

  let  test_forall_intro_2  : 
      p: (_: a -> _: b -> _: c -> Prims.Tot Type0) ->
      f: (x: a -> y: b -> z: c -> FStar.Pervasives.Lemma (ensures p x y z))
    -> FStar.Pervasives.Lemma (ensures forall (x: a) (y: b) (z: c). p x y z) = fun p f ->
    FStar.Classical.Sugar.forall_intro a
      (fun x -> forall (y: b) (z: c). p x y z)
      (fun x ->
          FStar.Classical.Sugar.forall_intro b
            (fun y -> forall (z: c). p x y z)
            (fun y ->
                FStar.Classical.Sugar.forall_intro c
                  (fun z -> p x y z)
                  (fun z -> f x y z <: Prims.squash (p x y z))))

Eliminating a universal quantifier

Eliminating a universal quantifier amounts to applying it to some specific arguments. Using SMT alone, the default way to instantiate such quantifiers is by relying on SMT patterns and triggers. To directly instantiate a quantifier, one can use the syntax below.

let test_elim_forall_2 (p: nat -> nat -> Type)
  : Lemma 
    (requires forall x y. p x y)
    (ensures p 0 1)
  = eliminate forall x y. p x y
    with 0 1

The general form is

eliminate forall x1...xn. p
with v1...vn

The x1..xn are in scope for p only. The instantiations v1..vn must have the same length as the binders x1..xn. In a context where forall x1...xn.p is provable, this piece of syntax proves p[v1..vn/x1..xn].

Existential quantifiers: exists

The existential quantifier exists (x:t). p is defined in prims.fst as squash (x:t & p x), i.e., a squashed dependent pair of a witness x:t and proof of p x. As with forall, working with this directly, especially the n-ary version is painful---one can rely on the SMT solver or tactics to work with exists, but again, the sugar below provides a lighter option.

Introducing an existential quantifier

If you have a proof of p va vb vc, you can turn it into exists x y z. p x y z using this syntax:

let test_exists_intro_1 #a #b #c (p: a -> b -> c -> Type) va vb vc
                        (f:squash (p va vb vc))
  : squash (exists x y z. p x y z)
  = introduce exists x y z. p x y z
    with va vb vc
    and f

The general form is

introduce exists x1 .. xn. p
with v1 .. vn
and proof
  • where the x1..xn are in scope for p only
  • v1..vn are instantiations for all the x1..xn
  • and proof establishes p [v1..vn/x1..xn], i.e., it is a proof of p with the x1..xn instantiated with v1..vn.

Eliminating an existential quantifier

To eliminate an existential formula and prove something else from it, you often need to "get your hands on" the witness. However, for soundness, one must also ensure that the witness does not escape its scope. Consider the following:

Suppose you have a binary predicate p with a lemma proving that it is transitive. And suppose you know that exists y. p x y /\ p y z. To apply the lemma and prove p x z, one needs access to the witness y. The syntax below helps:

let test_elim_exists_1 (p:nat -> nat -> Type)
                       (trans: (x:nat -> y:nat -> z:nat -> 
                                Lemma (requires p x y /\ p y z)
                                      (ensures p x z)))
                       (x z:nat)
  : Lemma
    (requires
      (exists y. p x y /\ p y z))
    (ensures
      p x z)
  = eliminate exists y. p x y /\ p y z
    returns p x z
    with _. trans x y z

The general form of eliminate for existential formulas is as follows:

eliminate exists x1 ... xn. p
returns q
with p_pf. proof

Here, x1..xn are in scope of p and proof, only. Additional p_pf is a binder whose type is squash p and is also in scope of proof. And proof is expected to prove q, i.e., proof : Lemma q or, equivalently, proof : squash q Importantly, the binders x1..xn are not in scope for q.

You may wonder why we have the additional binder p_pf. Sometimes, it can be convenient to have access to the proof term of p, as shown in this variant below that works with squash terms rather than Lemma. If you don't need the proof of p, you can always just use _ as its name, as shown in the first example above.

let test_elim_exists_2 p x z
                       (_:squash (exists y. p x y /\ p y z))
                       (trans : (#x:_ -> #y:_ -> #z:_ -> squash (p x y /\ p y z) -> squash (p x z)))
  : squash (p x z)
  = eliminate exists (y:nat).
         p x y /\ p y z
    returns p x z
    with pf. trans pf

Implications: ==>

In prims.fst, the formula p ==> q is defined as squash (p -> GTot q).

Introducing an implication

To turn a Lemma into an implication, one can write:

let test_implies_intro_2 p q (f: unit -> Lemma (requires p) (ensures q))
  : Lemma (p ==> q)
  = introduce p ==> q
    with _. f ()

The same syntax also works with squashed proofs.

let test_implies_intro_1 p q (f: squash p -> squash q)
  : squash (p ==> q)
  = introduce p ==> q
    with x. f x

The general form is

introduce p ==> q
with x. proof

where x:squash p and is in scope of proof : squash q.

Eliminating an implication

Conversely, eliminating an implication is the classic modus ponens rule of propositional logic. This rule is usually very well automated by the SMT solver, so it is unlikely that you would need to use the syntax described below very much. However, it is included for completeness.

You can write:

let test_elim_implies_1 p q (_:squash (p ==> q)) (x:squash p)
 : Tot (squash q)
  = eliminate p ==> q
    with x

let test_elim_implies_2 p q (f: unit -> Lemma p)
  : Lemma (requires (p ==> q))
          (ensures q)
  = eliminate p ==> q
    with f()

The general form is

eliminate p ==> q
with proof

where proof : squash p and the entire term proves squash q.

Disjunctions: \/

In prims.fst, p \/ q is defined as squash (c_or p q) where

type c_or p q =
 | Left : p -> c_or p q
 | Right : q -> c_or p q

That is, p \/ q is a squashed version of a constructor proof c_or p q.

Given a proof of p \/ q it is often convenient to "case analyze" it, to prove some goal conditionally on whether p holds or q holds. That is, the elimination form of p \/ q is quite useful. The introduction form is included for completeness, but is likely less useful, since it is well-automated by SMT.

Introducing a disjunction

let test_or_intro_left_1 p q (f: squash p)
  : squash (p \/ q)
  = introduce p \/ q
    with Left f

let test_or_intro_right_2 p q (f: unit -> Lemma q)
  : squash (p \/ q)
  = introduce p \/ q
    with Right (f())

The general form is

introduce p \/ q
with [Left | Right] proof

where when used with Left we check that proof : squash p, otherwise proof : squash q.

Eliminating a disjunction

Given p \/ q one can derive r if both p ==> r and q ==> r. The following syntax illustrates this:

let test_elim_or_2 p q r 
                   (f: unit -> Lemma (requires p) (ensures r))
                   (g: unit -> Lemma (requires q) (ensures r))                   
  : Lemma (requires p \/ q)
          (ensures r)
  = eliminate p \/ q
    returns r
    with _p. f ()
    and  _q. g ()

The general form is

eliminate p \/ q
returns r
with pf_p. proof1
and  pf_q. proof2

where

  • pf_p : squash p is in scope of proof1 : squash r
  • pf_q: squash q is in scope of proof2 : squash r

As in the case of eliminate exists, the proof terms can be bound to _ if not needed.

Conjunctions: /\

In prims.fst, p /\ q is defined as squash (c_and p q) where type c_and p q = And : p -> q -> c_and p q. I.e., it is squashed pair of proofs of p and q respectively.

Introducing a conjunction

let test_and_intro_1 p q (f:squash p) (g:squash q)
  : squash (p /\ q)
  = introduce p /\ q
    with f
    and g

The general form is

introduce p /\ q
with f
and g

where f : squash p and g : squash q.

Eliminating a conjunction

To eliminate a conjunction p /\ q, one derives a formula r from separate proofs of p and q.

let test_elim_and_2 p q r (f: squash p -> squash q -> Lemma r)
  : Lemma 
    (requires p /\ q)
    (ensures r)
  = eliminate p /\ q
    returns r
    with pf_p pf_q. f pf_p pf_q

The general form is

eliminate p /\ q
    returns r
    with pf_p pf_q. proof

where pf_p: squash p and pf_q: squash q and proof : squash r

Derived forms

Excluded middle

The disjunction squash (p \/ ~p) is directly provable in SMT for any p. To make use of this in a proof (e.g., a proof by contradiction), one can eliminate as shown below, using the elimination form for disjunctions. This provides a way to simulate a "case analysis" of any proposition.

let test_excluded_middle p r 
                   (f: unit -> Lemma (requires p) (ensures r))
                   (g: unit -> Lemma (requires ~p) (ensures r))                   
  : Lemma r
  = eliminate p \/ ~p
    returns r
    with _. f ()
    and  _. g ()

Proving a quantified implication

It's quite common to want to turn a lemma of the form x:t -> Lemma (requires p) (ensures q) into a quantified implication forall x. p ==> q. To do that, one can combine the introduction rule for universal quantifiers and implications, as shown below.

let test_forall_implies a (p:a -> Type) (q:a -> Type) (f: (x:a -> squash (p x) -> squash (q x)))
  : squash (forall x. p x ==> q x)
  = introduce forall x. p x ==> q x
    with introduce p x ==> q x
         with px. (
           f x px
         )

Note, however, that the sugar is integrated with F*'s type inference, so you can leave holes like _ and let F* infer the instantiations.

So, you could also write


let test_forall_implies_2_1 a (p:a -> Type) (q:a -> Type) (f: (x:a -> Lemma (requires p x) (ensures q x)))
  : Lemma (forall x. p x ==> q x)
  = introduce forall x. p x ==> q x
    with introduce _ ==> _
         with _. (
           assert (p x); //the asserts are optional, just here to show that any kind of proof term is legal here
           f x;
           assert (q x)
         )
Add a custom footer
Add a custom sidebar
Clone this wiki locally