Commit 7fefc298 authored by Joachim Bard's avatar Joachim Bard

proving remaining lemma for subdiv checker

parent 93b38ab7
......@@ -19,7 +19,7 @@ Definition CertificateChecker (e: expr Q) (absenv: analysisResult)
|Succes Gamma =>
match subdivs with
| [] => ResultChecker e absenv P Qmap defVars Gamma
| hd :: tl => SubdivsChecker e absenv P hd tl defVars Gamma
| _ => SubdivsChecker e absenv P subdivs defVars Gamma
end
| _ => false
end.
......
......@@ -54,19 +54,12 @@ Proof.
- exfalso. eapply He. set_tac.
Qed.
Definition checkSubdivsStep e absenv defVars Gamma (b: bool) (PA: precond * analysisResult) :=
Definition checkSubdivsStep e absenv defVars Gamma (PA: precond * analysisResult) :=
let (P, A) := PA in
b && (RangeErrorChecker e A P (FloverMap.empty(SMTLogic * SMTLogic)) defVars Gamma) &&
resultLeq e A absenv.
(RangeErrorChecker e A P (FloverMap.empty(SMTLogic * SMTLogic)) defVars Gamma) && resultLeq e A absenv.
Definition checkSubdivs e absenv subdivs defVars Gamma :=
fold_left (checkSubdivsStep e absenv defVars Gamma) subdivs true.
Lemma checkSubdivs_false_fp e absenv subdivs defVars Gamma :
fold_left (checkSubdivsStep e absenv defVars Gamma) subdivs false = false.
Proof.
induction subdivs as [|[P A] subdivs]; auto.
Qed.
forallb (checkSubdivsStep e absenv defVars Gamma) subdivs.
Lemma checkSubdivs_sound e absenv subdivs defVars Gamma P A :
checkSubdivs e absenv subdivs defVars Gamma = true ->
......@@ -77,16 +70,12 @@ Proof.
intros H Hin.
induction subdivs; cbn in Hin; auto.
destruct Hin; subst; auto.
- cbn in *.
destruct (RangeErrorChecker e A P (FloverMap.empty (SMTLogic * SMTLogic)) defVars Gamma) eqn:?;
try (rewrite checkSubdivs_false_fp in H; discriminate H).
split; auto.
destruct (resultLeq e A absenv) eqn: ?; auto.
rewrite checkSubdivs_false_fp in H; auto.
- cbn in H.
apply andb_true_iff in H as [H _].
apply andb_true_iff in H as [H1 H2].
now split.
- apply IHsubdivs; auto. cbn in H.
unfold checkSubdivs.
destruct (checkSubdivsStep e absenv defVars Gamma true a) eqn:?; auto.
rewrite checkSubdivs_false_fp in H. discriminate H.
now apply andb_true_iff in H as [_ H ].
Qed.
Fixpoint coverIntv iv intvs :=
......@@ -115,68 +104,83 @@ Proof.
cbn in *. lra.
Qed.
Fixpoint getBucket x iv Ps :=
Fixpoint getSlice x iv Ps :=
match Ps with
| nil => (nil, nil)
| P :: Ps' =>
match P with
| nil => (nil, Ps) (* fail *)
| (e, ivE) :: P' =>
match Q_orderedExps.compare e (Var Q x) with
| Eq =>
if isSupersetIntv iv ivE then
let (b, rest) := getBucket x iv Ps' in (P' :: b, rest)
else (nil, Ps)
| _ => (nil, Ps) (* fail *)
end
if FloverMapFacts.P.F.eqb (Var Q x) e && isSupersetIntv iv ivE then
let (sl, rest) := getSlice x iv Ps' in (P' :: sl, rest)
else (nil, Ps)
end
end.
Lemma getBucket_length x iv Ps b rest :
getBucket x iv Ps = (b, rest) ->
length Ps = length (b ++ rest).
Lemma getSlice_length x iv Ps sl rest :
getSlice x iv Ps = (sl, rest) ->
length Ps = length (sl ++ rest).
Proof with try now injection 1; intros; subst.
induction Ps as [|P Ps] in b |- *; cbn...
induction Ps as [|P Ps] in sl |- *; cbn...
destruct P as [|[e ivE] P]...
destruct (Q_orderedExps.compare e (Var Q x)) eqn:?...
destruct (FloverMapFacts.P.F.eqb (Var Q x) e) eqn:?...
destruct (isSupersetIntv iv ivE) eqn:?...
destruct (getBucket x iv Ps) eqn:?...
destruct (getSlice x iv Ps) eqn:?...
injection 1; intros; subst.
cbn. now rewrite <- IHPs.
Qed.
Lemma getBucket_sound x iv Ps b rest :
getBucket x iv Ps = (b, rest) ->
forall P, In P b ->
Lemma getSlice_sound x iv Ps sl rest :
getSlice x iv Ps = (sl, rest) ->
forall P, In P sl ->
exists ivx, In ((Var Q x, ivx) :: P) Ps /\ isSupersetIntv iv ivx = true.
Proof with try now injection 1; intros; subst.
induction Ps as [|P1 Ps] in b |- *; cbn...
induction Ps as [|P1 Ps] in sl |- *; cbn...
destruct P1 as [|[e ivE] P1]...
cbn.
destruct (Q_orderedExps.compare e (Var Q x)) eqn:Heqc...
destruct (FloverMapFacts.P.F.eqb (Var Q x) e) eqn:?...
destruct (isSupersetIntv iv ivE) eqn:?...
destruct (getBucket x iv Ps) eqn:?...
destruct (getSlice x iv Ps) eqn:?...
injection 1; intros; subst.
destruct H2 as [-> | Hin].
- assert (e = Var Q x)
by (destruct e; try discriminate Heqc;
now rewrite (nat_compare_eq _ _ Heqc)).
- apply eqb_var in Heqb.
exists ivE. subst. split; auto.
- edestruct IHPs as [ivx [inPs sub]]; eauto.
Qed.
Lemma getBucket_rest_sound x iv Ps b rest :
getBucket x iv Ps = (b, rest) ->
Lemma getSlice_rest_sound x iv Ps sl rest :
getSlice x iv Ps = (sl, rest) ->
forall P, In P rest -> In P Ps.
Proof with try now injection 1; intros; subst.
induction Ps as [|P Ps] in b |- *; cbn...
induction Ps as [|P Ps] in sl |- *; cbn...
destruct P as [|[e ivE] P]...
destruct (Q_orderedExps.compare e (Var Q x)) eqn:?...
destruct (FloverMapFacts.P.F.eqb (Var Q x) e) eqn:?...
destruct (isSupersetIntv iv ivE) eqn:?...
destruct (getBucket x iv Ps) eqn:?...
destruct (getSlice x iv Ps) eqn:?...
injection 1; intros; subst.
right. eapply IHPs; eauto.
Qed.
Lemma getSlice_complete x iv Ps sl rest :
getSlice x iv Ps = (sl, rest) ->
forall P, In P Ps ->
In P rest \/ exists P1 ivx, P = (Var Q x, ivx) :: P1 /\ In P1 sl.
Proof with try now injection 1; intros; subst; auto.
induction Ps as [|P Ps] in sl |- *...
destruct P as [|[e ivE] P]...
cbn.
destruct (FloverMapFacts.P.F.eqb (Var Q x) e) eqn:?...
destruct (isSupersetIntv iv ivE) eqn:?...
destruct (getSlice x iv Ps) eqn:?...
apply eqb_var in Heqb.
cbn.
injection 1; intros; subst.
destruct H2 as [<- | H2].
- right. exists P, ivE. split; now constructor.
- edestruct IHPs as [Hin | [P1 [ivx [Heq Hin]]]]; eauto.
right. exists P1, ivx. split; auto. now constructor 2.
Qed.
(*
Function checkDim cov x iv Ps {measure length Ps} :=
match Ps with
......@@ -184,7 +188,7 @@ Function checkDim cov x iv Ps {measure length Ps} :=
| P :: _ =>
match FloverMap.find (Var Q x) P with
| Some ivx =>
let (b, rest) := getBucket_aux x ivx Ps in
let (b, rest) := getSlice_aux x ivx Ps in
let covb := cov b in
covb && match rest with
| nil => isSupersetIntv iv ivx
......@@ -197,14 +201,14 @@ intros cov x iv Ps P Ps' HPs ivx Hfind b rest P' rest' Hrest.
rewrite <- Hrest.
rewrite <- HPs at 2.
cbn.
unfold addToBucket.
unfold addToSlice.
rewrite Hfind.
unfold isSupersetIntv, Qleb, Qle_bool.
rewrite !Z.leb_refl.
rewrite <- HPs.
cbn.
destruct (getBucket_aux x ivx Ps') eqn:Heq.
apply getBucket_aux_sound in Heq.
destruct (getSlice_aux x ivx Ps') eqn:Heq.
apply getSlice_aux_sound in Heq.
clear Hrest rest'.
injection 1; intros; subst.
cbn.
......@@ -219,27 +223,27 @@ Function checkDim cov x iv Ps {measure length Ps} :=
| P :: _ =>
match P with
| (e, ivx) :: _ =>
match Q_orderedExps.compare e (Var Q x) with
| Eq =>
let (b, rest) := getBucket x ivx Ps in
if isSupersetIntv iv ivx then cov b
else cov b && Qleb (fst ivx) (fst iv) && checkDim cov x (snd ivx, snd iv) rest
| _ => false
end
if FloverMapFacts.P.F.eqb (Var Q x) e then
let (sl, rest) := getSlice x ivx Ps in
match rest with
| nil => cov sl && isSupersetIntv iv ivx
| _ => cov sl && Qleb (fst ivx) (fst iv) && checkDim cov x (snd ivx, snd iv) rest
end
else false
| _ => false
end
end.
intros cov x iv Ps P rest [e ivE] b e' ivx H HP HPs Heq b' rest'.
intros cov x iv Ps P Ps' [e ivE] P' e' ivx H HP HPs Heq sl rest l1 l2 <-.
rewrite <- HPs at 2.
cbn.
rewrite Heq.
unfold isSupersetIntv, Qleb, Qle_bool.
rewrite !Z.leb_refl.
rewrite <- HPs.
destruct (getBucket x ivx rest) eqn:Hb.
destruct (getSlice x ivx Ps') eqn:Hsl.
injection 1; intros; subst.
cbn.
rewrite (getBucket_length _ _ _ Hb); eauto.
rewrite (getSlice_length _ _ _ Hsl); eauto.
rewrite app_length.
apply le_lt_n_Sm, le_plus_r.
Defined.
......@@ -268,9 +272,10 @@ Proof.
as [v [inE iniv]]
by (apply HPl; now constructor).
functional induction checkDim (covers P) n iv Ps; try discriminate H.
+ destruct (IHP _ H) as [P' [inb HP']].
+ apply andb_true_iff in H as [H Hsub].
destruct (IHP _ H) as [P' [inb HP']].
{ hnf. intros. apply HPl. now constructor. }
destruct (getBucket_sound _ _ _ e3 _ inb) as [iv1 [Hin1 Hsub1]].
destruct (getSlice_sound _ _ _ e3 _ inb) as [iv1 [Hin1 Hsub1]].
eexists; split; eauto.
intros x iv' [Heq | inP']; auto.
injection Heq. intros; subst.
......@@ -283,7 +288,7 @@ Proof.
destruct (Rle_or_lt v (Q2R (snd ivx))) as [Hle|Hlt].
* destruct (IHP _ L0) as [P' [inb HP']].
{ hnf. intros. apply HPl. now constructor. }
destruct (getBucket_sound _ _ _ e3 _ inb) as [iv1 [Hin1 Hsub1]].
destruct (getSlice_sound _ _ _ e3 _ inb) as [iv1 [Hin1 Hsub1]].
eexists; split; eauto.
intros x iv' [Heq | inP']; auto.
injection Heq. intros; subst.
......@@ -294,14 +299,13 @@ Proof.
exists v. split; [auto | lra].
* assert (Q2R (snd ivx) <= v <= Q2R (snd iv))%R as Hv.
{ unfold isSupersetIntv in *. cbn in *.
rewrite R0 in *. cbn in *.
canonize_hyps. split; lra. }
lra. }
destruct IHb0 as [P' [inrest H]]; auto.
{ intros x iv' [Heq | inP]; auto.
injection Heq; intros; subst.
cbn. exists v. split; auto. apply HPl; cbn; auto. }
exists P'; split; auto.
eapply getBucket_rest_sound; eauto.
eapply getSlice_rest_sound; eauto.
Qed.
Lemma covers_preVars P Ps :
......@@ -313,7 +317,26 @@ Proof.
intros _ P [H|[]].
rewrite <- H. cbn. apply NatSetProps.equal_refl.
- cbn. destruct e; try discriminate 1.
Admitted.
fold (preIntvVars P).
functional induction (checkDim (covers P) n iv Ps); try discriminate 1.
+ intros H P1 Hin.
apply andb_true_iff in H as [H _].
rename e3 into Hsl.
eapply getSlice_complete in Hsl; eauto.
destruct Hsl as [[] | [P2 [ivn [-> insl]]]].
cbn.
apply NatSetProps.FM.add_m; auto.
eapply IHP; eauto.
+ intros H P1 Hin.
Flover_compute.
rename e3 into Hsl.
eapply getSlice_complete in Hsl; eauto.
destruct Hsl as [inrest | [P2 [ivn [-> insl]]]].
* apply IHb0; auto.
* cbn.
apply NatSetProps.FM.add_m; auto.
eapply IHP; eauto.
Qed.
Definition checkPreconds (subdivs: list precond) (P: precond) :=
let Piv := FloverMap.elements (fst P) in
......@@ -356,21 +379,21 @@ Qed.
(* TODO: merge hd and tl again *)
(** Interval subdivisions checking function **)
Definition SubdivsChecker (e: expr Q) (absenv: analysisResult)
(P: precond) hd tl (defVars: FloverMap.t mType) Gamma :=
(P: precond) subdivs (defVars: FloverMap.t mType) Gamma :=
validSSA e (preVars P) &&
checkPreconds (map fst (hd :: tl)) P &&
checkSubdivs e absenv (hd :: tl) defVars Gamma.
checkPreconds (map fst subdivs) P &&
checkSubdivs e absenv subdivs defVars Gamma.
(**
Soundness proof for the interval subdivs checker.
**)
Theorem subdivs_checking_sound (e: expr Q) (absenv: analysisResult) P hd_subdivs tl_subdivs defVars Gamma:
Theorem subdivs_checking_sound (e: expr Q) (absenv: analysisResult) P subdivs defVars Gamma:
forall (E1 E2: env) DeltaMap,
(forall (e': expr R) (m': mType),
exists d: R, DeltaMap e' m' = Some d /\ (Rabs d <= mTypeToR m')%R) ->
eval_precond E1 P ->
getValidMap defVars e (FloverMap.empty mType) = Succes Gamma ->
SubdivsChecker e absenv P hd_subdivs tl_subdivs defVars Gamma = true ->
SubdivsChecker e absenv P subdivs defVars Gamma = true ->
exists Gamma,
approxEnv E1 (toRExpMap Gamma) absenv (freeVars e) NatSet.empty E2 ->
exists iv err vR vF m,
......@@ -384,7 +407,7 @@ Proof.
intros * deltas_matched P_valid valid_typeMap chk.
apply andb_prop in chk as [chk valid_subdivs].
apply andb_prop in chk as [valid_ssa valid_cover].
eapply (checkPreconds_sound (* (hd_subdivs :: tl_subdivs) *)) in P_valid as [P1 [in_subdivs P_valid]]; eauto.
eapply (checkPreconds_sound) in P_valid as [P1 [in_subdivs P_valid]]; eauto.
assert (validSSA e (preVars P1) = true) as valid_ssa'.
{ eapply validSSA_eq_set; eauto. eapply checkPreconds_preVars; eauto. }
apply in_map_iff in in_subdivs as [[P2 A] [Heq in_subdivs]].
......
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