Commit 2369fb36 authored by Joachim Bard's avatar Joachim Bard

removing conditionals

parent 5ef1892c
......@@ -90,6 +90,7 @@ Inductive eval_expr (E:env)
eval_expr E Gamma DeltaMap f1 v1 m1 ->
eval_expr (updEnv x v1 E) Gamma DeltaMap f2 v m2 ->
eval_expr E Gamma DeltaMap (Let m1 x f1 f2) v m
(*
| Cond_then m1 m2 m3 m f1 f2 f3 v1 v delta:
Gamma (Cond f1 f2 f3) = Some m ->
DeltaMap (Cond f1 f2 f3) m = Some delta ->
......@@ -107,6 +108,7 @@ Inductive eval_expr (E:env)
eval_expr E Gamma DeltaMap f1 0 m1 ->
eval_expr E Gamma DeltaMap f3 v m3 ->
eval_expr E Gamma DeltaMap (Cond f1 f2 f3) v m
*)
.
Definition DeltaMapR: expr R -> mType -> option R := (fun x m => Some 0).
......@@ -252,8 +254,10 @@ Proof.
destruct m; try congruence; auto.
- auto.
- cbn in H3. congruence.
(*
- cbn in H2. congruence.
- cbn in H2. congruence.
*)
Qed.
(**
......@@ -317,6 +321,7 @@ Proof.
destruct m4; try discriminate.
subst.
eapply IHf2; eauto.
(*
- inversion ev1; inversion ev2; subst.
+ assert (m2 = REAL) by (eapply toRTMap_eval_REAL; eauto).
assert (m4 = REAL) by (eapply toRTMap_eval_REAL; eauto).
......@@ -334,6 +339,7 @@ Proof.
assert (m5 = REAL) by (eapply toRTMap_eval_REAL; eauto).
subst.
eapply IHf3; eauto.
*)
Qed.
(**
......@@ -470,6 +476,7 @@ Proof.
apply beq_nat_true in Heqy. subst. now rewrite Heqx.
* intros ?. apply no_usedVar. set_tac.
right. apply beq_nat_false in Heqx. auto.
(*
- eapply Cond_then; eauto;
[ eapply IHe1 | eapply IHe2];
eauto;
......@@ -480,6 +487,7 @@ Proof.
eauto;
hnf; intros; eapply no_usedVar;
set_tac.
*)
Qed.
Lemma eval_expr_det_ignore_bind2 e:
......@@ -524,6 +532,7 @@ Proof.
apply beq_nat_true in Heqy. subst. now rewrite Heqx.
* intros ?. apply no_usedVar. set_tac.
right. apply beq_nat_false in Heqx. auto.
(*
- eapply Cond_then; eauto;
[ eapply IHe1 | eapply IHe2];
eauto;
......@@ -534,6 +543,7 @@ Proof.
eauto;
hnf; intros; eapply no_usedVar;
set_tac.
*)
Qed.
Lemma swap_Gamma_eval_expr e E vR m Gamma1 Gamma2 DeltaMap:
......@@ -552,8 +562,8 @@ Proof.
| eapply Fma_dist'
| eapply Downcast_dist'
| eapply Let_dist
| eapply Cond_then
| eapply Cond_else ]; try eauto;
(* | eapply Cond_then
| eapply Cond_else *) ]; try eauto;
rewrite <- Gamma_eq; auto.
Qed.
......@@ -598,11 +608,13 @@ Proof.
replace v0 with v3 in * by (eapply IHe1; eauto).
assert (m2 = m4) by (eapply Gamma_det; eauto); subst.
eapply IHe2; eauto.
(*
- inversion Heval1; inversion Heval2; subst.
+ eapply IHe2; erewrite Gamma_det; eauto.
+ exfalso. apply H6. eapply IHe1; eauto. erewrite Gamma_det; eauto.
+ exfalso. apply H17. eapply IHe1; eauto. erewrite Gamma_det; eauto.
+ eapply IHe3; erewrite Gamma_det; eauto.
*)
Qed.
Lemma real_eval_expr_ignores_delta_map (f:expr R) (E:env) Gamma:
......@@ -653,6 +665,7 @@ Proof.
- inversion ev1; subst.
destruct m2; try discriminate.
econstructor; eauto. rewrite Rabs_R0. cbn. lra.
(*
- inversion ev1; subst.
+ assert (m1 = REAL) by (eapply toRTMap_eval_REAL; eauto).
assert (m2 = REAL) by (eapply toRTMap_eval_REAL; eauto).
......@@ -664,4 +677,5 @@ Proof.
subst.
eapply Cond_else; eauto.
cbn. rewrite Rabs_R0. lra.
*)
Qed.
......@@ -114,8 +114,8 @@ Inductive expr (V:Type): Type :=
| Fma: expr V -> expr V -> expr V -> expr V
| Downcast: mType -> expr V -> expr V
(* TODO: do we need mType in let-exprs? *)
| Let: mType -> nat -> expr V -> expr V -> expr V
| Cond: expr V -> expr V -> expr V -> expr V.
| Let: mType -> nat -> expr V -> expr V -> expr V.
(* | Cond: expr V -> expr V -> expr V -> expr V.*)
Fixpoint toRExp (e:expr Q) :=
match e with
......@@ -126,7 +126,7 @@ Fixpoint toRExp (e:expr Q) :=
| Fma e1 e2 e3 => Fma (toRExp e1) (toRExp e2) (toRExp e3)
| Downcast m e1 => Downcast m (toRExp e1)
| Let m v e1 e2 => Let m v (toRExp e1) (toRExp e2)
| Cond e1 e2 e3 => Cond (toRExp e1) (toRExp e2) (toRExp e3)
(* | Cond e1 e2 e3 => Cond (toRExp e1) (toRExp e2) (toRExp e3)*)
end.
Fixpoint toREval (e:expr R) :=
......@@ -138,7 +138,7 @@ Fixpoint toREval (e:expr R) :=
| Fma e1 e2 e3 => Fma (toREval e1) (toREval e2) (toREval e3)
| Downcast _ e1 => Downcast REAL (toREval e1)
| Let _ v e1 e2 => Let REAL v (toREval e1) (toREval e2)
| Cond e1 e2 e3 => Cond (toREval e1) (toREval e2) (toREval e3)
(* | Cond e1 e2 e3 => Cond (toREval e1) (toREval e2) (toREval e3) *)
end.
Definition toRMap (d:expr R -> option mType) (e: expr R) :=
......@@ -176,7 +176,7 @@ Fixpoint freeVars (V:Type) (e:expr V) :NatSet.t :=
| Fma e1 e2 e3 => NatSet.union (freeVars e1) (NatSet.union (freeVars e2) (freeVars e3))
| Downcast _ e1 => freeVars e1
| Let _ x e1 e2 => freeVars e1 NatSet.remove x (freeVars e2)
| Cond e1 e2 e3 => freeVars e1 freeVars e2 freeVars e3
(* | Cond e1 e2 e3 => freeVars e1 freeVars e2 freeVars e3 *)
end.
Module Type OrderType := Coq.Structures.Orders.OrderedType.
......@@ -310,6 +310,7 @@ Module ExprOrderedType (V_ordered:OrderType) <: OrderType.
| Let _ _ _ _, Downcast _ _ => Gt
| Let _ _ _ _, Binop _ _ _ => Gt
| Let _ _ _ _, Fma _ _ _ => Gt
(*
| Let _ _ _ _, _ => Lt
| Cond e11 e12 e13, Cond e21 e22 e23 =>
match exprCompare e11 e21 with
......@@ -320,6 +321,7 @@ Module ExprOrderedType (V_ordered:OrderType) <: OrderType.
| r => r
end
| Cond _ _ _, _ => Gt
*)
end.
Lemma exprCompare_refl e: exprCompare e e = Eq.
......@@ -332,7 +334,7 @@ Module ExprOrderedType (V_ordered:OrderType) <: OrderType.
- now rewrite IHe1, IHe2, IHe3.
- rewrite mTypeEq_refl; auto.
- now rewrite mTypeEq_refl, Nat.compare_refl, IHe1, IHe2.
- now rewrite IHe1, IHe2, IHe3.
(* - now rewrite IHe1, IHe2, IHe3. *)
Qed.
Lemma exprCompare_eq_trans e1 :
......@@ -447,11 +449,13 @@ Module ExprOrderedType (V_ordered:OrderType) <: OrderType.
apply Ndec.Pcompare_Peqb in Heqc0;
apply N.compare_eq in Heqc1.
rewrite Pos.eqb_eq in *; subst; congruence.
(*
- destruct (exprCompare e1_1 e2_1) eqn:?;
destruct (exprCompare e2_1 e3_1) eqn:?;
destruct (exprCompare e1_2 e2_2) eqn:?;
destruct (exprCompare e2_2 e3_2) eqn:?;
try congruence; try erewrite IHe1_1, IHe1_2; eauto.
*)
Qed.
Lemma exprCompare_antisym e1:
......@@ -568,12 +572,14 @@ Module ExprOrderedType (V_ordered:OrderType) <: OrderType.
setoid_rewrite Pos.compare_antisym at 2.
destruct (w ?= w0) eqn:?;
destruct (f ?= f0)%N eqn:?; simpl; auto.
(*
- destruct (exprCompare e1_1 e2_1) eqn:first_comp;
destruct (exprCompare e1_2 e2_2) eqn:second_comp;
rewrite IHe1_1, IHe1_2 in *; simpl in *;
rewrite CompOpp_iff in first_comp;
rewrite CompOpp_iff in second_comp;
rewrite first_comp, second_comp; simpl; try auto.
*)
Qed.
Lemma exprCompare_eq_sym e1 e2:
......@@ -708,6 +714,7 @@ Module ExprOrderedType (V_ordered:OrderType) <: OrderType.
apply Ndec.Pcompare_Peqb in Heqc;
apply N.compare_eq in Heqc0;
rewrite Pos.eqb_eq in *; subst; congruence.
(*
- destruct (exprCompare e1_1 e2_1) eqn:?;
destruct (exprCompare e2_1 e3_1) eqn:?;
try congruence;
......@@ -718,6 +725,7 @@ Module ExprOrderedType (V_ordered:OrderType) <: OrderType.
try congruence;
try (erewrite IHe1_2; eauto; fail "");
try erewrite exprCompare_eq_trans; eauto.
*)
Qed.
Lemma exprCompare_eq_lt_is_lt e1:
......@@ -834,6 +842,7 @@ Module ExprOrderedType (V_ordered:OrderType) <: OrderType.
apply Ndec.Pcompare_Peqb in Heqc;
apply N.compare_eq in Heqc0;
rewrite Pos.eqb_eq in *; subst; congruence.
(*
- destruct (exprCompare e1_1 e2_1) eqn:?;
destruct (exprCompare e2_1 e3_1) eqn:?;
try congruence;
......@@ -844,6 +853,7 @@ Module ExprOrderedType (V_ordered:OrderType) <: OrderType.
try congruence;
try (erewrite IHe1_2; eauto; fail "");
try erewrite exprCompare_eq_trans; eauto.
*)
Qed.
Definition eq e1 e2 :=
......@@ -874,9 +884,11 @@ Module ExprOrderedType (V_ordered:OrderType) <: OrderType.
rewrite Nat.compare_refl in *.
destruct (exprCompare x1 x1) eqn:?;
destruct (exprCompare x2 x2) eqn:?; congruence.
(*
+ destruct (exprCompare x1 x1) eqn:?;
destruct (exprCompare x2 x2) eqn:?;
destruct (exprCompare x3 x3) eqn:?; congruence.
*)
- unfold Transitive.
intros e1. unfold lt.
induction e1; intros * lt_e1_e2 lt_e2_e3;
......@@ -1179,6 +1191,7 @@ Module ExprOrderedType (V_ordered:OrderType) <: OrderType.
eapply Pos.lt_trans; eauto);
rewrite G; auto. }
*)
(* case for Cond
+ destruct (exprCompare e1_1 y1) eqn:?; try congruence;
destruct (exprCompare y1 z1) eqn:?; try congruence;
try (erewrite exprCompare_eq_lt_is_lt; eauto; fail);
......@@ -1192,6 +1205,7 @@ Module ExprOrderedType (V_ordered:OrderType) <: OrderType.
try (erewrite exprCompare_eq_lt_is_lt; eauto; fail);
try (erewrite exprCompare_lt_eq_is_lt; eauto; fail);
try (erewrite IHe1_2; eauto).
*)
Qed.
Instance eq_compat: Proper (eq ==> eq ==> iff) eq.
......@@ -1328,6 +1342,7 @@ Module ExprOrderedType (V_ordered:OrderType) <: OrderType.
destruct (w ?= w0) eqn:c1; destruct (f ?= f0)%N eqn:c2; try congruence;
apply Ndec.Pcompare_Peqb in c1; apply N.compare_eq in c2;
rewrite Pos.eqb_eq in *; subst; congruence.
(*
- try (split; auto; fail);
destruct (exprCompare e1_1 e2_1) eqn:?;
destruct (exprCompare e3_1 e4_1) eqn:?;
......@@ -1354,6 +1369,7 @@ Module ExprOrderedType (V_ordered:OrderType) <: OrderType.
erewrite exprCompare_eq_trans; eauto;
rewrite exprCompare_antisym;
now (try rewrite e3_eq_e4; try rewrite e1_eq_e2).
*)
Qed.
Instance lt_compat: Proper (eq ==> eq ==> iff) lt.
......@@ -1522,6 +1538,7 @@ Module ExprOrderedType (V_ordered:OrderType) <: OrderType.
destruct (w ?= w0) eqn:c1; destruct (f ?= f0)%N eqn:c2; try congruence;
apply Ndec.Pcompare_Peqb in c1; apply N.compare_eq in c2;
rewrite Pos.eqb_eq in *; subst; congruence.
(*
- pose proof eq_compat as eq_comp. unfold Proper, eq in eq_comp.
destruct (exprCompare e1_1 e2_1) eqn:?;
destruct (exprCompare e3_1 e4_1) eqn:?;
......@@ -1554,6 +1571,7 @@ Module ExprOrderedType (V_ordered:OrderType) <: OrderType.
+ rewrite exprCompare_eq_sym in e3_eq_e4;
apply (exprCompare_lt_eq_is_lt _ _ _ H) in e3_eq_e4;
now apply (exprCompare_eq_lt_is_lt _ _ _ e1_eq_e2).
*)
Qed.
Lemma compare_spec : forall x y, CompSpec eq lt x y (exprCompare x y).
......
......@@ -107,11 +107,13 @@ Proof.
- rewrite e7; auto.
- rewrite e7; auto.
- rewrite e7; auto.
(*
- rewrite <- IHc, <- IHc0, e3, e4; auto.
- rewrite <- IHc, <- IHc0, e3, e4; auto.
- rewrite <- IHc, <- IHc0, e3, e4; auto.
- rewrite <- IHc, e3; auto.
- rewrite <- IHc, e3; auto.
*)
Qed.
(* Lemma QcompareExp_toREvalcompare e1 e2: *)
......@@ -190,6 +192,7 @@ Proof.
rewrite N.eqb_compare in e3.
rewrite Heq, e7 in e3.
discriminate.
(*
- specialize (IHc e3).
specialize (IHc0 e4).
specialize (IHc1 Heq).
......@@ -198,6 +201,7 @@ Proof.
apply NatSet.eq_leibniz in IHc1.
simpl.
now rewrite IHc, IHc0, IHc1.
*)
Qed.
Lemma freeVars_toREval_toRExp_compat e:
......@@ -207,7 +211,7 @@ Proof.
- now rewrite IHe1, IHe2.
- now rewrite IHe1, IHe2, IHe3.
- now rewrite IHe1, IHe2.
- now rewrite IHe1, IHe2, IHe3.
(* - now rewrite IHe1, IHe2, IHe3. *)
Qed.
Lemma freeVars_toRExp_compat e:
......@@ -217,7 +221,7 @@ Proof.
- now rewrite IHe1, IHe2.
- now rewrite IHe1, IHe2, IHe3.
- now rewrite IHe1, IHe2.
- now rewrite IHe1, IHe2, IHe3.
(* - now rewrite IHe1, IHe2, IHe3. *)
Qed.
Module FloverMap := FMapAVL.Make(legacy_OrderedQExps).
......@@ -470,7 +474,7 @@ Proof.
rewrite N.eqb_compare in e3.
rewrite H, e7 in e3.
discriminate.
- rewrite IHc, IHc0; auto.
(* - rewrite IHc, IHc0; auto. *)
Qed.
Lemma no_cycle_unop e:
......
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