Re: [Hol-info] Learning HOL Light

SourceForge Headquarters 1320 Columbia Street Suite 310 San Diego, CA 92101 +1 (858) 422-6466

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;
`;;