Commit 9ded8726 authored by Heiko Becker's avatar Heiko Becker

Shorter proofs

parent 92da81e9
This diff is collapsed.
......@@ -163,7 +163,8 @@ Definition vars_typed (S:NatSet.t) (Gamma: nat -> option mType) :=
Ltac kill_trivial_exists :=
match goal with
| [ |- exists iv err v, Some (?i,?e) = Some (iv, err) /\ _ /\ _] => exists i, e
| [ |- exists iv err v, Some (?i,?e) = Some (iv, err) /\ _ ] => exists i, e
| [ |- exists iv err, Some (?i,?e) = Some (iv, err) /\ _ ] => exists i, e
end.
Theorem validIntervalbounds_sound (f:exp Q) (A:analysisResult) (P:precond)
......
......@@ -114,41 +114,43 @@ Fixpoint typeMapCmd (Gamma:nat -> option mType) (f:cmd Q) tMap :=
|Ret e => typeMap Gamma e tMap
end.
Fixpoint typeCheck (e:exp Q) (Gamma:nat -> option mType) (tMap: exp Q -> option mType) : bool :=
Fixpoint typeCheck (e:exp Q) (Gamma:nat -> option mType)
(tMap: DaisyMap.t mType) : bool :=
match e with
| Var _ v => match tMap e, Gamma v with
| Var _ v => match DaisyMap.find e tMap, Gamma v with
| Some m, Some m' => mTypeEq m m'
| _, _ => false
end
| Const m n => match tMap e with
| Const m n => match DaisyMap.find e tMap with
| Some m' => mTypeEq m m'
| None => false
end
| Unop u e1 => match tMap e with
| Some m => match tMap e1 with
| Unop u e1 => match DaisyMap.find e tMap with
| Some m => match DaisyMap.find e1 tMap with
| Some m' => mTypeEq m m' && typeCheck e1 Gamma tMap
| None => false
end
| None => false
end
| Binop b e1 e2 => match tMap e, tMap e1, tMap e2 with
| Binop b e1 e2 => match DaisyMap.find e tMap, DaisyMap.find e1 tMap, DaisyMap.find e2 tMap with
| Some m, Some m1, Some m2 =>
mTypeEq m (join m1 m2)
&& typeCheck e1 Gamma tMap
&& typeCheck e2 Gamma tMap
| _, _, _ => false
end
| Downcast m e1 => match tMap e, tMap e1 with
| Downcast m e1 => match DaisyMap.find e tMap, DaisyMap.find e1 tMap with
| Some m', Some m1 => mTypeEq m m' && isMorePrecise m1 m && typeCheck e1 Gamma tMap
| _, _ => false
end
end.
Fixpoint typeCheckCmd (c:cmd Q) (Gamma:nat -> option mType) (tMap:exp Q -> option mType) : bool :=
Fixpoint typeCheckCmd (c:cmd Q) (Gamma:nat -> option mType)
(tMap:DaisyMap.t mType) : bool :=
match c with
| Let m x e g => if typeCheck e Gamma tMap
then
match tMap e, tMap (Var Q x) with
match DaisyMap.find e tMap, DaisyMap.find (Var Q x) tMap with
| Some me, Some mx => mTypeEq me m && mTypeEq m mx
&& typeCheckCmd g (updDefVars x me Gamma) tMap
| _, _ => false
......@@ -242,67 +244,25 @@ Theorem typingSoundnessExp Gamma E:
forall e v m expTypes,
typeCheck e Gamma expTypes = true ->
eval_exp E Gamma (toRExp e) v m ->
expTypes e = Some m.
DaisyMap.find e expTypes = Some m.
Proof.
induction e; intros * typechecks evals.
- simpl in typechecks.
inversion evals; subst.
rewrite H0 in typechecks.
case_eq (expTypes (Var Q n)); intros; rewrite H in typechecks; [ | inversion typechecks ].
apply mTypeEq_compat_eq in typechecks; subst; auto.
- simpl in typechecks.
inversion evals; subst.
case_eq (expTypes (Const m0 v)); intros; rewrite H in typechecks; [ | inversion typechecks ].
apply mTypeEq_compat_eq in typechecks; subst; auto.
- simpl in typechecks.
case_eq (expTypes (Unop u e)); intros; rewrite H in typechecks; [ | inversion typechecks ].
case_eq (expTypes e); intros; rewrite H0 in typechecks; [ | inversion typechecks ].
apply andb_true_iff in typechecks; destruct typechecks.
apply mTypeEq_compat_eq in H1; subst.
inversion evals; subst.
+ rewrite <- H0.
eapply IHe; eauto.
+ rewrite <- H0.
eapply IHe; eauto.
- inversion evals; subst.
simpl in typechecks.
case_eq (expTypes (Binop b e1 e2)); intros; rewrite H in typechecks; [ | inversion typechecks ].
case_eq (expTypes e1); intros; rewrite H0 in typechecks; [ | inversion typechecks ].
case_eq (expTypes e2); intros; rewrite H1 in typechecks; [ | inversion typechecks ].
andb_to_prop typechecks.
apply mTypeEq_compat_eq in L0; subst.
assert (expTypes e1 = Some m1) by (eapply IHe1; eauto).
assert (expTypes e2 = Some m2) by (eapply IHe2; eauto).
rewrite H0 in H4. rewrite H1 in H5.
inversion H4; inversion H5; subst; auto.
- simpl in typechecks.
case_eq (expTypes (Downcast m e)); intros; rewrite H in typechecks; [ | inversion typechecks ].
case_eq (expTypes e); intros; rewrite H0 in typechecks; [ | inversion typechecks ].
andb_to_prop typechecks.
apply mTypeEq_compat_eq in L0; subst.
inversion evals; subst.
auto.
induction e; cbn; intros * typechecks evals; Daisy_compute; type_conv;
inversion evals; subst; try auto.
- rewrite Heqo0 in *. inversion H0; auto.
- erewrite IHe in *; eauto.
- erewrite IHe in *; eauto.
- erewrite IHe1 in *; eauto.
erewrite IHe2 in *; eauto.
inversion Heqo0; subst; inversion Heqo1; subst; auto.
Qed.
Theorem typingSoundnessCmd c Gamma E v m expTypes:
typeCheckCmd c Gamma expTypes = true ->
bstep (toRCmd c) E Gamma v m ->
expTypes (getRetExp c) = Some m.
DaisyMap.find (getRetExp c) expTypes = Some m.
Proof.
revert Gamma E expTypes; induction c; intros * tc bc.
- simpl in tc.
inversion bc; subst.
andb_to_prop tc.
assert (expTypes e = Some m0)
as e_type_m0
by (eapply typingSoundnessExp; eauto).
specialize (IHc (updDefVars n m0 Gamma) (updEnv n v0 E)).
simpl.
rewrite e_type_m0 in R.
destruct (expTypes (Var Q n)) eqn:?; try congruence.
andb_to_prop R.
apply IHc; auto.
- simpl in *.
inversion bc; subst.
eapply typingSoundnessExp; eauto.
revert Gamma E expTypes; induction c; cbn; intros * tc bc;
Daisy_compute; try congruence; type_conv; subst; inversion bc; subst.
- eapply IHc; eauto.
- eapply typingSoundnessExp; eauto.
Qed.
\ No newline at end of file
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