diff options
Diffstat (limited to 'contrib/romega/ReflOmegaCore.v')
| -rw-r--r-- | contrib/romega/ReflOmegaCore.v | 2353 |
1 files changed, 1411 insertions, 942 deletions
diff --git a/contrib/romega/ReflOmegaCore.v b/contrib/romega/ReflOmegaCore.v index d20cafc1..9d379548 100644 --- a/contrib/romega/ReflOmegaCore.v +++ b/contrib/romega/ReflOmegaCore.v @@ -7,32 +7,852 @@ *************************************************************************) -Require Import Arith. -Require Import List. -Require Import Bool. -Require Import ZArith_base. -Require Import OmegaLemmas. - -Open Scope Z_scope. - -(* \subsection{Definition of basic types} *) - -(* \subsubsection{Environment of propositions (lists) *) -Inductive PropList : Type := - | Pnil : PropList - | Pcons : Prop -> PropList -> PropList. - -(* Access function for the environment with a default *) -Fixpoint nthProp (n : nat) (l : PropList) (default : Prop) {struct l} : - Prop := - match n, l with - | O, Pcons x l' => x - | O, other => default - | S m, Pnil => default - | S m, Pcons x t => nthProp m t default - end. +Require Import List Bool Sumbool EqNat Setoid Ring_theory Decidable. +Delimit Scope Int_scope with I. + +(* Abstract Integers. *) + +Module Type Int. + + Parameter int : Set. + + Parameter zero : int. + Parameter one : int. + Parameter plus : int -> int -> int. + Parameter opp : int -> int. + Parameter minus : int -> int -> int. + Parameter mult : int -> int -> int. + + Notation "0" := zero : Int_scope. + Notation "1" := one : Int_scope. + Infix "+" := plus : Int_scope. + Infix "-" := minus : Int_scope. + Infix "*" := mult : Int_scope. + Notation "- x" := (opp x) : Int_scope. + + Open Scope Int_scope. + + (* First, int is a ring: *) + Axiom ring : @ring_theory int 0 1 plus mult minus opp (@eq int). + + (* int should also be ordered: *) + + Parameter le : int -> int -> Prop. + Parameter lt : int -> int -> Prop. + Parameter ge : int -> int -> Prop. + Parameter gt : int -> int -> 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. + Notation "x > y" := (gt x y): Int_scope. + Axiom le_lt_iff : forall i j, (i<=j) <-> ~(j<i). + 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 *) + 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 *) + 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*) + Parameter compare : int -> int -> 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 + 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 *) + +End Int. + + + +(* Of course, Z is a model for our abstract int *) + +Module Z_as_Int <: Int. + + Require Import ZArith_base. + Open Scope Z_scope. + + Definition int := Z. + Definition zero := 0. + Definition one := 1. + Definition plus := Zplus. + Definition opp := Zopp. + Definition minus := Zminus. + Definition mult := Zmult. + + Lemma ring : @ring_theory int zero one plus mult minus opp (@eq int). + Proof. + constructor. + exact Zplus_0_l. + exact Zplus_comm. + exact Zplus_assoc. + exact Zmult_1_l. + exact Zmult_comm. + exact Zmult_assoc. + exact Zmult_plus_distr_l. + unfold minus, Zminus; auto. + exact Zplus_opp_r. + Qed. + + Definition le := Zle. + Definition lt := Zlt. + Definition ge := Zge. + Definition gt := Zgt. + Lemma le_lt_iff : forall i j, (i<=j) <-> ~(j<i). + Proof. + split; intros. + apply Zle_not_lt; auto. + rewrite <- Zge_iff_le. + apply Znot_lt_ge; auto. + Qed. + Definition ge_le_iff := Zge_iff_le. + Definition gt_lt_iff := Zgt_iff_lt. + + Definition lt_trans := Zlt_trans. + Definition lt_not_eq := Zlt_not_eq. + + Definition lt_0_1 := Zlt_0_1. + Definition plus_le_compat := Zplus_le_compat. + Definition mult_lt_compat_l := Zmult_lt_compat_l. + Lemma opp_le_compat : forall i j, i<=j -> (-j)<=(-i). + Proof. + unfold Zle; intros; rewrite <- Zcompare_opp; auto. + Qed. + + Definition compare := Zcompare. + Definition compare_Eq := Zcompare_Eq_iff_eq. + Lemma compare_Lt : forall i j, compare i j = Lt <-> i<j. + Proof. intros; unfold compare, Zlt; intuition. Qed. + Lemma compare_Gt : forall i j, compare i j = Gt <-> i>j. + Proof. intros; unfold compare, Zgt; intuition. Qed. + + Lemma le_lt_int : forall x y, x<y <-> x<=y+-(1). + Proof. + intros; split; intros. + generalize (Zlt_left _ _ H); simpl; intros. + apply Zle_left_rev; auto. + apply Zlt_0_minus_lt. + generalize (Zplus_le_lt_compat x (y+-1) (-x) (-x+1) H). + rewrite Zplus_opp_r. + rewrite <-Zplus_assoc. + rewrite (Zplus_permute (-1)). + simpl in *. + rewrite Zplus_0_r. + intro H'; apply H'. + replace (-x+1) with (Zsucc (-x)); auto. + apply Zlt_succ. + Qed. + +End Z_as_Int. + + + + +Module IntProperties (I:Int). + Import I. + + (* 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. *) + + Definition plus_assoc := ring.(Radd_assoc). + Definition plus_comm := ring.(Radd_comm). + Definition plus_0_l := ring.(Radd_0_l). + Definition mult_assoc := ring.(Rmul_assoc). + Definition mult_comm := ring.(Rmul_comm). + Definition mult_1_l := ring.(Rmul_1_l). + Definition mult_plus_distr_r := ring.(Rdistr_l). + Definition opp_def := ring.(Ropp_def). + Definition minus_def := ring.(Rsub_def). + + 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 *) + + 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). + 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. + + Lemma mult_plus_distr_l : forall x y z, x*(y+z)=x*y+x*z. + Proof. + intros. + rewrite (mult_comm x (y+z)), (mult_comm x y), (mult_comm x z). + apply mult_plus_distr_r. + Qed. + + Lemma mult_0_l : forall x, 0*x = 0. + Proof. + intros. + generalize (mult_plus_distr_r 0 1 x). + rewrite plus_0_l, mult_1_l, plus_comm; intros. + apply plus_reg_l with x. + rewrite <- H. + apply plus_0_r_reverse. + Qed. + + + (* More facts about opp *) + + Definition plus_opp_r := opp_def. + + Lemma plus_opp_l : forall x, -x + x = 0. + Proof. intros; now rewrite plus_comm, opp_def. Qed. + + Lemma mult_opp_comm : forall x y, - x * y = x * - y. + Proof. + intros. + apply plus_reg_l with (x*y). + rewrite <- mult_plus_distr_l, <- mult_plus_distr_r. + now rewrite opp_def, opp_def, mult_0_l, mult_comm, mult_0_l. + Qed. + + Lemma opp_eq_mult_neg_1 : forall x, -x = x * -(1). + Proof. + intros; now rewrite mult_comm, mult_opp_comm, mult_1_l. + Qed. + + Lemma opp_involutive : forall x, -(-x) = x. + Proof. + intros. + apply plus_reg_l with (-x). + now rewrite opp_def, plus_comm, opp_def. + Qed. + + Lemma opp_plus_distr : forall x y, -(x+y) = -x + -y. + Proof. + intros. + apply plus_reg_l with (x+y). + rewrite opp_def. + rewrite plus_permute. + do 2 rewrite plus_assoc. + now rewrite (plus_comm (-x)), opp_def, plus_0_l, opp_def. + Qed. + + Lemma opp_mult_distr_r : forall x y, -(x*y) = x * -y. + Proof. + intros. + rewrite <- mult_opp_comm. + apply plus_reg_l with (x*y). + 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). + Proof. + intros; now rewrite mult_plus_distr_l. + 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 *) + + 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. + + Lemma OMEGA12 : + forall v2 c2 l1 l2 k2 : int, + l1 + (v2 * c2 + l2) * k2 = v2 * (c2 * k2) + (l1 + l2 * k2). + Proof. + intros; autorewrite with int; now rewrite plus_permute. + Qed. + + Lemma OMEGA13 : + forall v l1 l2 x : int, + v * -x + l1 + (v * x + l2) = l1 + 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. + 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). + Proof. + intros; autorewrite with int; f_equal; now rewrite plus_permute. + Qed. + + Lemma OMEGA16 : forall v c l k : int, (v * c + l) * k = v * (c * k) + l * k. + 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 in |- *; auto. + now rewrite mult_0_l, mult_0_l, plus_0_l. + Qed. + + + (* Secondo, some results about order (and equality) *) + + Lemma lt_irrefl : forall n, ~ n<n. + Proof. + intros n H. + elim (lt_not_eq _ _ H); auto. + Qed. + + Lemma lt_antisym : forall n m, n<m -> m<n -> False. + Proof. + intros; elim (lt_irrefl _ (lt_trans _ _ _ H H0)); auto. + Qed. + + Lemma lt_le_weak : forall n m, n<m -> n<=m. + Proof. + intros; rewrite le_lt_iff; intro H'; eapply lt_antisym; eauto. + Qed. + + Lemma le_refl : forall n, n<=n. + Proof. + intros; rewrite le_lt_iff; apply lt_irrefl; auto. + Qed. + + Lemma le_antisym : forall n m, n<=m -> m<=n -> n=m. + Proof. + intros n m; do 2 rewrite le_lt_iff; intros. + rewrite <- compare_Lt in H0. + rewrite <- gt_lt_iff, <- compare_Gt in H. + rewrite <- compare_Eq. + destruct compare; intuition. + Qed. + + Lemma lt_eq_lt_dec : forall n m, { n<m }+{ n=m }+{ m<n }. + Proof. + intros. + generalize (compare_Lt n m)(compare_Eq n m)(compare_Gt n m). + destruct compare; [ left; right | left; left | right ]; intuition. + rewrite gt_lt_iff in H1; intuition. + Qed. + + Lemma lt_dec : forall n m: int, { n<m } + { ~n<m }. + Proof. + intros. + generalize (compare_Lt n m)(compare_Eq n m)(compare_Gt n m). + destruct compare; [ right | left | right ]; intuition discriminate. + Qed. + + Lemma lt_le_iff : forall n m, (n<m) <-> ~(m<=n). + Proof. + intros. + rewrite le_lt_iff. + destruct (lt_dec n m); intuition. + Qed. + + Lemma le_dec : forall n m: int, { n<=m } + { ~n<=m }. + Proof. + intros; destruct (lt_dec m n); [right|left]; rewrite le_lt_iff; intuition. + Qed. + + Lemma le_lt_dec : forall n m, { n<=m } + { m<n }. + Proof. + intros; destruct (le_dec n m); [left|right]; auto; now rewrite lt_le_iff. + Qed. + + + 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. + + Lemma beq_true : forall i j, beq i j = true -> i=j. + Proof. + intros. + rewrite <- beq_iff; auto. + Qed. + + Lemma beq_false : forall i j, beq i j = false -> i<>j. + Proof. + intros. + intro H'. + rewrite <- beq_iff in H'; rewrite H' in H; discriminate. + Qed. + + Lemma eq_dec : forall n m:int, { n=m } + { n<>m }. + Proof. + intros; generalize (beq_iff n m); destruct beq; [left|right]; intuition. + Qed. + + Definition bgt i j := match compare i j with Gt => true | _ => false end. + + Lemma bgt_iff : forall i j, bgt i j = true <-> i>j. + Proof. + intros; unfold bgt; generalize (compare_Gt i j). + destruct compare; intuition discriminate. + 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. + Proof. + intros. + rewrite le_lt_iff, <-gt_lt_iff, <-bgt_iff; intro H'; now rewrite H' in H. + Qed. + + Lemma le_is_lt_or_eq : forall n m, n<=m -> { n<m } + { n=m }. + Proof. + intros. + destruct (eq_dec n m) as [H'|H']. + right; intuition. + left; rewrite lt_le_iff. + contradict H'. + apply le_antisym; auto. + Qed. + + Lemma le_neq_lt : forall n m, n<=m -> n<>m -> n<m. + Proof. + intros. + destruct (le_is_lt_or_eq _ _ H); intuition. + 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. + 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. + 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. + Qed. + + Lemma le_0_neg' : forall n, n <= 0 <-> 0 <= -n. + Proof. + intros; rewrite le_0_neg, opp_involutive; intuition. + Qed. + + Lemma plus_le_reg_r : forall n m p, n + p <= m + p -> n <= m. + Proof. + intros. + replace n with ((n+p)+-p). + replace m with ((m+p)+-p). + apply plus_le_compat; auto. + apply le_refl. + now rewrite <- plus_assoc, opp_def, plus_0_r. + now rewrite <- plus_assoc, opp_def, plus_0_r. + Qed. + + Lemma plus_le_lt_compat : forall n m p q, n<=m -> p<q -> n+p<m+q. + Proof. + intros. + apply le_neq_lt. + apply plus_le_compat; auto. + apply lt_le_weak; auto. + rewrite lt_le_iff in H0. + contradict H0. + apply plus_le_reg_r with m. + rewrite (plus_comm q m), <-H0, (plus_comm p m). + apply plus_le_compat; auto. + apply le_refl; auto. + Qed. + + Lemma plus_lt_compat : forall n m p q, n<m -> p<q -> n+p<m+q. + Proof. + intros. + apply plus_le_lt_compat; auto. + apply lt_le_weak; auto. + Qed. + + Lemma opp_lt_compat : forall n m, n<m -> -m < -n. + Proof. + intros n m; do 2 rewrite lt_le_iff; intros H; contradict H. + rewrite <-(opp_involutive m), <-(opp_involutive n). + apply opp_le_compat; auto. + Qed. + + Lemma lt_0_neg : forall n, 0 < n <-> -n < 0. + Proof. + intros. + pattern 0 at 2; rewrite <- (mult_0_l (-(1))). + 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. + Qed. + + Lemma mult_lt_0_compat : forall n m, 0 < n -> 0 < m -> 0 < n*m. + Proof. + intros. + rewrite <- (mult_0_l n), mult_comm. + apply mult_lt_compat_l; auto. + Qed. + + Lemma mult_integral : forall n m, n * m = 0 -> n = 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; elimtype False. + + 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). + Qed. + + Lemma mult_le_compat : + forall i j k l, i<=j -> k<=l -> 0<=i -> 0<=k -> i*k<=j*l. + 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. + Qed. + + Lemma sum5 : + forall a b c d : int, c <> 0 -> 0 <> a -> 0 = b -> 0 <> a * c + b * d. + Proof. + intros. + subst b; rewrite mult_0_l, plus_0_r. + contradict H. + symmetry in H; destruct (mult_integral _ _ H); congruence. + Qed. + + Lemma one_neq_zero : 1 <> 0. + Proof. + red; intro. + symmetry in H. + apply (lt_not_eq 0 1); auto. + apply lt_0_1. + Qed. + + Lemma minus_one_neq_zero : -(1) <> 0. + Proof. + apply lt_not_eq. + rewrite <- lt_0_neg. + apply lt_0_1. + Qed. + + Lemma le_left : forall 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. + 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. + Proof. + intros. + assert (y=-x). + subst x; symmetry; apply opp_involutive. + clear H1; subst y. + destruct (eq_dec 0 x) as [H'|H']; auto. + assert (H'':=le_neq_lt _ _ H H'). + generalize (plus_le_lt_compat _ _ _ _ H0 H''). + rewrite plus_opp_l, plus_0_l. + intros. + 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. + Proof. + intros. + subst a; rewrite mult_0_l, plus_0_l. + rewrite <- (mult_0_l 0). + apply mult_le_compat; auto; apply le_refl. + Qed. + + Lemma sum3 : + forall a b c d : int, + 0 <= c -> 0 <= d -> 0 <= a -> 0 <= b -> 0 <= a * c + b * d. + Proof. + intros. + rewrite <- (plus_0_l 0). + apply plus_le_compat; auto. + rewrite <- (mult_0_l 0). + apply mult_le_compat; auto; apply le_refl. + rewrite <- (mult_0_l 0). + 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. + + Lemma lt_left_inv : forall x y, 0 <= y + -(1) + - x -> x < y. + Proof. + intros. + generalize (plus_le_compat _ _ _ _ H (le_refl x)); clear H. + now rewrite plus_0_l, <-plus_assoc, plus_opp_l, plus_0_r, le_lt_int. + Qed. + + Lemma OMEGA4 : forall x y z, x > 0 -> y > x -> z * y + x <> 0. + Proof. + intros. + intro H'. + rewrite gt_lt_iff in H,H0. + 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. + + 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. + rewrite <- (plus_0_l 0). + apply plus_lt_compat; auto. + apply mult_lt_0_compat; auto. + apply lt_trans with x; auto. + Qed. + + Lemma OMEGA19 : forall x, x<>0 -> 0 <= x + -(1) \/ 0 <= x * -(1) + -(1). + Proof. + intros. + do 2 rewrite <- le_lt_int. + rewrite <- opp_eq_mult_neg_1. + destruct (lt_eq_lt_dec 0 x) as [[H'|H']|H']. + auto. + congruence. + right. + rewrite <-(mult_0_l (-(1))), <-(opp_eq_mult_neg_1 0). + apply opp_lt_compat; auto. + Qed. + + Lemma mult_le_approx : + forall n m p, n > 0 -> n > p -> 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. + 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 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. + Qed. + + (* Some decidabilities *) + + Lemma dec_eq : forall i j:int, decidable (i=j). + Proof. + red; intros; destruct (eq_dec i j); auto. + Qed. + + Lemma dec_ne : forall i j:int, decidable (i<>j). + Proof. + red; intros; destruct (eq_dec i j); auto. + Qed. + + Lemma dec_le : forall i j:int, decidable (i<=j). + Proof. + red; intros; destruct (le_dec i j); auto. + Qed. + + Lemma dec_lt : forall i j:int, decidable (i<j). + Proof. + red; intros; destruct (lt_dec i j); auto. + Qed. + + Lemma dec_ge : forall i j:int, decidable (i>=j). + Proof. + red; intros; rewrite ge_le_iff; destruct (le_dec j i); auto. + Qed. + + Lemma dec_gt : forall i j:int, decidable (i>j). + Proof. + red; intros; rewrite gt_lt_iff; destruct (lt_dec j i); auto. + Qed. + +End IntProperties. + + + + +Module IntOmega (I:Int). +Import I. +Module IP:=IntProperties(I). +Import IP. -(* \subsubsection{Définition of reified integer expressions} +(* \subsubsection{Definition of reified integer expressions} Terms are either: \begin{itemize} \item integers [Tint] @@ -41,7 +861,7 @@ Fixpoint nthProp (n : nat) (l : PropList) (default : Prop) {struct l} : The last two are translated in additions and products. *) Inductive term : Set := - | Tint : Z -> term + | Tint : int -> term | Tplus : term -> term -> term | Tmult : term -> term -> term | Tminus : term -> term -> term @@ -49,6 +869,7 @@ Inductive term : Set := | Tvar : nat -> term. Delimit Scope romega_scope with term. +Arguments Scope Tint [Int_scope]. Arguments Scope Tplus [romega_scope romega_scope]. Arguments Scope Tmult [romega_scope romega_scope]. Arguments Scope Tminus [romega_scope romega_scope]. @@ -58,20 +879,21 @@ Infix "+" := Tplus : romega_scope. Infix "*" := Tmult : romega_scope. Infix "-" := Tminus : romega_scope. Notation "- x" := (Topp x) : romega_scope. -Notation "[ x ]" := (Tvar x) (at level 1) : romega_scope. +Notation "[ x ]" := (Tvar x) (at level 0) : romega_scope. (* \subsubsection{Definition of reified goals} *) + (* 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 (* egalité entre termes *) - | LeqTerm : term -> term -> proposition (* plus petit ou egal *) - | TrueTerm : proposition (* vrai *) - | FalseTerm : proposition (* faux *) - | Tnot : proposition -> proposition (* négation *) + | 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 *) | GeqTerm : term -> term -> proposition | GtTerm : term -> term -> proposition | LtTerm : term -> term -> proposition @@ -87,7 +909,7 @@ Notation hyps := (list proposition). (* Definition of lists of subgoals (set of open goals) *) Notation lhyps := (list hyps). -(* a syngle goal packed in a subgoal list *) +(* a single goal packed in a subgoal list *) Notation singleton := (fun a : hyps => a :: nil). (* an absurd goal *) @@ -110,24 +932,22 @@ Inductive t_fusion : Set := (* \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 *) + (* 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 *) + (* 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 *) + (* 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_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 @@ -152,261 +972,98 @@ Inductive step : Set := the trace coming from the decision procedure Omega. *) Inductive t_omega : Set := - (* n = 0 n!= 0 *) + (* n = 0 and n!= 0 *) | O_CONSTANT_NOT_NUL : nat -> t_omega - | O_CONSTANT_NEG : - nat -> t_omega - (* division et approximation of an equation *) - | O_DIV_APPROX : - Z -> - Z -> - term -> - nat -> - t_omega -> nat -> t_omega - (* no solution because no exact division *) - | O_NOT_EXACT_DIVIDE : - Z -> Z -> term -> nat -> nat -> t_omega - (* exact division *) - | O_EXACT_DIVIDE : Z -> term -> nat -> t_omega -> nat -> t_omega - | O_SUM : Z -> nat -> Z -> nat -> list t_fusion -> t_omega -> 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 : Z -> step -> nat -> nat -> t_omega -> 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. *) -(* \subsubsection{Règles pour normaliser les hypothèses} *) -(* Ces règles indiquent comment normaliser les propositions utiles - de chaque hypothèse utile avant la décomposition des hypothèses et - incluent l'étape d'inversion pour la suppression des négations *) 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. -(* Liste des normalisations a effectuer : avec un constructeur dans le - type [p_step] permettant - de parcourir à la fois les branches gauches et droit, on pourrait n'avoir - qu'une normalisation par hypothèse. Et comme toutes les hypothèses sont - utiles (sinon on ne les inclurait pas), on pourrait remplacer [h_step] - par une simple liste *) + +(* List of normalizations to perform : with a constructor of type + [p_step] allowing to visit both left and right branches, we would be + able to restrict to 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{Règles pour décomposer les hypothèses} *) -(* Ce type permet de se diriger dans les constructeurs logiques formant les - prédicats des hypothèses pour aller les décomposer. Ils permettent - en particulier d'extraire une hypothèse d'une conjonction avec - éventuellement le bon niveau de négations. *) +(* \subsubsection{Rules for decomposing the hypothesis} *) +(* This type allows to navigate 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 + conjonction with possibly the right level of negations. *) Inductive direction : Set := | D_left : direction | D_right : direction | D_mono : direction. -(* Ce type permet d'extraire les composants utiles des hypothèses : que ce - soit des hypothèses générées par éclatement d'une disjonction, ou - des équations. Le constructeur terminal indique comment résoudre le système - obtenu en recourrant au type de trace d'Omega [t_omega] *) +(* This type allows to extract 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{Egalité décidable efficace} *) -(* Pour chaque type de donnée réifié, on calcule un test d'égalité efficace. - Ce n'est pas le cas de celui rendu par [Decide Equality]. +(* \subsection{Efficient decidable equality} *) +(* For each reified data-type, we define an efficient equality test. + It is not the one produced by [Decide Equality]. - Puis on prouve deux théorèmes permettant d'éliminer de telles égalités : + Then we prove two theorem allowing to eliminate 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} *) -(* Ces deux tactiques permettent de résoudre pas mal de cas. L'une pour - les théorèmes positifs, l'autre pour les théorèmes négatifs *) - -Ltac absurd_case := simpl in |- *; intros; discriminate. -Ltac trivial_case := unfold not in |- *; intros; discriminate. - -(* \subsubsection{Entiers naturels} *) - -Fixpoint eq_nat (t1 t2 : nat) {struct t2} : bool := - match t1 with - | O => match t2 with - | O => true - | _ => false - end - | S n1 => match t2 with - | O => false - | S n2 => eq_nat n1 n2 - end - end. - -Theorem eq_nat_true : forall t1 t2 : nat, eq_nat t1 t2 = true -> t1 = t2. - -simple induction t1; - [ intro t2; case t2; [ trivial | absurd_case ] - | intros n H t2; case t2; - [ absurd_case - | simpl in |- *; intros; rewrite (H n0); [ trivial | assumption ] ] ]. - -Qed. - -Theorem eq_nat_false : forall t1 t2 : nat, eq_nat t1 t2 = false -> t1 <> t2. - -simple induction t1; - [ intro t2; case t2; [ simpl in |- *; intros; discriminate | trivial_case ] - | intros n H t2; case t2; simpl in |- *; unfold not in |- *; intros; - [ discriminate | elim (H n0 H0); simplify_eq H1; trivial ] ]. - -Qed. - - -(* \subsubsection{Entiers positifs} *) +(* \subsubsection{Reified terms} *) -Fixpoint eq_pos (p1 p2 : positive) {struct p2} : bool := - match p1 with - | xI n1 => match p2 with - | xI n2 => eq_pos n1 n2 - | _ => false - end - | xO n1 => match p2 with - | xO n2 => eq_pos n1 n2 - | _ => false - end - | xH => match p2 with - | xH => true - | _ => false - end - end. +Open Scope romega_scope. -Theorem eq_pos_true : forall t1 t2 : positive, eq_pos t1 t2 = true -> t1 = t2. - -simple induction t1; - [ intros p H t2; case t2; - [ simpl in |- *; intros; rewrite (H p0 H0); trivial - | absurd_case - | absurd_case ] - | intros p H t2; case t2; - [ absurd_case - | simpl in |- *; intros; rewrite (H p0 H0); trivial - | absurd_case ] - | intro t2; case t2; [ absurd_case | absurd_case | auto ] ]. - -Qed. - -Theorem eq_pos_false : - forall t1 t2 : positive, eq_pos t1 t2 = false -> t1 <> t2. - -simple induction t1; - [ intros p H t2; case t2; - [ simpl in |- *; unfold not in |- *; intros; elim (H p0 H0); - simplify_eq H1; auto - | trivial_case - | trivial_case ] - | intros p H t2; case t2; - [ trivial_case - | simpl in |- *; unfold not in |- *; intros; elim (H p0 H0); - simplify_eq H1; auto - | trivial_case ] - | intros t2; case t2; [ trivial_case | trivial_case | absurd_case ] ]. -Qed. - -(* \subsubsection{Entiers relatifs} *) - -Definition eq_Z (z1 z2 : Z) : bool := - match z1 with - | Z0 => match z2 with - | Z0 => true - | _ => false - end - | Zpos p1 => match z2 with - | Zpos p2 => eq_pos p1 p2 - | _ => false - end - | Zneg p1 => match z2 with - | Zneg p2 => eq_pos p1 p2 - | _ => false - end +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 + | _, _ => false end. -Theorem eq_Z_true : forall t1 t2 : Z, eq_Z t1 t2 = true -> t1 = t2. - -simple induction t1; - [ intros t2; case t2; [ auto | absurd_case | absurd_case ] - | intros p t2; case t2; - [ absurd_case - | simpl in |- *; intros; rewrite (eq_pos_true p p0 H); trivial - | absurd_case ] - | intros p t2; case t2; - [ absurd_case - | absurd_case - | simpl in |- *; intros; rewrite (eq_pos_true p p0 H); trivial ] ]. - -Qed. - -Theorem eq_Z_false : forall t1 t2 : Z, eq_Z t1 t2 = false -> t1 <> t2. - -simple induction t1; - [ intros t2; case t2; [ absurd_case | trivial_case | trivial_case ] - | intros p t2; case t2; - [ absurd_case - | simpl in |- *; unfold not in |- *; intros; elim (eq_pos_false p p0 H); - simplify_eq H0; auto - | trivial_case ] - | intros p t2; case t2; - [ absurd_case - | trivial_case - | simpl in |- *; unfold not in |- *; intros; elim (eq_pos_false p p0 H); - simplify_eq H0; auto ] ]. -Qed. - -(* \subsubsection{Termes réifiés} *) - -Fixpoint eq_term (t1 t2 : term) {struct t2} : bool := - match t1 with - | Tint st1 => match t2 with - | Tint st2 => eq_Z st1 st2 - | _ => false - end - | (st11 + st12)%term => - match t2 with - | (st21 + st22)%term => eq_term st11 st21 && eq_term st12 st22 - | _ => false - end - | (st11 * st12)%term => - match t2 with - | (st21 * st22)%term => eq_term st11 st21 && eq_term st12 st22 - | _ => false - end - | (st11 - st12)%term => - match t2 with - | (st21 - st22)%term => eq_term st11 st21 && eq_term st12 st22 - | _ => false - end - | (- st1)%term => - match t2 with - | (- st2)%term => eq_term st1 st2 - | _ => false - end - | [st1]%term => - match t2 with - | [st2]%term => eq_nat st1 st2 - | _ => false - end - end. +Close Scope romega_scope. Theorem eq_term_true : forall t1 t2 : term, eq_term t1 t2 = true -> t1 = t2. - - -simple induction t1; intros until t2; case t2; try absurd_case; simpl in |- *; - [ intros; elim eq_Z_true with (1 := H); trivial +Proof. + simple induction t1; intros until t2; case t2; simpl in *; + try (intros; discriminate; fail); + [ intros; elim beq_true with (1 := H); trivial | intros t21 t22 H3; elim andb_prop with (1 := H3); intros H4 H5; elim H with (1 := H4); elim H0 with (1 := H5); trivial @@ -417,16 +1074,17 @@ simple induction t1; intros until t2; case t2; try absurd_case; simpl in |- *; elim H with (1 := H4); elim H0 with (1 := H5); trivial | intros t21 H3; elim H with (1 := H3); trivial - | intros; elim eq_nat_true with (1 := H); trivial ]. - + | intros; elim beq_nat_true with (1 := H); trivial ]. Qed. +Ltac trivial_case := unfold not in |- *; intros; discriminate. + Theorem eq_term_false : forall t1 t2 : term, eq_term t1 t2 = false -> t1 <> t2. - -simple induction t1; +Proof. + simple induction t1; [ intros z t2; case t2; try trivial_case; simpl in |- *; unfold not in |- *; - intros; elim eq_Z_false with (1 := H); simplify_eq H0; + intros; elim beq_false with (1 := H); simplify_eq H0; auto | intros t11 H1 t12 H2 t2; case t2; try trivial_case; simpl in |- *; intros t21 t22 H3; unfold not in |- *; intro H4; @@ -447,9 +1105,8 @@ simple induction t1; unfold not in |- *; intro H4; elim H1 with (1 := H3); simplify_eq H4; auto | intros n t2; case t2; try trivial_case; simpl in |- *; unfold not in |- *; - intros; elim eq_nat_false with (1 := H); simplify_eq H0; + intros; elim beq_nat_false with (1 := H); simplify_eq H0; auto ]. - Qed. (* \subsubsection{Tactiques pour éliminer ces tests} @@ -463,54 +1120,29 @@ Qed. tel test préserve bien l'information voulue mais calculatoirement de telles fonctions sont trop lentes. *) -(* Le théorème suivant permet de garder dans les hypothèses la valeur - du booléen lors de l'élimination. *) - -Theorem bool_ind2 : - forall (P : bool -> Prop) (b : bool), - (b = true -> P true) -> (b = false -> P false) -> P b. - -simple induction b; auto. -Qed. - (* 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 := - pattern (eq_term t1 t2) in |- *; apply bool_ind2; intro Aux; + pattern (eq_term t1 t2) in |- *; 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_eq_Z t1 t2 := - pattern (eq_Z t1 t2) in |- *; apply bool_ind2; intro Aux; - [ generalize (eq_Z_true t1 t2 Aux); clear Aux - | generalize (eq_Z_false t1 t2 Aux); clear Aux ]. - -Ltac elim_eq_pos t1 t2 := - pattern (eq_pos t1 t2) in |- *; apply bool_ind2; intro Aux; - [ generalize (eq_pos_true t1 t2 Aux); clear Aux - | generalize (eq_pos_false t1 t2 Aux); clear Aux ]. +Ltac elim_beq t1 t2 := + pattern (beq t1 t2) in |- *; apply bool_eq_ind; intro Aux; + [ generalize (beq_true t1 t2 Aux); clear Aux + | generalize (beq_false t1 t2 Aux); clear Aux ]. -(* \subsubsection{Comparaison sur Z} *) - -(* Sujet très lié au précédent : on introduit la tactique d'élimination - avec son théorème *) - -Theorem relation_ind2 : - forall (P : comparison -> Prop) (b : comparison), - (b = Eq -> P Eq) -> - (b = Lt -> P Lt) -> - (b = Gt -> P Gt) -> P b. - -simple induction b; auto. -Qed. +Ltac elim_bgt t1 t2 := + pattern (bgt t1 t2) in |- *; apply bool_eq_ind; intro Aux; + [ generalize (bgt_true t1 t2 Aux); clear Aux + | generalize (bgt_false t1 t2 Aux); clear Aux ]. -Ltac elim_Zcompare t1 t2 := pattern (t1 ?= t2) in |- *; apply relation_ind2. (* \subsection{Interprétations} \subsubsection{Interprétation des termes dans Z} *) -Fixpoint interp_term (env : list Z) (t : term) {struct t} : Z := +Fixpoint interp_term (env : list int) (t : term) {struct t} : int := match t with | Tint x => x | (t1 + t2)%term => interp_term env t1 + interp_term env t2 @@ -521,7 +1153,8 @@ Fixpoint interp_term (env : list Z) (t : term) {struct t} : Z := end. (* \subsubsection{Interprétation des prédicats} *) -Fixpoint interp_proposition (envp : PropList) (env : list Z) + +Fixpoint interp_proposition (envp : list Prop) (env : list int) (p : proposition) {struct p} : Prop := match p with | EqTerm t1 t2 => interp_term env t1 = interp_term env t2 @@ -532,14 +1165,14 @@ Fixpoint interp_proposition (envp : PropList) (env : list Z) | 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 => Zne (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 - | Tprop n => nthProp n envp True + | Tprop n => nth n envp True end. (* \subsubsection{Inteprétation des listes d'hypothèses} @@ -547,7 +1180,7 @@ Fixpoint interp_proposition (envp : PropList) (env : list Z) Interprétation sous forme d'une conjonction d'hypothèses plus faciles à manipuler individuellement *) -Fixpoint interp_hyps (envp : PropList) (env : list Z) +Fixpoint interp_hyps (envp : list Prop) (env : list int) (l : hyps) {struct l} : Prop := match l with | nil => True @@ -559,8 +1192,8 @@ Fixpoint interp_hyps (envp : PropList) (env : list Z) [Generalize] et qu'une conjonction est forcément lourde (répétition des types dans les conjonctions intermédiaires) *) -Fixpoint interp_goal_concl (c : proposition) (envp : PropList) - (env : list Z) (l : hyps) {struct l} : Prop := +Fixpoint interp_goal_concl (c : proposition) (envp : list Prop) + (env : list int) (l : hyps) {struct l} : Prop := match l with | nil => interp_proposition envp env c | p' :: l' => @@ -573,19 +1206,19 @@ Notation interp_goal := (interp_goal_concl FalseTerm). interprétations. *) Theorem goal_to_hyps : - forall (envp : PropList) (env : list Z) (l : hyps), + forall (envp : list Prop) (env : list int) (l : hyps), (interp_hyps envp env l -> False) -> interp_goal envp env l. - -simple induction l; +Proof. + simple induction l; [ simpl in |- *; auto | simpl in |- *; intros a l1 H1 H2 H3; apply H1; intro H4; apply H2; auto ]. Qed. Theorem hyps_to_goal : - forall (envp : PropList) (env : list Z) (l : hyps), + forall (envp : list Prop) (env : list int) (l : hyps), interp_goal envp env l -> interp_hyps envp env l -> False. - -simple induction l; simpl in |- *; [ auto | intros; apply H; elim H1; auto ]. +Proof. + simple induction l; simpl in |- *; [ auto | intros; apply H; elim H1; auto ]. Qed. (* \subsection{Manipulations sur les hypothèses} *) @@ -593,7 +1226,7 @@ Qed. (* \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 Z) (t : term), interp_term e t = interp_term e (f t). + 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 @@ -602,11 +1235,11 @@ Definition term_stable (f : term -> term) := en argument (cela suffit pour omega). *) Definition valid1 (f : proposition -> proposition) := - forall (ep : PropList) (e : list Z) (p1 : 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 : PropList) (e : list Z) (p1 p2 : 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). @@ -615,31 +1248,31 @@ Definition valid2 (f : proposition -> proposition -> proposition) := On reste contravariant *) Definition valid_hyps (f : hyps -> hyps) := - forall (ep : PropList) (e : list Z) (lp : 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 : PropList) (env : list Z) (l : hyps) (a : hyps -> hyps), +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. - -intros; simpl in |- *; apply goal_to_hyps; intro H1; +Proof. + intros; simpl in |- *; apply goal_to_hyps; intro H1; apply (hyps_to_goal ep env (a l) H0); apply H; assumption. Qed. (* \subsubsection{Généralisation a des listes de buts (disjonctions)} *) -Fixpoint interp_list_hyps (envp : PropList) (env : list Z) +Fixpoint interp_list_hyps (envp : list Prop) (env : list int) (l : lhyps) {struct l} : 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 : PropList) (env : list Z) +Fixpoint interp_list_goal (envp : list Prop) (env : list int) (l : lhyps) {struct l} : Prop := match l with | nil => True @@ -647,10 +1280,10 @@ Fixpoint interp_list_goal (envp : PropList) (env : list Z) end. Theorem list_goal_to_hyps : - forall (envp : PropList) (env : list Z) (l : lhyps), + forall (envp : list Prop) (env : list int) (l : lhyps), (interp_list_hyps envp env l -> False) -> interp_list_goal envp env l. - -simple induction l; simpl in |- *; +Proof. + simple induction l; simpl in |- *; [ auto | intros h1 l1 H H1; split; [ apply goal_to_hyps; intro H2; apply H1; auto @@ -658,37 +1291,37 @@ simple induction l; simpl in |- *; Qed. Theorem list_hyps_to_goal : - forall (envp : PropList) (env : list Z) (l : lhyps), + forall (envp : list Prop) (env : list int) (l : lhyps), interp_list_goal envp env l -> interp_list_hyps envp env l -> False. - -simple induction l; simpl in |- *; +Proof. + simple induction l; simpl in |- *; [ auto | intros h1 l1 H (H1, H2) H3; elim H3; intro H4; [ apply hyps_to_goal with (1 := H1); assumption | auto ] ]. Qed. Definition valid_list_hyps (f : hyps -> lhyps) := - forall (ep : PropList) (e : list Z) (lp : hyps), + forall (ep : list Prop) (e : list int) (lp : hyps), interp_hyps ep e lp -> interp_list_hyps ep e (f lp). Definition valid_list_goal (f : hyps -> lhyps) := - forall (ep : PropList) (e : list Z) (lp : hyps), + forall (ep : list Prop) (e : list int) (lp : hyps), interp_list_goal ep e (f lp) -> interp_goal ep e lp. Theorem goal_valid : forall f : hyps -> lhyps, valid_list_hyps f -> valid_list_goal f. - -unfold valid_list_goal in |- *; intros f H ep e lp H1; apply goal_to_hyps; +Proof. + unfold valid_list_goal in |- *; intros f H ep e lp H1; apply goal_to_hyps; intro H2; apply list_hyps_to_goal with (1 := H1); apply (H ep e lp); assumption. Qed. Theorem append_valid : - forall (ep : PropList) (e : list Z) (l1 l2 : lhyps), + forall (ep : list Prop) (e : list int) (l1 l2 : lhyps), interp_list_hyps ep e l1 \/ interp_list_hyps ep e l2 -> interp_list_hyps ep e (l1 ++ l2). - -intros ep e; simple induction l1; +Proof. + intros ep e; simple induction l1; [ simpl in |- *; intros l2 [H| H]; [ contradiction | trivial ] | simpl in |- *; intros h1 t1 HR l2 [[H| H]| H]; [ auto @@ -703,10 +1336,10 @@ Qed. Definition nth_hyps (n : nat) (l : hyps) := nth n l TrueTerm. Theorem nth_valid : - forall (ep : PropList) (e : list Z) (i : nat) (l : hyps), + forall (ep : list Prop) (e : list int) (i : nat) (l : hyps), interp_hyps ep e l -> interp_proposition ep e (nth_hyps i l). - -unfold nth_hyps in |- *; simple induction i; +Proof. + unfold nth_hyps in |- *; simple induction i; [ simple induction l; simpl in |- *; [ auto | intros; elim H0; auto ] | intros n H; simple induction l; [ simpl in |- *; trivial @@ -722,8 +1355,8 @@ Definition apply_oper_2 (i j : nat) Theorem apply_oper_2_valid : forall (i j : nat) (f : proposition -> proposition -> proposition), valid2 f -> valid_hyps (apply_oper_2 i j f). - -intros i j f Hf; unfold apply_oper_2, valid_hyps in |- *; simpl in |- *; +Proof. + intros i j f Hf; unfold apply_oper_2, valid_hyps in |- *; simpl in |- *; intros lp Hlp; split; [ apply Hf; apply nth_valid; assumption | assumption ]. Qed. @@ -743,8 +1376,8 @@ Fixpoint apply_oper_1 (i : nat) (f : proposition -> proposition) Theorem apply_oper_1_valid : forall (i : nat) (f : proposition -> proposition), valid1 f -> valid_hyps (apply_oper_1 i f). - -unfold valid_hyps in |- *; intros i f Hf ep e; elim i; +Proof. + unfold valid_hyps in |- *; intros i f Hf ep e; elim i; [ intro lp; case lp; [ simpl in |- *; trivial | simpl in |- *; intros p l' (H1, H2); split; @@ -753,7 +1386,6 @@ unfold valid_hyps in |- *; intros i f Hf ep e; elim i; [ simpl in |- *; auto | simpl in |- *; intros p l' (H1, H2); split; [ assumption | apply Hrec; assumption ] ] ]. - Qed. (* \subsubsection{Manipulations de termes} *) @@ -789,31 +1421,31 @@ Definition apply_both (f g : term -> term) (t : term) := Theorem apply_left_stable : forall f : term -> term, term_stable f -> term_stable (apply_left f). - -unfold term_stable in |- *; intros f H e t; case t; auto; simpl in |- *; +Proof. + unfold term_stable in |- *; intros f H e t; case t; auto; simpl in |- *; intros; elim H; trivial. Qed. Theorem apply_right_stable : forall f : term -> term, term_stable f -> term_stable (apply_right f). - -unfold term_stable in |- *; intros f H e t; case t; auto; simpl in |- *; +Proof. + unfold term_stable in |- *; intros f H e t; case t; auto; simpl in |- *; 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). - -unfold term_stable in |- *; intros f g H1 H2 e t; case t; auto; simpl in |- *; +Proof. + unfold term_stable in |- *; intros f g H1 H2 e t; case t; auto; simpl in |- *; 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)). - -unfold term_stable in |- *; intros f g Hf Hg e t; elim Hf; apply Hg. +Proof. + unfold term_stable in |- *; intros f g Hf Hg e t; elim Hf; apply Hg. Qed. (* \subsection{Les règles de réécriture} *) @@ -879,21 +1511,7 @@ Ltac loop t := | Tand x x0 => _ | Timp x x0 => _ | Tprop x => _ - end => - case X1; - [ intro; intro - | intro; intro - | idtac - | idtac - | intro - | intro; intro - | intro; intro - | intro; intro - | intro; intro - | intro; intro - | intro; intro - | intro; intro - | intro ]; auto; Simplify + end => destruct X1; auto; Simplify | match ?X1 with | Tint x => _ | (x + x0)%term => _ @@ -901,38 +1519,27 @@ Ltac loop t := | (x - x0)%term => _ | (- x)%term => _ | [x]%term => _ - end => - case X1; - [ intro | intro; intro | intro; intro | intro; intro | intro | intro ]; - auto; Simplify - | match ?X1 ?= ?X2 with - | Eq => _ - | Lt => _ - | Gt => _ - end => - elim_Zcompare X1 X2; intro; auto; Simplify - | match ?X1 with - | Z0 => _ - | Zpos x => _ - | Zneg x => _ - end => - case X1; [ idtac | intro | intro ]; auto; Simplify - | (if eq_Z ?X1 ?X2 then _ else _) => - elim_eq_Z X1 X2; intro H; [ rewrite H; clear H | clear H ]; + end => destruct X1; auto; Simplify + | (if beq ?X1 ?X2 then _ else _) => + let H := fresh "H" in + elim_beq X1 X2; intro H; try (rewrite H in *; clear H); simpl in |- *; auto; Simplify + | (if bgt ?X1 ?X2 then _ else _) => + let H := fresh "H" in + elim_bgt X1 X2; intro H; simpl in |- *; auto; Simplify | (if eq_term ?X1 ?X2 then _ else _) => - elim_eq_term X1 X2; intro H; [ rewrite H; clear H | clear H ]; - simpl in |- *; auto; Simplify - | (if eq_pos ?X1 ?X2 then _ else _) => - elim_eq_pos X1 X2; intro H; [ rewrite H; clear H | clear H ]; + let H := fresh "H" in + elim_eq_term X1 X2; intro H; try (rewrite H in *; clear H); simpl in |- *; auto; Simplify + | (if _ && _ then _ else _) => rewrite andb_if; Simplify + | (if negb _ then _ else _) => rewrite negb_if; Simplify | _ => fail end - with Simplify := match goal with - | |- ?X1 => try loop X1 - | _ => idtac - end. +with Simplify := match goal with + | |- ?X1 => try loop X1 + | _ => idtac + end. Ltac prove_stable x th := match constr:x with @@ -949,8 +1556,8 @@ Definition Tplus_assoc_l (t : term) := end. Theorem Tplus_assoc_l_stable : term_stable Tplus_assoc_l. - -prove_stable Tplus_assoc_l Zplus_assoc. +Proof. + prove_stable Tplus_assoc_l (ring.(Radd_assoc)). Qed. Definition Tplus_assoc_r (t : term) := @@ -960,8 +1567,8 @@ Definition Tplus_assoc_r (t : term) := end. Theorem Tplus_assoc_r_stable : term_stable Tplus_assoc_r. - -prove_stable Tplus_assoc_r Zplus_assoc_reverse. +Proof. + prove_stable Tplus_assoc_r plus_assoc_reverse. Qed. Definition Tmult_assoc_r (t : term) := @@ -971,8 +1578,8 @@ Definition Tmult_assoc_r (t : term) := end. Theorem Tmult_assoc_r_stable : term_stable Tmult_assoc_r. - -prove_stable Tmult_assoc_r Zmult_assoc_reverse. +Proof. + prove_stable Tmult_assoc_r mult_assoc_reverse. Qed. Definition Tplus_permute (t : term) := @@ -982,46 +1589,44 @@ Definition Tplus_permute (t : term) := end. Theorem Tplus_permute_stable : term_stable Tplus_permute. - -prove_stable Tplus_permute Zplus_permute. +Proof. + prove_stable Tplus_permute plus_permute. Qed. -Definition Tplus_sym (t : term) := +Definition Tplus_comm (t : term) := match t with | (x + y)%term => (y + x)%term | _ => t end. -Theorem Tplus_sym_stable : term_stable Tplus_sym. - -prove_stable Tplus_sym Zplus_comm. +Theorem Tplus_comm_stable : term_stable Tplus_comm. +Proof. + prove_stable Tplus_comm plus_comm. Qed. -Definition Tmult_sym (t : term) := +Definition Tmult_comm (t : term) := match t with | (x * y)%term => (y * x)%term | _ => t end. -Theorem Tmult_sym_stable : term_stable Tmult_sym. - -prove_stable Tmult_sym Zmult_comm. +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 => - match eq_term v v' with - | true => - (v * Tint (c1 * k1 + c2 * k2) + (l1 * Tint k1 + l2 * Tint k2))%term - | false => t - end + 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. - -prove_stable T_OMEGA10 OMEGA10. +Proof. + prove_stable T_OMEGA10 OMEGA10. Qed. Definition T_OMEGA11 (t : term) := @@ -1032,8 +1637,8 @@ Definition T_OMEGA11 (t : term) := end. Theorem T_OMEGA11_stable : term_stable T_OMEGA11. - -prove_stable T_OMEGA11 OMEGA11. +Proof. + prove_stable T_OMEGA11 OMEGA11. Qed. Definition T_OMEGA12 (t : term) := @@ -1044,52 +1649,37 @@ Definition T_OMEGA12 (t : term) := end. Theorem T_OMEGA12_stable : term_stable T_OMEGA12. - -prove_stable T_OMEGA12 OMEGA12. +Proof. + prove_stable T_OMEGA12 OMEGA12. Qed. Definition T_OMEGA13 (t : term) := match t with - | (v * Tint (Zpos x) + l1 + (v' * Tint (Zneg x') + l2))%term => - match eq_term v v' with - | true => - match eq_pos x x' with - | true => (l1 + l2)%term - | false => t - end - | false => t - end - | (v * Tint (Zneg x) + l1 + (v' * Tint (Zpos x') + l2))%term => - match eq_term v v' with - | true => - match eq_pos x x' with - | true => (l1 + l2)%term - | false => t - end - | false => t - end + | (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. - -unfold term_stable, T_OMEGA13 in |- *; intros; Simplify; simpl in |- *; - [ apply OMEGA13 | apply OMEGA14 ]. +Proof. + unfold term_stable, T_OMEGA13 in |- *; intros; Simplify; simpl in |- *; + apply OMEGA13. Qed. Definition T_OMEGA15 (t : term) := match t with | (v * Tint c1 + l1 + (v' * Tint c2 + l2) * Tint k2)%term => - match eq_term v v' with - | true => (v * Tint (c1 + c2 * k2) + (l1 + l2 * Tint k2))%term - | false => t - end + 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. - -prove_stable T_OMEGA15 OMEGA15. +Proof. + prove_stable T_OMEGA15 OMEGA15. Qed. Definition T_OMEGA16 (t : term) := @@ -1100,20 +1690,19 @@ Definition T_OMEGA16 (t : term) := Theorem T_OMEGA16_stable : term_stable T_OMEGA16. - -prove_stable T_OMEGA16 OMEGA16. +Proof. + prove_stable T_OMEGA16 OMEGA16. Qed. Definition Tred_factor5 (t : term) := match t with - | (x * Tint Z0 + y)%term => y + | (x * Tint c + y)%term => if beq c 0 then y else t | _ => t end. Theorem Tred_factor5_stable : term_stable Tred_factor5. - - -prove_stable Tred_factor5 Zred_factor5. +Proof. + prove_stable Tred_factor5 red_factor5. Qed. Definition Topp_plus (t : term) := @@ -1123,8 +1712,8 @@ Definition Topp_plus (t : term) := end. Theorem Topp_plus_stable : term_stable Topp_plus. - -prove_stable Topp_plus Zopp_plus_distr. +Proof. + prove_stable Topp_plus opp_plus_distr. Qed. @@ -1135,8 +1724,8 @@ Definition Topp_opp (t : term) := end. Theorem Topp_opp_stable : term_stable Topp_opp. - -prove_stable Topp_opp Zopp_involutive. +Proof. + prove_stable Topp_opp opp_involutive. Qed. Definition Topp_mult_r (t : term) := @@ -1146,19 +1735,19 @@ Definition Topp_mult_r (t : term) := end. Theorem Topp_mult_r_stable : term_stable Topp_mult_r. - -prove_stable Topp_mult_r Zopp_mult_distr_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 + | (- x)%term => (x * Tint (-(1)))%term | _ => t end. Theorem Topp_one_stable : term_stable Topp_one. - -prove_stable Topp_one Zopp_eq_mult_neg_1. +Proof. + prove_stable Topp_one opp_eq_mult_neg_1. Qed. Definition Tmult_plus_distr (t : term) := @@ -1168,8 +1757,8 @@ Definition Tmult_plus_distr (t : term) := end. Theorem Tmult_plus_distr_stable : term_stable Tmult_plus_distr. - -prove_stable Tmult_plus_distr Zmult_plus_distr_l. +Proof. + prove_stable Tmult_plus_distr mult_plus_distr_r. Qed. Definition Tmult_opp_left (t : term) := @@ -1179,8 +1768,8 @@ Definition Tmult_opp_left (t : term) := end. Theorem Tmult_opp_left_stable : term_stable Tmult_opp_left. - -prove_stable Tmult_opp_left Zmult_opp_comm. +Proof. + prove_stable Tmult_opp_left mult_opp_comm. Qed. Definition Tmult_assoc_reduced (t : term) := @@ -1190,91 +1779,81 @@ Definition Tmult_assoc_reduced (t : term) := end. Theorem Tmult_assoc_reduced_stable : term_stable Tmult_assoc_reduced. - -prove_stable Tmult_assoc_reduced Zmult_assoc_reverse. +Proof. + prove_stable Tmult_assoc_reduced mult_assoc_reverse. Qed. Definition Tred_factor0 (t : term) := (t * Tint 1)%term. Theorem Tred_factor0_stable : term_stable Tred_factor0. - -prove_stable Tred_factor0 Zred_factor0. +Proof. + prove_stable Tred_factor0 red_factor0. Qed. Definition Tred_factor1 (t : term) := match t with | (x + y)%term => - match eq_term x y with - | true => (x * Tint 2)%term - | false => t - end + if eq_term x y + then (x * Tint 2)%term + else t | _ => t end. Theorem Tred_factor1_stable : term_stable Tred_factor1. - -prove_stable Tred_factor1 Zred_factor1. +Proof. + prove_stable Tred_factor1 red_factor1. Qed. Definition Tred_factor2 (t : term) := match t with | (x + y * Tint k)%term => - match eq_term x y with - | true => (x * Tint (1 + k))%term - | false => t - end + if eq_term x y + then (x * Tint (1 + k))%term + else t | _ => t end. -(* Attention : il faut rendre opaque [Zplus] pour éviter que la tactique - de simplification n'aille trop loin et défasse [Zplus 1 k] *) - -Opaque Zplus. - Theorem Tred_factor2_stable : term_stable Tred_factor2. -prove_stable Tred_factor2 Zred_factor2. +Proof. + prove_stable Tred_factor2 red_factor2. Qed. Definition Tred_factor3 (t : term) := match t with | (x * Tint k + y)%term => - match eq_term x y with - | true => (x * Tint (1 + k))%term - | false => t - end + if eq_term x y + then (x * Tint (1 + k))%term + else t | _ => t end. Theorem Tred_factor3_stable : term_stable Tred_factor3. - -prove_stable Tred_factor3 Zred_factor3. +Proof. + prove_stable Tred_factor3 red_factor3. Qed. Definition Tred_factor4 (t : term) := match t with | (x * Tint k1 + y * Tint k2)%term => - match eq_term x y with - | true => (x * Tint (k1 + k2))%term - | false => t - end + if eq_term x y + then (x * Tint (k1 + k2))%term + else t | _ => t end. Theorem Tred_factor4_stable : term_stable Tred_factor4. - -prove_stable Tred_factor4 Zred_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. - -prove_stable Tred_factor6 Zred_factor6. +Proof. + prove_stable Tred_factor6 red_factor6. Qed. -Transparent Zplus. - Definition Tminus_def (t : term) := match t with | (x - y)%term => (x + - y)%term @@ -1282,9 +1861,8 @@ Definition Tminus_def (t : term) := end. Theorem Tminus_def_stable : term_stable Tminus_def. - -(* Le théorème ne sert à rien. Le but est prouvé avant. *) -prove_stable Tminus_def False. +Proof. + prove_stable Tminus_def minus_def. Qed. (* \subsection{Fonctions de réécriture complexes} *) @@ -1332,8 +1910,8 @@ Fixpoint reduce (t : term) : term := end. Theorem reduce_stable : term_stable reduce. - -unfold term_stable in |- *; intros e t; elim t; auto; +Proof. + unfold term_stable in |- *; intros e t; elim t; auto; try (intros t0 H0 t1 H1; simpl in |- *; rewrite H0; rewrite H1; (case (reduce t0); @@ -1366,8 +1944,8 @@ Fixpoint fusion (trace : list t_fusion) (t : term) {struct trace} : term := end. Theorem fusion_stable : forall t : list t_fusion, term_stable (fusion t). - -simple induction t; simpl in |- *; +Proof. + simple induction t; simpl in |- *; [ exact reduce_stable | intros stp l H; case stp; [ apply compose_term_stable; @@ -1378,7 +1956,6 @@ simple induction t; simpl in |- *; [ apply apply_right_stable; assumption | exact T_OMEGA11_stable ] | apply compose_term_stable; [ apply apply_right_stable; assumption | exact T_OMEGA12_stable ] ] ]. - Qed. (* \paragraph{Fusion de deux équations dont une sans coefficient} *) @@ -1405,8 +1982,8 @@ Fixpoint fusion_cancel (trace : nat) (t : term) {struct trace} : term := end. Theorem fusion_cancel_stable : forall t : nat, term_stable (fusion_cancel t). - -unfold term_stable, fusion_cancel in |- *; intros trace e; elim trace; +Proof. + unfold term_stable, fusion_cancel in |- *; intros trace e; elim trace; [ exact (reduce_stable e) | intros n H t; elim H; exact (T_OMEGA13_stable e t) ]. Qed. @@ -1422,8 +1999,8 @@ Fixpoint scalar_norm_add (trace : nat) (t : term) {struct trace} : term := Theorem scalar_norm_add_stable : forall t : nat, term_stable (scalar_norm_add t). - -unfold term_stable, scalar_norm_add in |- *; intros trace; elim trace; +Proof. + unfold term_stable, scalar_norm_add in |- *; intros trace; elim trace; [ exact reduce_stable | intros n H e t; elim apply_right_stable; [ exact (T_OMEGA11_stable e t) | exact H ] ]. @@ -1437,8 +2014,8 @@ Fixpoint scalar_norm (trace : nat) (t : term) {struct trace} : term := end. Theorem scalar_norm_stable : forall t : nat, term_stable (scalar_norm t). - -unfold term_stable, scalar_norm in |- *; intros trace; elim trace; +Proof. + unfold term_stable, scalar_norm in |- *; intros trace; elim trace; [ exact reduce_stable | intros n H e t; elim apply_right_stable; [ exact (T_OMEGA16_stable e t) | exact H ] ]. @@ -1452,8 +2029,8 @@ Fixpoint add_norm (trace : nat) (t : term) {struct trace} : term := end. Theorem add_norm_stable : forall t : nat, term_stable (add_norm t). - -unfold term_stable, add_norm in |- *; intros trace; elim trace; +Proof. + unfold term_stable, add_norm in |- *; 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 ] ]. @@ -1480,7 +2057,7 @@ Fixpoint rewrite (s : step) : term -> term := | C_PLUS_ASSOC_R => Tplus_assoc_r | C_PLUS_ASSOC_L => Tplus_assoc_l | C_PLUS_PERMUTE => Tplus_permute - | C_PLUS_COMM => Tplus_sym + | C_PLUS_COMM => Tplus_comm | C_RED0 => Tred_factor0 | C_RED1 => Tred_factor1 | C_RED2 => Tred_factor2 @@ -1490,12 +2067,12 @@ Fixpoint rewrite (s : step) : term -> term := | C_RED6 => Tred_factor6 | C_MULT_ASSOC_REDUCED => Tmult_assoc_reduced | C_MINUS => Tminus_def - | C_MULT_COMM => Tmult_sym + | C_MULT_COMM => Tmult_comm end. Theorem rewrite_stable : forall s : step, term_stable (rewrite s). - -simple induction s; simpl in |- *; +Proof. + simple induction s; simpl in |- *; [ intros; apply apply_both_stable; auto | intros; apply apply_left_stable; auto | intros; apply apply_right_stable; auto @@ -1512,7 +2089,7 @@ simple induction s; simpl in |- *; | exact Tplus_assoc_r_stable | exact Tplus_assoc_l_stable | exact Tplus_permute_stable - | exact Tplus_sym_stable + | exact Tplus_comm_stable | exact Tred_factor0_stable | exact Tred_factor1_stable | exact Tred_factor2_stable @@ -1522,7 +2099,7 @@ simple induction s; simpl in |- *; | exact Tred_factor6_stable | exact Tmult_assoc_reduced_stable | exact Tminus_def_stable - | exact Tmult_sym_stable ]. + | exact Tmult_comm_stable ]. Qed. (* \subsection{tactiques de résolution d'un but omega normalisé} @@ -1532,20 +2109,18 @@ Qed. Definition constant_not_nul (i : nat) (h : hyps) := match nth_hyps i h with - | EqTerm (Tint Z0) (Tint n) => - match eq_Z n 0 with - | true => h - | false => absurd - end + | EqTerm (Tint Nul) (Tint n) => + if beq n Nul then h else absurd | _ => h end. Theorem constant_not_nul_valid : forall i : nat, valid_hyps (constant_not_nul i). - -unfold valid_hyps, constant_not_nul in |- *; intros; - generalize (nth_valid ep e i lp); Simplify; simpl in |- *; - elim_eq_Z ipattern:z0 0; auto; simpl in |- *; intros H1 H2; +Proof. + unfold valid_hyps, constant_not_nul in |- *; intros; + generalize (nth_valid ep e i lp); Simplify; simpl in |- *. + + elim_beq i1 i0; auto; simpl in |- *; intros H1 H2; elim H1; symmetry in |- *; auto. Qed. @@ -1553,66 +2128,55 @@ Qed. Definition constant_neg (i : nat) (h : hyps) := match nth_hyps i h with - | LeqTerm (Tint Z0) (Tint (Zneg n)) => absurd + | 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). - -unfold valid_hyps, constant_neg in |- *; intros; - generalize (nth_valid ep e i lp); Simplify; simpl in |- *; - unfold Zle in |- *; simpl in |- *; intros H1; elim H1; - [ assumption | trivial ]. -Qed. +Proof. + unfold valid_hyps, constant_neg in |- *; intros; + generalize (nth_valid ep e i lp); Simplify; simpl in |- *. + rewrite gt_lt_iff in H0; rewrite le_lt_iff; intuition. +Qed. (* \paragraph{[NOT_EXACT_DIVIDE]} *) -Definition not_exact_divide (k1 k2 : Z) (body : term) +Definition not_exact_divide (k1 k2 : int) (body : term) (t i : nat) (l : hyps) := match nth_hyps i l with - | EqTerm (Tint Z0) b => - match - eq_term (scalar_norm_add t (body * Tint k1 + Tint k2)%term) b - with - | true => - match k2 ?= 0 with - | Gt => - match k1 ?= k2 with - | Gt => absurd - | _ => l - end - | _ => l - end - | false => l - end + | 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 + else l | _ => l end. Theorem not_exact_divide_valid : - forall (k1 k2 : Z) (body : term) (t i : nat), + forall (k1 k2 : int) (body : term) (t i : nat), valid_hyps (not_exact_divide k1 k2 body t i). - -unfold valid_hyps, not_exact_divide in |- *; intros; - generalize (nth_valid ep e i lp); Simplify; - elim_eq_term (scalar_norm_add t (body * Tint k1 + Tint k2)%term) t1; - auto; Simplify; intro H2; elim H2; simpl in |- *; - elim (scalar_norm_add_stable t e); simpl in |- *; - intro H4; absurd (interp_term e body * k1 + k2 = 0); - [ apply OMEGA4; assumption | symmetry in |- *; auto ]. - +Proof. + unfold valid_hyps, not_exact_divide in |- *; intros; + generalize (nth_valid ep e i lp); Simplify. + rewrite (scalar_norm_add_stable t 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 ]. Qed. (* \paragraph{[O_CONTRADICTION]} *) Definition contradiction (t i j : nat) (l : hyps) := match nth_hyps i l with - | LeqTerm (Tint Z0) b1 => + | LeqTerm (Tint Nul) b1 => match nth_hyps j l with - | LeqTerm (Tint Z0) b2 => + | LeqTerm (Tint Nul') b2 => match fusion_cancel t (b1 + b2)%term with - | Tint k => match 0 ?= k with - | Gt => absurd - | _ => l - end + | Tint k => if beq Nul 0 && beq Nul' 0 && bgt 0 k + then absurd + else l | _ => l end | _ => l @@ -1622,43 +2186,40 @@ Definition contradiction (t i j : nat) (l : hyps) := Theorem contradiction_valid : forall t i j : nat, valid_hyps (contradiction t i j). - -unfold valid_hyps, contradiction in |- *; intros t i j ep e l H; +Proof. + unfold valid_hyps, contradiction in |- *; 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; case z; auto; case (nth_hyps j l); - auto; intros t3 t4; case t3; auto; intros z'; case z'; - auto; simpl in |- *; intros H1 H2; + auto; case (nth_hyps j l); + auto; intros t3 t4; case t3; auto; + simpl in |- *; intros z z' H1 H2; generalize (refl_equal (interp_term e (fusion_cancel t (t2 + t4)%term))); pattern (fusion_cancel t (t2 + t4)%term) at 2 3 in |- *; case (fusion_cancel t (t2 + t4)%term); simpl in |- *; - auto; intro k; elim (fusion_cancel_stable t); simpl in |- *; - intro E; generalize (OMEGA2 _ _ H2 H1); rewrite E; - case k; auto; unfold Zle in |- *; simpl in |- *; intros p H3; - elim H3; auto. - + auto; intro k; elim (fusion_cancel_stable t); simpl in |- *. + Simplify; intro H3. + generalize (OMEGA2 _ _ H2 H1); rewrite H3. + rewrite gt_lt_iff in H0; rewrite le_lt_iff; intuition. Qed. (* \paragraph{[O_NEGATE_CONTRADICT]} *) Definition negate_contradict (i1 i2 : nat) (h : hyps) := match nth_hyps i1 h with - | EqTerm (Tint Z0) b1 => + | EqTerm (Tint Nul) b1 => match nth_hyps i2 h with - | NeqTerm (Tint Z0) b2 => - match eq_term b1 b2 with - | true => absurd - | false => h - end + | NeqTerm (Tint Nul') b2 => + if beq Nul 0 && beq Nul' 0 && eq_term b1 b2 + then absurd + else h | _ => h end - | NeqTerm (Tint Z0) b1 => + | NeqTerm (Tint Nul) b1 => match nth_hyps i2 h with - | EqTerm (Tint Z0) b2 => - match eq_term b1 b2 with - | true => absurd - | false => h - end + | EqTerm (Tint Nul') b2 => + if beq Nul 0 && beq Nul' 0 && eq_term b1 b2 + then absurd + else h | _ => h end | _ => h @@ -1666,22 +2227,22 @@ Definition negate_contradict (i1 i2 : nat) (h : hyps) := Definition negate_contradict_inv (t i1 i2 : nat) (h : hyps) := match nth_hyps i1 h with - | EqTerm (Tint Z0) b1 => + | EqTerm (Tint Nul) b1 => match nth_hyps i2 h with - | NeqTerm (Tint Z0) b2 => - match eq_term b1 (scalar_norm t (b2 * Tint (-1))%term) with - | true => absurd - | false => h - end + | 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 Z0) b1 => + | NeqTerm (Tint Nul) b1 => match nth_hyps i2 h with - | EqTerm (Tint Z0) b2 => - match eq_term b1 (scalar_norm t (b2 * Tint (-1))%term) with - | true => absurd - | false => h - end + | 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 @@ -1689,45 +2250,33 @@ Definition negate_contradict_inv (t i1 i2 : nat) (h : hyps) := Theorem negate_contradict_valid : forall i j : nat, valid_hyps (negate_contradict i j). - -unfold valid_hyps, negate_contradict in |- *; intros i j ep e l H; +Proof. + unfold valid_hyps, negate_contradict in |- *; 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; case z; auto; case (nth_hyps j l); - auto; intros t3 t4; case t3; auto; intros z'; case z'; - auto; simpl in |- *; intros H1 H2; - [ elim_eq_term t2 t4; intro H3; - [ elim H1; elim H3; assumption | assumption ] - | elim_eq_term t2 t4; intro H3; - [ elim H2; rewrite H3; assumption | assumption ] ]. - + auto; intros z; auto; case (nth_hyps j l); + auto; intros t3 t4; case t3; auto; intros z'; + auto; simpl in |- *; intros H1 H2; Simplify. Qed. Theorem negate_contradict_inv_valid : forall t i j : nat, valid_hyps (negate_contradict_inv t i j). - - -unfold valid_hyps, negate_contradict_inv in |- *; intros t i j ep e l H; +Proof. + unfold valid_hyps, negate_contradict_inv in |- *; 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; case z; auto; case (nth_hyps j l); - auto; intros t3 t4; case t3; auto; intros z'; case z'; - auto; simpl in |- *; intros H1 H2; - (pattern (eq_term t2 (scalar_norm t (t4 * Tint (-1))%term)) in |- *; - apply bool_ind2; intro Aux; - [ generalize (eq_term_true t2 (scalar_norm t (t4 * Tint (-1))%term) Aux); - clear Aux - | generalize (eq_term_false t2 (scalar_norm t (t4 * Tint (-1))%term) Aux); - clear Aux ]); - [ intro H3; elim H1; generalize H2; rewrite H3; - rewrite <- (scalar_norm_stable t e); simpl in |- *; - elim (interp_term e t4); simpl in |- *; auto; intros p H4; - discriminate H4 - | auto - | intro H3; elim H2; rewrite H3; elim (scalar_norm_stable t e); - simpl in |- *; elim H1; simpl in |- *; trivial - | auto ]. - + auto; intros z; auto; case (nth_hyps j l); + auto; intros t3 t4; case t3; auto; intros z'; + auto; simpl in |- *; 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 + ]. Qed. (* \subsubsection{Tactiques générant une nouvelle équation} *) @@ -1737,150 +2286,93 @@ Qed. preuve un peu compliquée. On utilise quelques lemmes qui sont des généralisations des théorèmes utilisés par OMEGA. *) -Definition sum (k1 k2 : Z) (trace : list t_fusion) +Definition sum (k1 k2 : int) (trace : list t_fusion) (prop1 prop2 : proposition) := match prop1 with - | EqTerm (Tint Z0) b1 => + | EqTerm (Tint Null) b1 => match prop2 with - | EqTerm (Tint Z0) b2 => - EqTerm (Tint 0) (fusion trace (b1 * Tint k1 + b2 * Tint k2)%term) - | LeqTerm (Tint Z0) b2 => - match k2 ?= 0 with - | Gt => - LeqTerm (Tint 0) + | EqTerm (Tint Null') b2 => + if beq Null 0 && beq Null' 0 + then EqTerm (Tint 0) (fusion trace (b1 * Tint k1 + b2 * Tint k2)%term) + 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) - | _ => TrueTerm - end + else TrueTerm | _ => TrueTerm end - | LeqTerm (Tint Z0) b1 => - match k1 ?= 0 with - | Gt => - match prop2 with - | EqTerm (Tint Z0) b2 => + | LeqTerm (Tint Null) b1 => + if beq Null 0 && bgt k1 0 + 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) - | LeqTerm (Tint Z0) b2 => - match k2 ?= 0 with - | Gt => - LeqTerm (Tint 0) + 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) - | _ => TrueTerm - end + else TrueTerm | _ => TrueTerm end - | _ => TrueTerm - end - | NeqTerm (Tint Z0) b1 => + else TrueTerm + | NeqTerm (Tint Null) b1 => match prop2 with - | EqTerm (Tint Z0) b2 => - match eq_Z k1 0 with - | true => TrueTerm - | false => - NeqTerm (Tint 0) - (fusion trace (b1 * Tint k1 + b2 * Tint k2)%term) - end + | 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) + else TrueTerm | _ => TrueTerm end | _ => TrueTerm end. -Theorem sum1 : forall a b c d : Z, 0 = a -> 0 = b -> 0 = a * c + b * d. - -intros; elim H; elim H0; simpl in |- *; auto. -Qed. - -Theorem sum2 : - forall a b c d : Z, 0 <= d -> 0 = a -> 0 <= b -> 0 <= a * c + b * d. - -intros; elim H0; simpl in |- *; generalize H H1; case b; case d; - unfold Zle in |- *; simpl in |- *; auto. -Qed. - -Theorem sum3 : - forall a b c d : Z, - 0 <= c -> 0 <= d -> 0 <= a -> 0 <= b -> 0 <= a * c + b * d. - -intros a b c d; case a; case b; case c; case d; unfold Zle in |- *; - simpl in |- *; auto. -Qed. - -Theorem sum4 : forall k : Z, (k ?= 0) = Gt -> 0 <= k. - -intro; case k; unfold Zle in |- *; simpl in |- *; auto; intros; discriminate. -Qed. - -Theorem sum5 : - forall a b c d : Z, c <> 0 -> 0 <> a -> 0 = b -> 0 <> a * c + b * d. - -intros a b c d H1 H2 H3; elim H3; simpl in |- *; rewrite Zplus_comm; - simpl in |- *; generalize H1 H2; case a; case c; simpl in |- *; - intros; try discriminate; assumption. -Qed. - Theorem sum_valid : - forall (k1 k2 : Z) (t : list t_fusion), valid2 (sum k1 k2 t). - -unfold valid2 in |- *; intros k1 k2 t ep e p1 p2; unfold sum in |- *; + forall (k1 k2 : int) (t : list t_fusion), valid2 (sum k1 k2 t). +Proof. + unfold valid2 in |- *; intros k1 k2 t ep e p1 p2; unfold sum in |- *; Simplify; simpl in |- *; auto; try elim (fusion_stable t); simpl in |- *; intros; [ apply sum1; assumption | apply sum2; try assumption; apply sum4; assumption - | rewrite Zplus_comm; apply sum2; try assumption; apply sum4; assumption + | rewrite plus_comm; apply sum2; try assumption; apply sum4; assumption | apply sum3; try assumption; apply sum4; assumption - | elim_eq_Z k1 0; simpl in |- *; auto; elim (fusion_stable t); simpl in |- *; - intros; unfold Zne in |- *; apply sum5; 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 : Z) (body : term) (t : nat) +Definition exact_divide (k : int) (body : term) (t : nat) (prop : proposition) := match prop with - | EqTerm (Tint Z0) b => - match eq_term (scalar_norm t (body * Tint k)%term) b with - | true => - match eq_Z k 0 with - | true => TrueTerm - | false => EqTerm (Tint 0) body - end - | false => TrueTerm - end - | NeqTerm (Tint Z0) b => - match eq_term (scalar_norm t (body * Tint k)%term) b with - | true => - match eq_Z k 0 with - | true => FalseTerm - | false => NeqTerm (Tint 0) body - end - | false => TrueTerm - end + | 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 : Z) (t : term) (n : nat), valid1 (exact_divide k t n). - - -unfold valid1, exact_divide in |- *; intros k1 k2 t ep e p1; Simplify; - simpl in |- *; auto; elim_eq_term (scalar_norm t (k2 * Tint k1)%term) t1; - simpl in |- *; auto; elim_eq_Z k1 0; simpl in |- *; - auto; intros H1 H2; elim H2; elim scalar_norm_stable; - simpl in |- *; - [ - generalize H1; case (interp_term e k2); - try trivial; - (case k1; simpl in |- *; - [ intros; absurd (0 = 0); assumption - | intros p2 p3 H3 H4; discriminate H4 - | intros p2 p3 H3 H4; discriminate H4 ]) - | - subst k1; rewrite Zmult_comm; simpl in *; intros; absurd (0=0); trivial - | - generalize H1; case (interp_term e k2); - try trivial; intros p2 p3 H3 H4; discriminate H4 + forall (k : int) (t : term) (n : nat), valid1 (exact_divide k t n). +Proof. + unfold valid1, exact_divide in |- *; intros k1 k2 t ep e p1; + Simplify; simpl; auto; subst; + rewrite <- scalar_norm_stable; simpl; intros; + [ destruct (mult_integral _ _ (sym_eq H0)); intuition + | contradict H0; rewrite <- H0, mult_0_l; auto ]. Qed. @@ -1889,61 +2381,51 @@ Qed. 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 : Z) (body : term) +Definition divide_and_approx (k1 k2 : int) (body : term) (t : nat) (prop : proposition) := match prop with - | LeqTerm (Tint Z0) b => - match - eq_term (scalar_norm_add t (body * Tint k1 + Tint k2)%term) b - with - | true => - match k1 ?= 0 with - | Gt => - match k1 ?= k2 with - | Gt => LeqTerm (Tint 0) body - | _ => prop - end - | _ => prop - end - | false => prop - end + | 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 : Z) (body : term) (t : nat), + forall (k1 k2 : int) (body : term) (t : nat), valid1 (divide_and_approx k1 k2 body t). - -unfold valid1, divide_and_approx in |- *; intros k1 k2 body t ep e p1; - Simplify; - elim_eq_term (scalar_norm_add t (body * Tint k1 + Tint k2)%term) t1; - Simplify; auto; intro E; elim E; simpl in |- *; - elim (scalar_norm_add_stable t e); simpl in |- *; - intro H1; apply Zmult_le_approx with (3 := H1); assumption. +Proof. + unfold valid1, divide_and_approx in |- *; intros k1 k2 body t ep e p1; + Simplify; simpl; auto; subst; + elim (scalar_norm_add_stable t e); simpl in |- *. + intro H2; apply mult_le_approx with (3 := H2); assumption. Qed. (* \paragraph{[MERGE_EQ]} *) Definition merge_eq (t : nat) (prop1 prop2 : proposition) := match prop1 with - | LeqTerm (Tint Z0) b1 => + | LeqTerm (Tint Null) b1 => match prop2 with - | LeqTerm (Tint Z0) b2 => - match eq_term b1 (scalar_norm t (b2 * Tint (-1))%term) with - | true => EqTerm (Tint 0) b1 - | false => TrueTerm - end + | LeqTerm (Tint Null') b2 => + if beq Null 0 && beq Null' 0 && + eq_term b1 (scalar_norm t (b2 * Tint (-(1)))%term) + then EqTerm (Tint 0) b1 + else TrueTerm | _ => TrueTerm end | _ => TrueTerm end. Theorem merge_eq_valid : forall n : nat, valid2 (merge_eq n). - -unfold valid2, merge_eq in |- *; intros n ep e p1 p2; Simplify; simpl in |- *; +Proof. + unfold valid2, merge_eq in |- *; intros n ep e p1 p2; Simplify; simpl in |- *; auto; elim (scalar_norm_stable n e); simpl in |- *; intros; symmetry in |- *; apply OMEGA8 with (2 := H0); - [ assumption | elim Zopp_eq_mult_neg_1; trivial ]. + [ assumption | elim opp_eq_mult_neg_1; trivial ]. Qed. @@ -1952,36 +2434,39 @@ Qed. Definition constant_nul (i : nat) (h : hyps) := match nth_hyps i h with - | NeqTerm (Tint Z0) (Tint Z0) => absurd + | 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). - -unfold valid_hyps, constant_nul in |- *; intros; +Proof. + unfold valid_hyps, constant_nul in |- *; intros; generalize (nth_valid ep e i lp); Simplify; simpl in |- *; - unfold Zne in |- *; intro H1; absurd (0 = 0); auto. + intro H1; absurd (0 = 0); intuition. Qed. (* \paragraph{[O_STATE]} *) -Definition state (m : Z) (s : step) (prop1 prop2 : proposition) := +Definition state (m : int) (s : step) (prop1 prop2 : proposition) := match prop1 with - | EqTerm (Tint Z0) b1 => + | EqTerm (Tint Null) b1 => match prop2 with | EqTerm b2 b3 => - EqTerm (Tint 0) (rewrite s (b1 + (- b3 + b2) * Tint m)%term) + if beq Null 0 + then EqTerm (Tint 0) (rewrite s (b1 + (- b3 + b2) * Tint m)%term) + else TrueTerm | _ => TrueTerm end | _ => TrueTerm end. -Theorem state_valid : forall (m : Z) (s : step), valid2 (state m s). - -unfold valid2 in |- *; intros m s ep e p1 p2; unfold state in |- *; Simplify; +Theorem state_valid : forall (m : int) (s : step), valid2 (state m s). +Proof. + unfold valid2 in |- *; intros m s ep e p1 p2; unfold state in |- *; Simplify; simpl in |- *; auto; elim (rewrite_stable s e); simpl in |- *; intros H1 H2; elim H1. - rewrite H2; rewrite Zplus_opp_l; simpl; reflexivity. + now rewrite H2, plus_opp_l, plus_0_l, mult_0_l. Qed. (* \subsubsection{Tactiques générant plusieurs but} @@ -1991,11 +2476,13 @@ Qed. Definition split_ineq (i t : nat) (f1 f2 : hyps -> lhyps) (l : hyps) := match nth_hyps i l with - | NeqTerm (Tint Z0) b1 => - f1 (LeqTerm (Tint 0) (add_norm t (b1 + Tint (-1))%term) :: l) ++ + | 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) + (scalar_norm_add t (b1 * Tint (-(1)) + Tint (-(1)))%term) :: l) + else l :: nil | _ => l :: nil end. @@ -2003,17 +2490,18 @@ Theorem split_ineq_valid : forall (i t : nat) (f1 f2 : hyps -> lhyps), valid_list_hyps f1 -> valid_list_hyps f2 -> valid_list_hyps (split_ineq i t f1 f2). - -unfold valid_list_hyps, split_ineq in |- *; intros i t f1 f2 H1 H2 ep e lp H; +Proof. + unfold valid_list_hyps, split_ineq in |- *; intros i t f1 f2 H1 H2 ep e lp H; generalize (nth_valid _ _ i _ H); case (nth_hyps i lp); simpl in |- *; auto; intros t1 t2; case t1; simpl in |- *; - auto; intros z; case z; simpl in |- *; auto; intro H3; + auto; intros z; simpl in |- *; auto; intro H3. + Simplify. apply append_valid; elim (OMEGA19 (interp_term e t2)); [ intro H4; left; apply H1; simpl in |- *; elim (add_norm_stable t); simpl in |- *; auto | intro H4; right; apply H2; simpl in |- *; elim (scalar_norm_add_stable t); simpl in |- *; auto - | generalize H3; unfold Zne, not in |- *; intros E1 E2; apply E1; + | generalize H3; unfold not in |- *; intros E1 E2; apply E1; symmetry in |- *; trivial ]. Qed. @@ -2046,8 +2534,8 @@ Fixpoint execute_omega (t : t_omega) (l : hyps) {struct t} : lhyps := end. Theorem omega_valid : forall t : t_omega, valid_list_hyps (execute_omega t). - -simple induction t; simpl in |- *; +Proof. + simple induction t; simpl in |- *; [ unfold valid_list_hyps in |- *; simpl in |- *; intros; left; apply (constant_not_nul_valid n ep e lp H) | unfold valid_list_hyps in |- *; simpl in |- *; intros; left; @@ -2058,7 +2546,7 @@ simple induction t; simpl in |- *; (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 in |- *; simpl in |- *; intros; left; - apply (not_exact_divide_valid z z0 t0 n n0 ep e lp H) + apply (not_exact_divide_valid i i0 t0 n n0 ep e lp H) | unfold valid_list_hyps, valid_hyps in |- *; intros k body n t' Ht' m ep e lp H; apply Ht'; apply @@ -2101,36 +2589,30 @@ Definition move_right (s : step) (p : proposition) := | EqTerm t1 t2 => EqTerm (Tint 0) (rewrite s (t1 + - t2)%term) | LeqTerm t1 t2 => LeqTerm (Tint 0) (rewrite s (t2 + - t1)%term) | GeqTerm t1 t2 => LeqTerm (Tint 0) (rewrite s (t1 + - t2)%term) - | LtTerm t1 t2 => LeqTerm (Tint 0) (rewrite s (t2 + Tint (-1) + - t1)%term) - | GtTerm t1 t2 => LeqTerm (Tint 0) (rewrite s (t1 + Tint (-1) + - t2)%term) + | LtTerm t1 t2 => LeqTerm (Tint 0) (rewrite s (t2 + Tint (-(1)) + - t1)%term) + | GtTerm t1 t2 => LeqTerm (Tint 0) (rewrite s (t1 + Tint (-(1)) + - t2)%term) | NeqTerm t1 t2 => NeqTerm (Tint 0) (rewrite s (t1 + - t2)%term) | p => p end. -Theorem Zne_left_2 : forall x y : Z, Zne x y -> Zne 0 (x + - y). -unfold Zne, not in |- *; intros x y H1 H2; apply H1; - apply (Zplus_reg_l (- y)); rewrite Zplus_comm; elim H2; - rewrite Zplus_opp_l; trivial. -Qed. - Theorem move_right_valid : forall s : step, valid1 (move_right s). - -unfold valid1, move_right in |- *; intros s ep e p; Simplify; simpl in |- *; +Proof. + unfold valid1, move_right in |- *; intros s ep e p; Simplify; simpl in |- *; elim (rewrite_stable s e); simpl in |- *; - [ symmetry in |- *; apply Zegal_left; assumption - | intro; apply Zle_left; assumption - | intro; apply Zge_left; assumption - | intro; apply Zgt_left; assumption - | intro; apply Zlt_left; assumption - | intro; apply Zne_left_2; assumption ]. + [ symmetry in |- *; 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). - -intros; unfold do_normalize in |- *; apply apply_oper_1_valid; +Proof. + intros; unfold do_normalize in |- *; apply apply_oper_1_valid; apply move_right_valid. Qed. @@ -2143,43 +2625,40 @@ Fixpoint do_normalize_list (l : list step) (i : nat) Theorem do_normalize_list_valid : forall (l : list step) (i : nat), valid_hyps (do_normalize_list l i). - -simple induction l; simpl in |- *; unfold valid_hyps in |- *; +Proof. + simple induction l; simpl in |- *; unfold valid_hyps in |- *; [ 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 : PropList) (env : list Z) (l : hyps), + 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. - -intros; apply valid_goal with (2 := H); apply do_normalize_list_valid. +Proof. + intros; apply valid_goal with (2 := H); apply do_normalize_list_valid. Qed. (* \subsubsection{Exécution de la trace} *) Theorem execute_goal : - forall (t : t_omega) (ep : PropList) (env : list Z) (l : hyps), + forall (t : t_omega) (ep : list Prop) (env : list int) (l : hyps), interp_list_goal ep env (execute_omega t l) -> interp_goal ep env l. - -intros; apply (goal_valid (execute_omega t) (omega_valid t) ep env l H). +Proof. + intros; apply (goal_valid (execute_omega t) (omega_valid t) ep env l H). Qed. Theorem append_goal : - forall (ep : PropList) (e : list Z) (l1 l2 : lhyps), + 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). - -intros ep e; simple induction l1; +Proof. + intros ep e; simple induction l1; [ simpl in |- *; intros l2 (H1, H2); assumption | simpl in |- *; intros h1 t1 HR l2 ((H1, H2), H3); split; auto ]. - Qed. -Require Import Decidable. - (* 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 @@ -2203,30 +2682,29 @@ Fixpoint decidability (p : proposition) : bool := end. Theorem decidable_correct : - forall (ep : PropList) (e : list Z) (p : proposition), + forall (ep : list Prop) (e : list int) (p : proposition), decidability p = true -> decidable (interp_proposition ep e p). - -simple induction p; simpl in |- *; intros; +Proof. + simple induction p; simpl in |- *; intros; [ apply dec_eq - | apply dec_Zle + | apply dec_le | left; auto | right; unfold not in |- *; auto | apply dec_not; auto - | apply dec_Zge - | apply dec_Zgt - | apply dec_Zlt - | apply dec_Zne + | 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 : PropList) (env : list Z) +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 @@ -2234,7 +2712,7 @@ Fixpoint interp_full_goal (envp : PropList) (env : list Z) interp_proposition envp env p' -> interp_full_goal envp env c l' end. -Definition interp_full (ep : PropList) (e : list Z) +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 @@ -2244,12 +2722,11 @@ Definition interp_full (ep : PropList) (e : list Z) of its hypothesis and conclusion *) Theorem interp_full_false : - forall (ep : PropList) (e : list Z) (l : hyps) (c : proposition), + 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). - -simple induction l; unfold interp_full in |- *; simpl in |- *; +Proof. + simple induction l; unfold interp_full in |- *; simpl in |- *; [ auto | intros a l1 H1 c H2 H3; apply H1; auto ]. - Qed. (* Push the conclusion in the list of hypothesis using a double negation @@ -2265,11 +2742,11 @@ Definition to_contradict (lc : hyps * proposition) := hypothesis implies the original goal *) Theorem to_contradict_valid : - forall (ep : PropList) (e : list Z) (lc : hyps * proposition), + forall (ep : list Prop) (e : list int) (lc : hyps * proposition), interp_goal ep e (to_contradict lc) -> interp_full ep e lc. - -intros ep e lc; case lc; intros l c; simpl in |- *; - pattern (decidability c) in |- *; apply bool_ind2; +Proof. + intros ep e lc; case lc; intros l c; simpl in |- *; + pattern (decidability c) in |- *; apply bool_eq_ind; [ simpl in |- *; intros H H1; apply interp_full_false; intros H2; apply not_not; [ apply decidable_correct; assumption @@ -2333,19 +2810,19 @@ Fixpoint destructure_hyps (nn : nat) (ll : hyps) {struct nn} : lhyps := end. Theorem map_cons_val : - forall (ep : PropList) (e : list Z) (p : proposition) (l : lhyps), + 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). - -simple induction l; simpl in |- *; [ auto | intros; elim H1; intro H2; auto ]. +Proof. + simple induction l; simpl in |- *; [ 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). - -simple induction n; +Proof. + simple induction n; [ unfold valid_list_hyps in |- *; simpl in |- *; auto | unfold valid_list_hyps at 2 in |- *; intros n1 H ep e lp; case lp; [ simpl in |- *; auto @@ -2358,7 +2835,7 @@ simple induction n; (simpl in |- *; intros; apply map_cons_val; simpl in |- *; elim H0; auto); [ simpl in |- *; intros p1 (H1, H2); - pattern (decidability p1) in |- *; apply bool_ind2; + pattern (decidability p1) in |- *; apply bool_eq_ind; intro H3; [ apply H; simpl in |- *; split; [ apply not_not; auto | assumption ] @@ -2366,7 +2843,7 @@ simple induction n; | simpl in |- *; intros p1 p2 (H1, H2); apply H; simpl in |- *; elim not_or with (1 := H1); auto | simpl in |- *; intros p1 p2 (H1, H2); - pattern (decidability p1) in |- *; apply bool_ind2; + pattern (decidability p1) in |- *; apply bool_eq_ind; intro H3; [ apply append_valid; elim not_and with (2 := H1); [ intro; left; apply H; simpl in |- *; auto @@ -2378,18 +2855,17 @@ simple induction n; apply H; simpl in |- *; auto | simpl in |- *; intros; apply H; simpl in |- *; tauto | simpl in |- *; intros p1 p2 (H1, H2); - pattern (decidability p1) in |- *; apply bool_ind2; + pattern (decidability p1) in |- *; apply bool_eq_ind; intro H3; [ apply append_valid; elim imp_simp with (2 := H1); [ intro H4; left; simpl in |- *; apply H; simpl in |- *; auto | intro H4; right; simpl in |- *; apply H; simpl in |- *; auto | auto ] | auto ] ] ] ]. - Qed. Definition prop_stable (f : proposition -> proposition) := - forall (ep : PropList) (e : list Z) (p : 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) @@ -2405,8 +2881,8 @@ Definition p_apply_left (f : proposition -> proposition) Theorem p_apply_left_stable : forall f : proposition -> proposition, prop_stable f -> prop_stable (p_apply_left f). - -unfold prop_stable in |- *; intros f H ep e p; split; +Proof. + unfold prop_stable in |- *; intros f H ep e p; split; (case p; simpl in |- *; auto; intros p1; elim (H ep e p1); tauto). Qed. @@ -2423,8 +2899,8 @@ Definition p_apply_right (f : proposition -> proposition) Theorem p_apply_right_stable : forall f : proposition -> proposition, prop_stable f -> prop_stable (p_apply_right f). - -unfold prop_stable in |- *; intros f H ep e p; split; +Proof. + unfold prop_stable in |- *; intros f H ep e p; split; (case p; simpl in |- *; auto; [ intros p1; elim (H ep e p1); tauto | intros p1 p2; elim (H ep e p2); tauto @@ -2447,67 +2923,55 @@ Definition p_invert (f : proposition -> proposition) Theorem p_invert_stable : forall f : proposition -> proposition, prop_stable f -> prop_stable (p_invert f). - -unfold prop_stable in |- *; intros f H ep e p; split; +Proof. + unfold prop_stable in |- *; intros f H ep e p; split; (case p; simpl in |- *; auto; [ intros t1 t2; elim (H ep e (NeqTerm t1 t2)); simpl in |- *; - unfold Zne in |- *; generalize (dec_eq (interp_term e t1) (interp_term e t2)); unfold decidable in |- *; tauto | intros t1 t2; elim (H ep e (GtTerm t1 t2)); simpl in |- *; - unfold Zgt in |- *; - generalize (dec_Zgt (interp_term e t1) (interp_term e t2)); - unfold decidable, Zgt, Zle in |- *; tauto + generalize (dec_gt (interp_term e t1) (interp_term e t2)); + unfold decidable in |- *; rewrite le_lt_iff, <- gt_lt_iff; tauto | intros t1 t2; elim (H ep e (LtTerm t1 t2)); simpl in |- *; - unfold Zlt in |- *; - generalize (dec_Zlt (interp_term e t1) (interp_term e t2)); - unfold decidable, Zge in |- *; tauto + generalize (dec_lt (interp_term e t1) (interp_term e t2)); + unfold decidable in |- *; rewrite ge_le_iff, le_lt_iff; tauto | intros t1 t2; elim (H ep e (LeqTerm t1 t2)); simpl in |- *; - generalize (dec_Zgt (interp_term e t1) (interp_term e t2)); - unfold Zle, Zgt in |- *; unfold decidable in |- *; - tauto + generalize (dec_gt (interp_term e t1) (interp_term e t2)); + unfold decidable in |- *; repeat rewrite le_lt_iff; + repeat rewrite gt_lt_iff; tauto | intros t1 t2; elim (H ep e (GeqTerm t1 t2)); simpl in |- *; - generalize (dec_Zlt (interp_term e t1) (interp_term e t2)); - unfold Zge, Zlt in |- *; unfold decidable in |- *; - tauto + generalize (dec_lt (interp_term e t1) (interp_term e t2)); + unfold decidable in |- *; repeat rewrite ge_le_iff; + repeat rewrite le_lt_iff; tauto | intros t1 t2; elim (H ep e (EqTerm t1 t2)); simpl in |- *; generalize (dec_eq (interp_term e t1) (interp_term e t2)); - unfold decidable, Zne in |- *; tauto ]). -Qed. - -Theorem Zlt_left_inv : forall x y : Z, 0 <= y + -1 + - x -> x < y. - -intros; apply Zsucc_lt_reg; apply Zle_lt_succ; - apply (fun a b : Z => Zplus_le_reg_r a b (-1 + - x)); - rewrite Zplus_assoc; unfold Zsucc in |- *; rewrite (Zplus_assoc_reverse x); - rewrite (Zplus_assoc y); simpl in |- *; rewrite Zplus_0_r; - rewrite Zplus_opp_r; assumption. + unfold decidable; tauto ]). Qed. Theorem move_right_stable : forall s : step, prop_stable (move_right s). - -unfold move_right, prop_stable in |- *; intros s ep e p; split; +Proof. + unfold move_right, prop_stable in |- *; intros s ep e p; split; [ Simplify; simpl in |- *; elim (rewrite_stable s e); simpl in |- *; - [ symmetry in |- *; apply Zegal_left; assumption - | intro; apply Zle_left; assumption - | intro; apply Zge_left; assumption - | intro; apply Zgt_left; assumption - | intro; apply Zlt_left; assumption - | intro; apply Zne_left_2; assumption ] + [ symmetry in |- *; 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 in |- *; intros; auto; generalize H; elim (rewrite_stable s); simpl in |- *; intro H1; - [ rewrite (Zplus_0_r_reverse (interp_term e t0)); rewrite H1; - rewrite Zplus_permute; rewrite Zplus_opp_r; - rewrite Zplus_0_r; trivial - | apply (fun a b : Z => Zplus_le_reg_r a b (- interp_term e t)); - rewrite Zplus_opp_r; assumption - | apply Zle_ge; - apply (fun a b : Z => Zplus_le_reg_r a b (- interp_term e t0)); - rewrite Zplus_opp_r; assumption - | apply Zlt_gt; apply Zlt_left_inv; assumption - | apply Zlt_left_inv; assumption - | unfold Zne, not in |- *; unfold Zne in H1; intro H2; apply H1; - rewrite H2; rewrite Zplus_opp_r; trivial ] ]. + [ rewrite (plus_0_r_reverse (interp_term e t0)); 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 t)); + rewrite plus_opp_r; assumption + | rewrite ge_le_iff; + apply (fun a b => plus_le_reg_r a b (- interp_term e t0)); + rewrite plus_opp_r; assumption + | rewrite gt_lt_iff; apply lt_left_inv; assumption + | apply lt_left_inv; assumption + | unfold not in |- *; intro H2; apply H1; + rewrite H2; rewrite plus_opp_r; trivial ] ]. Qed. @@ -2521,9 +2985,8 @@ Fixpoint p_rewrite (s : p_step) : proposition -> proposition := end. Theorem p_rewrite_stable : forall s : p_step, prop_stable (p_rewrite s). - - -simple induction s; simpl in |- *; +Proof. + simple induction s; simpl in |- *; [ intros; apply p_apply_left_stable; trivial | intros; apply p_apply_right_stable; trivial | intros; apply p_invert_stable; apply move_right_stable @@ -2539,8 +3002,8 @@ Fixpoint normalize_hyps (l : list h_step) (lh : hyps) {struct l} : hyps := Theorem normalize_hyps_valid : forall l : list h_step, valid_hyps (normalize_hyps l). - -simple induction l; unfold valid_hyps in |- *; simpl in |- *; +Proof. + simple induction l; unfold valid_hyps in |- *; simpl in |- *; [ auto | intros n_s r; case n_s; intros n s H ep e lp H1; apply H; apply apply_oper_1_valid; @@ -2550,10 +3013,10 @@ simple induction l; unfold valid_hyps in |- *; simpl in |- *; Qed. Theorem normalize_hyps_goal : - forall (s : list h_step) (ep : PropList) (env : list Z) (l : hyps), + 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. - -intros; apply valid_goal with (2 := H); apply normalize_hyps_valid. +Proof. + intros; apply valid_goal with (2 := H); apply normalize_hyps_valid. Qed. Fixpoint extract_hyp_pos (s : list direction) (p : proposition) {struct s} : @@ -2604,18 +3067,18 @@ Fixpoint extract_hyp_pos (s : list direction) (p : proposition) {struct s} : end. Definition co_valid1 (f : proposition -> proposition) := - forall (ep : PropList) (e : list Z) (p1 : 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). - -unfold valid1, co_valid1 in |- *; simple induction s; +Proof. + unfold valid1, co_valid1 in |- *; simple induction s; [ split; [ simpl in |- *; auto | intros ep e p1; case p1; simpl in |- *; auto; intro p; - pattern (decidability p) in |- *; apply bool_ind2; + pattern (decidability p) in |- *; apply bool_eq_ind; [ intro H; generalize (decidable_correct ep e p H); unfold decidable in |- *; tauto | simpl in |- *; auto ] ] @@ -2623,12 +3086,11 @@ unfold valid1, co_valid1 in |- *; simple induction s; case p; auto; simpl in |- *; intros; (apply H1; tauto) || (apply H2; tauto) || - (pattern (decidability p0) in |- *; apply bool_ind2; + (pattern (decidability p0) in |- *; apply bool_eq_ind; [ intro H3; generalize (decidable_correct ep e p0 H3); unfold decidable in |- *; intro H4; apply H1; tauto | intro; tauto ]) ]. - Qed. Fixpoint decompose_solve (s : e_step) (h : hyps) {struct s} : lhyps := @@ -2655,13 +3117,13 @@ Fixpoint decompose_solve (s : e_step) (h : hyps) {struct s} : lhyps := Theorem decompose_solve_valid : forall s : e_step, valid_list_goal (decompose_solve s). - -intro s; apply goal_valid; unfold valid_list_hyps in |- *; elim s; +Proof. + intro s; apply goal_valid; unfold valid_list_hyps in |- *; elim s; simpl in |- *; intros; [ cut (interp_proposition ep e1 (extract_hyp_pos l (nth_hyps n lp))); [ case (extract_hyp_pos l (nth_hyps n lp)); simpl in |- *; auto; [ intro p; case p; simpl in |- *; auto; intros p1 p2 H2; - pattern (decidability p1) in |- *; apply bool_ind2; + pattern (decidability p1) in |- *; 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 in |- *; tauto @@ -2671,7 +3133,7 @@ intro s; apply goal_valid; unfold valid_list_hyps in |- *; elim s; [ intros H3; left; apply H; simpl in |- *; auto | intros H3; right; apply H0; simpl in |- *; auto ] | intros p1 p2 H2; - pattern (decidability p1) in |- *; apply bool_ind2; + pattern (decidability p1) in |- *; 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 in |- *; tauto @@ -2687,7 +3149,7 @@ Qed. (* \subsection{La dernière étape qui élimine tous les séquents inutiles} *) Definition valid_lhyps (f : lhyps -> lhyps) := - forall (ep : PropList) (e : list Z) (lp : lhyps), + forall (ep : list Prop) (e : list int) (lp : lhyps), interp_list_hyps ep e lp -> interp_list_hyps ep e (f lp). Fixpoint reduce_lhyps (lp : lhyps) : lhyps := @@ -2698,8 +3160,8 @@ Fixpoint reduce_lhyps (lp : lhyps) : lhyps := end. Theorem reduce_lhyps_valid : valid_lhyps reduce_lhyps. - -unfold valid_lhyps in |- *; intros ep e lp; elim lp; +Proof. + unfold valid_lhyps in |- *; intros ep e lp; elim lp; [ simpl in |- *; auto | intros a l HR; elim a; [ simpl in |- *; tauto @@ -2707,10 +3169,10 @@ unfold valid_lhyps in |- *; intros ep e lp; elim lp; Qed. Theorem do_reduce_lhyps : - forall (envp : PropList) (env : list Z) (l : lhyps), + forall (envp : list Prop) (env : list int) (l : lhyps), interp_list_goal envp env (reduce_lhyps l) -> interp_list_goal envp env l. - -intros envp env l H; apply list_goal_to_hyps; intro H1; +Proof. + intros envp env l H; apply list_goal_to_hyps; intro H1; apply list_hyps_to_goal with (1 := H); apply reduce_lhyps_valid; assumption. Qed. @@ -2719,13 +3181,13 @@ Definition concl_to_hyp (p : proposition) := if decidability p then Tnot p else TrueTerm. Definition do_concl_to_hyp : - forall (envp : PropList) (env : list Z) (c : proposition) (l : hyps), + forall (envp : list Prop) (env : list int) (c : proposition) (l : hyps), interp_goal envp env (concl_to_hyp c :: l) -> interp_goal_concl c envp env l. - -simpl in |- *; intros envp env c l; induction l as [| a l Hrecl]; +Proof. + simpl in |- *; intros envp env c l; induction l as [| a l Hrecl]; [ simpl in |- *; unfold concl_to_hyp in |- *; - pattern (decidability c) in |- *; apply bool_ind2; + pattern (decidability c) in |- *; apply bool_eq_ind; [ intro H; generalize (decidable_correct envp env c H); unfold decidable in |- *; simpl in |- *; tauto | simpl in |- *; intros H1 H2; elim H2; trivial ] @@ -2737,12 +3199,19 @@ Definition omega_tactic (t1 : e_step) (t2 : list h_step) reduce_lhyps (decompose_solve t1 (normalize_hyps t2 (concl_to_hyp c :: l))). Theorem do_omega : - forall (t1 : e_step) (t2 : list h_step) (envp : PropList) - (env : list Z) (c : proposition) (l : hyps), + forall (t1 : e_step) (t2 : list h_step) (envp : list Prop) + (env : list int) (c : proposition) (l : hyps), interp_list_goal envp env (omega_tactic t1 t2 c l) -> interp_goal_concl c envp env l. - -unfold omega_tactic in |- *; intros; apply do_concl_to_hyp; +Proof. + unfold omega_tactic in |- *; intros; apply do_concl_to_hyp; apply (normalize_hyps_goal t2); apply (decompose_solve_valid t1); apply do_reduce_lhyps; assumption. Qed. + +End IntOmega. + +(* For now, the above modular construction is instanciated on Z, + in order to retrieve the initial ROmega. *) + +Module ZOmega := IntOmega(Z_as_Int). |