Commit a91b364b authored by Nikita Zyuzin's avatar Nikita Zyuzin

Progress validation cmd soundness

parent 231e24bf
......@@ -2098,7 +2098,7 @@ Proof.
intros e' Hsome.
specialize (visitedExpr e').
specialize (visitedNewexpr e').
destruct (FloverMap.find (elt:=affine_form Q) e' iexpmap) eqn: ?.
destruct (FloverMap.find e' iexpmap) eqn: ?.
- specialize (visitedExpr ltac:(eauto)).
apply checked_expressions_contained with (expmap1 := iexpmap) (map1 := map1)
(noise1 := inoise); eauto.
......@@ -2113,7 +2113,18 @@ Proof.
exists af', vR', aiv', aerr'.
intuition.
admit.
- admit.
- destruct (FloverMap.find e' exprAfs') eqn: ?.
+ specialize (visitedNewexpr ltac:(eauto) ltac:(eauto)).
unfold checked_expressions in visitedNewexpr |-*.
destruct visitedNewexpr as [af' [vR' [aiv' [aerr' visitedNewexpr]]]].
destruct (FloverMapFacts.O.MO.eq_dec (Var Q n) e');
try (erewrite FloverMapFacts.P.F.find_o in Heqo0;
try eapply Q_orderedExps.expCompare_eq_sym; eauto; congruence).
exists af', vR', aiv', aerr'.
intuition.
* rewrite FloverMapFacts.P.F.add_neq_o; eauto.
* admit.
+ admit.
}
assert (contained_map map1 ihmap) as ?
by (etransitivity; eassumption).
......
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