aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins
diff options
context:
space:
mode:
authorGravatar Pierre Letouzey <pierre.letouzey@inria.fr>2017-05-18 15:47:50 +0200
committerGravatar Pierre Letouzey <pierre.letouzey@inria.fr>2017-05-22 15:26:59 +0200
commit2561930b8d163507f2a35e1ffddf90a6f14576de (patch)
treeb4d2425c4e11e7263c9dde52cf1ef6090640554a /plugins
parentd992ae9fc539bdadd9214d2c92d83bd08b68ef33 (diff)
ReflOmegaCore: misc cleanup, <? instead of bgt, etc
Diffstat (limited to 'plugins')
-rw-r--r--plugins/romega/ReflOmegaCore.v488
1 files changed, 205 insertions, 283 deletions
diff --git a/plugins/romega/ReflOmegaCore.v b/plugins/romega/ReflOmegaCore.v
index f08d62162..f95cfe364 100644
--- a/plugins/romega/ReflOmegaCore.v
+++ b/plugins/romega/ReflOmegaCore.v
@@ -167,12 +167,6 @@ Module IntProperties (I:Int).
Lemma plus_0_r : forall x, x+0 = x.
Proof. intros; rewrite plus_comm; apply plus_0_l. Qed.
- Lemma plus_0_r_reverse : forall x, x = x+0.
- Proof. intros; symmetry; apply plus_0_r. Qed.
-
- Lemma plus_assoc_reverse : forall x y z, x+y+z = x+(y+z).
- Proof. intros; symmetry; apply plus_assoc. Qed.
-
Lemma plus_permute : forall x y z, x+(y+z) = y+(x+z).
Proof. intros; do 2 rewrite plus_assoc; f_equal; apply plus_comm. Qed.
@@ -185,9 +179,6 @@ Module IntProperties (I:Int).
(** More facts about [mult] *)
- Lemma mult_assoc_reverse : forall x y z, x*y*z = x*(y*z).
- Proof. intros; symmetry; apply mult_assoc. Qed.
-
Lemma mult_plus_distr_l : forall x y z, x*(y+z)=x*y+x*z.
Proof.
intros.
@@ -258,21 +249,12 @@ Module IntProperties (I:Int).
now rewrite opp_def, <-mult_plus_distr_r, opp_def, mult_0_l.
Qed.
- Lemma egal_left : forall n m, n=m -> n+-m = 0.
- Proof. intros; subst; apply opp_def. Qed.
-
- Lemma egal_left_iff n m : n = m <-> 0 = n + - m.
- Proof.
- split. intros. symmetry. now apply egal_left.
- intros. apply plus_reg_l with (-m).
- rewrite plus_comm, <- H. symmetry. apply plus_opp_l.
- Qed.
-
- Lemma ne_left_2 : forall x y : int, x<>y -> 0<>(x + - y).
+ Lemma egal_left n m : 0 = n+-m <-> n = m.
Proof.
- intros; contradict H.
- apply (plus_reg_l (-y)).
- now rewrite plus_opp_l, plus_comm, H.
+ split; intros.
+ - apply plus_reg_l with (-m).
+ rewrite plus_comm, <- H. symmetry. apply plus_opp_l.
+ - symmetry. subst; apply opp_def.
Qed.
(** Specialized distributivities *)
@@ -280,32 +262,30 @@ Module IntProperties (I:Int).
Hint Rewrite mult_plus_distr_l mult_plus_distr_r mult_assoc : int.
Hint Rewrite <- plus_assoc : int.
- Lemma OMEGA10 :
- forall v c1 c2 l1 l2 k1 k2 : int,
- (v * c1 + l1) * k1 + (v * c2 + l2) * k2 =
- v * (c1 * k1 + c2 * k2) + (l1 * k1 + l2 * k2).
+ Hint Rewrite plus_0_l plus_0_r mult_0_l mult_0_r mult_1_l mult_1_r : int.
+
+ Lemma OMEGA10 v c1 c2 l1 l2 k1 k2 :
+ v * (c1 * k1 + c2 * k2) + (l1 * k1 + l2 * k2) =
+ (v * c1 + l1) * k1 + (v * c2 + l2) * k2.
Proof.
- intros; autorewrite with int; f_equal; now rewrite plus_permute.
+ autorewrite with int; f_equal; now rewrite plus_permute.
Qed.
- Lemma OMEGA11 :
- forall v1 c1 l1 l2 k1 : int,
- (v1 * c1 + l1) * k1 + l2 = v1 * (c1 * k1) + (l1 * k1 + l2).
+ Lemma OMEGA11 v1 c1 l1 l2 k1 :
+ v1 * (c1 * k1) + (l1 * k1 + l2) = (v1 * c1 + l1) * k1 + l2.
Proof.
- intros; now autorewrite with int.
+ now autorewrite with int.
Qed.
- Lemma OMEGA12 :
- forall v2 c2 l1 l2 k2 : int,
- l1 + (v2 * c2 + l2) * k2 = v2 * (c2 * k2) + (l1 + l2 * k2).
+ Lemma OMEGA12 v2 c2 l1 l2 k2 :
+ v2 * (c2 * k2) + (l1 + l2 * k2) = l1 + (v2 * c2 + l2) * k2.
Proof.
- intros; autorewrite with int; now rewrite plus_permute.
+ autorewrite with int; now rewrite plus_permute.
Qed.
- Lemma sum1 : forall a b c d : int, 0 = a -> 0 = b -> 0 = a * c + b * d.
+ Lemma sum1 a b c d : 0 = a -> 0 = b -> 0 = a * c + b * d.
Proof.
- intros; elim H; elim H0; simpl; auto.
- now rewrite mult_0_l, mult_0_l, plus_0_l.
+ intros; subst. now autorewrite with int.
Qed.
@@ -376,12 +356,14 @@ Module IntProperties (I:Int).
Definition beq i j := match compare i j with Eq => true | _ => false end.
- Lemma beq_iff i j : beq i j = true <-> i=j.
+ Infix "=?" := beq : Int_scope.
+
+ Lemma beq_iff i j : (i =? j) = true <-> i=j.
Proof.
unfold beq. rewrite <- (compare_Eq i j). now destruct compare.
Qed.
- Lemma beq_reflect i j : reflect (i=j) (beq i j).
+ Lemma beq_reflect i j : reflect (i=j) (i =? j).
Proof.
apply iff_reflect. symmetry. apply beq_iff.
Qed.
@@ -391,16 +373,18 @@ Module IntProperties (I:Int).
intros n m; generalize (beq_iff n m); destruct beq; [left|right]; intuition.
Qed.
- Definition bgt i j := match compare i j with Gt => true | _ => false end.
+ Definition blt i j := match compare i j with Lt => true | _ => false end.
+
+ Infix "<?" := blt : Int_scope.
- Lemma bgt_iff i j : bgt i j = true <-> i>j.
+ Lemma blt_iff i j : (i <? j) = true <-> i<j.
Proof.
- unfold bgt. rewrite <- (compare_Gt i j). now destruct compare.
+ unfold blt. rewrite <- (compare_Lt i j). now destruct compare.
Qed.
- Lemma bgt_reflect i j : reflect (i>j) (bgt i j).
+ Lemma blt_reflect i j : reflect (i<j) (i <? j).
Proof.
- apply iff_reflect. symmetry. apply bgt_iff.
+ apply iff_reflect. symmetry. apply blt_iff.
Qed.
Lemma le_is_lt_or_eq : forall n m, n<=m -> { n<m } + { n=m }.
@@ -432,20 +416,14 @@ Module IntProperties (I:Int).
(** Order and operations *)
- Lemma le_0_neg : forall n, 0 <= n <-> -n <= 0.
+ Lemma le_0_neg n : n <= 0 <-> 0 <= -n.
Proof.
- intros.
rewrite <- (mult_0_l (-(1))) at 2.
rewrite <- opp_eq_mult_neg_1.
split; intros.
- - apply opp_le_compat; auto.
+ - now apply opp_le_compat.
- rewrite <-(opp_involutive 0), <-(opp_involutive n).
- apply opp_le_compat; auto.
- Qed.
-
- Lemma le_0_neg' : forall n, n <= 0 <-> 0 <= -n.
- Proof.
- intros; rewrite le_0_neg, opp_involutive; intuition.
+ now apply opp_le_compat.
Qed.
Lemma plus_le_reg_r : forall n m p, n + p <= m + p -> n <= m.
@@ -487,20 +465,14 @@ Module IntProperties (I:Int).
apply opp_le_compat; auto.
Qed.
- Lemma lt_0_neg : forall n, 0 < n <-> -n < 0.
+ Lemma lt_0_neg n : n < 0 <-> 0 < -n.
Proof.
- intros.
rewrite <- (mult_0_l (-(1))) at 2.
rewrite <- opp_eq_mult_neg_1.
split; intros.
- - apply opp_lt_compat; auto.
+ - now apply opp_lt_compat.
- rewrite <-(opp_involutive 0), <-(opp_involutive n).
- apply opp_lt_compat; auto.
- Qed.
-
- Lemma lt_0_neg' : forall n, n < 0 <-> 0 < -n.
- Proof.
- intros; rewrite lt_0_neg, opp_involutive; intuition.
+ now apply opp_lt_compat.
Qed.
Lemma mult_lt_0_compat : forall n m, 0 < n -> 0 < m -> 0 < n*m.
@@ -517,7 +489,7 @@ Module IntProperties (I:Int).
- generalize (mult_lt_0_compat _ _ Hn Hm).
rewrite H.
exact (lt_irrefl 0).
- - rewrite lt_0_neg' in Hm.
+ - rewrite lt_0_neg in Hm.
generalize (mult_lt_0_compat _ _ Hn Hm).
rewrite <- opp_mult_distr_r, opp_eq_mult_neg_1, H, mult_0_l.
exact (lt_irrefl 0).
@@ -530,7 +502,7 @@ Module IntProperties (I:Int).
- right; apply (mult_integral_r n m); trivial.
- now left.
- right; apply (mult_integral_r (-n) m).
- + now apply lt_0_neg'.
+ + now apply lt_0_neg.
+ rewrite mult_comm, <- opp_mult_distr_r, mult_comm, H.
now rewrite opp_eq_mult_neg_1, mult_0_l.
Qed.
@@ -556,28 +528,10 @@ Module IntProperties (I:Int).
now apply le_trans with k.
Qed.
- Lemma sum5 :
- forall a b c d : int, c <> 0 -> 0 <> a -> 0 = b -> 0 <> a * c + b * d.
- Proof.
- intros.
- subst b; rewrite mult_0_l, plus_0_r.
- contradict H.
- symmetry in H; destruct (mult_integral _ _ H); congruence.
- Qed.
-
- Lemma one_neq_zero : 1 <> 0.
- Proof.
- red; intro.
- symmetry in H.
- apply (lt_not_eq 0 1); auto.
- apply lt_0_1.
- Qed.
-
- Lemma minus_one_neq_zero : -(1) <> 0.
+ Lemma sum5 a b c d : 0 <> c -> 0 <> a -> 0 = b -> 0 <> a * c + b * d.
Proof.
- apply lt_not_eq.
- rewrite <- lt_0_neg.
- apply lt_0_1.
+ intros Hc Ha <-. autorewrite with int. contradict Hc.
+ symmetry in Hc. destruct (mult_integral _ _ Hc); congruence.
Qed.
Lemma le_left n m : n <= m <-> 0 <= m + - n.
@@ -591,7 +545,7 @@ Module IntProperties (I:Int).
now rewrite plus_opp_r.
Qed.
- Lemma OMEGA8 : forall x y, 0 <= x -> 0 <= y -> x = - y -> x = 0.
+ Lemma OMEGA8 x y : 0 <= x -> 0 <= y -> x = - y -> x = 0.
Proof.
intros.
assert (y=-x).
@@ -605,17 +559,15 @@ Module IntProperties (I:Int).
elim (lt_not_eq _ _ H1); auto.
Qed.
- Lemma sum2 :
- forall a b c d : int, 0 <= d -> 0 = a -> 0 <= b -> 0 <= a * c + b * d.
+ Lemma sum2 a b c d :
+ 0 <= d -> 0 = a -> 0 <= b -> 0 <= a * c + b * d.
Proof.
- intros.
- subst a; rewrite mult_0_l, plus_0_l.
+ intros Hd <- Hb. autorewrite with int.
rewrite <- (mult_0_l 0).
apply mult_le_compat; auto; apply le_refl.
Qed.
- Lemma sum3 :
- forall a b c d : int,
+ Lemma sum3 a b c d :
0 <= c -> 0 <= d -> 0 <= a -> 0 <= b -> 0 <= a * c + b * d.
Proof.
intros.
@@ -627,56 +579,39 @@ Module IntProperties (I:Int).
apply mult_le_compat; auto; apply le_refl.
Qed.
- Lemma sum4 : forall k : int, k>0 -> 0 <= k.
- Proof.
- intros k; rewrite gt_lt_iff; apply lt_le_weak.
- Qed.
-
(** Lemmas specific to integers (they use [le_lt_int]) *)
- Lemma lt_left : forall n m, n < m -> 0 <= m + -(1) + - n.
+ Lemma lt_left n m : n < m <-> 0 <= m + -n + -(1).
Proof.
- intros. rewrite <- le_left.
- now rewrite <- le_lt_int.
+ rewrite <- plus_assoc, (plus_comm (-n)), plus_assoc.
+ rewrite <- le_left.
+ apply le_lt_int.
Qed.
- Lemma lt_left_inv : forall x y, 0 <= y + -(1) + - x -> x < y.
+ Lemma OMEGA4 x y z : 0 < x -> x < y -> z * y + x <> 0.
Proof.
- intros.
- generalize (plus_le_compat _ _ _ _ H (le_refl x)); clear H.
- now rewrite plus_0_l, <-plus_assoc, plus_opp_l, plus_0_r, le_lt_int.
- Qed.
-
- Lemma OMEGA4 : forall x y z, x > 0 -> y > x -> z * y + x <> 0.
- Proof.
- intros.
- intro H'.
- rewrite gt_lt_iff in H,H0.
+ intros H H0 H'.
+ assert (0 < y) by now apply lt_trans with x.
destruct (lt_eq_lt_dec z 0) as [[G|G]|G].
- - rewrite lt_0_neg' in G.
- generalize (plus_le_lt_compat _ _ _ _ (le_refl (z*y)) H0).
+ - generalize (plus_le_lt_compat _ _ _ _ (le_refl (z*y)) H0).
rewrite H'.
rewrite <-(mult_1_l y) at 2. rewrite <-mult_plus_distr_r.
- intros.
- rewrite le_lt_int in G.
- rewrite <- opp_plus_distr in G.
- assert (0 < y) by (apply lt_trans with x; auto).
- generalize (mult_le_compat _ _ _ _ G (lt_le_weak _ _ H2) (le_refl 0) (le_refl 0)).
- rewrite mult_0_l, mult_comm, <- opp_mult_distr_r, mult_comm, <-le_0_neg', le_lt_iff.
- intuition.
+ apply le_lt_iff.
+ rewrite mult_comm. rewrite <- (mult_0_r y).
+ apply mult_le_compat_l; auto using lt_le_weak.
+ apply le_0_neg. rewrite opp_plus_distr.
+ apply le_lt_int. now apply lt_0_neg.
- - subst; rewrite mult_0_l, plus_0_l in H'; subst.
- apply (lt_not_eq _ _ H); auto.
+ - apply (lt_not_eq 0 (z*y+x)); auto.
+ subst. now autorewrite with int.
- apply (lt_not_eq 0 (z*y+x)); auto.
rewrite <- (plus_0_l 0).
- apply plus_lt_compat; auto.
- apply mult_lt_0_compat; auto.
- apply lt_trans with x; auto.
+ auto using plus_lt_compat, mult_lt_0_compat.
Qed.
- Lemma OMEGA19 : forall x, x<>0 -> 0 <= x + -(1) \/ 0 <= x * -(1) + -(1).
+ Lemma OMEGA19 x : x<>0 -> 0 <= x + -(1) \/ 0 <= x * -(1) + -(1).
Proof.
intros.
do 2 rewrite <- le_lt_int.
@@ -689,23 +624,14 @@ Module IntProperties (I:Int).
apply opp_lt_compat; auto.
Qed.
- Lemma pos_ge_1 n : 0 < n -> 1 <= n.
- Proof.
- intros. apply plus_le_reg_r with (-(1)). rewrite opp_def.
- now apply le_lt_int.
- Qed.
-
Lemma mult_le_approx n m p :
- n > 0 -> n > p -> 0 <= m * n + p -> 0 <= m.
+ 0 < n -> p < n -> 0 <= m * n + p -> 0 <= m.
Proof.
- do 2 rewrite gt_lt_iff.
do 2 rewrite le_lt_iff; intros Hn Hpn H Hm. destruct H.
- apply lt_0_neg', pos_ge_1 in Hm.
- rewrite lt_0_neg'.
+ apply lt_0_neg, le_lt_int, le_left in Hm.
+ rewrite lt_0_neg.
rewrite opp_plus_distr, mult_comm, opp_mult_distr_r.
- rewrite le_lt_int.
- rewrite <- plus_assoc, (plus_comm (-p)), plus_assoc.
- apply lt_left.
+ rewrite le_lt_int. apply lt_left.
rewrite le_lt_int.
apply le_trans with (n+-(1)); [ now apply le_lt_int | ].
apply plus_le_compat; [ | apply le_refl ].
@@ -830,7 +756,7 @@ Definition absurd := FalseTerm :: nil.
Fixpoint eq_term (t1 t2 : term) {struct t2} : bool :=
match t1, t2 with
- | Tint i1, Tint i2 => beq i1 i2
+ | Tint i1, Tint i2 => i1 =? i2
| (t11 + t12), (t21 + t22) => eq_term t11 t21 && eq_term t12 t22
| (t11 * t12), (t21 * t22) => eq_term t11 t21 && eq_term t12 t22
| (t11 - t12), (t21 - t22) => eq_term t11 t21 && eq_term t12 t22
@@ -839,15 +765,17 @@ Fixpoint eq_term (t1 t2 : term) {struct t2} : bool :=
| _, _ => false
end%term.
+Infix "=?" := eq_term : romega_scope.
+
Theorem eq_term_iff (t t' : term) :
- eq_term t t' = true <-> t = t'.
+ (t =? t')%term = true <-> t = t'.
Proof.
revert t'. induction t; destruct t'; simpl in *;
rewrite ?andb_true_iff, ?beq_iff, ?N.eqb_eq, ?IHt, ?IHt1, ?IHt2;
intuition congruence.
Qed.
-Theorem eq_term_reflect (t t' : term) : reflect (t=t') (eq_term t t').
+Theorem eq_term_reflect (t t' : term) : reflect (t=t') (t =? t')%term.
Proof.
apply iff_reflect. symmetry. apply eq_term_iff.
Qed.
@@ -1107,13 +1035,13 @@ Ltac loop t :=
| (- ?X1)%term => loop X1
| (Tint ?X1) => loop X1
(* Eliminations *)
- | (if beq ?X1 ?X2 then _ else _) =>
+ | (if ?X1 =? ?X2 then _ else _) =>
let H := fresh "H" in
case (beq_reflect X1 X2); intro H;
try (rewrite H in *; clear H); simpl; auto; Simplify
- | (if bgt ?X1 ?X2 then _ else _) =>
- case (bgt_reflect X1 X2); intro; simpl; auto; Simplify
- | (if eq_term ?X1 ?X2 then _ else _) =>
+ | (if ?X1 <? ?X2 then _ else _) =>
+ case (blt_reflect X1 X2); intro; simpl; auto; Simplify
+ | (if (?X1 =? ?X2)%term then _ else _) =>
let H := fresh "H" in
case (eq_term_reflect X1 X2); intro H;
try (rewrite H in *; clear H); simpl; auto; Simplify
@@ -1148,31 +1076,32 @@ with Simplify := match goal with
(** Multiplication and sum by two constants. Invariant: [k1<>0]. *)
-Fixpoint scalar_norm_add (t : term) (k1 k2 : int) : term :=
+Fixpoint scalar_mult_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
+ | v1 * Tint x1 + l1 =>
+ v1 * Tint (x1 * k1) + scalar_mult_add l1 k1 k2
| Tint x => Tint (k1 * x + k2)
- | _ => (t * Tint k1 + Tint k2)%term (* shouldn't happen *)
- end.
+ | _ => t * Tint k1 + Tint k2 (* shouldn't happen *)
+ end%term.
-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).
+Theorem scalar_mult_add_stable e t k1 k2 :
+ interp_term e (scalar_mult_add t k1 k2) =
+ interp_term e (t * Tint k1 + Tint k2).
Proof.
induction t; simpl; Simplify; simpl; auto. f_equal. apply mult_comm.
- rewrite <- IHt2. simpl. apply OMEGA11.
+ rewrite IHt2. simpl. apply OMEGA11.
Qed.
(** Multiplication by a (non-nul) constant. *)
-Definition scalar_norm (t : term) (k : int) := scalar_norm_add t k 0.
+Definition scalar_mult (t : term) (k : int) := scalar_mult_add t k 0.
-Theorem scalar_norm_stable e t k :
- interp_term e (t * Tint k)%term = interp_term e (scalar_norm t k).
+Theorem scalar_mult_stable e t k :
+ interp_term e (scalar_mult t k) =
+ interp_term e (t * Tint k).
Proof.
- unfold scalar_norm. rewrite <- scalar_norm_add_stable. simpl.
- symmetry. apply plus_0_r.
+ unfold scalar_mult. rewrite scalar_mult_add_stable. simpl.
+ apply plus_0_r.
Qed.
(** Adding a constant
@@ -1181,18 +1110,18 @@ Qed.
definition spares some computations.
*)
-Fixpoint add_norm (t : term) (k : int) : term :=
+Fixpoint scalar_add (t : term) (k : int) : term :=
match t with
- | (m + l)%term => (m + add_norm l k)%term
+ | m + l => m + scalar_add l k
| Tint x => Tint (x + k)
- | _ => (t + Tint k)%term
- end.
+ | _ => t + Tint k
+ end%term.
-Theorem add_norm_stable e t k :
- interp_term e (t + Tint k)%term = interp_term e (add_norm t k).
+Theorem scalar_add_stable e t k :
+ interp_term e (scalar_add t k) = interp_term e (t + Tint k).
Proof.
induction t; simpl; Simplify; simpl; auto.
- rewrite <- IHt2. simpl. symmetry. apply plus_assoc.
+ rewrite IHt2. simpl. apply plus_assoc.
Qed.
(** Fusion of two equations.
@@ -1204,42 +1133,41 @@ Qed.
Fixpoint fusion (t1 t2 : term) (k1 k2 : int) : term :=
match t1 with
- | ([v1] * Tint x1 + l1)%term =>
+ | [v1] * Tint x1 + l1 =>
(fix fusion_t1 t2 : term :=
match t2 with
- | ([v2] * Tint x2 + l2)%term =>
+ | [v2] * Tint x2 + l2 =>
match N.compare v1 v2 with
| Eq =>
- 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 (k2 * x2) + fusion_t1 l2)%term
- | Gt => ([v1] * Tint (k1 * x1) + fusion l1 t2 k1 k2)%term
+ let k := (k1 * x1 + k2 * x2)%I in
+ if (k =? 0)%I then fusion l1 l2 k1 k2
+ else [v1] * Tint k + fusion l1 l2 k1 k2
+ | Lt => [v2] * Tint (k2 * x2) + fusion_t1 l2
+ | Gt => [v1] * Tint (k1 * x1) + fusion l1 t2 k1 k2
end
- | Tint x2 => ([v1] * Tint (k1 * x1) + fusion l1 t2 k1 k2)%term
- | _ => (t1 * Tint k1 + t2 * Tint k2)%term (* shouldn't happen *)
+ | Tint x2 => [v1] * Tint (k1 * x1) + fusion l1 t2 k1 k2
+ | _ => t1 * Tint k1 + t2 * Tint k2 (* shouldn't happen *)
end) t2
- | Tint x1 => scalar_norm_add t2 k2 (k1 * x1)
- | _ => (t1 * Tint k1 + t2 * Tint k2)%term (* shouldn't happen *)
- end.
+ | Tint x1 => scalar_mult_add t2 k2 (k1 * x1)
+ | _ => t1 * Tint k1 + t2 * Tint k2 (* shouldn't happen *)
+ end%term.
Theorem fusion_stable e t1 t2 k1 k2 :
- interp_term e (t1 * Tint k1 + t2 * Tint k2)%term =
- interp_term e (fusion t1 t2 k1 k2).
+ interp_term e (fusion t1 t2 k1 k2) =
+ interp_term e (t1 * Tint k1 + t2 * Tint k2).
Proof.
revert t2; induction t1; simpl; Simplify; simpl; auto.
- - intros; rewrite <- scalar_norm_add_stable. simpl.
+ - intros; rewrite scalar_mult_add_stable. simpl.
rewrite plus_comm. f_equal. apply mult_comm.
- intros. Simplify. induction t2; simpl; Simplify; simpl; auto.
- + rewrite <- IHt1_2. simpl. rewrite (mult_comm k1); apply OMEGA11.
- + rewrite <- IHt1_2. simpl. subst n0.
+ + 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 <- OMEGA10, H0. now autorewrite with int.
+ + 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.
+ + rewrite IHt2_2. simpl. rewrite (mult_comm k2); apply OMEGA12.
+ + rewrite IHt1_2. simpl. rewrite (mult_comm k1); apply OMEGA11.
Qed.
(** Term normalization.
@@ -1253,11 +1181,10 @@ Fixpoint normalize t :=
| Tint n => Tint n
| [n]%term => ([n] * Tint 1 + Tint 0)%term
| (t + t')%term => fusion (normalize t) (normalize t') 1 1
- | (- t)%term => scalar_norm (normalize t) (-(1))
+ | (- t)%term => scalar_mult (normalize t) (-(1))
| (t - t')%term => fusion (normalize t) (normalize t') 1 (-(1))
| (Tint k * t)%term | (t * Tint k)%term =>
- if beq k 0 then Tint 0
- else scalar_norm (normalize t) k
+ if k =? 0 then Tint 0 else scalar_mult (normalize t) k
| (t1 * t2)%term => (t1 * t2)%term (* shouldn't happen *)
end.
@@ -1265,9 +1192,8 @@ Theorem normalize_stable : term_stable normalize.
Proof.
intros e t.
induction t; simpl; Simplify; simpl;
- rewrite <- ?scalar_norm_stable; simpl in *; rewrite <- ?IHt1;
- rewrite <- ?fusion_stable; simpl;
- rewrite ?mult_0_l, ?mult_0_r, ?mult_1_l, ?mult_1_r, ?plus_0_r; auto.
+ rewrite ?scalar_mult_stable; simpl in *; rewrite <- ?IHt1;
+ rewrite ?fusion_stable; simpl; autorewrite with int; auto.
- now f_equal.
- rewrite mult_comm. now f_equal.
- rewrite <- opp_eq_mult_neg_1, <-minus_def. now f_equal.
@@ -1315,57 +1241,49 @@ Fixpoint normalize_prop (negated:bool)(p:proposition) :=
Definition normalize_hyps := List.map (normalize_prop false).
-Opaque normalize.
+Local Ltac simp := cbn -[normalize].
Theorem normalize_prop_valid b e ep p :
- interp_prop e ep p <->
- interp_prop e ep (normalize_prop b p).
+ interp_prop e ep (normalize_prop b p) <-> interp_prop e ep p.
Proof.
revert b.
- induction p; intros; simpl; try tauto.
- - destruct b; simpl;
+ induction p; intros; simp; try tauto.
+ - destruct b; simp;
rewrite <- ?normalize_stable; simpl; rewrite ?minus_def.
- + rewrite not_eq. apply egal_left_iff.
- + apply egal_left_iff.
- - destruct b; simpl;
- rewrite <- ? normalize_stable; simpl; rewrite ?minus_def;
- apply not_iff_compat, egal_left_iff.
- - destruct b; simpl;
+ + rewrite not_eq. apply egal_left.
+ + apply egal_left.
+ - destruct b; simp;
+ rewrite <- ?normalize_stable; simpl; rewrite ?minus_def;
+ apply not_iff_compat, egal_left.
+ - destruct b; simp;
rewrite <- ? normalize_stable; simpl; rewrite ?minus_def.
- + rewrite le_lt_iff. apply not_iff_compat.
- rewrite le_lt_int. rewrite le_left.
- rewrite <- !plus_assoc. now rewrite (plus_comm (-(1))).
- + apply le_left.
- - destruct b; simpl;
+ + symmetry. rewrite le_lt_iff. apply not_iff_compat, lt_left.
+ + now rewrite <- le_left.
+ - destruct b; simp;
rewrite <- ? normalize_stable; simpl; rewrite ?minus_def.
- + rewrite ge_le_iff, le_lt_iff. apply not_iff_compat.
- rewrite le_lt_int. rewrite le_left.
- rewrite <- !plus_assoc. now rewrite (plus_comm (-(1))).
- + rewrite ge_le_iff. apply le_left.
- - destruct b; simpl;
+ + symmetry. rewrite ge_le_iff, le_lt_iff.
+ apply not_iff_compat, lt_left.
+ + rewrite ge_le_iff. now rewrite <- le_left.
+ - destruct b; simp;
rewrite <- ? normalize_stable; simpl; rewrite ?minus_def.
+ rewrite gt_lt_iff, lt_le_iff. apply not_iff_compat.
- apply le_left.
- + rewrite gt_lt_iff. rewrite le_lt_int. rewrite le_left.
- rewrite <- !plus_assoc. now rewrite (plus_comm (-(1))).
- - destruct b; simpl;
+ now rewrite <- le_left.
+ + symmetry. rewrite gt_lt_iff. apply lt_left.
+ - destruct b; simp;
rewrite <- ? normalize_stable; simpl; rewrite ?minus_def.
+ rewrite lt_le_iff. apply not_iff_compat.
- apply le_left.
- + rewrite le_lt_int, le_left.
- rewrite <- !plus_assoc. now rewrite (plus_comm (-(1))).
- - now rewrite <- IHp.
- - now rewrite <- IHp1, <- IHp2.
- - now rewrite <- IHp1, <- IHp2.
- - now rewrite <- IHp1, <- IHp2.
+ now rewrite <- le_left.
+ + symmetry. apply lt_left.
+ - now rewrite IHp.
+ - now rewrite IHp1, IHp2.
+ - now rewrite IHp1, IHp2.
+ - now rewrite IHp1, IHp2.
Qed.
-Transparent normalize.
-
Theorem normalize_hyps_valid : valid_hyps normalize_hyps.
Proof.
intros e ep l. induction l; simpl; intuition.
- now rewrite <- normalize_prop_valid.
+ now rewrite normalize_prop_valid.
Qed.
Theorem normalize_hyps_goal (ep : list Prop) (env : list int) (l : hyps) :
@@ -1460,9 +1378,9 @@ Inductive t_omega : Set :=
Definition bad_constant (i : nat) (h : hyps) :=
match nth_hyps i h with
- | EqTerm (Tint Nul) (Tint n) => if beq n Nul then h else absurd
- | NeqTerm (Tint Nul) (Tint n) => if beq n Nul then absurd else h
- | LeqTerm (Tint Nul) (Tint n) => if bgt Nul n then absurd else h
+ | EqTerm (Tint Nul) (Tint n) => if n =? Nul then h else absurd
+ | NeqTerm (Tint Nul) (Tint n) => if n =? Nul then absurd else h
+ | LeqTerm (Tint Nul) (Tint n) => if n <? Nul then absurd else h
| _ => h
end.
@@ -1470,7 +1388,7 @@ Theorem bad_constant_valid i : valid_hyps (bad_constant i).
Proof.
unfold valid_hyps, bad_constant; intros ep e lp H.
generalize (nth_valid ep e i lp H); Simplify.
- rewrite gt_lt_iff in *. rewrite le_lt_iff. intuition.
+ rewrite le_lt_iff. intuition.
Qed.
(** [NOT_EXACT_DIVIDE] *)
@@ -1479,10 +1397,10 @@ Definition not_exact_divide (i : nat) (k1 k2 : int) (body : term)
(l : hyps) :=
match nth_hyps i l with
| EqTerm (Tint Nul) b =>
- if beq Nul 0 &&
- eq_term (scalar_norm_add body k1 k2) b &&
- bgt k2 0 &&
- bgt k1 k2
+ if (Nul =? 0) &&
+ (scalar_mult_add body k1 k2 =? b)%term &&
+ (0 <? k2) &&
+ (k2 <? k1)
then absurd
else l
| _ => l
@@ -1494,7 +1412,7 @@ Theorem not_exact_divide_valid :
Proof.
unfold valid_hyps, not_exact_divide; intros.
generalize (nth_valid ep e i lp); Simplify.
- rewrite <-H1, <-scalar_norm_add_stable. simpl.
+ rewrite <-H1, scalar_mult_add_stable. simpl.
intros.
absurd (interp_term e body * k1 + k2 = 0).
- now apply OMEGA4.
@@ -1507,12 +1425,12 @@ Qed.
Definition exact_divide (k : int) (body : term) (prop : proposition) :=
match prop with
- | EqTerm (Tint Null) b =>
- if beq Null 0 && eq_term (scalar_norm body k) b && negb (beq k 0)
+ | EqTerm (Tint o) b =>
+ if (o =? 0) && (scalar_mult body k =? b)%term && negb (k =? 0)
then EqTerm (Tint 0) body
else TrueTerm
- | NeqTerm (Tint Null) b =>
- if beq Null 0 && eq_term (scalar_norm body k) b && negb (beq k 0)
+ | NeqTerm (Tint o) b =>
+ if (o =? 0) && (scalar_mult body k =? b)%term && negb (k =? 0)
then NeqTerm (Tint 0) body
else TrueTerm
| _ => TrueTerm
@@ -1523,7 +1441,7 @@ Theorem exact_divide_valid :
Proof.
unfold valid1, exact_divide; intros k t ep e p1;
Simplify; simpl; auto; subst;
- rewrite <- scalar_norm_stable; simpl; intros.
+ rewrite scalar_mult_stable; simpl; intros.
- destruct (mult_integral _ _ (eq_sym H0)); intuition.
- contradict H0; rewrite <- H0, mult_0_l; auto.
Qed.
@@ -1533,11 +1451,11 @@ Qed.
Definition divide_and_approx (k1 k2 : int) (body : term)
(prop : proposition) :=
match prop with
- | LeqTerm (Tint Null) b =>
- if beq Null 0 &&
- eq_term (scalar_norm_add body k1 k2) b &&
- bgt k1 0 &&
- bgt k1 k2
+ | LeqTerm (Tint o) b =>
+ if (o =? 0) &&
+ (scalar_mult_add body k1 k2 =? b)%term &&
+ (0 <? k1) &&
+ (k2 <? k1)
then LeqTerm (Tint 0) body
else prop
| _ => prop
@@ -1549,7 +1467,7 @@ Theorem divide_and_approx_valid :
Proof.
unfold valid1, divide_and_approx.
intros k1 k2 body ep e p1. Simplify. subst.
- rewrite <- scalar_norm_add_stable. simpl.
+ rewrite scalar_mult_add_stable. simpl.
intro H; now apply mult_le_approx with (3 := H).
Qed.
@@ -1557,40 +1475,40 @@ Qed.
Definition sum (k1 k2 : int) (prop1 prop2 : proposition) :=
match prop1 with
- | EqTerm (Tint Null) b1 =>
+ | EqTerm (Tint o) b1 =>
match prop2 with
- | EqTerm (Tint Null') b2 =>
- if beq Null 0 && beq Null' 0
+ | EqTerm (Tint o') b2 =>
+ if (o =? 0) && (o' =? 0)
then EqTerm (Tint 0) (fusion b1 b2 k1 k2)
else TrueTerm
- | LeqTerm (Tint Null') b2 =>
- if beq Null 0 && beq Null' 0 && bgt k2 0
+ | LeqTerm (Tint o') b2 =>
+ if (o =? 0) && (o' =? 0) && (0 <? k2)
then LeqTerm (Tint 0) (fusion b1 b2 k1 k2)
else TrueTerm
- | NeqTerm (Tint Null') b2 =>
- if beq Null 0 && beq Null' 0 && negb (beq k2 0)
+ | NeqTerm (Tint o') b2 =>
+ if (o =? 0) && (o' =? 0) && negb (k2 =? 0)
then NeqTerm (Tint 0) (fusion b1 b2 k1 k2)
else TrueTerm
| _ => TrueTerm
end
- | LeqTerm (Tint Null) b1 =>
- if beq Null 0 && bgt k1 0
+ | LeqTerm (Tint o) b1 =>
+ if (o =? 0) && (0 <? k1)
then match prop2 with
- | EqTerm (Tint Null') b2 =>
- if beq Null' 0 then
+ | EqTerm (Tint o') b2 =>
+ if o' =? 0 then
LeqTerm (Tint 0) (fusion b1 b2 k1 k2)
else TrueTerm
- | LeqTerm (Tint Null') b2 =>
- if beq Null' 0 && bgt k2 0
+ | LeqTerm (Tint o') b2 =>
+ if (o' =? 0) && (0 <? k2)
then LeqTerm (Tint 0) (fusion b1 b2 k1 k2)
else TrueTerm
| _ => TrueTerm
end
else TrueTerm
- | NeqTerm (Tint Null) b1 =>
+ | NeqTerm (Tint o) b1 =>
match prop2 with
- | EqTerm (Tint Null') b2 =>
- if beq Null 0 && beq Null' 0 && negb (beq k1 0)
+ | EqTerm (Tint o') b2 =>
+ if (o =? 0) && (o' =? 0) && negb (k1 =? 0)
then NeqTerm (Tint 0) (fusion b1 b2 k1 k2)
else TrueTerm
| _ => TrueTerm
@@ -1602,21 +1520,25 @@ Theorem sum_valid :
forall (k1 k2 : int), valid2 (sum k1 k2).
Proof.
unfold valid2; intros k1 k2 t ep e p1 p2; unfold sum;
- Simplify; simpl; rewrite <- ?fusion_stable;
- simpl; intros; auto using sum1, sum2, sum3, sum4, sum5.
- - rewrite plus_comm. now apply sum5.
- - rewrite plus_comm. apply sum2; trivial; now apply sum4.
+ Simplify; simpl; rewrite ?fusion_stable;
+ simpl; intros; auto.
+ - apply sum1; auto.
+ - rewrite plus_comm. apply sum5; auto.
+ - apply sum2; auto using lt_le_weak.
+ - apply sum5; auto.
+ - rewrite plus_comm. apply sum2; auto using lt_le_weak.
+ - apply sum3; auto using lt_le_weak.
Qed.
(** [MERGE_EQ] *)
Definition merge_eq (prop1 prop2 : proposition) :=
match prop1 with
- | LeqTerm (Tint Null) b1 =>
+ | LeqTerm (Tint o) b1 =>
match prop2 with
- | LeqTerm (Tint Null') b2 =>
- if beq Null 0 && beq Null' 0 &&
- eq_term b1 (scalar_norm b2 (-(1)))
+ | LeqTerm (Tint o') b2 =>
+ if (o =? 0) && (o' =? 0) &&
+ (b1 =? scalar_mult b2 (-(1)))%term
then EqTerm (Tint 0) b1
else TrueTerm
| _ => TrueTerm
@@ -1627,7 +1549,7 @@ Definition merge_eq (prop1 prop2 : proposition) :=
Theorem merge_eq_valid : valid2 merge_eq.
Proof.
unfold valid2, merge_eq; intros ep e p1 p2; Simplify; simpl; auto.
- rewrite <- scalar_norm_stable. simpl.
+ rewrite scalar_mult_stable. simpl.
intros; symmetry ; apply OMEGA8 with (2 := H0).
- assumption.
- elim opp_eq_mult_neg_1; trivial.
@@ -1637,10 +1559,10 @@ Qed.
Definition split_ineq (i : nat) (f1 f2 : hyps -> lhyps) (l : hyps) :=
match nth_hyps i l with
- | NeqTerm (Tint Null) b1 =>
- if beq Null 0 then
- f1 (LeqTerm (Tint 0) (add_norm b1 (-(1))) :: l) ++
- f2 (LeqTerm (Tint 0) (scalar_norm_add b1 (-(1)) (-(1))) :: l)
+ | NeqTerm (Tint o) b1 =>
+ if o =? 0 then
+ f1 (LeqTerm (Tint 0) (scalar_add b1 (-(1))) :: l) ++
+ f2 (LeqTerm (Tint 0) (scalar_mult_add b1 (-(1)) (-(1))) :: l)
else l :: nil
| _ => l :: nil
end.
@@ -1656,9 +1578,9 @@ Proof.
auto; intros z; simpl; auto; intro H3.
Simplify.
apply append_valid; elim (OMEGA19 (interp_term e t2)).
- - intro H4; left; apply H1; simpl; rewrite <- add_norm_stable;
+ - intro H4; left; apply H1; simpl; rewrite scalar_add_stable;
simpl; auto.
- - intro H4; right; apply H2; simpl; rewrite <- scalar_norm_add_stable;
+ - intro H4; right; apply H2; simpl; rewrite scalar_mult_add_stable;
simpl; auto.
- generalize H3; unfold not; intros E1 E2; apply E1;
symmetry ; trivial.