aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--plugins/romega/ReflOmegaCore.v32
1 files changed, 18 insertions, 14 deletions
diff --git a/plugins/romega/ReflOmegaCore.v b/plugins/romega/ReflOmegaCore.v
index 2a0705b3d..0476c385c 100644
--- a/plugins/romega/ReflOmegaCore.v
+++ b/plugins/romega/ReflOmegaCore.v
@@ -1170,7 +1170,7 @@ Fixpoint scalar_norm_add (t : term) (k1 k2 : int) : term :=
match t with
| (v1 * Tint x1 + l1)%term =>
(v1 * Tint (x1 * k1) + scalar_norm_add l1 k1 k2)%term
- | Tint x => Tint (x * k1 + k2)
+ | Tint x => Tint (k1 * x + k2)
| _ => (t * Tint k1 + Tint k2)%term (* shouldn't happen *)
end.
@@ -1178,7 +1178,7 @@ Theorem scalar_norm_add_stable e t k1 k2 :
interp_term e (t * Tint k1 + Tint k2)%term =
interp_term e (scalar_norm_add t k1 k2).
Proof.
- induction t; simpl; Simplify; simpl; auto.
+ induction t; simpl; Simplify; simpl; auto. f_equal. apply mult_comm.
rewrite <- IHt2. simpl. apply OMEGA11.
Qed.
@@ -1224,16 +1224,16 @@ Fixpoint fusion (t1 t2 : term) (k1 k2 : int) : term :=
| ([v2] * Tint x2 + l2)%term =>
match N.compare v1 v2 with
| Eq =>
- let k := x1 * k1 + x2 * k2 in
+ let k := k1 * x1 + k2 * x2 in
if beq k 0 then fusion l1 l2 k1 k2
else ([v1] * Tint k + fusion l1 l2 k1 k2)%term
- | Lt => ([v2] * Tint (x2 * k2) + fusion_t1 l2)%term
- | Gt => ([v1] * Tint (x1 * k1) + fusion l1 t2 k1 k2)%term
+ | Lt => ([v2] * Tint (k2 * x2) + fusion_t1 l2)%term
+ | Gt => ([v1] * Tint (k1 * x1) + fusion l1 t2 k1 k2)%term
end
- | Tint x2 => ([v1] * Tint (x1 * k1) + fusion l1 t2 k1 k2)%term
+ | Tint x2 => ([v1] * Tint (k1 * x1) + fusion l1 t2 k1 k2)%term
| _ => (t1 * Tint k1 + t2 * Tint k2)%term (* shouldn't happen *)
end) t2
- | Tint x1 => scalar_norm_add t2 k2 (x1 * k1)
+ | Tint x1 => scalar_norm_add t2 k2 (k1 * x1)
| _ => (t1 * Tint k1 + t2 * Tint k2)%term (* shouldn't happen *)
end.
@@ -1242,14 +1242,18 @@ Theorem fusion_stable e t1 t2 k1 k2 :
interp_term e (fusion t1 t2 k1 k2).
Proof.
revert t2; induction t1; simpl; Simplify; simpl; auto.
- - intros; rewrite <- scalar_norm_add_stable. simpl. apply plus_comm.
+ - intros; rewrite <- scalar_norm_add_stable. simpl.
+ rewrite plus_comm. f_equal. apply mult_comm.
- intros. Simplify. induction t2; simpl; Simplify; simpl; auto.
- + rewrite <- IHt1_2. simpl. apply OMEGA11.
- + rewrite <- IHt1_2. simpl. subst n0. rewrite OMEGA10, H0.
- now rewrite mult_comm, mult_0_l, plus_0_l.
- + rewrite <- IHt1_2. simpl. subst n0. apply OMEGA10.
- + rewrite <- IHt2_2. simpl. apply OMEGA12.
- + rewrite <- IHt1_2. simpl. apply OMEGA11.
+ + rewrite <- IHt1_2. simpl. rewrite (mult_comm k1); apply OMEGA11.
+ + rewrite <- IHt1_2. simpl. subst n0.
+ rewrite (mult_comm k1), (mult_comm k2) in H0.
+ rewrite OMEGA10, H0.
+ now rewrite mult_0_r, plus_0_l.
+ + rewrite <- IHt1_2. simpl. subst n0.
+ rewrite (mult_comm k1), (mult_comm k2); apply OMEGA10.
+ + rewrite <- IHt2_2. simpl. rewrite (mult_comm k2); apply OMEGA12.
+ + rewrite <- IHt1_2. simpl. rewrite (mult_comm k1); apply OMEGA11.
Qed.
(** Term normalization.