diff options
Diffstat (limited to 'plugins/romega/ReflOmegaCore.v')
| -rw-r--r-- | plugins/romega/ReflOmegaCore.v | 3163 |
1 files changed, 934 insertions, 2229 deletions
diff --git a/plugins/romega/ReflOmegaCore.v b/plugins/romega/ReflOmegaCore.v index 187601fc..51b99b99 100644 --- a/plugins/romega/ReflOmegaCore.v +++ b/plugins/romega/ReflOmegaCore.v @@ -10,18 +10,20 @@ Require Import List Bool Sumbool EqNat Setoid Ring_theory Decidable ZArith_base. Delimit Scope Int_scope with I. -(* Abstract Integers. *) +(** * Abstract Integers. *) Module Type Int. Parameter t : Set. - Parameter zero : t. - Parameter one : t. - Parameter plus : t -> t -> t. - Parameter opp : t -> t. - Parameter minus : t -> t -> t. - Parameter mult : t -> t -> t. + Bind Scope Int_scope with t. + + Parameter Inline zero : t. + Parameter Inline one : t. + Parameter Inline plus : t -> t -> t. + Parameter Inline opp : t -> t. + Parameter Inline minus : t -> t -> t. + Parameter Inline mult : t -> t -> t. Notation "0" := zero : Int_scope. Notation "1" := one : Int_scope. @@ -32,15 +34,15 @@ Module Type Int. Open Scope Int_scope. - (* First, int is a ring: *) + (** First, Int is a ring: *) Axiom ring : @ring_theory t 0 1 plus mult minus opp (@eq t). - (* int should also be ordered: *) + (** Int should also be ordered: *) - Parameter le : t -> t -> Prop. - Parameter lt : t -> t -> Prop. - Parameter ge : t -> t -> Prop. - Parameter gt : t -> t -> Prop. + Parameter Inline le : t -> t -> Prop. + Parameter Inline lt : t -> t -> Prop. + Parameter Inline ge : t -> t -> Prop. + Parameter Inline gt : t -> t -> Prop. Notation "x <= y" := (le x y): Int_scope. Notation "x < y" := (lt x y) : Int_scope. Notation "x >= y" := (ge x y) : Int_scope. @@ -49,35 +51,47 @@ Module Type Int. Axiom ge_le_iff : forall i j, (i>=j) <-> (j<=i). Axiom gt_lt_iff : forall i j, (i>j) <-> (j<i). - (* Basic properties of this order *) + (** Basic properties of this order *) Axiom lt_trans : forall i j k, i<j -> j<k -> i<k. Axiom lt_not_eq : forall i j, i<j -> i<>j. - (* Compatibilities *) + (** Compatibilities *) Axiom lt_0_1 : 0<1. Axiom plus_le_compat : forall i j k l, i<=j -> k<=l -> i+k<=j+l. Axiom opp_le_compat : forall i j, i<=j -> (-j)<=(-i). Axiom mult_lt_compat_l : forall i j k, 0 < k -> i < j -> k*i<k*j. - (* We should have a way to decide the equality and the order*) + (** We should have a way to decide the equality and the order*) Parameter compare : t -> t -> comparison. Infix "?=" := compare (at level 70, no associativity) : Int_scope. Axiom compare_Eq : forall i j, compare i j = Eq <-> i=j. Axiom compare_Lt : forall i j, compare i j = Lt <-> i<j. Axiom compare_Gt : forall i j, compare i j = Gt <-> i>j. - (* Up to here, these requirements could be fulfilled + (** Up to here, these requirements could be fulfilled by any totally ordered ring. Let's now be int-specific: *) Axiom le_lt_int : forall x y, x<y <-> x<=y+-(1). - (* Btw, lt_0_1 could be deduced from this last axiom *) + (** Btw, lt_0_1 could be deduced from this last axiom *) + + (** Now we also require a division function. + It is deliberately underspecified, since that's enough + for the proofs below. But the most appropriate variant + (and the one needed to stay in sync with the omega engine) + is "Floor" (the historical version of Coq's [Z.div]). *) + + Parameter diveucl : t -> t -> t * t. + Notation "i / j" := (fst (diveucl i j)). + Notation "i 'mod' j" := (snd (diveucl i j)). + Axiom diveucl_spec : + forall i j, j<>0 -> i = j * (i/j) + (i mod j). End Int. -(* Of course, Z is a model for our abstract int *) +(** Of course, Z is a model for our abstract int *) Module Z_as_Int <: Int. @@ -131,21 +145,24 @@ Module Z_as_Int <: Int. Definition le_lt_int := Z.lt_le_pred. -End Z_as_Int. + Definition diveucl := Z.div_eucl. + Definition diveucl_spec := Z.div_mod. +End Z_as_Int. +(** * Properties of abstract integers *) Module IntProperties (I:Int). Import I. Local Notation int := I.t. - (* Primo, some consequences of being a ring theory... *) + (** Primo, some consequences of being a ring theory... *) Definition two := 1+1. Notation "2" := two : Int_scope. - (* Aliases for properties packed in the ring record. *) + (** Aliases for properties packed in the ring record. *) Definition plus_assoc := ring.(Radd_assoc). Definition plus_comm := ring.(Radd_comm). @@ -160,31 +177,22 @@ Module IntProperties (I:Int). Opaque plus_assoc plus_comm plus_0_l mult_assoc mult_comm mult_1_l mult_plus_distr_r opp_def minus_def. - (* More facts about plus *) + (** More facts about [plus] *) 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. Lemma plus_reg_l : forall x y z, x+y = x+z -> y = z. Proof. intros. - rewrite (plus_0_r_reverse y), (plus_0_r_reverse z), <-(opp_def x). + rewrite <- (plus_0_r y), <- (plus_0_r z), <-(opp_def x). now rewrite plus_permute, plus_assoc, H, <- plus_assoc, plus_permute. Qed. - (* 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. + (** More facts about [mult] *) Lemma mult_plus_distr_l : forall x y z, x*(y+z)=x*y+x*z. Proof. @@ -193,18 +201,25 @@ Module IntProperties (I:Int). apply mult_plus_distr_r. Qed. - Lemma mult_0_l : forall x, 0*x = 0. + Lemma mult_0_l x : 0*x = 0. Proof. - intros. - generalize (mult_plus_distr_r 0 1 x). - rewrite plus_0_l, mult_1_l, plus_comm; intros. + assert (H := mult_plus_distr_r 0 1 x). + rewrite plus_0_l, mult_1_l, plus_comm in H. apply plus_reg_l with x. - rewrite <- H. - apply plus_0_r_reverse. + now rewrite <- H, plus_0_r. + Qed. + + Lemma mult_0_r x : x*0 = 0. + Proof. + rewrite mult_comm. apply mult_0_l. Qed. + Lemma mult_1_r x : x*1 = x. + Proof. + rewrite mult_comm. apply mult_1_l. + Qed. - (* More facts about opp *) + (** More facts about [opp] *) Definition plus_opp_r := opp_def. @@ -249,104 +264,47 @@ 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 ne_left_2 : forall x y : int, x<>y -> 0<>(x + - y). - Proof. - intros; contradict H. - apply (plus_reg_l (-y)). - now rewrite plus_opp_l, plus_comm, H. - Qed. - - (* Special lemmas for factorisation. *) - - Lemma red_factor0 : forall n, n = n*1. - Proof. symmetry; rewrite mult_comm; apply mult_1_l. Qed. - - Lemma red_factor1 : forall n, n+n = n*2. - Proof. - intros; unfold two. - now rewrite mult_comm, mult_plus_distr_r, mult_1_l. - Qed. - - Lemma red_factor2 : forall n m, n + n*m = n * (1+m). - Proof. - intros; rewrite mult_plus_distr_l. - f_equal; now rewrite mult_comm, mult_1_l. - Qed. - - Lemma red_factor3 : forall n m, n*m + n = n*(1+m). - Proof. intros; now rewrite plus_comm, red_factor2. Qed. - - Lemma red_factor4 : forall n m p, n*m + n*p = n*(m+p). + Lemma egal_left n m : 0 = n+-m <-> n = m. Proof. - intros; now rewrite mult_plus_distr_l. + split; intros. + - apply plus_reg_l with (-m). + rewrite plus_comm, <- H. symmetry. apply plus_opp_l. + - symmetry. subst; apply opp_def. Qed. - Lemma red_factor5 : forall n m , n * 0 + m = m. - Proof. intros; now rewrite mult_comm, mult_0_l, plus_0_l. Qed. - - Definition red_factor6 := plus_0_r_reverse. - - - (* Specialized distributivities *) + (** Specialized distributivities *) 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). - Proof. - intros; 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). - Proof. - intros; now autorewrite with int. - Qed. + Hint Rewrite plus_0_l plus_0_r mult_0_l mult_0_r mult_1_l mult_1_r : int. - Lemma OMEGA12 : - forall v2 c2 l1 l2 k2 : int, - l1 + (v2 * c2 + l2) * k2 = v2 * (c2 * k2) + (l1 + l2 * k2). + 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; now rewrite plus_permute. + autorewrite with int; f_equal; now rewrite plus_permute. Qed. - Lemma OMEGA13 : - forall v l1 l2 x : int, - v * -x + l1 + (v * x + l2) = l1 + l2. + Lemma OMEGA11 v1 c1 l1 l2 k1 : + v1 * (c1 * k1) + (l1 * k1 + l2) = (v1 * c1 + l1) * k1 + l2. Proof. - intros; autorewrite with int. - rewrite plus_permute; f_equal. - rewrite plus_assoc. - now rewrite <- mult_plus_distr_l, plus_opp_l, mult_comm, mult_0_l, plus_0_l. + now autorewrite with int. Qed. - Lemma OMEGA15 : - forall v c1 c2 l1 l2 k2 : int, - v * c1 + l1 + (v * c2 + l2) * k2 = v * (c1 + 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; f_equal; now rewrite plus_permute. + autorewrite with int; now rewrite plus_permute. Qed. - Lemma OMEGA16 : forall v c l k : int, (v * c + l) * k = v * (c * k) + l * k. + Lemma sum1 a b c d : 0 = a -> 0 = b -> 0 = a * c + b * d. Proof. - intros; now autorewrite with int. - Qed. - - Lemma sum1 : forall a b c d : int, 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. - (* Secondo, some results about order (and equality) *) + (** Secondo, some results about order (and equality) *) Lemma lt_irrefl : forall n, ~ n<n. Proof. @@ -413,86 +371,74 @@ Module IntProperties (I:Int). Definition beq i j := match compare i j with Eq => true | _ => false end. - Lemma beq_iff : forall i j, beq i j = true <-> i=j. - Proof. - intros; unfold beq; generalize (compare_Eq i j). - destruct compare; intuition discriminate. - Qed. + Infix "=?" := beq : Int_scope. - Lemma beq_true : forall i j, beq i j = true -> i=j. + Lemma beq_iff i j : (i =? j) = true <-> i=j. Proof. - intros. - rewrite <- beq_iff; auto. + unfold beq. rewrite <- (compare_Eq i j). now destruct compare. Qed. - Lemma beq_false : forall i j, beq i j = false -> i<>j. + Lemma beq_reflect i j : reflect (i=j) (i =? j). Proof. - intros. - intro H'. - rewrite <- beq_iff in H'; rewrite H' in H; discriminate. + apply iff_reflect. symmetry. apply beq_iff. Qed. Lemma eq_dec : forall n m:int, { n=m } + { n<>m }. Proof. - intros; generalize (beq_iff n m); destruct beq; [left|right]; intuition. + 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 : forall i j, bgt i j = true <-> i>j. + Lemma blt_iff i j : (i <? j) = true <-> i<j. Proof. - intros; unfold bgt; generalize (compare_Gt i j). - destruct compare; intuition discriminate. + unfold blt. rewrite <- (compare_Lt i j). now destruct compare. Qed. - Lemma bgt_true : forall i j, bgt i j = true -> i>j. - Proof. intros; now rewrite <- bgt_iff. Qed. - - Lemma bgt_false : forall i j, bgt i j = false -> i<=j. + Lemma blt_reflect i j : reflect (i<j) (i <? j). Proof. - intros. - rewrite le_lt_iff, <-gt_lt_iff, <-bgt_iff; intro H'; now rewrite H' in H. + apply iff_reflect. symmetry. apply blt_iff. Qed. Lemma le_is_lt_or_eq : forall n m, n<=m -> { n<m } + { n=m }. Proof. - intros. + intros n m Hnm. destruct (eq_dec n m) as [H'|H']. - right; intuition. - left; rewrite lt_le_iff. - contradict H'. - apply le_antisym; auto. + - right; intuition. + - left; rewrite lt_le_iff. + contradict H'. + now apply le_antisym. Qed. Lemma le_neq_lt : forall n m, n<=m -> n<>m -> n<m. Proof. - intros. - destruct (le_is_lt_or_eq _ _ H); intuition. + intros n m H. now destruct (le_is_lt_or_eq _ _ H). Qed. Lemma le_trans : forall n m p, n<=m -> m<=p -> n<=p. Proof. - intros n m p; do 3 rewrite le_lt_iff; intros A B C. + intros n m p; rewrite 3 le_lt_iff; intros A B C. destruct (lt_eq_lt_dec p m) as [[H|H]|H]; subst; auto. generalize (lt_trans _ _ _ H C); intuition. Qed. - (* order and operations *) - - Lemma le_0_neg : forall n, 0 <= n <-> -n <= 0. + Lemma not_eq (a b:int) : ~ a <> b <-> a = b. Proof. - intros. - pattern 0 at 2; rewrite <- (mult_0_l (-(1))). - rewrite <- opp_eq_mult_neg_1. - split; intros. - apply opp_le_compat; auto. - rewrite <-(opp_involutive 0), <-(opp_involutive n). - apply opp_le_compat; auto. + destruct (eq_dec a b); intuition. Qed. - Lemma le_0_neg' : forall n, n <= 0 <-> 0 <= -n. + (** Order and operations *) + + Lemma le_0_neg n : n <= 0 <-> 0 <= -n. Proof. - intros; rewrite le_0_neg, opp_involutive; intuition. + rewrite <- (mult_0_l (-(1))) at 2. + rewrite <- opp_eq_mult_neg_1. + split; intros. + - now apply opp_le_compat. + - rewrite <-(opp_involutive 0), <-(opp_involutive n). + now apply opp_le_compat. Qed. Lemma plus_le_reg_r : forall n m p, n + p <= m + p -> n <= m. @@ -534,20 +480,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. - pattern 0 at 2; rewrite <- (mult_0_l (-(1))). + rewrite <- (mult_0_l (-(1))) at 2. rewrite <- opp_eq_mult_neg_1. split; intros. - apply opp_lt_compat; auto. - 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. + - rewrite <-(opp_involutive 0), <-(opp_involutive n). + now apply opp_lt_compat. Qed. Lemma mult_lt_0_compat : forall n m, 0 < n -> 0 < m -> 0 < n*m. @@ -557,111 +497,70 @@ Module IntProperties (I:Int). apply mult_lt_compat_l; auto. Qed. - Lemma mult_integral : forall n m, n * m = 0 -> n = 0 \/ m = 0. + Lemma mult_integral_r n m : 0 < n -> n * m = 0 -> m = 0. Proof. - intros. - destruct (lt_eq_lt_dec n 0) as [[Hn|Hn]|Hn]; auto; - destruct (lt_eq_lt_dec m 0) as [[Hm|Hm]|Hm]; auto; exfalso. - - rewrite lt_0_neg' in Hn. - rewrite lt_0_neg' in Hm. - generalize (mult_lt_0_compat _ _ Hn Hm). - rewrite <- opp_mult_distr_r, mult_comm, <- opp_mult_distr_r, opp_involutive. - rewrite mult_comm, H. - exact (lt_irrefl 0). - - rewrite lt_0_neg' in Hn. - generalize (mult_lt_0_compat _ _ Hn Hm). - rewrite mult_comm, <- opp_mult_distr_r, mult_comm. - rewrite H. - rewrite opp_eq_mult_neg_1, mult_0_l. - exact (lt_irrefl 0). - - rewrite lt_0_neg' in Hm. - generalize (mult_lt_0_compat _ _ Hn Hm). - rewrite <- opp_mult_distr_r. - rewrite H. - rewrite opp_eq_mult_neg_1, mult_0_l. - exact (lt_irrefl 0). - - generalize (mult_lt_0_compat _ _ Hn Hm). - rewrite H. - exact (lt_irrefl 0). + intros Hn H. + destruct (lt_eq_lt_dec 0 m) as [[Hm| <- ]|Hm]; auto; exfalso. + - generalize (mult_lt_0_compat _ _ Hn Hm). + rewrite H. + exact (lt_irrefl 0). + - 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). Qed. - Lemma mult_le_compat : - forall i j k l, i<=j -> k<=l -> 0<=i -> 0<=k -> i*k<=j*l. + Lemma mult_integral n m : n * m = 0 -> n = 0 \/ m = 0. Proof. - intros. - destruct (le_is_lt_or_eq _ _ H1). - - apply le_trans with (i*l). - destruct (le_is_lt_or_eq _ _ H0); [ | subst; apply le_refl]. - apply lt_le_weak. - apply mult_lt_compat_l; auto. - - generalize (le_trans _ _ _ H2 H0); clear H0 H1 H2; intros. - rewrite (mult_comm i), (mult_comm j). - destruct (le_is_lt_or_eq _ _ H0); - [ | subst; do 2 rewrite mult_0_l; apply le_refl]. - destruct (le_is_lt_or_eq _ _ H); - [ | subst; apply le_refl]. - apply lt_le_weak. - apply mult_lt_compat_l; auto. - - subst i. - rewrite mult_0_l. - generalize (le_trans _ _ _ H2 H0); clear H0 H1 H2; intros. - destruct (le_is_lt_or_eq _ _ H); - [ | subst; rewrite mult_0_l; apply le_refl]. - destruct (le_is_lt_or_eq _ _ H0); - [ | subst; rewrite mult_comm, mult_0_l; apply le_refl]. - apply lt_le_weak. - apply mult_lt_0_compat; auto. + intros H. + destruct (lt_eq_lt_dec 0 n) as [[Hn|Hn]|Hn]. + - right; apply (mult_integral_r n m); trivial. + - now left. + - right; apply (mult_integral_r (-n) m). + + 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. - Lemma sum5 : - forall a b c d : int, c <> 0 -> 0 <> a -> 0 = b -> 0 <> a * c + b * d. + Lemma mult_le_compat_l i j k : + 0<=k -> i<=j -> k*i <= k*j. Proof. - intros. - subst b; rewrite mult_0_l, plus_0_r. - contradict H. - symmetry in H; destruct (mult_integral _ _ H); congruence. + intros Hk Hij. + apply le_is_lt_or_eq in Hk. apply le_is_lt_or_eq in Hij. + destruct Hk as [Hk | <-], Hij as [Hij | <-]; + rewrite ? mult_0_l; try apply le_refl. + now apply lt_le_weak, mult_lt_compat_l. Qed. - Lemma one_neq_zero : 1 <> 0. + Lemma mult_le_compat i j k l : + i<=j -> k<=l -> 0<=i -> 0<=k -> i*k<=j*l. Proof. - red; intro. - symmetry in H. - apply (lt_not_eq 0 1); auto. - apply lt_0_1. + intros Hij Hkl Hi Hk. + apply le_trans with (i*l). + - now apply mult_le_compat_l. + - rewrite (mult_comm i), (mult_comm j). + apply mult_le_compat_l; trivial. + now apply le_trans with k. 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 : forall n m, n <= m -> 0 <= m + - n. + Lemma le_left n m : n <= m <-> 0 <= m + - n. Proof. - intros. - rewrite <- (opp_def m). - apply plus_le_compat. - apply le_refl. - apply opp_le_compat; auto. + split; intros. + - rewrite <- (opp_def m). + apply plus_le_compat. + apply le_refl. + apply opp_le_compat; auto. + - apply plus_le_reg_r with (-n). + now rewrite plus_opp_r. Qed. - Lemma OMEGA2 : forall x y, 0 <= x -> 0 <= y -> 0 <= x + y. - Proof. - intros. - replace 0 with (0+0). - apply plus_le_compat; auto. - rewrite plus_0_l; auto. - 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). @@ -675,17 +574,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. @@ -697,56 +594,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 lt_le_int) *) - - Lemma lt_left : forall n m, n < m -> 0 <= m + -(1) + - n. - Proof. - intros; apply le_left. - now rewrite <- le_lt_int. - Qed. + (** Lemmas specific to integers (they use [le_lt_int]) *) - Lemma lt_left_inv : forall x y, 0 <= y + -(1) + - x -> x < y. + Lemma lt_left n m : n < m <-> 0 <= m + -n + -(1). 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. + rewrite <- plus_assoc, (plus_comm (-n)), plus_assoc. + rewrite <- le_left. + apply le_lt_int. Qed. - Lemma OMEGA4 : forall x y z, x > 0 -> y > x -> z * y + x <> 0. + Lemma OMEGA4 x y z : 0 < x -> x < y -> 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). - rewrite H'. - pattern y at 2; rewrite <-(mult_1_l y), <-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. + - generalize (plus_le_lt_compat _ _ _ _ (le_refl (z*y)) H0). + rewrite H'. + rewrite <-(mult_1_l y) at 2. rewrite <-mult_plus_distr_r. + 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. + - apply (lt_not_eq 0 (z*y+x)); auto. + rewrite <- (plus_0_l 0). + 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. @@ -759,35 +639,22 @@ Module IntProperties (I:Int). apply opp_lt_compat; auto. Qed. - Lemma mult_le_approx : - forall n m p, n > 0 -> n > p -> 0 <= m * n + p -> 0 <= m. + Lemma mult_le_approx n m p : + 0 < n -> p < n -> 0 <= m * n + p -> 0 <= m. Proof. - intros n m p. - do 2 rewrite gt_lt_iff. - do 2 rewrite le_lt_iff; intros. - contradict H1. - rewrite lt_0_neg' in H1. - rewrite lt_0_neg'. - rewrite opp_plus_distr. - rewrite mult_comm, opp_mult_distr_r. + do 2 rewrite le_lt_iff; intros Hn Hpn H Hm. destruct H. + 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. apply lt_left. rewrite le_lt_int. - rewrite <- plus_assoc, (plus_comm (-p)), plus_assoc. - apply lt_left. - rewrite le_lt_int. - rewrite le_lt_int in H0. - apply le_trans with (n+-(1)); auto. + apply le_trans with (n+-(1)); [ now apply le_lt_int | ]. apply plus_le_compat; [ | apply le_refl ]. - rewrite le_lt_int in H1. - generalize (mult_le_compat _ _ _ _ (lt_le_weak _ _ H) H1 (le_refl 0) (le_refl 0)). - rewrite mult_0_l. - rewrite mult_plus_distr_l. - rewrite <- opp_eq_mult_neg_1. - intros. - generalize (plus_le_compat _ _ _ _ (le_refl n) H2). - now rewrite plus_permute, opp_def, plus_0_r, plus_0_r. + rewrite <- (mult_1_r n) at 1. + apply mult_le_compat_l; auto using lt_le_weak. Qed. - (* Some decidabilities *) + (** Some decidabilities *) Lemma dec_eq : forall i j:int, decidable (i=j). Proof. @@ -822,7 +689,7 @@ Module IntProperties (I:Int). End IntProperties. - +(** * The Coq side of the romega tactic *) Module IntOmega (I:Int). Import I. @@ -830,13 +697,16 @@ Module IP:=IntProperties(I). Import IP. Local Notation int := I.t. -(* \subsubsection{Definition of reified integer expressions} +(* ** Definition of reified integer expressions + Terms are either: - \begin{itemize} - \item integers [Tint] - \item variables [Tvar] - \item operation over integers (addition, product, opposite, subtraction) - The last two are translated in additions and products. *) + - integers [Tint] + - variables [Tvar] + - operation over integers (addition, product, opposite, subtraction) + + Opposite and subtraction are translated in additions and products. + Note that we'll only deal with products for which at least one side + is [Tint]. *) Inductive term : Set := | Tint : int -> term @@ -844,8 +714,9 @@ Inductive term : Set := | Tmult : term -> term -> term | Tminus : term -> term -> term | Topp : term -> term - | Tvar : nat -> term. + | Tvar : N -> term. +Bind Scope romega_scope with term. Delimit Scope romega_scope with term. Arguments Tint _%I. Arguments Tplus (_ _)%term. @@ -859,400 +730,212 @@ Infix "-" := Tminus : romega_scope. Notation "- x" := (Topp x) : romega_scope. Notation "[ x ]" := (Tvar x) (at level 0) : romega_scope. -(* \subsubsection{Definition of reified goals} *) +(* ** Definition of reified goals -(* Very restricted definition of handled predicates that should be extended + Very restricted definition of handled predicates that should be extended to cover a wider set of operations. Taking care of negations and disequations require solving more than a goal in parallel. This is a major improvement over previous versions. *) Inductive proposition : Set := - | EqTerm : term -> term -> proposition (* equality between terms *) - | LeqTerm : term -> term -> proposition (* less or equal on terms *) - | TrueTerm : proposition (* true *) - | FalseTerm : proposition (* false *) - | Tnot : proposition -> proposition (* negation *) + (** First, basic equations, disequations, inequations *) + | EqTerm : term -> term -> proposition + | NeqTerm : term -> term -> proposition + | LeqTerm : term -> term -> proposition | GeqTerm : term -> term -> proposition | GtTerm : term -> term -> proposition | LtTerm : term -> term -> proposition - | NeqTerm : term -> term -> proposition + (** Then, the supported logical connectors *) + | TrueTerm : proposition + | FalseTerm : proposition + | Tnot : proposition -> proposition | Tor : proposition -> proposition -> proposition | Tand : proposition -> proposition -> proposition | Timp : proposition -> proposition -> proposition + (** Everything else is left as a propositional atom (and ignored). *) | Tprop : nat -> proposition. -(* Definition of goals as a list of hypothesis *) +(** Definition of goals as a list of hypothesis *) Notation hyps := (list proposition). -(* Definition of lists of subgoals (set of open goals) *) +(** Definition of lists of subgoals (set of open goals) *) Notation lhyps := (list hyps). -(* a single goal packed in a subgoal list *) +(** A single goal packed in a subgoal list *) Notation singleton := (fun a : hyps => a :: nil). -(* an absurd goal *) +(** An absurd goal *) Definition absurd := FalseTerm :: nil. -(* \subsubsection{Traces for merging equations} - This inductive type describes how the monomial of two equations should be - merged when the equations are added. - - For [F_equal], both equations have the same head variable and coefficient - must be added, furthermore if coefficients are opposite, [F_cancel] should - be used to collapse the term. [F_left] and [F_right] indicate which monomial - should be put first in the result *) - -Inductive t_fusion : Set := - | F_equal : t_fusion - | F_cancel : t_fusion - | F_left : t_fusion - | F_right : t_fusion. - -(* \subsubsection{Rewriting steps to normalize terms} *) -Inductive step : Set := - (* apply the rewriting steps to both subterms of an operation *) - | C_DO_BOTH : step -> step -> step - (* apply the rewriting step to the first branch *) - | C_LEFT : step -> step - (* apply the rewriting step to the second branch *) - | C_RIGHT : step -> step - (* apply two steps consecutively to a term *) - | C_SEQ : step -> step -> step - (* empty step *) - | C_NOP : step - (* the following operations correspond to actual rewriting *) - | C_OPP_PLUS : step - | C_OPP_OPP : step - | C_OPP_MULT_R : step - | C_OPP_ONE : step - (* This is a special step that reduces the term (computation) *) - | C_REDUCE : step - | C_MULT_PLUS_DISTR : step - | C_MULT_OPP_LEFT : step - | C_MULT_ASSOC_R : step - | C_PLUS_ASSOC_R : step - | C_PLUS_ASSOC_L : step - | C_PLUS_PERMUTE : step - | C_PLUS_COMM : step - | C_RED0 : step - | C_RED1 : step - | C_RED2 : step - | C_RED3 : step - | C_RED4 : step - | C_RED5 : step - | C_RED6 : step - | C_MULT_ASSOC_REDUCED : step - | C_MINUS : step - | C_MULT_COMM : step. - -(* \subsubsection{Omega steps} *) -(* The following inductive type describes steps as they can be found in - the trace coming from the decision procedure Omega. *) - -Inductive t_omega : Set := - (* n = 0 and n!= 0 *) - | O_CONSTANT_NOT_NUL : nat -> t_omega - | O_CONSTANT_NEG : nat -> t_omega - (* division and approximation of an equation *) - | O_DIV_APPROX : int -> int -> term -> nat -> t_omega -> nat -> t_omega - (* no solution because no exact division *) - | O_NOT_EXACT_DIVIDE : int -> int -> term -> nat -> nat -> t_omega - (* exact division *) - | O_EXACT_DIVIDE : int -> term -> nat -> t_omega -> nat -> t_omega - | O_SUM : int -> nat -> int -> nat -> list t_fusion -> t_omega -> t_omega - | O_CONTRADICTION : nat -> nat -> nat -> t_omega - | O_MERGE_EQ : nat -> nat -> nat -> t_omega -> t_omega - | O_SPLIT_INEQ : nat -> nat -> t_omega -> t_omega -> t_omega - | O_CONSTANT_NUL : nat -> t_omega - | O_NEGATE_CONTRADICT : nat -> nat -> t_omega - | O_NEGATE_CONTRADICT_INV : nat -> nat -> nat -> t_omega - | O_STATE : int -> step -> nat -> nat -> t_omega -> t_omega. - -(* \subsubsection{Rules for normalizing the hypothesis} *) -(* These rules indicate how to normalize useful propositions - of each useful hypothesis before the decomposition of hypothesis. - The rules include the inversion phase for negation removal. *) - -Inductive p_step : Set := - | P_LEFT : p_step -> p_step - | P_RIGHT : p_step -> p_step - | P_INVERT : step -> p_step - | P_STEP : step -> p_step - | P_NOP : p_step. - -(* List of normalizations to perform : if the type [p_step] had a constructor - that indicated visiting both left and right branches, we would be able to - restrict ourselves to the case of only one normalization by hypothesis. - And since all hypothesis are useful (otherwise they wouldn't be included), - we would be able to replace [h_step] by a simple list. *) - -Inductive h_step : Set := - pair_step : nat -> p_step -> h_step. - -(* \subsubsection{Rules for decomposing the hypothesis} *) -(* This type allows navigation in the logical constructors that - form the predicats of the hypothesis in order to decompose them. - This allows in particular to extract one hypothesis from a - conjunction with possibly the right level of negations. *) - -Inductive direction : Set := - | D_left : direction - | D_right : direction - | D_mono : direction. - -(* This type allows extracting useful components from hypothesis, either - hypothesis generated by splitting a disjonction, or equations. - The last constructor indicates how to solve the obtained system - via the use of the trace type of Omega [t_omega] *) - -Inductive e_step : Set := - | E_SPLIT : nat -> list direction -> e_step -> e_step -> e_step - | E_EXTRACT : nat -> list direction -> e_step -> e_step - | E_SOLVE : t_omega -> e_step. - -(* \subsection{Efficient decidable equality} *) -(* For each reified data-type, we define an efficient equality test. - It is not the one produced by [Decide Equality]. - - Then we prove two theorem allowing elimination of such equalities : - \begin{verbatim} - (t1,t2: typ) (eq_typ t1 t2) = true -> t1 = t2. - (t1,t2: typ) (eq_typ t1 t2) = false -> ~ t1 = t2. - \end{verbatim} *) - -(* \subsubsection{Reified terms} *) - -Open Scope romega_scope. +(** ** Decidable equality on terms *) Fixpoint eq_term (t1 t2 : term) {struct t2} : bool := match t1, t2 with - | Tint st1, Tint st2 => beq st1 st2 - | (st11 + st12), (st21 + st22) => eq_term st11 st21 && eq_term st12 st22 - | (st11 * st12), (st21 * st22) => eq_term st11 st21 && eq_term st12 st22 - | (st11 - st12), (st21 - st22) => eq_term st11 st21 && eq_term st12 st22 - | (- st1), (- st2) => eq_term st1 st2 - | [st1], [st2] => beq_nat st1 st2 + | 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 + | (- t1), (- t2) => eq_term t1 t2 + | [v1], [v2] => N.eqb v1 v2 | _, _ => false - end. - -Close Scope romega_scope. + end%term. -Theorem eq_term_true : forall t1 t2 : term, eq_term t1 t2 = true -> t1 = t2. -Proof. - induction t1; destruct t2; simpl in *; try discriminate; - (rewrite andb_true_iff; intros (H1,H2)) || intros H; f_equal; - auto using beq_true, beq_nat_true. -Qed. +Infix "=?" := eq_term : romega_scope. -Theorem eq_term_refl : forall t0 : term, eq_term t0 t0 = true. +Theorem eq_term_iff (t t' : term) : + (t =? t')%term = true <-> t = t'. Proof. - induction t0; simpl in *; try (apply andb_true_iff; split); trivial. - - now apply beq_iff. - - now apply beq_nat_true_iff. + revert t'. induction t; destruct t'; simpl in *; + rewrite ?andb_true_iff, ?beq_iff, ?N.eqb_eq, ?IHt, ?IHt1, ?IHt2; + intuition congruence. Qed. -Ltac trivial_case := unfold not; intros; discriminate. - -Theorem eq_term_false : - forall t1 t2 : term, eq_term t1 t2 = false -> t1 <> t2. +Theorem eq_term_reflect (t t' : term) : reflect (t=t') (t =? t')%term. Proof. - intros t1 t2 H E. subst t2. now rewrite eq_term_refl in H. + apply iff_reflect. symmetry. apply eq_term_iff. Qed. -(* \subsubsection{Tactiques pour éliminer ces tests} - - Si on se contente de faire un [Case (eq_typ t1 t2)] on perd - totalement dans chaque branche le fait que [t1=t2] ou [~t1=t2]. - - Initialement, les développements avaient été réalisés avec les - tests rendus par [Decide Equality], c'est à dire un test rendant - des termes du type [{t1=t2}+{~t1=t2}]. Faire une élimination sur un - tel test préserve bien l'information voulue mais calculatoirement de - telles fonctions sont trop lentes. *) - -(* Les tactiques définies si après se comportent exactement comme si on - avait utilisé le test précédent et fait une elimination dessus. *) - -Ltac elim_eq_term t1 t2 := - let Aux := fresh "Aux" in - pattern (eq_term t1 t2); apply bool_eq_ind; intro Aux; - [ generalize (eq_term_true t1 t2 Aux); clear Aux - | generalize (eq_term_false t1 t2 Aux); clear Aux ]. - -Ltac elim_beq t1 t2 := - let Aux := fresh "Aux" in - pattern (beq t1 t2); apply bool_eq_ind; intro Aux; - [ generalize (beq_true t1 t2 Aux); clear Aux - | generalize (beq_false t1 t2 Aux); clear Aux ]. - -Ltac elim_bgt t1 t2 := - let Aux := fresh "Aux" in - pattern (bgt t1 t2); apply bool_eq_ind; intro Aux; - [ generalize (bgt_true t1 t2 Aux); clear Aux - | generalize (bgt_false t1 t2 Aux); clear Aux ]. - +(** ** Interpretations of terms (as integers). *) -(* \subsection{Interprétations} - \subsubsection{Interprétation des termes dans Z} *) +Fixpoint Nnth {A} (n:N)(l:list A)(default:A) := + match n, l with + | _, nil => default + | 0%N, x::_ => x + | _, _::l => Nnth (N.pred n) l default + end. -Fixpoint interp_term (env : list int) (t : term) {struct t} : int := +Fixpoint interp_term (env : list int) (t : term) : int := match t with | Tint x => x | (t1 + t2)%term => interp_term env t1 + interp_term env t2 | (t1 * t2)%term => interp_term env t1 * interp_term env t2 | (t1 - t2)%term => interp_term env t1 - interp_term env t2 | (- t)%term => - interp_term env t - | [n]%term => nth n env 0 + | [n]%term => Nnth n env 0 end. -(* \subsubsection{Interprétation des prédicats} *) +(** ** Interpretation of predicats (as Coq propositions) *) -Fixpoint interp_proposition (envp : list Prop) (env : list int) - (p : proposition) {struct p} : Prop := +Fixpoint interp_prop (envp : list Prop) (env : list int) + (p : proposition) : Prop := match p with | EqTerm t1 t2 => interp_term env t1 = interp_term env t2 + | NeqTerm t1 t2 => (interp_term env t1) <> (interp_term env t2) | LeqTerm t1 t2 => interp_term env t1 <= interp_term env t2 - | TrueTerm => True - | FalseTerm => False - | Tnot p' => ~ interp_proposition envp env p' | GeqTerm t1 t2 => interp_term env t1 >= interp_term env t2 | GtTerm t1 t2 => interp_term env t1 > interp_term env t2 | LtTerm t1 t2 => interp_term env t1 < interp_term env t2 - | NeqTerm t1 t2 => (interp_term env t1)<>(interp_term env t2) - | Tor p1 p2 => - interp_proposition envp env p1 \/ interp_proposition envp env p2 - | Tand p1 p2 => - interp_proposition envp env p1 /\ interp_proposition envp env p2 - | Timp p1 p2 => - interp_proposition envp env p1 -> interp_proposition envp env p2 + | TrueTerm => True + | FalseTerm => False + | Tnot p' => ~ interp_prop envp env p' + | Tor p1 p2 => interp_prop envp env p1 \/ interp_prop envp env p2 + | Tand p1 p2 => interp_prop envp env p1 /\ interp_prop envp env p2 + | Timp p1 p2 => interp_prop envp env p1 -> interp_prop envp env p2 | Tprop n => nth n envp True end. -(* \subsubsection{Inteprétation des listes d'hypothèses} - \paragraph{Sous forme de conjonction} - Interprétation sous forme d'une conjonction d'hypothèses plus faciles - à manipuler individuellement *) +(** ** Intepretation of hypothesis lists (as Coq conjunctions) *) -Fixpoint interp_hyps (envp : list Prop) (env : list int) - (l : hyps) {struct l} : Prop := +Fixpoint interp_hyps (envp : list Prop) (env : list int) (l : hyps) + : Prop := match l with | nil => True - | p' :: l' => interp_proposition envp env p' /\ interp_hyps envp env l' + | p' :: l' => interp_prop envp env p' /\ interp_hyps envp env l' end. -(* \paragraph{sous forme de but} - C'est cette interpétation que l'on utilise sur le but (car on utilise - [Generalize] et qu'une conjonction est forcément lourde (répétition des - types dans les conjonctions intermédiaires) *) +(** ** Interpretation of conclusion + hypotheses + + Here we use Coq implications : it's less easy to manipulate, + but handy to relate to the Coq original goal (cf. the use of + [generalize], and lighter (no repetition of types in intermediate + conjunctions). *) Fixpoint interp_goal_concl (c : proposition) (envp : list Prop) - (env : list int) (l : hyps) {struct l} : Prop := + (env : list int) (l : hyps) : Prop := match l with - | nil => interp_proposition envp env c + | nil => interp_prop envp env c | p' :: l' => - interp_proposition envp env p' -> interp_goal_concl c envp env l' + interp_prop envp env p' -> interp_goal_concl c envp env l' end. Notation interp_goal := (interp_goal_concl FalseTerm). -(* Les théorèmes qui suivent assurent la correspondance entre les deux - interprétations. *) +(** Equivalence between these two interpretations. *) Theorem goal_to_hyps : forall (envp : list Prop) (env : list int) (l : hyps), (interp_hyps envp env l -> False) -> interp_goal envp env l. Proof. - simple induction l; - [ simpl; auto - | simpl; intros a l1 H1 H2 H3; apply H1; intro H4; apply H2; auto ]. + induction l; simpl; auto. Qed. Theorem hyps_to_goal : forall (envp : list Prop) (env : list int) (l : hyps), interp_goal envp env l -> interp_hyps envp env l -> False. Proof. - simple induction l; simpl; [ auto | intros; apply H; elim H1; auto ]. -Qed. - -(* \subsection{Manipulations sur les hypothèses} *) - -(* \subsubsection{Définitions de base de stabilité pour la réflexion} *) -(* Une opération laisse un terme stable si l'égalité est préservée *) -Definition term_stable (f : term -> term) := - forall (e : list int) (t : term), interp_term e t = interp_term e (f t). - -(* Une opération est valide sur une hypothèse, si l'hypothèse implique le - résultat de l'opération. \emph{Attention : cela ne concerne que des - opérations sur les hypothèses et non sur les buts (contravariance)}. - On définit la validité pour une opération prenant une ou deux propositions - en argument (cela suffit pour omega). *) - -Definition valid1 (f : proposition -> proposition) := - forall (ep : list Prop) (e : list int) (p1 : proposition), - interp_proposition ep e p1 -> interp_proposition ep e (f p1). - -Definition valid2 (f : proposition -> proposition -> proposition) := - forall (ep : list Prop) (e : list int) (p1 p2 : proposition), - interp_proposition ep e p1 -> - interp_proposition ep e p2 -> interp_proposition ep e (f p1 p2). - -(* Dans cette notion de validité, la fonction prend directement une - liste de propositions et rend une nouvelle liste de proposition. - On reste contravariant *) - -Definition valid_hyps (f : hyps -> hyps) := - forall (ep : list Prop) (e : list int) (lp : hyps), - interp_hyps ep e lp -> interp_hyps ep e (f lp). - -(* Enfin ce théorème élimine la contravariance et nous ramène à une - opération sur les buts *) - -Theorem valid_goal : - forall (ep : list Prop) (env : list int) (l : hyps) (a : hyps -> hyps), - valid_hyps a -> interp_goal ep env (a l) -> interp_goal ep env l. -Proof. - intros; simpl; apply goal_to_hyps; intro H1; - apply (hyps_to_goal ep env (a l) H0); apply H; assumption. + induction l; simpl; auto. + intros H (H1,H2). auto. Qed. -(* \subsubsection{Généralisation a des listes de buts (disjonctions)} *) +(** ** Interpretations of list of goals + Here again, two flavours... *) Fixpoint interp_list_hyps (envp : list Prop) (env : list int) - (l : lhyps) {struct l} : Prop := + (l : lhyps) : Prop := match l with | nil => False | h :: l' => interp_hyps envp env h \/ interp_list_hyps envp env l' end. Fixpoint interp_list_goal (envp : list Prop) (env : list int) - (l : lhyps) {struct l} : Prop := + (l : lhyps) : Prop := match l with | nil => True | h :: l' => interp_goal envp env h /\ interp_list_goal envp env l' end. +(** Equivalence between the two flavours. *) + Theorem list_goal_to_hyps : forall (envp : list Prop) (env : list int) (l : lhyps), (interp_list_hyps envp env l -> False) -> interp_list_goal envp env l. Proof. - simple induction l; simpl; - [ auto - | intros h1 l1 H H1; split; - [ apply goal_to_hyps; intro H2; apply H1; auto - | apply H; intro H2; apply H1; auto ] ]. + induction l; simpl; intuition. now apply goal_to_hyps. Qed. Theorem list_hyps_to_goal : forall (envp : list Prop) (env : list int) (l : lhyps), interp_list_goal envp env l -> interp_list_hyps envp env l -> False. Proof. - simple induction l; simpl; - [ auto - | intros h1 l1 H (H1, H2) H3; elim H3; intro H4; - [ apply hyps_to_goal with (1 := H1); assumption | auto ] ]. + induction l; simpl; intuition. eapply hyps_to_goal; eauto. Qed. +(** ** Stabiliy and validity of operations *) + +(** An operation on terms is stable if the interpretation is unchanged. *) + +Definition term_stable (f : term -> term) := + forall (e : list int) (t : term), interp_term e t = interp_term e (f t). + +(** An operation on one hypothesis is valid if this hypothesis implies + the result of this operation. *) + +Definition valid1 (f : proposition -> proposition) := + forall (ep : list Prop) (e : list int) (p1 : proposition), + interp_prop ep e p1 -> interp_prop ep e (f p1). + +Definition valid2 (f : proposition -> proposition -> proposition) := + forall (ep : list Prop) (e : list int) (p1 p2 : proposition), + interp_prop ep e p1 -> + interp_prop ep e p2 -> interp_prop ep e (f p1 p2). + +(** Same for lists of hypotheses, and for list of goals *) + +Definition valid_hyps (f : hyps -> hyps) := + forall (ep : list Prop) (e : list int) (lp : hyps), + interp_hyps ep e lp -> interp_hyps ep e (f lp). + Definition valid_list_hyps (f : hyps -> lhyps) := forall (ep : list Prop) (e : list int) (lp : hyps), interp_hyps ep e lp -> interp_list_hyps ep e (f lp). @@ -1261,6 +944,16 @@ Definition valid_list_goal (f : hyps -> lhyps) := forall (ep : list Prop) (e : list int) (lp : hyps), interp_list_goal ep e (f lp) -> interp_goal ep e lp. +(** Some results about these validities. *) + +Theorem valid_goal : + forall (ep : list Prop) (env : list int) (l : hyps) (a : hyps -> hyps), + valid_hyps a -> interp_goal ep env (a l) -> interp_goal ep env l. +Proof. + intros; simpl; apply goal_to_hyps; intro H1; + apply (hyps_to_goal ep env (a l) H0); apply H; assumption. +Qed. + Theorem goal_valid : forall f : hyps -> lhyps, valid_list_hyps f -> valid_list_goal f. Proof. @@ -1274,33 +967,31 @@ Theorem append_valid : interp_list_hyps ep e l1 \/ interp_list_hyps ep e l2 -> interp_list_hyps ep e (l1 ++ l2). Proof. - intros ep e; simple induction l1; - [ simpl; intros l2 [H| H]; [ contradiction | trivial ] - | simpl; intros h1 t1 HR l2 [[H| H]| H]; - [ auto - | right; apply (HR l2); left; trivial - | right; apply (HR l2); right; trivial ] ]. - + induction l1; simpl in *. + - now intros l2 [H| H]. + - intros l2 [[H| H]| H]. + + auto. + + right; apply IHl1; now left. + + right; apply IHl1; now right. Qed. -(* \subsubsection{Opérateurs valides sur les hypothèses} *) +(** ** Valid operations on hypotheses *) + +(** Extract an hypothesis from the list *) -(* Extraire une hypothèse de la liste *) Definition nth_hyps (n : nat) (l : hyps) := nth n l TrueTerm. -Unset Printing Notations. + Theorem nth_valid : forall (ep : list Prop) (e : list int) (i : nat) (l : hyps), - interp_hyps ep e l -> interp_proposition ep e (nth_hyps i l). + interp_hyps ep e l -> interp_prop ep e (nth_hyps i l). Proof. - unfold nth_hyps; simple induction i; - [ simple induction l; simpl; [ auto | intros; elim H0; auto ] - | intros n H; simple induction l; - [ simpl; trivial - | intros; simpl; apply H; elim H1; auto ] ]. + unfold nth_hyps. induction i; destruct l; simpl in *; try easy. + intros (H1,H2). now apply IHi. Qed. -(* Appliquer une opération (valide) sur deux hypothèses extraites de - la liste et ajouter le résultat à la liste. *) +(** Apply a valid operation on two hypotheses from the list, and + store the result in the list. *) + Definition apply_oper_2 (i j : nat) (f : proposition -> proposition -> proposition) (l : hyps) := f (nth_hyps i l) (nth_hyps j l) :: l. @@ -1310,15 +1001,18 @@ Theorem apply_oper_2_valid : valid2 f -> valid_hyps (apply_oper_2 i j f). Proof. intros i j f Hf; unfold apply_oper_2, valid_hyps; simpl; - intros lp Hlp; split; [ apply Hf; apply nth_valid; assumption | assumption ]. + intros lp Hlp; split. + - apply Hf; apply nth_valid; assumption. + - assumption. Qed. -(* Modifier une hypothèse par application d'une opération valide *) +(** In-place modification of an hypothesis by application of + a valid operation. *) Fixpoint apply_oper_1 (i : nat) (f : proposition -> proposition) (l : hyps) {struct i} : hyps := match l with - | nil => nil (A:=proposition) + | nil => nil | p :: l' => match i with | O => f p :: l' @@ -1330,105 +1024,11 @@ Theorem apply_oper_1_valid : forall (i : nat) (f : proposition -> proposition), valid1 f -> valid_hyps (apply_oper_1 i f). Proof. - unfold valid_hyps; intros i f Hf ep e; elim i; - [ intro lp; case lp; - [ simpl; trivial - | simpl; intros p l' (H1, H2); split; - [ apply Hf with (1 := H1) | assumption ] ] - | intros n Hrec lp; case lp; - [ simpl; auto - | simpl; intros p l' (H1, H2); split; - [ assumption | apply Hrec; assumption ] ] ]. + unfold valid_hyps. + induction i; intros f Hf ep e [ | p lp]; simpl; intuition. Qed. -(* \subsubsection{Manipulations de termes} *) -(* Les fonctions suivantes permettent d'appliquer une fonction de - réécriture sur un sous terme du terme principal. Avec la composition, - cela permet de construire des réécritures complexes proches des - tactiques de conversion *) - -Definition apply_left (f : term -> term) (t : term) := - match t with - | (x + y)%term => (f x + y)%term - | (x * y)%term => (f x * y)%term - | (- x)%term => (- f x)%term - | x => x - end. - -Definition apply_right (f : term -> term) (t : term) := - match t with - | (x + y)%term => (x + f y)%term - | (x * y)%term => (x * f y)%term - | x => x - end. - -Definition apply_both (f g : term -> term) (t : term) := - match t with - | (x + y)%term => (f x + g y)%term - | (x * y)%term => (f x * g y)%term - | x => x - end. - -(* Les théorèmes suivants montrent la stabilité (conditionnée) des - fonctions. *) - -Theorem apply_left_stable : - forall f : term -> term, term_stable f -> term_stable (apply_left f). -Proof. - unfold term_stable; intros f H e t; case t; auto; simpl; - intros; elim H; trivial. -Qed. - -Theorem apply_right_stable : - forall f : term -> term, term_stable f -> term_stable (apply_right f). -Proof. - unfold term_stable; intros f H e t; case t; auto; simpl; - intros t0 t1; elim H; trivial. -Qed. - -Theorem apply_both_stable : - forall f g : term -> term, - term_stable f -> term_stable g -> term_stable (apply_both f g). -Proof. - unfold term_stable; intros f g H1 H2 e t; case t; auto; simpl; - intros t0 t1; elim H1; elim H2; trivial. -Qed. - -Theorem compose_term_stable : - forall f g : term -> term, - term_stable f -> term_stable g -> term_stable (fun t : term => f (g t)). -Proof. - unfold term_stable; intros f g Hf Hg e t; elim Hf; apply Hg. -Qed. - -(* \subsection{Les règles de réécriture} *) -(* Chacune des règles de réécriture est accompagnée par sa preuve de - stabilité. Toutes ces preuves ont la même forme : il faut analyser - suivant la forme du terme (élimination de chaque Case). On a besoin d'une - élimination uniquement dans les cas d'utilisation d'égalité décidable. - - Cette tactique itère la décomposition des Case. Elle est - constituée de deux fonctions s'appelant mutuellement : - \begin{itemize} - \item une fonction d'enrobage qui lance la recherche sur le but, - \item une fonction récursive qui décompose ce but. Quand elle a trouvé un - Case, elle l'élimine. - \end{itemize} - Les motifs sur les cas sont très imparfaits et dans certains cas, il - semble que cela ne marche pas. On aimerait plutot un motif de la - forme [ Case (?1 :: T) of _ end ] permettant de s'assurer que l'on - utilise le bon type. - - Chaque élimination introduit correctement exactement le nombre d'hypothèses - nécessaires et conserve dans le cas d'une égalité la connaissance du - résultat du test en faisant la réécriture. Pour un test de comparaison, - on conserve simplement le résultat. - - Cette fonction déborde très largement la résolution des réécritures - simples et fait une bonne partie des preuves des pas de Omega. -*) - -(* \subsubsection{La tactique pour prouver la stabilité} *) +(** ** A tactic for proving stability *) Ltac loop t := match t with @@ -1438,54 +1038,33 @@ Ltac loop t := (* Interpretations *) | (interp_hyps _ _ ?X1) => loop X1 | (interp_list_hyps _ _ ?X1) => loop X1 - | (interp_proposition _ _ ?X1) => loop X1 + | (interp_prop _ _ ?X1) => loop X1 | (interp_term _ ?X1) => loop X1 (* Propositions *) | (EqTerm ?X1 ?X2) => loop X1 || loop X2 | (LeqTerm ?X1 ?X2) => loop X1 || loop X2 - (* Termes *) + (* Terms *) | (?X1 + ?X2)%term => loop X1 || loop X2 | (?X1 - ?X2)%term => loop X1 || loop X2 | (?X1 * ?X2)%term => loop X1 || loop X2 | (- ?X1)%term => loop X1 | (Tint ?X1) => loop X1 (* Eliminations *) - | match ?X1 with - | EqTerm _ _ => _ - | LeqTerm _ _ => _ - | TrueTerm => _ - | FalseTerm => _ - | Tnot _ => _ - | GeqTerm _ _ => _ - | GtTerm _ _ => _ - | LtTerm _ _ => _ - | NeqTerm _ _ => _ - | Tor _ _ => _ - | Tand _ _ => _ - | Timp _ _ => _ - | Tprop _ => _ - end => destruct X1; auto; Simplify - | match ?X1 with - | Tint _ => _ - | (_ + _)%term => _ - | (_ * _)%term => _ - | (_ - _)%term => _ - | (- _)%term => _ - | [_]%term => _ - end => destruct X1; auto; Simplify - | (if beq ?X1 ?X2 then _ else _) => + | (if ?X1 =? ?X2 then _ else _) => let H := fresh "H" in - elim_beq X1 X2; intro H; try (rewrite H in *; clear H); - simpl; auto; Simplify - | (if bgt ?X1 ?X2 then _ else _) => + case (beq_reflect X1 X2); intro H; + try (rewrite H in *; clear H); simpl; auto; Simplify + | (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 - elim_bgt X1 X2; intro H; simpl; auto; Simplify - | (if eq_term ?X1 ?X2 then _ else _) => - let H := fresh "H" in - elim_eq_term X1 X2; intro H; try (rewrite H in *; clear H); - simpl; auto; Simplify + case (eq_term_reflect X1 X2); intro H; + try (rewrite H in *; clear H); simpl; auto; Simplify | (if _ && _ then _ else _) => rewrite andb_if; Simplify | (if negb _ then _ else _) => rewrite negb_if; Simplify + | match N.compare ?X1 ?X2 with _ => _ end => + destruct (N.compare_spec X1 X2); Simplify + | match ?X1 with _ => _ end => destruct X1; auto; Simplify | _ => fail end @@ -1494,875 +1073,529 @@ with Simplify := match goal with | _ => idtac end. -Ltac prove_stable x th := - match constr:(x) with - | ?X1 => - unfold term_stable, X1; intros; Simplify; simpl; - apply th - end. - -(* \subsubsection{Les règles elle mêmes} *) -Definition Tplus_assoc_l (t : term) := - match t with - | (n + (m + p))%term => (n + m + p)%term - | _ => t - end. - -Theorem Tplus_assoc_l_stable : term_stable Tplus_assoc_l. -Proof. - prove_stable Tplus_assoc_l (ring.(Radd_assoc)). -Qed. - -Definition Tplus_assoc_r (t : term) := - match t with - | (n + m + p)%term => (n + (m + p))%term - | _ => t - end. - -Theorem Tplus_assoc_r_stable : term_stable Tplus_assoc_r. -Proof. - prove_stable Tplus_assoc_r plus_assoc_reverse. -Qed. - -Definition Tmult_assoc_r (t : term) := - match t with - | (n * m * p)%term => (n * (m * p))%term - | _ => t - end. - -Theorem Tmult_assoc_r_stable : term_stable Tmult_assoc_r. -Proof. - prove_stable Tmult_assoc_r mult_assoc_reverse. -Qed. - -Definition Tplus_permute (t : term) := - match t with - | (n + (m + p))%term => (m + (n + p))%term - | _ => t - end. - -Theorem Tplus_permute_stable : term_stable Tplus_permute. -Proof. - prove_stable Tplus_permute plus_permute. -Qed. - -Definition Tplus_comm (t : term) := - match t with - | (x + y)%term => (y + x)%term - | _ => t - end. - -Theorem Tplus_comm_stable : term_stable Tplus_comm. -Proof. - prove_stable Tplus_comm plus_comm. -Qed. - -Definition Tmult_comm (t : term) := - match t with - | (x * y)%term => (y * x)%term - | _ => t - end. - -Theorem Tmult_comm_stable : term_stable Tmult_comm. -Proof. - prove_stable Tmult_comm mult_comm. -Qed. - -Definition T_OMEGA10 (t : term) := - match t with - | ((v * Tint c1 + l1) * Tint k1 + (v' * Tint c2 + l2) * Tint k2)%term => - if eq_term v v' - then (v * Tint (c1 * k1 + c2 * k2)%I + (l1 * Tint k1 + l2 * Tint k2))%term - else t - | _ => t - end. - -Theorem T_OMEGA10_stable : term_stable T_OMEGA10. -Proof. - prove_stable T_OMEGA10 OMEGA10. -Qed. - -Definition T_OMEGA11 (t : term) := - match t with - | ((v1 * Tint c1 + l1) * Tint k1 + l2)%term => - (v1 * Tint (c1 * k1) + (l1 * Tint k1 + l2))%term - | _ => t - end. - -Theorem T_OMEGA11_stable : term_stable T_OMEGA11. -Proof. - prove_stable T_OMEGA11 OMEGA11. -Qed. - -Definition T_OMEGA12 (t : term) := - match t with - | (l1 + (v2 * Tint c2 + l2) * Tint k2)%term => - (v2 * Tint (c2 * k2) + (l1 + l2 * Tint k2))%term - | _ => t - end. - -Theorem T_OMEGA12_stable : term_stable T_OMEGA12. -Proof. - prove_stable T_OMEGA12 OMEGA12. -Qed. - -Definition T_OMEGA13 (t : term) := - match t with - | (v * Tint x + l1 + (v' * Tint x' + l2))%term => - if eq_term v v' && beq x (-x') - then (l1+l2)%term - else t - | _ => t - end. - -Theorem T_OMEGA13_stable : term_stable T_OMEGA13. -Proof. - unfold term_stable, T_OMEGA13; intros; Simplify; simpl; - apply OMEGA13. -Qed. - -Definition T_OMEGA15 (t : term) := - match t with - | (v * Tint c1 + l1 + (v' * Tint c2 + l2) * Tint k2)%term => - if eq_term v v' - then (v * Tint (c1 + c2 * k2)%I + (l1 + l2 * Tint k2))%term - else t - | _ => t - end. - -Theorem T_OMEGA15_stable : term_stable T_OMEGA15. -Proof. - prove_stable T_OMEGA15 OMEGA15. -Qed. - -Definition T_OMEGA16 (t : term) := - match t with - | ((v * Tint c + l) * Tint k)%term => (v * Tint (c * k) + l * Tint k)%term - | _ => t - end. - - -Theorem T_OMEGA16_stable : term_stable T_OMEGA16. -Proof. - prove_stable T_OMEGA16 OMEGA16. -Qed. - -Definition Tred_factor5 (t : term) := - match t with - | (x * Tint c + y)%term => if beq c 0 then y else t - | _ => t - end. - -Theorem Tred_factor5_stable : term_stable Tred_factor5. -Proof. - prove_stable Tred_factor5 red_factor5. -Qed. - -Definition Topp_plus (t : term) := - match t with - | (- (x + y))%term => (- x + - y)%term - | _ => t - end. - -Theorem Topp_plus_stable : term_stable Topp_plus. -Proof. - prove_stable Topp_plus opp_plus_distr. -Qed. - - -Definition Topp_opp (t : term) := - match t with - | (- - x)%term => x - | _ => t - end. - -Theorem Topp_opp_stable : term_stable Topp_opp. -Proof. - prove_stable Topp_opp opp_involutive. -Qed. - -Definition Topp_mult_r (t : term) := - match t with - | (- (x * Tint k))%term => (x * Tint (- k))%term - | _ => t - end. - -Theorem Topp_mult_r_stable : term_stable Topp_mult_r. -Proof. - prove_stable Topp_mult_r opp_mult_distr_r. -Qed. - -Definition Topp_one (t : term) := - match t with - | (- x)%term => (x * Tint (-(1)))%term - | _ => t - end. - -Theorem Topp_one_stable : term_stable Topp_one. -Proof. - prove_stable Topp_one opp_eq_mult_neg_1. -Qed. - -Definition Tmult_plus_distr (t : term) := - match t with - | ((n + m) * p)%term => (n * p + m * p)%term - | _ => t - end. - -Theorem Tmult_plus_distr_stable : term_stable Tmult_plus_distr. -Proof. - prove_stable Tmult_plus_distr mult_plus_distr_r. -Qed. - -Definition Tmult_opp_left (t : term) := - match t with - | (- x * Tint y)%term => (x * Tint (- y))%term - | _ => t - end. - -Theorem Tmult_opp_left_stable : term_stable Tmult_opp_left. -Proof. - prove_stable Tmult_opp_left mult_opp_comm. -Qed. +(** ** Operations on equation bodies *) -Definition Tmult_assoc_reduced (t : term) := - match t with - | (n * Tint m * Tint p)%term => (n * Tint (m * p))%term - | _ => t - end. +(** The operations below handle in priority _normalized_ terms, i.e. + terms of the form: + [([v1]*Tint k1 + ([v2]*Tint k2 + (... + Tint cst)))] + with [v1>v2>...] and all [ki<>0]. + See [normalize] below for a way to put terms in this form. -Theorem Tmult_assoc_reduced_stable : term_stable Tmult_assoc_reduced. -Proof. - prove_stable Tmult_assoc_reduced mult_assoc_reverse. -Qed. + These operations also produce a correct (but suboptimal) + result in case of non-normalized input terms, but this situation + should normally not happen when running [romega]. -Definition Tred_factor0 (t : term) := (t * Tint 1)%term. + /!\ Do not modify this section (especially [fusion] and [normalize]) + without tweaking the corresponding functions in [refl_omega.ml]. +*) -Theorem Tred_factor0_stable : term_stable Tred_factor0. -Proof. - prove_stable Tred_factor0 red_factor0. -Qed. +(** Multiplication and sum by two constants. Invariant: [k1<>0]. *) -Definition Tred_factor1 (t : term) := +Fixpoint scalar_mult_add (t : term) (k1 k2 : int) : term := match t with - | (x + y)%term => - if eq_term x y - then (x * Tint 2)%term - else t - | _ => t - end. + | 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 (* shouldn't happen *) + end%term. -Theorem Tred_factor1_stable : term_stable Tred_factor1. +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. - prove_stable Tred_factor1 red_factor1. + induction t; simpl; Simplify; simpl; auto. f_equal. apply mult_comm. + rewrite IHt2. simpl. apply OMEGA11. Qed. -Definition Tred_factor2 (t : term) := - match t with - | (x + y * Tint k)%term => - if eq_term x y - then (x * Tint (1 + k))%term - else t - | _ => t - end. - -Theorem Tred_factor2_stable : term_stable Tred_factor2. -Proof. - prove_stable Tred_factor2 red_factor2. -Qed. +(** Multiplication by a (non-nul) constant. *) -Definition Tred_factor3 (t : term) := - match t with - | (x * Tint k + y)%term => - if eq_term x y - then (x * Tint (1 + k))%term - else t - | _ => t - end. +Definition scalar_mult (t : term) (k : int) := scalar_mult_add t k 0. -Theorem Tred_factor3_stable : term_stable Tred_factor3. +Theorem scalar_mult_stable e t k : + interp_term e (scalar_mult t k) = + interp_term e (t * Tint k). Proof. - prove_stable Tred_factor3 red_factor3. + unfold scalar_mult. rewrite scalar_mult_add_stable. simpl. + apply plus_0_r. Qed. +(** Adding a constant -Definition Tred_factor4 (t : term) := - match t with - | (x * Tint k1 + y * Tint k2)%term => - if eq_term x y - then (x * Tint (k1 + k2))%term - else t - | _ => t - end. - -Theorem Tred_factor4_stable : term_stable Tred_factor4. -Proof. - prove_stable Tred_factor4 red_factor4. -Qed. - -Definition Tred_factor6 (t : term) := (t + Tint 0)%term. - -Theorem Tred_factor6_stable : term_stable Tred_factor6. -Proof. - prove_stable Tred_factor6 red_factor6. -Qed. + Instead of using [scalar_norm_add t 1 k], the following + definition spares some computations. + *) -Definition Tminus_def (t : term) := +Fixpoint scalar_add (t : term) (k : int) : term := match t with - | (x - y)%term => (x + - y)%term - | _ => t - end. + | m + l => m + scalar_add l k + | Tint x => Tint (x + k) + | _ => t + Tint k + end%term. -Theorem Tminus_def_stable : term_stable Tminus_def. +Theorem scalar_add_stable e t k : + interp_term e (scalar_add t k) = interp_term e (t + Tint k). Proof. - prove_stable Tminus_def minus_def. + induction t; simpl; Simplify; simpl; auto. + rewrite IHt2. simpl. apply plus_assoc. Qed. -(* \subsection{Fonctions de réécriture complexes} *) +(** Division by a constant -(* \subsubsection{Fonction de réduction} *) -(* Cette fonction réduit un terme dont la forme normale est un entier. Il - suffit pour cela d'échanger le constructeur [Tint] avec les opérateurs - réifiés. La réduction est ``gratuite''. *) + All the non-constant coefficients should be exactly dividable *) -Fixpoint reduce (t : term) : term := +Fixpoint scalar_div (t : term) (k : int) : option (term * int) := match t with - | (x + y)%term => - match reduce x with - | Tint x' => - match reduce y with - | Tint y' => Tint (x' + y') - | y' => (Tint x' + y')%term - end - | x' => (x' + reduce y)%term - end - | (x * y)%term => - match reduce x with - | Tint x' => - match reduce y with - | Tint y' => Tint (x' * y') - | y' => (Tint x' * y')%term - end - | x' => (x' * reduce y)%term - end - | (x - y)%term => - match reduce x with - | Tint x' => - match reduce y with - | Tint y' => Tint (x' - y') - | y' => (Tint x' - y')%term - end - | x' => (x' - reduce y)%term + | v * Tint x + l => + let (q,r) := diveucl x k in + if (r =? 0)%I then + match scalar_div l k with + | None => None + | Some (u,c) => Some (v * Tint q + u, c) end - | (- x)%term => - match reduce x with - | Tint x' => Tint (- x') - | x' => (- x')%term - end - | _ => t - end. + else None + | Tint x => + let (q,r) := diveucl x k in + Some (Tint q, r) + | _ => None + end%term. + +Lemma scalar_div_stable e t k u c : k<>0 -> + scalar_div t k = Some (u,c) -> + interp_term e (u * Tint k + Tint c) = interp_term e t. +Proof. + revert u c. + induction t; simpl; Simplify; try easy. + - intros u c Hk. assert (H := diveucl_spec t0 k Hk). + simpl in H. + destruct diveucl as (q,r). simpl in H. rewrite H. + injection 1 as <- <-. simpl. f_equal. apply mult_comm. + - intros u c Hk. + destruct t1; simpl; Simplify; try easy. + destruct t1_2; simpl; Simplify; try easy. + assert (H := diveucl_spec t0 k Hk). + simpl in H. + destruct diveucl as (q,r). simpl in H. rewrite H. + case beq_reflect; [intros -> | easy]. + destruct (scalar_div t2 k) as [(u',c')|] eqn:E; [|easy]. + injection 1 as <- ->. simpl. + rewrite <- (IHt2 u' c Hk); simpl; auto. + rewrite plus_0_r , (mult_comm k q). symmetry. apply OMEGA11. +Qed. + + +(** Fusion of two equations. + + From two normalized equations, this fusion will produce + a normalized output corresponding to the coefficiented sum. + Invariant: [k1<>0] and [k2<>0]. +*) -Theorem reduce_stable : term_stable reduce. -Proof. - unfold term_stable; intros e t; elim t; auto; - try - (intros t0 H0 t1 H1; simpl; rewrite H0; rewrite H1; - (case (reduce t0); - [ intro z0; case (reduce t1); intros; auto - | intros; auto - | intros; auto - | intros; auto - | intros; auto - | intros; auto ])); intros t0 H0; simpl; - rewrite H0; case (reduce t0); intros; auto. -Qed. +Fixpoint fusion (t1 t2 : term) (k1 k2 : int) : term := + match t1 with + | [v1] * Tint x1 + l1 => + (fix fusion_t1 t2 : term := + match t2 with + | [v2] * Tint x2 + l2 => + match N.compare v1 v2 with + | Eq => + 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 + | _ => t1 * Tint k1 + t2 * Tint k2 (* shouldn't happen *) + end) t2 + | 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 (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_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 (mult_comm k1), (mult_comm k2) in H0. + 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. +Qed. + +(** Term normalization. + + Precondition: all [Tmult] should be on at least one [Tint]. + Postcondition: a normalized equivalent term (see below). +*) -(* \subsubsection{Fusions} - \paragraph{Fusion de deux équations} *) -(* On donne une somme de deux équations qui sont supposées normalisées. - Cette fonction prend une trace de fusion en argument et transforme - le terme en une équation normalisée. C'est une version très simplifiée - du moteur de réécriture [rewrite]. *) - -Fixpoint fusion (trace : list t_fusion) (t : term) {struct trace} : term := - match trace with - | nil => reduce t - | step :: trace' => - match step with - | F_equal => apply_right (fusion trace') (T_OMEGA10 t) - | F_cancel => fusion trace' (Tred_factor5 (T_OMEGA10 t)) - | F_left => apply_right (fusion trace') (T_OMEGA11 t) - | F_right => apply_right (fusion trace') (T_OMEGA12 t) - end +Fixpoint normalize t := + match t with + | 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_mult (normalize t) (-(1)) + | (t - t')%term => fusion (normalize t) (normalize t') 1 (-(1)) + | (Tint k * t)%term | (t * Tint k)%term => + if k =? 0 then Tint 0 else scalar_mult (normalize t) k + | (t1 * t2)%term => (t1 * t2)%term (* shouldn't happen *) end. -Theorem fusion_stable : forall trace : list t_fusion, term_stable (fusion trace). +Theorem normalize_stable : term_stable normalize. Proof. - simple induction trace; simpl; - [ exact reduce_stable - | intros stp l H; case stp; - [ apply compose_term_stable; - [ apply apply_right_stable; assumption | exact T_OMEGA10_stable ] - | unfold term_stable; intros e t1; rewrite T_OMEGA10_stable; - rewrite Tred_factor5_stable; apply H - | apply compose_term_stable; - [ apply apply_right_stable; assumption | exact T_OMEGA11_stable ] - | apply compose_term_stable; - [ apply apply_right_stable; assumption | exact T_OMEGA12_stable ] ] ]. + intros e t. + induction t; simpl; Simplify; simpl; + 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. + - rewrite <- opp_eq_mult_neg_1. now f_equal. Qed. -(* \paragraph{Fusion de deux équations dont une sans coefficient} *) - -Definition fusion_right (trace : list t_fusion) (t : term) : term := - match trace with - | nil => reduce t (* Il faut mettre un compute *) - | step :: trace' => - match step with - | F_equal => apply_right (fusion trace') (T_OMEGA15 t) - | F_cancel => fusion trace' (Tred_factor5 (T_OMEGA15 t)) - | F_left => apply_right (fusion trace') (Tplus_assoc_r t) - | F_right => apply_right (fusion trace') (T_OMEGA12 t) - end - end. +(** ** Normalization of a proposition. -(* \paragraph{Fusion avec annihilation} *) -(* Normalement le résultat est une constante *) + The only basic facts left after normalization are + [0 = ...] or [0 <> ...] or [0 <= ...]. + When a fact is in negative position, we factorize a [Tnot] + out of it, and normalize the reversed fact inside. -Fixpoint fusion_cancel (trace : nat) (t : term) {struct trace} : term := - match trace with - | O => reduce t - | S trace' => fusion_cancel trace' (T_OMEGA13 t) - end. + /!\ Here again, do not change this code without corresponding + modifications in [refl_omega.ml]. +*) -Theorem fusion_cancel_stable : forall t : nat, term_stable (fusion_cancel t). +Fixpoint normalize_prop (negated:bool)(p:proposition) := + match p with + | EqTerm t1 t2 => + if negated then Tnot (NeqTerm (Tint 0) (normalize (t1-t2))) + else EqTerm (Tint 0) (normalize (t1-t2)) + | NeqTerm t1 t2 => + if negated then Tnot (EqTerm (Tint 0) (normalize (t1-t2))) + else NeqTerm (Tint 0) (normalize (t1-t2)) + | LeqTerm t1 t2 => + if negated then Tnot (LeqTerm (Tint 0) (normalize (t1-t2+Tint (-(1))))) + else LeqTerm (Tint 0) (normalize (t2-t1)) + | GeqTerm t1 t2 => + if negated then Tnot (LeqTerm (Tint 0) (normalize (t2-t1+Tint (-(1))))) + else LeqTerm (Tint 0) (normalize (t1-t2)) + | LtTerm t1 t2 => + if negated then Tnot (LeqTerm (Tint 0) (normalize (t1-t2))) + else LeqTerm (Tint 0) (normalize (t2-t1+Tint (-(1)))) + | GtTerm t1 t2 => + if negated then Tnot (LeqTerm (Tint 0) (normalize (t2-t1))) + else LeqTerm (Tint 0) (normalize (t1-t2+Tint (-(1)))) + | Tnot p => Tnot (normalize_prop (negb negated) p) + | Tor p p' => Tor (normalize_prop negated p) (normalize_prop negated p') + | Tand p p' => Tand (normalize_prop negated p) (normalize_prop negated p') + | Timp p p' => Timp (normalize_prop (negb negated) p) + (normalize_prop negated p') + | Tprop _ | TrueTerm | FalseTerm => p + end. + +Definition normalize_hyps := List.map (normalize_prop false). + +Local Ltac simp := cbn -[normalize]. + +Theorem normalize_prop_valid b e ep p : + interp_prop e ep (normalize_prop b p) <-> interp_prop e ep p. +Proof. + revert b. + induction p; intros; simp; try tauto. + - destruct b; simp; + rewrite <- ?normalize_stable; simpl; rewrite ?minus_def. + + 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. + + 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. + + 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. + 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. + now rewrite <- le_left. + + symmetry. apply lt_left. + - now rewrite IHp. + - now rewrite IHp1, IHp2. + - now rewrite IHp1, IHp2. + - now rewrite IHp1, IHp2. +Qed. + +Theorem normalize_hyps_valid : valid_hyps normalize_hyps. +Proof. + intros e ep l. induction l; simpl; intuition. + now rewrite normalize_prop_valid. +Qed. + +Theorem normalize_hyps_goal (ep : list Prop) (env : list int) (l : hyps) : + interp_goal ep env (normalize_hyps l) -> interp_goal ep env l. Proof. - unfold term_stable, fusion_cancel; intros trace e; elim trace; - [ exact (reduce_stable e) - | intros n H t; elim H; exact (T_OMEGA13_stable e t) ]. + intros; apply valid_goal with (2 := H); apply normalize_hyps_valid. Qed. -(* \subsubsection{Opérations affines sur une équation} *) -(* \paragraph{Multiplication scalaire et somme d'une constante} *) - -Fixpoint scalar_norm_add (trace : nat) (t : term) {struct trace} : term := - match trace with - | O => reduce t - | S trace' => apply_right (scalar_norm_add trace') (T_OMEGA11 t) - end. +(** ** A simple decidability checker -Theorem scalar_norm_add_stable : - forall t : nat, term_stable (scalar_norm_add t). -Proof. - unfold term_stable, scalar_norm_add; intros trace; elim trace; - [ exact reduce_stable - | intros n H e t; elim apply_right_stable; - [ exact (T_OMEGA11_stable e t) | exact H ] ]. -Qed. + For us, everything is considered decidable except + propositional atoms [Tprop _]. *) -(* \paragraph{Multiplication scalaire} *) -Fixpoint scalar_norm (trace : nat) (t : term) {struct trace} : term := - match trace with - | O => reduce t - | S trace' => apply_right (scalar_norm trace') (T_OMEGA16 t) +Fixpoint decidability (p : proposition) : bool := + match p with + | Tnot t => decidability t + | Tand t1 t2 => decidability t1 && decidability t2 + | Timp t1 t2 => decidability t1 && decidability t2 + | Tor t1 t2 => decidability t1 && decidability t2 + | Tprop _ => false + | _ => true end. -Theorem scalar_norm_stable : forall t : nat, term_stable (scalar_norm t). -Proof. - unfold term_stable, scalar_norm; intros trace; elim trace; - [ exact reduce_stable - | intros n H e t; elim apply_right_stable; - [ exact (T_OMEGA16_stable e t) | exact H ] ]. -Qed. - -(* \paragraph{Somme d'une constante} *) -Fixpoint add_norm (trace : nat) (t : term) {struct trace} : term := - match trace with - | O => reduce t - | S trace' => apply_right (add_norm trace') (Tplus_assoc_r t) - end. +Theorem decidable_correct : + forall (ep : list Prop) (e : list int) (p : proposition), + decidability p = true -> decidable (interp_prop ep e p). +Proof. + induction p; simpl; intros Hp; try destruct (andb_prop _ _ Hp). + - apply dec_eq. + - apply dec_ne. + - apply dec_le. + - apply dec_ge. + - apply dec_gt. + - apply dec_lt. + - left; auto. + - right; unfold not; auto. + - apply dec_not; auto. + - apply dec_or; auto. + - apply dec_and; auto. + - apply dec_imp; auto. + - discriminate. +Qed. + +(** ** Omega steps + + The following inductive type describes steps as they can be + found in the trace coming from the decision procedure Omega. + We consider here only normalized equations [0=...], disequations + [0<>...] or inequations [0<=...]. + + First, the final steps leading to a contradiction: + - [O_BAD_CONSTANT i] : hypothesis i has a constant body + and this constant is not compatible with the kind of i. + - [O_NOT_EXACT_DIVIDE i k] : + equation i can be factorized as some [k*t+c] with [0<c<k]. + + Now, the intermediate steps leading to a new hypothesis: + - [O_DIVIDE i k cont] : + the body of hypothesis i could be factorized as [k*t+c] + with either [k<>0] and [c=0] for a (dis)equation, or + [0<k] and [c<k] for an inequation. We change in-place the + body of i for [t]. + - [O_SUM k1 i1 k2 i2 cont] : creates a new hypothesis whose + kind depends on the kind of hypotheses [i1] and [i2], and + whose body is [k1*body(i1) + k2*body(i2)]. Depending of the + situation, [k1] or [k2] might have to be positive or non-nul. + - [O_MERGE_EQ i j cont] : + inequations i and j have opposite bodies, we add an equation + with one these bodies. + - [O_SPLIT_INEQ i cont1 cont2] : + disequation i is split into a disjonction of inequations. +*) -Theorem add_norm_stable : forall t : nat, term_stable (add_norm t). -Proof. - unfold term_stable, add_norm; intros trace; elim trace; - [ exact reduce_stable - | intros n H e t; elim apply_right_stable; - [ exact (Tplus_assoc_r_stable e t) | exact H ] ]. -Qed. +Definition idx := nat. (** Index of an hypothesis in the list *) -(* \subsection{La fonction de normalisation des termes (moteur de réécriture)} *) +Inductive t_omega : Set := + | O_BAD_CONSTANT : idx -> t_omega + | O_NOT_EXACT_DIVIDE : idx -> int -> t_omega + | O_DIVIDE : idx -> int -> t_omega -> t_omega + | O_SUM : int -> idx -> int -> idx -> t_omega -> t_omega + | O_MERGE_EQ : idx -> idx -> t_omega -> t_omega + | O_SPLIT_INEQ : idx -> t_omega -> t_omega -> t_omega. -Fixpoint t_rewrite (s : step) : term -> term := - match s with - | C_DO_BOTH s1 s2 => apply_both (t_rewrite s1) (t_rewrite s2) - | C_LEFT s => apply_left (t_rewrite s) - | C_RIGHT s => apply_right (t_rewrite s) - | C_SEQ s1 s2 => fun t : term => t_rewrite s2 (t_rewrite s1 t) - | C_NOP => fun t : term => t - | C_OPP_PLUS => Topp_plus - | C_OPP_OPP => Topp_opp - | C_OPP_MULT_R => Topp_mult_r - | C_OPP_ONE => Topp_one - | C_REDUCE => reduce - | C_MULT_PLUS_DISTR => Tmult_plus_distr - | C_MULT_OPP_LEFT => Tmult_opp_left - | C_MULT_ASSOC_R => Tmult_assoc_r - | C_PLUS_ASSOC_R => Tplus_assoc_r - | C_PLUS_ASSOC_L => Tplus_assoc_l - | C_PLUS_PERMUTE => Tplus_permute - | C_PLUS_COMM => Tplus_comm - | C_RED0 => Tred_factor0 - | C_RED1 => Tred_factor1 - | C_RED2 => Tred_factor2 - | C_RED3 => Tred_factor3 - | C_RED4 => Tred_factor4 - | C_RED5 => Tred_factor5 - | C_RED6 => Tred_factor6 - | C_MULT_ASSOC_REDUCED => Tmult_assoc_reduced - | C_MINUS => Tminus_def - | C_MULT_COMM => Tmult_comm - end. +(** ** Actual resolution steps of an omega normalized goal *) -Theorem t_rewrite_stable : forall s : step, term_stable (t_rewrite s). -Proof. - simple induction s; simpl; - [ intros; apply apply_both_stable; auto - | intros; apply apply_left_stable; auto - | intros; apply apply_right_stable; auto - | unfold term_stable; intros; elim H0; apply H - | unfold term_stable; auto - | exact Topp_plus_stable - | exact Topp_opp_stable - | exact Topp_mult_r_stable - | exact Topp_one_stable - | exact reduce_stable - | exact Tmult_plus_distr_stable - | exact Tmult_opp_left_stable - | exact Tmult_assoc_r_stable - | exact Tplus_assoc_r_stable - | exact Tplus_assoc_l_stable - | exact Tplus_permute_stable - | exact Tplus_comm_stable - | exact Tred_factor0_stable - | exact Tred_factor1_stable - | exact Tred_factor2_stable - | exact Tred_factor3_stable - | exact Tred_factor4_stable - | exact Tred_factor5_stable - | exact Tred_factor6_stable - | exact Tmult_assoc_reduced_stable - | exact Tminus_def_stable - | exact Tmult_comm_stable ]. -Qed. +(** First, the final steps, leading to a contradiction *) -(* \subsection{tactiques de résolution d'un but omega normalisé} - Trace de la procédure -\subsubsection{Tactiques générant une contradiction} -\paragraph{[O_CONSTANT_NOT_NUL]} *) +(** [O_BAD_CONSTANT] *) -Definition constant_not_nul (i : nat) (h : hyps) := +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 + | 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. -Theorem constant_not_nul_valid : - forall i : nat, valid_hyps (constant_not_nul i). +Theorem bad_constant_valid i : valid_hyps (bad_constant i). Proof. - unfold valid_hyps, constant_not_nul; intros i ep e lp H. + unfold valid_hyps, bad_constant; intros ep e lp H. generalize (nth_valid ep e i lp H); Simplify. + rewrite le_lt_iff. intuition. Qed. -(* \paragraph{[O_CONSTANT_NEG]} *) +(** [O_NOT_EXACT_DIVIDE] *) -Definition constant_neg (i : nat) (h : hyps) := - match nth_hyps i h with - | LeqTerm (Tint Nul) (Tint Neg) => - if bgt Nul Neg then absurd else h - | _ => h - end. - -Theorem constant_neg_valid : forall i : nat, valid_hyps (constant_neg i). -Proof. - unfold valid_hyps, constant_neg; intros; - generalize (nth_valid ep e i lp); Simplify; simpl. - rewrite gt_lt_iff in H0; rewrite le_lt_iff; intuition. -Qed. - -(* \paragraph{[NOT_EXACT_DIVIDE]} *) -Definition not_exact_divide (k1 k2 : int) (body : term) - (t i : nat) (l : hyps) := +Definition not_exact_divide (i : nat) (k : int) (l : hyps) := match nth_hyps i l with | EqTerm (Tint Nul) b => - if beq Nul 0 && - eq_term (scalar_norm_add t (body * Tint k1 + Tint k2)%term) b && - bgt k2 0 && - bgt k1 k2 - then absurd + match scalar_div b k with + | Some (body,c) => + if (Nul =? 0) && (0 <? c) && (c <? k) then absurd else l + | None => l + end | _ => l end. -Theorem not_exact_divide_valid : - forall (k1 k2 : int) (body : term) (t0 i : nat), - valid_hyps (not_exact_divide k1 k2 body t0 i). +Theorem not_exact_divide_valid i k : + valid_hyps (not_exact_divide i k). Proof. - unfold valid_hyps, not_exact_divide; intros; - generalize (nth_valid ep e i lp); Simplify. - rewrite (scalar_norm_add_stable t0 e), <-H1. - do 2 rewrite <- scalar_norm_add_stable; simpl in *; intros. - absurd (interp_term e body * k1 + k2 = 0); - [ now apply OMEGA4 | symmetry; auto ]. + unfold valid_hyps, not_exact_divide; intros. + generalize (nth_valid ep e i lp). + destruct (nth_hyps i lp); simpl; auto. + destruct t0; auto. + destruct (scalar_div t1 k) as [(body,c)|] eqn:E; auto. + Simplify. + assert (k <> 0). + { intro. apply (lt_not_eq 0 k); eauto using lt_trans. } + apply (scalar_div_stable e) in E; auto. simpl in E. + intros H'; rewrite <- H' in E; auto. + exfalso. revert E. now apply OMEGA4. Qed. -(* \paragraph{[O_CONTRADICTION]} *) +(** Now, the steps generating a new equation. *) -Definition contradiction (t i j : nat) (l : hyps) := - match nth_hyps i l with - | LeqTerm (Tint Nul) b1 => - match nth_hyps j l with - | LeqTerm (Tint Nul') b2 => - match fusion_cancel t (b1 + b2)%term with - | Tint k => if beq Nul 0 && beq Nul' 0 && bgt 0 k - then absurd - else l - | _ => l - end - | _ => l - end - | _ => l - end. - -Theorem contradiction_valid : - forall t i j : nat, valid_hyps (contradiction t i j). -Proof. - unfold valid_hyps, contradiction; intros t i j ep e l H; - generalize (nth_valid _ _ i _ H); generalize (nth_valid _ _ j _ H); - case (nth_hyps i l); auto; intros t1 t2; case t1; - auto; case (nth_hyps j l); - auto; intros t3 t4; case t3; auto; - simpl; intros z z' H1 H2; - generalize (eq_refl (interp_term e (fusion_cancel t (t2 + t4)%term))); - pattern (fusion_cancel t (t2 + t4)%term) at 2 3; - case (fusion_cancel t (t2 + t4)%term); simpl; - auto; intro k; elim (fusion_cancel_stable t); simpl. - Simplify; intro H3. - generalize (OMEGA2 _ _ H2 H1); rewrite H3. - rewrite gt_lt_iff in H0; rewrite le_lt_iff; intuition. -Qed. +(** [O_DIVIDE] *) -(* \paragraph{[O_NEGATE_CONTRADICT]} *) - -Definition negate_contradict (i1 i2 : nat) (h : hyps) := - match nth_hyps i1 h with - | EqTerm (Tint Nul) b1 => - match nth_hyps i2 h with - | NeqTerm (Tint Nul') b2 => - if beq Nul 0 && beq Nul' 0 && eq_term b1 b2 - then absurd - else h - | _ => h - end - | NeqTerm (Tint Nul) b1 => - match nth_hyps i2 h with - | EqTerm (Tint Nul') b2 => - if beq Nul 0 && beq Nul' 0 && eq_term b1 b2 - then absurd - else h - | _ => h - end - | _ => h - end. - -Definition negate_contradict_inv (t i1 i2 : nat) (h : hyps) := - match nth_hyps i1 h with - | EqTerm (Tint Nul) b1 => - match nth_hyps i2 h with - | NeqTerm (Tint Nul') b2 => - if beq Nul 0 && beq Nul' 0 && - eq_term b1 (scalar_norm t (b2 * Tint (-(1)))%term) - then absurd - else h - | _ => h - end - | NeqTerm (Tint Nul) b1 => - match nth_hyps i2 h with - | EqTerm (Tint Nul') b2 => - if beq Nul 0 && beq Nul' 0 && - eq_term b1 (scalar_norm t (b2 * Tint (-(1)))%term) - then absurd - else h - | _ => h - end - | _ => h +Definition divide (k : int) (prop : proposition) := + match prop with + | EqTerm (Tint o) b => + match scalar_div b k with + | Some (body,c) => + if (o =? 0) && (c =? 0) && negb (k =? 0) + then EqTerm (Tint 0) body + else TrueTerm + | None => TrueTerm + end + | NeqTerm (Tint o) b => + match scalar_div b k with + | Some (body,c) => + if (o =? 0) && (c =? 0) && negb (k =? 0) + then NeqTerm (Tint 0) body + else TrueTerm + | None => TrueTerm + end + | LeqTerm (Tint o) b => + match scalar_div b k with + | Some (body,c) => + if (o =? 0) && (0 <? k) && (c <? k) + then LeqTerm (Tint 0) body + else prop + | None => prop + end + | _ => TrueTerm end. -Theorem negate_contradict_valid : - forall i j : nat, valid_hyps (negate_contradict i j). -Proof. - unfold valid_hyps, negate_contradict; intros i j ep e l H; - generalize (nth_valid _ _ i _ H); generalize (nth_valid _ _ j _ H); - case (nth_hyps i l); auto; intros t1 t2; case t1; - auto; intros z; auto; case (nth_hyps j l); - auto; intros t3 t4; case t3; auto; intros z'; - auto; simpl; intros H1 H2; Simplify. -Qed. - -Theorem negate_contradict_inv_valid : - forall t i j : nat, valid_hyps (negate_contradict_inv t i j). +Theorem divide_valid k : valid1 (divide k). Proof. - unfold valid_hyps, negate_contradict_inv; intros t i j ep e l H; - generalize (nth_valid _ _ i _ H); generalize (nth_valid _ _ j _ H); - case (nth_hyps i l); auto; intros t1 t2; case t1; - auto; intros z; auto; case (nth_hyps j l); - auto; intros t3 t4; case t3; auto; intros z'; - auto; simpl; intros H1 H2; Simplify; - [ - rewrite <- scalar_norm_stable in H2; simpl in *; - elim (mult_integral (interp_term e t4) (-(1))); intuition; - elim minus_one_neq_zero; auto - | - elim H2; clear H2; - rewrite <- scalar_norm_stable; simpl in *; - now rewrite <- H1, mult_0_l - ]. + unfold valid1, divide; intros ep e p; + destruct p; simpl; auto; + destruct t0; simpl; auto; + destruct scalar_div as [(body,c)|] eqn:E; simpl; Simplify; auto. + - apply (scalar_div_stable e) in E; auto. simpl in E. + intros H'; rewrite <- H' in E. rewrite plus_0_r in E. + apply mult_integral in E. intuition. + - apply (scalar_div_stable e) in E; auto. simpl in E. + intros H' H''. now rewrite <- H'', mult_0_l, plus_0_l in E. + - assert (k <> 0). + { intro. apply (lt_not_eq 0 k); eauto using lt_trans. } + apply (scalar_div_stable e) in E; auto. simpl in E. rewrite <- E. + intro H'. now apply mult_le_approx with (3 := H'). Qed. -(* \subsubsection{Tactiques générant une nouvelle équation} *) -(* \paragraph{[O_SUM]} - C'est une oper2 valide mais elle traite plusieurs cas à la fois (suivant - les opérateurs de comparaison des deux arguments) d'où une - preuve un peu compliquée. On utilise quelques lemmes qui sont des - généralisations des théorèmes utilisés par OMEGA. *) +(** [O_SUM]. Invariant: [k1] and [k2] non-nul. *) -Definition sum (k1 k2 : int) (trace : list t_fusion) - (prop1 prop2 : proposition) := +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 - then EqTerm (Tint 0) (fusion trace (b1 * Tint k1 + b2 * Tint k2)%term) + | EqTerm (Tint o') b2 => + if (o =? 0) && (o' =? 0) + then EqTerm (Tint 0) (fusion b1 b2 k1 k2) + else TrueTerm + | LeqTerm (Tint o') b2 => + if (o =? 0) && (o' =? 0) && (0 <? k2) + then LeqTerm (Tint 0) (fusion b1 b2 k1 k2) else TrueTerm - | LeqTerm (Tint Null') b2 => - if beq Null 0 && beq Null' 0 && bgt k2 0 - then LeqTerm (Tint 0) - (fusion trace (b1 * Tint k1 + b2 * Tint k2)%term) + | 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 - LeqTerm (Tint 0) - (fusion trace (b1 * Tint k1 + b2 * Tint k2)%term) + | 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 - then LeqTerm (Tint 0) - (fusion trace (b1 * Tint k1 + b2 * Tint k2)%term) + | 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)) - then NeqTerm (Tint 0) - (fusion trace (b1 * Tint k1 + b2 * Tint k2)%term) + | EqTerm (Tint o') b2 => + if (o =? 0) && (o' =? 0) && negb (k1 =? 0) + then NeqTerm (Tint 0) (fusion b1 b2 k1 k2) else TrueTerm | _ => TrueTerm end | _ => TrueTerm end. - Theorem sum_valid : - forall (k1 k2 : int) (t : list t_fusion), valid2 (sum k1 k2 t). + forall (k1 k2 : int), valid2 (sum k1 k2). Proof. unfold valid2; intros k1 k2 t ep e p1 p2; unfold sum; - Simplify; simpl; auto; try elim (fusion_stable t); - simpl; intros; - [ apply sum1; assumption - | apply sum2; try assumption; apply sum4; assumption - | rewrite plus_comm; apply sum2; try assumption; apply sum4; assumption - | apply sum3; try assumption; apply sum4; assumption - | apply sum5; auto ]. -Qed. - -(* \paragraph{[O_EXACT_DIVIDE]} - c'est une oper1 valide mais on préfère une substitution a ce point la *) - -Definition exact_divide (k : int) (body : term) (t : nat) - (prop : proposition) := - match prop with - | EqTerm (Tint Null) b => - if beq Null 0 && - eq_term (scalar_norm t (body * Tint k)%term) b && - negb (beq k 0) - then EqTerm (Tint 0) body - else TrueTerm - | NeqTerm (Tint Null) b => - if beq Null 0 && - eq_term (scalar_norm t (body * Tint k)%term) b && - negb (beq k 0) - then NeqTerm (Tint 0) body - else TrueTerm - | _ => TrueTerm - end. - -Theorem exact_divide_valid : - forall (k : int) (t : term) (n : nat), valid1 (exact_divide k t n). -Proof. - unfold valid1, exact_divide; intros k1 k2 t ep e p1; - Simplify; simpl; auto; subst; - rewrite <- scalar_norm_stable; simpl; intros; - [ destruct (mult_integral _ _ (eq_sym H0)); intuition - | contradict H0; rewrite <- H0, mult_0_l; auto - ]. + 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] *) -(* \paragraph{[O_DIV_APPROX]} - La preuve reprend le schéma de la précédente mais on - est sur une opération de type valid1 et non sur une opération terminale. *) - -Definition divide_and_approx (k1 k2 : int) (body : term) - (t : nat) (prop : proposition) := - match prop with - | LeqTerm (Tint Null) b => - if beq Null 0 && - eq_term (scalar_norm_add t (body * Tint k1 + Tint k2)%term) b && - bgt k1 0 && - bgt k1 k2 - then LeqTerm (Tint 0) body - else prop - | _ => prop - end. - -Theorem divide_and_approx_valid : - forall (k1 k2 : int) (body : term) (t : nat), - valid1 (divide_and_approx k1 k2 body t). -Proof. - unfold valid1, divide_and_approx; intros k1 k2 body t ep e p1; - Simplify; simpl; auto; subst; - elim (scalar_norm_add_stable t e); simpl. - intro H2; apply mult_le_approx with (3 := H2); assumption. -Qed. - -(* \paragraph{[MERGE_EQ]} *) - -Definition merge_eq (t : nat) (prop1 prop2 : proposition) := +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 t (b2 * Tint (-(1)))%term) + | LeqTerm (Tint o') b2 => + if (o =? 0) && (o' =? 0) && + (b1 =? scalar_mult b2 (-(1)))%term then EqTerm (Tint 0) b1 else TrueTerm | _ => TrueTerm @@ -2370,680 +1603,153 @@ Definition merge_eq (t : nat) (prop1 prop2 : proposition) := | _ => TrueTerm end. -Theorem merge_eq_valid : forall n : nat, valid2 (merge_eq n). -Proof. - unfold valid2, merge_eq; intros n ep e p1 p2; Simplify; simpl; - auto; elim (scalar_norm_stable n e); simpl; - intros; symmetry ; apply OMEGA8 with (2 := H0); - [ assumption | elim opp_eq_mult_neg_1; trivial ]. -Qed. - - - -(* \paragraph{[O_CONSTANT_NUL]} *) - -Definition constant_nul (i : nat) (h : hyps) := - match nth_hyps i h with - | NeqTerm (Tint Null) (Tint Null') => - if beq Null Null' then absurd else h - | _ => h - end. - -Theorem constant_nul_valid : forall i : nat, valid_hyps (constant_nul i). -Proof. - unfold valid_hyps, constant_nul; intros; - generalize (nth_valid ep e i lp); Simplify; simpl; - intro H1; absurd (0 = 0); intuition. -Qed. - -(* \paragraph{[O_STATE]} *) - -Definition state (m : int) (s : step) (prop1 prop2 : proposition) := - match prop1 with - | EqTerm (Tint Null) b1 => - match prop2 with - | EqTerm b2 b3 => - if beq Null 0 - then EqTerm (Tint 0) (t_rewrite s (b1 + (- b3 + b2) * Tint m)%term) - else TrueTerm - | _ => TrueTerm - end - | _ => TrueTerm - end. - -Theorem state_valid : forall (m : int) (s : step), valid2 (state m s). +Theorem merge_eq_valid : valid2 merge_eq. Proof. - unfold valid2; intros m s ep e p1 p2; unfold state; Simplify; - simpl; auto; elim (t_rewrite_stable s e); simpl; - intros H1 H2; elim H1. - now rewrite H2, plus_opp_l, plus_0_l, mult_0_l. + unfold valid2, merge_eq; intros ep e p1 p2; Simplify; simpl; auto. + rewrite scalar_mult_stable. simpl. + intros; symmetry ; apply OMEGA8 with (2 := H0). + - assumption. + - elim opp_eq_mult_neg_1; trivial. Qed. -(* \subsubsection{Tactiques générant plusieurs but} - \paragraph{[O_SPLIT_INEQ]} - La seule pour le moment (tant que la normalisation n'est pas réfléchie). *) +(** [O_SPLIT_INEQ] (only step to produce two subgoals). *) -Definition split_ineq (i t : nat) (f1 f2 : hyps -> lhyps) - (l : hyps) := +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 t (b1 + Tint (-(1)))%term) :: l) ++ - f2 - (LeqTerm (Tint 0) - (scalar_norm_add t (b1 * Tint (-(1)) + Tint (-(1)))%term) :: l) - else l :: nil + | 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. Theorem split_ineq_valid : - forall (i t : nat) (f1 f2 : hyps -> lhyps), + forall (i : nat) (f1 f2 : hyps -> lhyps), valid_list_hyps f1 -> - valid_list_hyps f2 -> valid_list_hyps (split_ineq i t f1 f2). + valid_list_hyps f2 -> valid_list_hyps (split_ineq i f1 f2). Proof. - unfold valid_list_hyps, split_ineq; intros i t f1 f2 H1 H2 ep e lp H; + unfold valid_list_hyps, split_ineq; intros i f1 f2 H1 H2 ep e lp H; generalize (nth_valid _ _ i _ H); case (nth_hyps i lp); simpl; auto; intros t1 t2; case t1; simpl; auto; intros z; simpl; auto; intro H3. Simplify. - apply append_valid; elim (OMEGA19 (interp_term e t2)); - [ intro H4; left; apply H1; simpl; elim (add_norm_stable t); - simpl; auto - | intro H4; right; apply H2; simpl; elim (scalar_norm_add_stable t); - simpl; auto - | generalize H3; unfold not; intros E1 E2; apply E1; - symmetry ; trivial ]. + apply append_valid; elim (OMEGA19 (interp_term e t2)). + - intro H4; left; apply H1; simpl; rewrite scalar_add_stable; + simpl; auto. + - intro H4; right; apply H2; simpl; rewrite scalar_mult_add_stable; + simpl; auto. + - generalize H3; unfold not; intros E1 E2; apply E1; + symmetry ; trivial. Qed. +(** ** Replaying the resolution trace *) -(* \subsection{La fonction de rejeu de la trace} *) - -Fixpoint execute_omega (t : t_omega) (l : hyps) {struct t} : lhyps := +Fixpoint execute_omega (t : t_omega) (l : hyps) : lhyps := match t with - | O_CONSTANT_NOT_NUL n => singleton (constant_not_nul n l) - | O_CONSTANT_NEG n => singleton (constant_neg n l) - | O_DIV_APPROX k1 k2 body t cont n => - execute_omega cont (apply_oper_1 n (divide_and_approx k1 k2 body t) l) - | O_NOT_EXACT_DIVIDE k1 k2 body t i => - singleton (not_exact_divide k1 k2 body t i l) - | O_EXACT_DIVIDE k body t cont n => - execute_omega cont (apply_oper_1 n (exact_divide k body t) l) - | O_SUM k1 i1 k2 i2 t cont => - execute_omega cont (apply_oper_2 i1 i2 (sum k1 k2 t) l) - | O_CONTRADICTION t i j => singleton (contradiction t i j l) - | O_MERGE_EQ t i1 i2 cont => - execute_omega cont (apply_oper_2 i1 i2 (merge_eq t) l) - | O_SPLIT_INEQ t i cont1 cont2 => - split_ineq i t (execute_omega cont1) (execute_omega cont2) l - | O_CONSTANT_NUL i => singleton (constant_nul i l) - | O_NEGATE_CONTRADICT i j => singleton (negate_contradict i j l) - | O_NEGATE_CONTRADICT_INV t i j => - singleton (negate_contradict_inv t i j l) - | O_STATE m s i1 i2 cont => - execute_omega cont (apply_oper_2 i1 i2 (state m s) l) + | O_BAD_CONSTANT i => singleton (bad_constant i l) + | O_NOT_EXACT_DIVIDE i k => singleton (not_exact_divide i k l) + | O_DIVIDE i k cont => + execute_omega cont (apply_oper_1 i (divide k) l) + | O_SUM k1 i1 k2 i2 cont => + execute_omega cont (apply_oper_2 i1 i2 (sum k1 k2) l) + | O_MERGE_EQ i1 i2 cont => + execute_omega cont (apply_oper_2 i1 i2 merge_eq l) + | O_SPLIT_INEQ i cont1 cont2 => + split_ineq i (execute_omega cont1) (execute_omega cont2) l end. Theorem omega_valid : forall tr : t_omega, valid_list_hyps (execute_omega tr). Proof. - simple induction tr; simpl; - [ unfold valid_list_hyps; simpl; intros; left; - apply (constant_not_nul_valid n ep e lp H) - | unfold valid_list_hyps; simpl; intros; left; - apply (constant_neg_valid n ep e lp H) - | unfold valid_list_hyps, valid_hyps; - intros k1 k2 body n t' Ht' m ep e lp H; apply Ht'; - apply - (apply_oper_1_valid m (divide_and_approx k1 k2 body n) - (divide_and_approx_valid k1 k2 body n) ep e lp H) - | unfold valid_list_hyps; simpl; intros; left; - apply (not_exact_divide_valid _ _ _ _ _ ep e lp H) - | unfold valid_list_hyps, valid_hyps; - intros k body n t' Ht' m ep e lp H; apply Ht'; + simple induction tr; unfold valid_list_hyps, valid_hyps; simpl. + - intros; left; now apply bad_constant_valid. + - intros; left; now apply not_exact_divide_valid. + - intros m k t' Ht' ep e lp H; apply Ht'; apply - (apply_oper_1_valid m (exact_divide k body n) - (exact_divide_valid k body n) ep e lp H) - | unfold valid_list_hyps, valid_hyps; - intros k1 i1 k2 i2 trace t' Ht' ep e lp H; apply Ht'; + (apply_oper_1_valid m (divide k) + (divide_valid k) ep e lp H). + - intros k1 i1 k2 i2 t' Ht' ep e lp H; apply Ht'; apply - (apply_oper_2_valid i1 i2 (sum k1 k2 trace) (sum_valid k1 k2 trace) ep e - lp H) - | unfold valid_list_hyps; simpl; intros; left; - apply (contradiction_valid n n0 n1 ep e lp H) - | unfold valid_list_hyps, valid_hyps; - intros trace i1 i2 t' Ht' ep e lp H; apply Ht'; + (apply_oper_2_valid i1 i2 (sum k1 k2) (sum_valid k1 k2) ep e + lp H). + - intros i1 i2 t' Ht' ep e lp H; apply Ht'; apply - (apply_oper_2_valid i1 i2 (merge_eq trace) (merge_eq_valid trace) ep e - lp H) - | intros t' i k1 H1 k2 H2; unfold valid_list_hyps; simpl; - intros ep e lp H; + (apply_oper_2_valid i1 i2 merge_eq merge_eq_valid ep e + lp H). + - intros i k1 H1 k2 H2 ep e lp H; apply - (split_ineq_valid i t' (execute_omega k1) (execute_omega k2) H1 H2 ep e - lp H) - | unfold valid_list_hyps; simpl; intros i ep e lp H; left; - apply (constant_nul_valid i ep e lp H) - | unfold valid_list_hyps; simpl; intros i j ep e lp H; left; - apply (negate_contradict_valid i j ep e lp H) - | unfold valid_list_hyps; simpl; intros n i j ep e lp H; - left; apply (negate_contradict_inv_valid n i j ep e lp H) - | unfold valid_list_hyps, valid_hyps; - intros m s i1 i2 t' Ht' ep e lp H; apply Ht'; - apply (apply_oper_2_valid i1 i2 (state m s) (state_valid m s) ep e lp H) ]. -Qed. - - -(* \subsection{Les opérations globales sur le but} - \subsubsection{Normalisation} *) - -Definition move_right (s : step) (p : proposition) := - match p with - | EqTerm t1 t2 => EqTerm (Tint 0) (t_rewrite s (t1 + - t2)%term) - | LeqTerm t1 t2 => LeqTerm (Tint 0) (t_rewrite s (t2 + - t1)%term) - | GeqTerm t1 t2 => LeqTerm (Tint 0) (t_rewrite s (t1 + - t2)%term) - | LtTerm t1 t2 => LeqTerm (Tint 0) (t_rewrite s (t2 + Tint (-(1)) + - t1)%term) - | GtTerm t1 t2 => LeqTerm (Tint 0) (t_rewrite s (t1 + Tint (-(1)) + - t2)%term) - | NeqTerm t1 t2 => NeqTerm (Tint 0) (t_rewrite s (t1 + - t2)%term) - | p => p - end. - -Theorem move_right_valid : forall s : step, valid1 (move_right s). -Proof. - unfold valid1, move_right; intros s ep e p; Simplify; simpl; - elim (t_rewrite_stable s e); simpl; - [ symmetry ; apply egal_left; assumption - | intro; apply le_left; assumption - | intro; apply le_left; rewrite <- ge_le_iff; assumption - | intro; apply lt_left; rewrite <- gt_lt_iff; assumption - | intro; apply lt_left; assumption - | intro; apply ne_left_2; assumption ]. -Qed. - -Definition do_normalize (i : nat) (s : step) := apply_oper_1 i (move_right s). - -Theorem do_normalize_valid : - forall (i : nat) (s : step), valid_hyps (do_normalize i s). -Proof. - intros; unfold do_normalize; apply apply_oper_1_valid; - apply move_right_valid. -Qed. - -Fixpoint do_normalize_list (l : list step) (i : nat) - (h : hyps) {struct l} : hyps := - match l with - | s :: l' => do_normalize_list l' (S i) (do_normalize i s h) - | nil => h - end. - -Theorem do_normalize_list_valid : - forall (l : list step) (i : nat), valid_hyps (do_normalize_list l i). -Proof. - simple induction l; simpl; unfold valid_hyps; - [ auto - | intros a l' Hl' i ep e lp H; unfold valid_hyps in Hl'; apply Hl'; - apply (do_normalize_valid i a ep e lp); assumption ]. -Qed. - -Theorem normalize_goal : - forall (s : list step) (ep : list Prop) (env : list int) (l : hyps), - interp_goal ep env (do_normalize_list s 0 l) -> interp_goal ep env l. -Proof. - intros; apply valid_goal with (2 := H); apply do_normalize_list_valid. + (split_ineq_valid i (execute_omega k1) (execute_omega k2) H1 H2 ep e + lp H). Qed. -(* \subsubsection{Exécution de la trace} *) -Theorem execute_goal : - forall (tr : t_omega) (ep : list Prop) (env : list int) (l : hyps), - interp_list_goal ep env (execute_omega tr l) -> interp_goal ep env l. -Proof. - intros; apply (goal_valid (execute_omega tr) (omega_valid tr) ep env l H). -Qed. +(** ** Rules for decomposing the hypothesis + This type allows navigation in the logical constructors that + form the predicats of the hypothesis in order to decompose them. + This allows in particular to extract one hypothesis from a conjunction. + NB: negations are now silently traversed. *) -Theorem append_goal : - forall (ep : list Prop) (e : list int) (l1 l2 : lhyps), - interp_list_goal ep e l1 /\ interp_list_goal ep e l2 -> - interp_list_goal ep e (l1 ++ l2). -Proof. - intros ep e; simple induction l1; - [ simpl; intros l2 (H1, H2); assumption - | simpl; intros h1 t1 HR l2 ((H1, H2), H3); split; auto ]. -Qed. - -(* A simple decidability checker : if the proposition belongs to the - simple grammar describe below then it is decidable. Proof is by - induction and uses well known theorem about arithmetic and propositional - calculus *) - -Fixpoint decidability (p : proposition) : bool := - match p with - | EqTerm _ _ => true - | LeqTerm _ _ => true - | GeqTerm _ _ => true - | GtTerm _ _ => true - | LtTerm _ _ => true - | NeqTerm _ _ => true - | FalseTerm => true - | TrueTerm => true - | Tnot t => decidability t - | Tand t1 t2 => decidability t1 && decidability t2 - | Timp t1 t2 => decidability t1 && decidability t2 - | Tor t1 t2 => decidability t1 && decidability t2 - | Tprop _ => false - end. - -Theorem decidable_correct : - forall (ep : list Prop) (e : list int) (p : proposition), - decidability p = true -> decidable (interp_proposition ep e p). -Proof. - simple induction p; simpl; intros; - [ apply dec_eq - | apply dec_le - | left; auto - | right; unfold not; auto - | apply dec_not; auto - | apply dec_ge - | apply dec_gt - | apply dec_lt - | apply dec_ne - | apply dec_or; elim andb_prop with (1 := H1); auto - | apply dec_and; elim andb_prop with (1 := H1); auto - | apply dec_imp; elim andb_prop with (1 := H1); auto - | discriminate H ]. -Qed. - -(* An interpretation function for a complete goal with an explicit - conclusion. We use an intermediate fixpoint. *) - -Fixpoint interp_full_goal (envp : list Prop) (env : list int) - (c : proposition) (l : hyps) {struct l} : Prop := - match l with - | nil => interp_proposition envp env c - | p' :: l' => - interp_proposition envp env p' -> interp_full_goal envp env c l' - end. - -Definition interp_full (ep : list Prop) (e : list int) - (lc : hyps * proposition) : Prop := - match lc with - | (l, c) => interp_full_goal ep e c l - end. - -(* Relates the interpretation of a complete goal with the interpretation - of its hypothesis and conclusion *) - -Theorem interp_full_false : - forall (ep : list Prop) (e : list int) (l : hyps) (c : proposition), - (interp_hyps ep e l -> interp_proposition ep e c) -> interp_full ep e (l, c). -Proof. - simple induction l; unfold interp_full; simpl; - [ auto | intros a l1 H1 c H2 H3; apply H1; auto ]. -Qed. - -(* Push the conclusion in the list of hypothesis using a double negation - If the decidability cannot be "proven", then just forget about the - conclusion (equivalent of replacing it with false) *) - -Definition to_contradict (lc : hyps * proposition) := - match lc with - | (l, c) => if decidability c then Tnot c :: l else l - end. - -(* The previous operation is valid in the sense that the new list of - hypothesis implies the original goal *) - -Theorem to_contradict_valid : - forall (ep : list Prop) (e : list int) (lc : hyps * proposition), - interp_goal ep e (to_contradict lc) -> interp_full ep e lc. -Proof. - intros ep e lc; case lc; intros l c; simpl; - pattern (decidability c); apply bool_eq_ind; - [ simpl; intros H H1; apply interp_full_false; intros H2; - apply not_not; - [ apply decidable_correct; assumption - | unfold not at 1; intro H3; apply hyps_to_goal with (2 := H2); - auto ] - | intros H1 H2; apply interp_full_false; intro H3; - elim hyps_to_goal with (1 := H2); assumption ]. -Qed. - -(* [map_cons x l] adds [x] at the head of each list in [l] (which is a list - of lists *) - -Fixpoint map_cons (A : Set) (x : A) (l : list (list A)) {struct l} : - list (list A) := - match l with - | nil => nil - | l :: ll => (x :: l) :: map_cons A x ll - end. - -(* This function breaks up a list of hypothesis in a list of simpler - list of hypothesis that together implie the original one. The goal - of all this is to transform the goal in a list of solvable problems. - Note that : - - we need a way to drive the analysis as some hypotheis may not - require a split. - - this procedure must be perfectly mimicked by the ML part otherwise - hypothesis will get desynchronised and this will be a mess. - *) - -Fixpoint destructure_hyps (nn : nat) (ll : hyps) {struct nn} : lhyps := - match nn with - | O => ll :: nil - | S n => - match ll with - | nil => nil :: nil - | Tor p1 p2 :: l => - destructure_hyps n (p1 :: l) ++ destructure_hyps n (p2 :: l) - | Tand p1 p2 :: l => destructure_hyps n (p1 :: p2 :: l) - | Timp p1 p2 :: l => - if decidability p1 - then - destructure_hyps n (Tnot p1 :: l) ++ destructure_hyps n (p2 :: l) - else map_cons _ (Timp p1 p2) (destructure_hyps n l) - | Tnot p :: l => - match p with - | Tnot p1 => - if decidability p1 - then destructure_hyps n (p1 :: l) - else map_cons _ (Tnot (Tnot p1)) (destructure_hyps n l) - | Tor p1 p2 => destructure_hyps n (Tnot p1 :: Tnot p2 :: l) - | Tand p1 p2 => - if decidability p1 - then - destructure_hyps n (Tnot p1 :: l) ++ - destructure_hyps n (Tnot p2 :: l) - else map_cons _ (Tnot p) (destructure_hyps n l) - | _ => map_cons _ (Tnot p) (destructure_hyps n l) - end - | x :: l => map_cons _ x (destructure_hyps n l) - end - end. - -Theorem map_cons_val : - forall (ep : list Prop) (e : list int) (p : proposition) (l : lhyps), - interp_proposition ep e p -> - interp_list_hyps ep e l -> interp_list_hyps ep e (map_cons _ p l). -Proof. - simple induction l; simpl; [ auto | intros; elim H1; intro H2; auto ]. -Qed. - -Hint Resolve map_cons_val append_valid decidable_correct. - -Theorem destructure_hyps_valid : - forall n : nat, valid_list_hyps (destructure_hyps n). -Proof. - simple induction n; - [ unfold valid_list_hyps; simpl; auto - | unfold valid_list_hyps at 2; intros n1 H ep e lp; case lp; - [ simpl; auto - | intros p l; case p; - try - (simpl; intros; apply map_cons_val; simpl; elim H0; - auto); - [ intro p'; case p'; - try - (simpl; intros; apply map_cons_val; simpl; elim H0; - auto); - [ simpl; intros p1 (H1, H2); - pattern (decidability p1); apply bool_eq_ind; - intro H3; - [ apply H; simpl; split; - [ apply not_not; auto | assumption ] - | auto ] - | simpl; intros p1 p2 (H1, H2); apply H; simpl; - elim not_or with (1 := H1); auto - | simpl; intros p1 p2 (H1, H2); - pattern (decidability p1); apply bool_eq_ind; - intro H3; - [ apply append_valid; elim not_and with (2 := H1); - [ intro; left; apply H; simpl; auto - | intro; right; apply H; simpl; auto - | auto ] - | auto ] ] - | simpl; intros p1 p2 (H1, H2); apply append_valid; - (elim H1; intro H3; simpl; [ left | right ]); - apply H; simpl; auto - | simpl; intros; apply H; simpl; tauto - | simpl; intros p1 p2 (H1, H2); - pattern (decidability p1); apply bool_eq_ind; - intro H3; - [ apply append_valid; elim imp_simp with (2 := H1); - [ intro H4; left; simpl; apply H; simpl; auto - | intro H4; right; simpl; apply H; simpl; auto - | auto ] - | auto ] ] ] ]. -Qed. - -Definition prop_stable (f : proposition -> proposition) := - forall (ep : list Prop) (e : list int) (p : proposition), - interp_proposition ep e p <-> interp_proposition ep e (f p). - -Definition p_apply_left (f : proposition -> proposition) - (p : proposition) := - match p with - | Timp x y => Timp (f x) y - | Tor x y => Tor (f x) y - | Tand x y => Tand (f x) y - | Tnot x => Tnot (f x) - | x => x - end. - -Theorem p_apply_left_stable : - forall f : proposition -> proposition, - prop_stable f -> prop_stable (p_apply_left f). -Proof. - unfold prop_stable; intros f H ep e p; split; - (case p; simpl; auto; intros p1; elim (H ep e p1); tauto). -Qed. - -Definition p_apply_right (f : proposition -> proposition) - (p : proposition) := - match p with - | Timp x y => Timp x (f y) - | Tor x y => Tor x (f y) - | Tand x y => Tand x (f y) - | Tnot x => Tnot (f x) - | x => x - end. - -Theorem p_apply_right_stable : - forall f : proposition -> proposition, - prop_stable f -> prop_stable (p_apply_right f). -Proof. - unfold prop_stable; intros f H ep e p; split; - (case p; simpl; auto; - [ intros p1; elim (H ep e p1); tauto - | intros p1 p2; elim (H ep e p2); tauto - | intros p1 p2; elim (H ep e p2); tauto - | intros p1 p2; elim (H ep e p2); tauto ]). -Qed. - -Definition p_invert (f : proposition -> proposition) - (p : proposition) := - match p with - | EqTerm x y => Tnot (f (NeqTerm x y)) - | LeqTerm x y => Tnot (f (GtTerm x y)) - | GeqTerm x y => Tnot (f (LtTerm x y)) - | GtTerm x y => Tnot (f (LeqTerm x y)) - | LtTerm x y => Tnot (f (GeqTerm x y)) - | NeqTerm x y => Tnot (f (EqTerm x y)) - | x => x - end. - -Theorem p_invert_stable : - forall f : proposition -> proposition, - prop_stable f -> prop_stable (p_invert f). -Proof. - unfold prop_stable; intros f H ep e p; split; - (case p; simpl; auto; - [ intros t1 t2; elim (H ep e (NeqTerm t1 t2)); simpl; - generalize (dec_eq (interp_term e t1) (interp_term e t2)); - unfold decidable; tauto - | intros t1 t2; elim (H ep e (GtTerm t1 t2)); simpl; - generalize (dec_gt (interp_term e t1) (interp_term e t2)); - unfold decidable; rewrite le_lt_iff, <- gt_lt_iff; tauto - | intros t1 t2; elim (H ep e (LtTerm t1 t2)); simpl; - generalize (dec_lt (interp_term e t1) (interp_term e t2)); - unfold decidable; rewrite ge_le_iff, le_lt_iff; tauto - | intros t1 t2; elim (H ep e (LeqTerm t1 t2)); simpl; - generalize (dec_gt (interp_term e t1) (interp_term e t2)); - unfold decidable; repeat rewrite le_lt_iff; - repeat rewrite gt_lt_iff; tauto - | intros t1 t2; elim (H ep e (GeqTerm t1 t2)); simpl; - generalize (dec_lt (interp_term e t1) (interp_term e t2)); - unfold decidable; repeat rewrite ge_le_iff; - repeat rewrite le_lt_iff; tauto - | intros t1 t2; elim (H ep e (EqTerm t1 t2)); simpl; - generalize (dec_eq (interp_term e t1) (interp_term e t2)); - unfold decidable; tauto ]). -Qed. - -Theorem move_right_stable : forall s : step, prop_stable (move_right s). -Proof. - unfold move_right, prop_stable; intros s ep e p; split; - [ Simplify; simpl; elim (t_rewrite_stable s e); simpl; - [ symmetry ; apply egal_left; assumption - | intro; apply le_left; assumption - | intro; apply le_left; rewrite <- ge_le_iff; assumption - | intro; apply lt_left; rewrite <- gt_lt_iff; assumption - | intro; apply lt_left; assumption - | intro; apply ne_left_2; assumption ] - | case p; simpl; intros; auto; generalize H; elim (t_rewrite_stable s); - simpl; intro H1; - [ rewrite (plus_0_r_reverse (interp_term e t1)); rewrite H1; - rewrite plus_permute; rewrite plus_opp_r; - rewrite plus_0_r; trivial - | apply (fun a b => plus_le_reg_r a b (- interp_term e t0)); - rewrite plus_opp_r; assumption - | rewrite ge_le_iff; - apply (fun a b => plus_le_reg_r a b (- interp_term e t1)); - rewrite plus_opp_r; assumption - | rewrite gt_lt_iff; apply lt_left_inv; assumption - | apply lt_left_inv; assumption - | unfold not; intro H2; apply H1; - rewrite H2; rewrite plus_opp_r; trivial ] ]. -Qed. - - -Fixpoint p_rewrite (s : p_step) : proposition -> proposition := - match s with - | P_LEFT s => p_apply_left (p_rewrite s) - | P_RIGHT s => p_apply_right (p_rewrite s) - | P_STEP s => move_right s - | P_INVERT s => p_invert (move_right s) - | P_NOP => fun p : proposition => p - end. - -Theorem p_rewrite_stable : forall s : p_step, prop_stable (p_rewrite s). -Proof. - simple induction s; simpl; - [ intros; apply p_apply_left_stable; trivial - | intros; apply p_apply_right_stable; trivial - | intros; apply p_invert_stable; apply move_right_stable - | apply move_right_stable - | unfold prop_stable; simpl; intros; split; auto ]. -Qed. +Inductive direction : Set := + | D_left : direction + | D_right : direction. -Fixpoint normalize_hyps (l : list h_step) (lh : hyps) {struct l} : hyps := - match l with - | nil => lh - | pair_step i s :: r => normalize_hyps r (apply_oper_1 i (p_rewrite s) lh) - end. +(** This type allows extracting useful components from hypothesis, either + hypothesis generated by splitting a disjonction, or equations. + The last constructor indicates how to solve the obtained system + via the use of the trace type of Omega [t_omega] *) -Theorem normalize_hyps_valid : - forall l : list h_step, valid_hyps (normalize_hyps l). -Proof. - simple induction l; unfold valid_hyps; simpl; - [ auto - | intros n_s r; case n_s; intros n s H ep e lp H1; apply H; - apply apply_oper_1_valid; - [ unfold valid1; intros ep1 e1 p1 H2; - elim (p_rewrite_stable s ep1 e1 p1); auto - | assumption ] ]. -Qed. +Inductive e_step : Set := + | E_SPLIT : nat -> list direction -> e_step -> e_step -> e_step + | E_EXTRACT : nat -> list direction -> e_step -> e_step + | E_SOLVE : t_omega -> e_step. -Theorem normalize_hyps_goal : - forall (s : list h_step) (ep : list Prop) (env : list int) (l : hyps), - interp_goal ep env (normalize_hyps s l) -> interp_goal ep env l. -Proof. - intros; apply valid_goal with (2 := H); apply normalize_hyps_valid. -Qed. +(** Selection of a basic fact inside an hypothesis. *) -Fixpoint extract_hyp_pos (s : list direction) (p : proposition) {struct s} : +Fixpoint extract_hyp_pos (s : list direction) (p : proposition) : proposition := - match s with - | D_left :: l => - match p with - | Tand x y => extract_hyp_pos l x - | _ => p - end - | D_right :: l => - match p with - | Tand x y => extract_hyp_pos l y - | _ => p - end - | D_mono :: l => match p with - | Tnot x => extract_hyp_neg l x - | _ => p - end - | _ => p + match p, s with + | Tand x y, D_left :: l => extract_hyp_pos l x + | Tand x y, D_right :: l => extract_hyp_pos l y + | Tnot x, _ => extract_hyp_neg s x + | _, _ => p end - with extract_hyp_neg (s : list direction) (p : proposition) {struct s} : + with extract_hyp_neg (s : list direction) (p : proposition) : proposition := - match s with - | D_left :: l => - match p with - | Tor x y => extract_hyp_neg l x - | Timp x y => if decidability x then extract_hyp_pos l x else Tnot p - | _ => Tnot p - end - | D_right :: l => - match p with - | Tor x y => extract_hyp_neg l y - | Timp x y => extract_hyp_neg l y - | _ => Tnot p - end - | D_mono :: l => - match p with - | Tnot x => if decidability x then extract_hyp_pos l x else Tnot p - | _ => Tnot p - end - | _ => - match p with - | Tnot x => if decidability x then x else Tnot p - | _ => Tnot p - end + match p, s with + | Tor x y, D_left :: l => extract_hyp_neg l x + | Tor x y, D_right :: l => extract_hyp_neg l y + | Timp x y, D_left :: l => + if decidability x then extract_hyp_pos l x else Tnot p + | Timp x y, D_right :: l => extract_hyp_neg l y + | Tnot x, _ => if decidability x then extract_hyp_pos s x else Tnot p + | _, _ => Tnot p end. -Definition co_valid1 (f : proposition -> proposition) := - forall (ep : list Prop) (e : list int) (p1 : proposition), - interp_proposition ep e (Tnot p1) -> interp_proposition ep e (f p1). - Theorem extract_valid : - forall s : list direction, - valid1 (extract_hyp_pos s) /\ co_valid1 (extract_hyp_neg s). + forall s : list direction, valid1 (extract_hyp_pos s). Proof. - unfold valid1, co_valid1; simple induction s; - [ split; - [ simpl; auto - | intros ep e p1; case p1; simpl; auto; intro p; - pattern (decidability p); apply bool_eq_ind; - [ intro H; generalize (decidable_correct ep e p H); - unfold decidable; tauto - | simpl; auto ] ] - | intros a s' (H1, H2); simpl in H2; split; intros ep e p; case a; auto; - case p; auto; simpl; intros; - (apply H1; tauto) || - (apply H2; tauto) || - (pattern (decidability p0); apply bool_eq_ind; - [ intro H3; generalize (decidable_correct ep e p0 H3); - unfold decidable; intro H4; apply H1; - tauto - | intro; tauto ]) ]. + assert (forall p s ep e, + (interp_prop ep e p -> + interp_prop ep e (extract_hyp_pos s p)) /\ + (interp_prop ep e (Tnot p) -> + interp_prop ep e (extract_hyp_neg s p))). + { induction p; destruct s; simpl; auto; split; try destruct d; try easy; + intros; (apply IHp || apply IHp1 || apply IHp2 || idtac); simpl; try tauto; + destruct decidability eqn:D; auto; + apply (decidable_correct ep e) in D; unfold decidable in D; + (apply IHp || apply IHp1); tauto. } + red. intros. now apply H. Qed. -Fixpoint decompose_solve (s : e_step) (h : hyps) {struct s} : lhyps := +(** Attempt to shorten error messages if romega goes rogue... + NB: [interp_list_goal _ _ BUG = False /\ True]. *) +Definition BUG : lhyps := nil :: nil. + +(** Split and extract in hypotheses *) + +Fixpoint decompose_solve (s : e_step) (h : hyps) : lhyps := match s with | E_SPLIT i dl s1 s2 => match extract_hyp_pos dl (nth_hyps i h) with @@ -3053,50 +1759,45 @@ Fixpoint decompose_solve (s : e_step) (h : hyps) {struct s} : lhyps := then decompose_solve s1 (Tnot x :: h) ++ decompose_solve s2 (Tnot y :: h) - else h :: nil + else BUG | Timp x y => if decidability x then decompose_solve s1 (Tnot x :: h) ++ decompose_solve s2 (y :: h) - else h::nil - | _ => h :: nil + else BUG + | _ => BUG end | E_EXTRACT i dl s1 => decompose_solve s1 (extract_hyp_pos dl (nth_hyps i h) :: h) | E_SOLVE t => execute_omega t h end. -Theorem decompose_solve_valid : - forall s : e_step, valid_list_goal (decompose_solve s). -Proof. - intro s; apply goal_valid; unfold valid_list_hyps; elim s; - simpl; intros; - [ cut (interp_proposition ep e1 (extract_hyp_pos l (nth_hyps n lp))); - [ case (extract_hyp_pos l (nth_hyps n lp)); simpl; auto; - [ intro p; case p; simpl; auto; intros p1 p2 H2; - pattern (decidability p1); apply bool_eq_ind; - [ intro H3; generalize (decidable_correct ep e1 p1 H3); intro H4; - apply append_valid; elim H4; intro H5; - [ right; apply H0; simpl; tauto - | left; apply H; simpl; tauto ] - | simpl; auto ] - | intros p1 p2 H2; apply append_valid; simpl; elim H2; - [ intros H3; left; apply H; simpl; auto - | intros H3; right; apply H0; simpl; auto ] - | intros p1 p2 H2; - pattern (decidability p1); apply bool_eq_ind; - [ intro H3; generalize (decidable_correct ep e1 p1 H3); intro H4; - apply append_valid; elim H4; intro H5; - [ right; apply H0; simpl; tauto - | left; apply H; simpl; tauto ] - | simpl; auto ] ] - | elim (extract_valid l); intros H2 H3; apply H2; apply nth_valid; auto ] - | intros; apply H; simpl; split; - [ elim (extract_valid l); intros H2 H3; apply H2; apply nth_valid; auto - | auto ] - | apply omega_valid with (1 := H) ]. -Qed. - -(* \subsection{La dernière étape qui élimine tous les séquents inutiles} *) +Theorem decompose_solve_valid (s : e_step) : + valid_list_goal (decompose_solve s). +Proof. + apply goal_valid. red. induction s; simpl; intros ep e lp H. + - assert (H' : interp_prop ep e (extract_hyp_pos l (nth_hyps n lp))). + { now apply extract_valid, nth_valid. } + destruct extract_hyp_pos; simpl in *; auto. + + destruct p; simpl; auto. + destruct decidability eqn:D; [ | simpl; auto]. + apply (decidable_correct ep e) in D. + apply append_valid. simpl in *. destruct D. + * right. apply IHs2. simpl; auto. + * left. apply IHs1. simpl; auto. + + apply append_valid. destruct H'. + * left. apply IHs1. simpl; auto. + * right. apply IHs2. simpl; auto. + + destruct decidability eqn:D; [ | simpl; auto]. + apply (decidable_correct ep e) in D. + apply append_valid. destruct D. + * right. apply IHs2. simpl; auto. + * left. apply IHs1. simpl; auto. + - apply IHs; simpl; split; auto. + now apply extract_valid, nth_valid. + - now apply omega_valid. +Qed. + +(** Reduction of subgoal list by discarding the contradictory subgoals. *) Definition valid_lhyps (f : lhyps -> lhyps) := forall (ep : list Prop) (e : list int) (lp : lhyps), @@ -3104,18 +1805,18 @@ Definition valid_lhyps (f : lhyps -> lhyps) := Fixpoint reduce_lhyps (lp : lhyps) : lhyps := match lp with + | nil => nil | (FalseTerm :: nil) :: lp' => reduce_lhyps lp' - | x :: lp' => x :: reduce_lhyps lp' - | nil => nil (A:=hyps) + | x :: lp' => BUG end. Theorem reduce_lhyps_valid : valid_lhyps reduce_lhyps. Proof. - unfold valid_lhyps; intros ep e lp; elim lp; - [ simpl; auto - | intros a l HR; elim a; - [ simpl; tauto - | intros a1 l1; case l1; case a1; simpl; try tauto ] ]. + unfold valid_lhyps; intros ep e lp; elim lp. + - simpl; auto. + - intros a l HR; elim a. + + simpl; tauto. + + intros a1 l1; case l1; case a1; simpl; tauto. Qed. Theorem do_reduce_lhyps : @@ -3127,6 +1828,8 @@ Proof. assumption. Qed. +(** Pushing the conclusion into the hypotheses. *) + Definition concl_to_hyp (p : proposition) := if decidability p then Tnot p else TrueTerm. @@ -3135,33 +1838,35 @@ Definition do_concl_to_hyp : interp_goal envp env (concl_to_hyp c :: l) -> interp_goal_concl c envp env l. Proof. - simpl; intros envp env c l; induction l as [| a l Hrecl]; - [ simpl; unfold concl_to_hyp; - pattern (decidability c); apply bool_eq_ind; - [ intro H; generalize (decidable_correct envp env c H); - unfold decidable; simpl; tauto - | simpl; intros H1 H2; elim H2; trivial ] - | simpl; tauto ]. + induction l; simpl. + - unfold concl_to_hyp; simpl. + destruct decidability eqn:D; [ | simpl; tauto ]. + apply (decidable_correct envp env) in D. unfold decidable in D. + simpl. tauto. + - simpl in *; tauto. Qed. -Definition omega_tactic (t1 : e_step) (t2 : list h_step) - (c : proposition) (l : hyps) := - reduce_lhyps (decompose_solve t1 (normalize_hyps t2 (concl_to_hyp c :: l))). +(** The omega tactic : all steps together *) + +Definition omega_tactic (t1 : e_step) (c : proposition) (l : hyps) := + reduce_lhyps (decompose_solve t1 (normalize_hyps (concl_to_hyp c :: l))). Theorem do_omega : - forall (t1 : e_step) (t2 : list h_step) (envp : list Prop) + forall (t : e_step) (envp : list Prop) (env : list int) (c : proposition) (l : hyps), - interp_list_goal envp env (omega_tactic t1 t2 c l) -> + interp_list_goal envp env (omega_tactic t c l) -> interp_goal_concl c envp env l. Proof. - unfold omega_tactic; intros; apply do_concl_to_hyp; - apply (normalize_hyps_goal t2); apply (decompose_solve_valid t1); - apply do_reduce_lhyps; assumption. + unfold omega_tactic; intros t ep e c l H. + apply do_concl_to_hyp. + apply normalize_hyps_goal. + apply (decompose_solve_valid t). + now apply do_reduce_lhyps. Qed. End IntOmega. -(* For now, the above modular construction is instanciated on Z, - in order to retrieve the initial ROmega. *) +(** For now, the above modular construction is instanciated on Z, + in order to retrieve the initial ROmega. *) Module ZOmega := IntOmega(Z_as_Int). |