Natural Deduction on Liquid Haskell
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".
Prelude
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.
Natural Deduction as Type Derivation
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 ϕ.
SMT-aided proofs
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.
Distributing Quantifiers
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
Properties of User Defined Datatypes
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.
Induction on Natural Numbers
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.