mmode

a Mizar mode for Coq by Mariusz Giero

Coq procedural proof

Mizar declarative proof

Mizar mode for Coq Henk: ‘mathematical mode’

‘Mariusz’ mode’ mmode [figure] everything else

[figure] proof style four mmode translations

• a basic Coq proof

Included_Add

• a complicated Coq proof from our C-CoRN library

FTA'
own tactics: Algebra, Rational

• a basic Mizar proof

min_przerobka_2

min(x, y) = \frac{x + y − |x − y|}{2}

• one of Henk’s ‘mathematical mode’ experiments

nat_factorizes

trying to keep it as simple to use as possible

our goal: just say

                   Require mmode.

• no special parser can’t use existing Coq keywords: LEt/MLet, MShow just a bunch of Coq tactics

• only L_{tac} tactics currently uses one ML level tactic: Msg no ML level tactics → no need for a special image

• needs a patch to Coq 7.4 ‘tactics that take tactics as arguments’ work in progress

demo