Commit d2e8cff4 authored by ='s avatar =

Filling the gaps in some simple typing proofs

parent e2419de3
......@@ -33,7 +33,7 @@ Fixpoint typeMap (e:exp Q) (e': exp Q) : option mType :=
| None => typeMap e2 e'
| x => x
end
| Downcast m e1 => if expEqBool e e' then Some m else typeMap e1 e'
| Downcast m e1 => if expEqBool e e' then typeExpression (Downcast m e1) else typeMap e1 e'
end.
Lemma typeMapVarDet e m m' v:
......@@ -57,24 +57,23 @@ Proof.
- simpl in H. apply IHe; auto.
Qed.
Lemma typedVarIsUsed f1 m1 v:
typeMap f1 (Var Q m1 v) = Some m1 ->
NatSet.In v (usedVars f1).
Admitted.
Lemma typeGivesTypeMap e m :
typeExpression e = Some m ->
typeMap e e = Some m.
Proof.
intros; induction e; simpl in *; auto.
- admit.
- admit.
- admit.
- rewrite mTypeEqBool_refl, <- beq_nat_refl; simpl; auto.
- rewrite mTypeEqBool_refl.
assert (Qeq_bool v v = true) by (apply Qeq_bool_iff; lra).
rewrite H0; simpl; auto.
- assert (unopEqBool u u = true) by (destruct u; auto).
rewrite H0, expEqBool_refl; simpl; auto.
- pose proof (expEqBool_refl (Binop b e1 e2)).
simpl in H0; rewrite H0.
auto.
- admit.
Admitted.
- rewrite mTypeEqBool_refl,expEqBool_refl.
simpl; auto.
Qed.
Lemma typeMap_gives_type:
forall e m,
......@@ -84,12 +83,25 @@ Proof.
intros e; induction e; intros; simpl in *; try auto.
- rewrite mTypeEqBool_refl in H.
rewrite <- beq_nat_refl in H. simpl in *. auto.
- admit.
- admit.
- admit.
- admit.
Admitted.
- assert (Qeq_bool v v = true) as Qeq_bool_refl by (apply Qeq_bool_iff; lra).
rewrite Qeq_bool_refl,mTypeEqBool_refl in H.
simpl in H; auto.
- assert (unopEqBool u u = true) as unopEqBool_refl by (destruct u; auto).
rewrite unopEqBool_refl,expEqBool_refl in H; simpl in H; auto.
- assert (binopEqBool b b = true) as binopEqBool_refl by (destruct b; auto).
rewrite binopEqBool_refl,expEqBool_refl,expEqBool_refl in H; simpl in H; auto.
- rewrite mTypeEqBool_refl,expEqBool_refl in H; simpl in H; auto.
Qed.
Lemma unop_neq u e:
expEqBool (Unop u e) e = true -> False .
Proof.
induction e; intros; simpl in *; try congruence.
case_eq ( unopEqBool u u0); intros; rewrite H0 in *; simpl in *; try congruence.
apply IHe.
assert (u = u0) by (destruct u; destruct u0; cbv in H0; inversion H0; auto).
subst. auto.
Qed.
Lemma t e u m:
typeMap e e = Some m ->
......@@ -98,10 +110,10 @@ Proof.
intros.
simpl. destruct e; try auto.
case_eq (expEqBool (Unop u0 e) e); intros case_exp.
- exfalso; admit.
- exfalso. eapply unop_neq; eauto.
- rewrite andb_false_r.
assumption.
Admitted.
Qed.
Inductive validType (Gamma:exp Q -> option mType) : exp Q -> mType -> Prop :=
|tVar m v:
......@@ -132,9 +144,17 @@ Proof.
- inversion H; constructor; auto.
- inversion H; constructor; auto.
- constructor; simpl; auto.
- admit.
- admit.
Admitted.
- case_eq (typeExpression e1); intros; rewrite H0 in H; [ | inversion H ].
case_eq (typeExpression e2); intros; rewrite H1 in H; inversion H; subst.
specialize (IHe1 _ H0). specialize (IHe2 _ H1).
econstructor; try eauto.
simpl; rewrite H0, H1; auto.
- case_eq (typeExpression e); intros; rewrite H0 in H; [| inversion H].
case_eq (isMorePrecise m1 m); intros; rewrite H1 in H; [| inversion H].
inversion H; subst.
econstructor; try eauto.
simpl; rewrite H0,H1; auto.
Qed.
......@@ -153,15 +173,6 @@ Definition GammaStronger (Gamma1 Gamma2:exp Q -> option mType):=
forall e m, Gamma1 e = Some m -> Gamma2 e = Some m.
Lemma unop_neq u e:
expEqBool (Unop u e) e = true -> False .
Proof.
induction e; intros; simpl in *; try congruence.
case_eq ( unopEqBool u u0); intros; rewrite H0 in *; simpl in *; try congruence.
apply IHe.
assert (u = u0) by (destruct u; destruct u0; cbv in H0; inversion H0; auto).
subst. auto.
Qed.
Lemma binop_neq_l b e1 e2:
expEqBool (Binop b e1 e2) e1 = false.
......
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