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

Prove existential rewriting in Coq, nearly finished error checker soundness

parent 53adcf51
This diff is collapsed.
......@@ -248,3 +248,34 @@ let gr_simps = define
`gr = \(e1:(V)exp). \(e2:(V)exp). less e2 e1`;;
let greq_simps = define
`greq = \(e1:(V)exp). \(e2:(V)exp). leq e2 e1`;;
let existential_rewriting = prove (
`!(b:binop) (e1:(real)exp) (e2:(real)exp) (eps:real) (cenv:env_ty) (v:real).
(eval_exp eps cenv (Binop b e1 e2) v <=>
(?(v1:real) (v2:real).
eval_exp eps cenv e1 v1 /\
eval_exp eps cenv e2 v2 /\
eval_exp eps (updEnv 2 v2 (updEnv 1 v1 cenv)) (Binop b (Var 1) (Var 2)) v))`,
intros "!b e1 e2 eps cenv v" THEN split
THENL [
intros "eval_bin"
THEN pose_proof binop_inv "eval_inv" [`eps:real`;`cenv:env_ty`; `b:binop`; `e1:(real)exp`; `e2:(real)exp`; `v:real`] [ "eval_bin"]
THEN destruct "eval_inv" "@d. @v1. @v2. v_eq eval_e1 eval_e2 d_leq"
THEN existsl [`v1:real`; `v2:real`] THEN (REPEAT split) THEN (TRY auto)
THEN LABEL_TAC "eval_cases" eval_exp_RULES THEN destruct "eval_cases" "_ _ _ binop_case"
THEN mp_asm "binop_case" THEN split THEN SIMP_TAC[]
THEN ASM_REWRITE_TAC[var_equiv; updEnv]
THEN SUBGOAL_TAC "cond_eq" `1:num = 2 <=> F` [ARITH_TAC]
THEN ASM_SIMP_TAC[];
intros "exists_val"
THEN destruct "exists_val" "@v1. @v2. eval_e1 eval_e2 eval_e_env"
THEN pose_proof binop_inv "eval_inv" [`eps:real`;`(updEnv 2 (v2:real) (updEnv 1 (v1:real) (cenv:num->real))):env_ty`; `b:binop`; `(Var 1):(real)exp`; `(Var 2):(real)exp`; `v:real`] ["eval_e_env"]
THEN destruct "eval_inv" "@d2. @v11. @v22. v_eq eval_e1 eval_e2 d_leq"
THEN LABEL_TAC "eval_cases" eval_exp_RULES THEN destruct "eval_cases" "_ _ _ binop_case"
THEN ASM_SIMP_TAC[]
THEN mp_asm "binop_case" THEN split
THEN rewrite var_equiv "eval_e1"
THEN rewrite var_equiv "eval_e2"
THEN SUBGOAL_TAC "cond_eq" `1:num = 2 <=> F` [ARITH_TAC]
THEN ASM_SIMP_TAC[updEnv]
]);;
......@@ -25,6 +25,11 @@ let reflexivity =
let auto = TRY reflexivity THEN TRY (ASM_SIMP_TAC[]);;
let rec existsl tlist =
match tlist with
| [] -> ALL_TAC
| tr::tlist -> EXISTS_TAC tr THEN (exsistsl tlist);;
(* Abbreviation! *)
let lcontra asm ty = lcontradiction asm ty;;
......
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