Embedding Display Calculi

into Logical Frameworks

Jeremy Dawson  Rajeev Goré

Automated Reasoning Group and Dept. of Computer Science Australian National University Canberra, Australia

jeremy@arp.anu.edu.au     rpg@arp.anu.edu.au

Dawson supported by Australian Research Council Small & Large Grants

Goré supported by an Australian Research Council QEII Fellowship

Introduction

• Display logic is a modular proof-theoretic framework using sequents

• it admits a general cut-elimination proof • used for many undecidable substructural

logics, so need interactive prover

• want to use existing theorem provers

• want to use syntactic proof-theoretic methods, not semantic embeddings

• we discuss and compare three mechanisations

Display Logic

• Display logic is a generalised Gentzen formulation due to Nuel Belnap

• We consider the particular display calculus δRA for relation algebra

• Structural connectives: I ∗ • , ;

• Structure (where φ is a formula):

X ::= φ | I | ∗X | •X | X, X | X; X

• Sequent: X ⊢ Y where X, Y are structures

• There is a single cut-elimination theorem applying to all display calculi (modulo conditions on the rules), our aim is to mechanise its proof

Display Logic Rules

• These two rules p ⊢ p \frac{X ⊢ φ φ ⊢ Y}{X ⊢ Y}

• Display postulates, can move structures around

(can display any substructure)

\frac{X, Y ⊢ Z}{Y ⊢ ∗X, Z} (dp) \frac{∗X ⊢ Y}{∗Y ⊢ X} (dp)

• Structural rules, give properties of logic

\frac{X, X ⊢ Z}{X ⊢ Z} (contr) \frac{X, Y ⊢ Z}{Y, X ⊢ Z} (comm)

• Logical introduction rules (left and right)

\frac{X ⊢ A, B}{X ⊢ A ∨ B} (⊢ ∨) \frac{A ⊢ X B ⊢ Y}{A ∨ B ⊢ X, Y} (∨ ⊢)

Formula introduced is always displayed

Isabelle/Pure implementation

• Isabelle’s meta-logic is intuitionistic (higherorder) logic

• User can supply own object-logic, or use one supplied

• Facilitates natural-deduction style proofs, can program combinations of proof steps

• To embed sequent system, use sequent (not formula) as top object language construct

• \frac{A ⊢ X B ⊢ Y}{A ∨ B ⊢ X, Y} [| ?A |- $?X; ?B |- $?Y |] ==>

                   ?A v ?B |- $?X, $?Y

• This is a shallow embedding - we can do derivations, but can’t prove things about them

The Curry-Howard Isomorphism

• Type theory rules correspond to intuitionistic logic rules.

• note: Natural Deduction style, ⊢ is type context (not sequent calculus or δRA)

• type A ⇝ proposition A

• t : A ⇝ t “is” proof of proposition A

\begin{matrix}\frac{f : A → B a : A}{f(a) : B} & \frac{π[A] : A → B ρ : A}{π[A := ρ] : B} \\ \frac{Γ, v : A ⊢ e : B}{Γ ⊢ λv.e : A → B} & \frac{π : A ⊢ ρ[π] : B}{⊢ ρ[π := A] : A → B} \end{matrix}

Dependent Types

• A type can be a function of a term – eg curried printf

• We can use this in two ways – firstly, quantifier logic

• I ={individuals}, for i ∈ I, let A(i) be a type (dependent on i)

• Function ρ, domain I, ρ(i) : A(i)

• With expressions as proofs, ρ(i) is a proof of A(i)

• ρ is a recipe for proving any A(i), ie ρ is a proof of ∀iA(i)

A Second Use of Dependent

Types

• F ={formulae}, for f ∈ F, let P (f) be a type, representing derivations of formula f

• Rule \frac{A → B A}{B} is (an object of) the type P (a → b) → P (a) → P (b) (a, b variables)

• f : P (a) → P (c) gives f′ : P (a) → P (b) → P (c), so rule \frac{A}{C} gives rule \frac{A B}{C}

• similarly contraction, exchange

• We use ⊢ (binary infix) for P

The Twelf Implementation

Twelf – a system based on Dependent Types

1 str :  type.
2 |- :  str -> str -> type.  %infix none 10 |-.
3 * :  str -> str.  %prefix 200 *.
4 % Display postulates
5 sA : (* X |- Y) -> (* Y |- X).
6 sS : (X |- * Y) -> (Y |- * X).
7 % Derived structural rules
8 ssASl = [D] sA (sS D).

      % (X |- * * Y) -> (* * X |- Y)

Lines 5,6 are \frac{∗X ⊢ Y}{∗Y ⊢ X} (sA) \frac{X ⊢ ∗Y}{Y ⊢ ∗X} (sS)

Line 8 means λD.sA(sSD), rule \frac{X ⊢ ∗ ∗ Y}{∗ ∗ X ⊢ Y}

{deriv of \atop U ⊢ ∗ ∗ V} ⟶^{sS} {deriv of \atop ∗V ⊢ ∗U} ⟶^{sA} {deriv of \atop ∗ ∗ U ⊢ V}

Twelf – Conclusions

• typechecker good for building proofs

• but no programmable proof search

• theorem prover under extensive development, workings not documented

Isabelle/CTT implementation

• Constructive Type Theory, has dependent types, similar to Twelf

• Isabelle tactics can be used – not all suitable

• more tactics can be programmed – ML programmability valuable

Some type rules

strT  "str type"
seqT  "[| A : str ; B : str |] ==> A |- B type"
stT   "X : str ==> * X : str"

CTT – Recording Proofs

Record of proof comes automatically

goal dkt.thy "[| X : str ; Y : str |] ==>
  ?P : ( * * X |- Y) --> ( X |- * * Y)"

Next step uses rule

\frac{A type  f : A → B  g : B → C}{f oo g : A → C}

?g oo ?f : * * X |- Y --> X |- * * Y
 1. * * X |- Y type
 2. ?f : * * X |- Y --> ?B
 3. ?g : ?B --> X |- * * Y
Using sA : * ?X |- ?Y --> * ?Y |- ?X
sS : ?X |- * ?Y --> ?Y |- * ?X
sS oo sA : * * X |- Y --> X |- * * Y
 1. * * X |- Y type

Dependent Types – Conclusions

• Attraction was to get derivations modelled for free

• Term representing derivation – can be built up automatically

– cannot freely place or manipulate it • can’t express arbitrary properties of deriva-

tion

• need an even “deeper” embedding

The Isabelle/HOL

implementation

• based on Church’s higher-order logic, has logical and functional language constructs

• deep embedding, we can look at the shape, content of sequents, derivations in the logical framework (not just by writing ML code)

datatype structr = Comma structr structr
| SemiC structr structr
| Star structr
| Blob structr
...
| Structform formula
| SV string
datatype pftree = Pr sequent rule (pftree list)
| Unf sequent

Example – given a proof tree, find the premises (unproved leaves)

primrec
  "premsPT (Unf seq) = [seq]"
  "premsPT (Pr rule pts) =
    premsPTl (premsRule rule) pts"
  "premsPTl prems [] = []"
  "premsPTl prems (pt # pts) =
    premsPT pt @ premsPTl (tl prems) pts"

Aim to mechanically verify Belnap’s general cut-elimination theorem for Display Logic – have now done this, and a proof of strong normalization of cut-elimination (later paper)

Deep vs Shallow Embeddings

Shallow  Deep

we derive some sequent in δRA we prove that a given sequent is derivable from a given set of rules (those of δRA)

we write an ML function to convert a proof with cuts into a cutfree proof we mechanise the proof of the cutelimination theorem

Isabelle variable to represent any structure; Isabelle substitutes for these Isabelle term SV ?str represents structure variable; we define substitution functions

Outcomes of the Deep Embedding

(slide omitted when detail of

cut-elimination given)

• Isabelle proof of cut-elimination theorem.

• Attempted Isabelle proof of Strong Normalization of cut-elimination.

• Discovered error in textbook proof.

• New proof of Strong Normalization – successfully implemented in Isabelle!

• Paper – 35 pages + more needed.

Principal Cut

Defn A cut is principal if the cut-formula is introduced immediately above, on both sides.

For example,

\begin{matrix}Π_{ZAB} \\ Z ⊢ A, B \end{matrix} (⊢ ∨) Z ⊢ A ∨ B  ^{\begin{matrix}Π_{AX} \\ A ⊢ X \end{matrix} \begin{matrix}Π_{BY} \\ B ⊢ Y \end{matrix} (∨ ⊢) A ∨ B ⊢ X, Y} (cut) Z ⊢ X, Y

is transformed to

Principal Cut – after

\begin{aligned}^{\begin{matrix}Π_{ZAB} \\ Z ⊢ A, B \end{matrix} (cs1) ∗A, Z ⊢ B} & \begin{matrix}Π_{BY} \\ B ⊢ Y \end{matrix} & (cut) & ∗A, Z ⊢ Y \\ & (\overline{cs1}) \\ Z ⊢ A, Y \end{aligned} ; (cs2) ; Z, ∗Y ⊢ A  \begin{matrix}Π_{AX} \\ A ⊢ X \end{matrix} (cut) Z, ∗Y ⊢ X

(\overline{cs2}) Z ⊢ X, Y

Making a Cut Left-Principal

\begin{aligned}Π′ & (intro-A) & X′ ⊢ A \\ & (π) \\ Π_{L} \end{aligned} ; (ρ) ; X ⊢ A  \begin{matrix}Π_{R} \\ A ⊢ Y \end{matrix} (cut) X ⊢ Y

is transformed to

Π′ (intro-A) X′ ⊢ A  \begin{matrix}Π_{R} \\ A ⊢ Y \end{matrix} (cut) X′ ⊢ Y

(π) Π_{L}[A?= Y]

(ρ) X ⊢ Y

How the proofs work

• Proof requires combining several inductive results.

• Arbitrary cut ⇝ Left-principal cut(s)

  canElimAll (cutIsLP ?A) ==>
      canElim (cutOnFmls {?A})

• Left-principal cut ⇝ Principal cut(s)

  canElimAll (cutIsLRP ?A) ==>
      canElim (cutIsLP ?A)

• Principal cut ⇝ Cuts on smaller cut-formulae

  canElimAll (cutOnFmls {?A, ?B}) ==>
      canElim (cutIsLRP (?A v ?B))

• For simple proof – always deal with topmost cut.

Putting them together

Put the above together using the following

canElim (cutIsLRP ?A) ==>
    canElimAll (cutIsLRP ?A)
canElim (cutIsLP ?A) ==>
    canElimAll (cutIsLP ?A)
canElim (cutOnFmls ?s) ==>
    canElimAll (cutOnFmls ?s)

and then do induction on size of cut-formula.

Higher-order predicates and functions crucial, eg above, or

allPT ::  "(pftree => bool) => pftree => bool"

allPT f tree returns true if every subtree of tree satisfies the boolean valued function f

Branch in left subtree

Π′ (intro-A) X′ ⊢ A ^{Π′′ (intro-A) X′′ ⊢ A} (π) Π_{L}

(ρ) X ⊢ A

\begin{matrix}Π_{R} \\ A ⊢ Y \end{matrix}

(cut)
X ⊢ Y

is transformed to

\begin{matrix}Π′ \\ X′ ⊢ A \end{matrix} \begin{matrix}Π_{R} \\ A ⊢ Y \end{matrix} (cut) X′ ⊢ Y ^{\begin{matrix}Π′′ \\ X′′ ⊢ A \end{matrix} \begin{matrix}Π_{R} \\ A ⊢ Y \end{matrix} (cut) X′′ ⊢ Y} (π) Π_{L}[A?= Y]

(ρ) X ⊢ Y

Two successive introductions – before

Π  (ρ) X, B ⊢ ∗B

(⊢ ¬) X, B ⊢ ¬B

(dp) ∗¬B, X ⊢ ∗B

(⊢ ¬) ∗¬B, X ⊢ ¬B

(dp) X ⊢ ¬B, ¬B

(⊢ cont ) X ⊢ ¬B

\begin{matrix}Π_{R} \\ ¬B ⊢ Y \end{matrix}

(cut)

X ⊢ Y

Two successive introductions – after

\begin{aligned}\begin{aligned}Π & (ρ) & X, B ⊢ ∗B \\ & (⊢ ¬) \\ X, B ⊢ ¬B \end{aligned} & \begin{matrix}Π_{R} \\ ¬B ⊢ Y \end{matrix} & (cut) & X, B ⊢ Y \\ & (dp) \\ ∗Y, X ⊢ ∗B \end{aligned} ; (⊢ ¬) ; ∗Y, X ⊢ ¬B \begin{matrix}Π_{R} \\ ¬B ⊢ Y \end{matrix} (cut) ∗Y, X ⊢ Y

(dp) X ⊢ Y, Y

(⊢ cont ) X ⊢ Y

Strong normalization

• Alternatively, can perform a reduction step at any point in the tree.

• Want to prove that this terminates.

• Textbook proof wrong (assimilates two previous cases).

• This discovered only in implementing proof in Isabelle!

• Alternative proof found and performed in Isabelle (paper: 35 pages + more to come!).

Use in Hardware Design / Verification

• Work by Fairtlough & Mendler

• Same idea used in Hardware Timing Constraints

• Construct proof around basic logic of gates – ∧, ∨, etc, plus Lax Logic ◯

• Timing constraints recorded automatically • s ∈ P means P true at time s

• S ∈ ◯_{∀}P means P true at any time s ∈ S

Lax Logic (Fairtlough & Mendler)

As intuitionistic logic, with operator ◯ ◯R : M → ◯M ◯M : ◯ ◯ M → ◯M ◯F : (M → N) → (◯M → ◯N) Note similarity to types of monad functions

Some rules as implemented

Abstract  Concrete

\frac{P Q}{P ∧ Q}(∧I)  \frac{s ∈ P t ∈ Q}{(s, t) ∈ (P ⊓ Q)} (⊓I)

\frac{P → Q P}{Q} (→ E)  \frac{f ∈ P ⊐ Q x ∈ P}{fp ∈ Q} (⊐ E)

\frac{∀y.P y}{P x}(∀E)  \frac{f ∈ ⊓y.P y}{fx ∈ P x}

\frac{◯_{∀}(◯_{∀}P)}{◯_{∀}P} (◯_{∀}M)  \frac{S ∈ ◯_{∀}(◯_{∀}P)}{⋃ S ∈ ◯_{∀}P}

Example (Fairtlough, Mendler &

Cheng)

ψ_{1} : ∀s.s ≥ 5 → s ∈ P_{1}a ψ_{2} : ∀sy.s ≥ 9y → s ∈ P_{2}(fy) ψ_{3} : ∀tsy_{1}y_{2}.(t ≥ s+35∧s ∈ P_{1}y_{1} ∧s ∈ P_{2}y_{2}) →

t ∈ Q(g(y_{1}, y_{2})) Rewrite them to ψ_{1}^{♯} : {s ≥ 5} ∈ ◯_{∀}(P_{1}a) ψ_{2}^{♯} : ∀y.{s ≥ 9y} ∈ ◯_{∀}(P_{2}(fy)) ψ_{3}^{♯} : ∀y_{1}y_{2}s_{1}s_{2}.s_{1} ∈ P_{1}y_{1} ∧ s_{2} ∈ P_{2}y_{2} →

{t | s_{1} = s_{2}∧t >= s_{1}+35} ∈ ◯_{∀}(Q(g(y_{1}, y_{2})))

Proof of Lax Logic version

\begin{matrix}ψ_{3} \\ ∀y_{1}y_{2}.P_{1}y_{1} ∧ P_{2}y_{2} → ◯_{∀}(Q(g(y_{1}, y_{2}))) \end{matrix} (∀E, ∀E) P_{1}a ∧ P_{2}(fb) → ◯_{∀}(Q(g(a, fb))) ; ⋮

⋮ ⋮ ⋮  ^{\begin{matrix}ψ_{1} \\ ◯_{∀}(P_{1}a) \end{matrix}  ^{\begin{matrix}ψ_{2} \\ ∀y. ◯_{∀} (P_{2}(fy)) \end{matrix} (∀E) ◯_{∀}(P_{2}(fb))} (◯_{∀}S) ◯_{∀}(P_{1}a ∧ P_{2}(fb))} (◯_{∀}E) ◯_{∀}(Q(g(a, fb)))

(∃I) ∃v. ◯_{∀} (Qv)

Further rewrite equations from ψ_{1}^{♯} : {s ≥ 5} ∈ ◯_{∀}(P_{1}a) ψ_{2}^{♯} : ∀y.{s ≥ 9y} ∈ ◯_{∀}(P_{2}(fy)) ψ_{3}^{♯} : ∀y_{1}y_{2}s_{1}s_{2}.s_{1} ∈ P_{1}y_{1} ∧ s_{2} ∈ P_{2}y_{2} →

{t | s_{1} = s_{2}∧t >= s_{1}+35} ∈ ◯_{∀}(Q(g(y_{1}, y_{2}))) to ψ_{1}^{♯} : {s ≥ 5} ∈ ◯_{∀}(P_{1}a) ψ_{2}^{♯} : λy.{s ≥ 9y} ∈ ⊓y. ◯_{∀} (P_{2}(fy)) ψ_{3}^{♯} : λy_{1}y_{2}.λ(s_{1}, s_{2}).{t | s_{1} = s_{2} ∧ t ≥ s_{1} + 35} ∈

⊓y_{1}y_{2}.P_{1}y_{1} ∧ P_{2}y_{2} → ◯_{∀}(Q(g(y_{1}, y_{2})))

Proof in Isabelle

goal Tiny_thy "?p : (SUM v. Oall(Q v))"
Level 2 (2 subgoals)
[?x1;Union (?r8 ` ?a2)] :
   SUM v. (Oall (Q v))
 1. ?r8 : (?P8 ---> Oall (Q ?x1))
 2. ?a2 : Oall ?P8
Level 4 (2 subgoals)
[g (?y10, ?y9);
 Union (((%y1 y2 (z1, z2).
   {t. z1 = z2 & z1 + #35 <= t}) `` ?y10 `` ?y9) `
   (?p11 <*> ?q11))]
: SUM v. (Oall (Q v))
 1. ?p11 : Oall (P1 ?y10)
 2. ?q11 : Oall (P2 ?y9)

Level 6
[g (a, f ?y12);
 Union (((%y1 y2 (z1, z2).
   {t. z1 = z2 & z1 + #35 <= t}) `` a `` f ?y12) `
   (Collect (op <= #5) <*>
     ((%y. Collect (op <= (#9 * y))) `` ?y12)))]
: SUM v. (Oall (Q v))
No subgoals!

The above uses

p3 = "(%y1 y2 (z1, z2).
   {t. z1 = z2 & z1 + #35 <= t})
 : PROD y1 y2. (P1 y1 && P2 y2 --->
   Oall (Q (g (y1, y2))))"
p3 RS Prodd_Ep p3 RS Prodd_Ep =
"(%y1 y2 (z1, z2).
   {t. z1 = z2 & z1 + #35 <= t}) `` ?y1 `` ?y
 : (P1 ?y1 && P2 ?y ---> Oall (Q (g (?y1, ?y))))"