Commit 05f76de4 authored by ='s avatar =

Cheats removed

parent f0dec55f
......@@ -2228,7 +2228,7 @@ val validErrorbound_sound = store_thm ("validErrorbound_sound",
>- (drule validErrorboundCorrectVariable
\\ disch_then (qspecl_then [`E1`, `E2`, `absenv`, `fVars`, `dVars`, `nR`, `nF`, `err`, `elo`, `ehi`, `P`, `m`] match_mp_tac)
\\ fs [])
>- (`m = m'` by (cheat) \\ rveq
>- (`m = m'` by (fs [Once eval_exp_cases_old]) \\ rveq
\\ drule validErrorboundCorrectConstant
\\ disch_then (
qspecl_then [`E2`, `absenv`, `nF`, `err`, `elo`, `ehi`, `dVars`, `Gamma`]
......@@ -2392,7 +2392,7 @@ val validErrorbound_sound = store_thm ("validErrorbound_sound",
>- (simp [Once typeCheck_def])
>- (rw [Once validErrorbound_def] \\ fs [])
>- (fs [] \\ fs [IVhi_def, IVlo_def] \\ fs [IVhi_def, IVlo_def] \\ fs [IVhi_def, IVlo_def])))
>- (`m = m'` by (cheat) \\ fs[] \\ rveq (* TODO: ask Magnus *)
>- (`m = m'` by (fs [Once eval_exp_cases_old]) \\ fs[] \\ rveq
\\ `Gamma (Downcast m e) = SOME m` by (match_mp_tac typingSoundnessExp \\ qexistsl_tac [`nF`, `E2`, `defVars`] \\ fs [])
\\ qpat_x_assum `typeCheck _ defVars Gamma` (fn thm => ASSUME_TAC (ONCE_REWRITE_RULE [typeCheck_def] thm)) \\ fs [] \\ rveq
\\ qpat_x_assum `Gamma _ = _` (fn thm => fs [thm] \\ ASSUME_TAC thm)
......
......@@ -101,6 +101,9 @@ val (eval_exp_rules, eval_exp_ind, eval_exp_cases) = Hol_reln `
eval_exp E defVars f1 v1 m1 ==>
eval_exp E defVars (Downcast m f1) (perturb v1 delta) m)`;
val eval_exp_cases_old = save_thm ("eval_exp_cases_old", eval_exp_cases);
(**
Generate a better case lemma
**)
......
......@@ -421,44 +421,44 @@ val validIntervalboundsCmd_sound = store_thm ("validIntervalboundsCmd_sound",
\\ fs [domain_union]
\\ CCONTR_TAC \\ metis_tac []));
val validIntervalbounds_validates_iv = store_thm ("validIntervalbounds_validates_iv",
``!(f:real exp) (absenv:analysisResult) (P:precond) (dVars:num_set).
(!v. v IN domain dVars ==>
valid (FST (absenv (Var v)))) /\
validIntervalbounds f absenv P dVars ==>
valid (FST (absenv f))``,
cheat
(* Induct
\\ rpt strip_tac \\ fs [Once validIntervalbounds_def]
>- (first_x_assum (fn thm => qspecl_then [`n`] ASSUME_TAC thm)
\\ Cases_on `absenv (Var n)` \\ fs[])
>- (Cases_on `absenv (Param n)` \\ fs[valid_def, isSupersetInterval_def]
\\ match_mp_tac REAL_LE_TRANS
\\ asm_exists_tac
\\ CONJ_TAC \\ TRY (simp[])
\\ match_mp_tac REAL_LE_TRANS
\\ asm_exists_tac
\\ CONJ_TAC \\ simp[])
>- (Cases_on `absenv (Const v)` \\ fs[isSupersetInterval_def, valid_def]
\\ match_mp_tac REAL_LE_TRANS
\\ asm_exists_tac \\ CONJ_TAC \\ fs[IVlo_def, IVhi_def])
>- (Cases_on `absenv (Unop u f)` \\ fs[]
\\ qpat_x_assum `validIntervalbounds _ _ _ _` (fn thm => ASSUME_TAC (ONCE_REWRITE_RULE[validIntervalbounds_def] thm))
\\ `valid (FST (absenv f))`
by (first_x_assum match_mp_tac \\
qexists_tac `P` \\ qexists_tac `dVars`
\\ fs[])
\\ Cases_on `absenv f` \\ fs[]
\\ Cases_on `u` \\ fs[isSupersetInterval_def]
>- (`valid (negateInterval q')` by (match_mp_tac iv_neg_preserves_valid \\ fs[])
\\ fs[valid_def]
\\ match_mp_tac REAL_LE_TRANS
\\ asm_exists_tac \\ fs[]
\\ match_mp_tac REAL_LE_TRANS
\\ asm_exists_tac \\ fs[])
>- (cheat) (* FIXME: ONLY TWO CASES! *)
>- (cheat))
>- (cheat) *)
);
(* val validIntervalbounds_validates_iv = store_thm ("validIntervalbounds_validates_iv", *)
(* ``!(f:real exp) (absenv:analysisResult) (P:precond) (dVars:num_set). *)
(* (!v. v IN domain dVars ==> *)
(* valid (FST (absenv (Var v)))) /\ *)
(* validIntervalbounds f absenv P dVars ==> *)
(* valid (FST (absenv f))``, *)
(* cheat *)
(* Induct *)
(* \\ rpt strip_tac \\ fs [Once validIntervalbounds_def] *)
(* >- (first_x_assum (fn thm => qspecl_then [`n`] ASSUME_TAC thm) *)
(* \\ Cases_on `absenv (Var n)` \\ fs[]) *)
(* >- (Cases_on `absenv (Param n)` \\ fs[valid_def, isSupersetInterval_def] *)
(* \\ match_mp_tac REAL_LE_TRANS *)
(* \\ asm_exists_tac *)
(* \\ CONJ_TAC \\ TRY (simp[]) *)
(* \\ match_mp_tac REAL_LE_TRANS *)
(* \\ asm_exists_tac *)
(* \\ CONJ_TAC \\ simp[]) *)
(* >- (Cases_on `absenv (Const v)` \\ fs[isSupersetInterval_def, valid_def] *)
(* \\ match_mp_tac REAL_LE_TRANS *)
(* \\ asm_exists_tac \\ CONJ_TAC \\ fs[IVlo_def, IVhi_def]) *)
(* >- (Cases_on `absenv (Unop u f)` \\ fs[] *)
(* \\ qpat_x_assum `validIntervalbounds _ _ _ _` (fn thm => ASSUME_TAC (ONCE_REWRITE_RULE[validIntervalbounds_def] thm)) *)
(* \\ `valid (FST (absenv f))` *)
(* by (first_x_assum match_mp_tac \\ *)
(* qexists_tac `P` \\ qexists_tac `dVars` *)
(* \\ fs[]) *)
(* \\ Cases_on `absenv f` \\ fs[] *)
(* \\ Cases_on `u` \\ fs[isSupersetInterval_def] *)
(* >- (`valid (negateInterval q')` by (match_mp_tac iv_neg_preserves_valid \\ fs[]) *)
(* \\ fs[valid_def] *)
(* \\ match_mp_tac REAL_LE_TRANS *)
(* \\ asm_exists_tac \\ fs[] *)
(* \\ match_mp_tac REAL_LE_TRANS *)
(* \\ asm_exists_tac \\ fs[]) *)
(* >- (cheat) (* FIXME: ONLY TWO CASES! *) *)
(* >- (cheat)) *)
(* >- (cheat) *)
(* ); *)
val _ = export_theory();
......@@ -82,8 +82,8 @@ val typeCheck_def = Define `
/\ typeCheck e1 defVars tMap
/\ typeCheck e2 defVars tMap)
| _, _, _ => F)
| Downcast m e1 => (case tMap e, tMap e1 of
| SOME m', SOME m1 => (m = m') /\ isMorePrecise m1 m
| Downcast m_ e1 => (case tMap e, tMap e1 of
| SOME m', SOME m1 => (m' = m_) /\ isMorePrecise m1 m_
/\ typeCheck e1 defVars tMap
| _, _ => F)`
......@@ -107,9 +107,8 @@ val typingSoundnessExp = store_thm("typingSoundnessExp",
>- (inversion `eval_exp _ _ _ _ _` eval_exp_cases \\ rveq \\ fs []
\\ fs [typeCheck_def]
\\ Cases_on `Gamma (Var n)` \\ fs [])
>- (fs [typeCheck_def]
(* TODO: Ask magnus about a way to prove that m = m' in this eval_exp *)
\\ cheat)
>- (fs [typeCheck_def, Once eval_exp_cases_old] \\ rveq \\ fs[]
\\ Cases_on `Gamma (Const m v)` \\ fs [])
>- (qpat_x_assum `typeCheck _ _ _` (fn thm => ASSUME_TAC (ONCE_REWRITE_RULE [typeCheck_def] thm)) \\ fs []
\\ Cases_on `Gamma (Unop u e)` \\ rveq \\ fs []
\\ Cases_on `Gamma e` \\ rveq \\ fs []
......@@ -126,11 +125,9 @@ val typingSoundnessExp = store_thm("typingSoundnessExp",
\\ `x'' = m2` by (fs [SOME_11])
\\ rveq \\ fs [])
>- (qpat_x_assum `typeCheck _ _ _` (fn thm => ASSUME_TAC (ONCE_REWRITE_RULE [typeCheck_def] thm)) \\ fs []
\\ `m = m'` by (fs [Once eval_exp_cases_old]) \\ rveq \\ fs []
\\ Cases_on `Gamma (Downcast m e)` \\ rveq \\ fs []
\\ Cases_on `Gamma e` \\ rveq \\ fs []
\\ inversion `eval_exp _ _ _ _ _` eval_exp_cases \\ rveq \\ fs []
\\ cheat
(* SAME TODO AS ABOVE. *)));
\\ Cases_on `Gamma e` \\ rveq \\ fs []));
val typingSoundnessCmd = store_thm("typingSoundnessCmd",
``!(c:real cmd) (defVars:num -> mType option) (E:env) (v:real) (m:mType) (Gamma:real exp -> mType option).
......
......@@ -18,9 +18,9 @@ for file in "${arr[@]}"
do
echo $file
echo "Coq certificate"
/usr/bin/time -o $1 -a -f "%C %E" ./daisy $file --certificate=coq >/dev/null
/usr/bin/time -o $1 -a -f "%C %E" ./daisy $file --certificate=coq --randomMP >/dev/null
echo "HOL Certificate"
/usr/bin/time -o $1 -a -f "%C %E" ./daisy $file --certificate=hol4 >/dev/null
/usr/bin/time -o $1 -a -f "%C %E" ./daisy $file --certificate=hol4 --randomMP >/dev/null
echo ""
done
......@@ -28,29 +28,30 @@ echo ""
echo "[Certificate Test]"
echo ""
cd coq
arrCoq=()
cd ./hol4/output
arrHOL=()
while IFS= read -r -d $'\0'; do
arrCoq+=("$REPLY")
done < <(find ./output/ -name "*.v" -print0)
arrHOL+=("$REPLY")
done < <(find ./ -name "*Script.sml" -print0)
for file in "${arrCoq[@]}"
for file in "${arrHOL[@]}"
do
echo $file
echo ""
/usr/bin/time -o $1 -a -f "%C %E" coqc -R ./ Daisy $file
/usr/bin/time -o $1 -a -f "%C %E" Holmake ${file/Script.sml/Theory.sig}
done
cd ../hol4/output
arrHOL=()
cd ../../coq
arrCoq=()
while IFS= read -r -d $'\0'; do
arrHOL+=("$REPLY")
done < <(find ./ -name "*Script.sml" -print0)
arrCoq+=("$REPLY")
done < <(find ./output/ -name "*.v" -print0)
for file in "${arrHOL[@]}"
for file in "${arrCoq[@]}"
do
echo $file
echo ""
/usr/bin/time -o $1 -a -f "%C %E" $HOLDIR/bin/Holmake ${file/Script.sml/Theory.sig}
/usr/bin/time -o $1 -a -f "%C %E" coqc -R ./ Daisy $file
done
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