# 5. Implementing Propositional Logic

## 5.1. Syntax

We have seen that the set of propositional formulas can be defined inductively, and we have seen that Lean makes it easy to specify inductively defined types. It’s a match made in heaven! Here is the definition of the type of propositional formulas that we will use in this course:

```
namespace hidden
inductive PropForm
| tr : PropForm
| fls : PropForm
| var : String → PropForm
| conj : PropForm → PropForm → PropForm
| disj : PropForm → PropForm → PropForm
| impl : PropForm → PropForm → PropForm
| neg : PropForm → PropForm
| biImpl : PropForm → PropForm → PropForm
deriving Repr, DecidableEq
end hidden
#print PropForm
open PropForm
#check (impl (conj (var "p") (var "q")) (var "r"))
```

You can find this example in the file `implementing_propositional_logic/examples.lean`

in the `User`

folder of the course repository.

The command `import LAMR.Util.Propositional`

at the top of the file
imports the part of the library with functions that we provide for you
to deal with propositional logic.
We will often put a copy of a definition from the library in an
examples file so you can experiment with it.
Here we have put it in a namespace called `hidden`

so that
our copy’s full name is `hidden.PropForm`

,
which won’t conflict with the one in the library.
Outside the `hidden`

namespace, the command `#print PropForm`

refers to the real one, that is, the one in the library.
The command `open PropForm`

means that we can write, for example,
`tr`

for the first constructor instead of `PropForm.tr`

.
Try writing some propositional formulas of your own.
There should be squiggly blue lines under the the `#print`

and `#check`

commands in VSCode,
indicating that there is Lean output associated with these.
You can see it by hovering over the commands,
or by moving the caret to the command and checking the
`Lean infoview`

window.

The phrase `deriving Repr, DecidableEq`

tells Lean to automatically
define functions to be used to test equality of two expressions
of type `PropForm`

and to display the result of an `#eval`

.
We’ll generally leave these out of the display from now on.
You an always use `#check`

and `#print`

to learn more about
a definition in the library. If you hold down `ctrl`

and click on an identifier,
the VSCode Lean extension will take you to the definition in the library.
Simply holding down `ctrl`

and hovering over it will show you the
definition in a pop-up window.
Try taking a look at the definition of `PropForm`

in the library.

Writing propositional formulas using constructors can be a pain in the neck. In the library, we have used Lean’s mechanisms for defining new syntax to implement nicer syntax.

```
#check prop!{p ∧ q → (r ∨ ¬ p) → q}
#check prop!{p ∧ q ∧ r → p}
def propExample := prop!{p ∧ q → r ∧ p ∨ ¬ s1 → s2 }
#print propExample
#eval propExample
#eval toString propExample
```

You can get the symbols by typing `\\and`

, `\\to`

, `\\or`

, `\\not`

, and `\\iff`

in VS Code. And, in general, when you see a symbol in VSCode,
hovering over it with the mouse shows you how to type it.
Once again, try typing some examples of your own.
The library defines the function `PropForm.toString`

that produces
a more readable version of a propositional formula,
one that, when inserted within the `prop!{...}`

brackets,
should produce the same result.

Because `PropForm`

is inductively defined, we can easily define
functions using structural recursion.

```
namespace PropForm
def complexity : PropForm → Nat
| var _ => 0
| tr => 0
| fls => 0
| neg A => complexity A + 1
| conj A B => complexity A + complexity B + 1
| disj A B => complexity A + complexity B + 1
| impl A B => complexity A + complexity B + 1
| biImpl A B => complexity A + complexity B + 1
def depth : PropForm → Nat
| var _ => 0
| tr => 0
| fls => 0
| neg A => depth A + 1
| conj A B => Nat.max (depth A) (depth B) + 1
| disj A B => Nat.max (depth A) (depth B) + 1
| impl A B => Nat.max (depth A) (depth B) + 1
| biImpl A B => Nat.max (depth A) (depth B) + 1
def vars : PropForm → List String
| var s => [s]
| tr => []
| fls => []
| neg A => vars A
| conj A B => (vars A).union' (vars B)
| disj A B => (vars A).union' (vars B)
| impl A B => (vars A).union' (vars B)
| biImpl A B => (vars A).union' (vars B)
#eval complexity propExample
#eval depth propExample
#eval vars propExample
end PropForm
#eval PropForm.complexity propExample
#eval propExample.complexity
```

`Mathlib`

defines a function `List.union`

that
returns the concatenation of the two lists with
duplicates removed, assuming that the original two lists had no duplicate elements.
Unfortunately, that function has quadratic complexity.
The file `LAMR/Util/Misc`

defines a more efficient version,
`List.union'`

, that uses hash sets.

## 5.2. Semantics

The course library defines the type `PropAssignment`

to be `List (String × Bool)`

.
If `v`

has type `PropAssignment`

, you should think of the expression `v.eval s`

as
assigning a truth value to the variable named `s`

.
The following function then evaluates the truth value of any propositional
formula under assignment `v`

:

```
def PropForm.eval (v : PropAssignment) : PropForm → Bool
| var s => v.eval s
| tr => true
| fls => false
| neg A => !(eval v A)
| conj A B => (eval v A) && (eval v B)
| disj A B => (eval v A) || (eval v B)
| impl A B => !(eval v A) || (eval v B)
| biImpl A B => (!(eval v A) || (eval v B)) && (!(eval v B) || (eval v A))
-- try it out
#eval let v := PropAssignment.mk [("p", true), ("q", true), ("r", true)]
propExample.eval v
```

The example at the end defines `v`

to be the assignment that
assigns the value `true`

to the strings `"p"`

, `"q"`

, and `"r"`

and false to all the others.
This is a reasonably convenient way to describe truth assignments manually,
so the library provides a function `PropAssignment.mk`

and notation `propassign!{...}`

to support that.

```
#check propassign!{p, q, r}
#eval propExample.eval propassign!{p, q, r}
```

You should think about how the next function manages to compute a list of all the sublists of a given list. It is analogous to the power set operation in set theory.

```
def allSublists : List α → List (List α)
| [] => [[]]
| (a :: as) =>
let recval := allSublists as
recval.map (a :: .) ++ recval
#eval allSublists propExample.vars
```

With that in hand, here is a function that computes the truth table of a
propositional formula.
The value of `truthTable A`

is a list of pairs:
the first element of the pair is the list of `true`

/`false`

values assigned
to the elements of `vars A`

, and the second element
is the truth value of `A`

under that assignment.

```
def truthTable (A : PropForm) : List (List Bool × Bool) :=
let vars := A.vars
let assignments := (allSublists vars).map (fun l => PropAssignment.mk (l.map (., true)))
let evalLine := fun v : PropAssignment => (vars.map v.eval, A.eval v)
assignments.map evalLine
#eval truthTable propExample
```

We can now use the list operation `List.all`

to test whether a formula is valid,
and we can use `List.some`

to test whether it is satisfiable.

```
def PropForm.isValid (A : PropForm) : Bool := List.all (truthTable A) Prod.snd
def PropForm.isSat(A : PropForm) : Bool := List.any (truthTable A) Prod.snd
#eval propExample.isValid
#eval propExample.isSat
```

## 5.3. Normal Forms

The library defines an inductive type of negation-normal form formulas:

```
inductive Lit
| tr : Lit
| fls : Lit
| pos : String → Lit
| neg : String → Lit
inductive NnfForm :=
| lit (l : Lit) : NnfForm
| conj (p q : NnfForm) : NnfForm
| disj (p q : NnfForm) : NnfForm
```

It is then straightforward to define the negation operation for formulas in negation normal form, and a translation from propositional formulas to formulas in negation normal form.

```
def Lit.negate : Lit → Lit
| tr => fls
| fls => tr
| pos s => neg s
| neg s => pos s
def NnfForm.neg : NnfForm → NnfForm
| lit l => lit l.negate
| conj p q => disj (neg p) (neg q)
| disj p q => conj (neg p) (neg q)
namespace PropForm
def toNnfForm : PropForm → NnfForm
| tr => NnfForm.lit Lit.tr
| fls => NnfForm.lit Lit.fls
| var n => NnfForm.lit (Lit.pos n)
| neg p => p.toNnfForm.neg
| conj p q => NnfForm.conj p.toNnfForm q.toNnfForm
| disj p q => NnfForm.disj p.toNnfForm q.toNnfForm
| impl p q => NnfForm.disj p.toNnfForm.neg q.toNnfForm
| biImpl p q => NnfForm.conj (NnfForm.disj p.toNnfForm.neg q.toNnfForm)
(NnfForm.disj q.toNnfForm.neg p.toNnfForm)
end PropForm
```

Putting the first in the namespace `NnfForm`

has the effect that given `A : NnfForm`

,
we can write `A.neg`

instead of `NnfForm.neg A`

.
Similarly, putting the second definition in the namespace `PropForm`

means we can write
`A.toNnfForm`

to put a propositional formula in negation normal form.

We can try them out on the example defined above:

```
#eval propExample.toNnfForm
#eval toString propExample.toNnfForm
```

To handle conjunctive normal form, the library defines a type `Lit`

of literals.
A `Clause`

is then a list of literals, and a `CnfForm`

is a list of clauses.

```
def Clause := List Lit
def CnfForm := List Clause
```

As usual, you can use `#check`

and `#print`

to find information about them, and ctrl-click
to see the definitions in the library.
Since, as usual, defining things using constructors can be annoying,
the library defines syntax for writing expressions of these types.

```
def exLit0 := lit!{ p }
def exLit1 := lit!{ -q }
#print exLit0
#print exLit1
def exClause0 := clause!{ p }
def exClause1 := clause!{ p -q r }
def exClause2 := clause!{ r -s }
#print exClause0
#print exClause1
#print exClause2
def exCnf0 := cnf!{
p,
-p q -r,
-p q
}
def exCnf1 := cnf!{
p -q,
p q,
-p -r,
-p r
}
def exCnf2 := cnf!{
p q,
-p,
-q
}
#print exCnf0
#print exCnf1
#print exCnf2
#eval toString exClause1
#eval toString exCnf2
```

Let us now consider what is needed to put an arbitrary propositional formula in
conjunctive normal form. In Section 4.5, we saw that the key
is to show that the disjunction of two CNF formulas is again CNF.
Lean’s library has a function `List.insert`

, which adds an element to a list;
if the element already appears in the list, it does nothing.
The file `LAMR/Util/Misc.lean`

defines a function `List.union'`

that forms the union of two lists;
if the original two lists have no duplicates, the union won’t either.
It also defines a function `List.Union`

which takes the union of a list of lists.
Since clauses are lists, we can use them on clauses:

```
#eval List.insert lit!{ r } exClause0
#eval exClause0.union' exClause1
#eval List.Union [exClause0, exClause1, exClause2]
```

We can now take the disjunction of a single clause and a CNF formula by taking
the union of the clause with each element of the CNF formula.
We can implement that with the function `List.map`

:

```
#eval exCnf1.map exClause0.union'
```

This applied the function “take the union with `exClause0`

” to each element of `exCnf1`

,
and returns the resulting list.
We can now define the disjunction of two CNF formulas by taking all the
clauses in the first,
taking the disjunction of each clause with the second CNF,
and then taking the union of all of those, corresponding to the conjunctions
of the CNFs. Here is the library definition, and an example:

```
def CnfForm.disj (cnf1 cnf2 : CnfForm) : CnfForm :=
(cnf1.map (fun cls => cnf2.map cls.union')).Union
#eval cnf!{p, q, u -v}.disj cnf!{r1 r2, s1 s2, t1 t2 t3}
#eval toString <| cnf!{p, q, u -v}.disj cnf!{r1 r2, s1 s2, t1 t2 t3}
```

Functional programmers like this sort of definition; it’s short, clever,
and inscrutable.
You should think about defining the disjunction of two CNF formulas by hand,
using recursions over clauses and CNF formulas.
Your solution will most likely reconstruct the effect of the instance `map`

and
`Union`

in the library definition,
and that will help you understand why they make sense.

In any case, with this in hand, it is easy to define the translation from negation normal form formulas and arbitrary propositional formulas to CNF.

```
def NnfForm.toCnfForm : NnfForm → CnfForm
| NnfForm.lit (Lit.pos s) => [ [Lit.pos s] ]
| NnfForm.lit (Lit.neg s) => [ [Lit.neg s] ]
| NnfForm.lit Lit.tr => []
| NnfForm.lit Lit.fls => [ [] ]
| NnfForm.conj A B => A.toCnfForm.conj B.toCnfForm
| NnfForm.disj A B => A.toCnfForm.disj B.toCnfForm
def PropForm.toCnfForm (A : PropForm) : CnfForm := A.toNnfForm.toCnfForm
```

We can try them out:

```
#eval propExample.toCnfForm
#eval prop!{(p1 ∧ p2) ∨ (q1 ∧ q2)}.toCnfForm.toString
#eval prop!{(p1 ∧ p2) ∨ (q1 ∧ q2) ∨ (r1 ∧ r2) ∨ (s1 ∧ s2)}.toCnfForm.toString
```

## 5.4. Exercises

Write a Lean function that, given any element of

`PropForm`

, outputs a list of all the subformulas.Write a function in Lean that implements substitution for propositional formulas, and test it on one or two examples.

Write a Lean function that, given a list of propositional formulas and another propositional formula, determines whether the second is a logical consequence of the first.

Write a Lean function that, given a clause, tests whether any literal

`Lit.pos p`

appears together with its negation`Lit.neg p`

. Write another Lean function that, given a formula in conjunctive normal form, deletes all these clauses.In Section 5.2, we defined a Lean function

`PropForm.eval`

that evaluates a propositional formula with respect to a truth assignment. Define a similar function,`CnfForm.eval`

, that evaluates a formula in conjunctive normal form. (Do it directly: don’t translate it to a propositional formula.)In Section 5.3, we defined a Lean data type

`NnfForm`

for NNF formulas, and we defined a function`PropForm.toNnfForm`

that converts a propositional formula to one in NNF. Notice that the method we used to expand \(\liff\) can lead to an exponential increase in length.Define a Lean data type

`EnnfForm`

for*extended*negation normal form formulas, which adds the \(\liff\) connective to ordinary NNF. Then define a function that translates any propositional formula to an extended NNF formula.