mapping HOL into Coq

Freek Wiedijk University of Nijmegen

TYPES 2002, Nijmegen 2002-04-28, 12:00

LRI, Paris 2002-06-28, 13:30 overview

translating HOL proofs to Coq analogue of HOL to Nuprl translator by Naumov, Stehr and Mesequer

I’ll describe my attempt that failed translation used axioms: inconsistent with Coq can anyone help me do this properly?

translating constructive HOL proofs to Coq still a problem left with HOL type definitions from FTA to FTC?

FTA project: 1999-2000

Fundamental Theorem of Algebra:

every complex polynomial has a root also formalized in Mizar and HOL

next step?

Fundamental Theorem of Calculus \frac{d}{dx} and ∫ are inverse operations

already present in Mizar and HOL libraries!

import this into Coq? in the meantime:

Luís Cruz-Filipe has proved FTC in the FTA framework constructive proof from Bishop’s book translating mathematics: the de Bruijn criterion

Coq

– proofs checked by small kernel: ‘proof object’

– don’t contain the traces of the calculations checking time can be much bigger than size of proof object

HOL

– proofs checked by small kernel proofs not stored in memory: ‘ephemeral proof object’

– do contain full traces of calculations β-reduction is proof step called BETA

basic HOL library  1.5 million proof steps
HOL version of FTC 2.5 million proof steps

translation approach: generate a Coq definition for each HOL proof step Coq proof objects 2 sort constructors:

   Prop (= Prop, Set) Type

16 term constructors:

   Rel  Var  Meta  Evar  Sort  Cast  Prod  Lambda  LetIn
   App  Const  Ind  Construct  Case  Fix  CoFix

HOL ephemeral proof objects

2 type constructors:

Tyvar  Tyapp (bool, fun, ind)

4 term constructors:

Var  Const (=, @) Comb  Abs

10 + 3 thm constructors:

REFL  TRANS  MK COMB  ABS  BETA  ASSUME  EQ MP
DEDUCT ANTISYM RULE  INST  INST TYPE
new axiom (INFINITY AX, ETA AX, SELECT AX)
new basic definition
new basic type definition

a naive translation scheme translation scheme:

   hol_type → Set
        fun → ->
       bool → bool
        ind → nat

= → Leibniz equality

add two ‘classical axioms’ to get classical mathematics:

 extensionality (A,B:Set; f,g:A->B)((x:A)(f x)=(g x))->f=g
 choice  (A:Set)~(is_empty A)->A

   is_empty [A:Set]:Prop := (a:A)False (≡ ∀a ∈ A. ⊥)

choice is equivalent to excluded middle for Set choice implies excluded middle for Prop: classical logic impredicativity of Set

in Coq:

                       Set->bool : Set
                    (A:Set)A->bool : Set

in the λ-cube, λ2: \begin{matrix}2 : ∗ ⊢ (ΠA:∗. 2) : ∗ \\ 2 : ∗ ⊢ (ΠA:∗. Πa:A. 2) : ∗ \end{matrix}

mathematically:

P(Set) ∈ Set
∏_{A∈Set} P(A) ∈ Set

in classical set theory this gives a paradox:

define U ≡ ∏_{A∈Set} P(A)

define X ≡ {u ∈ U | u ∉ u_{U}} ∈ P(U)

take any x ∈ U with x_{U} = X

x ∈ x_{U} ⟺ x ∈ X ⟺ x ∉ x_{U} contradiction Coq is incompatible with classical mathematics

naive thought: constructive mathematics is weaker than classical mathematics

⇒ adding ‘classical’ axioms to Coq is safe

doesn’t work!

excluded middle for Set is inconsistent with the Coq logic! (excluded middle for Prop is safe)

moving the two axioms from Set to Type: does it help?

  Set ⊆ Type

⇒ a choice operator for Type is also a choice operator for Set

wanted: classical axioms

– use Coq as a ‘super-HOL’

– consistent with the Coq logic

Prop ↔ bool

Coq: Prop type for propositions Coq: bool type for ‘decidable propositions’

exactly two elements:

    (b:bool) b = true \/ b = false

HOL: bool classical logic

also has exactly two elements:

    !b:bool. (b = T) \/ (b = F)

which of the two Coq types corresponds to the HOL bool? the HOL Light architecture: LCF kernel + constructive core + rest

HOL Light by John Harrison

top level file hol.ml, loads 35 subfiles:

1 file with basic library functions lib.ml
3 files with the ‘de Bruijn kernel’ type.ml term.ml thm.ml
13 files with constructive HOL  … num.ml …
18 files with classical HOL  class.ml …

‘Extensional, classical reasoning with AC starts now!’

axioms: one ‘constructive axiom’: infinity (INFINITY_AX) two ‘classical axioms’: extensionality (ETA_AX) and choice (SELECT_AX)

HOL definitions of logical operators basic notions: λ-calculus and = HOL definitions of logical operators:

⊤ ≡ ((λx. x) = (λx. x))
(t_{1} ∧ t_{2}) ≡ (λf. ft_{1}t_{2}) = (λf. f⊤⊤)
(t_{1} → t_{2}) ≡ ((t_{1} ∧ t_{2}) = t_{1})
(∀x. P x) ≡ (P = λx. ⊤)
(∃x. P x) ≡ (∀Q. (∀x. P x → Q) → Q)
(t_{1} ∨ t_{2}) ≡ (∀t. (t_{1} → t) → (t_{2} → t) → t)
⊥ ≡ (∀t. t)

translating HOL types into Coq setoids

translation scheme:

hol_type → ‘typoid’: setoid in Type
fun → ‘functionoid’: function setoid
bool → ‘Ω setoid’: Prop with <-> as setoid equality
ind → nat with == as setoid equality
= → setoid equality

seems to work (with no axioms needed for constructive HOL)

– no ‘uniform’ equality (hol_type does not translate to a Coq type but to a Coq record)

– extensionality (ETA_AX) turns out to be valid

– HOL bool corresponds to Coq Prop HOL type definitions are not constructive

HOL type definitions: subtypes

type A + predicate P on A + object of type A that satisfies P

– new type A′

– two functions abs : A → A′ and rep : A′ → A

– two thms that state that they are inverse to each other

abs maps all objects of A to A′ not constructive! constructivizing HOL type definitions

variant of HOL type definition scheme (John Harrison):

A + P + π : A → A that will correspond to rep ∘ abs

thms to prove:

∀a. π(πa) = πa
∀a. P a ↔ (πa = a)

valid under the setoid interpretation too weak: HOL definitions of ℕ and A × B don’t work anymore

wanted: variant of HOL subtype definitions

– constructive

– allows definition of ℕ and A × B in the HOL style