Commit ca62044e authored by Florian Rabe's avatar Florian Rabe

no message

parent 6c2eedb4
namespace http://cds.omdoc.org/examples
/T
Intuitionistic propositional logic with natural deduction rules and a few example proofs 
/T
We start with the syntax of propositional logic.
theory PL : http://cds.omdoc.org/urtheories?LF =
# :types The Basic Concepts
/T the type of propositions 
prop : type 
/T Given [F:prop], the type $ded F$ holds the proofs of $F$.
ded : prop → type  # ded 1 prec 0## ⊦ 1 prec 0role Judgment
## Abbreviations
/T The type $contra$ abbreviates the judgment of inconsistency.
If we can give an element of the type, then every proposition has a proof.
contra : type  = {a} ded a # ↯ 
# Constructors
/T The constructors provide the expressions of the types above.
true : prop 
and : prop → prop → prop  # 1 ∧ 2 prec 15
or : prop → prop → prop  # 1 ∨ 2 prec 15
impl : prop → prop → prop  # 1 ⇒ 2 prec 10
not : prop → prop  # ¬ 1 prec 20
/T Equivalence is taken as a non-primitive here and defined such that for [F:prop,G:prop] we define $F⇔G$ as $(F ⇒ G) ∧ (G ⇒ F)$.
equiv : prop → prop → prop  # 1 ⇔ 2 prec 10
= [x,y] (x ⇒ y) ∧ (y ⇒ x)

/T Now we describe the proof theory.
theory PLNatDed : http://cds.omdoc.org/urtheories?LF =
include ?PL 
/T We use natural deduction proof rules that construct expressions of type $ded F$ for some [F:prop].
{For example, assume two propositions [F: prop, G: prop].
{If [p:ded F, q: ded G], then $andI p q$ is a proof of $F∧G$.}
{If [p:ded F∧G], then $andEl p$ is a proof of $F$.}
}

trueI : ded true
andI : {A,B} ded A → ded B → ded A ∧ B 
andEl : {A,B} ded A ∧ B → ded A  role ForwardRule
andEr : {A,B} ded A ∧ B → ded B  role ForwardRule
orIl : {A,B} ded A → ded A ∨ B 
orIr : {A,B} ded B → ded A ∨ B 
orE : {A,B,C} ded A ∨ B → (ded A → ded C) → (ded B → ded C) → ded C

impI : {A,B} (ded A → ded B) → ded A ⇒ B 
impE : {A,B} ded A ⇒ B → ded A → ded B  role ForwardRule
notI : {A} (ded A → ↯) → ded ¬ A# notI 2
notE : {A} ded ¬ A → ded A → ↯ # notE 2 3 role ForwardRule
equivI : {A,B} (ded A → ded B) → (ded B → ded A) → ded A ⇔ B 
= [A,B,p,q] andI (impI [x] p x) (impI [x] q x) 
equivEl : {A,B} ded A ⇔ B → ded A → ded B  role ForwardRule
= [A,B,p,a] impE (andEl p) a 
equivEr : {A,B} ded A ⇔ B → ded B → ded A  role ForwardRule
= [A,B,p,b] impE (andEr p) b 
imp2I : {A,B,C} (ded A → (ded B → ded C)) → ded A ⇒ (B ⇒ C) 
= [A,B,C] [f] impI [p] (impI ([q] f p q)) 
imp2E : {A,B,C} ded A ⇒ (B ⇒ C) → ded A → ded B → ded C 
= [A,B,C] [p,q,r] impE (impE p q) r 
example : {A} ded A ⇒ (A ∧ A) 
= [A]impI [p]andI p p
interactive_example : {A} ded A ⇒ (A ∧ A)
= ≪{A} ded A⇒A∧A≫ 

\ No newline at end of file
namespace http://cds.omdoc.org/examples
theory ProverTest : http://cds.omdoc.org/urtheories?LF =
a: type
b: type
c: type
d: type
k: a
r: a → b role ForwardRule
s: a → b → c role ForwardRule
t: a → b → c → d
q: d → d
test : a → a → d  = [x,y] ≪d ≫

theory PLProofs : http://cds.omdoc.org/urtheories?LF =
include ?PLNatDed
/T this doesn't work currently 
// test : {a,b} ded (a ∧ b) ⇒ (b ∧ a) = _
// test2 : {a,b} ded (a ∨ b) ⇒ (b ∨ a) = _

theory FOLProofs : http://cds.omdoc.org/urtheories?LF =
include ?FOLNatDed
// test : {f} ded (forall [x] forall [y] f x y) ⇒ (forall [y] forall [x] f x y) = _
// test2 : {f} ded (exists [x] exists [y] f x y) ⇒ (exists [y] exists [x] f x y) = _

namespace http://cds.omdoc.org/examples/programs
import rules scala://mmt.kwarc.info
theory Machine : http://cds.omdoc.org/urtheories?LF =
obj: type
loc: type
command: type
add: obj → loc → command
get: loc → obj → command
update: loc → obj → command
delete: loc → obj → command
chan: type
stdio: chan
in : chan → obj → command
out: chan → obj → command
execute: command → type

namespace http://cds.omdoc.org/examples/programs
theory Syntax : http://cds.omdoc.org/urtheories?LF =
tp: type
Bool: tp
Nat : tp
Unit: tp
prog: tp → type
true : prog Bool
false: prog Bool
unit : prog Unit
zero : prog Nat
succ : prog Nat → prog Nat# succ 1
one : prog Nat
= succ zero
equal : {a} prog a → prog a → prog Bool  # 2 = 3 prec 10
not : prog Bool → prog Bool  # ¬ 1 prec 8 
plus : prog Nat → prog Nat → prog Nat  # 1 + 2 prec 20
minus : prog Nat → prog Nat → prog Nat  # 1 - 2 prec 20
seq : {a,b} prog a → prog b → prog b  # 3 ; 4 prec 5
ifte : {a} prog Bool → prog a → prog a → prog a # if 2 then 3 else 4 prec 3
ifte2 : prog Bool → prog Unit → prog Unit
= [b,c] if b then c else unit
while : prog Bool → prog Unit → prog Unit
print : {a} prog a → prog Unit # print 2
read : {a} prog a
val : {a,b} prog a → (prog a → prog b) → prog b # val 3 4
Var : tp → type
var : {a,b} prog a → (Var a → prog b) → prog b # var 3 4
varref : {a} Var a → prog a # 2 ' prec 30
assign : {a} Var a → prog a → prog Unit # 2 ← 3 prec 10

theory Test : ?Syntax =
main = val (read Nat) [x]
var zero [y]
while (¬ x = y') (
print x;
y ← succ y'
)

theory Machine : http://cds.omdoc.org/urtheories?LF =
obj: type
loc: type
command: type
add: obj → loc → command
get: loc → obj → command
update: loc → obj → command
delete: loc → obj → command
chan: type
stdio: chan
in : chan → obj → command
out: chan → obj → command
execute: command → type

theory OperationalSemantics : http://cds.omdoc.org/urtheories?LF =
include ?Syntax
include ?Machine
objectify : {a} prog a → obj  # objectify 2
varloc: {a} Var a → loc → type # 2 @ 3
eval : {a} prog a → prog a → type # 2 ⟿ 3 prec 3
eval_seq: {a,b, p:prog a, q: prog b, x,y} p⟿x → q⟿y → p;q ⟿ y
eval_if_true : {a, c, t,e: prog a, x} c⟿true → t⟿x → if c then t else e ⟿ x
eval_if_false: {a, c, t,e: prog a, x} c⟿false → e⟿x → if c then t else e ⟿ x
eval_while_true : {c, b, x, y} c⟿true → b⟿x → while c b ⟿ y → while c b ⟿ y
eval_while_false: {c, b} c⟿false → while c b ⟿ unit
eval_var : {a,b, p: prog a, cont: Var a → prog b, l, x, y}
p⟿x → execute (add (objectify x) l) → ({v} v@l → cont v ⟿ y)
→ (var p cont)⟿y
eval_varref : {a,v:Var a,l,x}
v@l → execute (get l (objectify x))
→ v' ⟿ x
eval_assign : {a, v: Var a,p,l,x}
p⟿x → v@l → execute (update l (objectify x))
→ v←p ⟿ unit
eval_print : {a, p: prog a, x}
p⟿x → execute (out stdio (objectify x))
→ (print p) ⟿ unit
eval_read : {a, x: prog a}
execute (in stdio (objectify x))
→ (read a) ⟿ x

\ No newline at end of file
namespace http://cds.omdoc.org/examples/programs
theory OperationalSemantics : http://cds.omdoc.org/urtheories?LF =
include ?Syntax
include ?Machine
objectify : {a} prog a → obj  # objectify 2
varloc: {a} Var a → loc → type # 2 @ 3
eval : {a} prog a → prog a → type # 2 ⟿ 3 prec 3
eval_seq: {a,b, p:prog a, q: prog b, x,y} p⟿x → q⟿y → p;q ⟿ y
eval_if_true : {a, c, t,e: prog a, x} c⟿true → t⟿x → if c then t else e ⟿ x
eval_if_false: {a, c, t,e: prog a, x} c⟿false → e⟿x → if c then t else e ⟿ x
eval_while_true : {c, b, x, y} c⟿true → b⟿x → while c b ⟿ y → while c b ⟿ y
eval_while_false: {c, b} c⟿false → while c b ⟿ unit
eval_var : {a,b, p: prog a, cont: Var a → prog b, l, x, y}
p⟿x → execute (add (objectify x) l) → ({v} v@l → cont v ⟿ y)
→ (var p cont)⟿y
eval_varref : {a,v:Var a,l,x}
v@l → execute (get l (objectify x))
→ v' ⟿ x
eval_assign : {a, v: Var a,p,l,x}
p⟿x → v@l → execute (update l (objectify x))
→ v←p ⟿ unit
eval_print : {a, p: prog a, x}
p⟿x → execute (out stdio (objectify x))
→ (print p) ⟿ unit
eval_read : {a, x: prog a}
execute (in stdio (objectify x))
→ (read a) ⟿ x

\ No newline at end of file
namespace http://cds.omdoc.org/examples/programs
theory Syntax : http://cds.omdoc.org/urtheories?LF =
tp: type
Bool: tp
Nat : tp
Unit: tp
prog: tp → type
true : prog Bool
false: prog Bool
unit : prog Unit
zero : prog Nat
succ : prog Nat → prog Nat# succ 1
one : prog Nat
= succ zero
equal : {a} prog a → prog a → prog Bool  # 2 = 3 prec 10
not : prog Bool → prog Bool  # ¬ 1 prec 8 
plus : prog Nat → prog Nat → prog Nat  # 1 + 2 prec 20
minus : prog Nat → prog Nat → prog Nat  # 1 - 2 prec 20
seq : {a,b} prog a → prog b → prog b  # 3 ; 4 prec 5
ifte : {a} prog Bool → prog a → prog a → prog a # if 2 then 3 else 4 prec 3
ifte2 : prog Bool → prog Unit → prog Unit
= [b,c] if b then c else unit
while : prog Bool → prog Unit → prog Unit
print : {a} prog a → prog Unit # print 2
read : {a} prog a
val : {a,b} prog a → (prog a → prog b) → prog b # val 3 4
Var : tp → type
var : {a,b} prog a → (Var a → prog b) → prog b # var 3 4
varref : {a} Var a → prog a # 2 ' prec 30
assign : {a} Var a → prog a → prog Unit # 2 ← 3 prec 10

theory Test : ?Syntax =
main = val (read Nat) [x]
var zero [y]
while (¬ x = y') (
print x;
y ← succ y'
)

// Comments begin with // and end with the delimiter of the current level.
Comments starting with /T count as content themselves and are, e.g., preserved in the HTML rendering of a file.
Therefore, all comments in this file start with /T
/T This file contains a definition of first-order logic in MMT as used in the MMT tutorial given at CICM 2016.
/T A namespace declaration defines the root URI of the following content.
namespace http://cds.omdoc.org/examples/tutorial
/T A theory defines a language. It may optionally use a meta-theory, which is given by its URI.
theory FOL : http://cds.omdoc.org/urtheories?LF =
/T The simplest declaration in an MMT theory introduces a named symbol.
Every declaration can have multiple attributes following the name.
Each attribute is introduced by a special keywork:
the type - introduced by ':'.
the definiens - introduced by '='
the notation - introduced by '#'
If multiple attributes are present, they must be ended with the object delimiter.

/T The following declaration introduces the type of FOL propositions.
Its type is the object 'type', which is defined by LF.
prop : type 
/T All symbols occuring in an MMT object are cross-linked to their declaration.
Try hovering or control-clicking on 'type' above
/T The following declarations introduce the constructors of propositional logic and their notations.
/T → is used for simple functions. It is part of the notations defined by LF.
It is right-associative. By double-clicking on →, you can see its arguments.
true : prop 
false : prop 
and : prop → prop → prop  # 1 ∧ 2 prec 15
or : prop → prop → prop  # 1 ∨ 2 prec 15
impl : prop → prop → prop  # 1 ⇒ 2 prec 10
not : prop → prop  # ¬ 1 prec 20
/T Note that multiple attributes (here: type and notation) must be separated by .
Among other things, that allows using :, =, and # as ordinary characters anywhere else.
/T Notations consist of numbers refering to argument positions and arbitrary Unicode strings defining delimiters.
Optionally, a notation may end in 'prec NUMBER' to define a precedence. Higher precedences bind stronger.
For example, '1 ∧ 2 prec 15' makes conjunction an infix operator with precedence 15.

/T As an example for a defined symbol, let us consider the equivalence connective.
We define it in terms of conjunction and implication.
The definiens uses [x,y], which is the notation defined for lambda-abstraction in LF.
The types of the bound variables are infered by MMT - try hovering over them to see the types.

equiv : prop → prop → prop  # 1 ⇔ 2 prec 10
= [x,y] (x ⇒ y) ∧ (y ⇒ x)
/T Here three attributes (type, notation, and definition) are present. The order does not matter.
/T Now for the first-order aspects.
We opt for sorted (also called typed) first-order logic, e.g., there may be multiple sorts that we can quantify over separately.
/T The following declarations introduce the LF-type of sorts and the LF type of terms of a given sort.
sort : type
term : sort → type # tm 1
/T The point of the latter is as follows: If, e.g., 's:sort' is a sort, then 'tm s' is the type of all terms of sort s
/T The following declaration introduces a symbol for sorted equality.
equal : {s: sort} tm s → tm s → prop# 2 = 3 prec 30  role Eq 
/T Here {s: sort} is the Pi-binder of LF for dependent function spaces.
Thus, equal takes a sort as its first argument and then 2 terms of that sort.
/T In the notation for equal, the first argument - the sort - is not mentioned.
That makes the sort an implicit argument that is infered by MMT.

/T The types of the quantifiers use LF's higher-order abstract syntax:
'tm s → prop' can be used as the type of proposition with a free variables of type 'tm s'.
The sort is an implicit argument again, and the type of sort is infered by MMT.

forall : {s} (tm s → prop) → prop# ∀ 2
exists : {s} (tm s → prop) → prop# ∃ 2
/T Finally, we need to be able to talk about the truth of propositions.
For that, we introduce a Curry-Howard style judgment: The LF-type '⊢ P' is the type of proofs of the proposition 'P'.

proof : prop → type # ⊢ 1 prec 0
 role Judgment
/T It's practical to give ⊢ a very low precedence to avoid brackets later on.
/T The 'role Judgment' is an attribute introduced by the LF plugin (which tells MMT to be loaded automatically whenever LF is used).
By annotation the symbol 'proof' in this way, the plugin can add some LF-specific language support, in particular, it can generate appropriate default notations.


/T Now we define the proof theory of LF using natural deduction proof rules.
It is practical to do this in a separate theory that includes the syntax above.

theory NatDed : http://cds.omdoc.org/urtheories?LF =
/T 'include THEORY' includes another theory.
When refering to a theory, we do not actually have to give the absolute URI.
Below the relative URI '?FOL' is resolved relative to the current namespace and yields http://cds.omdoc.org/examples/tutorial?FOL.

include ?FOL 
/T Some FOL proof rules talk about contradictioins.
A FOL theory is contradictory if we can derive any formula. That can be captured by the LF type '{a: prop} ⊢ a'. If this type is non-empty, a theory is inconsistent.
We introduce an abbreviation for it:
contra : type  = {a} ⊢ a # ↯
trueI : ⊢ true
falseE : ⊢ false → ↯
andI : {A,B} ⊢ A → ⊢ B → ⊢ A ∧ B 
andEl : {A,B} ⊢ A ∧ B → ⊢ A 
andEr : {A,B} ⊢ A ∧ B → ⊢ B 
orIl : {A,B} ⊢ A → ⊢ A ∨ B 
orIr : {A,B} ⊢ B → ⊢ A ∨ B 
orE : {A,B,C} ⊢ A ∨ B → (⊢ A → ⊢ C) → (⊢ B → ⊢ C) → ⊢ C

impI : {A,B} (⊢ A → ⊢ B) → ⊢ A ⇒ B 
impE : {A,B} ⊢ A ⇒ B → ⊢ A → ⊢ B 
notI : {A} (⊢ A → ↯) → ⊢ ¬ A# notI 2
notE : {A} ⊢ ¬ A → ⊢ A → ↯ # notE 2 3
/T Because equivalence is defined, we can derive its rules.
As usual for Curry-Howard style representations, a derived rule is simply a rule with a definiens.

equivI : {A,B} (⊢ A → ⊢ B) → (⊢ B → ⊢ A) → ⊢ A ⇔ B 
= [A,B,p,q] andI (impI [x] p x) (impI [x] q x) 
equivEl : {A,B} ⊢ A ⇔ B → ⊢ A → ⊢ B
= [A,B,p,a] impE (andEl p) a 
equivEr : {A,B} ⊢ A ⇔ B → ⊢ B → ⊢ A
= [A,B,p,b] impE (andEr p) b 
forallI : {s, A: tm s → prop} ({x} ⊢ (A x)) → ⊢ ∀ A  # allI 3
forallE : {s, A: tm s → prop} ⊢ (∀ A) → {x} ⊢ (A x)  # allE 3
existsI : {s, A: tm s → prop} {c} ⊢ (A c) → ⊢ ∃ [x] (A x) # exI 2 4
existsE : {s, A: tm s → prop, C} ⊢ (∃ A) → ({x} ⊢ (A x) → ⊢ C) → ⊢ C  # exE 4 5
/T The rules for equality consist of the equivalence rules at every sort ...
refl : {s,x: tm s} ⊢ x = x  # refl 2 
sym : {s,x: tm s,y} ⊢ x = y → ⊢ y = x
trans : {s,x: tm s,y,z} ⊢ x = y → ⊢ y = z → ⊢ x = z
/T ... and congruence rules for substituting a subterm x with y in any term T or formula F.
congTerm : {s,t, T: tm s → tm t}{x,y} ⊢ x = y → ⊢ (T x) = (T y)
congForm : {s, F: tm s → prop}{x,y} ⊢ x = y → ⊢ (F x) → ⊢ (F y)

/T The rules declared so far only yield intuitionistic first-order logic. To get to classical logic,
we can use the modular approach and extend NatDed by the law of excluded middle: 
theory ClassicalSFOL : ur:?LF =
include ?NatDed 
TND : {A} ⊢ A ∨ ¬ A  # TND 1 

\ No newline at end of file
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment