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

Add small docstring to subdiv checker

parent f8feba16
......@@ -610,7 +610,12 @@ Definition checkPreconds (subdivs: list precond) (P: precond) :=
let Piv := FloverMap.elements (fst P) in
let Ps := map (fun P => FloverMap.elements (fst P)) subdivs in
let S_qs := map snd subdivs in
covers Piv (sort Ps) && forallbTailrec (fun q => SMTLogic_eqb q (snd P)) S_qs.
(* Check that join of the preconditions for the subdivisions
covers the global precondition *)
covers Piv (sort Ps) &&
(* Check that additional constraints encoded by Daisy agree
for each subdivision *)
forallbTailrec (fun q => SMTLogic_eqb q (snd P)) S_qs.
Lemma checkPreconds_sound (subdivs: list precond) E P :
checkPreconds subdivs P = true ->
......@@ -703,7 +708,7 @@ Proof.
{ apply unsat_qs. apply in_map_iff. now exists (P1, A, Qmap). }
repeat split; eauto using resultLeq_range_sound, resultLeq_error_sound.
exists Gamma; intros approxE1E2.
assert (approxEnv E1 (toRExpMap Gamma) A (freeVars e) NatSet.empty E2) as approxE1E2'
Supports Markdown
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