diff options
Diffstat (limited to 'plugins/romega')
| -rw-r--r-- | plugins/romega/README | 6 | ||||
| -rw-r--r-- | plugins/romega/ROmega.v | 14 | ||||
| -rw-r--r-- | plugins/romega/ReflOmegaCore.v | 3216 | ||||
| -rw-r--r-- | plugins/romega/const_omega.ml | 352 | ||||
| -rw-r--r-- | plugins/romega/const_omega.mli | 176 | ||||
| -rw-r--r-- | plugins/romega/g_romega.ml4 | 42 | ||||
| -rw-r--r-- | plugins/romega/refl_omega.ml | 1299 | ||||
| -rw-r--r-- | plugins/romega/romega_plugin.mllib | 4 | ||||
| -rw-r--r-- | plugins/romega/vo.itarget | 2 |
9 files changed, 5111 insertions, 0 deletions
diff --git a/plugins/romega/README b/plugins/romega/README new file mode 100644 index 00000000..86c9e58a --- /dev/null +++ b/plugins/romega/README @@ -0,0 +1,6 @@ +This work was done for the RNRT Project Calife. +As such it is distributed under the LGPL licence. + +Report bugs to : + pierre.cregut@francetelecom.com + diff --git a/plugins/romega/ROmega.v b/plugins/romega/ROmega.v new file mode 100644 index 00000000..3ddb6bed --- /dev/null +++ b/plugins/romega/ROmega.v @@ -0,0 +1,14 @@ +(************************************************************************* + + PROJET RNRT Calife - 2001 + Author: Pierre Crégut - France Télécom R&D + Licence : LGPL version 2.1 + + *************************************************************************) + +Require Import ReflOmegaCore. +Require Export Setoid. +Require Export PreOmega. +Require Export ZArith_base. +Require Import OmegaPlugin. +Declare ML Module "romega_plugin".
\ No newline at end of file diff --git a/plugins/romega/ReflOmegaCore.v b/plugins/romega/ReflOmegaCore.v new file mode 100644 index 00000000..c82abfc8 --- /dev/null +++ b/plugins/romega/ReflOmegaCore.v @@ -0,0 +1,3216 @@ +(* -*- coding: utf-8 -*- *) +(************************************************************************* + + PROJET RNRT Calife - 2001 + Author: Pierre Crégut - France Télécom R&D + Licence du projet : LGPL version 2.1 + + *************************************************************************) + +Require Import List Bool Sumbool EqNat Setoid Ring_theory Decidable ZArith_base. +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. + + 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; exfalso. + + rewrite lt_0_neg' in Hn. + rewrite lt_0_neg' in Hm. + generalize (mult_lt_0_compat _ _ Hn Hm). + rewrite <- opp_mult_distr_r, mult_comm, <- opp_mult_distr_r, opp_involutive. + rewrite mult_comm, H. + exact (lt_irrefl 0). + + rewrite lt_0_neg' in Hn. + generalize (mult_lt_0_compat _ _ Hn Hm). + rewrite mult_comm, <- opp_mult_distr_r, mult_comm. + rewrite H. + rewrite opp_eq_mult_neg_1, mult_0_l. + exact (lt_irrefl 0). + + rewrite lt_0_neg' in Hm. + generalize (mult_lt_0_compat _ _ Hn Hm). + rewrite <- opp_mult_distr_r. + rewrite H. + rewrite opp_eq_mult_neg_1, mult_0_l. + exact (lt_irrefl 0). + + generalize (mult_lt_0_compat _ _ Hn Hm). + rewrite H. + exact (lt_irrefl 0). + 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{Definition of reified integer expressions} + Terms are either: + \begin{itemize} + \item integers [Tint] + \item variables [Tvar] + \item operation over integers (addition, product, opposite, subtraction) + The last two are translated in additions and products. *) + +Inductive term : Set := + | Tint : int -> term + | Tplus : term -> term -> term + | Tmult : term -> term -> term + | Tminus : term -> term -> term + | Topp : term -> term + | 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]. +Arguments Scope Topp [romega_scope romega_scope]. + +Infix "+" := Tplus : romega_scope. +Infix "*" := Tmult : romega_scope. +Infix "-" := Tminus : romega_scope. +Notation "- x" := (Topp x) : 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 (* 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 + | NeqTerm : term -> term -> proposition + | Tor : proposition -> proposition -> proposition + | Tand : proposition -> proposition -> proposition + | Timp : proposition -> proposition -> proposition + | Tprop : nat -> proposition. + +(* Definition of goals as a list of hypothesis *) +Notation hyps := (list proposition). + +(* Definition of lists of subgoals (set of open goals) *) +Notation lhyps := (list hyps). + +(* a single goal packed in a subgoal list *) +Notation singleton := (fun a : hyps => a :: nil). + +(* an absurd goal *) +Definition absurd := FalseTerm :: nil. + +(* \subsubsection{Traces for merging equations} + This inductive type describes how the monomial of two equations should be + merged when the equations are added. + + For [F_equal], both equations have the same head variable and coefficient + must be added, furthermore if coefficients are opposite, [F_cancel] should + be used to collapse the term. [F_left] and [F_right] indicate which monomial + should be put first in the result *) + +Inductive t_fusion : Set := + | F_equal : t_fusion + | F_cancel : t_fusion + | F_left : t_fusion + | F_right : t_fusion. + +(* \subsubsection{Rewriting steps to normalize terms} *) +Inductive step : Set := + (* apply the rewriting steps to both subterms of an operation *) + | C_DO_BOTH : step -> step -> step + (* apply the rewriting step to the first branch *) + | C_LEFT : step -> step + (* apply the rewriting step to the second branch *) + | C_RIGHT : step -> step + (* apply two steps consecutively to a term *) + | C_SEQ : step -> step -> step + (* empty step *) + | C_NOP : step + (* the following operations correspond to actual rewriting *) + | C_OPP_PLUS : step + | C_OPP_OPP : step + | C_OPP_MULT_R : step + | C_OPP_ONE : step + (* This is a special step that reduces the term (computation) *) + | C_REDUCE : step + | C_MULT_PLUS_DISTR : step + | C_MULT_OPP_LEFT : step + | C_MULT_ASSOC_R : step + | C_PLUS_ASSOC_R : step + | C_PLUS_ASSOC_L : step + | C_PLUS_PERMUTE : step + | C_PLUS_COMM : step + | C_RED0 : step + | C_RED1 : step + | C_RED2 : step + | C_RED3 : step + | C_RED4 : step + | C_RED5 : step + | C_RED6 : step + | C_MULT_ASSOC_REDUCED : step + | C_MINUS : step + | C_MULT_COMM : step. + +(* \subsubsection{Omega steps} *) +(* The following inductive type describes steps as they can be found in + the trace coming from the decision procedure Omega. *) + +Inductive t_omega : Set := + (* n = 0 and n!= 0 *) + | O_CONSTANT_NOT_NUL : nat -> t_omega + | O_CONSTANT_NEG : nat -> t_omega + (* division and approximation of an equation *) + | O_DIV_APPROX : int -> int -> term -> nat -> t_omega -> nat -> t_omega + (* no solution because no exact division *) + | O_NOT_EXACT_DIVIDE : int -> int -> term -> nat -> nat -> t_omega + (* exact division *) + | O_EXACT_DIVIDE : int -> term -> nat -> t_omega -> nat -> t_omega + | O_SUM : int -> nat -> int -> nat -> list t_fusion -> t_omega -> t_omega + | O_CONTRADICTION : nat -> nat -> nat -> t_omega + | O_MERGE_EQ : nat -> nat -> nat -> t_omega -> t_omega + | O_SPLIT_INEQ : nat -> nat -> t_omega -> t_omega -> t_omega + | O_CONSTANT_NUL : nat -> t_omega + | O_NEGATE_CONTRADICT : nat -> nat -> t_omega + | O_NEGATE_CONTRADICT_INV : nat -> nat -> nat -> t_omega + | O_STATE : int -> step -> nat -> nat -> t_omega -> t_omega. + +(* \subsubsection{Rules for normalizing the hypothesis} *) +(* These rules indicate how to normalize useful propositions + of each useful hypothesis before the decomposition of hypothesis. + The rules include the inversion phase for negation removal. *) + +Inductive p_step : Set := + | P_LEFT : p_step -> p_step + | P_RIGHT : p_step -> p_step + | P_INVERT : step -> p_step + | P_STEP : step -> p_step + | P_NOP : p_step. + +(* List of normalizations to perform : 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{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. + +(* 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{Efficient decidable equality} *) +(* For each reified data-type, we define an efficient equality test. + It is not the one produced by [Decide Equality]. + + Then we prove two theorem allowing 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} *) + +(* \subsubsection{Reified terms} *) + +Open Scope romega_scope. + +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. + +Close Scope romega_scope. + +Theorem eq_term_true : forall t1 t2 : term, eq_term t1 t2 = true -> t1 = t2. +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 + | intros t21 t22 H3; elim andb_prop with (1 := H3); intros H4 H5; + elim H with (1 := H4); elim H0 with (1 := H5); + 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 + | intros t21 H3; elim H with (1 := H3); 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. +Proof. + simple induction t1; + [ intros z t2; case t2; try trivial_case; simpl in |- *; unfold not in |- *; + 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; + elim andb_false_elim with (1 := H3); intros H5; + [ elim H1 with (1 := H5); simplify_eq H4; auto + | elim H2 with (1 := H5); simplify_eq H4; auto ] + | intros t11 H1 t12 H2 t2; case t2; try trivial_case; simpl in |- *; + intros t21 t22 H3; unfold not in |- *; intro H4; + elim andb_false_elim with (1 := H3); intros H5; + [ elim H1 with (1 := H5); simplify_eq H4; auto + | elim H2 with (1 := H5); simplify_eq H4; auto ] + | intros t11 H1 t12 H2 t2; case t2; try trivial_case; simpl in |- *; + intros t21 t22 H3; unfold not in |- *; intro H4; + elim andb_false_elim with (1 := H3); intros H5; + [ elim H1 with (1 := H5); simplify_eq H4; auto + | elim H2 with (1 := H5); simplify_eq H4; auto ] + | intros t11 H1 t2; case t2; try trivial_case; simpl in |- *; intros t21 H3; + 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 beq_nat_false with (1 := H); simplify_eq H0; + auto ]. +Qed. + +(* \subsubsection{Tactiques pour éliminer ces tests} + + Si on se contente de faire un [Case (eq_typ t1 t2)] on perd + totalement dans chaque branche le fait que [t1=t2] ou [~t1=t2]. + + Initialement, les développements avaient été réalisés avec les + tests rendus par [Decide Equality], c'est à dire un test rendant + des termes du type [{t1=t2}+{~t1=t2}]. Faire une élimination sur un + tel test préserve bien l'information voulue mais calculatoirement de + telles fonctions sont trop lentes. *) + +(* Les tactiques définies si après se comportent exactement comme si on + avait utilisé le test précédent et fait une elimination dessus. *) + +Ltac elim_eq_term t1 t2 := + 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_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 ]. + +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 ]. + + +(* \subsection{Interprétations} + \subsubsection{Interprétation des termes dans 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 + | (t1 * t2)%term => interp_term env t1 * interp_term env t2 + | (t1 - t2)%term => interp_term env t1 - interp_term env t2 + | (- t)%term => - interp_term env t + | [n]%term => nth n env 0 + end. + +(* \subsubsection{Interprétation des prédicats} *) + +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 + | LeqTerm t1 t2 => interp_term env t1 <= interp_term env t2 + | TrueTerm => True + | FalseTerm => False + | Tnot p' => ~ interp_proposition envp env p' + | GeqTerm t1 t2 => interp_term env t1 >= interp_term env t2 + | GtTerm t1 t2 => interp_term env t1 > interp_term env t2 + | LtTerm t1 t2 => interp_term env t1 < interp_term env t2 + | NeqTerm t1 t2 => (interp_term env t1)<>(interp_term env t2) + | Tor p1 p2 => + interp_proposition envp env p1 \/ interp_proposition envp env p2 + | Tand p1 p2 => + interp_proposition envp env p1 /\ interp_proposition envp env p2 + | Timp p1 p2 => + interp_proposition envp env p1 -> interp_proposition envp env p2 + | Tprop n => nth n envp True + end. + +(* \subsubsection{Inteprétation des listes d'hypothèses} + \paragraph{Sous forme de conjonction} + Interprétation sous forme d'une conjonction d'hypothèses plus faciles + à manipuler individuellement *) + +Fixpoint interp_hyps (envp : list Prop) (env : list int) + (l : hyps) {struct l} : Prop := + match l with + | nil => True + | p' :: l' => interp_proposition envp env p' /\ interp_hyps envp env l' + end. + +(* \paragraph{sous forme de but} + C'est cette interpétation que l'on utilise sur le but (car on utilise + [Generalize] et qu'une conjonction est forcément lourde (répétition des + types dans les conjonctions intermédiaires) *) + +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' => + interp_proposition envp env p' -> interp_goal_concl c envp env l' + end. + +Notation interp_goal := (interp_goal_concl FalseTerm). + +(* Les théorèmes qui suivent assurent la correspondance entre les deux + interprétations. *) + +Theorem goal_to_hyps : + forall (envp : list Prop) (env : list int) (l : hyps), + (interp_hyps envp env l -> False) -> interp_goal envp env l. +Proof. + simple induction l; + [ simpl in |- *; auto + | simpl in |- *; intros a l1 H1 H2 H3; apply H1; intro H4; apply H2; auto ]. +Qed. + +Theorem hyps_to_goal : + forall (envp : list Prop) (env : list int) (l : hyps), + interp_goal envp env l -> interp_hyps envp env l -> False. +Proof. + simple induction l; simpl in |- *; [ auto | intros; apply H; elim H1; auto ]. +Qed. + +(* \subsection{Manipulations sur les hypothèses} *) + +(* \subsubsection{Définitions de base de stabilité pour la réflexion} *) +(* Une opération laisse un terme stable si l'égalité est préservée *) +Definition term_stable (f : term -> term) := + forall (e : list int) (t : term), interp_term e t = interp_term e (f t). + +(* Une opération est valide sur une hypothèse, si l'hypothèse implique le + résultat de l'opération. \emph{Attention : cela ne concerne que des + opérations sur les hypothèses et non sur les buts (contravariance)}. + On définit la validité pour une opération prenant une ou deux propositions + en argument (cela suffit pour omega). *) + +Definition valid1 (f : proposition -> proposition) := + forall (ep : list Prop) (e : list int) (p1 : proposition), + interp_proposition ep e p1 -> interp_proposition ep e (f p1). + +Definition valid2 (f : proposition -> proposition -> proposition) := + forall (ep : list Prop) (e : list int) (p1 p2 : proposition), + interp_proposition ep e p1 -> + interp_proposition ep e p2 -> interp_proposition ep e (f p1 p2). + +(* Dans cette notion de validité, la fonction prend directement une + liste de propositions et rend une nouvelle liste de proposition. + On reste contravariant *) + +Definition valid_hyps (f : hyps -> hyps) := + forall (ep : list Prop) (e : list int) (lp : hyps), + interp_hyps ep e lp -> interp_hyps ep e (f lp). + +(* Enfin ce théorème élimine la contravariance et nous ramène à une + opération sur les buts *) + +Theorem valid_goal : + forall (ep : list Prop) (env : list int) (l : hyps) (a : hyps -> hyps), + valid_hyps a -> interp_goal ep env (a l) -> interp_goal ep env l. +Proof. + intros; simpl 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 : 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 : list Prop) (env : list int) + (l : lhyps) {struct l} : Prop := + match l with + | nil => True + | h :: l' => interp_goal envp env h /\ interp_list_goal envp env l' + end. + +Theorem list_goal_to_hyps : + forall (envp : list Prop) (env : list int) (l : lhyps), + (interp_list_hyps envp env l -> False) -> interp_list_goal envp env l. +Proof. + simple induction l; simpl in |- *; + [ auto + | intros h1 l1 H H1; split; + [ apply goal_to_hyps; intro H2; apply H1; auto + | apply H; intro H2; apply H1; auto ] ]. +Qed. + +Theorem list_hyps_to_goal : + forall (envp : list Prop) (env : list int) (l : lhyps), + interp_list_goal envp env l -> interp_list_hyps envp env l -> False. +Proof. + simple induction l; simpl 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 : 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 : 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. +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 : 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). +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 + | right; apply (HR l2); left; trivial + | right; apply (HR l2); right; trivial ] ]. + +Qed. + +(* \subsubsection{Opérateurs valides sur les hypothèses} *) + +(* Extraire une hypothèse de la liste *) +Definition nth_hyps (n : nat) (l : hyps) := nth n l TrueTerm. + +Theorem nth_valid : + forall (ep : list Prop) (e : list int) (i : nat) (l : hyps), + interp_hyps ep e l -> interp_proposition ep e (nth_hyps i l). +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 + | intros; simpl in |- *; apply H; elim H1; auto ] ]. +Qed. + +(* Appliquer une opération (valide) sur deux hypothèses extraites de + la liste et ajouter le résultat à la liste. *) +Definition apply_oper_2 (i j : nat) + (f : proposition -> proposition -> proposition) (l : hyps) := + f (nth_hyps i l) (nth_hyps j l) :: l. + +Theorem apply_oper_2_valid : + forall (i j : nat) (f : proposition -> proposition -> proposition), + valid2 f -> valid_hyps (apply_oper_2 i j f). +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. + +(* Modifier une hypothèse par application d'une opération valide *) + +Fixpoint apply_oper_1 (i : nat) (f : proposition -> proposition) + (l : hyps) {struct i} : hyps := + match l with + | nil => nil (A:=proposition) + | p :: l' => + match i with + | O => f p :: l' + | S j => p :: apply_oper_1 j f l' + end + end. + +Theorem apply_oper_1_valid : + forall (i : nat) (f : proposition -> proposition), + valid1 f -> valid_hyps (apply_oper_1 i f). +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; + [ apply Hf with (1 := H1) | assumption ] ] + | intros n Hrec lp; case lp; + [ simpl in |- *; auto + | simpl in |- *; intros p l' (H1, H2); split; + [ assumption | apply Hrec; assumption ] ] ]. +Qed. + +(* \subsubsection{Manipulations de termes} *) +(* Les fonctions suivantes permettent d'appliquer une fonction de + réécriture sur un sous terme du terme principal. Avec la composition, + cela permet de construire des réécritures complexes proches des + tactiques de conversion *) + +Definition apply_left (f : term -> term) (t : term) := + match t with + | (x + y)%term => (f x + y)%term + | (x * y)%term => (f x * y)%term + | (- x)%term => (- f x)%term + | x => x + end. + +Definition apply_right (f : term -> term) (t : term) := + match t with + | (x + y)%term => (x + f y)%term + | (x * y)%term => (x * f y)%term + | x => x + end. + +Definition apply_both (f g : term -> term) (t : term) := + match t with + | (x + y)%term => (f x + g y)%term + | (x * y)%term => (f x * g y)%term + | x => x + end. + +(* Les théorèmes suivants montrent la stabilité (conditionnée) des + fonctions. *) + +Theorem apply_left_stable : + forall f : term -> term, term_stable f -> term_stable (apply_left f). +Proof. + unfold term_stable 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). +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). +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)). +Proof. + unfold term_stable in |- *; intros f g Hf Hg e t; elim Hf; apply Hg. +Qed. + +(* \subsection{Les règles de réécriture} *) +(* Chacune des règles de réécriture est accompagnée par sa preuve de + stabilité. Toutes ces preuves ont la même forme : il faut analyser + suivant la forme du terme (élimination de chaque Case). On a besoin d'une + élimination uniquement dans les cas d'utilisation d'égalité décidable. + + Cette tactique itère la décomposition des Case. Elle est + constituée de deux fonctions s'appelant mutuellement : + \begin{itemize} + \item une fonction d'enrobage qui lance la recherche sur le but, + \item une fonction récursive qui décompose ce but. Quand elle a trouvé un + Case, elle l'élimine. + \end{itemize} + Les motifs sur les cas sont très imparfaits et dans certains cas, il + semble que cela ne marche pas. On aimerait plutot un motif de la + forme [ Case (?1 :: T) of _ end ] permettant de s'assurer que l'on + utilise le bon type. + + Chaque élimination introduit correctement exactement le nombre d'hypothèses + nécessaires et conserve dans le cas d'une égalité la connaissance du + résultat du test en faisant la réécriture. Pour un test de comparaison, + on conserve simplement le résultat. + + Cette fonction déborde très largement la résolution des réécritures + simples et fait une bonne partie des preuves des pas de Omega. +*) + +(* \subsubsection{La tactique pour prouver la stabilité} *) + +Ltac loop t := + match t with + (* Global *) + | (?X1 = ?X2) => loop X1 || loop X2 + | (_ -> ?X1) => loop X1 + (* Interpretations *) + | (interp_hyps _ _ ?X1) => loop X1 + | (interp_list_hyps _ _ ?X1) => loop X1 + | (interp_proposition _ _ ?X1) => loop X1 + | (interp_term _ ?X1) => loop X1 + (* Propositions *) + | (EqTerm ?X1 ?X2) => loop X1 || loop X2 + | (LeqTerm ?X1 ?X2) => loop X1 || loop X2 + (* Termes *) + | (?X1 + ?X2)%term => loop X1 || loop X2 + | (?X1 - ?X2)%term => loop X1 || loop X2 + | (?X1 * ?X2)%term => loop X1 || loop X2 + | (- ?X1)%term => loop X1 + | (Tint ?X1) => loop X1 + (* Eliminations *) + | match ?X1 with + | EqTerm x x0 => _ + | LeqTerm x x0 => _ + | TrueTerm => _ + | FalseTerm => _ + | Tnot x => _ + | GeqTerm x x0 => _ + | GtTerm x x0 => _ + | LtTerm x x0 => _ + | NeqTerm x x0 => _ + | Tor x x0 => _ + | Tand x x0 => _ + | Timp x x0 => _ + | Tprop x => _ + end => destruct X1; auto; Simplify + | match ?X1 with + | Tint x => _ + | (x + x0)%term => _ + | (x * x0)%term => _ + | (x - x0)%term => _ + | (- x)%term => _ + | [x]%term => _ + 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 _) => + 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. + +Ltac prove_stable x th := + match constr:x with + | ?X1 => + unfold term_stable, X1 in |- *; intros; Simplify; simpl in |- *; + apply th + end. + +(* \subsubsection{Les règles elle mêmes} *) +Definition Tplus_assoc_l (t : term) := + match t with + | (n + (m + p))%term => (n + m + p)%term + | _ => t + end. + +Theorem Tplus_assoc_l_stable : term_stable Tplus_assoc_l. +Proof. + prove_stable Tplus_assoc_l (ring.(Radd_assoc)). +Qed. + +Definition Tplus_assoc_r (t : term) := + match t with + | (n + m + p)%term => (n + (m + p))%term + | _ => t + end. + +Theorem Tplus_assoc_r_stable : term_stable Tplus_assoc_r. +Proof. + prove_stable Tplus_assoc_r plus_assoc_reverse. +Qed. + +Definition Tmult_assoc_r (t : term) := + match t with + | (n * m * p)%term => (n * (m * p))%term + | _ => t + end. + +Theorem Tmult_assoc_r_stable : term_stable Tmult_assoc_r. +Proof. + prove_stable Tmult_assoc_r mult_assoc_reverse. +Qed. + +Definition Tplus_permute (t : term) := + match t with + | (n + (m + p))%term => (m + (n + p))%term + | _ => t + end. + +Theorem Tplus_permute_stable : term_stable Tplus_permute. +Proof. + prove_stable Tplus_permute plus_permute. +Qed. + +Definition Tplus_comm (t : term) := + match t with + | (x + y)%term => (y + x)%term + | _ => t + end. + +Theorem Tplus_comm_stable : term_stable Tplus_comm. +Proof. + prove_stable Tplus_comm plus_comm. +Qed. + +Definition Tmult_comm (t : term) := + match t with + | (x * y)%term => (y * x)%term + | _ => t + end. + +Theorem Tmult_comm_stable : term_stable Tmult_comm. +Proof. + prove_stable Tmult_comm mult_comm. +Qed. + +Definition T_OMEGA10 (t : term) := + match t with + | ((v * Tint c1 + l1) * Tint k1 + (v' * Tint c2 + l2) * Tint k2)%term => + if eq_term v v' + then (v * Tint (c1 * k1 + c2 * k2)%I + (l1 * Tint k1 + l2 * Tint k2))%term + else t + | _ => t + end. + +Theorem T_OMEGA10_stable : term_stable T_OMEGA10. +Proof. + prove_stable T_OMEGA10 OMEGA10. +Qed. + +Definition T_OMEGA11 (t : term) := + match t with + | ((v1 * Tint c1 + l1) * Tint k1 + l2)%term => + (v1 * Tint (c1 * k1) + (l1 * Tint k1 + l2))%term + | _ => t + end. + +Theorem T_OMEGA11_stable : term_stable T_OMEGA11. +Proof. + prove_stable T_OMEGA11 OMEGA11. +Qed. + +Definition T_OMEGA12 (t : term) := + match t with + | (l1 + (v2 * Tint c2 + l2) * Tint k2)%term => + (v2 * Tint (c2 * k2) + (l1 + l2 * Tint k2))%term + | _ => t + end. + +Theorem T_OMEGA12_stable : term_stable T_OMEGA12. +Proof. + prove_stable T_OMEGA12 OMEGA12. +Qed. + +Definition T_OMEGA13 (t : term) := + match t with + | (v * Tint x + l1 + (v' * Tint x' + l2))%term => + if eq_term v v' && beq x (-x') + then (l1+l2)%term + else t + | _ => t + end. + +Theorem T_OMEGA13_stable : term_stable T_OMEGA13. +Proof. + unfold term_stable, T_OMEGA13 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 => + if eq_term v v' + then (v * Tint (c1 + c2 * k2)%I + (l1 + l2 * Tint k2))%term + else t + | _ => t + end. + +Theorem T_OMEGA15_stable : term_stable T_OMEGA15. +Proof. + prove_stable T_OMEGA15 OMEGA15. +Qed. + +Definition T_OMEGA16 (t : term) := + match t with + | ((v * Tint c + l) * Tint k)%term => (v * Tint (c * k) + l * Tint k)%term + | _ => t + end. + + +Theorem T_OMEGA16_stable : term_stable T_OMEGA16. +Proof. + prove_stable T_OMEGA16 OMEGA16. +Qed. + +Definition Tred_factor5 (t : term) := + match t with + | (x * Tint c + y)%term => if beq c 0 then y else t + | _ => t + end. + +Theorem Tred_factor5_stable : term_stable Tred_factor5. +Proof. + prove_stable Tred_factor5 red_factor5. +Qed. + +Definition Topp_plus (t : term) := + match t with + | (- (x + y))%term => (- x + - y)%term + | _ => t + end. + +Theorem Topp_plus_stable : term_stable Topp_plus. +Proof. + prove_stable Topp_plus opp_plus_distr. +Qed. + + +Definition Topp_opp (t : term) := + match t with + | (- - x)%term => x + | _ => t + end. + +Theorem Topp_opp_stable : term_stable Topp_opp. +Proof. + prove_stable Topp_opp opp_involutive. +Qed. + +Definition Topp_mult_r (t : term) := + match t with + | (- (x * Tint k))%term => (x * Tint (- k))%term + | _ => t + end. + +Theorem Topp_mult_r_stable : term_stable Topp_mult_r. +Proof. + prove_stable Topp_mult_r opp_mult_distr_r. +Qed. + +Definition Topp_one (t : term) := + match t with + | (- x)%term => (x * Tint (-(1)))%term + | _ => t + end. + +Theorem Topp_one_stable : term_stable Topp_one. +Proof. + prove_stable Topp_one opp_eq_mult_neg_1. +Qed. + +Definition Tmult_plus_distr (t : term) := + match t with + | ((n + m) * p)%term => (n * p + m * p)%term + | _ => t + end. + +Theorem Tmult_plus_distr_stable : term_stable Tmult_plus_distr. +Proof. + prove_stable Tmult_plus_distr mult_plus_distr_r. +Qed. + +Definition Tmult_opp_left (t : term) := + match t with + | (- x * Tint y)%term => (x * Tint (- y))%term + | _ => t + end. + +Theorem Tmult_opp_left_stable : term_stable Tmult_opp_left. +Proof. + prove_stable Tmult_opp_left mult_opp_comm. +Qed. + +Definition Tmult_assoc_reduced (t : term) := + match t with + | (n * Tint m * Tint p)%term => (n * Tint (m * p))%term + | _ => t + end. + +Theorem Tmult_assoc_reduced_stable : term_stable Tmult_assoc_reduced. +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. +Proof. + prove_stable Tred_factor0 red_factor0. +Qed. + +Definition Tred_factor1 (t : term) := + match t with + | (x + y)%term => + if eq_term x y + then (x * Tint 2)%term + else t + | _ => t + end. + +Theorem Tred_factor1_stable : term_stable Tred_factor1. +Proof. + prove_stable Tred_factor1 red_factor1. +Qed. + +Definition Tred_factor2 (t : term) := + match t with + | (x + y * Tint k)%term => + if eq_term x y + then (x * Tint (1 + k))%term + else t + | _ => t + end. + +Theorem Tred_factor2_stable : term_stable Tred_factor2. +Proof. + prove_stable Tred_factor2 red_factor2. +Qed. + +Definition Tred_factor3 (t : term) := + match t with + | (x * Tint k + y)%term => + if eq_term x y + then (x * Tint (1 + k))%term + else t + | _ => t + end. + +Theorem Tred_factor3_stable : term_stable Tred_factor3. +Proof. + prove_stable Tred_factor3 red_factor3. +Qed. + + +Definition Tred_factor4 (t : term) := + match t with + | (x * Tint k1 + y * Tint k2)%term => + if eq_term x y + then (x * Tint (k1 + k2))%term + else t + | _ => t + end. + +Theorem Tred_factor4_stable : term_stable Tred_factor4. +Proof. + prove_stable Tred_factor4 red_factor4. +Qed. + +Definition Tred_factor6 (t : term) := (t + Tint 0)%term. + +Theorem Tred_factor6_stable : term_stable Tred_factor6. +Proof. + prove_stable Tred_factor6 red_factor6. +Qed. + +Definition Tminus_def (t : term) := + match t with + | (x - y)%term => (x + - y)%term + | _ => t + end. + +Theorem Tminus_def_stable : term_stable Tminus_def. +Proof. + prove_stable Tminus_def minus_def. +Qed. + +(* \subsection{Fonctions de réécriture complexes} *) + +(* \subsubsection{Fonction de réduction} *) +(* Cette fonction réduit un terme dont la forme normale est un entier. Il + suffit pour cela d'échanger le constructeur [Tint] avec les opérateurs + réifiés. La réduction est ``gratuite''. *) + +Fixpoint reduce (t : term) : term := + match t with + | (x + y)%term => + match reduce x with + | Tint x' => + match reduce y with + | Tint y' => Tint (x' + y') + | y' => (Tint x' + y')%term + end + | x' => (x' + reduce y)%term + end + | (x * y)%term => + match reduce x with + | Tint x' => + match reduce y with + | Tint y' => Tint (x' * y') + | y' => (Tint x' * y')%term + end + | x' => (x' * reduce y)%term + end + | (x - y)%term => + match reduce x with + | Tint x' => + match reduce y with + | Tint y' => Tint (x' - y') + | y' => (Tint x' - y')%term + end + | x' => (x' - reduce y)%term + end + | (- x)%term => + match reduce x with + | Tint x' => Tint (- x') + | x' => (- x')%term + end + | _ => t + end. + +Theorem reduce_stable : term_stable reduce. +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); + [ intro z0; case (reduce t1); intros; auto + | intros; auto + | intros; auto + | intros; auto + | intros; auto + | intros; auto ])); intros t0 H0; simpl in |- *; + rewrite H0; case (reduce t0); intros; auto. +Qed. + +(* \subsubsection{Fusions} + \paragraph{Fusion de deux équations} *) +(* On donne une somme de deux équations qui sont supposées normalisées. + Cette fonction prend une trace de fusion en argument et transforme + le terme en une équation normalisée. C'est une version très simplifiée + du moteur de réécriture [rewrite]. *) + +Fixpoint fusion (trace : list t_fusion) (t : term) {struct trace} : term := + match trace with + | nil => reduce t + | step :: trace' => + match step with + | F_equal => apply_right (fusion trace') (T_OMEGA10 t) + | F_cancel => fusion trace' (Tred_factor5 (T_OMEGA10 t)) + | F_left => apply_right (fusion trace') (T_OMEGA11 t) + | F_right => apply_right (fusion trace') (T_OMEGA12 t) + end + end. + +Theorem fusion_stable : forall t : list t_fusion, term_stable (fusion t). +Proof. + simple induction t; simpl in |- *; + [ exact reduce_stable + | intros stp l H; case stp; + [ apply compose_term_stable; + [ apply apply_right_stable; assumption | exact T_OMEGA10_stable ] + | unfold term_stable in |- *; intros e t1; rewrite T_OMEGA10_stable; + rewrite Tred_factor5_stable; apply H + | apply compose_term_stable; + [ apply apply_right_stable; assumption | exact T_OMEGA11_stable ] + | apply compose_term_stable; + [ apply apply_right_stable; assumption | exact T_OMEGA12_stable ] ] ]. +Qed. + +(* \paragraph{Fusion de deux équations dont une sans coefficient} *) + +Definition fusion_right (trace : list t_fusion) (t : term) : term := + match trace with + | nil => reduce t (* Il faut mettre un compute *) + | step :: trace' => + match step with + | F_equal => apply_right (fusion trace') (T_OMEGA15 t) + | F_cancel => fusion trace' (Tred_factor5 (T_OMEGA15 t)) + | F_left => apply_right (fusion trace') (Tplus_assoc_r t) + | F_right => apply_right (fusion trace') (T_OMEGA12 t) + end + end. + +(* \paragraph{Fusion avec annihilation} *) +(* Normalement le résultat est une constante *) + +Fixpoint fusion_cancel (trace : nat) (t : term) {struct trace} : term := + match trace with + | O => reduce t + | S trace' => fusion_cancel trace' (T_OMEGA13 t) + end. + +Theorem fusion_cancel_stable : forall t : nat, term_stable (fusion_cancel t). +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. + +(* \subsubsection{Opérations affines sur une équation} *) +(* \paragraph{Multiplication scalaire et somme d'une constante} *) + +Fixpoint scalar_norm_add (trace : nat) (t : term) {struct trace} : term := + match trace with + | O => reduce t + | S trace' => apply_right (scalar_norm_add trace') (T_OMEGA11 t) + end. + +Theorem scalar_norm_add_stable : + forall t : nat, term_stable (scalar_norm_add t). +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 ] ]. +Qed. + +(* \paragraph{Multiplication scalaire} *) +Fixpoint scalar_norm (trace : nat) (t : term) {struct trace} : term := + match trace with + | O => reduce t + | S trace' => apply_right (scalar_norm trace') (T_OMEGA16 t) + end. + +Theorem scalar_norm_stable : forall t : nat, term_stable (scalar_norm t). +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 ] ]. +Qed. + +(* \paragraph{Somme d'une constante} *) +Fixpoint add_norm (trace : nat) (t : term) {struct trace} : term := + match trace with + | O => reduce t + | S trace' => apply_right (add_norm trace') (Tplus_assoc_r t) + end. + +Theorem add_norm_stable : forall t : nat, term_stable (add_norm t). +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 ] ]. +Qed. + +(* \subsection{La fonction de normalisation des termes (moteur de réécriture)} *) + + +Fixpoint rewrite (s : step) : term -> term := + match s with + | C_DO_BOTH s1 s2 => apply_both (rewrite s1) (rewrite s2) + | C_LEFT s => apply_left (rewrite s) + | C_RIGHT s => apply_right (rewrite s) + | C_SEQ s1 s2 => fun t : term => rewrite s2 (rewrite s1 t) + | C_NOP => fun t : term => t + | C_OPP_PLUS => Topp_plus + | C_OPP_OPP => Topp_opp + | C_OPP_MULT_R => Topp_mult_r + | C_OPP_ONE => Topp_one + | C_REDUCE => reduce + | C_MULT_PLUS_DISTR => Tmult_plus_distr + | C_MULT_OPP_LEFT => Tmult_opp_left + | C_MULT_ASSOC_R => Tmult_assoc_r + | C_PLUS_ASSOC_R => Tplus_assoc_r + | C_PLUS_ASSOC_L => Tplus_assoc_l + | C_PLUS_PERMUTE => Tplus_permute + | C_PLUS_COMM => Tplus_comm + | C_RED0 => Tred_factor0 + | C_RED1 => Tred_factor1 + | C_RED2 => Tred_factor2 + | C_RED3 => Tred_factor3 + | C_RED4 => Tred_factor4 + | C_RED5 => Tred_factor5 + | C_RED6 => Tred_factor6 + | C_MULT_ASSOC_REDUCED => Tmult_assoc_reduced + | C_MINUS => Tminus_def + | C_MULT_COMM => Tmult_comm + end. + +Theorem rewrite_stable : forall s : step, term_stable (rewrite s). +Proof. + simple induction s; simpl in |- *; + [ intros; apply apply_both_stable; auto + | intros; apply apply_left_stable; auto + | intros; apply apply_right_stable; auto + | unfold term_stable in |- *; intros; elim H0; apply H + | unfold term_stable in |- *; auto + | exact Topp_plus_stable + | exact Topp_opp_stable + | exact Topp_mult_r_stable + | exact Topp_one_stable + | exact reduce_stable + | exact Tmult_plus_distr_stable + | exact Tmult_opp_left_stable + | exact Tmult_assoc_r_stable + | exact Tplus_assoc_r_stable + | exact Tplus_assoc_l_stable + | exact Tplus_permute_stable + | exact Tplus_comm_stable + | exact Tred_factor0_stable + | exact Tred_factor1_stable + | exact Tred_factor2_stable + | exact Tred_factor3_stable + | exact Tred_factor4_stable + | exact Tred_factor5_stable + | exact Tred_factor6_stable + | exact Tmult_assoc_reduced_stable + | exact Tminus_def_stable + | exact Tmult_comm_stable ]. +Qed. + +(* \subsection{tactiques de résolution d'un but omega normalisé} + Trace de la procédure +\subsubsection{Tactiques générant une contradiction} +\paragraph{[O_CONSTANT_NOT_NUL]} *) + +Definition constant_not_nul (i : nat) (h : hyps) := + match nth_hyps i h with + | 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). +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. + +(* \paragraph{[O_CONSTANT_NEG]} *) + +Definition constant_neg (i : nat) (h : hyps) := + match nth_hyps i h with + | LeqTerm (Tint Nul) (Tint Neg) => + if bgt Nul Neg then absurd else h + | _ => h + end. + +Theorem constant_neg_valid : forall i : nat, valid_hyps (constant_neg i). +Proof. + unfold valid_hyps, constant_neg 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 : int) (body : term) + (t i : nat) (l : hyps) := + match nth_hyps i l with + | EqTerm (Tint Nul) b => + if beq Nul 0 && + eq_term (scalar_norm_add t (body * Tint k1 + Tint k2)%term) b && + bgt k2 0 && + bgt k1 k2 + then absurd + else l + | _ => l + end. + +Theorem not_exact_divide_valid : + forall (k1 k2 : int) (body : term) (t i : nat), + valid_hyps (not_exact_divide k1 k2 body t i). +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 Nul) b1 => + match nth_hyps j l with + | LeqTerm (Tint Nul') b2 => + match fusion_cancel t (b1 + b2)%term with + | Tint k => if beq Nul 0 && beq Nul' 0 && bgt 0 k + then absurd + else l + | _ => l + end + | _ => l + end + | _ => l + end. + +Theorem contradiction_valid : + forall t i j : nat, valid_hyps (contradiction t i j). +Proof. + unfold valid_hyps, contradiction 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; 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 |- *. + 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 Nul) b1 => + match nth_hyps i2 h with + | NeqTerm (Tint Nul') b2 => + if beq Nul 0 && beq Nul' 0 && eq_term b1 b2 + then absurd + else h + | _ => h + end + | NeqTerm (Tint Nul) b1 => + match nth_hyps i2 h with + | EqTerm (Tint Nul') b2 => + if beq Nul 0 && beq Nul' 0 && eq_term b1 b2 + then absurd + else h + | _ => h + end + | _ => h + end. + +Definition negate_contradict_inv (t i1 i2 : nat) (h : hyps) := + match nth_hyps i1 h with + | EqTerm (Tint Nul) b1 => + match nth_hyps i2 h with + | NeqTerm (Tint Nul') b2 => + if beq Nul 0 && beq Nul' 0 && + eq_term b1 (scalar_norm t (b2 * Tint (-(1)))%term) + then absurd + else h + | _ => h + end + | NeqTerm (Tint Nul) b1 => + match nth_hyps i2 h with + | EqTerm (Tint Nul') b2 => + if beq Nul 0 && beq Nul' 0 && + eq_term b1 (scalar_norm t (b2 * Tint (-(1)))%term) + then absurd + else h + | _ => h + end + | _ => h + end. + +Theorem negate_contradict_valid : + forall i j : nat, valid_hyps (negate_contradict i j). +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; 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). +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; 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} *) +(* \paragraph{[O_SUM]} + C'est une oper2 valide mais elle traite plusieurs cas à la fois (suivant + les opérateurs de comparaison des deux arguments) d'où une + preuve un peu compliquée. On utilise quelques lemmes qui sont des + généralisations des théorèmes utilisés par OMEGA. *) + +Definition sum (k1 k2 : int) (trace : list t_fusion) + (prop1 prop2 : proposition) := + match prop1 with + | EqTerm (Tint Null) b1 => + match prop2 with + | EqTerm (Tint Null') b2 => + if beq Null 0 && beq Null' 0 + then EqTerm (Tint 0) (fusion trace (b1 * Tint k1 + b2 * Tint k2)%term) + 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) + else TrueTerm + | _ => TrueTerm + end + | 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) + 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) + else TrueTerm + | _ => TrueTerm + end + else TrueTerm + | NeqTerm (Tint Null) b1 => + match prop2 with + | EqTerm (Tint Null') b2 => + if beq Null 0 && beq Null' 0 && (negb (beq k1 0)) + then NeqTerm (Tint 0) + (fusion trace (b1 * Tint k1 + b2 * Tint k2)%term) + else TrueTerm + | _ => TrueTerm + end + | _ => TrueTerm + end. + + +Theorem sum_valid : + 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 plus_comm; apply sum2; try assumption; apply sum4; assumption + | apply sum3; try assumption; apply sum4; assumption + | apply sum5; auto ]. +Qed. + +(* \paragraph{[O_EXACT_DIVIDE]} + c'est une oper1 valide mais on préfère une substitution a ce point la *) + +Definition exact_divide (k : int) (body : term) (t : nat) + (prop : proposition) := + match prop with + | EqTerm (Tint Null) b => + if beq Null 0 && + eq_term (scalar_norm t (body * Tint k)%term) b && + negb (beq k 0) + then EqTerm (Tint 0) body + else TrueTerm + | NeqTerm (Tint Null) b => + if beq Null 0 && + eq_term (scalar_norm t (body * Tint k)%term) b && + negb (beq k 0) + then NeqTerm (Tint 0) body + else TrueTerm + | _ => TrueTerm + end. + +Theorem exact_divide_valid : + forall (k : int) (t : term) (n : nat), valid1 (exact_divide k t n). +Proof. + unfold valid1, exact_divide 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. + + +(* \paragraph{[O_DIV_APPROX]} + La preuve reprend le schéma de la précédente mais on + est sur une opération de type valid1 et non sur une opération terminale. *) + +Definition divide_and_approx (k1 k2 : int) (body : term) + (t : nat) (prop : proposition) := + match prop with + | LeqTerm (Tint Null) b => + if beq Null 0 && + eq_term (scalar_norm_add t (body * Tint k1 + Tint k2)%term) b && + bgt k1 0 && + bgt k1 k2 + then LeqTerm (Tint 0) body + else prop + | _ => prop + end. + +Theorem divide_and_approx_valid : + forall (k1 k2 : int) (body : term) (t : nat), + valid1 (divide_and_approx k1 k2 body t). +Proof. + unfold valid1, divide_and_approx 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 Null) b1 => + match prop2 with + | LeqTerm (Tint Null') b2 => + if beq Null 0 && beq Null' 0 && + eq_term b1 (scalar_norm t (b2 * Tint (-(1)))%term) + then EqTerm (Tint 0) b1 + else TrueTerm + | _ => TrueTerm + end + | _ => TrueTerm + end. + +Theorem merge_eq_valid : forall n : nat, valid2 (merge_eq n). +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 opp_eq_mult_neg_1; trivial ]. +Qed. + + + +(* \paragraph{[O_CONSTANT_NUL]} *) + +Definition constant_nul (i : nat) (h : hyps) := + match nth_hyps i h with + | NeqTerm (Tint Null) (Tint Null') => + if beq Null Null' then absurd else h + | _ => h + end. + +Theorem constant_nul_valid : forall i : nat, valid_hyps (constant_nul i). +Proof. + unfold valid_hyps, constant_nul in |- *; intros; + generalize (nth_valid ep e i lp); Simplify; simpl in |- *; + intro H1; absurd (0 = 0); intuition. +Qed. + +(* \paragraph{[O_STATE]} *) + +Definition state (m : int) (s : step) (prop1 prop2 : proposition) := + match prop1 with + | EqTerm (Tint Null) b1 => + match prop2 with + | EqTerm b2 b3 => + if beq Null 0 + then EqTerm (Tint 0) (rewrite s (b1 + (- b3 + b2) * Tint m)%term) + else TrueTerm + | _ => TrueTerm + end + | _ => TrueTerm + end. + +Theorem state_valid : forall (m : int) (s : step), valid2 (state m s). +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. + now rewrite H2, plus_opp_l, plus_0_l, mult_0_l. +Qed. + +(* \subsubsection{Tactiques générant plusieurs but} + \paragraph{[O_SPLIT_INEQ]} + La seule pour le moment (tant que la normalisation n'est pas réfléchie). *) + +Definition split_ineq (i t : nat) (f1 f2 : hyps -> lhyps) + (l : hyps) := + match nth_hyps i l with + | NeqTerm (Tint Null) b1 => + if beq Null 0 then + f1 (LeqTerm (Tint 0) (add_norm t (b1 + Tint (-(1)))%term) :: l) ++ + f2 + (LeqTerm (Tint 0) + (scalar_norm_add t (b1 * Tint (-(1)) + Tint (-(1)))%term) :: l) + else l :: nil + | _ => l :: nil + end. + +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). +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; 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 not in |- *; intros E1 E2; apply E1; + symmetry in |- *; trivial ]. +Qed. + + +(* \subsection{La fonction de rejeu de la trace} *) + +Fixpoint execute_omega (t : t_omega) (l : hyps) {struct t} : lhyps := + match t with + | O_CONSTANT_NOT_NUL n => singleton (constant_not_nul n l) + | O_CONSTANT_NEG n => singleton (constant_neg n l) + | O_DIV_APPROX k1 k2 body t cont n => + execute_omega cont (apply_oper_1 n (divide_and_approx k1 k2 body t) l) + | O_NOT_EXACT_DIVIDE k1 k2 body t i => + singleton (not_exact_divide k1 k2 body t i l) + | O_EXACT_DIVIDE k body t cont n => + execute_omega cont (apply_oper_1 n (exact_divide k body t) l) + | O_SUM k1 i1 k2 i2 t cont => + execute_omega cont (apply_oper_2 i1 i2 (sum k1 k2 t) l) + | O_CONTRADICTION t i j => singleton (contradiction t i j l) + | O_MERGE_EQ t i1 i2 cont => + execute_omega cont (apply_oper_2 i1 i2 (merge_eq t) l) + | O_SPLIT_INEQ t i cont1 cont2 => + split_ineq i t (execute_omega cont1) (execute_omega cont2) l + | O_CONSTANT_NUL i => singleton (constant_nul i l) + | O_NEGATE_CONTRADICT i j => singleton (negate_contradict i j l) + | O_NEGATE_CONTRADICT_INV t i j => + singleton (negate_contradict_inv t i j l) + | O_STATE m s i1 i2 cont => + execute_omega cont (apply_oper_2 i1 i2 (state m s) l) + end. + +Theorem omega_valid : forall t : t_omega, valid_list_hyps (execute_omega t). +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; + apply (constant_neg_valid n ep e lp H) + | unfold valid_list_hyps, valid_hyps in |- *; + intros k1 k2 body n t' Ht' m ep e lp H; apply Ht'; + apply + (apply_oper_1_valid m (divide_and_approx k1 k2 body n) + (divide_and_approx_valid k1 k2 body n) ep e lp H) + | unfold valid_list_hyps in |- *; simpl in |- *; intros; left; + 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 + (apply_oper_1_valid m (exact_divide k body n) + (exact_divide_valid k body n) ep e lp H) + | unfold valid_list_hyps, valid_hyps in |- *; + intros k1 i1 k2 i2 trace t' Ht' ep e lp H; apply Ht'; + apply + (apply_oper_2_valid i1 i2 (sum k1 k2 trace) (sum_valid k1 k2 trace) ep e + lp H) + | unfold valid_list_hyps in |- *; simpl in |- *; intros; left; + apply (contradiction_valid n n0 n1 ep e lp H) + | unfold valid_list_hyps, valid_hyps in |- *; + intros trace i1 i2 t' Ht' ep e lp H; apply Ht'; + apply + (apply_oper_2_valid i1 i2 (merge_eq trace) (merge_eq_valid trace) ep e + lp H) + | intros t' i k1 H1 k2 H2; unfold valid_list_hyps in |- *; simpl in |- *; + intros ep e lp H; + apply + (split_ineq_valid i t' (execute_omega k1) (execute_omega k2) H1 H2 ep e + lp H) + | unfold valid_list_hyps in |- *; simpl in |- *; intros i ep e lp H; left; + apply (constant_nul_valid i ep e lp H) + | unfold valid_list_hyps in |- *; simpl in |- *; intros i j ep e lp H; left; + apply (negate_contradict_valid i j ep e lp H) + | unfold valid_list_hyps in |- *; simpl in |- *; intros n i j ep e lp H; + left; apply (negate_contradict_inv_valid n i j ep e lp H) + | unfold valid_list_hyps, valid_hyps in |- *; + intros m s i1 i2 t' Ht' ep e lp H; apply Ht'; + apply (apply_oper_2_valid i1 i2 (state m s) (state_valid m s) ep e lp H) ]. +Qed. + + +(* \subsection{Les opérations globales sur le but} + \subsubsection{Normalisation} *) + +Definition move_right (s : step) (p : proposition) := + match p with + | EqTerm t1 t2 => EqTerm (Tint 0) (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) + | NeqTerm t1 t2 => NeqTerm (Tint 0) (rewrite s (t1 + - t2)%term) + | p => p + end. + +Theorem move_right_valid : forall s : step, valid1 (move_right s). +Proof. + unfold valid1, move_right in |- *; intros s ep e p; Simplify; simpl in |- *; + elim (rewrite_stable s e); simpl in |- *; + [ 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). +Proof. + intros; unfold do_normalize in |- *; apply apply_oper_1_valid; + apply move_right_valid. +Qed. + +Fixpoint do_normalize_list (l : list step) (i : nat) + (h : hyps) {struct l} : hyps := + match l with + | s :: l' => do_normalize_list l' (S i) (do_normalize i s h) + | nil => h + end. + +Theorem do_normalize_list_valid : + forall (l : list step) (i : nat), valid_hyps (do_normalize_list l i). +Proof. + simple induction l; simpl 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 : list Prop) (env : list int) (l : hyps), + interp_goal ep env (do_normalize_list s 0 l) -> interp_goal ep env l. +Proof. + intros; apply valid_goal with (2 := H); apply do_normalize_list_valid. +Qed. + +(* \subsubsection{Exécution de la trace} *) + +Theorem execute_goal : + 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. +Proof. + intros; apply (goal_valid (execute_omega t) (omega_valid t) ep env l H). +Qed. + + +Theorem append_goal : + forall (ep : list Prop) (e : list int) (l1 l2 : lhyps), + interp_list_goal ep e l1 /\ interp_list_goal ep e l2 -> + interp_list_goal ep e (l1 ++ l2). +Proof. + intros ep e; simple induction l1; + [ simpl in |- *; intros l2 (H1, H2); assumption + | simpl in |- *; intros h1 t1 HR l2 ((H1, H2), H3); split; auto ]. +Qed. + +(* A simple decidability checker : if the proposition belongs to the + simple grammar describe below then it is decidable. Proof is by + induction and uses well known theorem about arithmetic and propositional + calculus *) + +Fixpoint decidability (p : proposition) : bool := + match p with + | EqTerm _ _ => true + | LeqTerm _ _ => true + | GeqTerm _ _ => true + | GtTerm _ _ => true + | LtTerm _ _ => true + | NeqTerm _ _ => true + | FalseTerm => true + | TrueTerm => true + | Tnot t => decidability t + | Tand t1 t2 => decidability t1 && decidability t2 + | Timp t1 t2 => decidability t1 && decidability t2 + | Tor t1 t2 => decidability t1 && decidability t2 + | Tprop _ => false + end. + +Theorem decidable_correct : + forall (ep : list Prop) (e : list int) (p : proposition), + decidability p = true -> decidable (interp_proposition ep e p). +Proof. + simple induction p; simpl in |- *; intros; + [ apply dec_eq + | apply dec_le + | left; auto + | right; unfold not in |- *; auto + | apply dec_not; auto + | apply dec_ge + | apply dec_gt + | apply dec_lt + | apply dec_ne + | apply dec_or; elim andb_prop with (1 := H1); auto + | apply dec_and; elim andb_prop with (1 := H1); auto + | apply dec_imp; elim andb_prop with (1 := H1); auto + | discriminate H ]. +Qed. + +(* An interpretation function for a complete goal with an explicit + conclusion. We use an intermediate fixpoint. *) + +Fixpoint interp_full_goal (envp : list Prop) (env : list int) + (c : proposition) (l : hyps) {struct l} : Prop := + match l with + | nil => interp_proposition envp env c + | p' :: l' => + interp_proposition envp env p' -> interp_full_goal envp env c l' + end. + +Definition interp_full (ep : list Prop) (e : list int) + (lc : hyps * proposition) : Prop := + match lc with + | (l, c) => interp_full_goal ep e c l + end. + +(* Relates the interpretation of a complete goal with the interpretation + of its hypothesis and conclusion *) + +Theorem interp_full_false : + forall (ep : list Prop) (e : list int) (l : hyps) (c : proposition), + (interp_hyps ep e l -> interp_proposition ep e c) -> interp_full ep e (l, c). +Proof. + simple induction l; unfold interp_full 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 + If the decidability cannot be "proven", then just forget about the + conclusion (equivalent of replacing it with false) *) + +Definition to_contradict (lc : hyps * proposition) := + match lc with + | (l, c) => if decidability c then Tnot c :: l else l + end. + +(* The previous operation is valid in the sense that the new list of + hypothesis implies the original goal *) + +Theorem to_contradict_valid : + forall (ep : list Prop) (e : list int) (lc : hyps * proposition), + interp_goal ep e (to_contradict lc) -> interp_full ep e lc. +Proof. + intros ep e lc; case lc; intros l c; simpl 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 + | unfold not at 1 in |- *; intro H3; apply hyps_to_goal with (2 := H2); + auto ] + | intros H1 H2; apply interp_full_false; intro H3; + elim hyps_to_goal with (1 := H2); assumption ]. +Qed. + +(* [map_cons x l] adds [x] at the head of each list in [l] (which is a list + of lists *) + +Fixpoint map_cons (A : Set) (x : A) (l : list (list A)) {struct l} : + list (list A) := + match l with + | nil => nil + | l :: ll => (x :: l) :: map_cons A x ll + end. + +(* This function breaks up a list of hypothesis in a list of simpler + list of hypothesis that together implie the original one. The goal + of all this is to transform the goal in a list of solvable problems. + Note that : + - we need a way to drive the analysis as some hypotheis may not + require a split. + - this procedure must be perfectly mimicked by the ML part otherwise + hypothesis will get desynchronised and this will be a mess. + *) + +Fixpoint destructure_hyps (nn : nat) (ll : hyps) {struct nn} : lhyps := + match nn with + | O => ll :: nil + | S n => + match ll with + | nil => nil :: nil + | Tor p1 p2 :: l => + destructure_hyps n (p1 :: l) ++ destructure_hyps n (p2 :: l) + | Tand p1 p2 :: l => destructure_hyps n (p1 :: p2 :: l) + | Timp p1 p2 :: l => + if decidability p1 + then + destructure_hyps n (Tnot p1 :: l) ++ destructure_hyps n (p2 :: l) + else map_cons _ (Timp p1 p2) (destructure_hyps n l) + | Tnot p :: l => + match p with + | Tnot p1 => + if decidability p1 + then destructure_hyps n (p1 :: l) + else map_cons _ (Tnot (Tnot p1)) (destructure_hyps n l) + | Tor p1 p2 => destructure_hyps n (Tnot p1 :: Tnot p2 :: l) + | Tand p1 p2 => + if decidability p1 + then + destructure_hyps n (Tnot p1 :: l) ++ + destructure_hyps n (Tnot p2 :: l) + else map_cons _ (Tnot p) (destructure_hyps n l) + | _ => map_cons _ (Tnot p) (destructure_hyps n l) + end + | x :: l => map_cons _ x (destructure_hyps n l) + end + end. + +Theorem map_cons_val : + forall (ep : list Prop) (e : list int) (p : proposition) (l : lhyps), + interp_proposition ep e p -> + interp_list_hyps ep e l -> interp_list_hyps ep e (map_cons _ p l). +Proof. + simple induction l; simpl 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). +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 + | intros p l; case p; + try + (simpl in |- *; intros; apply map_cons_val; simpl in |- *; elim H0; + auto); + [ intro p'; case p'; + try + (simpl in |- *; intros; apply map_cons_val; simpl in |- *; elim H0; + auto); + [ simpl in |- *; intros p1 (H1, H2); + pattern (decidability p1) in |- *; apply bool_eq_ind; + intro H3; + [ apply H; simpl in |- *; split; + [ apply not_not; auto | assumption ] + | auto ] + | 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_eq_ind; + intro H3; + [ apply append_valid; elim not_and with (2 := H1); + [ intro; left; apply H; simpl in |- *; auto + | intro; right; apply H; simpl in |- *; auto + | auto ] + | auto ] ] + | simpl in |- *; intros p1 p2 (H1, H2); apply append_valid; + (elim H1; intro H3; simpl in |- *; [ left | right ]); + 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_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 : list Prop) (e : list int) (p : proposition), + interp_proposition ep e p <-> interp_proposition ep e (f p). + +Definition p_apply_left (f : proposition -> proposition) + (p : proposition) := + match p with + | Timp x y => Timp (f x) y + | Tor x y => Tor (f x) y + | Tand x y => Tand (f x) y + | Tnot x => Tnot (f x) + | x => x + end. + +Theorem p_apply_left_stable : + forall f : proposition -> proposition, + prop_stable f -> prop_stable (p_apply_left f). +Proof. + unfold prop_stable in |- *; intros f H ep e p; split; + (case p; simpl in |- *; auto; intros p1; elim (H ep e p1); tauto). +Qed. + +Definition p_apply_right (f : proposition -> proposition) + (p : proposition) := + match p with + | Timp x y => Timp x (f y) + | Tor x y => Tor x (f y) + | Tand x y => Tand x (f y) + | Tnot x => Tnot (f x) + | x => x + end. + +Theorem p_apply_right_stable : + forall f : proposition -> proposition, + prop_stable f -> prop_stable (p_apply_right f). +Proof. + unfold prop_stable 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 + | intros p1 p2; elim (H ep e p2); tauto + | intros p1 p2; elim (H ep e p2); tauto ]). +Qed. + +Definition p_invert (f : proposition -> proposition) + (p : proposition) := + match p with + | EqTerm x y => Tnot (f (NeqTerm x y)) + | LeqTerm x y => Tnot (f (GtTerm x y)) + | GeqTerm x y => Tnot (f (LtTerm x y)) + | GtTerm x y => Tnot (f (LeqTerm x y)) + | LtTerm x y => Tnot (f (GeqTerm x y)) + | NeqTerm x y => Tnot (f (EqTerm x y)) + | x => x + end. + +Theorem p_invert_stable : + forall f : proposition -> proposition, + prop_stable f -> prop_stable (p_invert f). +Proof. + unfold prop_stable 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 |- *; + 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 |- *; + 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 |- *; + 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_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_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; tauto ]). +Qed. + +Theorem move_right_stable : forall s : step, prop_stable (move_right s). +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 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 (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. + + +Fixpoint p_rewrite (s : p_step) : proposition -> proposition := + match s with + | P_LEFT s => p_apply_left (p_rewrite s) + | P_RIGHT s => p_apply_right (p_rewrite s) + | P_STEP s => move_right s + | P_INVERT s => p_invert (move_right s) + | P_NOP => fun p : proposition => p + end. + +Theorem p_rewrite_stable : forall s : p_step, prop_stable (p_rewrite s). +Proof. + simple induction s; simpl in |- *; + [ intros; apply p_apply_left_stable; trivial + | intros; apply p_apply_right_stable; trivial + | intros; apply p_invert_stable; apply move_right_stable + | apply move_right_stable + | unfold prop_stable in |- *; simpl in |- *; intros; split; auto ]. +Qed. + +Fixpoint normalize_hyps (l : list h_step) (lh : hyps) {struct l} : hyps := + match l with + | nil => lh + | pair_step i s :: r => normalize_hyps r (apply_oper_1 i (p_rewrite s) lh) + end. + +Theorem normalize_hyps_valid : + forall l : list h_step, valid_hyps (normalize_hyps l). +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; + [ unfold valid1 in |- *; intros ep1 e1 p1 H2; + elim (p_rewrite_stable s ep1 e1 p1); auto + | assumption ] ]. +Qed. + +Theorem normalize_hyps_goal : + forall (s : list h_step) (ep : list Prop) (env : list int) (l : hyps), + interp_goal ep env (normalize_hyps s l) -> interp_goal ep env l. +Proof. + intros; apply valid_goal with (2 := H); apply normalize_hyps_valid. +Qed. + +Fixpoint extract_hyp_pos (s : list direction) (p : proposition) {struct s} : + proposition := + match s with + | D_left :: l => + match p with + | Tand x y => extract_hyp_pos l x + | _ => p + end + | D_right :: l => + match p with + | Tand x y => extract_hyp_pos l y + | _ => p + end + | D_mono :: l => match p with + | Tnot x => extract_hyp_neg l x + | _ => p + end + | _ => p + end + + with extract_hyp_neg (s : list direction) (p : proposition) {struct s} : + proposition := + match s with + | D_left :: l => + match p with + | Tor x y => extract_hyp_neg l x + | Timp x y => if decidability x then extract_hyp_pos l x else Tnot p + | _ => Tnot p + end + | D_right :: l => + match p with + | Tor x y => extract_hyp_neg l y + | Timp x y => extract_hyp_neg l y + | _ => Tnot p + end + | D_mono :: l => + match p with + | Tnot x => if decidability x then extract_hyp_pos l x else Tnot p + | _ => Tnot p + end + | _ => + match p with + | Tnot x => if decidability x then x else Tnot p + | _ => Tnot p + end + end. + +Definition co_valid1 (f : proposition -> proposition) := + forall (ep : list Prop) (e : list int) (p1 : proposition), + interp_proposition ep e (Tnot p1) -> interp_proposition ep e (f p1). + +Theorem extract_valid : + forall s : list direction, + valid1 (extract_hyp_pos s) /\ co_valid1 (extract_hyp_neg s). +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_eq_ind; + [ intro H; generalize (decidable_correct ep e p H); + unfold decidable in |- *; tauto + | simpl in |- *; auto ] ] + | intros a s' (H1, H2); simpl in H2; split; intros ep e p; case a; auto; + case p; auto; simpl in |- *; intros; + (apply H1; tauto) || + (apply H2; tauto) || + (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 := + match s with + | E_SPLIT i dl s1 s2 => + match extract_hyp_pos dl (nth_hyps i h) with + | Tor x y => decompose_solve s1 (x :: h) ++ decompose_solve s2 (y :: h) + | Tnot (Tand x y) => + if decidability x + then + decompose_solve s1 (Tnot x :: h) ++ + decompose_solve s2 (Tnot y :: h) + else h :: nil + | Timp x y => + if decidability x then + decompose_solve s1 (Tnot x :: h) ++ decompose_solve s2 (y :: h) + else h::nil + | _ => h :: nil + end + | E_EXTRACT i dl s1 => + decompose_solve s1 (extract_hyp_pos dl (nth_hyps i h) :: h) + | E_SOLVE t => execute_omega t h + end. + +Theorem decompose_solve_valid : + forall s : e_step, valid_list_goal (decompose_solve s). +Proof. + intro s; apply goal_valid; unfold valid_list_hyps 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_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 + | left; apply H; simpl in |- *; tauto ] + | simpl in |- *; auto ] + | intros p1 p2 H2; apply append_valid; simpl in |- *; elim H2; + [ 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_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 + | left; apply H; simpl in |- *; tauto ] + | simpl in |- *; auto ] ] + | elim (extract_valid l); intros H2 H3; apply H2; apply nth_valid; auto ] + | intros; apply H; simpl in |- *; split; + [ elim (extract_valid l); intros H2 H3; apply H2; apply nth_valid; auto + | auto ] + | apply omega_valid with (1 := H) ]. +Qed. + +(* \subsection{La dernière étape qui élimine tous les séquents inutiles} *) + +Definition valid_lhyps (f : lhyps -> 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 := + match lp with + | (FalseTerm :: nil) :: lp' => reduce_lhyps lp' + | x :: lp' => x :: reduce_lhyps lp' + | nil => nil (A:=hyps) + end. + +Theorem reduce_lhyps_valid : valid_lhyps reduce_lhyps. +Proof. + unfold valid_lhyps in |- *; intros ep e lp; elim lp; + [ simpl in |- *; auto + | intros a l HR; elim a; + [ simpl in |- *; tauto + | intros a1 l1; case l1; case a1; simpl in |- *; try tauto ] ]. +Qed. + +Theorem do_reduce_lhyps : + forall (envp : list Prop) (env : list int) (l : lhyps), + interp_list_goal envp env (reduce_lhyps l) -> interp_list_goal envp env l. +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. + +Definition concl_to_hyp (p : proposition) := + if decidability p then Tnot p else TrueTerm. + +Definition do_concl_to_hyp : + 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. +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_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 ] + | simpl in |- *; tauto ]. +Qed. + +Definition omega_tactic (t1 : e_step) (t2 : list h_step) + (c : proposition) (l : hyps) := + reduce_lhyps (decompose_solve t1 (normalize_hyps t2 (concl_to_hyp c :: l))). + +Theorem do_omega : + 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. +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). diff --git a/plugins/romega/const_omega.ml b/plugins/romega/const_omega.ml new file mode 100644 index 00000000..f4368a1b --- /dev/null +++ b/plugins/romega/const_omega.ml @@ -0,0 +1,352 @@ +(************************************************************************* + + PROJET RNRT Calife - 2001 + Author: Pierre Crégut - France Télécom R&D + Licence : LGPL version 2.1 + + *************************************************************************) + +let module_refl_name = "ReflOmegaCore" +let module_refl_path = ["Coq"; "romega"; module_refl_name] + +type result = + Kvar of string + | Kapp of string * Term.constr list + | Kimp of Term.constr * Term.constr + | Kufo;; + +let destructurate t = + let c, args = Term.decompose_app t in + match Term.kind_of_term c, args with + | Term.Const sp, args -> + Kapp (Names.string_of_id + (Nametab.basename_of_global (Libnames.ConstRef sp)), + args) + | Term.Construct csp , args -> + Kapp (Names.string_of_id + (Nametab.basename_of_global (Libnames.ConstructRef csp)), + args) + | Term.Ind isp, args -> + Kapp (Names.string_of_id + (Nametab.basename_of_global (Libnames.IndRef isp)), + args) + | Term.Var id,[] -> Kvar(Names.string_of_id id) + | Term.Prod (Names.Anonymous,typ,body), [] -> Kimp(typ,body) + | Term.Prod (Names.Name _,_,_),[] -> + Util.error "Omega: Not a quantifier-free goal" + | _ -> Kufo + +exception Destruct + +let dest_const_apply t = + let f,args = Term.decompose_app t in + let ref = + match Term.kind_of_term f with + | Term.Const sp -> Libnames.ConstRef sp + | Term.Construct csp -> Libnames.ConstructRef csp + | Term.Ind isp -> Libnames.IndRef isp + | _ -> raise Destruct + in Nametab.basename_of_global ref, args + +let logic_dir = ["Coq";"Logic";"Decidable"] + +let coq_modules = + Coqlib.init_modules @ [logic_dir] @ Coqlib.arith_modules @ Coqlib.zarith_base_modules + @ [["Coq"; "Lists"; "List"]] + @ [module_refl_path] + @ [module_refl_path@["ZOmega"]] + + +let init_constant = Coqlib.gen_constant_in_modules "Omega" Coqlib.init_modules +let constant = Coqlib.gen_constant_in_modules "Omega" coq_modules + +(* Logic *) +let coq_eq = lazy(init_constant "eq") +let coq_refl_equal = lazy(init_constant "eq_refl") +let coq_and = lazy(init_constant "and") +let coq_not = lazy(init_constant "not") +let coq_or = lazy(init_constant "or") +let coq_True = lazy(init_constant "True") +let coq_False = lazy(init_constant "False") +let coq_I = lazy(init_constant "I") + +(* ReflOmegaCore/ZOmega *) + +let coq_h_step = lazy (constant "h_step") +let coq_pair_step = lazy (constant "pair_step") +let coq_p_left = lazy (constant "P_LEFT") +let coq_p_right = lazy (constant "P_RIGHT") +let coq_p_invert = lazy (constant "P_INVERT") +let coq_p_step = lazy (constant "P_STEP") + +let coq_t_int = lazy (constant "Tint") +let coq_t_plus = lazy (constant "Tplus") +let coq_t_mult = lazy (constant "Tmult") +let coq_t_opp = lazy (constant "Topp") +let coq_t_minus = lazy (constant "Tminus") +let coq_t_var = lazy (constant "Tvar") + +let coq_proposition = lazy (constant "proposition") +let coq_p_eq = lazy (constant "EqTerm") +let coq_p_leq = lazy (constant "LeqTerm") +let coq_p_geq = lazy (constant "GeqTerm") +let coq_p_lt = lazy (constant "LtTerm") +let coq_p_gt = lazy (constant "GtTerm") +let coq_p_neq = lazy (constant "NeqTerm") +let coq_p_true = lazy (constant "TrueTerm") +let coq_p_false = lazy (constant "FalseTerm") +let coq_p_not = lazy (constant "Tnot") +let coq_p_or = lazy (constant "Tor") +let coq_p_and = lazy (constant "Tand") +let coq_p_imp = lazy (constant "Timp") +let coq_p_prop = lazy (constant "Tprop") + +(* Constructors for shuffle tactic *) +let coq_t_fusion = lazy (constant "t_fusion") +let coq_f_equal = lazy (constant "F_equal") +let coq_f_cancel = lazy (constant "F_cancel") +let coq_f_left = lazy (constant "F_left") +let coq_f_right = lazy (constant "F_right") + +(* Constructors for reordering tactics *) +let coq_c_do_both = lazy (constant "C_DO_BOTH") +let coq_c_do_left = lazy (constant "C_LEFT") +let coq_c_do_right = lazy (constant "C_RIGHT") +let coq_c_do_seq = lazy (constant "C_SEQ") +let coq_c_nop = lazy (constant "C_NOP") +let coq_c_opp_plus = lazy (constant "C_OPP_PLUS") +let coq_c_opp_opp = lazy (constant "C_OPP_OPP") +let coq_c_opp_mult_r = lazy (constant "C_OPP_MULT_R") +let coq_c_opp_one = lazy (constant "C_OPP_ONE") +let coq_c_reduce = lazy (constant "C_REDUCE") +let coq_c_mult_plus_distr = lazy (constant "C_MULT_PLUS_DISTR") +let coq_c_opp_left = lazy (constant "C_MULT_OPP_LEFT") +let coq_c_mult_assoc_r = lazy (constant "C_MULT_ASSOC_R") +let coq_c_plus_assoc_r = lazy (constant "C_PLUS_ASSOC_R") +let coq_c_plus_assoc_l = lazy (constant "C_PLUS_ASSOC_L") +let coq_c_plus_permute = lazy (constant "C_PLUS_PERMUTE") +let coq_c_plus_comm = lazy (constant "C_PLUS_COMM") +let coq_c_red0 = lazy (constant "C_RED0") +let coq_c_red1 = lazy (constant "C_RED1") +let coq_c_red2 = lazy (constant "C_RED2") +let coq_c_red3 = lazy (constant "C_RED3") +let coq_c_red4 = lazy (constant "C_RED4") +let coq_c_red5 = lazy (constant "C_RED5") +let coq_c_red6 = lazy (constant "C_RED6") +let coq_c_mult_opp_left = lazy (constant "C_MULT_OPP_LEFT") +let coq_c_mult_assoc_reduced = lazy (constant "C_MULT_ASSOC_REDUCED") +let coq_c_minus = lazy (constant "C_MINUS") +let coq_c_mult_comm = lazy (constant "C_MULT_COMM") + +let coq_s_constant_not_nul = lazy (constant "O_CONSTANT_NOT_NUL") +let coq_s_constant_neg = lazy (constant "O_CONSTANT_NEG") +let coq_s_div_approx = lazy (constant "O_DIV_APPROX") +let coq_s_not_exact_divide = lazy (constant "O_NOT_EXACT_DIVIDE") +let coq_s_exact_divide = lazy (constant "O_EXACT_DIVIDE") +let coq_s_sum = lazy (constant "O_SUM") +let coq_s_state = lazy (constant "O_STATE") +let coq_s_contradiction = lazy (constant "O_CONTRADICTION") +let coq_s_merge_eq = lazy (constant "O_MERGE_EQ") +let coq_s_split_ineq =lazy (constant "O_SPLIT_INEQ") +let coq_s_constant_nul =lazy (constant "O_CONSTANT_NUL") +let coq_s_negate_contradict =lazy (constant "O_NEGATE_CONTRADICT") +let coq_s_negate_contradict_inv =lazy (constant "O_NEGATE_CONTRADICT_INV") + +(* construction for the [extract_hyp] tactic *) +let coq_direction = lazy (constant "direction") +let coq_d_left = lazy (constant "D_left") +let coq_d_right = lazy (constant "D_right") +let coq_d_mono = lazy (constant "D_mono") + +let coq_e_split = lazy (constant "E_SPLIT") +let coq_e_extract = lazy (constant "E_EXTRACT") +let coq_e_solve = lazy (constant "E_SOLVE") + +let coq_interp_sequent = lazy (constant "interp_goal_concl") +let coq_do_omega = lazy (constant "do_omega") + +(* \subsection{Construction d'expressions} *) + +let do_left t = + if t = Lazy.force coq_c_nop then Lazy.force coq_c_nop + else Term.mkApp (Lazy.force coq_c_do_left, [|t |] ) + +let do_right t = + if t = Lazy.force coq_c_nop then Lazy.force coq_c_nop + else Term.mkApp (Lazy.force coq_c_do_right, [|t |]) + +let do_both t1 t2 = + if t1 = Lazy.force coq_c_nop then do_right t2 + else if t2 = Lazy.force coq_c_nop then do_left t1 + else Term.mkApp (Lazy.force coq_c_do_both , [|t1; t2 |]) + +let do_seq t1 t2 = + if t1 = Lazy.force coq_c_nop then t2 + else if t2 = Lazy.force coq_c_nop then t1 + else Term.mkApp (Lazy.force coq_c_do_seq, [|t1; t2 |]) + +let rec do_list = function + | [] -> Lazy.force coq_c_nop + | [x] -> x + | (x::l) -> do_seq x (do_list l) + +(* Nat *) + +let coq_S = lazy(init_constant "S") +let coq_O = lazy(init_constant "O") + +let rec mk_nat = function + | 0 -> Lazy.force coq_O + | n -> Term.mkApp (Lazy.force coq_S, [| mk_nat (n-1) |]) + +(* Lists *) + +let coq_cons = lazy (constant "cons") +let coq_nil = lazy (constant "nil") + +let mk_list typ l = + let rec loop = function + | [] -> + Term.mkApp (Lazy.force coq_nil, [|typ|]) + | (step :: l) -> + Term.mkApp (Lazy.force coq_cons, [|typ; step; loop l |]) in + loop l + +let mk_plist l = mk_list Term.mkProp l + +let mk_shuffle_list l = mk_list (Lazy.force coq_t_fusion) l + + +type parse_term = + | Tplus of Term.constr * Term.constr + | Tmult of Term.constr * Term.constr + | Tminus of Term.constr * Term.constr + | Topp of Term.constr + | Tsucc of Term.constr + | Tnum of Bigint.bigint + | Tother + +type parse_rel = + | Req of Term.constr * Term.constr + | Rne of Term.constr * Term.constr + | Rlt of Term.constr * Term.constr + | Rle of Term.constr * Term.constr + | Rgt of Term.constr * Term.constr + | Rge of Term.constr * Term.constr + | Rtrue + | Rfalse + | Rnot of Term.constr + | Ror of Term.constr * Term.constr + | Rand of Term.constr * Term.constr + | Rimp of Term.constr * Term.constr + | Riff of Term.constr * Term.constr + | Rother + +let parse_logic_rel c = + try match destructurate c with + | Kapp("True",[]) -> Rtrue + | Kapp("False",[]) -> Rfalse + | Kapp("not",[t]) -> Rnot t + | Kapp("or",[t1;t2]) -> Ror (t1,t2) + | Kapp("and",[t1;t2]) -> Rand (t1,t2) + | Kimp(t1,t2) -> Rimp (t1,t2) + | Kapp("iff",[t1;t2]) -> Riff (t1,t2) + | _ -> Rother + with e when Logic.catchable_exception e -> Rother + + +module type Int = sig + val typ : Term.constr Lazy.t + val plus : Term.constr Lazy.t + val mult : Term.constr Lazy.t + val opp : Term.constr Lazy.t + val minus : Term.constr Lazy.t + + val mk : Bigint.bigint -> Term.constr + val parse_term : Term.constr -> parse_term + val parse_rel : Proof_type.goal Tacmach.sigma -> Term.constr -> parse_rel + (* check whether t is built only with numbers and + * - *) + val is_scalar : Term.constr -> bool +end + +module Z : Int = struct + +let typ = lazy (constant "Z") +let plus = lazy (constant "Zplus") +let mult = lazy (constant "Zmult") +let opp = lazy (constant "Zopp") +let minus = lazy (constant "Zminus") + +let coq_xH = lazy (constant "xH") +let coq_xO = lazy (constant "xO") +let coq_xI = lazy (constant "xI") +let coq_Z0 = lazy (constant "Z0") +let coq_Zpos = lazy (constant "Zpos") +let coq_Zneg = lazy (constant "Zneg") + +let recognize t = + let rec loop t = + let f,l = dest_const_apply t in + match Names.string_of_id f,l with + "xI",[t] -> Bigint.add Bigint.one (Bigint.mult Bigint.two (loop t)) + | "xO",[t] -> Bigint.mult Bigint.two (loop t) + | "xH",[] -> Bigint.one + | _ -> failwith "not a number" in + let f,l = dest_const_apply t in + match Names.string_of_id f,l with + "Zpos",[t] -> loop t + | "Zneg",[t] -> Bigint.neg (loop t) + | "Z0",[] -> Bigint.zero + | _ -> failwith "not a number";; + +let rec mk_positive n = + if n=Bigint.one then Lazy.force coq_xH + else + let (q,r) = Bigint.euclid n Bigint.two in + Term.mkApp + ((if r = Bigint.zero then Lazy.force coq_xO else Lazy.force coq_xI), + [| mk_positive q |]) + +let mk_Z n = + if n = Bigint.zero then Lazy.force coq_Z0 + else if Bigint.is_strictly_pos n then + Term.mkApp (Lazy.force coq_Zpos, [| mk_positive n |]) + else + Term.mkApp (Lazy.force coq_Zneg, [| mk_positive (Bigint.neg n) |]) + +let mk = mk_Z + +let parse_term t = + try match destructurate t with + | Kapp("Zplus",[t1;t2]) -> Tplus (t1,t2) + | Kapp("Zminus",[t1;t2]) -> Tminus (t1,t2) + | Kapp("Zmult",[t1;t2]) -> Tmult (t1,t2) + | Kapp("Zopp",[t]) -> Topp t + | Kapp("Zsucc",[t]) -> Tsucc t + | Kapp("Zpred",[t]) -> Tplus(t, mk_Z (Bigint.neg Bigint.one)) + | Kapp(("Zpos"|"Zneg"|"Z0"),_) -> + (try Tnum (recognize t) with _ -> Tother) + | _ -> Tother + with e when Logic.catchable_exception e -> Tother + +let parse_rel gl t = + try match destructurate t with + | Kapp("eq",[typ;t1;t2]) + when destructurate (Tacmach.pf_nf gl typ) = Kapp("Z",[]) -> Req (t1,t2) + | Kapp("Zne",[t1;t2]) -> Rne (t1,t2) + | Kapp("Zle",[t1;t2]) -> Rle (t1,t2) + | Kapp("Zlt",[t1;t2]) -> Rlt (t1,t2) + | Kapp("Zge",[t1;t2]) -> Rge (t1,t2) + | Kapp("Zgt",[t1;t2]) -> Rgt (t1,t2) + | _ -> parse_logic_rel t + with e when Logic.catchable_exception e -> Rother + +let is_scalar t = + let rec aux t = match destructurate t with + | Kapp(("Zplus"|"Zminus"|"Zmult"),[t1;t2]) -> aux t1 & aux t2 + | Kapp(("Zopp"|"Zsucc"|"Zpred"),[t]) -> aux t + | Kapp(("Zpos"|"Zneg"|"Z0"),_) -> let _ = recognize t in true + | _ -> false in + try aux t with _ -> false + +end diff --git a/plugins/romega/const_omega.mli b/plugins/romega/const_omega.mli new file mode 100644 index 00000000..b8db71e4 --- /dev/null +++ b/plugins/romega/const_omega.mli @@ -0,0 +1,176 @@ +(************************************************************************* + + PROJET RNRT Calife - 2001 + Author: Pierre Crégut - France Télécom R&D + Licence : LGPL version 2.1 + + *************************************************************************) + + +(** Coq objects used in romega *) + +(* from Logic *) +val coq_refl_equal : Term.constr lazy_t +val coq_and : Term.constr lazy_t +val coq_not : Term.constr lazy_t +val coq_or : Term.constr lazy_t +val coq_True : Term.constr lazy_t +val coq_False : Term.constr lazy_t +val coq_I : Term.constr lazy_t + +(* from ReflOmegaCore/ZOmega *) +val coq_h_step : Term.constr lazy_t +val coq_pair_step : Term.constr lazy_t +val coq_p_left : Term.constr lazy_t +val coq_p_right : Term.constr lazy_t +val coq_p_invert : Term.constr lazy_t +val coq_p_step : Term.constr lazy_t + +val coq_t_int : Term.constr lazy_t +val coq_t_plus : Term.constr lazy_t +val coq_t_mult : Term.constr lazy_t +val coq_t_opp : Term.constr lazy_t +val coq_t_minus : Term.constr lazy_t +val coq_t_var : Term.constr lazy_t + +val coq_proposition : Term.constr lazy_t +val coq_p_eq : Term.constr lazy_t +val coq_p_leq : Term.constr lazy_t +val coq_p_geq : Term.constr lazy_t +val coq_p_lt : Term.constr lazy_t +val coq_p_gt : Term.constr lazy_t +val coq_p_neq : Term.constr lazy_t +val coq_p_true : Term.constr lazy_t +val coq_p_false : Term.constr lazy_t +val coq_p_not : Term.constr lazy_t +val coq_p_or : Term.constr lazy_t +val coq_p_and : Term.constr lazy_t +val coq_p_imp : Term.constr lazy_t +val coq_p_prop : Term.constr lazy_t + +val coq_f_equal : Term.constr lazy_t +val coq_f_cancel : Term.constr lazy_t +val coq_f_left : Term.constr lazy_t +val coq_f_right : Term.constr lazy_t + +val coq_c_do_both : Term.constr lazy_t +val coq_c_do_left : Term.constr lazy_t +val coq_c_do_right : Term.constr lazy_t +val coq_c_do_seq : Term.constr lazy_t +val coq_c_nop : Term.constr lazy_t +val coq_c_opp_plus : Term.constr lazy_t +val coq_c_opp_opp : Term.constr lazy_t +val coq_c_opp_mult_r : Term.constr lazy_t +val coq_c_opp_one : Term.constr lazy_t +val coq_c_reduce : Term.constr lazy_t +val coq_c_mult_plus_distr : Term.constr lazy_t +val coq_c_opp_left : Term.constr lazy_t +val coq_c_mult_assoc_r : Term.constr lazy_t +val coq_c_plus_assoc_r : Term.constr lazy_t +val coq_c_plus_assoc_l : Term.constr lazy_t +val coq_c_plus_permute : Term.constr lazy_t +val coq_c_plus_comm : Term.constr lazy_t +val coq_c_red0 : Term.constr lazy_t +val coq_c_red1 : Term.constr lazy_t +val coq_c_red2 : Term.constr lazy_t +val coq_c_red3 : Term.constr lazy_t +val coq_c_red4 : Term.constr lazy_t +val coq_c_red5 : Term.constr lazy_t +val coq_c_red6 : Term.constr lazy_t +val coq_c_mult_opp_left : Term.constr lazy_t +val coq_c_mult_assoc_reduced : Term.constr lazy_t +val coq_c_minus : Term.constr lazy_t +val coq_c_mult_comm : Term.constr lazy_t + +val coq_s_constant_not_nul : Term.constr lazy_t +val coq_s_constant_neg : Term.constr lazy_t +val coq_s_div_approx : Term.constr lazy_t +val coq_s_not_exact_divide : Term.constr lazy_t +val coq_s_exact_divide : Term.constr lazy_t +val coq_s_sum : Term.constr lazy_t +val coq_s_state : Term.constr lazy_t +val coq_s_contradiction : Term.constr lazy_t +val coq_s_merge_eq : Term.constr lazy_t +val coq_s_split_ineq : Term.constr lazy_t +val coq_s_constant_nul : Term.constr lazy_t +val coq_s_negate_contradict : Term.constr lazy_t +val coq_s_negate_contradict_inv : Term.constr lazy_t + +val coq_direction : Term.constr lazy_t +val coq_d_left : Term.constr lazy_t +val coq_d_right : Term.constr lazy_t +val coq_d_mono : Term.constr lazy_t + +val coq_e_split : Term.constr lazy_t +val coq_e_extract : Term.constr lazy_t +val coq_e_solve : Term.constr lazy_t + +val coq_interp_sequent : Term.constr lazy_t +val coq_do_omega : Term.constr lazy_t + +(** Building expressions *) + +val do_left : Term.constr -> Term.constr +val do_right : Term.constr -> Term.constr +val do_both : Term.constr -> Term.constr -> Term.constr +val do_seq : Term.constr -> Term.constr -> Term.constr +val do_list : Term.constr list -> Term.constr + +val mk_nat : int -> Term.constr +val mk_list : Term.constr -> Term.constr list -> Term.constr +val mk_plist : Term.types list -> Term.types +val mk_shuffle_list : Term.constr list -> Term.constr + +(** Analyzing a coq term *) + +(* The generic result shape of the analysis of a term. + One-level depth, except when a number is found *) +type parse_term = + Tplus of Term.constr * Term.constr + | Tmult of Term.constr * Term.constr + | Tminus of Term.constr * Term.constr + | Topp of Term.constr + | Tsucc of Term.constr + | Tnum of Bigint.bigint + | Tother + +(* The generic result shape of the analysis of a relation. + One-level depth. *) +type parse_rel = + Req of Term.constr * Term.constr + | Rne of Term.constr * Term.constr + | Rlt of Term.constr * Term.constr + | Rle of Term.constr * Term.constr + | Rgt of Term.constr * Term.constr + | Rge of Term.constr * Term.constr + | Rtrue + | Rfalse + | Rnot of Term.constr + | Ror of Term.constr * Term.constr + | Rand of Term.constr * Term.constr + | Rimp of Term.constr * Term.constr + | Riff of Term.constr * Term.constr + | Rother + +(* A module factorizing what we should now about the number representation *) +module type Int = + sig + (* the coq type of the numbers *) + val typ : Term.constr Lazy.t + (* the operations on the numbers *) + val plus : Term.constr Lazy.t + val mult : Term.constr Lazy.t + val opp : Term.constr Lazy.t + val minus : Term.constr Lazy.t + (* building a coq number *) + val mk : Bigint.bigint -> Term.constr + (* parsing a term (one level, except if a number is found) *) + val parse_term : Term.constr -> parse_term + (* parsing a relation expression, including = < <= >= > *) + val parse_rel : Proof_type.goal Tacmach.sigma -> Term.constr -> parse_rel + (* Is a particular term only made of numbers and + * - ? *) + val is_scalar : Term.constr -> bool + end + +(* Currently, we only use Z numbers *) +module Z : Int diff --git a/plugins/romega/g_romega.ml4 b/plugins/romega/g_romega.ml4 new file mode 100644 index 00000000..2db86e00 --- /dev/null +++ b/plugins/romega/g_romega.ml4 @@ -0,0 +1,42 @@ +(************************************************************************* + + PROJET RNRT Calife - 2001 + Author: Pierre Crégut - France Télécom R&D + Licence : LGPL version 2.1 + + *************************************************************************) + +(*i camlp4deps: "parsing/grammar.cma" i*) + +open Refl_omega +open Refiner + +let romega_tactic l = + let tacs = List.map + (function + | "nat" -> Tacinterp.interp <:tactic<zify_nat>> + | "positive" -> Tacinterp.interp <:tactic<zify_positive>> + | "N" -> Tacinterp.interp <:tactic<zify_N>> + | "Z" -> Tacinterp.interp <:tactic<zify_op>> + | s -> Util.error ("No ROmega knowledge base for type "^s)) + (Util.list_uniquize (List.sort compare l)) + in + tclTHEN + (tclREPEAT (tclPROGRESS (tclTHENLIST tacs))) + (tclTHEN + (* because of the contradiction process in (r)omega, + we'd better leave as little as possible in the conclusion, + for an easier decidability argument. *) + Tactics.intros + total_reflexive_omega_tactic) + + +TACTIC EXTEND romega +| [ "romega" ] -> [ romega_tactic [] ] +END + +TACTIC EXTEND romega' +| [ "romega" "with" ne_ident_list(l) ] -> + [ romega_tactic (List.map Names.string_of_id l) ] +| [ "romega" "with" "*" ] -> [ romega_tactic ["nat";"positive";"N";"Z"] ] +END diff --git a/plugins/romega/refl_omega.ml b/plugins/romega/refl_omega.ml new file mode 100644 index 00000000..570bb187 --- /dev/null +++ b/plugins/romega/refl_omega.ml @@ -0,0 +1,1299 @@ +(************************************************************************* + + PROJET RNRT Calife - 2001 + Author: Pierre Crégut - France Télécom R&D + Licence : LGPL version 2.1 + + *************************************************************************) + +open Util +open Const_omega +module OmegaSolver = Omega.MakeOmegaSolver (Bigint) +open OmegaSolver + +(* \section{Useful functions and flags} *) +(* Especially useful debugging functions *) +let debug = ref false + +let show_goal gl = + if !debug then Pp.ppnl (Tacmach.pr_gls gl); Tacticals.tclIDTAC gl + +let pp i = print_int i; print_newline (); flush stdout + +(* More readable than the prefix notation *) +let (>>) = Tacticals.tclTHEN + +let mkApp = Term.mkApp + +(* \section{Types} + \subsection{How to walk in a term} + To represent how to get to a proposition. Only choice points are + kept (branch to choose in a disjunction and identifier of the disjunctive + connector) *) +type direction = Left of int | Right of int + +(* Step to find a proposition (operators are at most binary). A list is + a path *) +type occ_step = O_left | O_right | O_mono +type occ_path = occ_step list + +(* chemin identifiant une proposition sous forme du nom de l'hypothèse et + d'une liste de pas à partir de la racine de l'hypothèse *) +type occurence = {o_hyp : Names.identifier; o_path : occ_path} + +(* \subsection{refiable formulas} *) +type oformula = + (* integer *) + | Oint of Bigint.bigint + (* recognized binary and unary operations *) + | Oplus of oformula * oformula + | Omult of oformula * oformula + | Ominus of oformula * oformula + | Oopp of oformula + (* an atome in the environment *) + | Oatom of int + (* weird expression that cannot be translated *) + | Oufo of oformula + +(* Operators for comparison recognized by Omega *) +type comparaison = Eq | Leq | Geq | Gt | Lt | Neq + +(* Type des prédicats réifiés (fragment de calcul propositionnel. Les + * quantifications sont externes au langage) *) +type oproposition = + Pequa of Term.constr * oequation + | Ptrue + | Pfalse + | Pnot of oproposition + | Por of int * oproposition * oproposition + | Pand of int * oproposition * oproposition + | Pimp of int * oproposition * oproposition + | Pprop of Term.constr + +(* Les équations ou proposiitions atomiques utiles du calcul *) +and oequation = { + e_comp: comparaison; (* comparaison *) + e_left: oformula; (* formule brute gauche *) + e_right: oformula; (* formule brute droite *) + e_trace: Term.constr; (* tactique de normalisation *) + e_origin: occurence; (* l'hypothèse dont vient le terme *) + e_negated: bool; (* vrai si apparait en position nié + après normalisation *) + e_depends: direction list; (* liste des points de disjonction dont + dépend l'accès à l'équation avec la + direction (branche) pour y accéder *) + e_omega: afine (* la fonction normalisée *) + } + +(* \subsection{Proof context} + This environment codes + \begin{itemize} + \item the terms and propositions that are given as + parameters of the reified proof (and are represented as variables in the + reified goals) + \item translation functions linking the decision procedure and the Coq proof + \end{itemize} *) + +type environment = { + (* La liste des termes non reifies constituant l'environnement global *) + mutable terms : Term.constr list; + (* La meme chose pour les propositions *) + mutable props : Term.constr list; + (* Les variables introduites par omega *) + mutable om_vars : (oformula * int) list; + (* Traduction des indices utilisés ici en les indices finaux utilisés par + * la tactique Omega après dénombrement des variables utiles *) + real_indices : (int,int) Hashtbl.t; + mutable cnt_connectors : int; + equations : (int,oequation) Hashtbl.t; + constructors : (int, occurence) Hashtbl.t +} + +(* \subsection{Solution tree} + Définition d'une solution trouvée par Omega sous la forme d'un identifiant, + d'un ensemble d'équation dont dépend la solution et d'une trace *) +(* La liste des dépendances est triée et sans redondance *) +type solution = { + s_index : int; + s_equa_deps : int list; + s_trace : action list } + +(* Arbre de solution résolvant complètement un ensemble de systèmes *) +type solution_tree = + Leaf of solution + (* un noeud interne représente un point de branchement correspondant à + l'élimination d'un connecteur générant plusieurs buts + (typ. disjonction). Le premier argument + est l'identifiant du connecteur *) + | Tree of int * solution_tree * solution_tree + +(* Représentation de l'environnement extrait du but initial sous forme de + chemins pour extraire des equations ou d'hypothèses *) + +type context_content = + CCHyp of occurence + | CCEqua of int + +(* \section{Specific utility functions to handle base types} *) +(* Nom arbitraire de l'hypothèse codant la négation du but final *) +let id_concl = Names.id_of_string "__goal__" + +(* Initialisation de l'environnement de réification de la tactique *) +let new_environment () = { + terms = []; props = []; om_vars = []; cnt_connectors = 0; + real_indices = Hashtbl.create 7; + equations = Hashtbl.create 7; + constructors = Hashtbl.create 7; +} + +(* Génération d'un nom d'équation *) +let new_connector_id env = + env.cnt_connectors <- succ env.cnt_connectors; env.cnt_connectors + +(* Calcul de la branche complémentaire *) +let barre = function Left x -> Right x | Right x -> Left x + +(* Identifiant associé à une branche *) +let indice = function Left x | Right x -> x + +(* Affichage de l'environnement de réification (termes et propositions) *) +let print_env_reification env = + let rec loop c i = function + [] -> Printf.printf " ===============================\n\n" + | t :: l -> + Printf.printf " (%c%02d) := " c i; + Pp.ppnl (Printer.pr_lconstr t); + Pp.flush_all (); + loop c (succ i) l in + print_newline (); + Printf.printf " ENVIRONMENT OF PROPOSITIONS :\n\n"; loop 'P' 0 env.props; + Printf.printf " ENVIRONMENT OF TERMS :\n\n"; loop 'V' 0 env.terms + + +(* \subsection{Gestion des environnements de variable pour Omega} *) +(* generation d'identifiant d'equation pour Omega *) + +let new_omega_eq, rst_omega_eq = + let cpt = ref 0 in + (function () -> incr cpt; !cpt), + (function () -> cpt:=0) + +(* generation d'identifiant de variable pour Omega *) + +let new_omega_var, rst_omega_var = + let cpt = ref 0 in + (function () -> incr cpt; !cpt), + (function () -> cpt:=0) + +(* Affichage des variables d'un système *) + +let display_omega_var i = Printf.sprintf "OV%d" i + +(* Recherche la variable codant un terme pour Omega et crée la variable dans + l'environnement si il n'existe pas. Cas ou la variable dans Omega représente + le terme d'un monome (le plus souvent un atome) *) + +let intern_omega env t = + begin try List.assoc t env.om_vars + with Not_found -> + let v = new_omega_var () in + env.om_vars <- (t,v) :: env.om_vars; v + end + +(* Ajout forcé d'un lien entre un terme et une variable Cas où la + variable est créée par Omega et où il faut la lier après coup à un atome + réifié introduit de force *) +let intern_omega_force env t v = env.om_vars <- (t,v) :: env.om_vars + +(* Récupère le terme associé à une variable *) +let unintern_omega env id = + let rec loop = function + [] -> failwith "unintern" + | ((t,j)::l) -> if id = j then t else loop l in + loop env.om_vars + +(* \subsection{Gestion des environnements de variable pour la réflexion} + Gestion des environnements de traduction entre termes des constructions + non réifiés et variables des termes reifies. Attention il s'agit de + l'environnement initial contenant tout. Il faudra le réduire après + calcul des variables utiles. *) + +let add_reified_atom t env = + try list_index0 t env.terms + with Not_found -> + let i = List.length env.terms in + env.terms <- env.terms @ [t]; i + +let get_reified_atom env = + try List.nth env.terms with _ -> failwith "get_reified_atom" + +(* \subsection{Gestion de l'environnement de proposition pour Omega} *) +(* ajout d'une proposition *) +let add_prop env t = + try list_index0 t env.props + with Not_found -> + let i = List.length env.props in env.props <- env.props @ [t]; i + +(* accès a une proposition *) +let get_prop v env = try List.nth v env with _ -> failwith "get_prop" + +(* \subsection{Gestion du nommage des équations} *) +(* Ajout d'une equation dans l'environnement de reification *) +let add_equation env e = + let id = e.e_omega.id in + try let _ = Hashtbl.find env.equations id in () + with Not_found -> Hashtbl.add env.equations id e + +(* accès a une equation *) +let get_equation env id = + try Hashtbl.find env.equations id + with e -> Printf.printf "Omega Equation %d non trouvée\n" id; raise e + +(* Affichage des termes réifiés *) +let rec oprint ch = function + | Oint n -> Printf.fprintf ch "%s" (Bigint.to_string n) + | Oplus (t1,t2) -> Printf.fprintf ch "(%a + %a)" oprint t1 oprint t2 + | Omult (t1,t2) -> Printf.fprintf ch "(%a * %a)" oprint t1 oprint t2 + | Ominus(t1,t2) -> Printf.fprintf ch "(%a - %a)" oprint t1 oprint t2 + | Oopp t1 ->Printf.fprintf ch "~ %a" oprint t1 + | Oatom n -> Printf.fprintf ch "V%02d" n + | Oufo x -> Printf.fprintf ch "?" + +let rec pprint ch = function + Pequa (_,{ e_comp=comp; e_left=t1; e_right=t2 }) -> + let connector = + match comp with + Eq -> "=" | Leq -> "<=" | Geq -> ">=" + | Gt -> ">" | Lt -> "<" | Neq -> "!=" in + Printf.fprintf ch "%a %s %a" oprint t1 connector oprint t2 + | Ptrue -> Printf.fprintf ch "TT" + | Pfalse -> Printf.fprintf ch "FF" + | Pnot t -> Printf.fprintf ch "not(%a)" pprint t + | Por (_,t1,t2) -> Printf.fprintf ch "(%a or %a)" pprint t1 pprint t2 + | Pand(_,t1,t2) -> Printf.fprintf ch "(%a and %a)" pprint t1 pprint t2 + | Pimp(_,t1,t2) -> Printf.fprintf ch "(%a => %a)" pprint t1 pprint t2 + | Pprop c -> Printf.fprintf ch "Prop" + +let rec weight env = function + | Oint _ -> -1 + | Oopp c -> weight env c + | Omult(c,_) -> weight env c + | Oplus _ -> failwith "weight" + | Ominus _ -> failwith "weight minus" + | Oufo _ -> -1 + | Oatom _ as c -> (intern_omega env c) + +(* \section{Passage entre oformules et représentation interne de Omega} *) + +(* \subsection{Oformula vers Omega} *) + +let omega_of_oformula env kind = + let rec loop accu = function + | Oplus(Omult(v,Oint n),r) -> + loop ({v=intern_omega env v; c=n} :: accu) r + | Oint n -> + let id = new_omega_eq () in + (*i tag_equation name id; i*) + {kind = kind; body = List.rev accu; + constant = n; id = id} + | t -> print_string "CO"; oprint stdout t; failwith "compile_equation" in + loop [] + +(* \subsection{Omega vers Oformula} *) + +let rec oformula_of_omega env af = + let rec loop = function + | ({v=v; c=n}::r) -> + Oplus(Omult(unintern_omega env v,Oint n),loop r) + | [] -> Oint af.constant in + loop af.body + +let app f v = mkApp(Lazy.force f,v) + +(* \subsection{Oformula vers COQ reel} *) + +let rec coq_of_formula env t = + let rec loop = function + | Oplus (t1,t2) -> app Z.plus [| loop t1; loop t2 |] + | Oopp t -> app Z.opp [| loop t |] + | Omult(t1,t2) -> app Z.mult [| loop t1; loop t2 |] + | Oint v -> Z.mk v + | Oufo t -> loop t + | Oatom var -> + (* attention ne traite pas les nouvelles variables si on ne les + * met pas dans env.term *) + get_reified_atom env var + | Ominus(t1,t2) -> app Z.minus [| loop t1; loop t2 |] in + loop t + +(* \subsection{Oformula vers COQ reifié} *) + +let reified_of_atom env i = + try Hashtbl.find env.real_indices i + with Not_found -> + Printf.printf "Atome %d non trouvé\n" i; + Hashtbl.iter (fun k v -> Printf.printf "%d -> %d\n" k v) env.real_indices; + raise Not_found + +let rec reified_of_formula env = function + | Oplus (t1,t2) -> + app coq_t_plus [| reified_of_formula env t1; reified_of_formula env t2 |] + | Oopp t -> + app coq_t_opp [| reified_of_formula env t |] + | Omult(t1,t2) -> + app coq_t_mult [| reified_of_formula env t1; reified_of_formula env t2 |] + | Oint v -> app coq_t_int [| Z.mk v |] + | Oufo t -> reified_of_formula env t + | Oatom i -> app coq_t_var [| mk_nat (reified_of_atom env i) |] + | Ominus(t1,t2) -> + app coq_t_minus [| reified_of_formula env t1; reified_of_formula env t2 |] + +let reified_of_formula env f = + begin try reified_of_formula env f with e -> oprint stderr f; raise e end + +let rec reified_of_proposition env = function + Pequa (_,{ e_comp=Eq; e_left=t1; e_right=t2 }) -> + app coq_p_eq [| reified_of_formula env t1; reified_of_formula env t2 |] + | Pequa (_,{ e_comp=Leq; e_left=t1; e_right=t2 }) -> + app coq_p_leq [| reified_of_formula env t1; reified_of_formula env t2 |] + | Pequa(_,{ e_comp=Geq; e_left=t1; e_right=t2 }) -> + app coq_p_geq [| reified_of_formula env t1; reified_of_formula env t2 |] + | Pequa(_,{ e_comp=Gt; e_left=t1; e_right=t2 }) -> + app coq_p_gt [| reified_of_formula env t1; reified_of_formula env t2 |] + | Pequa(_,{ e_comp=Lt; e_left=t1; e_right=t2 }) -> + app coq_p_lt [| reified_of_formula env t1; reified_of_formula env t2 |] + | Pequa(_,{ e_comp=Neq; e_left=t1; e_right=t2 }) -> + app coq_p_neq [| reified_of_formula env t1; reified_of_formula env t2 |] + | Ptrue -> Lazy.force coq_p_true + | Pfalse -> Lazy.force coq_p_false + | Pnot t -> + app coq_p_not [| reified_of_proposition env t |] + | Por (_,t1,t2) -> + app coq_p_or + [| reified_of_proposition env t1; reified_of_proposition env t2 |] + | Pand(_,t1,t2) -> + app coq_p_and + [| reified_of_proposition env t1; reified_of_proposition env t2 |] + | Pimp(_,t1,t2) -> + app coq_p_imp + [| reified_of_proposition env t1; reified_of_proposition env t2 |] + | Pprop t -> app coq_p_prop [| mk_nat (add_prop env t) |] + +let reified_of_proposition env f = + begin try reified_of_proposition env f + with e -> pprint stderr f; raise e end + +(* \subsection{Omega vers COQ réifié} *) + +let reified_of_omega env body constant = + let coeff_constant = + app coq_t_int [| Z.mk constant |] in + let mk_coeff {c=c; v=v} t = + let coef = + app coq_t_mult + [| reified_of_formula env (unintern_omega env v); + app coq_t_int [| Z.mk c |] |] in + app coq_t_plus [|coef; t |] in + List.fold_right mk_coeff body coeff_constant + +let reified_of_omega env body c = + begin try + reified_of_omega env body c + with e -> + display_eq display_omega_var (body,c); raise e + end + +(* \section{Opérations sur les équations} +Ces fonctions préparent les traces utilisées par la tactique réfléchie +pour faire des opérations de normalisation sur les équations. *) + +(* \subsection{Extractions des variables d'une équation} *) +(* Extraction des variables d'une équation. *) +(* Chaque fonction retourne une liste triée sans redondance *) + +let (@@) = list_merge_uniq compare + +let rec vars_of_formula = function + | Oint _ -> [] + | Oplus (e1,e2) -> (vars_of_formula e1) @@ (vars_of_formula e2) + | Omult (e1,e2) -> (vars_of_formula e1) @@ (vars_of_formula e2) + | Ominus (e1,e2) -> (vars_of_formula e1) @@ (vars_of_formula e2) + | Oopp e -> vars_of_formula e + | Oatom i -> [i] + | Oufo _ -> [] + +let rec vars_of_equations = function + | [] -> [] + | e::l -> + (vars_of_formula e.e_left) @@ + (vars_of_formula e.e_right) @@ + (vars_of_equations l) + +let rec vars_of_prop = function + | Pequa(_,e) -> vars_of_equations [e] + | Pnot p -> vars_of_prop p + | Por(_,p1,p2) -> (vars_of_prop p1) @@ (vars_of_prop p2) + | Pand(_,p1,p2) -> (vars_of_prop p1) @@ (vars_of_prop p2) + | Pimp(_,p1,p2) -> (vars_of_prop p1) @@ (vars_of_prop p2) + | Pprop _ | Ptrue | Pfalse -> [] + +(* \subsection{Multiplication par un scalaire} *) + +let rec scalar n = function + Oplus(t1,t2) -> + let tac1,t1' = scalar n t1 and + tac2,t2' = scalar n t2 in + do_list [Lazy.force coq_c_mult_plus_distr; do_both tac1 tac2], + Oplus(t1',t2') + | Oopp t -> + do_list [Lazy.force coq_c_mult_opp_left], Omult(t,Oint(Bigint.neg n)) + | Omult(t1,Oint x) -> + do_list [Lazy.force coq_c_mult_assoc_reduced], Omult(t1,Oint (n*x)) + | Omult(t1,t2) -> + Util.error "Omega: Can't solve a goal with non-linear products" + | (Oatom _ as t) -> do_list [], Omult(t,Oint n) + | Oint i -> do_list [Lazy.force coq_c_reduce],Oint(n*i) + | (Oufo _ as t)-> do_list [], Oufo (Omult(t,Oint n)) + | Ominus _ -> failwith "scalar minus" + +(* \subsection{Propagation de l'inversion} *) + +let rec negate = function + Oplus(t1,t2) -> + let tac1,t1' = negate t1 and + tac2,t2' = negate t2 in + do_list [Lazy.force coq_c_opp_plus ; (do_both tac1 tac2)], + Oplus(t1',t2') + | Oopp t -> + do_list [Lazy.force coq_c_opp_opp], t + | Omult(t1,Oint x) -> + do_list [Lazy.force coq_c_opp_mult_r], Omult(t1,Oint (Bigint.neg x)) + | Omult(t1,t2) -> + Util.error "Omega: Can't solve a goal with non-linear products" + | (Oatom _ as t) -> + do_list [Lazy.force coq_c_opp_one], Omult(t,Oint(negone)) + | Oint i -> do_list [Lazy.force coq_c_reduce] ,Oint(Bigint.neg i) + | Oufo c -> do_list [], Oufo (Oopp c) + | Ominus _ -> failwith "negate minus" + +let rec norm l = (List.length l) + +(* \subsection{Mélange (fusion) de deux équations} *) +(* \subsubsection{Version avec coefficients} *) +let rec shuffle_path k1 e1 k2 e2 = + let rec loop = function + (({c=c1;v=v1}::l1) as l1'), + (({c=c2;v=v2}::l2) as l2') -> + if v1 = v2 then + if k1*c1 + k2 * c2 = zero then ( + Lazy.force coq_f_cancel :: loop (l1,l2)) + else ( + Lazy.force coq_f_equal :: loop (l1,l2) ) + else if v1 > v2 then ( + Lazy.force coq_f_left :: loop(l1,l2')) + else ( + Lazy.force coq_f_right :: loop(l1',l2)) + | ({c=c1;v=v1}::l1), [] -> + Lazy.force coq_f_left :: loop(l1,[]) + | [],({c=c2;v=v2}::l2) -> + Lazy.force coq_f_right :: loop([],l2) + | [],[] -> flush stdout; [] in + mk_shuffle_list (loop (e1,e2)) + +(* \subsubsection{Version sans coefficients} *) +let rec shuffle env (t1,t2) = + match t1,t2 with + Oplus(l1,r1), Oplus(l2,r2) -> + if weight env l1 > weight env l2 then + let l_action,t' = shuffle env (r1,t2) in + do_list [Lazy.force coq_c_plus_assoc_r;do_right l_action], Oplus(l1,t') + else + let l_action,t' = shuffle env (t1,r2) in + do_list [Lazy.force coq_c_plus_permute;do_right l_action], Oplus(l2,t') + | Oplus(l1,r1), t2 -> + if weight env l1 > weight env t2 then + let (l_action,t') = shuffle env (r1,t2) in + do_list [Lazy.force coq_c_plus_assoc_r;do_right l_action],Oplus(l1, t') + else do_list [Lazy.force coq_c_plus_comm], Oplus(t2,t1) + | t1,Oplus(l2,r2) -> + if weight env l2 > weight env t1 then + let (l_action,t') = shuffle env (t1,r2) in + do_list [Lazy.force coq_c_plus_permute;do_right l_action], Oplus(l2,t') + else do_list [],Oplus(t1,t2) + | Oint t1,Oint t2 -> + do_list [Lazy.force coq_c_reduce], Oint(t1+t2) + | t1,t2 -> + if weight env t1 < weight env t2 then + do_list [Lazy.force coq_c_plus_comm], Oplus(t2,t1) + else do_list [],Oplus(t1,t2) + +(* \subsection{Fusion avec réduction} *) + +let shrink_pair f1 f2 = + begin match f1,f2 with + Oatom v,Oatom _ -> + Lazy.force coq_c_red1, Omult(Oatom v,Oint two) + | Oatom v, Omult(_,c2) -> + Lazy.force coq_c_red2, Omult(Oatom v,Oplus(c2,Oint one)) + | Omult (v1,c1),Oatom v -> + Lazy.force coq_c_red3, Omult(Oatom v,Oplus(c1,Oint one)) + | Omult (Oatom v,c1),Omult (v2,c2) -> + Lazy.force coq_c_red4, Omult(Oatom v,Oplus(c1,c2)) + | t1,t2 -> + oprint stdout t1; print_newline (); oprint stdout t2; print_newline (); + flush Pervasives.stdout; Util.error "shrink.1" + end + +(* \subsection{Calcul d'une sous formule constante} *) + +let reduce_factor = function + Oatom v -> + let r = Omult(Oatom v,Oint one) in + [Lazy.force coq_c_red0],r + | Omult(Oatom v,Oint n) as f -> [],f + | Omult(Oatom v,c) -> + let rec compute = function + Oint n -> n + | Oplus(t1,t2) -> compute t1 + compute t2 + | _ -> Util.error "condense.1" in + [Lazy.force coq_c_reduce], Omult(Oatom v,Oint(compute c)) + | t -> Util.error "reduce_factor.1" + +(* \subsection{Réordonnancement} *) + +let rec condense env = function + Oplus(f1,(Oplus(f2,r) as t)) -> + if weight env f1 = weight env f2 then begin + let shrink_tac,t = shrink_pair f1 f2 in + let assoc_tac = Lazy.force coq_c_plus_assoc_l in + let tac_list,t' = condense env (Oplus(t,r)) in + assoc_tac :: do_left (do_list [shrink_tac]) :: tac_list, t' + end else begin + let tac,f = reduce_factor f1 in + let tac',t' = condense env t in + [do_both (do_list tac) (do_list tac')], Oplus(f,t') + end + | Oplus(f1,Oint n) -> + let tac,f1' = reduce_factor f1 in + [do_left (do_list tac)],Oplus(f1',Oint n) + | Oplus(f1,f2) -> + if weight env f1 = weight env f2 then begin + let tac_shrink,t = shrink_pair f1 f2 in + let tac,t' = condense env t in + tac_shrink :: tac,t' + end else begin + let tac,f = reduce_factor f1 in + let tac',t' = condense env f2 in + [do_both (do_list tac) (do_list tac')],Oplus(f,t') + end + | (Oint _ as t)-> [],t + | t -> + let tac,t' = reduce_factor t in + let final = Oplus(t',Oint zero) in + tac @ [Lazy.force coq_c_red6], final + +(* \subsection{Elimination des zéros} *) + +let rec clear_zero = function + Oplus(Omult(Oatom v,Oint n),r) when n=zero -> + let tac',t = clear_zero r in + Lazy.force coq_c_red5 :: tac',t + | Oplus(f,r) -> + let tac,t = clear_zero r in + (if tac = [] then [] else [do_right (do_list tac)]),Oplus(f,t) + | t -> [],t;; + +(* \subsection{Transformation des hypothèses} *) + +let rec reduce env = function + Oplus(t1,t2) -> + let t1', trace1 = reduce env t1 in + let t2', trace2 = reduce env t2 in + let trace3,t' = shuffle env (t1',t2') in + t', do_list [do_both trace1 trace2; trace3] + | Ominus(t1,t2) -> + let t,trace = reduce env (Oplus(t1, Oopp t2)) in + t, do_list [Lazy.force coq_c_minus; trace] + | Omult(t1,t2) as t -> + let t1', trace1 = reduce env t1 in + let t2', trace2 = reduce env t2 in + begin match t1',t2' with + | (_, Oint n) -> + let tac,t' = scalar n t1' in + t', do_list [do_both trace1 trace2; tac] + | (Oint n,_) -> + let tac,t' = scalar n t2' in + t', do_list [do_both trace1 trace2; Lazy.force coq_c_mult_comm; tac] + | _ -> Oufo t, Lazy.force coq_c_nop + end + | Oopp t -> + let t',trace = reduce env t in + let trace',t'' = negate t' in + t'', do_list [do_left trace; trace'] + | (Oint _ | Oatom _ | Oufo _) as t -> t, Lazy.force coq_c_nop + +let normalize_linear_term env t = + let t1,trace1 = reduce env t in + let trace2,t2 = condense env t1 in + let trace3,t3 = clear_zero t2 in + do_list [trace1; do_list trace2; do_list trace3], t3 + +(* Cette fonction reproduit très exactement le comportement de [p_invert] *) +let negate_oper = function + Eq -> Neq | Neq -> Eq | Leq -> Gt | Geq -> Lt | Lt -> Geq | Gt -> Leq + +let normalize_equation env (negated,depends,origin,path) (oper,t1,t2) = + let mk_step t1 t2 f kind = + let t = f t1 t2 in + let trace, oterm = normalize_linear_term env t in + let equa = omega_of_oformula env kind oterm in + { e_comp = oper; e_left = t1; e_right = t2; + e_negated = negated; e_depends = depends; + e_origin = { o_hyp = origin; o_path = List.rev path }; + e_trace = trace; e_omega = equa } in + try match (if negated then (negate_oper oper) else oper) with + | Eq -> mk_step t1 t2 (fun o1 o2 -> Oplus (o1,Oopp o2)) EQUA + | Neq -> mk_step t1 t2 (fun o1 o2 -> Oplus (o1,Oopp o2)) DISE + | Leq -> mk_step t1 t2 (fun o1 o2 -> Oplus (o2,Oopp o1)) INEQ + | Geq -> mk_step t1 t2 (fun o1 o2 -> Oplus (o1,Oopp o2)) INEQ + | Lt -> + mk_step t1 t2 (fun o1 o2 -> Oplus (Oplus(o2,Oint negone),Oopp o1)) + INEQ + | Gt -> + mk_step t1 t2 (fun o1 o2 -> Oplus (Oplus(o1,Oint negone),Oopp o2)) + INEQ + with e when Logic.catchable_exception e -> raise e + +(* \section{Compilation des hypothèses} *) + +let rec oformula_of_constr env t = + match Z.parse_term t with + | Tplus (t1,t2) -> binop env (fun x y -> Oplus(x,y)) t1 t2 + | Tminus (t1,t2) -> binop env (fun x y -> Ominus(x,y)) t1 t2 + | Tmult (t1,t2) when Z.is_scalar t1 || Z.is_scalar t2 -> + binop env (fun x y -> Omult(x,y)) t1 t2 + | Topp t -> Oopp(oformula_of_constr env t) + | Tsucc t -> Oplus(oformula_of_constr env t, Oint one) + | Tnum n -> Oint n + | _ -> Oatom (add_reified_atom t env) + +and binop env c t1 t2 = + let t1' = oformula_of_constr env t1 in + let t2' = oformula_of_constr env t2 in + c t1' t2' + +and binprop env (neg2,depends,origin,path) + add_to_depends neg1 gl c t1 t2 = + let i = new_connector_id env in + let depends1 = if add_to_depends then Left i::depends else depends in + let depends2 = if add_to_depends then Right i::depends else depends in + if add_to_depends then + Hashtbl.add env.constructors i {o_hyp = origin; o_path = List.rev path}; + let t1' = + oproposition_of_constr env (neg1,depends1,origin,O_left::path) gl t1 in + let t2' = + oproposition_of_constr env (neg2,depends2,origin,O_right::path) gl t2 in + (* On numérote le connecteur dans l'environnement. *) + c i t1' t2' + +and mk_equation env ctxt c connector t1 t2 = + let t1' = oformula_of_constr env t1 in + let t2' = oformula_of_constr env t2 in + (* On ajoute l'equation dans l'environnement. *) + let omega = normalize_equation env ctxt (connector,t1',t2') in + add_equation env omega; + Pequa (c,omega) + +and oproposition_of_constr env ((negated,depends,origin,path) as ctxt) gl c = + match Z.parse_rel gl c with + | Req (t1,t2) -> mk_equation env ctxt c Eq t1 t2 + | Rne (t1,t2) -> mk_equation env ctxt c Neq t1 t2 + | Rle (t1,t2) -> mk_equation env ctxt c Leq t1 t2 + | Rlt (t1,t2) -> mk_equation env ctxt c Lt t1 t2 + | Rge (t1,t2) -> mk_equation env ctxt c Geq t1 t2 + | Rgt (t1,t2) -> mk_equation env ctxt c Gt t1 t2 + | Rtrue -> Ptrue + | Rfalse -> Pfalse + | Rnot t -> + let t' = + oproposition_of_constr + env (not negated, depends, origin,(O_mono::path)) gl t in + Pnot t' + | Ror (t1,t2) -> + binprop env ctxt (not negated) negated gl (fun i x y -> Por(i,x,y)) t1 t2 + | Rand (t1,t2) -> + binprop env ctxt negated negated gl + (fun i x y -> Pand(i,x,y)) t1 t2 + | Rimp (t1,t2) -> + binprop env ctxt (not negated) (not negated) gl + (fun i x y -> Pimp(i,x,y)) t1 t2 + | Riff (t1,t2) -> + binprop env ctxt negated negated gl + (fun i x y -> Pand(i,x,y)) (Term.mkArrow t1 t2) (Term.mkArrow t2 t1) + | _ -> Pprop c + +(* Destructuration des hypothèses et de la conclusion *) + +let reify_gl env gl = + let concl = Tacmach.pf_concl gl in + let t_concl = + Pnot (oproposition_of_constr env (true,[],id_concl,[O_mono]) gl concl) in + if !debug then begin + Printf.printf "REIFED PROBLEM\n\n"; + Printf.printf " CONCL: "; pprint stdout t_concl; Printf.printf "\n" + end; + let rec loop = function + (i,t) :: lhyps -> + let t' = oproposition_of_constr env (false,[],i,[]) gl t in + if !debug then begin + Printf.printf " %s: " (Names.string_of_id i); + pprint stdout t'; + Printf.printf "\n" + end; + (i,t') :: loop lhyps + | [] -> + if !debug then print_env_reification env; + [] in + let t_lhyps = loop (Tacmach.pf_hyps_types gl) in + (id_concl,t_concl) :: t_lhyps + +let rec destructurate_pos_hyp orig list_equations list_depends = function + | Pequa (_,e) -> [e :: list_equations] + | Ptrue | Pfalse | Pprop _ -> [list_equations] + | Pnot t -> destructurate_neg_hyp orig list_equations list_depends t + | Por (i,t1,t2) -> + let s1 = + destructurate_pos_hyp orig list_equations (i::list_depends) t1 in + let s2 = + destructurate_pos_hyp orig list_equations (i::list_depends) t2 in + s1 @ s2 + | Pand(i,t1,t2) -> + let list_s1 = + destructurate_pos_hyp orig list_equations (list_depends) t1 in + let rec loop = function + le1 :: ll -> destructurate_pos_hyp orig le1 list_depends t2 @ loop ll + | [] -> [] in + loop list_s1 + | Pimp(i,t1,t2) -> + let s1 = + destructurate_neg_hyp orig list_equations (i::list_depends) t1 in + let s2 = + destructurate_pos_hyp orig list_equations (i::list_depends) t2 in + s1 @ s2 + +and destructurate_neg_hyp orig list_equations list_depends = function + | Pequa (_,e) -> [e :: list_equations] + | Ptrue | Pfalse | Pprop _ -> [list_equations] + | Pnot t -> destructurate_pos_hyp orig list_equations list_depends t + | Pand (i,t1,t2) -> + let s1 = + destructurate_neg_hyp orig list_equations (i::list_depends) t1 in + let s2 = + destructurate_neg_hyp orig list_equations (i::list_depends) t2 in + s1 @ s2 + | Por(_,t1,t2) -> + let list_s1 = + destructurate_neg_hyp orig list_equations list_depends t1 in + let rec loop = function + le1 :: ll -> destructurate_neg_hyp orig le1 list_depends t2 @ loop ll + | [] -> [] in + loop list_s1 + | Pimp(_,t1,t2) -> + let list_s1 = + destructurate_pos_hyp orig list_equations list_depends t1 in + let rec loop = function + le1 :: ll -> destructurate_neg_hyp orig le1 list_depends t2 @ loop ll + | [] -> [] in + loop list_s1 + +let destructurate_hyps syst = + let rec loop = function + (i,t) :: l -> + let l_syst1 = destructurate_pos_hyp i [] [] t in + let l_syst2 = loop l in + list_cartesian (@) l_syst1 l_syst2 + | [] -> [[]] in + loop syst + +(* \subsection{Affichage d'un système d'équation} *) + +(* Affichage des dépendances de système *) +let display_depend = function + Left i -> Printf.printf " L%d" i + | Right i -> Printf.printf " R%d" i + +let display_systems syst_list = + let display_omega om_e = + Printf.printf " E%d : %a %s 0\n" + om_e.id + (fun _ -> display_eq display_omega_var) + (om_e.body, om_e.constant) + (operator_of_eq om_e.kind) in + + let display_equation oformula_eq = + pprint stdout (Pequa (Lazy.force coq_c_nop,oformula_eq)); print_newline (); + display_omega oformula_eq.e_omega; + Printf.printf " Depends on:"; + List.iter display_depend oformula_eq.e_depends; + Printf.printf "\n Path: %s" + (String.concat "" + (List.map (function O_left -> "L" | O_right -> "R" | O_mono -> "M") + oformula_eq.e_origin.o_path)); + Printf.printf "\n Origin: %s (negated : %s)\n\n" + (Names.string_of_id oformula_eq.e_origin.o_hyp) + (if oformula_eq.e_negated then "yes" else "no") in + + let display_system syst = + Printf.printf "=SYSTEM===================================\n"; + List.iter display_equation syst in + List.iter display_system syst_list + +(* Extraction des prédicats utilisées dans une trace. Permet ensuite le + calcul des hypothèses *) + +let rec hyps_used_in_trace = function + | act :: l -> + begin match act with + | HYP e -> [e.id] @@ (hyps_used_in_trace l) + | SPLIT_INEQ (_,(_,act1),(_,act2)) -> + hyps_used_in_trace act1 @@ hyps_used_in_trace act2 + | _ -> hyps_used_in_trace l + end + | [] -> [] + +(* Extraction des variables déclarées dans une équation. Permet ensuite + de les déclarer dans l'environnement de la procédure réflexive et + éviter les créations de variable au vol *) + +let rec variable_stated_in_trace = function + | act :: l -> + begin match act with + | STATE action -> + (*i nlle_equa: afine, def: afine, eq_orig: afine, i*) + (*i coef: int, var:int i*) + action :: variable_stated_in_trace l + | SPLIT_INEQ (_,(_,act1),(_,act2)) -> + variable_stated_in_trace act1 @ variable_stated_in_trace act2 + | _ -> variable_stated_in_trace l + end + | [] -> [] +;; + +let add_stated_equations env tree = + (* Il faut trier les variables par ordre d'introduction pour ne pas risquer + de définir dans le mauvais ordre *) + let stated_equations = + let cmpvar x y = Pervasives.(-) x.st_var y.st_var in + let rec loop = function + | Tree(_,t1,t2) -> List.merge cmpvar (loop t1) (loop t2) + | Leaf s -> List.sort cmpvar (variable_stated_in_trace s.s_trace) + in loop tree + in + let add_env st = + (* On retransforme la définition de v en formule reifiée *) + let v_def = oformula_of_omega env st.st_def in + (* Notez que si l'ordre de création des variables n'est pas respecté, + * ca va planter *) + let coq_v = coq_of_formula env v_def in + let v = add_reified_atom coq_v env in + (* Le terme qu'il va falloir introduire *) + let term_to_generalize = app coq_refl_equal [|Lazy.force Z.typ; coq_v|] in + (* sa représentation sous forme d'équation mais non réifié car on n'a pas + * l'environnement pour le faire correctement *) + let term_to_reify = (v_def,Oatom v) in + (* enregistre le lien entre la variable omega et la variable Coq *) + intern_omega_force env (Oatom v) st.st_var; + (v, term_to_generalize,term_to_reify,st.st_def.id) in + List.map add_env stated_equations + +(* Calcule la liste des éclatements à réaliser sur les hypothèses + nécessaires pour extraire une liste d'équations donnée *) + +(* PL: experimentally, the result order of the following function seems + _very_ crucial for efficiency. No idea why. Do not remove the List.rev + or modify the current semantics of Util.list_union (some elements of first + arg, then second arg), unless you know what you're doing. *) + +let rec get_eclatement env = function + i :: r -> + let l = try (get_equation env i).e_depends with Not_found -> [] in + list_union (List.rev l) (get_eclatement env r) + | [] -> [] + +let select_smaller l = + let comp (_,x) (_,y) = Pervasives.(-) (List.length x) (List.length y) in + try List.hd (List.sort comp l) with Failure _ -> failwith "select_smaller" + +let filter_compatible_systems required systems = + let rec select = function + (x::l) -> + if List.mem x required then select l + else if List.mem (barre x) required then failwith "Exit" + else x :: select l + | [] -> [] in + map_succeed (function (sol,splits) -> (sol,select splits)) systems + +let rec equas_of_solution_tree = function + Tree(_,t1,t2) -> (equas_of_solution_tree t1)@@(equas_of_solution_tree t2) + | Leaf s -> s.s_equa_deps + +(* [really_useful_prop] pushes useless props in a new Pprop variable *) +(* Things get shorter, but may also get wrong, since a Prop is considered + to be undecidable in ReflOmegaCore.concl_to_hyp, whereas for instance + Pfalse is decidable. So should not be used on conclusion (??) *) + +let really_useful_prop l_equa c = + let rec real_of = function + Pequa(t,_) -> t + | Ptrue -> app coq_True [||] + | Pfalse -> app coq_False [||] + | Pnot t1 -> app coq_not [|real_of t1|] + | Por(_,t1,t2) -> app coq_or [|real_of t1; real_of t2|] + | Pand(_,t1,t2) -> app coq_and [|real_of t1; real_of t2|] + (* Attention : implications sur le lifting des variables à comprendre ! *) + | Pimp(_,t1,t2) -> Term.mkArrow (real_of t1) (real_of t2) + | Pprop t -> t in + let rec loop c = + match c with + Pequa(_,e) -> + if List.mem e.e_omega.id l_equa then Some c else None + | Ptrue -> None + | Pfalse -> None + | Pnot t1 -> + begin match loop t1 with None -> None | Some t1' -> Some (Pnot t1') end + | Por(i,t1,t2) -> binop (fun (t1,t2) -> Por(i,t1,t2)) t1 t2 + | Pand(i,t1,t2) -> binop (fun (t1,t2) -> Pand(i,t1,t2)) t1 t2 + | Pimp(i,t1,t2) -> binop (fun (t1,t2) -> Pimp(i,t1,t2)) t1 t2 + | Pprop t -> None + and binop f t1 t2 = + begin match loop t1, loop t2 with + None, None -> None + | Some t1',Some t2' -> Some (f(t1',t2')) + | Some t1',None -> Some (f(t1',Pprop (real_of t2))) + | None,Some t2' -> Some (f(Pprop (real_of t1),t2')) + end in + match loop c with + None -> Pprop (real_of c) + | Some t -> t + +let rec display_solution_tree ch = function + Leaf t -> + output_string ch + (Printf.sprintf "%d[%s]" + t.s_index + (String.concat " " (List.map string_of_int t.s_equa_deps))) + | Tree(i,t1,t2) -> + Printf.fprintf ch "S%d(%a,%a)" i + display_solution_tree t1 display_solution_tree t2 + +let rec solve_with_constraints all_solutions path = + let rec build_tree sol buf = function + [] -> Leaf sol + | (Left i :: remainder) -> + Tree(i, + build_tree sol (Left i :: buf) remainder, + solve_with_constraints all_solutions (List.rev(Right i :: buf))) + | (Right i :: remainder) -> + Tree(i, + solve_with_constraints all_solutions (List.rev (Left i :: buf)), + build_tree sol (Right i :: buf) remainder) in + let weighted = filter_compatible_systems path all_solutions in + let (winner_sol,winner_deps) = + try select_smaller weighted + with e -> + Printf.printf "%d - %d\n" + (List.length weighted) (List.length all_solutions); + List.iter display_depend path; raise e in + build_tree winner_sol (List.rev path) winner_deps + +let find_path {o_hyp=id;o_path=p} env = + let rec loop_path = function + ([],l) -> Some l + | (x1::l1,x2::l2) when x1 = x2 -> loop_path (l1,l2) + | _ -> None in + let rec loop_id i = function + CCHyp{o_hyp=id';o_path=p'} :: l when id = id' -> + begin match loop_path (p',p) with + Some r -> i,r + | None -> loop_id (succ i) l + end + | _ :: l -> loop_id (succ i) l + | [] -> failwith "find_path" in + loop_id 0 env + +let mk_direction_list l = + let trans = function + O_left -> coq_d_left | O_right -> coq_d_right | O_mono -> coq_d_mono in + mk_list (Lazy.force coq_direction) (List.map (fun d-> Lazy.force(trans d)) l) + + +(* \section{Rejouer l'historique} *) + +let get_hyp env_hyp i = + try list_index0 (CCEqua i) env_hyp + with Not_found -> failwith (Printf.sprintf "get_hyp %d" i) + +let replay_history env env_hyp = + let rec loop env_hyp t = + match t with + | CONTRADICTION (e1,e2) :: l -> + let trace = mk_nat (List.length e1.body) in + mkApp (Lazy.force coq_s_contradiction, + [| trace ; mk_nat (get_hyp env_hyp e1.id); + mk_nat (get_hyp env_hyp e2.id) |]) + | DIVIDE_AND_APPROX (e1,e2,k,d) :: l -> + mkApp (Lazy.force coq_s_div_approx, + [| Z.mk k; Z.mk d; + reified_of_omega env e2.body e2.constant; + mk_nat (List.length e2.body); + loop env_hyp l; mk_nat (get_hyp env_hyp e1.id) |]) + | NOT_EXACT_DIVIDE (e1,k) :: l -> + let e2_constant = floor_div e1.constant k in + let d = e1.constant - e2_constant * k in + let e2_body = map_eq_linear (fun c -> c / k) e1.body in + mkApp (Lazy.force coq_s_not_exact_divide, + [|Z.mk k; Z.mk d; + reified_of_omega env e2_body e2_constant; + mk_nat (List.length e2_body); + mk_nat (get_hyp env_hyp e1.id)|]) + | EXACT_DIVIDE (e1,k) :: l -> + let e2_body = + map_eq_linear (fun c -> c / k) e1.body in + let e2_constant = floor_div e1.constant k in + mkApp (Lazy.force coq_s_exact_divide, + [|Z.mk k; + reified_of_omega env e2_body e2_constant; + mk_nat (List.length e2_body); + loop env_hyp l; mk_nat (get_hyp env_hyp e1.id)|]) + | (MERGE_EQ(e3,e1,e2)) :: l -> + let n1 = get_hyp env_hyp e1.id and n2 = get_hyp env_hyp e2 in + mkApp (Lazy.force coq_s_merge_eq, + [| mk_nat (List.length e1.body); + mk_nat n1; mk_nat n2; + loop (CCEqua e3:: env_hyp) l |]) + | SUM(e3,(k1,e1),(k2,e2)) :: l -> + let n1 = get_hyp env_hyp e1.id + and n2 = get_hyp env_hyp e2.id in + let trace = shuffle_path k1 e1.body k2 e2.body in + mkApp (Lazy.force coq_s_sum, + [| Z.mk k1; mk_nat n1; Z.mk k2; + mk_nat n2; trace; (loop (CCEqua e3 :: env_hyp) l) |]) + | CONSTANT_NOT_NUL(e,k) :: l -> + mkApp (Lazy.force coq_s_constant_not_nul, + [| mk_nat (get_hyp env_hyp e) |]) + | CONSTANT_NEG(e,k) :: l -> + mkApp (Lazy.force coq_s_constant_neg, + [| mk_nat (get_hyp env_hyp e) |]) + | STATE {st_new_eq=new_eq; st_def =def; + st_orig=orig; st_coef=m; + st_var=sigma } :: l -> + let n1 = get_hyp env_hyp orig.id + and n2 = get_hyp env_hyp def.id in + let v = unintern_omega env sigma in + let o_def = oformula_of_omega env def in + let o_orig = oformula_of_omega env orig in + let body = + Oplus (o_orig,Omult (Oplus (Oopp v,o_def), Oint m)) in + let trace,_ = normalize_linear_term env body in + mkApp (Lazy.force coq_s_state, + [| Z.mk m; trace; mk_nat n1; mk_nat n2; + loop (CCEqua new_eq.id :: env_hyp) l |]) + | HYP _ :: l -> loop env_hyp l + | CONSTANT_NUL e :: l -> + mkApp (Lazy.force coq_s_constant_nul, + [| mk_nat (get_hyp env_hyp e) |]) + | NEGATE_CONTRADICT(e1,e2,true) :: l -> + mkApp (Lazy.force coq_s_negate_contradict, + [| mk_nat (get_hyp env_hyp e1.id); + mk_nat (get_hyp env_hyp e2.id) |]) + | NEGATE_CONTRADICT(e1,e2,false) :: l -> + mkApp (Lazy.force coq_s_negate_contradict_inv, + [| mk_nat (List.length e2.body); + mk_nat (get_hyp env_hyp e1.id); + mk_nat (get_hyp env_hyp e2.id) |]) + | SPLIT_INEQ(e,(e1,l1),(e2,l2)) :: l -> + let i = get_hyp env_hyp e.id in + let r1 = loop (CCEqua e1 :: env_hyp) l1 in + let r2 = loop (CCEqua e2 :: env_hyp) l2 in + mkApp (Lazy.force coq_s_split_ineq, + [| mk_nat (List.length e.body); mk_nat i; r1 ; r2 |]) + | (FORGET_C _ | FORGET _ | FORGET_I _) :: l -> + loop env_hyp l + | (WEAKEN _ ) :: l -> failwith "not_treated" + | [] -> failwith "no contradiction" + in loop env_hyp + +let rec decompose_tree env ctxt = function + Tree(i,left,right) -> + let org = + try Hashtbl.find env.constructors i + with Not_found -> + failwith (Printf.sprintf "Cannot find constructor %d" i) in + let (index,path) = find_path org ctxt in + let left_hyp = CCHyp{o_hyp=org.o_hyp;o_path=org.o_path @ [O_left]} in + let right_hyp = CCHyp{o_hyp=org.o_hyp;o_path=org.o_path @ [O_right]} in + app coq_e_split + [| mk_nat index; + mk_direction_list path; + decompose_tree env (left_hyp::ctxt) left; + decompose_tree env (right_hyp::ctxt) right |] + | Leaf s -> + decompose_tree_hyps s.s_trace env ctxt s.s_equa_deps +and decompose_tree_hyps trace env ctxt = function + [] -> app coq_e_solve [| replay_history env ctxt trace |] + | (i::l) -> + let equation = + try Hashtbl.find env.equations i + with Not_found -> + failwith (Printf.sprintf "Cannot find equation %d" i) in + let (index,path) = find_path equation.e_origin ctxt in + let full_path = if equation.e_negated then path @ [O_mono] else path in + let cont = + decompose_tree_hyps trace env + (CCEqua equation.e_omega.id :: ctxt) l in + app coq_e_extract [|mk_nat index; + mk_direction_list full_path; + cont |] + +(* \section{La fonction principale} *) + (* Cette fonction construit la +trace pour la procédure de décision réflexive. A partir des résultats +de l'extraction des systèmes, elle lance la résolution par Omega, puis +l'extraction d'un ensemble minimal de solutions permettant la +résolution globale du système et enfin construit la trace qui permet +de faire rejouer cette solution par la tactique réflexive. *) + +let resolution env full_reified_goal systems_list = + let num = ref 0 in + let solve_system list_eq = + let index = !num in + let system = List.map (fun eq -> eq.e_omega) list_eq in + let trace = + simplify_strong + (new_omega_eq,new_omega_var,display_omega_var) + system in + (* calcule les hypotheses utilisées pour la solution *) + let vars = hyps_used_in_trace trace in + let splits = get_eclatement env vars in + if !debug then begin + Printf.printf "SYSTEME %d\n" index; + display_action display_omega_var trace; + print_string "\n Depend :"; + List.iter (fun i -> Printf.printf " %d" i) vars; + print_string "\n Split points :"; + List.iter display_depend splits; + Printf.printf "\n------------------------------------\n" + end; + incr num; + {s_index = index; s_trace = trace; s_equa_deps = vars}, splits in + if !debug then Printf.printf "\n====================================\n"; + let all_solutions = List.map solve_system systems_list in + let solution_tree = solve_with_constraints all_solutions [] in + if !debug then begin + display_solution_tree stdout solution_tree; + print_newline() + end; + (* calcule la liste de toutes les hypothèses utilisées dans l'arbre de solution *) + let useful_equa_id = equas_of_solution_tree solution_tree in + (* recupere explicitement ces equations *) + let equations = List.map (get_equation env) useful_equa_id in + let l_hyps' = list_uniquize (List.map (fun e -> e.e_origin.o_hyp) equations) in + let l_hyps = id_concl :: list_remove id_concl l_hyps' in + let useful_hyps = + List.map (fun id -> List.assoc id full_reified_goal) l_hyps in + let useful_vars = + let really_useful_vars = vars_of_equations equations in + let concl_vars = vars_of_prop (List.assoc id_concl full_reified_goal) in + really_useful_vars @@ concl_vars + in + (* variables a introduire *) + let to_introduce = add_stated_equations env solution_tree in + let stated_vars = List.map (fun (v,_,_,_) -> v) to_introduce in + let l_generalize_arg = List.map (fun (_,t,_,_) -> t) to_introduce in + let hyp_stated_vars = List.map (fun (_,_,_,id) -> CCEqua id) to_introduce in + (* L'environnement de base se construit en deux morceaux : + - les variables des équations utiles (et de la conclusion) + - les nouvelles variables declarées durant les preuves *) + let all_vars_env = useful_vars @ stated_vars in + let basic_env = + let rec loop i = function + var :: l -> + let t = get_reified_atom env var in + Hashtbl.add env.real_indices var i; t :: loop (succ i) l + | [] -> [] in + loop 0 all_vars_env in + let env_terms_reified = mk_list (Lazy.force Z.typ) basic_env in + (* On peut maintenant généraliser le but : env est a jour *) + let l_reified_stated = + List.map (fun (_,_,(l,r),_) -> + app coq_p_eq [| reified_of_formula env l; + reified_of_formula env r |]) + to_introduce in + let reified_concl = + match useful_hyps with + (Pnot p) :: _ -> reified_of_proposition env p + | _ -> reified_of_proposition env Pfalse in + let l_reified_terms = + (List.map + (fun p -> + reified_of_proposition env (really_useful_prop useful_equa_id p)) + (List.tl useful_hyps)) in + let env_props_reified = mk_plist env.props in + let reified_goal = + mk_list (Lazy.force coq_proposition) + (l_reified_stated @ l_reified_terms) in + let reified = + app coq_interp_sequent + [| reified_concl;env_props_reified;env_terms_reified;reified_goal|] in + let normalize_equation e = + let rec loop = function + [] -> app (if e.e_negated then coq_p_invert else coq_p_step) + [| e.e_trace |] + | ((O_left | O_mono) :: l) -> app coq_p_left [| loop l |] + | (O_right :: l) -> app coq_p_right [| loop l |] in + let correct_index = + let i = list_index0 e.e_origin.o_hyp l_hyps in + (* PL: it seems that additionnally introduced hyps are in the way during + normalization, hence this index shifting... *) + if i=0 then 0 else Pervasives.(+) i (List.length to_introduce) + in + app coq_pair_step [| mk_nat correct_index; loop e.e_origin.o_path |] in + let normalization_trace = + mk_list (Lazy.force coq_h_step) (List.map normalize_equation equations) in + + let initial_context = + List.map (fun id -> CCHyp{o_hyp=id;o_path=[]}) (List.tl l_hyps) in + let context = + CCHyp{o_hyp=id_concl;o_path=[]} :: hyp_stated_vars @ initial_context in + let decompose_tactic = decompose_tree env context solution_tree in + + Tactics.generalize + (l_generalize_arg @ List.map Term.mkVar (List.tl l_hyps)) >> + Tactics.change_in_concl None reified >> + Tactics.apply (app coq_do_omega [|decompose_tactic; normalization_trace|]) >> + show_goal >> + Tactics.normalise_vm_in_concl >> + (*i Alternatives to the previous line: + - Normalisation without VM: + Tactics.normalise_in_concl + - Skip the conversion check and rely directly on the QED: + Tacmach.convert_concl_no_check (Lazy.force coq_True) Term.VMcast >> + i*) + Tactics.apply (Lazy.force coq_I) + +let total_reflexive_omega_tactic gl = + Coqlib.check_required_library ["Coq";"romega";"ROmega"]; + rst_omega_eq (); + rst_omega_var (); + try + let env = new_environment () in + let full_reified_goal = reify_gl env gl in + let systems_list = destructurate_hyps full_reified_goal in + if !debug then display_systems systems_list; + resolution env full_reified_goal systems_list gl + with NO_CONTRADICTION -> Util.error "ROmega can't solve this system" + + +(*i let tester = Tacmach.hide_atomic_tactic "TestOmega" test_tactic i*) + + diff --git a/plugins/romega/romega_plugin.mllib b/plugins/romega/romega_plugin.mllib new file mode 100644 index 00000000..1625009d --- /dev/null +++ b/plugins/romega/romega_plugin.mllib @@ -0,0 +1,4 @@ +Const_omega +Refl_omega +G_romega +Romega_plugin_mod diff --git a/plugins/romega/vo.itarget b/plugins/romega/vo.itarget new file mode 100644 index 00000000..f7a3c41c --- /dev/null +++ b/plugins/romega/vo.itarget @@ -0,0 +1,2 @@ +ReflOmegaCore.vo +ROmega.vo |