Commit d3a8628a authored by Pierre Letouzey's avatar Pierre Letouzey
Browse files

hol, some more proofs

parent 724b7944
A Brief Description of HOL-Light
================================
HOL : Higher-Order Logic.
HOL-light : one member of a family of provers based on this HOL logic.
Reference: [HOL Light: an overview. John Harrison](http://www.cl.cam.ac.uk/~jrh13/papers/hollight.pdf)
## The logical framework
......@@ -18,15 +21,14 @@ All starts with (polymorphic) simply-typed lambda-calculus.
- Variables `x, y, z, ...`
- Functions `λx. t`
- Application `t(u)`
- Two predifined constants : `(=) : α → α → bool` and `ε : (α → bool) → α` (Hilbert choice operator).
- Two predefined constants : `(=) : α → α → bool` and `ε : (α → bool) → α` (Hilbert choice operator).
Syntax : `t = u` is just `(((=) t) u)`.
And when `p` and `q` are of type `bool` (hence propositions), `p = q` is rather written `p <=> q`.
#### The deducibility predicate
Unlike in Coq or Agda, provability is **not** based on a typing relation. The type system is just here to ensure that propositions (and other
elements) are well-formed.
Unlike in Coq or Agda, provability is **not** based on a typing relation. The type system is just here to ensure that propositions (and other elements) are well-formed.
So for a proposition `p` (i.e. a well-typed lambda-term of type `bool`) and a context `Γ` (i.e. a set of well-typed lambda-terms of type `bool`), a separate predicate `Γ ⊢ p` will express that `p` is deducible from `Γ`.
......@@ -62,7 +64,7 @@ This deducibility predicate is obtained through the following ten inference rule
----------------------- (EQ_MP)
Γ ∪ ∆ ⊢ q
Γ ⊢ p ∆ ⊢ q
Γ ⊢ p ∆ ⊢ q
--------------------------------- (DEDUCT_ANTISYM_RULE)
(Γ − {q}) ∪ (∆ − {p}) ⊢ p <=> q
......@@ -96,6 +98,7 @@ p ‌\/ q := ∀r. (p ==> r) ==> (q ==> r) ==> r
⊥ := ∀p. p
¬p := p ==> ⊥
```
Note : the encodings for exist and disjunction and false are called impredicative encodings.
Note that `∀x.P(x)` (actually written `!x.P(x)` in HOL-Light syntax) is a notation for `∀P` or equivalently `∀(λx.P(x))`. Similarly, `∃x.P(x)` (written `?x.P(x)` in HOL-Light) is `∃P` or `∃(λx.P(x))`.
......@@ -137,4 +140,77 @@ Transitivity is one of the basic rules (for efficiency reasons). But it can actu
Exercise : retreive the usual introduction and elimination rules for `T`, `/\`, `==>`, ``, ``, `\/`, ``, `¬`.
Truth introduction :
```
--------------------REFL
⊢ (λp. p) = (λp. p)
=
⊢ T
```
Side note : `|- p ` and `|- p = T` are equivalent :
```
|- p |- T
-----------------------DEDUCT_ANTISYM_RULE
|- p=T
|- p=T
--------SYM
|- T=p |- T
------------------------EQ_MP
|- p
```
Conjunction introduction :
```
|-p
-------R ------(See above)
|- f=f |-p=T |- q
-----------------MK_COMB ----------(See above)
|- f p = f T |- q = T
---------------------------------------MK_COMB
|- f p q = f T T
---------------------------------ABS
|- (λf. f p q) = (λf. f T T)
=
|- p /\ q
```
Conjunction left elimination :
```
|- p/\q
= ----------REFL
|- (λf. f p q) = (λf. f T T) |- f = f
----------------------------------------------- MK_COMB
|- (λf. f p q) f = (λf. f T T ) f
(... TRANS + BETA ...)
|| ||
|- f p q = f T T
------------------------------------ INST
|- (λxy.x) p q = (λxy.x) T T
(...beta conversion, see below...)
|- p = T
---------(see before)
|-p
```
NB : we indeed have a more general beta conversion, via `BETA+INST` :
```
------------(BETA)
⊢ (λx.t)x = t
---------------------------(INST)
⊢ ((λx.t)x)[x/u] = t[x/u]
=
⊢ (λx.t)u = t[x/u]
```
Exercise(++) : retreive at least one classical law from `SELECT_AX`.
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