We illustrate the encoding natural deduction in Liquid Haskell. It is a formed versions of § 3.3 of "Towards Complete Specification and Verification with SMT".
To use Liquid Haskell as a higher order theorem prover you need to enable the higherorder
flag (for efficiency it is off by default) and import the ProofCombinators
library.
We illustrate the mapping from natural deduction rules to typing rules in the below figure which uses typing judgments to express Gentzen’s proof of the proposition
ϕ ≡ (∃x.∀y.(p x y)) ⇒ (∀y.∃x.(p x y))
Read bottom-up, the derivation provides a proof of ϕ
. Read top-down, it constructs a proof of the formula as the term λe y.case e of {(x, ex ) → (x, ex y)}
. This proof term corresponds directly to the following Haskell expression that typechecks with type ϕ
.
The great benefit of using refinement types to encode natural deduction is that quantifier-free portions of the proof can get automated via SMTs. For every quantifier-free proposition ϕ
, you can convert between {ϕ}
, where ϕ
is treated as an SMT-proposition and ϕ
, where ϕ
is treated as a type; and this conversion goes both ways. For example, let ϕ ≡ p ∧ (q||r)
. Then flatten converts from ϕ
to {ϕ}
and expand the other way, while this conversion is SMT-aided.
Next, we construct the proof terms needed to prove two logical properties: that existentials distribute over disjunctions and foralls over conjunctions, i.e.
ϕ∃ ≡ (∃x.p x ∨ q x) ⇒ ((∃x.p x) ∨ (∃x.q x))
(1) ϕ∀ ≡ (∀x.p x ∧ q x) ⇒ ((∀x.p x) ∧ (∀x.q x))
(2)
The specification of these properties requires nesting quantifiers inside connectives and vice versa. The proof of ϕ∃
(1) proceeds by existential case splitting and introduction:
Dually, we prove ϕ∀
(2) via a λ-abstraction and case spitting inside the conjunction pair:
The above proof term corresponds to its natural deduction proof derivation but using SMT-aided verification can get simplified to the following
As ϕ
can describe properties of data types like lists, we can prove properties of such types, e.g. that for every list xs
, if there exists a list ys
such that xs == ys ++ ys
,then xs
has even length.
ϕ ≡ ∀xs.((∃ys. xs = ys ++ ys) ⇒ (∃n.length xs = n + n))
The proof (evenLen
) proceeds by existential elimination and introduction. and uses the lenAppend
lemma.
The lenAppend
lemma is proved by induction on the input list and PLE to automate equational reasoning.
Lists in the above proof are used defined inductive data types whose length
is decreasing at each recursive call.
(++)
is Haskell's usual append reflected in the logic.
Finally, we specify and verify induction on natural numbers:
ϕind ≡ (p 0 ∧ (∀n.p (n − 1) ⇒ p n) ⇒ ∀n.p n)
The proof proceeds by induction (e.g. case splitting). In the base case, n == 0
, the proof calls the left conjunct, which contains a proof of the base case. Otherwise, 0 < n
, the proof applies the induction hypothesis to the right conjunct instantiated at n-1
.