Commit 316bad71 authored by Joachim Bard's avatar Joachim Bard

Proving last part for soundness of SubdivChecker

parent c00f40b3
......@@ -95,10 +95,26 @@ Proof.
apply orb_true_iff.
apply andb_true_iff in Hdiv as [Herr Hdiv].
apply orb_true_iff in Hdiv as [Hdiv | Hdiv]; [left | right].
* Flover_compute.
* apply andb_true_iff in Hdiv as [Hle Hneq].
apply andb_true_iff.
admit.
* admit.
apply Qle_bool_iff in Herr.
apply Qle_bool_iff in Hle.
split; [apply Qle_bool_iff; lra |].
destruct (Qeq_bool (snd ivA2) 0) eqn: H; auto.
apply Qeq_bool_iff in H.
assert (snd ivA2 + errA2 == 0) as Heq by lra.
apply Qeq_bool_iff in Heq.
now rewrite Heq in Hneq.
* apply andb_true_iff in Hdiv as [Hle Hneq].
apply andb_true_iff.
apply Qle_bool_iff in Herr.
apply Qle_bool_iff in Hle.
split; [apply Qle_bool_iff; lra |].
destruct (Qeq_bool (fst ivA2) 0) eqn: H; auto.
apply Qeq_bool_iff in H.
assert (fst ivA2 - errA2 == 0) as Heq by lra.
apply Qeq_bool_iff in Heq.
now rewrite Heq in Hneq.
+ destruct (FloverMap.find (Binop b e1 e2) A2) as [[iv2 err2]|] eqn: Hfind2; try congruence.
kill_trivial_exists. exists vR.
apply andb_true_iff in Hleq as [Hsub _].
......@@ -127,7 +143,7 @@ Proof.
now rewrite L1, R2.
+ kill_trivial_exists. exists vR. canonize_hyps; cbn in *.
repeat split; auto; lra.
Admitted.
Qed.
Lemma resultLeq_error_sound e A1 A2 E1 E2 Gamma :
resultLeq e A1 A2 = true ->
......
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