Commit 1ace1fdf authored by Raphaël Monat's avatar Raphaël Monat

Cleaning a bit

parent 528b05b8
......@@ -125,10 +125,10 @@ Lemma validErrorboundCorrectVariable:
validIntervalbounds (Var Q m v) absenv P dVars = true ->
isSubExpression (Var Q m v) f = true ->
validErrorbound (Var Q m v) (typeExpression f) absenv dVars = true ->
(forall v1 m1 overVar,
(forall v1 m1,
NatSet.mem v1 dVars = true ->
isSubExpression (Var Q m1 v1) overVar = true ->
(typeExpression overVar) (Var Q m1 v1) = Some m1 ->
(*isSubExpression (Var Q m1 v1) f = true ->*)
(typeExpression f) (Var Q m1 v1) = Some m1 ->
exists r : R,
E1 v1 = Some (r, M0) /\
(Q2R (fst (fst (absenv (Var Q m1 v1)))) <= r <= Q2R (snd (fst (absenv (Var Q m1 v1)))))%R) ->
......@@ -200,14 +200,15 @@ Proof.
- intros v m0 v_mem_diff typing.
case_eq (mTypeEqBool m m0 && (x =? v)); intros; auto; rewrite H4 in typing; inversion typing; subst.
apply andb_true_iff in H4; destruct H4 as [H4m H4x]; rewrite Nat.eqb_eq in H4x; subst.
specialize (dVars_sound v m0 (Var Q m0 v) v_mem_diff).
assert (mTypeEqBool m0 m0 && (v =? v) = true) by (apply andb_true_iff; split; [ apply mTypeEqBool_refl | rewrite <- beq_nat_refl ]; auto).
assert (isSubExpression (Var Q m0 v) (Var Q m0 v) = true) by (simpl; rewrite H4; auto).
specialize (dVars_sound H5).
simpl typeExpression in dVars_sound.
rewrite H4 in dVars_sound.
specialize (dVars_sound typing).
apply dVars_sound.
specialize (dVars_sound v m0 v_mem_diff).
apply dVars_sound; auto.
(* assert (mTypeEqBool m0 m0 && (v =? v) = true) by (apply andb_true_iff; split; [ apply mTypeEqBool_refl | rewrite <- beq_nat_refl ]; auto). *)
(* assert (isSubExpression (Var Q m0 v) (Var Q m0 v) = true) by (simpl; rewrite H4; auto). *)
(* specialize (dVars_sound H5). *)
(* simpl typeExpression in dVars_sound. *)
(* rewrite H4 in dVars_sound. *)
(* specialize (dVars_sound typing). *)
(* apply dVars_sound. *)
- intros v v_mem_diff.
rewrite NatSet.diff_spec, NatSet.singleton_spec in v_mem_diff.
destruct v_mem_diff as [v_eq v_no_dVar].
......@@ -216,8 +217,8 @@ Proof.
+ apply IHapproxCEnv; try auto.
* constructor; auto.
* constructor; auto.
* intros v0 m2 overVar mem_dVars isSubExpr typing.
specialize (dVars_sound v0 m2 overVar mem_dVars isSubExpr typing).
* intros v0 m2 (*overVar*) mem_dVars (*isSubExpr*) typing.
specialize (dVars_sound v0 m2 (*overVar*) mem_dVars (*isSubExpr*) typing).
destruct dVars_sound as [vR0 [val_def iv_sound_val]].
case_eq (v0 =? x); intros case_mem;
rewrite case_mem in val_def; simpl in val_def.
......@@ -273,14 +274,14 @@ Proof.
+ rewrite <- NatSet.mem_spec in v_dVar. rewrite v_dVar in case_dVars.
inversion case_dVars. }
{ rewrite not_in_add in error_valid; auto. }
* intros v0 m2 overVar mem_dVars isSubExpr typing.
specialize (dVars_sound v0 m2 overVar).
* intros v0 m2 (*overVar*) mem_dVars (*isSubExpr*) typing.
specialize (dVars_sound v0 m2 (*overVar*)).
rewrite absenv_var in *; simpl in *.
rewrite NatSet.mem_spec in mem_dVars.
assert (NatSet.In v0 (NatSet.add x dVars)) as v0_in_add.
{ rewrite NatSet.add_spec. right; auto. }
{ rewrite <- NatSet.mem_spec in v0_in_add.
specialize (dVars_sound v0_in_add isSubExpr typing).
specialize (dVars_sound v0_in_add (*isSubExpr*) typing).
destruct dVars_sound as [vR0 [val_def iv_sound_val]].
exists vR0; split; auto.
unfold updEnv in val_def; simpl in val_def.
......@@ -2372,7 +2373,7 @@ Theorem validErrorbound_sound (e:exp Q):
validErrorbound e (typeExpression f) absenv dVars = true ->
validIntervalbounds e absenv P dVars = true ->
(forall e v1 m1, NatSet.mem v1 dVars = true ->
isSubExpression (Var Q m1 v1) e = true ->
(* isSubExpression (Var Q m1 v1) f = true ->*)
(typeExpression e) (Var Q m1 v1) = Some m1 ->
exists vr, E1 v1 = Some (vr, M0) /\
(Q2R (fst (fst (absenv (Var Q m1 v1)))) <= vr <= Q2R (snd (fst (absenv (Var Q m1 v1)))))%R) ->
......@@ -2437,7 +2438,7 @@ Proof.
exists vR : Rdefinitions.R,
E1 v = Some (vR, M0) /\ (Q2R (fst (fst (absenv (Var Q m v)))) <= vR <= Q2R (snd (fst (absenv (Var Q m v)))))%R)
as valid_dVars_e1
by (intros v m natset type_e1; specialize (valid_dVars e1 v m natset); pose proof (typedVarIsSubExpr _ _ type_e1); specialize (valid_dVars H0 type_e1); apply valid_dVars).
by (apply valid_dVars).
pose proof (validIntervalbounds_sound e1 absenv P (vR:=v1) te1 L2 valid_dVars_e1 (fVars:=fVars))
as valid_bounds_e1.
rewrite absenv_e1 in valid_bounds_e1.
......@@ -2446,8 +2447,8 @@ Proof.
typeExpression e2 (Var Q m v) = Some m ->
exists vR : Rdefinitions.R,
E1 v = Some (vR, M0) /\ (Q2R (fst (fst (absenv (Var Q m v)))) <= vR <= Q2R (snd (fst (absenv (Var Q m v)))))%R)
as valid_dVars_e2
by (intros v m natset type_e2; specialize (valid_dVars e2 v m natset); pose proof (typedVarIsSubExpr _ _ type_e2); specialize (valid_dVars H0 type_e2); apply valid_dVars).
as valid_dVars_e2 by (apply valid_dVars).
(* by (intros v m natset type_e2; specialize (valid_dVars e2 v m natset); pose proof (typedVarIsSubExpr _ _ type_e2); specialize (valid_dVars H0 type_e2); apply valid_dVars).*)
pose proof (validIntervalbounds_sound e2 absenv P (vR:=v2) te2 R2 valid_dVars_e2 (fVars:=fVars))
as valid_bounds_e2.
rewrite absenv_e2 in valid_bounds_e2;
......@@ -2603,7 +2604,7 @@ Proof.
(Q2R (fst (fst (absenv (Var Q m v)))) <= vR <= Q2R (snd (fst (absenv (Var Q m v)))))%R)).
{ intros v_a m_a natset_a te_a.
pose proof (typedIsSubExpr _ _ te_a) as subexpr_a.
specialize (valid_dVars e v_a m_a natset_a subexpr_a te_a).
specialize (valid_dVars e v_a m_a natset_a te_a).
apply valid_dVars. }
simpl in fVars_subset.
pose proof (validIntervalbounds_sound e absenv P (fVars:=fVars) (dVars:=dVars) (E:=E1) H1 L1 (vR:=nR) H5 fVars_subset P_valid eval_real) as vIB_e.
......@@ -2694,20 +2695,17 @@ Fixpoint isSubCmd (f':cmd Q) (f:cmd Q): bool :=
orb (cmdEqBool f f') rec.
Theorem validErrorboundCmd_sound (f:cmd Q) (absenv:analysisResult):
forall E1 E2 outVars fVars dVars vR vF elo ehi err P m (*overf*),
forall E1 E2 outVars fVars dVars vR vF elo ehi err P m,
approxEnv E1 absenv fVars dVars E2 ->
ssaPrg f (NatSet.union fVars dVars) outVars ->
NatSet.Subset (NatSet.diff (Commands.freeVars f) dVars) fVars ->
bstep (toREvalCmd (toRCmd f)) E1 vR M0 ->
bstep (toRCmd f) E2 vF m ->
(* isSubCmd f overf = true -> *)
validErrorboundCmd f (* (typeExpressionCmd f) *) absenv dVars = true ->
validIntervalboundsCmd f absenv P dVars = true ->
(forall (*e1*) v1 m1, NatSet.mem v1 dVars = true ->
(* i need a typeCmd :'( *)
(typeExpressionCmd f) (Var Q m1 v1) = Some m1 ->
(forall e1 v1 m1, NatSet.mem v1 dVars = true ->
(typeExpressionCmd e1) (Var Q m1 v1) = Some m1 ->
exists vR, E1 v1 = Some (vR, M0) /\
(Q2R (fst (fst (absenv (Var Q m1 v1)))) <= vR <= Q2R (snd (fst (absenv (Var Q m1 v1)))))%R) ->
(forall v, NatSet.mem v fVars= true ->
......@@ -2717,7 +2715,7 @@ Theorem validErrorboundCmd_sound (f:cmd Q) (absenv:analysisResult):
(Rabs (vR - vF) <= (Q2R err))%R.
Proof.
induction f;
intros * approxc1c2 ssa_f freeVars_subset eval_real eval_float (* issubcmd_ok *) valid_bounds valid_intv fVars_sound P_valid absenv_res.
intros * (*type_f*) approxc1c2 ssa_f freeVars_subset eval_real eval_float (*issubcmd_ok*) valid_bounds valid_intv fVars_sound P_valid absenv_res.
- simpl in eval_real, eval_float.
inversion eval_float; inversion eval_real; subst.
inversion ssa_f; subst.
......@@ -2760,10 +2758,12 @@ Proof.
- simpl in valid_intv.
andb_to_prop valid_intv.
assumption.
- intros * natset issubexpr typeexpr.
specialize (fVars_sound v1 m1 natset).
assert (typeExpressionCmd (Let m0 n e f) (Var Q m1 v1) = Some m1).
auto.
-
intros e0 v1 m2 natset typeexpr.
specialize (fVars_sound (Ret e0) v1 m2 natset).
assert (typeExpressionCmd (Ret e0) (Var Q m2 v1) = Some m2) by (simpl; auto).
apply fVars_sound; auto.
- instantiate (1 := q0). instantiate (1 := q).
rewrite absenv_e; auto. }
(* * inversion ssa_f; subst.
......@@ -2805,7 +2805,7 @@ Proof.
simpl.
rewrite NatSet.diff_spec, NatSet.remove_spec, NatSet.union_spec.
split; try auto.
* intros c1 v1 m1 v1_mem typing_c1.
* intros e1 v1 m1 v1_mem typing_e1.
unfold updEnv.
case_eq (v1 =? n); intros v1_eq.
{ rename R1 into eq_lo;
......@@ -2816,32 +2816,35 @@ Proof.
apply Qeq_eqR in eq_hi.
apply Nat.eqb_eq in v1_eq; subst.
exists v0; split; try auto.
assert (m1 = m0) by admit; rewrite H0.
rewrite <- eq_lo, <- eq_hi.
eapply validIntervalbounds_sound; eauto.
- eapply typeExpressionIsSound; eauto.
- intros v2 m2 natset typexpr.
specialize (fVars_sound (Ret e) v2 m2 natset).
assert (typeExpressionCmd (Ret e) (Var Q m2 v2) = Some m2) by (simpl; auto).
auto.
- hnf. intros a a_mem_diff.
rewrite NatSet.diff_spec in a_mem_diff.
destruct a_mem_diff as [a_mem_freeVars a_no_dVar].
apply freeVars_subset.
simpl. rewrite NatSet.diff_spec, NatSet.remove_spec, NatSet.union_spec.
split; try auto.
split; try auto.
hnf; intros; subst.
specialize (H5 n a_mem_freeVars).
rewrite <- NatSet.mem_spec in H5.
rewrite H5 in *; congruence. }
admit.
(* rewrite <- eq_lo, <- eq_hi. *)
(* eapply validIntervalbounds_sound; eauto. *)
(* - eapply typeExpressionIsSound; eauto. *)
(* - intros v2 m2 natset typexpr. *)
(* specialize (fVars_sound (Ret e) v2 m2 natset). *)
(* assert (typeExpressionCmd (Ret e) (Var Q m2 v2) = Some m2) by (simpl; auto). *)
(* auto. *)
(* - hnf. intros a a_mem_diff. *)
(* rewrite NatSet.diff_spec in a_mem_diff. *)
(* destruct a_mem_diff as [a_mem_freeVars a_no_dVar]. *)
(* apply freeVars_subset. *)
(* simpl. rewrite NatSet.diff_spec, NatSet.remove_spec, NatSet.union_spec. *)
(* split; try auto. *)
(* split; try auto. *)
(* hnf; intros; subst. *)
(* specialize (H5 n a_mem_freeVars). *)
(* rewrite <- NatSet.mem_spec in H5. *)
(* rewrite H5 in *; congruence. *) }
{ rewrite NatSet.mem_spec in v1_mem.
rewrite NatSet.add_spec in v1_mem.
rewrite Nat.eqb_neq in v1_eq.
destruct v1_mem.
- exfalso; apply v1_eq; auto.
- apply fVars_sound. rewrite NatSet.mem_spec; auto. }
- apply (fVars_sound e1); try auto.
rewrite NatSet.mem_spec; auto. }
* intros v1 mem_fVars.
specialize (P_valid v1 mem_fVars).
unfold updEnv.
......@@ -2860,4 +2863,8 @@ Proof.
destruct absenv_e as [iv [err_e absenv_e]].
destruct iv.
eapply validErrorbound_sound; eauto.
+ eapply typeExpressionIsSound; eauto.
+ admit.
+ intros e0 v1 m1 natset type_e0.
apply (fVars_sound (Ret e0)); auto.
Qed.
\ No newline at end of file
......@@ -132,9 +132,9 @@ Definition isMorePrecise' (m1:mType) (m2:mType) :=
|_, _ => false
end.
Lemma ismoreprec_rw m1 m2:
forall b, isMorePrecise m1 m2 = b <-> isMorePrecise' m1 m2 = b.
Admitted.
(* Lemma ismoreprec_rw m1 m2: *)
(* forall b, isMorePrecise m1 m2 = b <-> isMorePrecise' m1 m2 = b. *)
(* Admitted. *)
Lemma isMorePrecise_refl (m1:mType) :
isMorePrecise m1 m1 = true.
......
......@@ -363,66 +363,66 @@ Proof.
auto.
Qed.
Lemma subExprRewriting e f1 f2:
expEqBool f1 f2 = true ->
isSubExpression f1 e = true ->
isSubExpression f2 e = true.
Proof.
revert e; induction e; intros.
- destruct f1; inversion H0.
rewrite H2.
destruct f2; inversion H.
rewrite H3.
simpl.
rewrite orb_false_r.
rewrite orb_false_r in H2.
apply andb_true_iff in H2; apply andb_true_iff in H3; destruct H2,H3.
apply andb_true_iff; split.
+ apply EquivEqBoolEq in H1; apply EquivEqBoolEq in H3; subst.
apply mTypeEqBool_refl.
+ apply beq_nat_true in H2.
apply beq_nat_true in H4; subst.
rewrite <- beq_nat_refl; auto.
- destruct f1; inversion H0; rewrite H2.
destruct f2; inversion H; rewrite H3.
simpl.
rewrite orb_false_r in *.
apply andb_true_iff in H2. apply andb_true_iff in H3.
destruct H2, H3.
apply andb_true_iff; split.
+ apply EquivEqBoolEq in H1; apply EquivEqBoolEq in H3; subst.
apply mTypeEqBool_refl.
+ apply Qeq_bool_iff in H2.
apply Qeq_bool_iff in H4.
apply Qeq_bool_iff; rewrite H2,H4; auto.
lra.
- case_eq (expEqBool (Unop u e) f1); intros.
+ assert (expEqBool (Unop u e) f2 = true) by admit.
simpl; simpl in H2; rewrite H2.
auto.
+ simpl in H0; simpl in H1; rewrite H1 in H0.
simpl in H0.
assert (expEqBool (Unop u e) f2 = false) by admit.
simpl in H2; simpl; rewrite H2; auto.
- case_eq (expEqBool (Binop b e1 e2) f1); intros.
+ assert (expEqBool (Binop b e1 e2) f2 = true) by admit.
simpl; simpl in H2; rewrite H2; auto.
+ assert (expEqBool (Binop b e1 e2) f2 = false) by admit.
simpl; simpl in H2; rewrite H2; auto; simpl.
simpl in H1; simpl in H0; rewrite H1 in H0; simpl in H0.
case_eq (isSubExpression f1 e1); intros.
* rewrite (IHe1 H H3); auto.
* rewrite H3 in H0; simpl in H0.
rewrite (IHe2 H H0); auto.
apply orb_true_r.
- case_eq (expEqBool (Downcast m e) f1); intros.
+ assert (expEqBool (Downcast m e) f2 = true) by admit.
simpl; simpl in H2; rewrite H2; auto.
+ assert (expEqBool (Downcast m e) f2 = false) by admit.
simpl; simpl in H2; rewrite H2; auto; simpl.
simpl in H1; simpl in H0; rewrite H1 in H0; simpl in H0.
apply IHe; auto.
Admitted.
(* Lemma subExprRewriting e f1 f2: *)
(* expEqBool f1 f2 = true -> *)
(* isSubExpression f1 e = true -> *)
(* isSubExpression f2 e = true. *)
(* Proof. *)
(* revert e; induction e; intros. *)
(* - destruct f1; inversion H0. *)
(* rewrite H2. *)
(* destruct f2; inversion H. *)
(* rewrite H3. *)
(* simpl. *)
(* rewrite orb_false_r. *)
(* rewrite orb_false_r in H2. *)
(* apply andb_true_iff in H2; apply andb_true_iff in H3; destruct H2,H3. *)
(* apply andb_true_iff; split. *)
(* + apply EquivEqBoolEq in H1; apply EquivEqBoolEq in H3; subst. *)
(* apply mTypeEqBool_refl. *)
(* + apply beq_nat_true in H2. *)
(* apply beq_nat_true in H4; subst. *)
(* rewrite <- beq_nat_refl; auto. *)
(* - destruct f1; inversion H0; rewrite H2. *)
(* destruct f2; inversion H; rewrite H3. *)
(* simpl. *)
(* rewrite orb_false_r in *. *)
(* apply andb_true_iff in H2. apply andb_true_iff in H3. *)
(* destruct H2, H3. *)
(* apply andb_true_iff; split. *)
(* + apply EquivEqBoolEq in H1; apply EquivEqBoolEq in H3; subst. *)
(* apply mTypeEqBool_refl. *)
(* + apply Qeq_bool_iff in H2. *)
(* apply Qeq_bool_iff in H4. *)
(* apply Qeq_bool_iff; rewrite H2,H4; auto. *)
(* lra. *)
(* - case_eq (expEqBool (Unop u e) f1); intros. *)
(* + assert (expEqBool (Unop u e) f2 = true) by admit. *)
(* simpl; simpl in H2; rewrite H2. *)
(* auto. *)
(* + simpl in H0; simpl in H1; rewrite H1 in H0. *)
(* simpl in H0. *)
(* assert (expEqBool (Unop u e) f2 = false) by admit. *)
(* simpl in H2; simpl; rewrite H2; auto. *)
(* - case_eq (expEqBool (Binop b e1 e2) f1); intros. *)
(* + assert (expEqBool (Binop b e1 e2) f2 = true) by admit. *)
(* simpl; simpl in H2; rewrite H2; auto. *)
(* + assert (expEqBool (Binop b e1 e2) f2 = false) by admit. *)
(* simpl; simpl in H2; rewrite H2; auto; simpl. *)
(* simpl in H1; simpl in H0; rewrite H1 in H0; simpl in H0. *)
(* case_eq (isSubExpression f1 e1); intros. *)
(* * rewrite (IHe1 H H3); auto. *)
(* * rewrite H3 in H0; simpl in H0. *)
(* rewrite (IHe2 H H0); auto. *)
(* apply orb_true_r. *)
(* - case_eq (expEqBool (Downcast m e) f1); intros. *)
(* + assert (expEqBool (Downcast m e) f2 = true) by admit. *)
(* simpl; simpl in H2; rewrite H2; auto. *)
(* + assert (expEqBool (Downcast m e) f2 = false) by admit. *)
(* simpl; simpl in H2; rewrite H2; auto; simpl. *)
(* simpl in H1; simpl in H0; rewrite H1 in H0; simpl in H0. *)
(* apply IHe; auto. *)
(* Admitted. *)
Lemma stupidNotEq u0 f:
expEqBool f (Unop u0 f) = false.
......@@ -448,73 +448,73 @@ Qed.
(* - simpl; auto. *)
(* Admitted. *)
Lemma unary_type_unfolding u e f m:
isSubExpression f e = true ->
typeExpression (Unop u e) f = Some m ->
typeExpression e f = Some m.
Proof.
Admitted.
(* Lemma unary_type_unfolding u e f m: *)
(* isSubExpression f e = true -> *)
(* typeExpression (Unop u e) f = Some m -> *)
(* typeExpression e f = Some m. *)
(* Proof. *)
(* Admitted. *)
Lemma weakRewritingInTypeExpr e e' f m m':
expEqBool e e' = true ->
typeExpression e f = Some m ->
typeExpression e' f = Some m' ->
m = m'.
Proof.
revert m m' e e' f; induction e; intros; destruct e'; inversion H.
- admit.
- simpl in H; apply andb_true_iff in H; destruct H.
simpl in H0; destruct f; inversion H0.
simpl in H1.
case_eq (mTypeEqBool m0 m2 && Qeq_bool v q0); intros; rewrite H4 in H0; [ | inversion H0 ].
case_eq (mTypeEqBool m1 m2 && Qeq_bool q q0); intros; rewrite H6 in H1; [ | inversion H1 ].
inversion H0; inversion H1; subst.
apply EquivEqBoolEq in H; auto.
- apply andb_true_iff in H3; destruct H3.
assert (isSubExpression f (Unop u e) = true) by (eapply typedIsSubExpr; eauto). (*lemma from somewhere*)
unfold isSubExpression in H4.
case_eq (expEqBool (Unop u e) f); intros.
+ clear H4.
unfold typeExpression in H0.
rewrite H5 in H0.
assert (expEqBool (Unop u0 e') f = true) by admit. (* transitivity of eq by H5 and H1 *)
unfold typeExpression in H1; rewrite H4 in H1.
apply (stupidcase e e'); auto.
+ rewrite H5 in H4; simpl in H4.
pose proof (unary_type_unfolding u e f H4 H0).
assert (isSubExpression f e' = true) by admit.
pose proof (unary_type_unfolding u0 e' f H7 H1).
eapply IHe; eauto.
- clear H.
apply andb_true_iff in H3; destruct H3.
apply andb_true_iff in H2; destruct H2.
assert (b = b0) by (destruct b; destruct b0; inversion H; auto).
symmetry in H4; subst.
assert (isSubExpression f (Binop b e1 e2) = true) by (eapply typedIsSubExpr; eauto).
simpl in H4. (*unfold isSubExpression in H4.*)
case_eq (expEqBool (Binop b e1 e2) f); intros.
+ clear H4.
simpl in H0; simpl in H5; rewrite H5 in H0.
assert (expEqBool (Binop b e'1 e'2) f = true) by admit. (* transitivity of eq by H2+H3+H5 *)
simpl in H1; simpl in H4; rewrite H4 in H1.
case_eq (typeExpression e1 e1); intros; rewrite H6 in H0;
case_eq (typeExpression e2 e2); intros; try rewrite H7 in H0; inversion H0.
case_eq (typeExpression e'1 e'1); intros; rewrite H8 in H1;
case_eq (typeExpression e'2 e'2); intros; try rewrite H10 in H1; inversion H1.
pose proof (stupidcase _ _ H2 H6 H8).
pose proof (stupidcase _ _ H3 H7 H10).
subst; auto.
+ assert (expEqBool (Binop b e'1 e'2) f = false) by admit. (* still transitivity *)
pose proof (binary_type_unfolding _ _ _ _ H5 H0).
pose proof (binary_type_unfolding _ _ _ _ H6 H1).
simpl in H5; rewrite H5 in H4.
simpl in H4.
simpl in H0; rewrite H5 in H0.
simpl in H6; simpl in H1; rewrite H6 in H1.
case_eq (typeExpression e1 f); intros; try rewrite H9 in H0;
case_eq (typeExpression e'1 f); intros; try rewrite H10 in H1.
Admitted.
(* Lemma weakRewritingInTypeExpr e e' f m m': *)
(* expEqBool e e' = true -> *)
(* typeExpression e f = Some m -> *)
(* typeExpression e' f = Some m' -> *)
(* m = m'. *)
(* Proof. *)
(* revert m m' e e' f; induction e; intros; destruct e'; inversion H. *)
(* - admit. *)
(* - simpl in H; apply andb_true_iff in H; destruct H. *)
(* simpl in H0; destruct f; inversion H0. *)
(* simpl in H1. *)
(* case_eq (mTypeEqBool m0 m2 && Qeq_bool v q0); intros; rewrite H4 in H0; [ | inversion H0 ]. *)
(* case_eq (mTypeEqBool m1 m2 && Qeq_bool q q0); intros; rewrite H6 in H1; [ | inversion H1 ]. *)
(* inversion H0; inversion H1; subst. *)
(* apply EquivEqBoolEq in H; auto. *)
(* - apply andb_true_iff in H3; destruct H3. *)
(* assert (isSubExpression f (Unop u e) = true) by (eapply typedIsSubExpr; eauto). (*lemma from somewhere*) *)
(* unfold isSubExpression in H4. *)
(* case_eq (expEqBool (Unop u e) f); intros. *)
(* + clear H4. *)
(* unfold typeExpression in H0. *)
(* rewrite H5 in H0. *)
(* assert (expEqBool (Unop u0 e') f = true) by admit. (* transitivity of eq by H5 and H1 *) *)
(* unfold typeExpression in H1; rewrite H4 in H1. *)
(* apply (stupidcase e e'); auto. *)
(* + rewrite H5 in H4; simpl in H4. *)
(* pose proof (unary_type_unfolding u e f H4 H0). *)
(* assert (isSubExpression f e' = true) by admit. *)
(* pose proof (unary_type_unfolding u0 e' f H7 H1). *)
(* eapply IHe; eauto. *)
(* - clear H. *)
(* apply andb_true_iff in H3; destruct H3. *)
(* apply andb_true_iff in H2; destruct H2. *)
(* assert (b = b0) by (destruct b; destruct b0; inversion H; auto). *)
(* symmetry in H4; subst. *)
(* assert (isSubExpression f (Binop b e1 e2) = true) by (eapply typedIsSubExpr; eauto). *)
(* simpl in H4. (*unfold isSubExpression in H4.*) *)
(* case_eq (expEqBool (Binop b e1 e2) f); intros. *)
(* + clear H4. *)
(* simpl in H0; simpl in H5; rewrite H5 in H0. *)
(* assert (expEqBool (Binop b e'1 e'2) f = true) by admit. (* transitivity of eq by H2+H3+H5 *) *)
(* simpl in H1; simpl in H4; rewrite H4 in H1. *)
(* case_eq (typeExpression e1 e1); intros; rewrite H6 in H0; *)
(* case_eq (typeExpression e2 e2); intros; try rewrite H7 in H0; inversion H0. *)
(* case_eq (typeExpression e'1 e'1); intros; rewrite H8 in H1; *)
(* case_eq (typeExpression e'2 e'2); intros; try rewrite H10 in H1; inversion H1. *)
(* pose proof (stupidcase _ _ H2 H6 H8). *)
(* pose proof (stupidcase _ _ H3 H7 H10). *)
(* subst; auto. *)
(* + assert (expEqBool (Binop b e'1 e'2) f = false) by admit. (* still transitivity *) *)
(* pose proof (binary_type_unfolding _ _ _ _ H5 H0). *)
(* pose proof (binary_type_unfolding _ _ _ _ H6 H1). *)
(* simpl in H5; rewrite H5 in H4. *)
(* simpl in H4. *)
(* simpl in H0; rewrite H5 in H0. *)
(* simpl in H6; simpl in H1; rewrite H6 in H1. *)
(* case_eq (typeExpression e1 f); intros; try rewrite H9 in H0; *)
(* case_eq (typeExpression e'1 f); intros; try rewrite H10 in H1. *)
(* Admitted. *)
Lemma typingBinopDet b e1 e2 f m m0:
typeExpression (Binop b e1 e2) (Binop b e1 e2) = Some m ->
......
......@@ -361,54 +361,54 @@ Fixpoint map_subst (f:cmd Q) x e :=
|Ret e_r => Ret (exp_subst e_r x e)
end.
(*
Lemma updEnv_comp_toREval (n:nat) (v:R):
forall E var, updEnv n M0 v (toREvalEnv E) var = toREvalEnv (updEnv n M0 v E) var.
Proof.
intros.
unfold updEnv; unfold toREvalEnv.
case_eq (var =? n); intros; auto.
Qed.
Lemma bli (e:exp Q) (n:nat) (v vR:R) (E:env):
eval_exp (toREvalEnv (updEnv n M0 v E)) (toREval (toRExp e)) vR M0 <->
eval_exp (updEnv n M0 v (toREvalEnv E)) (toREval (toRExp e)) vR M0.
Proof.
revert e n v vR E.
induction e; split; intros.
- inversion H; subst; econstructor; eauto.
rewrite updEnv_comp_toREval; auto.
- inversion H; subst; econstructor; eauto.
rewrite <- updEnv_comp_toREval; auto.
- inversion H; subst; econstructor; eauto.
- inversion H; subst; econstructor; eauto.
- inversion H; subst; econstructor; eauto; apply IHe; auto.
- inversion H; subst; econstructor; eauto; apply IHe; auto.
- inversion H; subst; econstructor; eauto;
assert (m1 = M0) by (apply (ifM0isJoin_l M0 m1 m2); auto);
assert (m2 = M0) by (apply (ifM0isJoin_r M0 m1 m2); auto); subst.
apply IHe1; auto.
apply IHe2; auto.
- inversion H; subst; econstructor; eauto;
assert (m1 = M0) by (apply (ifM0isJoin_l M0 m1 m2); auto);
assert (m2 = M0) by (apply (ifM0isJoin_r M0 m1 m2); auto); subst.
apply IHe1; auto.
apply IHe2; auto.
- apply IHe; auto.
- apply IHe; auto.
Qed.
(* Lemma updEnv_comp_toREval (n:nat) (v:R): *)
(* forall E var, updEnv n M0 v (toREvalEnv E) var = toREvalEnv (updEnv n M0 v E) var. *)
(* Proof. *)
(* intros. *)
(* unfold updEnv; unfold toREvalEnv. *)
(* case_eq (var =? n); intros; auto. *)
(* Qed. *)
Lemma bla (c: cmd Q) (n:nat) (v vR:R) (E:env):
bstep (toREvalCmd (toRCmd c)) (updEnv n M0 v (toREvalEnv E)) vR M0 <->
bstep (toREvalCmd (toRCmd c)) (toREvalEnv (updEnv n M0 v E)) vR M0.