Commit 703be8b5 authored by Joachim Bard's avatar Joachim Bard
Browse files

minor simplifications for precond checker

parent 06604887
......@@ -502,6 +502,7 @@ Proof.
Qed.
(* checker for precondition *)
(* not needed
Fixpoint checkPrelist (lP: list (FloverMap.key * intv)) C q : bool :=
match lP, q with
| List.nil, _ => SMTLogic_eqb C q
......@@ -509,6 +510,7 @@ Fixpoint checkPrelist (lP: list (FloverMap.key * intv)) C q : bool :=
| List.cons (Var _ x, _) _, _ => false
| List.cons el lP', _ => checkPrelist lP' C q
end.
*)
(*
Lemma checkPrelist_LessQ lP C e1 e2 : checkPrelist lP C (LessQ e1 e2) = false.
......@@ -542,22 +544,32 @@ Proof.
Qed.
*)
Definition checkPre (P: precond) q := checkPrelist (FloverMap.elements (fst P)) (snd P) q.
(* Definition checkPre (P: precond) q := checkPrelist (FloverMap.elements (fst P)) (snd P) q. *)
Definition checkPre (P: precond) q := SMTLogic_eqb (precond2SMT P) q.
Lemma checkPre_precond P : checkPre P (precond2SMT P) = true.
Proof.
(*
unfold precond2SMT, checkPre.
destruct P as [Piv C]. cbn.
induction (FloverMap.elements Piv) as [|[e [lo hi]] l IHl]; cbn.
- apply SMTLogic_eqb_refl.
- destruct e; cbn; auto.
now rewrite Nat.eqb_refl, !Qeq_bool_refl, IHl.
*)
unfold checkPre. apply SMTLogic_eqb_refl.
Qed.
Lemma checkPre_pre_smt E P q :
checkPre P q = true ->
eval_precond E P ->
eval_smt_logic E q.
Proof.
intros Heq HP.
apply (SMTLogic_eqb_sound _ _ _ Heq).
now apply pre_to_smt_correct.
Qed.
(*
Proof with try discriminate.
unfold checkPre, eval_precond, eval_preIntv.
destruct P as [Piv C]. cbn.
......@@ -589,6 +601,7 @@ Proof with try discriminate.
exists v, (Q2R r'). repeat split; try now constructor. erewrite Qeq_eqR; now eauto.
+ apply IHl; auto.
Qed.
*)
(*
Lemma checkPre_smt_pre E P q :
......
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