a Mizar mode for Coq?

Freek Wiedijk University of Nijmegen

Math-in-Coq meeting Laboratoire de Recherche en Informatique CNRS/Université Paris-Sud Orsay

2003 04 24, 09:30 wishes

• predicative Set

• tactics in terms

[x,y:F; H:~y=0](div x y <% Assumption %>)

simulate type-correctness conditions like in PVS

• overloading based on argument types A /\ B notation both for Prop and Set

• uniform way to indicate labels to tactics ‘⟨tactic⟩ labeled ⟨labels⟩’

Intros A B C would be a special case of Intros labeled A B C

warning for labels that are still implicit

• block structured syntax for tactic scripts ⟨tactic⟩. \underbrace{Proof. … Qed. Proof. … Qed.}_{first n−1 generated subgoals} \underbrace{…}_{last subgoal} subject of the talk

[figure: Isabelle; Coq; Isar; ?]

a small language

a small grammar

proposition = [ label : ] formula
statement = proposition justification
justification = [ by label {, label}]
| proof {step ;} [ cases ] end
step = [ then ] statement
| assume proposition | let variable {, variable}
| thus statement | hence statement
| [ then ] consider variable {, variable}

such that proposition justification

| take term {, term}
cases = per cases justification ;

{suppose proposition ; {step ;}} example: infinity of primes

for n ex p st p is prime & p > n proof

let n ; n! > 0 by NEWTON : 23 ; then n! >= 0 + 1 by NAT 1 : 38 ; then n! + 1 >= 1 + 1 by REAL 1 : 55 ; then consider p such that

A1 : p is prime & p divides n! + 1 by INT 2 : 48 ; A2 : p <> 0 & p > 1 by A1, INT 2 : def 5 ;

take p ; thus p is prime by A1 ; assume p <= n ; then p divides n! by A2, NAT LAT : 16 ; then p divides 1 by A1, NAT 1 : 57 ; hence contradiction by A2, NAT 1 : 54 ;

end ; the basic Mizar proof step

A2 : p <> 0 & p > 1 by A1, INT 2 : def 5 ;

⟨label⟩: ⟨formula⟩ by ⟨references⟩; Coq analogue:

Cut ⟨formula⟩; [Intro ⟨label⟩ | Auto with ⟨references⟩]. ‘cut’ in the proof + automation of the easy part by: ‘small’ inference Mizar proofs: long lists of this kind of step many cuts! big contexts! then

generally a step refers to the previous step ‘… by ⟨label of previous step⟩’ may be written as ‘then … ’

so

A1 : ⟨formula⟩ by B0 ; A2 : ⟨other formula⟩ by A1,B1 ; A3 : ⟨third formula⟩ by A2,B2 ;

can be written as

⟨formula⟩ by B0 ; then ⟨other formula⟩ by B1 ; then A3 : ⟨third formula⟩ by B2 ; natural deduction steps

Mizar  Coq
→-intro  assume H : ⟨formula⟩;  Intro H.
∀-intro  let x;  Intro x.
∧-intro  thus ⟨formula⟩ by R;  Split; [Auto with R | Idtac].
∃-elim  consider x such that  Elim ⟨existential⟩;
H : ⟨formula⟩;  Intro x; Intro H.
∃-intro  take ⟨term⟩;  Exists ⟨term⟩.
∨-elim  per cases by ⟨refs⟩;  Elim ⟨disjunction⟩.
suppose H1 : ⟨formula⟩;  Intro H1.
⟨sub-proof⟩  ⟨sub-proof⟩
suppose H2 : ⟨formula⟩;  Intro H2.
⟨sub-proof⟩  ⟨sub-proof⟩

all other natural deduction rules: by a small grammar (continued)

step = … | set variable = term
statement = … | [ label : ] term = term justification

{.= term justification}

formula = … | thesis

some more features of the Mizar proof language: • local definitions

• iterative equalities

(x + y)^{2} = (x + y)(x + y)  by …
.= x(x + y) + y(x + y) by …
.= x^{2} + xy + yx + y^{2} by …
.= x^{2} + 2xy + y^{2}  by …;

Mizar modes

what’s a Mizar mode? full Mizar:

• proof language

• foundations (first order logic, ZFC-style set theory)

• type system (multiple types, sub-typing, ‘adjectives’, structures)

• automation (powerful type inference, very fast inference checking)

• expression syntax (heavy overloading, flexible operator syntax) Mizar mode: only the proof language on top of another system Mizar modes various systems that isolate the Mizar proof language from Mizar:

Andrzej Trybulec: baby Mizar (= Mizar MSE)
John Harrison: Mizar mode for HOL Light
Markus Wenzel: Isar for Isabelle
Freek Wiedijk: Mizar Light for HOL Light
Henk Barendregt: ‘math mode’ for Coq
(Bas Spitters: partial implementation using L_{tac} language)

only one serious system keywords

Mizar  Isar  ‘math mode’
⟨label⟩:  ⟨label⟩:  doesn’t exist
by  from, using  by
then  then, with  Then
proof/end  proof/qed  Proof/QED
no keyword  have  Then
thus  show  Then
hence  then show  Then
assume  assume  Assume/Towards
let  fix  Let
consider/such that  obtain/where  There exists/such that, Pick
take  doesn’t exist  Take
per cases/suppose  next assume  Case
set  let, def  doesn’t exist
thesis  ?thesis  doesn’t exist

synonyms keywords ⟷ meaning

• mature languages (Mizar, Isar): one-to-one

• Henk’s ‘math mode’: many-to-one

‘math mode’ synonyms Then = We have = It follows that = Hence = Moreover = Again Towards = Suffices = In order to show = We must show Let = Given

Mizar Light

experiment

[figure: Isabelle; HOL Light; Isar; Mizar Light II]

mixing procedural and declarative proof

• John’s Mizar mode for HOL Light & Isar for Isabelle: separate language on top of original system

• Mizar Light:

freely interleaving ‘old style’ tactics and Mizar style proof

just define 8 new tactics in the system: ‘Mizar tactics’ ‘imitate’ a Mizar proof in a tactic script

HOL/Mizar Light: a ‘proof’ is just an ML program no special parser on top of the ML interpreter Mizar Light tactic types

HOL ML types:

term, thm, tactic

Mizar Light tactics:

BY : string list → thm list → tactic HAVE : string × term → tactic → tactic ASSUME : string × term → tactic LET : term list → tactic THUS : string × term → tactic → tactic CONSIDER : term list → (string × term) list → tactic → tactic TAKE : term list → tactic PER_CASES : tactic → ((string × term) × tactic) list → tactic Mizar Light II Mizar Light: it’s all about concepts

   CONSIDER [`a:A`] ["A1",`~(P:A->bool) a`] (BY ["A0"][]) THEN

important features missing: no ‘then’ Mizar Light II: more practical version

            so consider ["a:A"] st "~P a" at 1;

but: ML types of the tactics less meaningful

step type instead of tactic type but: some renamings to fit ML syntax

⟨label⟩:  → at ⟨label⟩
then  → so
let  → fix
such that → st

translating a Coq proof to Mizar Light II Luís Cruz-Filipe: Fundamental Theorem of Calculus one of his lemmas translated into Mizar Light lemma: ‘Barrow’s rule’

g′ = f ⇒ ∫_{a}^{b} f(x) dx = g(b) − g(a) derivative g f ⇒ integral a b f = g b – g a

first order version proved from functional version: FTC2

g′ = f ⇒ ( ∫ f) − g = c the Coq version

Theorem Barrow : (a,b:IR)(iprop J a)->(iprop J b)->
  (H:(Continuous_I (Min_leEq_Max a b) F))(Ha,Hb:?)
  (Integral H)[=](G0[@]b (G0_inc b Hb))[-](G0[@]a (G0_inc a Ha)).
Intros.
Elim FTC2; Intros c Hc.
Inversion_clear Hc.
Inversion_clear H2.
RStepr ((G0[@]b (G0_inc b Hb))[+]c)[-]((G0[@]a (G0_inc a Ha))[+]c).
Apply eq_transitive_unfolded with (G[@]b Hb)[-](G[@]a Ha).
Unfold G; Simpl.
Cut (x,y,z:IR)(z[=]x[+]y)->(y[=]z[-]x); Intros.
Apply H2.
Apply Integral_plus_Integral with (Min3_leEq_Max3 x0 b a).
Apply included_imp_Continuous with J.
Auto.
Apply included3_interval; Auto. Apply eq_symmetric_unfolded.
RStepr (x[+]y)[-]x; Algebra.
Cut (x,y,z:IR)(x[-]y[=]z)->(x[=]y[+]z); Intros.

the Coq version (continued)

Opaque G.
Cut (x:IR)(iprop J x)->(Hx,Hx':?)(G[@]x Hx)[-](G0[@]x Hx')[=]c; Intros.
Apply cg_minus_wd; Apply H2; Auto.
Simpl in H3.
EApply eq_transitive_unfolded.
2: Apply H3 with Hx:=(Hx,Hx').
Algebra.
Auto.
Auto.
RStep y[+](x[-]y).
Algebra.
Qed.

the Mizar Light version

let Barrow = theorem
"!J f g0 a b.
   interval J /\ Continuous J f /\ Derivative J g0 f /\ a IN J /\ b IN J
   ==> (integral' a b f = g0 b - g0 a)"
[fix ["J:real->bool"; "f:real->real"; "g0:real->real"; "a:real"; "b:real"];
assume "interval J" at 0;
assume "Continuous J f" at 1;
assume "Derivative J g0 f" at 2;
assume "a IN J /\ b IN J" at 3;
consider ["x0:real"] st "x0 IN J" at 4 from [3];
so consider ["c:real"] st
  "Feq J (Fprim f x0 - g0) (Fconst c)" at 5 from [0;2] by [FTC2];
have "!x. x IN J ==> (integral' x0 x f = g0 x + c)" at 6
proof
 [fix ["x:real"];
  assume "x IN J";
  so have "(Fprim f x0 - g0) x = c" from [5] by [Feq; Fconst];
  so have "integral' x0 x f - g0 x = c" by [Fminus; Fprim];

the Mizar Light version (continued)

  hence thesis by [ARITH_CONV `(x - y = z) ==> (x = y + z)`]];
have "compact (x0 MIN b MIN a) (x0 MAX b MAX a) SUBSET J"
  from [0;3;4] by [included3_interval];
so have "continuous_I (x0 MIN b MIN a) (x0 MAX b MAX a) f"
  from [1] by [included_imp_Continuous];
so have "integral' x0 b f = integral' x0 a f + integral' a b f"
  by [Integral_plus_Integral];
so have "integral' a b f = integral' x0 b f - integral' x0 a f"
  by [ARITH_CONV `(z = x + y) ==> (y = z - x)`];
so have "... = (g0 b + c) - (g0 a + c)" from [3;6];
hence "... = g0 b - g0 a" using K ARITH_TAC using REWRITE_TAC];;

a formal proof sketch

current_prover := sketch_prover;;
let Barrow = theorem
"!J f g0 a b.
   interval J /\ Continuous J f /\ Derivative J g0 f /\ a IN J /\ b IN J
   ==> (integral' a b f = g0 b - g0 a)"
[fix ["J:real->bool"; "f:real->real"; "g0:real->real"; "a:real"; "b:real"];
assume "interval J; assume "Continuous J f"; assume "Derivative J g0 f";
assume "a IN J /\ b IN J";
consider ["x0:real"] st "x0 IN J";
consider ["c:real"] st "Feq J (Fprim f x0 - g0) (Fconst c)";
have "!x. x IN J ==> (integral' x0 x f = g0 x + c)";
have "integral' x0 b f = integral' x0 a f + integral' a b f";
have "integral' a b f = integral' x0 b f - integral' x0 a f";
have "... = (g0 b + c) - (g0 a + c)";
thus "... = g0 b - g0 a"];;

a shorter proof (formal proof sketch)

current_prover := sketch_prover;;
let Barrow = theorem
"!J f g0 a b.
   interval J /\ Derivative J g0 f /\ a IN J /\ b IN J
   ==> (integral' a b f = g0 b - g0 a)"
[fix ["J:real->bool"; "f:real->real"; "g0:real->real"; "a:real"; "b:real"];
assume "interval J"; assume "Derivative J g0 f";
assume "a IN J /\ b IN J";
consider ["c:real"] st "Feq J (Fprim f a - g0) (Fconst c)";
have "!x. x IN J ==> (integral' a x f - g0 x = c)";
have "integral' a a f = &0";
have "c = --g0 a";
have "integral' a b f - g0 b = c";
thus "integral' a b f = g0 b - g0 a"];;

a shorter proof (full proof)

let Barrow = theorem
"!J f g0 a b.
   interval J /\ Derivative J g0 f /\ a IN J /\ b IN J
   ==> (integral' a b f = g0 b - g0 a)"
[fix ["J:real->bool"; "f:real->real"; "g0:real->real"; "a:real"; "b:real"];
assume "interval J" at 0;
assume "Derivative J g0 f" at 1;
assume "a IN J /\ b IN J" at 2;
so consider ["c:real"] st
  "Feq J (Fprim f a - g0) (Fconst c)" from [0;1] by [FTC2];
so have "!x. x IN J ==> (integral' a x f - g0 x = c)" at 4
  using (REWRITE_TAC o map (REWRITE_RULE[Feq; Fconst; Fminus; Fprim]));
have "integral' a a f = &0" by [INTEGRAL'; INTEGRAL_NULL; REAL_LE_REFL];
so have "c = --g0 a" at 6 from [2;4] by [ARITH_CONV `&0 - x = --x`];
have "integral' a b f - g0 b = c" from [2;4];
hence thesis from [6] by [ARITH_CONV `(--y = w - x) ==> (w = x - y)`]];;

implementing a Mizar mode

the easy part implementing the ‘natural deduction’ behavior of the steps Mizar Light & Bas’ ‘math mode’ show: this is easy support for writing steps in a Mizar mode? Mizar steps need much more typing

Intro. → assume ⟨label⟩: ⟨formula⟩;

menu items to generate proof text: interactive mode but: having ‘meta-scripts’ to generate proof text is a bad idea the file that the user interacts with should be understandable! the hard part Mizar’s by tactic: not clear how to map it to Coq possibility:

• put all statements referred to in a hint class H

• solve sub-goal for the statement using: Intuition Auto with H how to write a ‘Mizar style’ proof that uses other tactics?

Elim? Induction? Inversion? Omega? Field? own tactics?

approach in Mizar Light:

… using ⟨tactic⟩;

my experience with this in practice: I don’t like it I want to think about the proof, not about why a tactic doesn’t work! working in an incomplete proof text

Mizar style of working: one often has to reprocess the whole proof when a change is made

Proof General: split between correct text and unprocessed text
Mizar: everything is checked everywhere all the time

working behind errors

explicit formulas make error recovery possible (like adding temporary axioms manually)

Mizar demo

conclusion

what needs to be done? someone should do a proper Mizar mode for Coq

• no significant change of the Coq system will be needed

• the problem of an appropriate by for Coq will need to be solved first