Commit 8bc8c028 authored by Nikita Zyuzin's avatar Nikita Zyuzin

Complete proofs in RealRangeValidator;

Progress on validAffineBoundsCmd
parent 9e2ebfc6
......@@ -494,33 +494,6 @@ Proof.
now apply (fresh_noise _ freshn1).
Lemma plus_aff_contaiment a1 a2 v1 v2:
contained v1 (toInterval a1) ->
contained v2 (toInterval a2) ->
contained (v1 + v2) (toInterval (plus_aff a1 a2)).
revert v1 v2.
remember (a1, a2) as a12.
assert (fst a12 = a1 /\ snd a12 = a2) as Havals by now rewrite Heqa12.
destruct Havals as [Heqa1 Heqa2].
rewrite <- Heqa1, <- Heqa2.
clear Heqa1 Heqa2 Heqa12 a1 a2.
unfold plus_aff.
rewrite <- surjective_pairing.
functional induction (plus_aff_tuple a12); intros v__a1 v__a2 cont1 cont2;
simpl fst in *; simpl snd in *.
- simpl in *; lra.
- unfold toInterval in *.
simpl get_const in *.
simpl radius in *.
specialize (IHa v__a1).
(* Lemma contained_noise v a n nv: *)
(* contained v (toInterval (Noise n nv a)) -> *)
(* contained v (fst (toInterval a) - Rabs nv, snd (toInterval a) + Rabs nv). *)
(* contained x (toInterval a). *)
(***** Multiplication of two affine forms ******)
This diff is collapsed.
......@@ -39,7 +39,7 @@ Proof.
assert (affine_dVars_range_valid NatSet.empty E A) as HdVarsValid
by (unfold affine_dVars_range_valid; intros * H; set_tac).
assert (NatSet.Subset (usedVars f -- NatSet.empty) (usedVars f)) as Hsubset by set_tac.
assert (affine_fVars_P_sound (usedVars f) E P) as HfVars by admit.
assert (affine_fVars_P_sound (usedVars f) E P) as HfVars by exact H0.
assert (affine_vars_typed (usedVars f NatSet.empty) Gamma) as Hvarstyped
by (unfold affine_vars_typed; intros v in_set; set_tac; destruct in_set; set_tac).
specialize (sound_affine f A P (usedVars f) NatSet.empty E Gamma
......@@ -60,4 +60,4 @@ Proof.
simpl in Heval.
destruct Heval as [Heval1 Heval2].
split; eauto using Rle_trans.
Markdown is supported
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment