summaryrefslogtreecommitdiff
path: root/plugins/romega
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/romega')
-rw-r--r--plugins/romega/README6
-rw-r--r--plugins/romega/ROmega.v14
-rw-r--r--plugins/romega/ReflOmegaCore.v3216
-rw-r--r--plugins/romega/const_omega.ml352
-rw-r--r--plugins/romega/const_omega.mli176
-rw-r--r--plugins/romega/g_romega.ml442
-rw-r--r--plugins/romega/refl_omega.ml1299
-rw-r--r--plugins/romega/romega_plugin.mllib4
-rw-r--r--plugins/romega/vo.itarget2
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