Skip to content

GitLab

Commit ecccb575 authored by Nikita Zyuzin's avatar Nikita Zyuzin
Browse files

Fix some merge errors in Expressions

parent 7dd4f12f
Hide whitespace changes
Inline Side-by-side
Showing with 66 additions and 3 deletions
coq/Expressions.v
View file @ ecccb575
......@@ -219,6 +219,7 @@ Module ExpOrderedType (V_ordered:OrderType) <: OrderType.
if unopEq u1 u2
then expCompare e1 e2
else (if unopEq u1 Neg then Lt else Gt)
| Unop _ _, Fma _ _ _ => Lt
| Unop _ _, Binop _ _ _ => Lt
| Unop _ _, Downcast _ _ => Lt
| Unop _ _, _ => Gt
......@@ -226,6 +227,7 @@ Module ExpOrderedType (V_ordered:OrderType) <: OrderType.
if mTypeEq m1 m2
then expCompare e1 e2
else (if morePrecise m1 m2 then Lt else Gt)
| Downcast _ _, Fma _ _ _ => Lt
| Downcast _ _, Binop _ _ _ => Lt
| Downcast _ _, _ => Gt
| Binop b1 e11 e12, Binop b2 e21 e22 =>
......@@ -251,7 +253,19 @@ Module ExpOrderedType (V_ordered:OrderType) <: OrderType.
end
| _ => res
end
|_ , _ => Gt
| Binop _ _ _, Fma _ _ _ => Lt
| Binop _ _ _, _ => Gt
| Fma e11 e12 e13, Fma e21 e22 e23 =>
match expCompare e11 e21 with
| Eq => match expCompare e12 e22 with
| Eq => expCompare e13 e23
| Lt => Lt
| Gt => Gt
end
| Lt => Lt
| Gt => Gt
end
| Fma _ _ _ , _ => Gt
end.
Lemma expCompare_refl e: expCompare e e = Eq.
......@@ -261,6 +275,7 @@ Module ExpOrderedType (V_ordered:OrderType) <: OrderType.
- rewrite mTypeEq_refl. apply V_orderedFacts.compare_refl.
- rewrite unopEq_refl; auto.
- rewrite IHe1, IHe2. destruct b; auto.
- now rewrite IHe1, IHe2, IHe3.
- rewrite mTypeEq_refl; auto.
Qed.
......@@ -308,6 +323,11 @@ Module ExpOrderedType (V_ordered:OrderType) <: OrderType.
destruct (expCompare e1_1 e2_1) eqn:?;
destruct (expCompare e2_1 e3_1) eqn:?;
try congruence; try erewrite IHe1_1; eauto.
- destruct (expCompare e1_1 e2_1) eqn:?;
destruct (expCompare e2_1 e3_1) eqn:?;
destruct (expCompare e1_2 e2_2) eqn:?;
destruct (expCompare e2_2 e3_2) eqn:?;
try congruence; try erewrite IHe1_1, IHe1_2; eauto.
- destruct (mTypeEq m m0) eqn:?;
destruct (mTypeEq m0 m1) eqn:?;
type_conv;
......@@ -347,6 +367,13 @@ Module ExpOrderedType (V_ordered:OrderType) <: OrderType.
rewrite IHe1_1 in *; simpl in *;
rewrite CompOpp_iff in first_comp;
rewrite first_comp; simpl; try auto.
-
destruct (expCompare e1_1 e2_1) eqn:first_comp;
destruct (expCompare 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.
- rewrite mTypeEq_sym.
destruct (mTypeEq m0 m) eqn:?;
type_conv; try auto.
......@@ -390,6 +417,16 @@ Module ExpOrderedType (V_ordered:OrderType) <: OrderType.
try congruence;
try (erewrite IHe1_1; eauto; fail "");
try erewrite expCompare_eq_trans; eauto.
- destruct (expCompare e1_1 e2_1) eqn:?;
destruct (expCompare e2_1 e3_1) eqn:?;
try congruence;
try (erewrite IHe1_1; eauto; fail "");
try erewrite expCompare_eq_trans; eauto.
destruct (expCompare e1_2 e2_2) eqn:?;
destruct (expCompare e2_2 e3_2) eqn:?;
try congruence;
try (erewrite IHe1_2; eauto; fail "");
try erewrite expCompare_eq_trans; eauto.
- destruct (mTypeEq m m0) eqn:?;
destruct (mTypeEq m0 m1) eqn:?.
+ type_conv; subst. rewrite mTypeEq_refl. eapply IHe1; eauto.
......@@ -430,6 +467,16 @@ Module ExpOrderedType (V_ordered:OrderType) <: OrderType.
try congruence;
try (erewrite IHe1_1; eauto; fail "");
try erewrite expCompare_eq_trans; eauto.
- destruct (expCompare e1_1 e2_1) eqn:?;
destruct (expCompare e2_1 e3_1) eqn:?;
try congruence;
try (erewrite IHe1_1; eauto; fail "");
try erewrite expCompare_eq_trans; eauto.
destruct (expCompare e1_2 e2_2) eqn:?;
destruct (expCompare e2_2 e3_2) eqn:?;
try congruence;
try (erewrite IHe1_2; eauto; fail "");
try erewrite expCompare_eq_trans; eauto.
- destruct (mTypeEq m m0) eqn:?;
destruct (mTypeEq m0 m1) eqn:?.
+ type_conv; subst. rewrite mTypeEq_refl. eapply IHe1; eauto.
......@@ -462,6 +509,7 @@ Module ExpOrderedType (V_ordered:OrderType) <: OrderType.
apply IHx; auto.
+ destruct b;
destruct (expCompare x1 x1) eqn:?; try congruence.
+ destruct (expCompare x1 x1) eqn:?; destruct (expCompare x2 x2) eqn:?; try congruence.
+ rewrite mTypeEq_refl in lt_x.
apply IHx; auto.
- unfold Transitive.
......@@ -515,6 +563,19 @@ Module ExpOrderedType (V_ordered:OrderType) <: OrderType.
try (erewrite expCompare_eq_lt_is_lt; eauto; fail);
try (erewrite expCompare_lt_eq_is_lt; eauto; fail);
try (erewrite IHe1_1; eauto).
+ destruct (expCompare e1_1 y1) eqn:?; try congruence;
destruct (expCompare y1 z1) eqn:?; try congruence;
try (erewrite expCompare_eq_lt_is_lt; eauto; fail);
try (erewrite expCompare_lt_eq_is_lt; eauto; fail);
try (erewrite IHe1_1; eauto; fail).
apply (expCompare_eq_trans _ _ _ Heqc) in Heqc0;
rewrite Heqc0.
destruct (expCompare e1_2 y2) eqn:?; try congruence;
destruct (expCompare y2 z2) eqn:?; try congruence;
try (erewrite expCompare_eq_trans; eauto; fail);
try (erewrite expCompare_eq_lt_is_lt; eauto; fail);
try (erewrite expCompare_lt_eq_is_lt; eauto; fail);
try (erewrite IHe1_2; eauto).
+ destruct (mTypeEq m m0) eqn:?;
destruct (mTypeEq m0 m1) eqn:?;
[type_conv; subst; rewrite mTypeEq_refl | | | ].
......@@ -571,6 +632,7 @@ Module ExpOrderedType (V_ordered:OrderType) <: OrderType.
try (split; try congruence; intros);
try (specialize (IHe1_1 _ Heqc _ _ Heqc0); simpl in *; rewrite IHe1_1 in *; congruence);
try (specialize (IHe1_1 _ Heqc _ _ Heqc0); simpl in *; rewrite <- IHe1_1 in *; congruence).
- admit.
- destruct (mTypeEq m m0) eqn:?; destruct (mTypeEq m1 m2) eqn:?;
[type_conv | | |].
+ specialize (IHe1 _ e1_eq_e2 _ _ e3_eq_e4); simpl in *.
......@@ -579,7 +641,7 @@ Module ExpOrderedType (V_ordered:OrderType) <: OrderType.
+ destruct (morePrecise m1 m2); congruence.
+ destruct (morePrecise m m0); congruence.
+ destruct (morePrecise m m0); congruence.
Qed.
Admitted.
Instance lt_compat: Proper (eq ==> eq ==> iff) lt.
Proof.
......@@ -619,6 +681,7 @@ Module ExpOrderedType (V_ordered:OrderType) <: OrderType.
try (specialize (IHe1_1 _ Heqc _ _ Heqc0); simpl in *; rewrite <- IHe1_1 in *; congruence);
try (rewrite (eq_comp _ _ Heqc _ _ Heqc0) in *; congruence);
try (rewrite <- (eq_comp _ _ Heqc _ _ Heqc0) in *; congruence).
- admit.
- destruct (mTypeEq m m0) eqn:?; destruct (mTypeEq m1 m2) eqn:?;
[type_conv | | |].
+ specialize (IHe1 _ e1_eq_e2 _ _ e3_eq_e4); simpl in *.
......@@ -627,7 +690,7 @@ Module ExpOrderedType (V_ordered:OrderType) <: OrderType.
+ destruct (morePrecise m1 m2); congruence.
+ destruct (morePrecise m m0); congruence.
+ destruct (morePrecise m m0); congruence.
Defined.
Admitted.
Lemma compare_spec : forall x y, CompSpec eq lt x y (expCompare x y).
Proof.
......
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