I finally understand how to translate between miz3 and straight HOL Light. I
profited from the Mizar-like code in the HOL Light tutorial p 76--78, which I
modified to
let consider th pf = SUBGOAL_THEN th CHOOSE_TAC THENL [pf; ALL_TAC];;
let state th pf = SUBGOAL_THEN th ASSUME_TAC THENL [pf; ALL_TAC];;
let statelab th lab pf = SUBGOAL_THEN th (LABEL_TAC lab) THENL [pf; ALL_TAC];;
let toprove th = SUBGOAL_THEN th ASSUME_TAC;;
let mby labs MesonList = MAP_EVERY (fun l -> USE_THEN l MP_TAC) labs THEN
(MESON_TAC MesonList);;
let soby labs MesonList = FIRST_ASSUM MP_TAC THEN MAP_EVERY
(fun l -> USE_THEN l MP_TAC) labs THEN (MESON_TAC MesonList);;
Using this code I mechanically turned a 35-line miz3 proof of
UniversalPropertyProduct
|- ∀ M A B f g.
f ∈ M → A ∧ g ∈ M → B
⇒ (∃! h. h ∈ M → A ∏ B ∧ FST ∘ (h,M) = f ∧ SND ∘ (h,M) = g)
into a 28-line tactics script with almost identical MESON solved at numbers:
42063, 42992, 2590, 2687, 4515, 70020
42063, 42992, 1757 1854 4173, 70020
The only purpose of my Mizar-like code is to replace long lines with much
shorter ones, as in
e(FIRST_ASSUM MP_TAC THEN USE_THEN "hDef" MP_TAC THEN USE_THEN "kOffM" MP_TAC
THEN
MESON_TAC[FUN_EQ_THM; ∉]);;
soby ["hDef"; "kOffM"] [FUN_EQ_THM; ∉]
As Rob explained, STRIP_ASSUME_TAC handles the miz3 cases, so there's no need
for special coding. My `toprove' could easily be removed, and `state th pf'
could be replaced by `statelab th "" pf'.
Here's my tactics script for UniversalPropertyProduct, together with the
definitions and lemmas needed and my modification of John's Mizar-like code,
first with more readable math characters, with working HOL Light code below.
I'm including the miz3 proof, and you can see it's practically the same as my
tactics script except the miz3 proof is prettier, far fewer backquotes,
double-quotes, square braces, parentheses and type annotations. I impressed
that Freek made the miz3 code so pretty, and got Ocaml to cache results, but
it's basically what I'm doing in my tactics script.
parse_as_infix("∉",(11, "right"));;
parse_as_infix("∏",(20, "right"));;
parse_as_infix("∘",(20, "right"));;
parse_as_infix("→",(13,"right"));;
let ∉ = new_definition
`∀ a:A l:A->bool. a ∉ l ⇔ ¬(a ∈ l)`;;
let CartesianProduct = new_definition
`∀ X Y. X ∏ Y = {x,y | x ∈ X ∧ y ∈ Y}`;;
let IN_CartesianProduct = prove
(`∀ X Y x y. x,y ∈ X ∏ Y ⇔ x ∈ X ∧ y ∈ Y`,
REWRITE_TAC[IN_ELIM_THM; CartesianProduct] THEN MESON_TAC[PAIR_EQ]);;
let FunctionSpace = new_definition
`∀ s t. s → t = {f | (∀ x. x ∈ s ⇒ f x ∈ t) ∧
∀ x. x ∉ s ⇒ f x = @y. T}`;;
let IN_FunctionSpace = prove
(`∀ s t f. f ∈ s → t
⇔ (∀ x. x ∈ s ⇒ f x ∈ t) ∧ ∀ x. x ∉ s ⇒ f x = @y. T`,
REWRITE_TAC[IN_ELIM_THM; FunctionSpace]);;
let FunctionComposition = new_definition
`∀ f:A->B s:A->bool g:B->C x.
(g ∘ (f,s)) x = if x ∈ s then g (f x) else @y:C. T`;;
let UniversalPropertyProduct = prove
(`∀ M:μ->bool A:α->bool B:β->bool f:μ->α g:μ->β .
f ∈ M → A ∧ g ∈ M → B
⇒ (∃! h. h ∈ M → A ∏ B ∧ FST ∘ (h,M) = f ∧ SND ∘ (h,M) = g)`,
REPEAT GEN_TAC THEN DISCH_THEN(LABEL_TAC "H1") THEN
consider `?h:μ->α#β. h = λx:μ. if x ∈ M then f x,g x else @y. T` (mby []
[]) THEN
statelab `∀ x:μ. (x ∈ M ⇒ (h:μ->α#β) x = f x,g x) ∧ (x ∉ M ⇒ h x = @y.
T)` "hDef"
(soby [] [∉]) THEN
statelab `∀ x:μ. x ∈ M ⇒ (h:μ->α#β) x ∈ A ∏ B` "hProd" (soby ["H1"]
[IN_FunctionSpace; IN_CartesianProduct]) THEN
state `∀ x:μ. x ∈ M ⇒ FST ((h:μ->α#β) x) = f x ∧ SND (h x) = g x`
(mby ["hDef"] [FST_DEF; SND_DEF; PAIR_EQ]) THEN
state `∀ x:μ. (x ∈ M ⇒ (FST ∘ ((h:μ->α#β),M)) x = f x) ∧ (x ∉ M ⇒ (FST ∘
(h,M)) x = f x) ∧
(x ∈ M ⇒ (SND ∘ (h,M)) x = g x) ∧ (x ∉ M ⇒ (SND ∘ (h,M)) x = g x)`
(soby ["H1"] [FunctionComposition; ∉; IN_FunctionSpace]) THEN
statelab `(h:μ->α#β) ∈ M → A ∏ B ∧ FST ∘ (h,M) = f ∧ SND ∘ (h,M) = g`
"hWorks"
(soby ["hDef"; "hProd"] [IN_FunctionSpace; ∉; FUN_EQ_THM]) THEN
toprove `∀ (k:μ->α#β). (k ∈ M → A ∏ B ∧ FST ∘ (k,M) = f ∧ SND ∘ (k,M) =
g) ⇒ h = k`
THENL[GEN_TAC THEN DISCH_THEN(LABEL_TAC "kWorks");
soby ["hWorks"] [EXISTS_UNIQUE_THM]] THEN
statelab `∀ x:μ. x ∉ M ⇒ (k:μ->α#β) x = @y. T` "kOffM" (soby []
[IN_FunctionSpace]) THEN
toprove `∀ x:μ. x ∈ M ⇒ (k:μ->α#β) x = f x,g x ` THENL[
GEN_TAC THEN DISCH_THEN(LABEL_TAC "xM");
soby ["hDef"; "kOffM"] [FUN_EQ_THM; ∉]] THEN
state `FST ((k:μ->α#β) x) = f x ∧ SND (k x) = g x` (soby ["kWorks"]
[FunctionComposition]) THEN
state `(k:μ->α#β) x = FST (k x), SND (k x) ∧ FST (k x) = f x ∧ SND (k x)
= g x`
(soby ["kWorks"] [PAIR]) THEN
soby [] [PAIR_EQ]);;
Here's my original miz3 proof, which I mechanically turned into the above
tactics script. I think they look very similar, and I think this shows that I
understand miz3 in terms of HOL LIGHT.
let UniversalPropertyProduct = thm `;
∀ M:μ->bool A:α->bool B:β->bool f:μ->α g:μ->β .
f ∈ M → A ∧ g ∈ M → B
⇒ (∃! h. h ∈ M → A ∏ B ∧ FST ∘ (h,M) = f ∧ SND ∘ (h,M) = g)
proof
let M be μ->bool;
let A be α->bool;
let B be β->bool;
let f be μ->α;
let g be μ->β;
assume f ∈ M → A ∧ g ∈ M → B [H1];
consider h such that
h = λx. if x ∈ M then f x,g x else @y. T;
∀ x. (x ∈ M ⇒ h x = f x,g x) ∧ (x ∉ M ⇒ h x = @y. T) [hDef] by -, ∉;
∀ x. x ∈ M ⇒ h x ∈ A ∏ B [hProd] by -, H1, IN_FunctionSpace,
IN_CartesianProduct;
∀ x. x ∈ M ⇒ FST (h x) = f x ∧ SND (h x) = g x by hDef, FST_DEF,
SND_DEF, PAIR_EQ;
∀ x. (x ∈ M ⇒ (FST ∘ (h,M)) x = f x) ∧ (x ∉ M ⇒ (FST ∘ (h,M)) x = f x)
∧
(x ∈ M ⇒ (SND ∘ (h,M)) x = g x) ∧ (x ∉ M ⇒ (SND ∘ (h,M)) x = g x)
by FunctionComposition, ∉, -, H1, IN_FunctionSpace;
h ∈ M → A ∏ B ∧ FST ∘ (h,M) = f ∧ SND ∘ (h,M) = g [hWorks] by hDef,
hProd, IN_FunctionSpace, -, ∉, FUN_EQ_THM;
∀ k. (k ∈ M → A ∏ B ∧ FST ∘ (k,M) = f ∧ SND ∘ (k,M) = g) ⇒ h = k
proof
let k be μ->α#β;
assume k ∈ M → A ∏ B ∧ FST ∘ (k,M) = f ∧ SND ∘ (k,M) = g [kWorks];
∀ x. x ∉ M ⇒ k x = @y. T [kOffM] by -, IN_FunctionSpace;
∀ x. x ∈ M ⇒ k x = f x,g x
proof
let x be μ;
assume x ∈ M [xM];
FST (k x) = f x ∧ SND (k x) = g x by -, kWorks, FunctionComposition;
k x = FST (k x), SND (k x) ∧ FST (k x) = f x ∧ SND (k x) = g x by
-, PAIR, kWorks;
qed by -, PAIR_EQ;
qed by hDef, -, kOffM, FUN_EQ_THM, ∉;
qed by hWorks, -, EXISTS_UNIQUE_THM;
`;;
--
Best,
Bill
HOL Light code:
parse_as_infix("NOTIN",(11, "right"));;
parse_as_infix("times",(20, "right"));;
parse_as_infix("composition",(20, "right"));;
parse_as_infix("--->",(13,"right"));;
let NOTIN = new_definition
`! a:A l:A->bool. a NOTIN l <=> ~(a IN l)`;;
let CartesianProduct = new_definition
`! X Y. X times Y = {x,y | x IN X /\ y IN Y}`;;
let IN_CartesianProduct = prove
(`! X Y x y. x,y IN X times Y <=> x IN X /\ y IN Y`,
REWRITE_TAC[IN_ELIM_THM; CartesianProduct] THEN MESON_TAC[PAIR_EQ]);;
let FunctionSpace = new_definition
`! s t. s ---> t = {f | (! x. x IN s ==> f x IN t) /\
! x. x NOTIN s ==> f x = @y. T}`;;
let IN_FunctionSpace = prove
(`! s t f. f IN s ---> t
<=> (! x. x IN s ==> f x IN t) /\ ! x. x NOTIN s ==> f x = @y. T`,
REWRITE_TAC[IN_ELIM_THM; FunctionSpace]);;
let FunctionComposition = new_definition
`! f:A->B s:A->bool g:B->C x.
(g composition (f,s)) x = if x IN s then g (f x) else @y:C. T`;;
let UniversalPropertyProduct = prove
(`! M:mu->bool A:alpha->bool B:beta->bool f:mu->alpha g:mu->beta .
f IN M ---> A /\ g IN M ---> B
==> (?! h. h IN M ---> A times B /\ FST composition (h,M) = f /\
SND composition (h,M) = g)`,
REPEAT GEN_TAC THEN DISCH_THEN(LABEL_TAC "H1") THEN
consider `?h:mu->alpha#beta. h = \x:mu. if x IN M then f x,g x else @y. T`
(mby [] []) THEN
statelab `! x:mu. (x IN M ==> (h:mu->alpha#beta) x = f x,g x) /\ (x NOTIN
M ==> h x = @y. T)` "hDef"
(soby [] [NOTIN]) THEN
statelab `! x:mu. x IN M ==> (h:mu->alpha#beta) x IN A times B` "hProd"
(soby ["H1"] [IN_FunctionSpace; IN_CartesianProduct]) THEN
state `! x:mu. x IN M ==> FST ((h:mu->alpha#beta) x) = f x /\ SND (h x)
= g x`
(mby ["hDef"] [FST_DEF; SND_DEF; PAIR_EQ]) THEN
state `! x:mu. (x IN M ==> (FST composition ((h:mu->alpha#beta),M)) x = f
x) /\ (x NOTIN M ==> (FST composition (h,M)) x = f x) /\
(x IN M ==> (SND composition (h,M)) x = g x) /\ (x NOTIN M ==> (SND
composition (h,M)) x = g x)`
(soby ["H1"] [FunctionComposition; NOTIN; IN_FunctionSpace]) THEN
statelab `(h:mu->alpha#beta) IN M ---> A times B /\ FST composition (h,M)
= f /\ SND composition (h,M) = g` "hWorks"
(soby ["hDef"; "hProd"] [IN_FunctionSpace; NOTIN; FUN_EQ_THM]) THEN
toprove `! (k:mu->alpha#beta). (k IN M ---> A times B /\ FST composition
(k,M) = f /\ SND composition (k,M) = g) ==> h = k`
THENL[GEN_TAC THEN DISCH_THEN(LABEL_TAC "kWorks");
soby ["hWorks"] [EXISTS_UNIQUE_THM]] THEN
statelab `! x:mu. x NOTIN M ==> (k:mu->alpha#beta) x = @y. T` "kOffM"
(soby [] [IN_FunctionSpace]) THEN
toprove `! x:mu. x IN M ==> (k:mu->alpha#beta) x = f x,g x ` THENL[
GEN_TAC THEN DISCH_THEN(LABEL_TAC "xM");
soby ["hDef"; "kOffM"] [FUN_EQ_THM; NOTIN]] THEN
state `FST ((k:mu->alpha#beta) x) = f x /\ SND (k x) = g x` (soby
["kWorks"] [FunctionComposition]) THEN
state `(k:mu->alpha#beta) x = FST (k x), SND (k x) /\ FST (k x) = f x /\
SND (k x) = g x`
(soby ["kWorks"] [PAIR]) THEN
soby [] [PAIR_EQ]);;
#load "unix.cma";;
loadt "miz3/miz3.ml";;
horizon := 0;;
timeout := 50;;
let UniversalPropertyProduct = thm `;
! M:mu->bool A:alpha->bool B:beta->bool f:mu->alpha g:mu->beta .
f IN M ---> A /\ g IN M ---> B
==> (?! h. h IN M ---> A times B /\ FST composition (h,M) = f /\
SND composition (h,M) = g)
proof
let M be mu->bool;
let A be alpha->bool;
let B be beta->bool;
let f be mu->alpha;
let g be mu->beta;
assume f IN M ---> A /\ g IN M ---> B
[H1];
consider h such that
h = \x. if x IN M then f x,g x else @y. T;
! x. (x IN M ==> h x = f x,g x) /\ (x NOTIN M ==> h x = @y. T)
[hDef] by -, NOTIN;
! x. x IN M ==> h x IN A times B [hProd] by -, H1, IN_FunctionSpace,
IN_CartesianProduct;
! x. x IN M ==> FST (h x) = f x /\ SND (h x) = g x by hDef,
FST_DEF, SND_DEF, PAIR_EQ;
! x. (x IN M ==> (FST composition (h,M)) x = f x) /\ (x NOTIN M ==>
(FST composition (h,M)) x = f x) /\
(x IN M ==> (SND composition (h,M)) x = g x) /\ (x NOTIN M ==> (SND
composition (h,M)) x = g x) by FunctionComposition, NOTIN, -, H1,
IN_FunctionSpace;
h IN M ---> A times B /\ FST composition (h,M) = f /\ SND composition
(h,M) = g [hWorks] by hDef, hProd, IN_FunctionSpace, -, NOTIN, FUN_EQ_THM;
! k. (k IN M ---> A times B /\ FST composition (k,M) = f /\ SND
composition (k,M) = g) ==> h = k
proof
let k be mu->alpha#beta;
assume k IN M ---> A times B /\ FST composition (k,M) = f /\ SND
composition (k,M) = g [kWorks];
! x. x NOTIN M ==> k x = @y. T [kOffM] by -, IN_FunctionSpace;
! x. x IN M ==> k x = f x,g x
proof
let x be mu;
assume x IN M [xM];
FST (k x) = f x /\ SND (k x) = g x by -, kWorks, FunctionComposition;
k x = FST (k x), SND (k x) /\ FST (k x) = f x /\ SND (k x) = g x
by -, PAIR, kWorks;
qed by -, PAIR_EQ;
qed by hDef, -, kOffM, FUN_EQ_THM, NOTIN;
qed by hWorks, -, EXISTS_UNIQUE_THM;
`;;
------------------------------------------------------------------------------
Master HTML5, CSS3, ASP.NET, MVC, AJAX, Knockout.js, Web API and
much more. Get web development skills now with LearnDevNow -
350+ hours of step-by-step video tutorials by Microsoft MVPs and experts.
SALE $99.99 this month only -- learn more at:
http://p.sf.net/sfu/learnmore_122812
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
