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

Prove determinism lemma with help from hol-info mails

parent 2cc0bc48
......@@ -98,7 +98,6 @@ e (destruct "binopc" "@b2. @e1'. @e2'. @v1. @v2. @d. b_eq v_eq eval_e1 eval_e2
e (EXISTS_TAC `d:real` THEN EXISTS_TAC `v1:real` THEN EXISTS_TAC `v2:real`);;
e (RULE_ASSUM_TAC (REWRITE_RULE[injectivity "exp"]) THEN ASM_REWRITE_TAC[]);;
let binop_inv = top_thm();;
(*
Define real evaluation as a predicate on the epsilon of the evaluation relation
*)
......@@ -119,88 +118,60 @@ let abs_leq_0_impl_zero =
g `!e:(real)exp v1:real v2:real env.
eval_exp (&0) env e v1 /\ eval_exp (&0) env e v2 ==> v1 = v2`;;
e (MATCH_MP_TAC exp_IND THEN REPEAT STRIP_TAC);;
(* Now the problem with the "inversions" *)
e (SUBGOAL_TAC "v1_eq_env_a" `env a = v1` [ALL_TAC]);;
e (MP_TAC (ASSUME `eval_exp (&0) env (Var a) v1`));;
e (CHANGED_TAC (ONCE_REWRITE_TAC [eval_exp_CASES]));;
e (STRIP_TAC);;
e (MP_TAC (ASSUME `(Var a):(real)exp = Var v`));;
e (ASM_REWRITE_TAC[injectivity "exp"]);;
e (STRIP_TAC);;
e (CHEAT_TAC);;
(* FIXME:
e (CHANGED_TAC(ASM_REWRITE_TAC [(ASSUME `a:num = v:num`)]));;
does not work
*)
e (contradiction `(Var a):(real)exp = Const n` "exp");;
e (contradiction `(Var a):(real)exp = Binop b e1 e2` "exp");;
(* FINISH FIRST INVERSION, START SECOND *)
e (SUBGOAL_TAC "v2_eq_env_a" `env a = v2` [ALL_TAC]);;
e (MP_TAC (ASSUME `eval_exp (&0) env (Var a) v2`));;
e (CHANGED_TAC (ONCE_REWRITE_TAC [eval_exp_CASES]));;
e (STRIP_TAC);;
e (MP_TAC (ASSUME `(Var a):(real)exp = Var v`));;
e (ASM_REWRITE_TAC[injectivity "exp"]);;
e (MATCH_MP_TAC exp_IND);;
e (STRIP_TAC);;
e (CHEAT_TAC);;
(* FIXME:
e (CHANGED_TAC(ASM_REWRITE_TAC [(ASSUME `a:num = v:num`)]));;
does not work
*)
e (contradiction `(Var a):(real)exp = Const n` "exp");;
e (contradiction `(Var a):(real)exp = Binop b e1 e2` "exp");;
(* INVERSIONS FINISHED, now rewrite *)
e (CHEAT_TAC);; (* FIXME *)
(* First inversion *)
e (SUBGOAL_TAC "delta_0" `?d. d = &0 /\ v1 = perturb a d` [ALL_TAC]);;
e (MP_TAC (ASSUME `eval_exp (&0) env (Const a) v1`));;
e (ONCE_REWRITE_TAC [eval_exp_CASES]);;
e (STRIP_TAC);;
e (contradiction `(Const a):(real)exp = Var v` "exp");;
(* equivalence proof as above *)
e (SUBGOAL_TAC "" `a = n` [CHEAT_TAC]);;
e (EXISTS_TAC `delta:real`);;
e (CONJ_TAC);;
e (ASSUME_TAC (SPECL [`delta:real`] abs_leq_0_impl_zero));;
e (MATCH_MP_TAC (ASSUME `abs delta <= &0 ==> delta = &0`));;
e (ASM_MESON_TAC[]);;
e (INTRO_TAC "!a v1 v2 env; eval_exps");;
e (destruct "eval_exps" "eval_v1 eval_v2");;
(* Var Case *)
e (SUBGOAL_TAC "v1_eq_env_a" `v1:real = (env (a:num)):real` [ALL_TAC]);;
e (MATCH_MP_TAC var_inv);;
e (EXISTS_TAC `&0`);;
e (ASM_SIMP_TAC[]);;
e (SUBGOAL_TAC "v2_eq_env_a" `v2:real = (env (a:num)):real` [ALL_TAC]);;
e (MATCH_MP_TAC var_inv);;
e (EXISTS_TAC `&0`);;
e (ASM_SIMP_TAC[]);;
e (ASM_REWRITE_TAC[]);;
e (CHEAT_TAC);; (* FIXME: Rewrites *)
e (contradiction `(Const a):(real)exp = Binop b e1 e2` "exp");;
(* Second inversion *)
e (SUBGOAL_TAC "delta_0" `?d. d = &0 /\ v2 = perturb a d` [ALL_TAC]);;
e (MP_TAC (ASSUME `eval_exp (&0) env (Const a) v2`));;
e (ONCE_REWRITE_TAC [eval_exp_CASES]);;
(* Const Case *)
e (STRIP_TAC);;
e (contradiction `(Const a):(real)exp = Var v` "exp");;
(* equivalence proof as above *)
e (SUBGOAL_TAC "" `a = n` [CHEAT_TAC]);;
e (EXISTS_TAC `delta:real`);;
e (CONJ_TAC);;
e (ASSUME_TAC (SPECL [`delta:real`] abs_leq_0_impl_zero));;
e (MATCH_MP_TAC (ASSUME `abs delta <= &0 ==> delta = &0`));;
e (ASM_MESON_TAC[]);;
e (INTRO_TAC "!a v1 v2 env; eval_exps");;
e (destruct "eval_exps" "eval_v1 eval_v2");;
e (SUBGOAL_TAC "v1_eq_a" `?d. v1:real = perturb (a:real) d /\ abs d <= &0`
[MATCH_MP_TAC const_inv THEN EXISTS_TAC `env:num->real` THEN ASM_SIMP_TAC[]]);;
e (MATCH_MP_TAC const_inv);;
e (EXISTS_TAC `env:num->real`);;
e (STRIP_ASSUME_TAC const_inv);;
e (ASM_SIMP_TAC[]);;
e (SUBGOAL_TAC "v2_eq_a" `?d. v2:real = perturb (a:real) d /\ abs d <= &0`
[MATCH_MP_TAC const_inv THEN EXISTS_TAC `env:num->real` THEN ASM_SIMP_TAC[]]);;
e (destruct "v1_eq_a" "@d1. v1_eq abs");;
e (destruct "v2_eq_a" "@d2. v2_eq abs2");;
e (SUBGOAL_TAC "abs_d1_0" `d1 = &0` [MATCH_MP_TAC abs_leq_0_impl_zero THEN ASM_SIMP_TAC[]]);;
e (SUBGOAL_TAC "abs_d2_0" `d2 = &0` [MATCH_MP_TAC abs_leq_0_impl_zero THEN ASM_SIMP_TAC[]]);;
e (ASM_REWRITE_TAC[]);;
(* Binop Case *)
e (REPEAT STRIP_TAC);;
e (FIND_ASSUM (LABEL_TAC "IH1") `!(v1:real) (v2:real) (env:num->real).
eval_exp (&0) (env:num->real) (a1:(real)exp) (v1:real) /\
eval_exp (&0) (env:num->real) (a1:(real)exp) (v2:real)
==> (v1:real) = (v2:real)`);;
e (FIND_ASSUM (LABEL_TAC "IH2") `!(v1:real) (v2:real) (env:num->real).
eval_exp (&0) (env:num->real) (a2:(real)exp) (v1:real) /\
eval_exp (&0) (env:num->real) (a2:(real)exp) (v2:real)
==> (v1:real) = (v2:real)`);;
e (SUBGOAL_TAC "v1_eq_op_a" `?d v1' v2'. v1:real = perturb (eval_binop (a0:binop) (v1':real) (v2':real)) d /\ eval_exp (&0) env a1 v1' /\ eval_exp (&0) env a2 v2' /\ abs d <= &0`
[MATCH_MP_TAC binop_inv THEN ASM_SIMP_TAC[]]);;
e (SUBGOAL_TAC "v2_eq_op_a" `?d v1' v2'. v2:real = perturb (eval_binop (a0:binop) (v1':real) (v2':real)) d /\ eval_exp (&0) env a1 v1' /\ eval_exp (&0) env a2 v2' /\ abs d <= &0`
[MATCH_MP_TAC binop_inv THEN ASM_SIMP_TAC[]]);;
e (destruct "v1_eq_op_a" "@d1. @v11. @v21. v1_eq eval_a11 eval_a21 abs_0");;
e (destruct "v2_eq_op_a" "@d2. @v12. @v22. v2_eq eval_a12 eval_a22 abs_0");;
e (SUBGOAL_TAC "abs_d1_0" `d1 = &0` [MATCH_MP_TAC abs_leq_0_impl_zero THEN ASM_SIMP_TAC[]]);;
e (SUBGOAL_TAC "abs_d2_0" `d2 = &0` [MATCH_MP_TAC abs_leq_0_impl_zero THEN ASM_SIMP_TAC[]]);;
e (SUBGOAL_TAC "v11_eq_v12" `v11:real = v12:real` [REMOVE_THEN "IH1" (MATCH_MP_TAC)]);;
e (EXISTS_TAC `env:num->real` THEN ASM_SIMP_TAC[]);;
e (SUBGOAL_TAC "v21_eq_v22" `v21:real = v22:real` [REMOVE_THEN "IH2" (MATCH_MP_TAC)]);;
e (EXISTS_TAC `env:num->real` THEN ASM_SIMP_TAC[]);;
e (ASM_REWRITE_TAC[]);;
e (CHEAT_TAC);; (* FIXME: Rewrites *)
e (contradiction `(Const a):(real)exp = Binop b e1 e2` "exp");;
e (CHEAT_TAC);; (*Rewrites *)
(* Induction step *)
e (SUBGOAL_TAC "" `?v11 v12. eval_exp (&0) env a1 v11 /\ eval_exp (&0) env a2 v12` [ALL_TAC]);;
e (MP_TAC (ASSUME `eval_exp (&0) env (Binop a0 a1 a2) v1`));;
e (ONCE_REWRITE_TAC [eval_exp_CASES]);;
e (STRIP_TAC);;
e (contradiction `(Binop a0 a1 a2):(real)exp = Var v` "exp");;
e (contradiction `(Binop a0 a1 a2):(real)exp = Const n` "exp");;
e (EXISTS_TAC `v1:real`);;
e (EXISTS_TAC `v1:real`);;
e (STRIP_TAC);;
e (DISJ2_TAC THEN DISJ2_TAC);;
e (CHEAT_TAC);; (* FIXME: Follows from Asms *)
e (DISJ2_TAC THEN DISJ2_TAC);;
e (CHEAT_TAC);; (* FIXME: Follows from Asms *)
(* Destruct IH, rewrite then done *)
e (CHEAT_TAC);;
let eval_0_det = top_thm();;
(*
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment