Examples/prog.ml: VC_TAC has trouble with with single-variable programs

[GoogleCodeExporter]

What steps will reproduce the problem?

Execute these commands:
# needs "Examples/prog.ml";;
# install_parser ("correct",parse_program_assertion);;
# g `correct
     T
       var x;
       x := 1
       end
     x > 0`;;
# e VC_TAC;;

What is the expected output? What do you see instead?

VC_TAC should generate verification conditions `1 > 0`, but it leaves the goal 
unmodified.

What version of the product are you using? On what operating system?

HOL Light from SVN, revision 200; ocaml 4.01.0, Linux

Please provide any additional information below.

VC_TAC works as expected if I introduce a dummy variable:

# g `correct T var x, dummy; x := 1 end x > 0`;;

Original issue reported on code.google.com by [email protected] on 20 Oct 2014 at 9:50

[zidongtuili]

Hi, I wonder if it's too late to mention this. The tactics in this file actually have some requirements for your programmes. They can be neither too hard, nor too easy.
For this particular problem, it failed at VC_UNPACK_TAC (in VC_STEP_TAC). So if you do

e (MATCH_MP_TAC VC_ASSIGN THEN REWRITE_TAC[IMPLIES;o_THM] );;