Commit 68dc402f authored by Nikita Zyuzin's avatar Nikita Zyuzin

[WIP] Remove DeltaMap as a parameter for type validator

parent dcd05c90
......@@ -685,7 +685,7 @@ Lemma validAffineBounds_sound_var A P E Gamma fVars dVars n:
affine_dVars_range_valid dVars E A inoise iexpmap map1 ->
NatSet.Subset (usedVars (Var Q n) -- dVars) fVars ->
fVars_P_sound fVars E P ->
validTypes (Var Q n) Gamma DeltaMapR ->
validTypes (Var Q n) Gamma ->
exists (map2 : noise_mapping) (af : affine_form Q) (vR : R) (aiv : intv)
(aerr : error),
contained_map map1 map2 /\
......@@ -874,7 +874,7 @@ Lemma validAffineBounds_sound_const A P E Gamma fVars dVars m v:
affine_dVars_range_valid dVars E A inoise iexpmap map1 ->
NatSet.Subset (usedVars (Const m v) -- dVars) fVars ->
fVars_P_sound fVars E P ->
validTypes (Const m v) Gamma DeltaMapR ->
validTypes (Const m v) Gamma ->
exists (map2 : noise_mapping) (af : affine_form Q) (vR : R) (aiv : intv)
(aerr : error),
contained_map map1 map2 /\
......@@ -998,7 +998,7 @@ Definition validAffineBounds_IH_e A P E Gamma fVars dVars e :=
affine_dVars_range_valid dVars E A inoise iexpmap map1 ->
NatSet.Subset (usedVars e -- dVars) fVars ->
fVars_P_sound fVars E P ->
validTypes e Gamma DeltaMapR ->
validTypes e Gamma ->
exists (map2 : noise_mapping) (af : affine_form Q) (vR : R) (aiv : intv)
(aerr : error),
contained_map map1 map2 /\
......@@ -1030,7 +1030,7 @@ Lemma validAffineBounds_sound_unop A P E Gamma fVars dVars u e:
affine_dVars_range_valid dVars E A inoise iexpmap map1 ->
NatSet.Subset (usedVars (Unop u e) -- dVars) fVars ->
fVars_P_sound fVars E P ->
validTypes (Unop u e) Gamma DeltaMapR ->
validTypes (Unop u e) Gamma ->
exists (map2 : noise_mapping) (af : affine_form Q) (vR : R) (aiv : intv)
(aerr : error),
contained_map map1 map2 /\
......@@ -1221,7 +1221,7 @@ Lemma validAffineBounds_sound_binop A P E Gamma fVars dVars b e1 e2:
affine_dVars_range_valid dVars E A inoise iexpmap map1 ->
NatSet.Subset (usedVars (Binop b e1 e2) -- dVars) fVars ->
fVars_P_sound fVars E P ->
validTypes (Binop b e1 e2) Gamma DeltaMapR ->
validTypes (Binop b e1 e2) Gamma ->
exists (map2 : noise_mapping) (af : affine_form Q) (vR : R) (aiv : intv)
(aerr : error),
contained_map map1 map2 /\
......@@ -1797,7 +1797,7 @@ Lemma validAffineBounds_sound_fma A P E Gamma fVars dVars e1 e2 e3:
affine_dVars_range_valid dVars E A inoise iexpmap map1 ->
NatSet.Subset (usedVars (Fma e1 e2 e3) -- dVars) fVars ->
fVars_P_sound fVars E P ->
validTypes (Fma e1 e2 e3) Gamma DeltaMapR ->
validTypes (Fma e1 e2 e3) Gamma ->
exists (map2 : noise_mapping) (af : affine_form Q) (vR : R) (aiv : intv)
(aerr : error),
contained_map map1 map2 /\
......@@ -2086,7 +2086,7 @@ Lemma validAffineBounds_sound_downcast A P E Gamma fVars dVars m e:
affine_dVars_range_valid dVars E A inoise iexpmap map1 ->
NatSet.Subset (usedVars (Downcast m e) -- dVars) fVars ->
fVars_P_sound fVars E P ->
validTypes (Downcast m e) Gamma DeltaMapR ->
validTypes (Downcast m e) Gamma ->
exists (map2 : noise_mapping) (af : affine_form Q) (vR : R) (aiv : intv)
(aerr : error),
contained_map map1 map2 /\
......@@ -2195,7 +2195,7 @@ Lemma validAffineBounds_sound (e: expr Q) (A: analysisResult) (P: precond)
affine_dVars_range_valid dVars E A inoise iexpmap map1 ->
NatSet.Subset (NatSet.diff (Expressions.usedVars e) dVars) fVars ->
fVars_P_sound fVars E P ->
validTypes e Gamma DeltaMapR ->
validTypes e Gamma ->
exists map2 af vR aiv aerr,
contained_map map1 map2 /\
contained_flover_map iexpmap exprAfs /\
......@@ -2249,7 +2249,7 @@ Lemma validAffineBoundsCmd_sound (c: cmd Q) (A: analysisResult) (P: precond)
affine_dVars_range_valid dVars E A inoise iexpmap map1 ->
NatSet.Subset (NatSet.diff (Commands.freeVars c) dVars) fVars ->
fVars_P_sound fVars E P ->
validTypesCmd c Gamma DeltaMapR ->
validTypesCmd c Gamma ->
exists map2 af vR aiv aerr,
contained_map map1 map2 /\
contained_flover_map iexpmap exprAfs /\
......
......@@ -164,7 +164,7 @@ Section soundnessProofs.
Lemma validErrorboundCorrectVariable_eval E1 E2 A (v:nat) e nR nlo nhi fVars
dVars Gamma DeltaMap exprTypes:
eval_Real E1 Gamma (Var Q v) nR ->
validTypes (Var Q v) Gamma DeltaMap ->
validTypes (Var Q v) Gamma ->
approxEnv E1 (toRExpMap Gamma) A fVars dVars E2 ->
validRanges (Var Q v) A E1 (toRTMap (toRExpMap Gamma)) ->
validErrorbound (Var Q v) exprTypes A dVars = true ->
......@@ -195,7 +195,7 @@ Lemma validErrorboundCorrectVariable:
eval_Real E1 Gamma (Var Q v) nR ->
eval_Fin E2 Gamma DeltaMap (Var Q v) nF mF ->
approxEnv E1 (toRExpMap Gamma) A fVars dVars E2 ->
validTypes (Var Q v) (Gamma) DeltaMap ->
validTypes (Var Q v) (Gamma) ->
validRanges (Var Q v) A E1 (toRTMap (toRExpMap Gamma)) ->
validErrorbound (Var Q v) Gamma A dVars = true ->
NatSet.Subset (NatSet.diff (usedVars (Var Q v)) dVars) fVars ->
......@@ -238,7 +238,7 @@ Qed.
Lemma validErrorboundCorrectConstant_eval E2 m n Gamma DeltaMap:
(forall (e' : expr R) (m' : mType),
exists d : R, DeltaMap e' m' = Some d /\ (Rabs d <= mTypeToR m')%R) ->
validTypes (Const m n) Gamma DeltaMap ->
validTypes (Const m n) Gamma ->
exists nF m',
eval_Fin E2 Gamma DeltaMap (Const m n) nF m'.
Proof.
......@@ -253,7 +253,7 @@ Qed.
Lemma validErrorboundCorrectConstant E1 E2 A m n nR nF e nlo nhi dVars Gamma DeltaMap:
eval_Real E1 Gamma (Const m n) nR ->
eval_Fin E2 Gamma DeltaMap (Const m n) nF m ->
validTypes (Const m n) Gamma DeltaMap ->
validTypes (Const m n) Gamma ->
validErrorbound (Const m n) Gamma A dVars = true ->
(Q2R nlo <= nR <= Q2R nhi)%R ->
FloverMap.find (Const m n) A = Some ((nlo,nhi),e) ->
......@@ -1997,7 +1997,7 @@ Theorem validErrorbound_sound (e:expr Q):
forall E1 E2 fVars dVars A Gamma DeltaMap,
(forall (e' : expr R) (m' : mType),
exists d : R, DeltaMap e' m' = Some d /\ (Rabs d <= mTypeToR m')%R) ->
validTypes e Gamma DeltaMap ->
validTypes e Gamma ->
approxEnv E1 (toRExpMap Gamma) A fVars dVars E2 ->
NatSet.Subset (NatSet.diff (Expressions.usedVars e) dVars) fVars ->
validErrorbound e Gamma A dVars = true ->
......@@ -2020,7 +2020,7 @@ Proof.
split.
+ eapply validErrorboundCorrectConstant_eval; eauto.
+ intros * eval_float.
eapply validErrorboundCorrectConstant with (E2 := E2); eauto.
eapply validErrorboundCorrectConstant with (E2 := E2) (DeltaMap := DeltaMap); eauto.
inversion eval_float; subst; auto.
- rename IHe into IHe'.
assert (validErrorBounds e E1 E2 A Gamma DeltaMap) as IHe.
......@@ -2328,7 +2328,7 @@ Theorem validErrorboundCmd_gives_eval (f:cmd Q) :
NatSet.Subset (NatSet.diff (Commands.freeVars f) dVars) fVars ->
bstep (toREvalCmd (toRCmd f)) E1 (toRTMap (toRExpMap Gamma)) DeltaMapR vR REAL ->
validErrorboundCmd f Gamma A dVars = true ->
validTypesCmd f Gamma DeltaMap ->
validTypesCmd f Gamma ->
validRangesCmd f A E1 (toRTMap (toRExpMap Gamma)) ->
FloverMap.find (getRetExp f) A = Some ((elo,ehi),err) ->
(exists vF m,
......@@ -2424,7 +2424,7 @@ Theorem validErrorboundCmd_sound (f:cmd Q):
ssa f (NatSet.union fVars dVars) outVars ->
NatSet.Subset (NatSet.diff (Commands.freeVars f) dVars) fVars ->
validErrorboundCmd f Gamma A dVars = true ->
validTypesCmd f Gamma DeltaMap ->
validTypesCmd f Gamma ->
validRangesCmd f A E1 (toRTMap (toRExpMap Gamma)) ->
validErrorBoundsCmd f E1 E2 A Gamma DeltaMap.
Proof.
......
......@@ -144,7 +144,7 @@ Theorem validIntervalbounds_sound (f:expr Q) (A:analysisResult) (P:precond)
dVars_range_valid dVars E A ->
NatSet.Subset (NatSet.diff (Expressions.usedVars f) dVars) fVars ->
fVars_P_sound fVars E P ->
validTypes f Gamma DeltaMapR ->
validTypes f Gamma ->
validRanges f A E (toRTMap (toRExpMap Gamma)).
Proof.
induction f;
......@@ -396,7 +396,7 @@ Theorem validIntervalboundsCmd_sound (f:cmd Q) (A:analysisResult):
fVars_P_sound fVars E P ->
NatSet.Subset (NatSet.diff (Commands.freeVars f) dVars) fVars ->
validIntervalboundsCmd f A P dVars = true ->
validTypesCmd f Gamma DeltaMapR ->
validTypesCmd f Gamma ->
validRangesCmd f A E (toRTMap (toRExpMap Gamma)).
Proof.
induction f;
......
......@@ -25,7 +25,7 @@ Theorem RangeValidator_sound (e : expr Q) (A : analysisResult) (P : precond) dVa
RangeValidator e A P dVars = true ->
dVars_range_valid dVars E A ->
affine_dVars_range_valid dVars E A 1 (FloverMap.empty (affine_form Q)) (fun _: nat => None) ->
validTypes e Gamma DeltaMapR ->
validTypes e Gamma ->
fVars_P_sound (usedVars e) E P ->
validRanges e A E (toRTMap (toRExpMap Gamma)).
Proof.
......@@ -76,7 +76,7 @@ Theorem RangeValidatorCmd_sound (f : cmd Q) (A : analysisResult) (P : precond) d
affine_dVars_range_valid dVars E A 1 (FloverMap.empty (affine_form Q)) (fun _: nat => None) ->
fVars_P_sound fVars E P ->
NatSet.Subset (freeVars f -- dVars) fVars ->
validTypesCmd f Gamma DeltaMapR ->
validTypesCmd f Gamma ->
validRangesCmd f A E (toRTMap (toRExpMap Gamma)).
Proof.
intros ranges_valid; intros.
......
......@@ -22,45 +22,45 @@ From Flover
assignment
**)
Fixpoint validTypes e (Gamma:FloverMap.t mType) DeltaMap :Prop :=
Fixpoint validTypes e (Gamma:FloverMap.t mType): Prop :=
exists mG,
FloverMap.find e Gamma = Some mG /\
match e with
| Var _ x => True
| Const m v => m = mG
| Unop u e1 =>
validTypes e1 Gamma DeltaMap /\
validTypes e1 Gamma /\
exists me, FloverMap.find e1 Gamma = Some me /\ isCompat me mG = true
| Binop b e1 e2 =>
validTypes e1 Gamma DeltaMap /\
validTypes e2 Gamma DeltaMap /\
validTypes e1 Gamma /\
validTypes e2 Gamma /\
exists m1 m2, FloverMap.find e1 Gamma = Some m1 /\
FloverMap.find e2 Gamma = Some m2 /\
isJoin m1 m2 mG = true
| Fma e1 e2 e3 =>
validTypes e1 Gamma DeltaMap /\
validTypes e2 Gamma DeltaMap /\
validTypes e3 Gamma DeltaMap /\
validTypes e1 Gamma /\
validTypes e2 Gamma /\
validTypes e3 Gamma /\
exists m1 m2 m3,
FloverMap.find e1 Gamma = Some m1 /\ FloverMap.find e2 Gamma = Some m2 /\
FloverMap.find e3 Gamma = Some m3 /\
isJoin3 m1 m2 m3 mG = true
| Downcast m e1 =>
validTypes e1 Gamma DeltaMap /\ m = mG /\
validTypes e1 Gamma /\ m = mG /\
exists m1,
(FloverMap.find e1 Gamma = Some m1 /\ isMorePrecise m1 mG = true)
end /\
(forall E Gamma2 v m,
(forall E Gamma2 DeltaMap v m,
(forall e m, FloverMap.find e Gamma = Some m ->
FloverMap.find e Gamma2 = Some m) ->
eval_expr E (toRExpMap Gamma2) DeltaMap (toRExp e) v m ->
m = mG).
Corollary validTypes_single e Gamma DeltaMap:
validTypes e Gamma DeltaMap ->
Corollary validTypes_single e Gamma:
validTypes e Gamma ->
exists mG,
FloverMap.find e Gamma = Some mG /\
forall E v m Gamma2,
forall E v m Gamma2 DeltaMap,
(forall e m, FloverMap.find e Gamma = Some m -> FloverMap.find e Gamma2 = Some m) ->
eval_expr E (toRExpMap Gamma2) DeltaMap (toRExp e) v m ->
m = mG.
......@@ -68,10 +68,10 @@ Proof.
destruct e; intros * [? [defined_m [check_t valid_top]]]; simpl in *; eauto.
Qed.
Corollary validTypes_exec e Gamma DeltaMap m:
validTypes e Gamma DeltaMap ->
Corollary validTypes_exec e Gamma m:
validTypes e Gamma ->
FloverMap.find e Gamma = Some m ->
forall E v mR,
forall E DeltaMap v mR,
eval_expr E (toRExpMap Gamma) DeltaMap (toRExp e) v mR ->
m = mR.
Proof.
......@@ -84,45 +84,45 @@ Qed.
Ltac validTypes_split :=
match goal with
| [ H: validTypes (Const ?m ?v) ?Gamma ?DeltaMap |- _] => idtac
| [ H: validTypes (Var ?t ?x) ?Gamma ?DeltaMap |- _] => idtac
| [ H: validTypes (Unop ?u ?e) ?Gamma ?DeltaMap |- _] =>
| [ H: validTypes (Const ?m ?v) ?Gamma |- _] => idtac
| [ H: validTypes (Var ?t ?x) ?Gamma |- _] => idtac
| [ H: validTypes (Unop ?u ?e) ?Gamma |- _] =>
let n := fresh "valid_arg" in
assert (validTypes e Gamma DeltaMap)
assert (validTypes e Gamma)
as n
by (destruct H as [? [? [[? ?] ?]]]; eauto)
| [ H: validTypes (Binop ?b ?e1 ?e2) ?Gamma ?DeltaMap |- _] =>
| [ H: validTypes (Binop ?b ?e1 ?e2) ?Gamma |- _] =>
let n1 := fresh "valid_arg" in
let n2 := fresh "valid_arg" in
assert (validTypes e1 Gamma DeltaMap)
assert (validTypes e1 Gamma)
as n1
by (destruct H as [? [? [[? [? ?]] ?]]]; auto);
assert (validTypes e2 Gamma DeltaMap)
assert (validTypes e2 Gamma)
as n2
by (destruct H as [? [? [[? [? ?]] ?]]]; auto)
| [ H: validTypes (Fma ?e1 ?e2 ?e3) ?Gamma ?DeltaMap |- _] =>
| [ H: validTypes (Fma ?e1 ?e2 ?e3) ?Gamma |- _] =>
let n1 := fresh "valid_arg" in
let n2 := fresh "valid_arg" in
let n3 := fresh "valid_arg" in
assert (validTypes e1 Gamma DeltaMap)
assert (validTypes e1 Gamma)
as n1
by (destruct H as [? [? [[? [? [? ?]]] ?]]]; auto);
assert (validTypes e2 Gamma DeltaMap)
assert (validTypes e2 Gamma)
as n2
by (destruct H as [? [? [[? [? [? ?]]] ?]]]; auto);
assert (validTypes e3 Gamma DeltaMap)
assert (validTypes e3 Gamma)
as n3
by (destruct H as [? [? [[? [? [? ?]]] ?]]]; auto)
| [ H: validTypes (Downcast ?m ?e) ?Gamma ?DeltaMap |- _] =>
| [ H: validTypes (Downcast ?m ?e) ?Gamma |- _] =>
let n := fresh "valid_arg" in
assert (validTypes e Gamma DeltaMap)
assert (validTypes e Gamma)
as n
by (destruct H as [? [? [[? ?] ?]]]; eauto)
end.
Ltac validTypes_simp :=
match goal with
| [ H: validTypes ?e ?Gamma ?DeltaMap |- _ ] => validTypes_split; apply validTypes_single in H
| [ H: validTypes ?e ?Gamma |- _ ] => validTypes_split; apply validTypes_single in H
| _ => fail "No typing assumption found"
end.
......@@ -374,10 +374,10 @@ Proof.
Qed.
Lemma validTypes_mono e:
forall map1 map2 DeltaMap,
forall map1 map2,
(forall e m, FloverMap.find e map1 = Some m -> FloverMap.find e map2 = Some m) ->
validTypes e map1 DeltaMap ->
validTypes e map2 DeltaMap.
validTypes e map1 ->
validTypes e map2.
Proof.
induction e; intros * maps_mono valid_m1; simpl in *;
destruct valid_m1 as [t_m1 [find_map1 [check_top valid_rec]]];
......@@ -404,12 +404,12 @@ Proof.
Qed.
Lemma validTypes_eq_compat e1:
forall e2 Gamma DeltaMap,
forall e2 Gamma,
Q_orderedExps.compare e1 e2 = Eq ->
validTypes e1 Gamma DeltaMap ->
validTypes e2 Gamma DeltaMap.
validTypes e1 Gamma ->
validTypes e2 Gamma.
Proof.
induction e1; intros e2 Gamma DeltaMap eq_exp valid_e1;
induction e1; intros e2 Gamma eq_exp valid_e1;
cbn in valid_e1;
pose proof eq_exp as eq_clone; destruct e2; cbn in eq_exp; try congruence.
- destruct valid_e1 as [mG [find_mG [_ valid_exec]]].
......@@ -440,7 +440,7 @@ Proof.
apply N.compare_eq in Heqc0; subst; congruence.
- destruct (unopEq u u0) eqn:?; [ | destruct (unopEq u Neg) eqn:?; congruence ].
destruct valid_e1 as [mG [find_mG [[valid_e1 [? ?]] valid_exec]]].
specialize (IHe1 _ _ _ eq_exp valid_e1).
specialize (IHe1 _ _ eq_exp valid_e1).
rewrite unopEq_compat_eq in Heqb; subst.
erewrite FloverMapFacts.P.F.find_o with (y:=Unop u0 e2) in find_mG; eauto.
exists mG; repeat split; try auto.
......@@ -461,8 +461,8 @@ Proof.
as eq_rec2
by (destruct b0; try congruence; auto).
clear eq_exp.
specialize (IHe1_1 _ _ _ eq_rec1 valid_esub1).
specialize (IHe1_2 _ _ _ eq_rec2 valid_esub2).
specialize (IHe1_1 _ _ eq_rec1 valid_esub1).
specialize (IHe1_2 _ _ eq_rec2 valid_esub2).
erewrite FloverMapFacts.P.F.find_o in find_mG; try eauto.
destruct join_valid as [? [? [find_e11 [find_e12 join_valid]]]].
erewrite FloverMapFacts.P.F.find_o in find_e11,find_e12; eauto.
......@@ -485,9 +485,9 @@ Proof.
clear eq_exp.
destruct valid_e1 as
[mG [find_mG [[valid_e1 [valid_e2 [valid_e3 validJoin]]] valid_exec]]].
specialize (IHe1_1 _ _ _ eq_rec1 valid_e1).
specialize (IHe1_2 _ _ _ eq_rec2 valid_e2).
specialize (IHe1_3 _ _ _ eq_rec3 valid_e3).
specialize (IHe1_1 _ _ eq_rec1 valid_e1).
specialize (IHe1_2 _ _ eq_rec2 valid_e2).
specialize (IHe1_3 _ _ eq_rec3 valid_e3).
erewrite FloverMapFacts.P.F.find_o in find_mG; try eauto.
destruct validJoin as [? [? [? [find1 [find2 [find3 validJoin]]]]]].
erewrite FloverMapFacts.P.F.find_o in find1,find2, find3; eauto.
......@@ -499,7 +499,7 @@ Proof.
- destruct (mTypeEq m m0) eqn:?; type_conv; subst.
+ destruct valid_e1 as [mG [find_mG [[valid_e1 [t_eq upper_bound]] valid_exec]]].
subst.
specialize (IHe1 _ _ _ eq_exp valid_e1).
specialize (IHe1 _ _ eq_exp valid_e1).
erewrite FloverMapFacts.P.F.find_o in find_mG; try eauto.
destruct upper_bound as [? [find_e1 upperBound]].
erewrite FloverMapFacts.P.F.find_o in find_e1; try eauto.
......@@ -532,16 +532,16 @@ Proof.
Qed.
Theorem getValidMap_correct e:
forall (Gamma akk:FloverMap.t mType) DeltaMap res,
forall (Gamma akk:FloverMap.t mType) res,
(forall e,
FloverMap.mem e akk = true ->
validTypes e akk DeltaMap) ->
validTypes e akk) ->
getValidMap Gamma e akk = Succes res ->
forall e, FloverMap.mem e res = true ->
validTypes e res DeltaMap.
validTypes e res.
Proof.
pose (eT := e);
induction e ; intros Gamma akk DeltaMap res akk_sound validMap_succ;
induction e ; intros Gamma akk res akk_sound validMap_succ;
destruct (FloverMap.mem eT akk) eqn:Hmem; subst;
cbn in validMap_succ; subst eT;
rewrite Hmem in *; try (inversion validMap_succ; subst; eapply akk_sound; now eauto).
......@@ -576,7 +576,7 @@ Proof.
destruct (FloverMap.find (elt:=mType) e t) eqn:?; simpl in *;
try congruence.
intros * mem_add.
assert (forall e, FloverMap.mem e t = true -> validTypes e t DeltaMap) as valid_rec.
assert (forall e, FloverMap.mem e t = true -> validTypes e t) as valid_rec.
{ eapply IHe; eauto. }
destruct (isFixedPointB m) eqn:?.
+ Flover_compute.
......@@ -642,16 +642,16 @@ Proof.
destruct (getValidMap Gamma e2 t) eqn:?; cbn in *; try congruence.
destruct (FloverMap.find (elt:=mType) e1 t0) eqn:e1_find; try congruence.
destruct (FloverMap.find (elt:=mType) e2 t0) eqn:e2_find; try congruence.
assert (forall e, FloverMap.mem e t = true -> validTypes e t DeltaMap).
assert (forall e, FloverMap.mem e t = true -> validTypes e t).
{ eapply IHe1; eauto. }
assert (forall e, FloverMap.mem e t0 = true -> validTypes e t0 DeltaMap)
assert (forall e, FloverMap.mem e t0 = true -> validTypes e t0)
as valid_akk_sub.
{ eapply IHe2; eauto. }
assert (validTypes e1 t0 DeltaMap).
assert (validTypes e1 t0).
{ assert (FloverMap.mem e1 t0 = true)
by (rewrite FloverMapFacts.P.F.mem_find_b; rewrite e1_find; eauto).
eauto. }
assert (validTypes e2 t0 DeltaMap).
assert (validTypes e2 t0).
{ assert (FloverMap.mem e2 t0 = true)
by (rewrite FloverMapFacts.P.F.mem_find_b; rewrite e2_find; eauto).
eauto. }
......@@ -756,21 +756,21 @@ Proof.
destruct (FloverMap.find (elt:=mType) e1 t1) eqn:e1_find; try congruence.
destruct (FloverMap.find (elt:=mType) e2 t1) eqn:e2_find; try congruence.
destruct (FloverMap.find (elt:=mType) e3 t1) eqn:e3_find; try congruence.
assert (forall e, FloverMap.mem e t = true -> validTypes e t DeltaMap).
assert (forall e, FloverMap.mem e t = true -> validTypes e t).
{ eapply IHe1; eauto. }
assert (forall e, FloverMap.mem e t0 = true -> validTypes e t0 DeltaMap).
assert (forall e, FloverMap.mem e t0 = true -> validTypes e t0).
{ eapply IHe2; eauto. }
assert (forall e, FloverMap.mem e t1 = true -> validTypes e t1 DeltaMap).
assert (forall e, FloverMap.mem e t1 = true -> validTypes e t1).
{ eapply IHe3; eauto. }
assert (validTypes e1 t1 DeltaMap).
assert (validTypes e1 t1).
{ assert (FloverMap.mem e1 t1 = true)
by (rewrite FloverMapFacts.P.F.mem_find_b; rewrite e1_find; eauto).
eauto. }
assert (validTypes e2 t1 DeltaMap).
assert (validTypes e2 t1).
{ assert (FloverMap.mem e2 t1 = true)
by (rewrite FloverMapFacts.P.F.mem_find_b; rewrite e2_find; eauto).
eauto. }
assert (validTypes e3 t1 DeltaMap).
assert (validTypes e3 t1).
{ assert (FloverMap.mem e3 t1 = true)
by (rewrite FloverMapFacts.P.F.mem_find_b; rewrite e3_find; eauto).
eauto. }
......@@ -871,10 +871,10 @@ Proof.
by (eapply toRExpMap_some; eauto).
inversion eval_fma; subst; simpl in *; congruence.
- destruct (getValidMap Gamma e akk) eqn:?; cbn in validMap_succ; try congruence.
assert (forall e, FloverMap.mem e t = true -> validTypes e t DeltaMap).
assert (forall e, FloverMap.mem e t = true -> validTypes e t).
{ eapply IHe; eauto. }
destruct (FloverMap.find e t) eqn:e_find; try congruence.
assert (validTypes e t DeltaMap).
assert (validTypes e t).
{ assert (FloverMap.mem e t = true)
by (rewrite FloverMapFacts.P.F.mem_find_b; rewrite e_find; eauto).
eauto. }
......@@ -965,42 +965,42 @@ Proof.
auto.
Qed.
Corollary getValidMap_top_correct e DeltaMap:
Corollary getValidMap_top_correct e:
forall akk Gamma res,
(forall e, FloverMap.mem e akk = true ->
validTypes e akk DeltaMap) ->
validTypes e akk) ->
getValidMap Gamma e akk = Succes res ->
validTypes e res DeltaMap.
validTypes e res.
Proof.
intros * akk_sound validMap.
pose proof (getValidMap_correct _ _ _ _ akk_sound validMap) as all_sound.
pose proof (getValidMap_correct _ _ _ akk_sound validMap) as all_sound.
pose proof (getValidMap_top_contained _ _ _ validMap).
eauto.
Qed.
Fixpoint validTypesCmd f (Gamma:FloverMap.t mType) DeltaMap :Prop :=
Fixpoint validTypesCmd f (Gamma:FloverMap.t mType) :Prop :=
match f with
| Let m x e g =>
exists mG,
FloverMap.find e Gamma = Some mG /\
FloverMap.find (Var Q x) Gamma = Some m /\
mTypeEq m mG = true /\
validTypes e Gamma DeltaMap /\
validTypesCmd g Gamma DeltaMap
| Ret e => validTypes e Gamma DeltaMap
validTypes e Gamma /\
validTypesCmd g Gamma
| Ret e => validTypes e Gamma
end /\
exists mT,
FloverMap.find (getRetExp f) Gamma = Some mT /\
(forall E Gamma2 v m,
(forall E Gamma2 DeltaMap v m,
(forall e m, FloverMap.find e Gamma = Some m -> FloverMap.find e Gamma2 = Some m) ->
bstep (toRCmd f) E (toRExpMap Gamma2) DeltaMap v m ->
m = mT).
Corollary validTypesCmd_single f Gamma DeltaMap:
validTypesCmd f Gamma DeltaMap ->
Corollary validTypesCmd_single f Gamma:
validTypesCmd f Gamma ->
exists mT,
FloverMap.find (getRetExp f) Gamma = Some mT /\
(forall E Gamma2 v m,
(forall E Gamma2 DeltaMap v m,
(forall e m, FloverMap.find e Gamma = Some m -> FloverMap.find e Gamma2 = Some m) ->
bstep (toRCmd f) E (toRExpMap Gamma2) DeltaMap v m ->
m = mT).
......@@ -1051,14 +1051,14 @@ Proof.
- simpl in *. eapply getValidMap_mono; eauto.
Qed.
Theorem getValidMapCmd_correct f DeltaMap:
Theorem getValidMapCmd_correct f:
forall Gamma akk res,
(forall e, FloverMap.mem e akk = true ->
validTypes e akk DeltaMap) ->
validTypes e akk) ->
getValidMapCmd Gamma f akk = Succes res ->
validTypesCmd f res DeltaMap /\
validTypesCmd f res /\
(forall e, FloverMap.mem e res = true ->
validTypes e res DeltaMap).
validTypes e res).
Proof.
induction f; intros * akk_sound getMap_succeeds;
cbn in * |-.
......@@ -1066,7 +1066,7 @@ Proof.
try congruence.
destruct (FloverMap.find e t) eqn:?; try congruence.
destruct (mTypeEq m m0) eqn:?; try congruence.
pose proof (getValidMap_correct _ _ _ _ akk_sound Heqr) as t_sound.
pose proof (getValidMap_correct _ _ _ akk_sound Heqr) as t_sound.
unfold addMono in getMap_succeeds; Flover_compute.
assert (FloverMap.mem (Var Q n) t = false)
by (rewrite FloverMapFacts.P.F.mem_find_b; rewrite Heqo0; auto).
......@@ -1113,9 +1113,9 @@ Proof.
inversion bstep_let; subst.
eapply valid_exec; eauto.
- simpl.
pose proof (getValidMap_correct _ _ _ _ akk_sound getMap_succeeds)
pose proof (getValidMap_correct _ _ _ akk_sound getMap_succeeds)
as valid_exp_types.
pose proof (getValidMap_top_correct _ _ _ _ akk_sound getMap_succeeds) as valid_top.
pose proof (getValidMap_top_correct _ _ _ akk_sound getMap_succeeds) as valid_top.
repeat split; try auto.
eapply validTypes_single in valid_top.
destruct valid_top as [mT [find_mT valid_exec]].
......
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