Commit 02b248c7 authored by Heiko Becker's avatar Heiko Becker
Browse files

Do some cleanup for commented out proofs

parent 6fd90de5
......@@ -3063,6 +3063,7 @@ Proof.
}
Qed.
(*
Theorem validErrorboundAA_sound (e: expr Q) E1 E2 A Gamma DeltaMap fVars dVars:
validErrorboundAA_sound_statement e E1 E2 A Gamma DeltaMap fVars dVars.
Proof.
......@@ -3073,8 +3074,8 @@ Proof.
- apply validErrorboundAA_sound_binop; auto.
- apply validErrorboundAA_sound_fma; auto.
- apply validErrorboundAA_sound_downcast; auto.
- admit.
Admitted.
- (*FIXME *)
Qed.
Corollary validErrorbound_sound_validErrorBounds e E1 E2 A Gamma DeltaMap expr_map noise noise_map:
(forall e' : FloverMap.key,
......@@ -3123,7 +3124,7 @@ Proof.
specialize Hsubexpr as (Hsubexpr & Hin).
unfold validErrorBounds in IHe.
split.
{ admit. (* FIXME! Invariant from checker *) }
{ (* FIXME! Invariant from checker *) }
intros * Heval__R Hcert.
specialize Hchecked as (Hex & Hall); eauto.
intuition.
......@@ -3144,7 +3145,7 @@ Proof.
specialize Hsubexpr as ((Hsubexpr1 & Hsubexpr2) & Hin).
unfold validErrorBounds in IHe1, IHe2.
split; [repeat split; try auto | ].
{ admit. }
{ (* FIXME *) }
intros * Heval__R Hcert.
specialize Hchecked as (Hex & Hall); eauto.
intuition.
......@@ -3199,8 +3200,7 @@ Proof.
end.
cbn in Hiv.
now rewrite Rabs_Rle_condition.
- admit.
Admitted.
- (* FIXME *)
(*
Definition checked_error_commands c E1 E2 A Gamma DeltaMap noise_map noise expr_map :=
......
......@@ -488,7 +488,7 @@ Proof.
+ intros.
destruct (n =? n0)%nat eqn:Heqn.
* rewrite Nat.eqb_eq in Heqn; subst.
* admit.
* (* FIXME *)
+ exists iv, err, vR; intuition.
eapply eval_expr_ssa_extension; eauto.
cbn.
......
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