propositional logic

logical verification week 1 2004 09 08

who

Femke

Freek  Paulien

what

• 13 lectures

• practical work – Coq proofs & paper proofs – 9 out of 12

• final test

stuff

• hand out – course notes

– exercises

• web page – hand out

– files for the exercises

– solutions for the exercises – slides

– old tests

where

• lectures: S201 Coq lab: S345

http://www.cs.vu.nl/~tcs/al/
tcs@cs.vu.nl

• Freek:

tuesdays & wednesdays: U333

freek@cs.ru.nl

topic

computer science

formal methods

proof assistants type theory

examples of applications of formal methods

• Intel bug

• driverless train

• spacecraft

• credit cards

proof assistants

• PVS

• Coq/NuPRL • ACL2

• HOL/Isabelle • Mizar

what we will do here

Curry-Howard-de Bruijn isomorphism

logic  ⟷  lambda calculus
natural deduction  ‘type theory’
on paper  •  •
in Coq  •  •

logics

• the systems in this course

propositional logic ⟷ calculus called λ→
predicate logic ⟷ calculus called λP
2nd order propositional logic ⟷ calculus called λ2
[figure: λω; λC; λ2; λP 2; λ\underline{ω}; λP \underline{ω}; λ→; λP]

and also

• inductive types – built-in

– higher order encoding • program extraction

today

first order propositional logic first order predicate logic

second order propositional logic

formulas

A → B

⊥

⊤

¬A  := A → ⊥

A ∧ B

A ∨ B

logical rules

two kinds of rules • introduction rules • elimination rules

rules for →

introduction rule [A^{x}] assumption ⋮

B / (A → B)

I[x]→

elimination rule

\frac{⋮ ; A → B  ⋮ ; A}{B} E→

example_{A → A}

15

bigger example

((A → B) → (C → D)) → C → B → D

second hour

rules for the other connectives

⊥ elimination

⊤ introduction

¬ introduction ¬ elimination excluded middle A ∨ ¬A

∧ introduction ∧ elimination, left rule ∧ elimination, right rule

∨ introduction, left rule ∨ introduction, right rule ∨ elimination

the rules for ∨

∨ introduction

\frac{⋮ ; A}{A ∨ B} Il∨  \frac{⋮ ; B}{A ∨ B} Ir∨

∨ elimination

\frac{⋮ ; A ∨ B  ⋮ ; A → C  ⋮ ; B → C}{C} E∨

example with ∨

(A ∨ B) → (B ∨ A)

Coq

• goals Coq tells you what is left to be proved

• tactics you tell Coq how to prove it

Coq term syntax

A -> B
 False
 True
  ~A
A /\ B
A \/ B

the Coq language

commands

• Parameter ; • Lemma ; • Qed

tactics

• intro  I[x]→

• apply  E→

• elim  E⊥ El∧ Er∧ E∨
• exact  assumption

• split  I∧
• left right  Il∨ Ir∨

interfaces

• coqtop + coqc

‘command line’

• xemacs + Proof General

• coqide
• pcoq

example

                        A -> A
• with coqtop

• with Proof General

the second example

((A -> B) -> (C -> D)) -> C -> B -> D

and the third example

                   (A \/ B) -> (B \/ A)

summary

• formal methods

• type theory the Curry-Howard-de Bruijn isomorphism

• propositional logic

• Coq