読者です 読者をやめる 読者になる 読者になる

冪乗と階乗

g(`!n. 3 < n ==> 2 EXP n < FACT n`);;
e(INDUCT_TAC);;
e(ARITH_TAC);;
e(SIMP_TAC[LT;EXP;FACT]);;
e(STRIP_TAC);;
e(POP_ASSUM (SUBST1_TAC o GSYM) THEN ARITH_TAC);;
e(MATCH_MP_TAC LESS_MULT);;
e(ASM_ARITH_TAC);;
prove
 (`!n. 3 < n ==> 2 EXP n < FACT n`,
  INDUCT_TAC THENL
  [ARITH_TAC;
   SIMP_TAC[LT;EXP;FACT] THEN STRIP_TAC THENL
   [POP_ASSUM (SUBST1_TAC o GSYM) THEN ARITH_TAC;
    MATCH_MP_TAC LESS_MULT THEN ASM_ARITH_TAC]]);;
dmtcp_checkpoint (DMTCP + MTCP) 1.2.5
Copyright (C) 2006-2011  Jason Ansel, Michael Rieker, Kapil Arya, and
                                                       Gene Cooperman
This program comes with ABSOLUTELY NO WARRANTY.
This is free software, and you are welcome to redistribute it
under certain conditions; see COPYING file for details.
(Use flag "-q" to hide this message.)

dmtcp_coordinator starting...
    Port: 7779
    Checkpoint Interval: disabled (checkpoint manually instead)
    Exit on last client: 1
Backgrounding...
# g(`!n. 3 < n ==> 2 EXP n < FACT n`);;
val it : goalstack = 1 subgoal (1 total)

`!n. 3 < n ==> 2 EXP n < FACT n`

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

  0 [`3 < n ==> 2 EXP n < FACT n`]

`3 < SUC n ==> 2 EXP SUC n < FACT (SUC n)`

`3 < 0 ==> 2 EXP 0 < FACT 0`

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

  0 [`3 < n ==> 2 EXP n < FACT n`]

`3 < SUC n ==> 2 EXP SUC n < FACT (SUC n)`

# e(SIMP_TAC[LT;EXP;FACT]);;
val it : goalstack = 1 subgoal (1 total)

  0 [`3 < n ==> 2 EXP n < FACT n`]

`3 = n \/ 3 < n ==> 2 * 2 EXP n < SUC n * FACT n`

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

  0 [`3 < n ==> 2 EXP n < FACT n`]
  1 [`3 < n`]

`2 * 2 EXP n < SUC n * FACT n`

  0 [`3 < n ==> 2 EXP n < FACT n`]
  1 [`3 = n`]

`2 * 2 EXP n < SUC n * FACT n`

# e(POP_ASSUM (SUBST1_TAC o GSYM) THEN ARITH_TAC);;
val it : goalstack = 1 subgoal (1 total)

  0 [`3 < n ==> 2 EXP n < FACT n`]
  1 [`3 < n`]

`2 * 2 EXP n < SUC n * FACT n`

# e(MATCH_MP_TAC LESS_MULT);;
val it : goalstack = 1 subgoal (1 total)

  0 [`3 < n ==> 2 EXP n < FACT n`]
  1 [`3 < n`]

`2 < SUC n /\ 2 EXP n < FACT n`

# e(ASM_ARITH_TAC);;
val it : goalstack = No subgoals