Commit b687a796 authored by Heiko Becker's avatar Heiko Becker
Browse files

Merge branch 'certification' of gitlab.mpi-sws.org:AVA/Daisy into certification

parents 799925ec 5b9628df
......@@ -3,6 +3,7 @@ target/
.DS_Store
src/test/resources/range_regression_today.txt
hol/.ocamlinit
hol/output/*
dmtcp*
ckpt*
hol/run_hol.sh
......@@ -16,9 +17,10 @@ coq/Makefile
coq/*/*.glob
coq/*/.*
coq/*/*.vo
coq/output/*
daisy
rawdata/*
.ensime*
/daisy
last.log
output/*.scala
output/*
......@@ -104,7 +104,7 @@ Lemma subtract_abs_err_bounded (e1:exp R) (e1R:R) (e1F:R) (e2:exp R) (e2R:R) (e2
eval_exp machineEpsilon (updEnv 2 e2F (updEnv 1 e1F cenv)) (Binop Sub (Var R 1) (Var R 2)) vF ->
(Rabs (e1R - e1F) <= err1)%R ->
(Rabs (e2R - e2F) <= err2)%R ->
(Rabs (vR - vF) <= err1 + err2 + ((Rabs e1F + Rabs e2F) * machineEpsilon))%R.
(Rabs (vR - vF) <= err1 + err2 + ((Rabs (e1F - e2F)) * machineEpsilon))%R.
Proof.
intros e1_real e1_float e2_real e2_float sub_real sub_float bound_e1 bound_e2.
(* Prove that e1R and e2R are the correct values and that vR is e1R + e2R *)
......@@ -130,37 +130,21 @@ Proof.
repeat rewrite Rsub_eq_Ropp_Rplus.
repeat rewrite Ropp_plus_distr.
rewrite plus_bounds_simplify.
pose proof (Rabs_triang (e1R + - e1F) ((- e2R + - - e2F) + - ((e1F + - e2F) * delta))).
rewrite Ropp_involutive.
rewrite Rplus_assoc.
eapply Rle_trans.
apply H.
pose proof (Rabs_triang (- e2R + - - e2F) (- ((e1F + - e2F) * delta))).
pose proof (Rplus_le_compat_l (Rabs (e1R + - e1F)) _ _ H0).
apply Rabs_triang.
eapply Rle_trans.
apply H1.
eapply Rplus_le_compat_l.
apply Rabs_triang.
rewrite <- Rplus_assoc.
setoid_rewrite Rplus_comm at 4.
repeat rewrite <- Rsub_eq_Ropp_Rplus.
rewrite Rabs_Ropp.
assert (Rabs (- e2R - - e2F)%R = Rabs (e2R - e2F)).
- rewrite Rsub_eq_Ropp_Rplus.
rewrite <- Ropp_plus_distr.
rewrite Rabs_Ropp.
rewrite <- Rsub_eq_Ropp_Rplus; auto.
- rewrite H3.
eapply Rplus_le_compat.
+ eapply Rplus_le_compat; auto.
+ rewrite Rabs_mult.
eapply Rle_trans.
eapply Rmult_le_compat_l.
apply Rabs_pos.
apply H2.
rewrite Rsub_eq_Ropp_Rplus.
eapply Rle_trans.
eapply Rmult_le_compat_r.
unfold machineEpsilon, RealConstruction.realFromNum, RealConstruction.negativePower; interval.
apply Rabs_triang.
rewrite Rabs_Ropp.
apply Req_le; auto.
rewrite Rabs_minus_sym in bound_e2.
apply Rplus_le_compat; [apply Rplus_le_compat; auto | ].
rewrite Rabs_mult.
eapply Rmult_le_compat_l; [apply Rabs_pos | auto].
Qed.
Lemma mult_abs_err_bounded (e1:exp R) (e1R:R) (e1F:R) (e2:exp R) (e2R:R) (e2F:R) (vR:R) (vF:R) (cenv:nat->R) (err1:R) (err2:R):
......
......@@ -19,20 +19,38 @@ Fixpoint validErrorbound (e:exp Q) (env:analysisResult) :=
let (ive1, err1) := env e1 in
let (ive2, err2) := env e2 in
let rec := andb (validErrorbound e1 env) (validErrorbound e2 env) in
let errIve1 := widenIntv ive1 err1 in
let errIve2 := widenIntv ive2 err2 in
let upperBoundE1 := maxAbs ive1 in
let upperBoundE2 := maxAbs ive2 in
let e1F := upperBoundE1 + err1 in
let e2F := upperBoundE2 + err2 in
let theVal :=
match b with
| Plus => Qleb (err1 + err2 + (Qabs e1F + Qabs e2F) * RationalSimps.machineEpsilon) err
| Sub => Qleb (err1 + err2 + ((Qabs e1F + Qabs e2F) * RationalSimps.machineEpsilon)) err
| Mult => Qleb ((upperBoundE1 * err2 + upperBoundE2 * err1 + err1 * err2) + Qabs(e1F * e2F) * RationalSimps.machineEpsilon) err
| Plus => Qleb (err1 + err2 + (maxAbs (addIntv errIve1 errIve2)) * RationalSimps.machineEpsilon) err
| Sub => Qleb (err1 + err2 + (maxAbs (subtractIntv errIve1 errIve2)) * RationalSimps.machineEpsilon) err
| Mult => Qleb ((upperBoundE1 * err2 + upperBoundE2 * err1 + err1 * err2) + (maxAbs (multIntv errIve1 errIve2)) * RationalSimps.machineEpsilon) err
| Div => false
end
in andb (andb rec errPos) theVal
end.
Ltac iv_assert iv name:=
assert (exists ivlo ivhi, iv = (ivlo, ivhi)) as name by (destruct iv; repeat eexists; auto).
Lemma Qred_eq_frac:
forall q1 q2,
Is_true (Qleb q1 q2) <-> Is_true (Qleb (Qred q1) q2).
Proof.
intros; split; intros.
- apply Is_true_eq_left. apply Is_true_eq_true in H.
unfold Qleb in *; apply Qle_bool_iff. apply Qle_bool_iff in H.
rewrite Qred_correct; auto.
- apply Is_true_eq_left. apply Is_true_eq_true in H. unfold Qleb in *.
rewrite Qle_bool_iff.
rewrite Qle_bool_iff in H.
rewrite Qred_correct in H.
auto.
Qed.
(** Since errors are intervals with 0 as center, we track them as single value since this eases proving upper bounds **)
Lemma err_always_positive e (absenv:analysisResult) iv err:
validErrorbound e absenv = true ->
......@@ -218,21 +236,29 @@ Proof.
apply andb_prop_elim in valid_error.
destruct valid_error as [ valid_rec valid_error].
apply andb_prop_elim in valid_rec.
destruct valid_rec as [valid_rec err_pos].
apply andb_prop_elim in valid_rec.
destruct valid_rec as [valid_e1 valid_e2].
apply Is_true_eq_true in valid_error.
apply Qle_bool_iff in valid_error.
apply Qle_Rle in valid_error.
eapply Rle_trans.
apply Rplus_le_compat_l.
eapply Rmult_le_compat_r.
apply mEps_geq_zero.
Focus 2.
apply Rle_Qle in valid_error.
rewrite <- Qle_bool_iff in valid_error.
apply Is_true_eq_left in valid_error.
apply Is_true_eq_true in valid_error.
rewrite Qle_bool_iff in valid_error.
apply Qle_Rle in valid_error.
repeat rewrite Q2R_plus in valid_error.
repeat rewrite Q2R_mult in valid_error.
repeat rewrite Q2R_plus in valid_error.
repeat rewrite <- Rabs_eq_Qabs in valid_error.
repeat rewrite Q2R_plus in valid_error.
repeat rewrite <- maxAbs_impl_RmaxAbs in valid_error.
eapply Rle_trans.
apply Rplus_le_compat_l.
eapply Rmult_le_compat_r.
apply mEps_geq_zero.
Focus 2.
apply valid_error.
clear valid_e1 valid_e2.
simpl in valid_intv.
......@@ -243,15 +269,33 @@ Proof.
apply andb_prop_elim in valid_rec.
destruct valid_rec as [valid_iv_e1 valid_iv_e2].
apply Is_true_eq_true in valid_iv_e1; apply Is_true_eq_true in valid_iv_e2.
eapply Rle_trans.
eapply Rabs_triang.
eapply Rplus_le_compat.
- pose proof (validIntervalbounds_sound _ _ _ _ _ p_valid valid_iv_e1 e1_real) as valid_bounds_e1.
apply (Rabs_error_bounded_maxAbs nR1); try auto.
unfold contained; rewrite absenv_e1 in valid_bounds_e1; auto.
- pose proof (validIntervalbounds_sound _ _ _ _ _ p_valid valid_iv_e2 e2_real) as valid_bounds_e2.
apply (Rabs_error_bounded_maxAbs nR2); try auto.
unfold contained; rewrite absenv_e2 in valid_bounds_e2; auto.
remember (addIntv (widenIntv (e1lo, e1hi) err1) (widenIntv (e2lo, e2hi) err2)) as iv.
iv_assert iv iv_unf.
destruct iv_unf as [ivl [ivh iv_unf]].
rewrite iv_unf.
rewrite <- maxAbs_impl_RmaxAbs.
assert (ivlo iv = ivl) by (rewrite iv_unf; auto).
assert (ivhi iv = ivh) by (rewrite iv_unf; auto).
rewrite <- H, <- H0.
pose proof (validIntervalbounds_sound _ _ _ _ _ p_valid valid_iv_e1 e1_real) as valid_bounds_e1.
rewrite absenv_e1 in valid_bounds_e1.
simpl in valid_bounds_e1.
pose proof (distance_gives_iv nR1 nF1 (Q2R err1) (Q2R e1lo, Q2R e1hi) valid_bounds_e1 err1_bounded).
pose proof (validIntervalbounds_sound _ _ _ _ _ p_valid valid_iv_e2 e2_real) as valid_bounds_e2.
rewrite absenv_e2 in valid_bounds_e2.
simpl in valid_bounds_e2.
pose proof (distance_gives_iv nR2 nF2 (Q2R err2) (Q2R e2lo, Q2R e2hi) valid_bounds_e2 err2_bounded).
pose proof (IntervalArith.additionIsValid _ _ _ _ H1 H2).
unfold IntervalArith.contained in H3.
destruct H3.
subst; simpl in *.
apply RmaxAbs; simpl.
- rewrite Q2R_min4.
repeat rewrite Q2R_plus;
repeat rewrite Q2R_minus; auto.
- rewrite Q2R_max4.
repeat rewrite Q2R_plus;
repeat rewrite Q2R_minus; auto.
Qed.
Lemma validErrorboundCorrectSubtraction cenv absenv (e1:exp Q) (e2:exp Q) (nR nR1 nR2 nF nF1 nF2 :R) (e err1 err2 :error) (alo ahi e1lo e1hi e2lo e2hi:Q) P :
......@@ -318,13 +362,39 @@ Proof.
apply Is_true_eq_true in valid_iv_e1; apply Is_true_eq_true in valid_iv_e2.
Focus 2.
apply valid_error.
eapply Rplus_le_compat.
- pose proof (validIntervalbounds_sound _ _ _ _ _ p_valid valid_iv_e1 e1_real) as valid_bounds_e1.
apply (Rabs_error_bounded_maxAbs nR1); try auto.
unfold contained; rewrite absenv_e1 in valid_bounds_e1; auto.
- pose proof (validIntervalbounds_sound _ _ _ _ _ p_valid valid_iv_e2 e2_real) as valid_bounds_e2.
apply (Rabs_error_bounded_maxAbs nR2); try auto.
unfold contained; rewrite absenv_e2 in valid_bounds_e2; auto.
remember (subtractIntv (widenIntv (e1lo, e1hi) err1) (widenIntv (e2lo, e2hi) err2)) as iv.
iv_assert iv iv_unf.
destruct iv_unf as [ivl [ivh iv_unf]].
rewrite iv_unf.
rewrite <- maxAbs_impl_RmaxAbs.
assert (ivlo iv = ivl) by (rewrite iv_unf; auto).
assert (ivhi iv = ivh) by (rewrite iv_unf; auto).
rewrite <- H, <- H0.
pose proof (validIntervalbounds_sound _ _ _ _ _ p_valid valid_iv_e1 e1_real) as valid_bounds_e1.
rewrite absenv_e1 in valid_bounds_e1.
simpl in valid_bounds_e1.
pose proof (distance_gives_iv nR1 nF1 (Q2R err1) (Q2R e1lo, Q2R e1hi) valid_bounds_e1 err1_bounded).
pose proof (validIntervalbounds_sound _ _ _ _ _ p_valid valid_iv_e2 e2_real) as valid_bounds_e2.
rewrite absenv_e2 in valid_bounds_e2.
simpl in valid_bounds_e2.
pose proof (distance_gives_iv nR2 nF2 (Q2R err2) (Q2R e2lo, Q2R e2hi) valid_bounds_e2 err2_bounded).
pose proof (IntervalArith.subtractionIsValid _ _ _ _ H1 H2).
unfold IntervalArith.contained in H3.
destruct H3.
subst; simpl in *.
apply RmaxAbs; simpl.
- rewrite Q2R_min4.
repeat rewrite Q2R_plus;
repeat rewrite Q2R_minus;
repeat rewrite Q2R_opp;
repeat rewrite Q2R_plus;
repeat rewrite Q2R_minus; auto.
- rewrite Q2R_max4.
repeat rewrite Q2R_plus;
repeat rewrite Q2R_minus;
repeat rewrite Q2R_opp;
repeat rewrite Q2R_plus;
repeat rewrite Q2R_minus; auto.
Qed.
Lemma validErrorboundCorrectMult cenv absenv (e1:exp Q) (e2:exp Q) (nR nR1 nR2 nF nF1 nF2 :R) (e err1 err2 :error) (alo ahi e1lo e1hi e2lo e2hi:Q) P :
......@@ -932,21 +1002,39 @@ Proof.
rewrite H1.
lra.
}
- apply Rmult_le_compat; [ apply Rabs_pos | apply mEps_geq_zero | | apply Req_le; auto ].
rewrite Q2R_mult; repeat rewrite Q2R_plus.
repeat rewrite <- maxAbs_impl_RmaxAbs.
repeat rewrite Rabs_mult.
apply Rmult_le_compat; [apply Rabs_pos | apply Rabs_pos | | ].
+ apply (Rabs_error_bounded_maxAbs nR1); try auto.
rewrite absenv_e1 in valid_e1; simpl in *; unfold contained; auto.
+ apply (Rabs_error_bounded_maxAbs nR2); try auto.
rewrite absenv_e2 in valid_e2; simpl in *; unfold contained; auto.
- remember (multIntv (widenIntv (e1lo, e1hi) err1) (widenIntv (e2lo, e2hi) err2)) as iv.
iv_assert iv iv_unf.
destruct iv_unf as [ivl [ivh iv_unf]].
rewrite iv_unf.
rewrite <- maxAbs_impl_RmaxAbs.
assert (ivlo iv = ivl) by (rewrite iv_unf; auto).
assert (ivhi iv = ivh) by (rewrite iv_unf; auto).
rewrite <- H, <- H0.
pose proof (validIntervalbounds_sound _ _ _ _ _ p_valid valid_iv_e1 e1_real) as valid_bounds_e1.
rewrite absenv_e1 in valid_bounds_e1.
simpl in valid_bounds_e1.
pose proof (distance_gives_iv nR1 nF1 (Q2R err1) (Q2R e1lo, Q2R e1hi) valid_bounds_e1 err1_bounded).
pose proof (validIntervalbounds_sound _ _ _ _ _ p_valid valid_iv_e2 e2_real) as valid_bounds_e2.
rewrite absenv_e2 in valid_bounds_e2.
simpl in valid_bounds_e2.
pose proof (distance_gives_iv nR2 nF2 (Q2R err2) (Q2R e2lo, Q2R e2hi) valid_bounds_e2 err2_bounded).
pose proof (IntervalArith.interval_multiplication_valid _ _ _ _ H1 H2).
unfold IntervalArith.contained in H3.
destruct H3.
unfold RmaxAbsFun.
apply Rmult_le_compat_r.
apply mEps_geq_zero.
apply RmaxAbs; subst; simpl in *.
- rewrite Q2R_min4.
repeat rewrite Q2R_mult;
repeat rewrite Q2R_minus;
repeat rewrite Q2R_plus; auto.
- rewrite Q2R_max4.
repeat rewrite Q2R_mult;
repeat rewrite Q2R_minus;
repeat rewrite Q2R_plus; auto.
Qed.
Ltac iv_assert iv name:=
assert (exists ivlo ivhi, iv = (ivlo, ivhi)) as name by (destruct iv; repeat eexists; auto).
Lemma validErrorbound_sound (e:exp Q):
forall cenv absenv nR nF err P elo ehi,
precondValidForExec P cenv ->
......
This diff is collapsed.
================================================================================
== HOL LIGHT TACTICIAN ==
== ==
== by Mark Adams ==
== Copyright (c) Univeristy of Edinburgh, 2012 ==
== Copyright (c) Proof Technologies Ltd, 2012-2015 ==
================================================================================
This is HOL Light Tactician, version 3.1.
All files are distributed under the terms of the GNU General Public License:
they are free and open source and come with no warranty. See the LICENSE file
for details.
Subsequent sections in this README deal with:
1. Directory Contents
2. Overview of Tactician
3. Installation / Loading
4. Using Tactician
5. Examples
6. Author and Acknowledgements
7. Website and Contact Details
* * * * * * *
1. DIRECTORY CONTENTS
The Tactician directory consists of the following files:
LICENSE Disclaimer and terms of the open source licence.
README This file.
USER_GUIDE Guide to using Tactician, including all of its commands.
*.ml ML source code implementing Tactician.
*.mli ML source code implementing Tactician.
and the following directory:
env Adjusted model of OCaml environment for various OCaml versions.
toploops Adjusted OCaml file 'toploop.ml' for various OCaml versions.
* * * * * * *
2. OVERVIEW OF TACTICIAN
Tactician is a utility for refactoring and visualising HOL Light tactic proofs.
It is aimed at HOL Light users of the subgoal package, both for novices wanting
to learn from legacy tactic proofs by stepping through them, and for experts
wanting reduce the effort involved in maintaining their own proof scripts.
Tactician works by dynamically recording tactic proofs as they are executed,
storing them internally as proof trees. The proof tree can then be exported
either as ML source code or as a .dot graph. Export to source code can
optionally involve refactoring the proof into various forms, including:
- flattened out into individual 'e' commands;
- packaged up with 'THEN's and 'THENL's into a single tactic proof.
Tactician works for virtually all the packaged up tactic proofs that occur in
the HOL Light source code. However there are theoretical limitations on what
it will work for. See USER_GUIDE for details.
* * * * * * *
3. INSTALLATION / LOADING
1. Download the source tarball (which includes this README) from the Proof
Technologies Tactician webpage:
http://www.proof-technologies.com/tactician
Change directory to your HOL Light distribution directory and unpack the
Tactician tarball as a subdirectory (called 'Tactician'):
> cd <hollight-dir>
> tar -xzf <download-dir>/hollight_tactician-<version>.tar.gz
2. This step is optional. It makes using Tactician easier, saving you from
having to execute "promote_all_values ();;" before each tactic proof you want
to refactor. However it involves rebuilding OCaml from source, which you
might not want to do.
Firstly, make sure you have a source distribution of OCaml. If you don't,
this can be obtained from the INRIA OCaml webpages at:
http://caml.inria.fr/ocaml/index.en.html
Secondly, overwrite the file 'toplevel/toploop.ml' in OCaml's source
distribution with the relevant file from Tactician's 'toploops' directory
(where "x" is the OCaml version):
> cd <ocaml-x-dir>
> mv toplevel/toploop.ml toplevel/toploop.ml.orig
> cp <hollight-dir>/Tactician/toploops/toploop.<x>.ml toplevel/toploop.ml
Thirdly, rebuild OCaml from source in the normal way:
> ./configure (with any options you want, e.g. --prefix `pwd`)
> make world.opt
> make install (may need to be done as sudoer or root)
> make clean
You should ensure that HOL Light works with your adjusted OCaml. If you are
using the same OCaml version with executables installed in the same directory,
and if you rebuild HOL Light from source each time you use HOL Light (as
opposed to using checkpointing), then there is nothing to do. Otherwise you
will need to ensure that the OCaml executables are in your execution path,
that the correct version of Camlp5 has been installed and/or that HOL Light
has been rebuilt accordingly. See the HOL Light README for details.
3. Start a HOL Light session as you normally do, and incorporate any extra
supporting files that get used in the proofs you want to refactor. For
example, to rebuild HOL Light from source, start an OCaml session in your HOL
Light distribution directory, and then execute the following:
# #use "hol.ml";; (the first '#' indicates the OCaml prompt)
# #use ... (for any subsequent supporting files)
4. Then load Tactician into the HOL Light session by processing the 'main.ml'
file from the 'Tactician' subdirectory:
# #use "Tactician/main.ml";;
* * * * * * *
4. USING TACTICIAN
A brief overview of some commands for basic refactoring of the most recently
processed tactic proof is given here. For full details about all of Tactician's
capabilities, see USER_GUIDE.
1. If a bespoke OCaml toplevel for Tactician (see installation step 2) is *not*
being used, then before executing each tactic proof, it is first necessary to
execute the following command:
# promote_all_values ();;
2. Then process the tactic proof from the proof script, as per normal:
# g `...`;;
# e (...);;
# e (...);;
OR
# prove (`...`,
... THEN ... THENL [...]);;
OR
# prove_by_refinement (`...`,
[ ... ; ... ; ...] );;
3. You can then use the ML output commands to output the proof to screen or
file in the desired form. The most commonly used commands for outputting to
screen are as follows:
# print_ge_proof ();;
- Prints the proof as a flattened series of "g/e" style single-tactic
steps, with no connecting top-level 'THEN' tacticals. Branch-
numbering comments are inserted wherever the proof branches.
# print_pbr_proof ();;
- Like 'print_ge_proof' but outputs in Flyspeck's "prove-by-
refinement" style instead of "g/e" style.
# print_thenl_prove_proof ();;
- Prints the proof as a single-step "prove" style proof, with
tactics that result in single goals connected by 'THEN' and those
that result in multiple goals connected by 'THENL'. This structure
directly reflects the tree structure of the proof as it was executed.
# print_prove_proof ();;
- Like 'print_thenl_prove_proof', but tries to print a more concise
proof, not necessarily reflecting the original tree structure.
This is done by spotting opportunities for replacing 'THENL' with
'THEN'.
# print_original_proof ();;
- Tries to reproduce the inputted proof verbatim, with the same
structure and style as the original.
* * * * * * *
5. EXAMPLES
Here we provide two examples of Tactician in use. For more examples, visit the
Tactician webpages (see Section 7 of this README).
PROOF FLATTENING
First an example of the proof flattening export facility, flattening the
packaged-up "prove" style proof of 'REAL_MUL_LINV_UNIQ' (from HOL Light source
code file 'real.ml') into a "g/e" style proof.
Steping through the following packaged-up proof of 'REAL_MUL_LINV_UNIQ' without
the aid of Tactician can be done by laboriously replacing "... THEN" around each
tactic with "e (...);;" to be ready for HOL Light input. However, usage of
'THEN' in the packaged-up proof obscures where the proof branches are and how
long those branches are, and so it is not obvious which tactics need to be
re-entered and at which point. Thus the user would also have to keep track of
the proof branching points.
# let REAL_MUL_LINV_UNIQ = prove
(`!x y. (x * y = &1) ==> (inv(y) = x)`,
REPEAT GEN_TAC THEN
ASM_CASES_TAC `y = &0` THEN
ASM_REWRITE_TAC[REAL_MUL_RZERO; REAL_OF_NUM_EQ; ARITH_EQ] THEN
FIRST_ASSUM(SUBST1_TAC o SYM o MATCH_MP REAL_MUL_LINV) THEN
ASM_REWRITE_TAC[REAL_EQ_MUL_RCANCEL] THEN
DISCH_THEN(ACCEPT_TAC o SYM));;
Once the above proof has been entered, Tactician flattens it out with a single
command:
# print_ge_proof ();;
This outputs the proof in a form ready to be stepped through by the user:
g `!x y. (x * y = &1) ==> (inv(y) = x)`;;
e (REPEAT GEN_TAC);;
e (ASM_CASES_TAC `y = &0`);;
(* *** Branch 1 *** *)
e (ASM_REWRITE_TAC [REAL_MUL_RZERO;REAL_OF_NUM_EQ;ARITH_EQ]);;
(* *** Branch 2 *** *)
e (ASM_REWRITE_TAC [REAL_MUL_RZERO;REAL_OF_NUM_EQ;ARITH_EQ]);;
e (FIRST_ASSUM (SUBST1_TAC o SYM o MATCH_MP REAL_MUL_LINV));;
e (ASM_REWRITE_TAC [REAL_EQ_MUL_RCANCEL]);;
e (DISCH_THEN (ACCEPT_TAC o SYM));;
The flattened proof reveals that 'ASM_CASES_TAC' causes the proof to branch into
two, and that the first 'ASM_REWRITE_TAC' gets applied to each resulting
subgoal, finishing off the first.
PROOF PACKAGING
Now an example of the proof packaging facility, packaging up a flat "g/e" style
proof into a "prove" style proof. This "g/e" style proof is a flattened version
of the proof of 'REAL_LE_LCANCEL_IMP' (from HOL Light source code file
'real.ml').
Without the aid of Tactician, packaging up the following proof not only invovles
replacing "e(...)" lines with "... THEN", but also keeping track of branching
points, by stepping through the proof, and putting the branches into a 'THENL'
list. To produce a concise version, it is then necessary to review the
resulting proof to find where branches have common proofs, and thus where
duplicated 'THENL' list elements can be removed. Finally, it is nice to
reformat the resulting optimised proof so that it occupies fewer lines but still
remains readable.
# g `!x y z. &0 < x /\ x * y <= x * z ==> y <= z`;;
# e (REPEAT GEN_TAC);;
# e (REWRITE_TAC [REAL_LE_LT; REAL_EQ_MUL_LCANCEL]);;
# e (ASM_CASES_TAC `x = &0`);;
# e (ASM_REWRITE_TAC [REAL_LT_REFL]);;
# e (ASM_REWRITE_TAC [REAL_LT_REFL]);;
# e (STRIP_TAC);;
# e (ASM_REWRITE_TAC []);;
# e (DISJ1_TAC);;
# e (MATCH_MP_TAC REAL_LT_LCANCEL_IMP);;
# e (EXISTS_TAC `x:real`);;
# e (ASM_REWRITE_TAC []);;
# e (ASM_REWRITE_TAC []);;
The proof actually branches at two points: firstly after 'ASM_CASES_TAC' on line
4 of the proof; secondly in the second branch after 'STRIP_TAC' on line 7. The
first branch from 'ASM_CASES_TAC' is finished in a single step, which is also
the first step of the second branch, and so there is no need for a 'THENL' list
for this branching point. Also, the second branch from 'STRIP_TAC' is finished
in a single step, which is also the first step of the first branch, and so
neither does this branching point require a 'THENL' list.
Tactician packages up the above proof, finds where 'THENL' lists can be
optimised and reformats the result, all in a single command:
# print_prove_proof ();;
prove
(`!x y z. &0 < x /\ x * y <= x * z ==> y <= z`,
REPEAT GEN_TAC THEN REWRITE_TAC [REAL_LE_LT; REAL_EQ_MUL_LCANCEL] THEN
ASM_CASES_TAC `x = &0` THEN ASM_REWRITE_TAC [REAL_LT_REFL] THEN
STRIP_TAC THEN ASM_REWRITE_TAC [] THEN DISJ1_TAC THEN
MATCH_MP_TAC REAL_LT_LCANCEL_IMP THEN EXISTS_TAC `x:real` THEN
ASM_REWRITE_TAC []);;
* * * * * * *
6. AUTHOR AND ACKNOWLEDGEMENTS
Tactician is written by Mark Adams, Proof Technologies Ltd. The original
version was written whilst working for David Aspinall at the Department of
Informatics, University of Edinburgh, and was funded by the University of
Edinburgh. Some of the subsequent work has been written whilst working for
Josef Urban at Radboud University, funded by Tom Hales and Radboud University.
* * * * * * *
7. WEBSITE AND CONTACT DETAILS
The Proof Technologies website has pages dedicated to Tactician, including the
download for the latest version, at:
http://www.proof-technologies.com/tactician
Users are encouraged to contact Proof Technologies with any problems found in
Tactician, or with any suggestions for improvements.
You can contact us via the website Tactician pages. Alternatively, you can
e-mail us:
tactician@proof-technologies.com
This diff is collapsed.
This diff is collapsed.
<