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

Add prove of determinism for evaluation at least using CHEAT_TAC

parent 870a71d1
......@@ -70,13 +70,93 @@ let abs_leq_0_impl_zero =
THEN MP_TAC (ASSUME `abs d = &0`)
THEN ASM_REWRITE_TAC [REAL_ABS_ZERO]);;
g `!e v1 v2 env.
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_env_a" `eval_exp eps env (Var a) (env a)` [ALL_TAC]);;
e (ASM_REWRITE_TAC [eval_exp_CASES]);;
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_REC);;
e (contradiction `(Var a):(real)exp = Binop b e1 e2` exp_REC);;
(* 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 (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_REC);;
e (contradiction `(Var a):(real)exp = Binop b e1 e2` exp_REC);;
(* 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_REC);;
(* 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 (ASM_REWRITE_TAC[]);;
e (CHEAT_TAC);; (* FIXME: Rewrites *)
e (contradiction `(Const a):(real)exp = Binop b e1 e2` exp_REC);;
(* 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]);;
e (STRIP_TAC);;
e (contradiction `(Const a):(real)exp = Var v` exp_REC);;
(* 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 (ASM_REWRITE_TAC[]);;
e (CHEAT_TAC);; (* FIXME: Rewrites *)
e (contradiction `(Const a):(real)exp = Binop b e1 e2` exp_REC);;
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_REC);;
e (contradiction `(Binop a0 a1 a2):(real)exp = Const n` exp_REC);;
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);;
b();;
b();;
(*
Using the parametric expressions, define boolean expressions for conditionals
*)
......
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