Pollack-inconsistency

Freek Wiedijk

Radboud University Nijmegen

2010 07 15 , 12 : 00_{UITP 2010}

Pollack-inconsistency

Freek Wiedijk

Radboud University Nijmegen

2010 07 15 , 12 : 00_{UITP 2010}

I

when can one trust a proof assistant?

1

Randy Pollack and how to believe a machine-checked proof

1

Randy Pollack and how to believe a machine-checked proof formal proof versus correctness

the computer has checked a formalization without finding errors is it now certain that there are no errors?

▶ philosophical issues ‘certainty without any doubt is impossible’

▶ software issues ‘all programs have bugs’

▶ the real problem certain that the proofs are correct not certain that the definitions are ‘correct’ formal proof versus correctness

the computer has checked a formalization without finding errors is it now certain that there are no errors?

▶ philosophical issues ‘certainty without any doubt is impossible’

▶ software issues ‘all programs have bugs’

▶ the real problem certain that the proofs are correct not certain that the definitions are ‘correct’ formal proof versus correctness

the computer has checked a formalization without finding errors is it now certain that there are no errors?

▶ philosophical issues ‘certainty without any doubt is impossible’

▶ software issues ‘all programs have bugs’

▶ the real problem certain that the proofs are correct not certain that the definitions are ‘correct’ formal proof versus correctness

the computer has checked a formalization without finding errors is it now certain that there are no errors?

▶ philosophical issues ‘certainty without any doubt is impossible’

▶ software issues ‘all programs have bugs’

▶ the real problem certain that the proofs are correct not certain that the definitions are ‘correct’ formal proof versus correctness

the computer has checked a formalization without finding errors is it now certain that there are no errors?

▶ philosophical issues ‘certainty without any doubt is impossible’

▶ software issues ‘all programs have bugs’

▶ the real problem certain that the proofs are correct not certain that the definitions are ‘correct’ the de Bruijn criterion the de Bruijn criterion

proof assistant

independent proof checker

proof object

the de Bruijn criterion

independent proof checker

the de Bruijn criterion

proof checking kernel

the de Bruijn criterion

proof checking kernel

remainder of the system: theorem database, basic reasoning,

rewriting, back-chaining, proof search, decision procedures,

etc.

the de Bruijn criterion

proof checking kernel

remainder of the system: theorem database, basic reasoning,

rewriting, back-chaining, proof search, decision procedures,

etc.

II a student’s remark a proof assistant for propositional logic

course proof assistants at Radboud University Nijmegen

▶ implement small proof assistant LCF-style proof assistant minimal propositional logic (= only implication)

\overline{Γ ∪ \{A\} ⊢ A} \frac{Γ ∪ \{A\} ⊢ B}{Γ ⊢ A → B} \frac{Γ ⊢ A → B Γ ⊢ A}{Γ ⊢ B}

student Marc Schoolderman:

▶ let’s add the other propositional connectives … … in the parser and pretty-printer! parser and pretty-printer have to know about logic a proof assistant for propositional logic

course proof assistants at Radboud University Nijmegen

▶ implement small proof assistant LCF-style proof assistant minimal propositional logic (= only implication)

\overline{Γ ∪ \{A\} ⊢ A} \frac{Γ ∪ \{A\} ⊢ B}{Γ ⊢ A → B} \frac{Γ ⊢ A → B Γ ⊢ A}{Γ ⊢ B}

student Marc Schoolderman:

▶ let’s add the other propositional connectives … … in the parser and pretty-printer! parser and pretty-printer have to know about logic a proof assistant for propositional logic

course proof assistants at Radboud University Nijmegen

▶ implement small proof assistant LCF-style proof assistant minimal propositional logic (= only implication)

\overline{\{A\} ⊢ A} \frac{Γ ⊢ B}{Γ − \{A\} ⊢ A → B} \frac{Γ ⊢ A → B Δ ⊢ A}{Γ ∪ Δ ⊢ B}

student Marc Schoolderman:

▶ let’s add the other propositional connectives … … in the parser and pretty-printer! parser and pretty-printer have to know about logic a proof assistant for propositional logic

course proof assistants at Radboud University Nijmegen

▶ implement small proof assistant LCF-style proof assistant minimal propositional logic (= only implication)

\overline{\{A\} ⊢ A} \frac{Γ ⊢ B}{Γ − \{A\} ⊢ A → B} \frac{Γ ⊢ A → B Δ ⊢ A}{Γ ∪ Δ ⊢ B}

student Marc Schoolderman:

▶ let’s add the other propositional connectives … … in the parser and pretty-printer! parser and pretty-printer have to know about logic a proof assistant for propositional logic

course proof assistants at Radboud University Nijmegen

▶ implement small proof assistant LCF-style proof assistant minimal propositional logic (= only implication)

\overline{\{A\} ⊢ A} \frac{Γ ⊢ B}{Γ − \{A\} ⊢ A → B} \frac{Γ ⊢ A → B Δ ⊢ A}{Γ ∪ Δ ⊢ B}

student Marc Schoolderman:

▶ let’s add the other propositional connectives … … in the parser and pretty-printer! parser and pretty-printer have to know about logic a proof assistant for propositional logic

course proof assistants at Radboud University Nijmegen

▶ implement small proof assistant LCF-style proof assistant minimal propositional logic (= only implication)

\overline{\{A\} ⊢ A} \frac{Γ ⊢ B}{Γ − \{A\} ⊢ A → B} \frac{Γ ⊢ A → B Δ ⊢ A}{Γ ∪ Δ ⊢ B}

student Marc Schoolderman:

▶ let’s add the other propositional connectives … … in the parser and pretty-printer! parser and pretty-printer have to know about logic

III

the digits of hundred factorial the kernel of HOL Light

proof assistant that best satisfies the de Bruijn criterion: HOL Light, John Harrison, 1998–today proof checking kernel = fusion.ml 671 lines ≈ 10 printed pages ≈ 0.2 % of the system only 395 lines of actual code self-verification of HOL Light: John Harrison, 2006 the kernel of HOL Light

proof assistant that best satisfies the de Bruijn criterion: HOL Light, John Harrison, 1998–today proof checking kernel = fusion.ml 671 lines ≈ 10 printed pages ≈ 0.2 % of the system only 395 lines of actual code self-verification of HOL Light: John Harrison, 2006 the kernel of HOL Light

proof assistant that best satisfies the de Bruijn criterion: HOL Light, John Harrison, 1998–today proof checking kernel = fusion.ml 671 lines ≈ 10 printed pages ≈ 0.2 % of the system only 395 lines of actual code self-verification of HOL Light: John Harrison, 2006 the kernel of HOL Light

proof assistant that best satisfies the de Bruijn criterion:

HOL Light, John Harrison, 1998–today

proof checking kernel = fusion.ml

671 lines ≈ 10 printed pages ≈ 0.2 % of the system only 395 lines of actual code

self-verification of HOL Light: John Harrison, 2006

let rec type_of tm =
  match tm with
    Var(_,ty) -> ty
  | Const(_,ty) -> ty
  | Comb(s,_) -> hd(tl(snd(dest_type(type_of s))))
  | Abs(Var(_,ty),t) -> Tyapp("fun",[ty;type_of t])

the kernel of HOL Light

proof assistant that best satisfies the de Bruijn criterion:

HOL Light, John Harrison, 1998–today

proof checking kernel = fusion.ml

671 lines ≈ 10 printed pages ≈ 0.2 % of the system only 395 lines of actual code

self-verification of HOL Light: John Harrison, 2006

let typeof = define
 `(typeof (Var n ty) = ty) /\
  (typeof (Equal ty) = Fun ty (Fun ty Bool)) /\
  (typeof (Select ty) = Fun (Fun ty Bool) ty) /\
  (typeof (Comb s t) = codomain (typeof s)) /\
  (typeof (Abs n ty t) = Fun ty (typeof t))`;;

numerical calculations in HOL Light

# `1 + 1`;;
val it : term = `1 + 1`
# NUM_REDUCE_CONV it;;
val it : thm = |- 1 + 1 = 2
# rhs (concl it);;
val it : term = `2`
# #remove_printer print_qterm;;
# it;;
val it : term =
  Comb (Const ("NUMERAL", `:num->num`),
   Comb (Const ("BIT0", `:num->num`),
    Comb (Const ("BIT1", `:num->num`), Const ("_0", `:num`))))
# #install_printer print_qterm;;
# `NUMERAL (BIT0 (BIT1 _0))`;;
val it : term = `2`
#
# rhs (concl (NUM_REDUCE_CONV `FACT 100`));;
val it : term =
  `93326215443944152681699238856266700490715968264381621468592963895217599993229915608941463976156518286253697920827223758251185210916864000000000000000000000000`
#

numerical calculations in HOL Light

# `1 + 1`;;
val it : term = `1 + 1`
# NUM_REDUCE_CONV it;;
val it : thm = |- 1 + 1 = 2
# rhs (concl it);;
val it : term = `2`
# #remove_printer print_qterm;;
# it;;
val it : term =
  Comb (Const ("NUMERAL", `:num->num`),
   Comb (Const ("BIT0", `:num->num`),
    Comb (Const ("BIT1", `:num->num`), Const ("_0", `:num`))))
# #install_printer print_qterm;;
# `NUMERAL (BIT0 (BIT1 _0))`;;
val it : term = `2`
#
# rhs (concl (NUM_REDUCE_CONV `FACT 100`));;
val it : term =
  `93326215443944152681699238856266700490715968264381621468592963895217599993229915608941463976156518286253697920827223758251185210916864000000000000000000000000`
#

numerical calculations in HOL Light

# `1 + 1`;;
val it : term = `1 + 1`
# NUM_REDUCE_CONV it;;
val it : thm = |- 1 + 1 = 2
# rhs (concl it);;
val it : term = `2`
# #remove_printer print_qterm;;
# it;;
val it : term =
  Comb (Const ("NUMERAL", `:num->num`),
   Comb (Const ("BIT0", `:num->num`),
    Comb (Const ("BIT1", `:num->num`), Const ("_0", `:num`))))
# #install_printer print_qterm;;
# `NUMERAL (BIT0 (BIT1 _0))`;;
val it : term = `2`
#
# rhs (concl (NUM_REDUCE_CONV `FACT 100`));;
val it : term =
  `93326215443944152681699238856266700490715968264381621468592963895217599993229915608941463976156518286253697920827223758251185210916864000000000000000000000000`
#

numerical calculations in HOL Light

# `1 + 1`;;
val it : term = `1 + 1`
# NUM_REDUCE_CONV it;;
val it : thm = |- 1 + 1 = 2
# rhs (concl it);;
val it : term = `2`
# #remove_printer print_qterm;;
# it;;
val it : term =
  Comb (Const ("NUMERAL", `:num->num`),
   Comb (Const ("BIT0", `:num->num`),
    Comb (Const ("BIT1", `:num->num`), Const ("_0", `:num`))))
# #install_printer print_qterm;;
# `NUMERAL (BIT0 (BIT1 _0))`;;
val it : term = `2`
#
# rhs (concl (NUM_REDUCE_CONV `FACT 100`));;
val it : term =
  `93326215443944152681699238856266700490715968264381621468592963895217599993229915608941463976156518286253697920827223758251185210916864000000000000000000000000`
#

numerical calculations in HOL Light

# `1 + 1`;;
val it : term = `1 + 1`
# NUM_REDUCE_CONV it;;
val it : thm = |- 1 + 1 = 2
# rhs (concl it);;
val it : term = `2`
# #remove_printer print_qterm;;
# it;;
val it : term =
  Comb (Const ("NUMERAL", `:num->num`),
   Comb (Const ("BIT0", `:num->num`),
    Comb (Const ("BIT1", `:num->num`), Const ("_0", `:num`))))
# #install_printer print_qterm;;
# `NUMERAL (BIT0 (BIT1 _0))`;;
val it : term = `2`
#
# rhs (concl (NUM_REDUCE_CONV `FACT 100`));;
val it : term =
  `93326215443944152681699238856266700490715968264381621468592963895217599993229915608941463976156518286253697920827223758251185210916864000000000000000000000000`
#

numerical calculations in HOL Light

# `1 + 1`;;
val it : term = `1 + 1`
# NUM_REDUCE_CONV it;;
val it : thm = |- 1 + 1 = 2
# rhs (concl it);;
val it : term = `2`
# #remove_printer print_qterm;;
# it;;
val it : term =
  Comb (Const ("NUMERAL", `:num->num`),
   Comb (Const ("BIT0", `:num->num`),
    Comb (Const ("BIT1", `:num->num`), Const ("_0", `:num`))))
# #install_printer print_qterm;;
# `NUMERAL (BIT0 (BIT1 _0))`;;
val it : term = `2`
#
# rhs (concl (NUM_REDUCE_CONV `FACT 100`));;
val it : term =
  `93326215443944152681699238856266700490715968264381621468592963895217599993229915608941463976156518286253697920827223758251185210916864000000000000000000000000`
#

numerical calculations in HOL Light

# `1 + 1`;;
val it : term = `1 + 1`
# NUM_REDUCE_CONV it;;
val it : thm = |- 1 + 1 = 2
# rhs (concl it);;
val it : term = `2`
# #remove_printer print_qterm;;
# it;;
val it : term =
  Comb (Const ("NUMERAL", `:num->num`),
   Comb (Const ("BIT0", `:num->num`),
    Comb (Const ("BIT1", `:num->num`), Const ("_0", `:num`))))
# #install_printer print_qterm;;
# `NUMERAL (BIT0 (BIT1 _0))`;;
val it : term = `2`
#
# rhs (concl (NUM_REDUCE_CONV `FACT 100`));;
val it : term =
  `93326215443944152681699238856266700490715968264381621468592963895217599993229915608941463976156518286253697920827223758251185210916864000000000000000000000000`
#

numerical calculations in HOL Light

# `1 + 1`;;
val it : term = `1 + 1`
# NUM_REDUCE_CONV it;;
val it : thm = |- 1 + 1 = 2
# rhs (concl it);;
val it : term = `2`
# #remove_printer print_qterm;;
# it;;
val it : term =
  Comb (Const ("NUMERAL", `:num->num`),
   Comb (Const ("BIT0", `:num->num`),
    Comb (Const ("BIT1", `:num->num`), Const ("_0", `:num`))))
# #install_printer print_qterm;;
# `NUMERAL (BIT0 (BIT1 _0))`;;
val it : term = `2`
#
# rhs (concl (NUM_REDUCE_CONV `FACT 100`));;
val it : term =
  `93326215443944152681699238856266700490715968264381621468592963895217599993229915608941463976156518286253697920827223758251185210916864000000000000000000000000`
#

IV Pollack-inconsistency the structure of a proof assistant

proof checking kernel

remainder of the system: theorem database, basic reasoning,

rewriting, back-chaining, proof search, decision procedures,

etc.

the structure of a proof assistant

interface proof checking kernel

remainder of the system: theorem database, basic reasoning,

rewriting, back-chaining, proof search, decision procedures,

etc.

the structure of a proof assistant

interface proof checking kernel

remainder of the system: theorem database, basic reasoning,

rewriting, back-chaining, proof search, decision procedures,

etc. parser

printer editor

the structure of a proof assistant

interface proof checking kernel

remainder of the system: theorem database, basic reasoning,

rewriting, back-chaining, proof search, decision procedures,

etc. formula parser

formula printer editor

the structure of a proof assistant

interface proof checking kernel

remainder of the system: theorem database, basic reasoning,

rewriting, back-chaining, proof search, decision procedures,

etc. formula parser

formula printer editor

is parsing the left inverse of pretty-printing?

formula parser and pretty-printer:

parse_{f} : string → formula
print_{f} : formula → string

generally print_{f} is total while parse_{f} is not

‘well-behaved’:  parse_{f}(print_{f}(ϕ)) = ϕ

in practice well-behavedness occasionally breaks

print_{f}(parse_{f}(s)) ≠ s is parsing the left inverse of pretty-printing?

formula parser and pretty-printer:

parse_{f} : string → formula
print_{f} : formula → string

generally print_{f} is total while parse_{f} is not

‘well-behaved’:  parse_{f}(print_{f}(ϕ)) = ϕ

in practice well-behavedness occasionally breaks

print_{f}(parse_{f}(s)) ≠ s is parsing the left inverse of pretty-printing?

formula parser and pretty-printer:

parse_{f} : string → formula
print_{f} : formula → string

generally print_{f} is total while parse_{f} is not

‘well-behaved’:  parse_{f}(print_{f}(ϕ)) = ϕ

in practice well-behavedness occasionally breaks

print_{f}(parse_{f}(s)) ≠ s is parsing the left inverse of pretty-printing?

formula parser and pretty-printer:

parse_{f} : string → formula
print_{f} : formula → string

generally print_{f} is total while parse_{f} is not

‘well-behaved’:  parse_{f}(print_{f}(ϕ)) = ϕ

in practice well-behavedness occasionally breaks

print_{f}(parse_{f}(s)) ≠ s is parsing the left inverse of pretty-printing?

formula parser and pretty-printer:

parse_{f} : string → formula
print_{f} : formula → string

generally print_{f} is total while parse_{f} is not

‘well-behaved’:  parse_{f}(print_{f}(ϕ)) = ϕ

in practice well-behavedness occasionally breaks

print_{f}(parse_{f}(s)) ≠ s Pollack-axioms and Pollack-inconsistency

Pollack-inconsistency:

‘⊥ is provable from Pollack-axioms’

Pollack-axioms:

‘ϕ_{1} ⇔ ϕ_{2}’ when print_{f}(ϕ_{1}) = print_{f}(ϕ_{2})
‘t_{1} = t_{2}’ when print_{t}(t_{1}) = print_{t}(t_{2})

▶ default printer with default settings

▶ default equality

Coq: ‘Leibniz equality’ ▶ only t_{1} and t_{2} for which t_{1} = t_{2} is well-typed Pollack-axioms and Pollack-inconsistency

Pollack-inconsistency:

‘⊥ is provable from Pollack-axioms’

Pollack-axioms:

‘ϕ_{1} ⇔ ϕ_{2}’ when print_{f}(ϕ_{1}) = print_{f}(ϕ_{2})
‘t_{1} = t_{2}’ when print_{t}(t_{1}) = print_{t}(t_{2})

▶ default printer with default settings

▶ default equality

Coq: ‘Leibniz equality’ ▶ only t_{1} and t_{2} for which t_{1} = t_{2} is well-typed Pollack-axioms and Pollack-inconsistency

Pollack-inconsistency:

‘⊥ is provable from Pollack-axioms’

Pollack-axioms:

‘ϕ_{1} ⇔ ϕ_{2}’ when print_{f}(ϕ_{1}) = print_{f}(ϕ_{2})
‘t_{1} = t_{2}’ when print_{t}(t_{1}) = print_{t}(t_{2})

▶ default printer with default settings

▶ default equality

Coq: ‘Leibniz equality’ ▶ only t_{1} and t_{2} for which t_{1} = t_{2} is well-typed Pollack-axioms and Pollack-inconsistency

Pollack-inconsistency:

‘⊥ is provable from Pollack-axioms’

Pollack-axioms:

‘ϕ_{1} ⇔ ϕ_{2}’ when print_{f}(ϕ_{1}) = print_{f}(ϕ_{2})
‘t_{1} = t_{2}’ when print_{t}(t_{1}) = print_{t}(t_{2})

▶ default printer with default settings

▶ default equality

Coq: ‘Leibniz equality’ ▶ only t_{1} and t_{2} for which t_{1} = t_{2} is well-typed weak versus strong Pollack-inconsistency

strong Pollack-inconsistency = … without adding definitions

weak Pollack-inconsistency = … extra definitions allowed

▶ … on top of the standard library of the system

▶ only conservative definitions

same provable formulas not involving the new definition

▶ notations considered a form of definition

Coq: coercions Pollack-super-inconsistency

Pollack-super-inconsistency =

ϕ is provable with print_{f}(ϕ) = print_{f}(⊥)

where

            ⊥ = \{ \begin{matrix}F & HOL \\ False & Isabelle \\ False & Coq \\ contradiction & Mizar \end{matrix} \}

Pollack-super-inconsistency

Pollack-super-inconsistency =

ϕ is provable with print_{f}(ϕ) = print_{f}(⊥)

where

            ⊥ = \{ \begin{matrix}F & HOL \\ False & Isabelle \\ False & Coq \\ contradiction & Mizar \end{matrix} \}

V

some of the best proof assistants are Pollack-inconsistent HOL Light^{12}

# `?!x:1. T`;;
val it : term = `?!x. T`
# `?!x:bool. T`;;
val it : term = `?!x. T`
# mk_eq(mk_var("0",`:1`),mk_var("1",`:1`));;
val it : term = `0 = 1`
# prove(it, ONCE_REWRITE_TAC[one] THEN REFL_TAC);;
val it : thm = |- 0 = 1
# override_interface("F",`T`);;
val it : unit = ()
# mk_const("F",[]);;
val it : term = `F`
# `T`;;
val it : term = `F`
# prove(`F`, ACCEPT_TAC TRUTH);;
val it : thm = |- F
#

HOL Light (and Isabelle)

# `?!x:1. T`;;
val it : term = `?!x. T`
# `?!x:bool. T`;;
val it : term = `?!x. T`
# mk_eq(mk_var("0",`:1`),mk_var("1",`:1`));;
val it : term = `0 = 1`
# prove(it, ONCE_REWRITE_TAC[one] THEN REFL_TAC);;
val it : thm = |- 0 = 1
# override_interface("F",`T`);;
val it : unit = ()
# mk_const("F",[]);;
val it : term = `F`
# `T`;;
val it : term = `F`
# prove(`F`, ACCEPT_TAC TRUTH);;
val it : thm = |- F
#

HOL Light (and Isabelle)

# `?!x:1. T`;;
val it : term = `?!x. T`
# `?!x:bool. T`;;
val it : term = `?!x. T`
# mk_eq(mk_var("0",`:1`),mk_var("1",`:1`));;
val it : term = `0 = 1`
# prove(it, ONCE_REWRITE_TAC[one] THEN REFL_TAC);;
val it : thm = |- 0 = 1
# override_interface("F",`T`);;
val it : unit = ()
# mk_const("F",[]);;
val it : term = `F`
# `T`;;
val it : term = `F`
# prove(`F`, ACCEPT_TAC TRUTH);;
val it : thm = |- F
#

HOL Light (and Isabelle)

# `?!x:1. T`;;
val it : term = `?!x. T`
# `?!x:bool. T`;;
val it : term = `?!x. T`
# mk_eq(mk_var("0",`:1`),mk_var("1",`:1`));;
val it : term = `0 = 1`
# prove(it, ONCE_REWRITE_TAC[one] THEN REFL_TAC);;
val it : thm = |- 0 = 1
# override_interface("F",`T`);;
val it : unit = ()
# mk_const("F",[]);;
val it : term = `F`
# `T`;;
val it : term = `F`
# prove(`F`, ACCEPT_TAC TRUTH);;
val it : thm = |- F
#

HOL Light (and Isabelle)

# `?!x:1. T`;;
val it : term = `?!x. T`
# `?!x:bool. T`;;
val it : term = `?!x. T`
#
# mk_eq(mk_var("0",`:1`),mk_var("1",`:1`));;
val it : term = `0 = 1`
# prove(it, ONCE_REWRITE_TAC[one] THEN REFL_TAC);;
val it : thm = |- 0 = 1
# override_interface("F",`T`);;
val it : unit = ()
# mk_const("F",[]);;
val it : term = `F`
# `T`;;
val it : term = `F`
# prove(`F`, ACCEPT_TAC TRUTH);;
val it : thm = |- F
#

HOL Light (and Isabelle)

# `?!x:1. T`;;
val it : term = `?!x. T`
# `?!x:bool. T`;;
val it : term = `?!x. T`
# mk_eq(mk_var("0",`:1`),mk_var("1",`:1`));;
val it : term = `0 = 1`
# prove(it, ONCE_REWRITE_TAC[one] THEN REFL_TAC);;
val it : thm = |- 0 = 1
# override_interface("F",`T`);;
val it : unit = ()
# mk_const("F",[]);;
val it : term = `F`
# `T`;;
val it : term = `F`
# prove(`F`, ACCEPT_TAC TRUTH);;
val it : thm = |- F
#

HOL Light (and Isabelle)

# `?!x:1. T`;;
val it : term = `?!x. T`
# `?!x:bool. T`;;
val it : term = `?!x. T`
# mk_eq(mk_var("0",`:1`),mk_var("1",`:1`));;
val it : term = `0 = 1`
# prove(it, ONCE_REWRITE_TAC[one] THEN REFL_TAC);;
val it : thm = |- 0 = 1
# override_interface("F",`T`);;
val it : unit = ()
# mk_const("F",[]);;
val it : term = `F`
# `T`;;
val it : term = `F`
# prove(`F`, ACCEPT_TAC TRUTH);;
val it : thm = |- F
#

HOL Light (and Isabelle)

# `?!x:1. T`;;
val it : term = `?!x. T`
# `?!x:bool. T`;;
val it : term = `?!x. T`
# mk_eq(mk_var("0",`:1`),mk_var("1",`:1`));;
val it : term = `0 = 1`
# prove(it, ONCE_REWRITE_TAC[one] THEN REFL_TAC);;
val it : thm = |- 0 = 1
#
# override_interface("F",`T`);;
val it : unit = ()
# mk_const("F",[]);;
val it : term = `F`
# `T`;;
val it : term = `F`
# prove(`F`, ACCEPT_TAC TRUTH);;
val it : thm = |- F
#

HOL Light (and Isabelle)

# `?!x:1. T`;;
val it : term = `?!x. T`
# `?!x:bool. T`;;
val it : term = `?!x. T`
# mk_eq(mk_var("0",`:1`),mk_var("1",`:1`));;
val it : term = `0 = 1`
# prove(it, ONCE_REWRITE_TAC[one] THEN REFL_TAC);;
val it : thm = |- 0 = 1
# override_interface("F",`T`);;
val it : unit = ()
# mk_const("F",[]);;
val it : term = `F`
# `T`;;
val it : term = `F`
# prove(`F`, ACCEPT_TAC TRUTH);;
val it : thm = |- F
#

HOL Light (and Isabelle)

# `?!x:1. T`;;
val it : term = `?!x. T`
# `?!x:bool. T`;;
val it : term = `?!x. T`
# mk_eq(mk_var("0",`:1`),mk_var("1",`:1`));;
val it : term = `0 = 1`
# prove(it, ONCE_REWRITE_TAC[one] THEN REFL_TAC);;
val it : thm = |- 0 = 1
# override_interface("F",`T`);;
val it : unit = ()
# mk_const("F",[]);;
val it : term = `F`
# `T`;;
val it : term = `F`
# prove(`F`, ACCEPT_TAC TRUTH);;
val it : thm = |- F
#

HOL Light (and Isabelle)

# `?!x:1. T`;;
val it : term = `?!x. T`
# `?!x:bool. T`;;
val it : term = `?!x. T`
# mk_eq(mk_var("0",`:1`),mk_var("1",`:1`));;
val it : term = `0 = 1`
# prove(it, ONCE_REWRITE_TAC[one] THEN REFL_TAC);;
val it : thm = |- 0 = 1
# override_interface("F",`T`);;
val it : unit = ()
# mk_const("F",[]);;
val it : term = `F`
# `T`;;
val it : term = `F`
# prove(`F`, ACCEPT_TAC TRUTH);;
val it : thm = |- F
#

Coq^{13}

Coq < Coercion S : nat >-> nat.
S is now a coercion
Coq < Check 0.
0
     : nat
Coq < Check 1.
0
     : nat
Coq < Definition _Prop := Prop.
_Prop is defined
Coq < Definition _not : _Prop -> Prop := not.
_not is defined
Coq < Coercion _not : _Prop >-> Sortclass.
_not is now a coercion

Coq^{13}

Coq < Coercion S : nat >-> nat.
S is now a coercion
Coq < Check 0.
0
     : nat
Coq < Check 1.
0
     : nat
Coq < Definition _Prop := Prop.
_Prop is defined
Coq < Definition _not : _Prop -> Prop := not.
_not is defined
Coq < Coercion _not : _Prop >-> Sortclass.
_not is now a coercion

Coq^{13}

Coq < Coercion S : nat >-> nat.
S is now a coercion
Coq < Check 0.
0
     : nat
Coq < Check 1.
0
     : nat
Coq < Definition _Prop := Prop.
_Prop is defined
Coq < Definition _not : _Prop -> Prop := not.
_not is defined
Coq < Coercion _not : _Prop >-> Sortclass.
_not is now a coercion

Coq^{13}

Coq < Coercion S : nat >-> nat.
S is now a coercion
Coq < Check 0.
0
     : nat
Coq < Check 1.
0
     : nat
Coq < Definition _Prop := Prop.
_Prop is defined
Coq < Definition _not : _Prop -> Prop := not.
_not is defined
Coq < Coercion _not : _Prop >-> Sortclass.
_not is now a coercion

Coq^{13}

Coq < Coercion S : nat >-> nat.
S is now a coercion
Coq < Check 0.
0
     : nat
Coq < Check 1.
0
     : nat
Coq < Definition _Prop := Prop.
_Prop is defined
Coq < Definition _not : _Prop -> Prop := not.
_not is defined
Coq < Coercion _not : _Prop >-> Sortclass.
_not is now a coercion

Coq (continued)

Coq < Coercion _not : _Prop >-> Sortclass.
_not is now a coercion
Coq < Lemma _I : _not False.
1 subgoal
  ============================
   False
_I < exact (fun x => x).
Proof completed.
_I < Qed.
exact (fun x => x).
_I is defined
Coq < Check _I.
_I
     : False

Coq (continued)

Coq < Coercion _not : _Prop >-> Sortclass.
_not is now a coercion
Coq < Lemma _I : _not False.
1 subgoal
  ============================
   False
_I < exact (fun x => x).
Proof completed.
_I < Qed.
exact (fun x => x).
_I is defined
Coq < Check _I.
_I
     : False

Coq (continued)

Coq < Coercion _not : _Prop >-> Sortclass.
_not is now a coercion
Coq < Lemma _I : _not False.
1 subgoal
  ============================
   False
_I < exact (fun x => x).
Proof completed.
_I < Qed.
exact (fun x => x).
_I is defined
Coq < Check _I.
_I
     : False

Mizar^{15}

definition let x be real number;
  func [x] equals 1; coherence;
end;
definition let x be natural number;
  func [x] equals 0; coherence;
end;
theorem [0] <> [0 qua real number];

theorem theorem :: POLLACK:1
  [0 ] <> [0 ] ;

\overline{}

Mizar^{15}

definition let x be real number;
  func [x] equals 1; coherence;
end;
definition let x be natural number;
  func [x] equals 0; coherence;
end;
theorem [0] <> [0 qua real number];

theorem theorem :: POLLACK:1
  [0 ] <> [0 ] ;

\overline{}

Mizar^{15}

definition let x be real number;
  func [x] equals 1; coherence;
end;
definition let x be natural number;
  func [x] equals 0; coherence;
end;
theorem [0] <> [0 qua real number];

theorem theorem :: POLLACK:1
  [0 ] <> [0 ] ;

\overline{}

Mizar^{15}

definition let x be real number;
  func [x] equals 1; coherence;
end;
definition let x be natural number;
  func [x] equals 0; coherence;
end;
theorem [0] <> [0 qua real number];

theorem theorem :: POLLACK:1
  [0 ] <> [0 ] ;

\overline{}

Mizar^{15}

definition let x be real number;
  func [x] equals 1; coherence;
end;
definition let x be natural number;
  func [x] equals 0; coherence;
end;
theorem [0] <> [0 qua real number];

theorem theorem :: POLLACK:1
  [0 ] <> [0 ] ;

\overline{}

Mizar^{15}

definition let x be real number;
  func [x] equals 1; coherence;
end;
definition let x be natural number;
  func [x] equals 0; coherence;
end;
theorem [0] <> [0 qua real number];

theorem theorem :: POLLACK:1
  [0 ] <> [0 ] ;

\overline{}

Mizar^{15}

definition let x be real number;
  func [x] equals 1; coherence;
end;
definition let x be natural number;
  func [x] equals 0; coherence;
end;
theorem [0] <> [0 qua real number];

theorem theorem :: POLLACK:1
  [0 ] <> [0 ] ;

\overline{}

VI

Pollack-consistency on the cheap checking the pretty-printer at runtime

‘hack’ for making it easier to prove Pollack-consistency

▶ print_{normal}

good, complicated

▶ print_{failsafe}

failsafe, trivial

combine into print_{combined}:

s := print_{normal}(ϕ)

parse(s) = ϕ?

[figure] [figure] [figure]

no

yes

return s

parse(print_{failsafe}(ϕ)) = ϕ ⇓ parse(print_{combined}(ϕ)) = ϕ checking the pretty-printer at runtime

return print_{failsafe}(ϕ)

‘hack’ for making it easier to prove Pollack-consistency

▶ print_{normal}

good, complicated

▶ print_{failsafe}

failsafe, trivial

combine into print_{combined}:

s := print_{normal}(ϕ)

parse(s) = ϕ?

[figure] [figure] [figure]

no

yes

return s

parse(print_{failsafe}(ϕ)) = ϕ ⇓ parse(print_{combined}(ϕ)) = ϕ checking the pretty-printer at runtime

return print_{failsafe}(ϕ)

‘hack’ for making it easier to prove Pollack-consistency

▶ print_{normal}

good, complicated

▶ print_{failsafe}

failsafe, trivial

combine into print_{combined}:

s := print_{normal}(ϕ)

parse(s) = ϕ?

[figure] [figure] [figure]

no

yes

return s

parse(print_{failsafe}(ϕ)) = ϕ ⇓ parse(print_{combined}(ϕ)) = ϕ checking the pretty-printer at runtime

return print_{failsafe}(ϕ)

‘hack’ for making it easier to prove Pollack-consistency

▶ print_{normal}

good, complicated

▶ print_{failsafe}

failsafe, trivial

combine into print_{combined}:

s := print_{normal}(ϕ)

parse(s) = ϕ?

[figure] [figure] [figure]

no

yes

return s

parse(print_{failsafe}(ϕ)) = ϕ ⇓ parse(print_{combined}(ϕ)) = ϕ

return print_{failsafe}(ϕ)

VII

does Pollack-inconsistency matter? the attitude of the proof assistants community

computer algebra users a little inconsistency does not matter much …

>
> evalf(subs(x=-1, %));

−0.6931471806 = −0.6931471806 − 3.141592654i

proof assistant users consistency is very important! a little Pollack-inconsistency does not matter much … the attitude of the proof assistants community

computer algebra users a little inconsistency does not matter much …

> 1/(1-x) = simplify(1/(1-x))

\frac{1}{1 − x} = − \frac{1}{−1 + x}

> evalf(subs(x=-1, %));

−0.6931471806 = −0.6931471806 − 3.141592654i

proof assistant users consistency is very important! a little Pollack-inconsistency does not matter much … the attitude of the proof assistants community

computer algebra users a little inconsistency does not matter much …

> int(1/(1-x),x) = int(simplify(1/(1-x)),x)

− ln(1 − x) = − ln(−1 + x)

> evalf(subs(x=-1, %));

−0.6931471806 = −0.6931471806 − 3.141592654i

proof assistant users consistency is very important! a little Pollack-inconsistency does not matter much … the attitude of the proof assistants community

computer algebra users a little inconsistency does not matter much …

> int(1/(1-x),x) = int(simplify(1/(1-x)),x)

− ln(1 − x) = − ln(−1 + x)

> evalf(subs(x=-1, %));

−0.6931471806 = −0.6931471806 − 3.141592654i

proof assistant users consistency is very important! a little Pollack-inconsistency does not matter much … the attitude of the proof assistants community

computer algebra users a little inconsistency does not matter much …

> int(1/(1-x),x) = int(simplify(1/(1-x)),x)

− ln(1 − x) = − ln(−1 + x)

> evalf(subs(x=-1, %));

−0.6931471806 = −0.6931471806 − 3.141592654i

proof assistant users consistency is very important! a little Pollack-inconsistency does not matter much … the attitude of the proof assistants community

computer algebra users a little inconsistency does not matter much …

> int(1/(1-x),x) = int(simplify(1/(1-x)),x)

− ln(1 − x) = − ln(−1 + x)

> evalf(subs(x=-1, %));

−0.6931471806 = −0.6931471806 − 3.141592654i

proof assistant users consistency is very important! a little Pollack-inconsistency does not matter much … the attitude of the proof assistants community

computer algebra users a little inconsistency does not matter much …

> int(1/(1-x),x) = int(simplify(1/(1-x)),x)

− ln(1 − x) = − ln(−1 + x)

> evalf(subs(x=-1, %));

−0.6931471806 = −0.6931471806 − 3.141592654i

proof assistant users apart from principled people like Randy Pollack and Mark Adams consistency is very important! a little Pollack-inconsistency does not matter much …