Coq like Tactics

Revision: r154 で新規実装された４つのTactic
　HYP　DESTRUCT_TAC　FIX_TAC　INTRO_TAC
は（鶏風ではありますが）ラベリングには便利です．

例えば，GEN_TACやDISCH_TAC，DISJ*_TACの働きを有するのが
INTRO_TAC
http://www.cl.cam.ac.uk/~jrh13/hol-light/HTML/INTRO_TAC.html
です．

# g `!x y.
 (A0 /\ A1) \/ A2 \/ (A3 /\ A4 /\ A5)
 ==> A6 \/ (A7 /\ A8)
 ==> !w. C1 \/ C2  \/ C3`;;
Warning: inventing type variables
Warning: Free variables in goal: A0, A1, A2, A3, A4, A5, A6, A7, A8, C1, C2, C3
val it : goalstack = 1 subgoal (1 total)

`!x y.
     A0 /\ A1 \/ A2 \/ A3 /\ A4 /\ A5
     ==> A6 \/ A7 /\ A8
     ==> (!w. C1 \/ C2 \/ C3)`

# e( INTRO_TAC "! x y ; 0 1 | 2 | 3 4 5" );;
val it : goalstack = 3 subgoals (3 total)

  0 [`A3`] (3)
  1 [`A4`] (4)
  2 [`A5`] (5)

`A6 \/ A7 /\ A8 ==> (!w. C1 \/ C2 \/ C3)`

  0 [`A2`] (2)

`A6 \/ A7 /\ A8 ==> (!w. C1 \/ C2 \/ C3)`

  0 [`A0`] (0)
  1 [`A1`] (1)

`A6 \/ A7 /\ A8 ==> (!w. C1 \/ C2 \/ C3)`

# r 2;;
val it : goalstack = 1 subgoal (3 total)

  0 [`A3`] (3)
  1 [`A4`] (4)
  2 [`A5`] (5)

`A6 \/ A7 /\ A8 ==> (!w. C1 \/ C2 \/ C3)`

# e( INTRO_TAC "6 | 7 8" );;
val it : goalstack = 2 subgoals (4 total)

  0 [`A3`] (3)
  1 [`A4`] (4)
  2 [`A5`] (5)
  3 [`A7`] (7)
  4 [`A8`] (8)

`!w. C1 \/ C2 \/ C3`

  0 [`A3`] (3)
  1 [`A4`] (4)
  2 [`A5`] (5)
  3 [`A6`] (6)

`!w. C1 \/ C2 \/ C3`

# e( INTRO_TAC "! w" );;
val it : goalstack = 1 subgoal (4 total)

  0 [`A3`] (3)
  1 [`A4`] (4)
  2 [`A5`] (5)
  3 [`A6`] (6)

`C1 \/ C2 \/ C3`

# e( INTRO_TAC "# 3" );;
val it : goalstack = 1 subgoal (4 total)

  0 [`A3`] (3)
  1 [`A4`] (4)
  2 [`A5`] (5)
  3 [`A6`] (6)

`C3`

同様に，既存のthmに対するLABEL_TAC，CHOOSE_TACの働きを持つのが
　DESTRUCT_TAC
http://www.cl.cam.ac.uk/~jrh13/hol-light/HTML/DESTRUCT_TAC.html
です．

# g `C:bool`;;
Warning: Free variables in goal: C
val it : goalstack = 1 subgoal (1 total)

`C`

# e( DESTRUCT_TAC "z | p" (ARITH_RULE`n=0 \/ 0<n`) );;
val it : goalstack = 2 subgoals (2 total)

  0 [`0 < n`] (p)

`C`

  0 [`n = 0`] (z)

`C`

# r 1;;
val it : goalstack = 1 subgoal (2 total)

  0 [`0 < n`] (p)

`C`

# SPEC`n:num`num_CASES;;
val it : thm = |- n = 0 \/ (?n'. n = SUC n')
# e( DESTRUCT_TAC "q | @ n' . r" (SPEC`n:num`num_CASES) );;
val it : goalstack = 2 subgoals (3 total)

  0 [`0 < n`] (p)
  1 [`n = SUC n'`] (r)

`C`

  0 [`0 < n`] (p)
  1 [`n = 0`] (q)

`C`

また，DISCH_THEN で前件を定理として DESTRUCT_TAC "ラベル" に渡せば

# g `A==>(?x.x=0)==>x=0`;;
Warning: Free variables in goal: A, x
val it : goalstack = 1 subgoal (1 total)

`A ==> (?x. x = 0) ==> x = 0`

# e( DISCH_THEN (DESTRUCT_TAC "0") );;
val it : goalstack = 1 subgoal (1 total)

  0 [`A`] (0)

`(?x. x = 0) ==> x = 0`

# e( DISCH_THEN (DESTRUCT_TAC "@ x . 1") );;
Exception: Failure "X_CHOOSE_TAC".
# e( DISCH_THEN (DESTRUCT_TAC "@ x' . 1") );;
val it : goalstack = 1 subgoal (1 total)

  0 [`A`] (0)
  1 [`x' = 0`] (1)

`x = 0`

のようにも使えます．

さらに，INTRO_TAC を用いると，既存の仮定にラベルを付ける NAME_TAC も簡単に作れます．

# let NAME_TAC (s:string) = REPEAT ((POP_ASSUM MP_TAC) THEN (REWRITE_TAC [IMP_IM
P]) ) THEN INTRO_TAC s ;;
val ( NAME_TAC ) : string -> tactic = <fun>

# g `x=1 /\ y=1 /\ z=1 ==> a=1` ;;
Warning: Free variables in goal: a, x, y, z
val it : goalstack = 1 subgoal (1 total)

`x = 1 /\ y = 1 /\ z = 1 ==> a = 1`

# e( REPEAT STRIP_TAC );;
val it : goalstack = 1 subgoal (1 total)

  0 [`x = 1`]
  1 [`y = 1`]
  2 [`z = 1`]

`a = 1`

# e( NAME_TAC "0 1 2" );;
val it : goalstack = 1 subgoal (1 total)

  0 [`x = 1`] (0)
  1 [`y = 1`] (1)
  2 [`z = 1`] (2)

`a = 1`

# g `x=1 /\ y=1 \/ z=1 ==> a=1` ;;
Warning: Free variables in goal: a, x, y, z
val it : goalstack = 1 subgoal (1 total)

`x = 1 /\ y = 1 \/ z = 1 ==> a = 1`

# e( REPEAT STRIP_TAC );;
val it : goalstack = 2 subgoals (2 total)

  0 [`z = 1`]

`a = 1`

  0 [`x = 1`]
  1 [`y = 1`]

`a = 1`

# e( NAME_TAC "0 1" );;
val it : goalstack = 1 subgoal (2 total)

  0 [`x = 1`] (0)
  1 [`y = 1`] (1)

`a = 1`

# r 1;;
val it : goalstack = 1 subgoal (2 total)

  0 [`z = 1`]

`a = 1`

# e( NAME_TAC "0" );;
val it : goalstack = 1 subgoal (2 total)

  0 [`z = 1`] (0)

`a = 1`