diff options
Diffstat (limited to 'contrib/romega')
| -rw-r--r-- | contrib/romega/ROmega.v | 1 | ||||
| -rw-r--r-- | contrib/romega/ReflOmegaCore.v | 643 | ||||
| -rw-r--r-- | contrib/romega/const_omega.ml | 246 | ||||
| -rw-r--r-- | contrib/romega/g_romega.ml4 | 4 | ||||
| -rw-r--r-- | contrib/romega/omega2.ml | 675 | ||||
| -rw-r--r-- | contrib/romega/refl_omega.ml | 316 |
6 files changed, 508 insertions, 1377 deletions
diff --git a/contrib/romega/ROmega.v b/contrib/romega/ROmega.v index b3895b2a..19933873 100644 --- a/contrib/romega/ROmega.v +++ b/contrib/romega/ROmega.v @@ -6,6 +6,5 @@ *************************************************************************) -Require Import Omega. Require Import ReflOmegaCore. diff --git a/contrib/romega/ReflOmegaCore.v b/contrib/romega/ReflOmegaCore.v index 3dfb5593..2aa3516f 100644 --- a/contrib/romega/ReflOmegaCore.v +++ b/contrib/romega/ReflOmegaCore.v @@ -1,3 +1,4 @@ +(* -*- coding: utf-8 -*- *) (************************************************************************* PROJET RNRT Calife - 2001 @@ -9,9 +10,11 @@ Require Import Arith. Require Import List. Require Import Bool. -Require Import ZArith. +Require Import ZArith_base. Require Import OmegaLemmas. +Open Scope Z_scope. + (* \subsection{Definition of basic types} *) (* \subsubsection{Environment of propositions (lists) *) @@ -45,6 +48,13 @@ Inductive term : Set := | Topp : term -> term | Tvar : nat -> term. +Delimit Scope romega_scope with term. +Infix "+" := Tplus : romega_scope. +Infix "*" := Tmult : romega_scope. +Infix "-" := Tminus : romega_scope. +Notation "- x" := (Topp x) : romega_scope. +Notation "[ x ]" := (Tvar x) (at level 1) : romega_scope. + (* \subsubsection{Definition of reified goals} *) (* Very restricted definition of handled predicates that should be extended to cover a wider set of operations. @@ -67,13 +77,13 @@ Inductive proposition : Set := | Tprop : nat -> proposition. (* Definition of goals as a list of hypothesis *) -Notation hyps := (list proposition) (only parsing). +Notation hyps := (list proposition). (* Definition of lists of subgoals (set of open goals) *) -Notation lhyps := (list (list proposition)) (only parsing). +Notation lhyps := (list hyps). (* a syngle goal packed in a subgoal list *) -Notation singleton := (fun a : list proposition => a :: nil) (only parsing). +Notation singleton := (fun a : hyps => a :: nil). (* an absurd goal *) Definition absurd := FalseTerm :: nil. @@ -120,7 +130,7 @@ Inductive step : Set := | C_PLUS_ASSOC_R : step | C_PLUS_ASSOC_L : step | C_PLUS_PERMUTE : step - | C_PLUS_SYM : step + | C_PLUS_COMM : step | C_RED0 : step | C_RED1 : step | C_RED2 : step @@ -130,7 +140,7 @@ Inductive step : Set := | C_RED6 : step | C_MULT_ASSOC_REDUCED : step | C_MINUS : step - | C_MULT_SYM : step. + | C_MULT_COMM : step. (* \subsubsection{Omega steps} *) (* The following inductive type describes steps as they can be found in @@ -176,7 +186,7 @@ Inductive p_step : Set := type [p_step] permettant de parcourir à la fois les branches gauches et droit, on pourrait n'avoir qu'une normalisation par hypothèse. Et comme toutes les hypothèses sont - utiles (sinon on ne les incluerait pas), on pourrait remplacer [h_step] + utiles (sinon on ne les inclurait pas), on pourrait remplacer [h_step] par une simple liste *) Inductive h_step : Set := @@ -360,29 +370,31 @@ Fixpoint eq_term (t1 t2 : term) {struct t2} : bool := | Tint st2 => eq_Z st1 st2 | _ => false end - | Tplus st11 st12 => + | (st11 + st12)%term => match t2 with - | Tplus st21 st22 => eq_term st11 st21 && eq_term st12 st22 + | (st21 + st22)%term => eq_term st11 st21 && eq_term st12 st22 | _ => false end - | Tmult st11 st12 => + | (st11 * st12)%term => match t2 with - | Tmult st21 st22 => eq_term st11 st21 && eq_term st12 st22 + | (st21 * st22)%term => eq_term st11 st21 && eq_term st12 st22 | _ => false end - | Tminus st11 st12 => + | (st11 - st12)%term => match t2 with - | Tminus st21 st22 => eq_term st11 st21 && eq_term st12 st22 + | (st21 - st22)%term => eq_term st11 st21 && eq_term st12 st22 + | _ => false + end + | (- st1)%term => + match t2 with + | (- st2)%term => eq_term st1 st2 + | _ => false + end + | [st1]%term => + match t2 with + | [st2]%term => eq_nat st1 st2 | _ => false end - | Topp st1 => match t2 with - | Topp st2 => eq_term st1 st2 - | _ => false - end - | Tvar st1 => match t2 with - | Tvar st2 => eq_nat st1 st2 - | _ => false - end end. Theorem eq_term_true : forall t1 t2 : term, eq_term t1 t2 = true -> t1 = t2. @@ -480,15 +492,15 @@ Ltac elim_eq_pos t1 t2 := avec son théorème *) Theorem relation_ind2 : - forall (P : Datatypes.comparison -> Prop) (b : Datatypes.comparison), - (b = Datatypes.Eq -> P Datatypes.Eq) -> - (b = Datatypes.Lt -> P Datatypes.Lt) -> - (b = Datatypes.Gt -> P Datatypes.Gt) -> P b. + forall (P : comparison -> Prop) (b : comparison), + (b = Eq -> P Eq) -> + (b = Lt -> P Lt) -> + (b = Gt -> P Gt) -> P b. simple induction b; auto. Qed. -Ltac elim_Zcompare t1 t2 := pattern (t1 ?= t2)%Z in |- *; apply relation_ind2. +Ltac elim_Zcompare t1 t2 := pattern (t1 ?= t2) in |- *; apply relation_ind2. (* \subsection{Interprétations} \subsubsection{Interprétation des termes dans Z} *) @@ -496,11 +508,11 @@ Ltac elim_Zcompare t1 t2 := pattern (t1 ?= t2)%Z in |- *; apply relation_ind2. Fixpoint interp_term (env : list Z) (t : term) {struct t} : Z := match t with | Tint x => x - | Tplus t1 t2 => (interp_term env t1 + interp_term env t2)%Z - | Tmult t1 t2 => (interp_term env t1 * interp_term env t2)%Z - | Tminus t1 t2 => (interp_term env t1 - interp_term env t2)%Z - | Topp t => (- interp_term env t)%Z - | Tvar n => nth n env 0%Z + | (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} *) @@ -508,13 +520,13 @@ Fixpoint interp_proposition (envp : PropList) (env : list Z) (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)%Z + | 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)%Z - | GtTerm t1 t2 => (interp_term env t1 > interp_term env t2)%Z - | LtTerm t1 t2 => (interp_term env t1 < interp_term env t2)%Z + | GeqTerm t1 t2 => interp_term env t1 >= interp_term env t2 + | GtTerm t1 t2 => interp_term env t1 > interp_term env t2 + | LtTerm t1 t2 => interp_term env t1 < interp_term env t2 | NeqTerm t1 t2 => Zne (interp_term env t1) (interp_term env t2) | Tor p1 p2 => interp_proposition envp env p1 \/ interp_proposition envp env p2 @@ -531,7 +543,7 @@ Fixpoint interp_proposition (envp : PropList) (env : list Z) à manipuler individuellement *) Fixpoint interp_hyps (envp : PropList) (env : list Z) - (l : list proposition) {struct l} : Prop := + (l : hyps) {struct l} : Prop := match l with | nil => True | p' :: l' => interp_proposition envp env p' /\ interp_hyps envp env l' @@ -542,26 +554,22 @@ Fixpoint interp_hyps (envp : PropList) (env : list Z) [Generalize] et qu'une conjonction est forcément lourde (répétition des types dans les conjonctions intermédiaires) *) -Fixpoint interp_goal_concl (envp : PropList) (env : list Z) - (c : proposition) (l : list proposition) {struct l} : Prop := +Fixpoint interp_goal_concl (c : proposition) (envp : PropList) + (env : list Z) (l : hyps) {struct l} : Prop := match l with | nil => interp_proposition envp env c | p' :: l' => - interp_proposition envp env p' -> interp_goal_concl envp env c l' + interp_proposition envp env p' -> interp_goal_concl c envp env l' end. -Notation interp_goal := - (fun (envp : PropList) (env : list Z) (l : list proposition) => - interp_goal_concl envp env FalseTerm l) (only parsing). +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 : PropList) (env : list Z) (l : list proposition), - (interp_hyps envp env l -> False) -> - (fun (envp : PropList) (env : list Z) (l : list proposition) => - interp_goal_concl envp env FalseTerm l) envp env l. + forall (envp : PropList) (env : list Z) (l : hyps), + (interp_hyps envp env l -> False) -> interp_goal envp env l. simple induction l; [ simpl in |- *; auto @@ -569,10 +577,8 @@ simple induction l; Qed. Theorem hyps_to_goal : - forall (envp : PropList) (env : list Z) (l : list proposition), - (fun (envp : PropList) (env : list Z) (l : list proposition) => - interp_goal_concl envp env FalseTerm l) envp env l -> - interp_hyps envp env l -> False. + forall (envp : PropList) (env : list Z) (l : hyps), + interp_goal envp env l -> interp_hyps envp env l -> False. simple induction l; simpl in |- *; [ auto | intros; apply H; elim H1; auto ]. Qed. @@ -603,22 +609,16 @@ Definition valid2 (f : proposition -> proposition -> proposition) := liste de propositions et rend une nouvelle liste de proposition. On reste contravariant *) -Definition valid_hyps (f : list proposition -> list proposition) := - forall (ep : PropList) (e : list Z) (lp : list proposition), +Definition valid_hyps (f : hyps -> hyps) := + forall (ep : PropList) (e : list Z) (lp : hyps), interp_hyps ep e lp -> interp_hyps ep e (f lp). (* Enfin ce théorème élimine la contravariance et nous ramène à une opération sur les buts *) Theorem valid_goal : - forall (ep : PropList) (env : list Z) (l : list proposition) - (a : list proposition -> list proposition), - valid_hyps a -> - (fun (envp : PropList) (env : list Z) (l : list proposition) => - interp_goal_concl envp env FalseTerm l) ep env ( - a l) -> - (fun (envp : PropList) (env : list Z) (l : list proposition) => - interp_goal_concl envp env FalseTerm l) ep env l. + forall (ep : PropList) (env : list Z) (l : hyps) (a : hyps -> hyps), + valid_hyps a -> interp_goal ep env (a l) -> interp_goal ep env l. intros; simpl in |- *; apply goal_to_hyps; intro H1; apply (hyps_to_goal ep env (a l) H0); apply H; assumption. @@ -627,25 +627,22 @@ Qed. (* \subsubsection{Généralisation a des listes de buts (disjonctions)} *) -Fixpoint interp_list_hyps (envp : PropList) (env : list Z) - (l : list (list proposition)) {struct l} : Prop := +Fixpoint interp_list_hyps (envp : PropList) (env : list Z) + (l : lhyps) {struct l} : Prop := match l with | nil => False | h :: l' => interp_hyps envp env h \/ interp_list_hyps envp env l' end. -Fixpoint interp_list_goal (envp : PropList) (env : list Z) - (l : list (list proposition)) {struct l} : Prop := +Fixpoint interp_list_goal (envp : PropList) (env : list Z) + (l : lhyps) {struct l} : Prop := match l with | nil => True - | h :: l' => - (fun (envp : PropList) (env : list Z) (l : list proposition) => - interp_goal_concl envp env FalseTerm l) envp env h /\ - interp_list_goal envp env l' + | h :: l' => interp_goal envp env h /\ interp_list_goal envp env l' end. Theorem list_goal_to_hyps : - forall (envp : PropList) (env : list Z) (l : list (list proposition)), + forall (envp : PropList) (env : list Z) (l : lhyps), (interp_list_hyps envp env l -> False) -> interp_list_goal envp env l. simple induction l; simpl in |- *; @@ -656,7 +653,7 @@ simple induction l; simpl in |- *; Qed. Theorem list_hyps_to_goal : - forall (envp : PropList) (env : list Z) (l : list (list proposition)), + forall (envp : PropList) (env : list Z) (l : lhyps), interp_list_goal envp env l -> interp_list_hyps envp env l -> False. simple induction l; simpl in |- *; @@ -665,21 +662,16 @@ simple induction l; simpl in |- *; [ apply hyps_to_goal with (1 := H1); assumption | auto ] ]. Qed. -Definition valid_list_hyps - (f : list proposition -> list (list proposition)) := - forall (ep : PropList) (e : list Z) (lp : list proposition), +Definition valid_list_hyps (f : hyps -> lhyps) := + forall (ep : PropList) (e : list Z) (lp : hyps), interp_hyps ep e lp -> interp_list_hyps ep e (f lp). -Definition valid_list_goal - (f : list proposition -> list (list proposition)) := - forall (ep : PropList) (e : list Z) (lp : list proposition), - interp_list_goal ep e (f lp) -> - (fun (envp : PropList) (env : list Z) (l : list proposition) => - interp_goal_concl envp env FalseTerm l) ep e lp. +Definition valid_list_goal (f : hyps -> lhyps) := + forall (ep : PropList) (e : list Z) (lp : hyps), + interp_list_goal ep e (f lp) -> interp_goal ep e lp. Theorem goal_valid : - forall f : list proposition -> list (list proposition), - valid_list_hyps f -> valid_list_goal f. + forall f : hyps -> lhyps, valid_list_hyps f -> valid_list_goal f. unfold valid_list_goal in |- *; intros f H ep e lp H1; apply goal_to_hyps; intro H2; apply list_hyps_to_goal with (1 := H1); @@ -687,7 +679,7 @@ unfold valid_list_goal in |- *; intros f H ep e lp H1; apply goal_to_hyps; Qed. Theorem append_valid : - forall (ep : PropList) (e : list Z) (l1 l2 : list (list proposition)), + forall (ep : PropList) (e : list Z) (l1 l2 : lhyps), interp_list_hyps ep e l1 \/ interp_list_hyps ep e l2 -> interp_list_hyps ep e (l1 ++ l2). @@ -703,10 +695,10 @@ Qed. (* \subsubsection{Opérateurs valides sur les hypothèses} *) (* Extraire une hypothèse de la liste *) -Definition nth_hyps (n : nat) (l : list proposition) := nth n l TrueTerm. +Definition nth_hyps (n : nat) (l : hyps) := nth n l TrueTerm. Theorem nth_valid : - forall (ep : PropList) (e : list Z) (i : nat) (l : list proposition), + forall (ep : PropList) (e : list Z) (i : nat) (l : hyps), interp_hyps ep e l -> interp_proposition ep e (nth_hyps i l). unfold nth_hyps in |- *; simple induction i; @@ -719,7 +711,7 @@ 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 : list proposition) := + (f : proposition -> proposition -> proposition) (l : hyps) := f (nth_hyps i l) (nth_hyps j l) :: l. Theorem apply_oper_2_valid : @@ -732,8 +724,8 @@ Qed. (* Modifier une hypothèse par application d'une opération valide *) -Fixpoint apply_oper_1 (i : nat) (f : proposition -> proposition) - (l : list proposition) {struct i} : list proposition := +Fixpoint apply_oper_1 (i : nat) (f : proposition -> proposition) + (l : hyps) {struct i} : hyps := match l with | nil => nil (A:=proposition) | p :: l' => @@ -767,23 +759,23 @@ Qed. Definition apply_left (f : term -> term) (t : term) := match t with - | Tplus x y => Tplus (f x) y - | Tmult x y => Tmult (f x) y - | Topp x => Topp (f x) + | (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 - | Tplus x y => Tplus x (f y) - | Tmult x y => Tmult x (f y) + | (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 - | Tplus x y => Tplus (f x) (g y) - | Tmult x y => Tmult (f x) (g y) + | (x + y)%term => (f x + g y)%term + | (x * y)%term => (f x * g y)%term | x => x end. @@ -849,31 +841,25 @@ Qed. (* \subsubsection{La tactique pour prouver la stabilité} *) Ltac loop t := - match constr:t with - | (?X1 = ?X2) => - (* Global *) - loop X1 || loop X2 + match t with + (* Global *) + | (?X1 = ?X2) => loop X1 || loop X2 | (_ -> ?X1) => loop X1 - | (interp_hyps _ _ ?X1) => - (* Interpretations *) - loop X1 + | (interp_hyps _ _ ?X1) => loop X1 | (interp_list_hyps _ _ ?X1) => loop X1 | (interp_proposition _ _ ?X1) => loop X1 | (interp_term _ ?X1) => loop X1 - | (EqTerm ?X1 ?X2) => - - (* Propositions *) - loop X1 || loop X2 + (* Propositions *) + | (EqTerm ?X1 ?X2) => loop X1 || loop X2 | (LeqTerm ?X1 ?X2) => loop X1 || loop X2 - | (Tplus ?X1 ?X2) => - (* Termes *) - loop X1 || loop X2 - | (Tminus ?X1 ?X2) => loop X1 || loop X2 - | (Tmult ?X1 ?X2) => loop X1 || loop X2 - | (Topp ?X1) => loop X1 - | (Tint ?X1) => - loop X1 + (* 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 => _ @@ -889,8 +875,6 @@ Ltac loop t := | Timp x x0 => _ | Tprop x => _ end => - - (* Eliminations *) case X1; [ intro; intro | intro; intro @@ -907,19 +891,19 @@ Ltac loop t := | intro ]; auto; Simplify | match ?X1 with | Tint x => _ - | Tplus x x0 => _ - | Tmult x x0 => _ - | Tminus x x0 => _ - | Topp x => _ - | Tvar x => _ + | (x + x0)%term => _ + | (x * x0)%term => _ + | (x - x0)%term => _ + | (- x)%term => _ + | [x]%term => _ end => case X1; [ intro | intro; intro | intro; intro | intro; intro | intro | intro ]; auto; Simplify - | match (?X1 ?= ?X2)%Z with - | Datatypes.Eq => _ - | Datatypes.Lt => _ - | Datatypes.Gt => _ + | match ?X1 ?= ?X2 with + | Eq => _ + | Lt => _ + | Gt => _ end => elim_Zcompare X1 X2; intro; auto; Simplify | match ?X1 with @@ -955,7 +939,7 @@ Ltac prove_stable x th := (* \subsubsection{Les règles elle mêmes} *) Definition Tplus_assoc_l (t : term) := match t with - | Tplus n (Tplus m p) => Tplus (Tplus n m) p + | (n + (m + p))%term => (n + m + p)%term | _ => t end. @@ -966,7 +950,7 @@ Qed. Definition Tplus_assoc_r (t : term) := match t with - | Tplus (Tplus n m) p => Tplus n (Tplus m p) + | (n + m + p)%term => (n + (m + p))%term | _ => t end. @@ -977,7 +961,7 @@ Qed. Definition Tmult_assoc_r (t : term) := match t with - | Tmult (Tmult n m) p => Tmult n (Tmult m p) + | (n * m * p)%term => (n * (m * p))%term | _ => t end. @@ -988,7 +972,7 @@ Qed. Definition Tplus_permute (t : term) := match t with - | Tplus n (Tplus m p) => Tplus m (Tplus n p) + | (n + (m + p))%term => (m + (n + p))%term | _ => t end. @@ -999,7 +983,7 @@ Qed. Definition Tplus_sym (t : term) := match t with - | Tplus x y => Tplus y x + | (x + y)%term => (y + x)%term | _ => t end. @@ -1010,7 +994,7 @@ Qed. Definition Tmult_sym (t : term) := match t with - | Tmult x y => Tmult y x + | (x * y)%term => (y * x)%term | _ => t end. @@ -1021,12 +1005,10 @@ Qed. Definition T_OMEGA10 (t : term) := match t with - | Tplus (Tmult (Tplus (Tmult v (Tint c1)) l1) (Tint k1)) (Tmult (Tplus - (Tmult v' (Tint c2)) l2) (Tint k2)) => + | ((v * Tint c1 + l1) * Tint k1 + (v' * Tint c2 + l2) * Tint k2)%term => match eq_term v v' with | true => - Tplus (Tmult v (Tint (c1 * k1 + c2 * k2))) - (Tplus (Tmult l1 (Tint k1)) (Tmult l2 (Tint k2))) + (v * Tint (c1 * k1 + c2 * k2) + (l1 * Tint k1 + l2 * Tint k2))%term | false => t end | _ => t @@ -1039,8 +1021,8 @@ Qed. Definition T_OMEGA11 (t : term) := match t with - | Tplus (Tmult (Tplus (Tmult v1 (Tint c1)) l1) (Tint k1)) l2 => - Tplus (Tmult v1 (Tint (c1 * k1))) (Tplus (Tmult l1 (Tint k1)) l2) + | ((v1 * Tint c1 + l1) * Tint k1 + l2)%term => + (v1 * Tint (c1 * k1) + (l1 * Tint k1 + l2))%term | _ => t end. @@ -1051,8 +1033,8 @@ Qed. Definition T_OMEGA12 (t : term) := match t with - | Tplus l1 (Tmult (Tplus (Tmult v2 (Tint c2)) l2) (Tint k2)) => - Tplus (Tmult v2 (Tint (c2 * k2))) (Tplus l1 (Tmult l2 (Tint k2))) + | (l1 + (v2 * Tint c2 + l2) * Tint k2)%term => + (v2 * Tint (c2 * k2) + (l1 + l2 * Tint k2))%term | _ => t end. @@ -1063,22 +1045,22 @@ Qed. Definition T_OMEGA13 (t : term) := match t with - | Tplus (Tplus (Tmult v (Tint (Zpos x))) l1) (Tplus (Tmult v' (Tint (Zneg - x'))) l2) => + | (v * Tint (Zpos x) + l1 + (v' * Tint (Zneg x') + l2))%term => match eq_term v v' with - | true => match eq_pos x x' with - | true => Tplus l1 l2 - | false => t - end + | true => + match eq_pos x x' with + | true => (l1 + l2)%term + | false => t + end | false => t end - | Tplus (Tplus (Tmult v (Tint (Zneg x))) l1) (Tplus (Tmult v' (Tint (Zpos - x'))) l2) => + | (v * Tint (Zneg x) + l1 + (v' * Tint (Zpos x') + l2))%term => match eq_term v v' with - | true => match eq_pos x x' with - | true => Tplus l1 l2 - | false => t - end + | true => + match eq_pos x x' with + | true => (l1 + l2)%term + | false => t + end | false => t end | _ => t @@ -1092,12 +1074,9 @@ Qed. Definition T_OMEGA15 (t : term) := match t with - | Tplus (Tplus (Tmult v (Tint c1)) l1) (Tmult (Tplus (Tmult v' (Tint c2)) - l2) (Tint k2)) => + | (v * Tint c1 + l1 + (v' * Tint c2 + l2) * Tint k2)%term => match eq_term v v' with - | true => - Tplus (Tmult v (Tint (c1 + c2 * k2))) - (Tplus l1 (Tmult l2 (Tint k2))) + | true => (v * Tint (c1 + c2 * k2) + (l1 + l2 * Tint k2))%term | false => t end | _ => t @@ -1110,8 +1089,7 @@ Qed. Definition T_OMEGA16 (t : term) := match t with - | Tmult (Tplus (Tmult v (Tint c)) l) (Tint k) => - Tplus (Tmult v (Tint (c * k))) (Tmult l (Tint k)) + | ((v * Tint c + l) * Tint k)%term => (v * Tint (c * k) + l * Tint k)%term | _ => t end. @@ -1123,7 +1101,7 @@ Qed. Definition Tred_factor5 (t : term) := match t with - | Tplus (Tmult x (Tint Z0)) y => y + | (x * Tint Z0 + y)%term => y | _ => t end. @@ -1135,7 +1113,7 @@ Qed. Definition Topp_plus (t : term) := match t with - | Topp (Tplus x y) => Tplus (Topp x) (Topp y) + | (- (x + y))%term => (- x + - y)%term | _ => t end. @@ -1147,7 +1125,7 @@ Qed. Definition Topp_opp (t : term) := match t with - | Topp (Topp x) => x + | (- - x)%term => x | _ => t end. @@ -1158,7 +1136,7 @@ Qed. Definition Topp_mult_r (t : term) := match t with - | Topp (Tmult x (Tint k)) => Tmult x (Tint (- k)) + | (- (x * Tint k))%term => (x * Tint (- k))%term | _ => t end. @@ -1169,7 +1147,7 @@ Qed. Definition Topp_one (t : term) := match t with - | Topp x => Tmult x (Tint (-1)) + | (- x)%term => (x * Tint (-1))%term | _ => t end. @@ -1180,7 +1158,7 @@ Qed. Definition Tmult_plus_distr (t : term) := match t with - | Tmult (Tplus n m) p => Tplus (Tmult n p) (Tmult m p) + | ((n + m) * p)%term => (n * p + m * p)%term | _ => t end. @@ -1191,7 +1169,7 @@ Qed. Definition Tmult_opp_left (t : term) := match t with - | Tmult (Topp x) (Tint y) => Tmult x (Tint (- y)) + | (- x * Tint y)%term => (x * Tint (- y))%term | _ => t end. @@ -1202,7 +1180,7 @@ Qed. Definition Tmult_assoc_reduced (t : term) := match t with - | Tmult (Tmult n (Tint m)) (Tint p) => Tmult n (Tint (m * p)) + | (n * Tint m * Tint p)%term => (n * Tint (m * p))%term | _ => t end. @@ -1211,7 +1189,7 @@ Theorem Tmult_assoc_reduced_stable : term_stable Tmult_assoc_reduced. prove_stable Tmult_assoc_reduced Zmult_assoc_reverse. Qed. -Definition Tred_factor0 (t : term) := Tmult t (Tint 1). +Definition Tred_factor0 (t : term) := (t * Tint 1)%term. Theorem Tred_factor0_stable : term_stable Tred_factor0. @@ -1220,9 +1198,9 @@ Qed. Definition Tred_factor1 (t : term) := match t with - | Tplus x y => + | (x + y)%term => match eq_term x y with - | true => Tmult x (Tint 2) + | true => (x * Tint 2)%term | false => t end | _ => t @@ -1235,9 +1213,9 @@ Qed. Definition Tred_factor2 (t : term) := match t with - | Tplus x (Tmult y (Tint k)) => + | (x + y * Tint k)%term => match eq_term x y with - | true => Tmult x (Tint (1 + k)) + | true => (x * Tint (1 + k))%term | false => t end | _ => t @@ -1254,9 +1232,9 @@ Qed. Definition Tred_factor3 (t : term) := match t with - | Tplus (Tmult x (Tint k)) y => + | (x * Tint k + y)%term => match eq_term x y with - | true => Tmult x (Tint (1 + k)) + | true => (x * Tint (1 + k))%term | false => t end | _ => t @@ -1270,9 +1248,9 @@ Qed. Definition Tred_factor4 (t : term) := match t with - | Tplus (Tmult x (Tint k1)) (Tmult y (Tint k2)) => + | (x * Tint k1 + y * Tint k2)%term => match eq_term x y with - | true => Tmult x (Tint (k1 + k2)) + | true => (x * Tint (k1 + k2))%term | false => t end | _ => t @@ -1283,7 +1261,7 @@ Theorem Tred_factor4_stable : term_stable Tred_factor4. prove_stable Tred_factor4 Zred_factor4. Qed. -Definition Tred_factor6 (t : term) := Tplus t (Tint 0). +Definition Tred_factor6 (t : term) := (t + Tint 0)%term. Theorem Tred_factor6_stable : term_stable Tred_factor6. @@ -1294,7 +1272,7 @@ Transparent Zplus. Definition Tminus_def (t : term) := match t with - | Tminus x y => Tplus x (Topp y) + | (x - y)%term => (x + - y)%term | _ => t end. @@ -1313,37 +1291,37 @@ Qed. Fixpoint reduce (t : term) : term := match t with - | Tplus x y => + | (x + y)%term => match reduce x with | Tint x' => match reduce y with | Tint y' => Tint (x' + y') - | y' => Tplus (Tint x') y' + | y' => (Tint x' + y')%term end - | x' => Tplus x' (reduce y) + | x' => (x' + reduce y)%term end - | Tmult x y => + | (x * y)%term => match reduce x with | Tint x' => match reduce y with | Tint y' => Tint (x' * y') - | y' => Tmult (Tint x') y' + | y' => (Tint x' * y')%term end - | x' => Tmult x' (reduce y) + | x' => (x' * reduce y)%term end - | Tminus x y => + | (x - y)%term => match reduce x with | Tint x' => match reduce y with | Tint y' => Tint (x' - y') - | y' => Tminus (Tint x') y' + | y' => (Tint x' - y')%term end - | x' => Tminus x' (reduce y) + | x' => (x' - reduce y)%term end - | Topp x => + | (- x)%term => match reduce x with | Tint x' => Tint (- x') - | x' => Topp x' + | x' => (- x')%term end | _ => t end. @@ -1412,7 +1390,7 @@ Definition fusion_right (trace : list t_fusion) (t : term) : term := end end. -(* \paragraph{Fusion avec anihilation} *) +(* \paragraph{Fusion avec annihilation} *) (* Normalement le résultat est une constante *) Fixpoint fusion_cancel (trace : nat) (t : term) {struct trace} : term := @@ -1428,7 +1406,7 @@ unfold term_stable, fusion_cancel in |- *; intros trace e; elim trace; | intros n H t; elim H; exact (T_OMEGA13_stable e t) ]. Qed. -(* \subsubsection{Opérations afines sur une équation} *) +(* \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 := @@ -1497,7 +1475,7 @@ Fixpoint rewrite (s : step) : term -> term := | C_PLUS_ASSOC_R => Tplus_assoc_r | C_PLUS_ASSOC_L => Tplus_assoc_l | C_PLUS_PERMUTE => Tplus_permute - | C_PLUS_SYM => Tplus_sym + | C_PLUS_COMM => Tplus_sym | C_RED0 => Tred_factor0 | C_RED1 => Tred_factor1 | C_RED2 => Tred_factor2 @@ -1507,7 +1485,7 @@ Fixpoint rewrite (s : step) : term -> term := | C_RED6 => Tred_factor6 | C_MULT_ASSOC_REDUCED => Tmult_assoc_reduced | C_MINUS => Tminus_def - | C_MULT_SYM => Tmult_sym + | C_MULT_COMM => Tmult_sym end. Theorem rewrite_stable : forall s : step, term_stable (rewrite s). @@ -1547,7 +1525,7 @@ Qed. \subsubsection{Tactiques générant une contradiction} \paragraph{[O_CONSTANT_NOT_NUL]} *) -Definition constant_not_nul (i : nat) (h : list proposition) := +Definition constant_not_nul (i : nat) (h : hyps) := match nth_hyps i h with | EqTerm (Tint Z0) (Tint n) => match eq_Z n 0 with @@ -1562,13 +1540,13 @@ Theorem constant_not_nul_valid : unfold valid_hyps, constant_not_nul in |- *; intros; generalize (nth_valid ep e i lp); Simplify; simpl in |- *; - elim_eq_Z ipattern:z0 0%Z; auto; simpl in |- *; intros H1 H2; + elim_eq_Z ipattern:z0 0; auto; simpl in |- *; intros H1 H2; elim H1; symmetry in |- *; auto. Qed. (* \paragraph{[O_CONSTANT_NEG]} *) -Definition constant_neg (i : nat) (h : list proposition) := +Definition constant_neg (i : nat) (h : hyps) := match nth_hyps i h with | LeqTerm (Tint Z0) (Tint (Zneg n)) => absurd | _ => h @@ -1584,18 +1562,17 @@ Qed. (* \paragraph{[NOT_EXACT_DIVIDE]} *) Definition not_exact_divide (k1 k2 : Z) (body : term) - (t i : nat) (l : list proposition) := + (t i : nat) (l : hyps) := match nth_hyps i l with | EqTerm (Tint Z0) b => match - eq_term (scalar_norm_add t (Tplus (Tmult body (Tint k1)) (Tint k2))) - b + eq_term (scalar_norm_add t (body * Tint k1 + Tint k2)%term) b with | true => - match (k2 ?= 0)%Z with - | Datatypes.Gt => - match (k1 ?= k2)%Z with - | Datatypes.Gt => absurd + match k2 ?= 0 with + | Gt => + match k1 ?= k2 with + | Gt => absurd | _ => l end | _ => l @@ -1611,27 +1588,26 @@ Theorem not_exact_divide_valid : unfold valid_hyps, not_exact_divide in |- *; intros; generalize (nth_valid ep e i lp); Simplify; - elim_eq_term (scalar_norm_add t (Tplus (Tmult body (Tint k1)) (Tint k2))) t1; + elim_eq_term (scalar_norm_add t (body * Tint k1 + Tint k2)%term) t1; auto; Simplify; intro H2; elim H2; simpl in |- *; elim (scalar_norm_add_stable t e); simpl in |- *; - intro H4; absurd ((interp_term e body * k1 + k2)%Z = 0%Z); + intro H4; absurd (interp_term e body * k1 + k2 = 0); [ apply OMEGA4; assumption | symmetry in |- *; auto ]. Qed. (* \paragraph{[O_CONTRADICTION]} *) -Definition contradiction (t i j : nat) (l : list proposition) := +Definition contradiction (t i j : nat) (l : hyps) := match nth_hyps i l with | LeqTerm (Tint Z0) b1 => match nth_hyps j l with | LeqTerm (Tint Z0) b2 => - match fusion_cancel t (Tplus b1 b2) with - | Tint k => - match (0 ?= k)%Z with - | Datatypes.Gt => absurd - | _ => l - end + match fusion_cancel t (b1 + b2)%term with + | Tint k => match 0 ?= k with + | Gt => absurd + | _ => l + end | _ => l end | _ => l @@ -1648,9 +1624,9 @@ unfold valid_hyps, contradiction in |- *; intros t i j ep e l H; auto; intros z; case z; auto; case (nth_hyps j l); auto; intros t3 t4; case t3; auto; intros z'; case z'; auto; simpl in |- *; intros H1 H2; - generalize (refl_equal (interp_term e (fusion_cancel t (Tplus t2 t4)))); - pattern (fusion_cancel t (Tplus t2 t4)) at 2 3 in |- *; - case (fusion_cancel t (Tplus t2 t4)); simpl in |- *; + generalize (refl_equal (interp_term e (fusion_cancel t (t2 + t4)%term))); + pattern (fusion_cancel t (t2 + t4)%term) at 2 3 in |- *; + case (fusion_cancel t (t2 + t4)%term); simpl in |- *; auto; intro k; elim (fusion_cancel_stable t); simpl in |- *; intro E; generalize (OMEGA2 _ _ H2 H1); rewrite E; case k; auto; unfold Zle in |- *; simpl in |- *; intros p H3; @@ -1660,7 +1636,7 @@ Qed. (* \paragraph{[O_NEGATE_CONTRADICT]} *) -Definition negate_contradict (i1 i2 : nat) (h : list proposition) := +Definition negate_contradict (i1 i2 : nat) (h : hyps) := match nth_hyps i1 h with | EqTerm (Tint Z0) b1 => match nth_hyps i2 h with @@ -1683,12 +1659,12 @@ Definition negate_contradict (i1 i2 : nat) (h : list proposition) := | _ => h end. -Definition negate_contradict_inv (t i1 i2 : nat) (h : list proposition) := +Definition negate_contradict_inv (t i1 i2 : nat) (h : hyps) := match nth_hyps i1 h with | EqTerm (Tint Z0) b1 => match nth_hyps i2 h with | NeqTerm (Tint Z0) b2 => - match eq_term b1 (scalar_norm t (Tmult b2 (Tint (-1)))) with + match eq_term b1 (scalar_norm t (b2 * Tint (-1))%term) with | true => absurd | false => h end @@ -1697,7 +1673,7 @@ Definition negate_contradict_inv (t i1 i2 : nat) (h : list proposition) := | NeqTerm (Tint Z0) b1 => match nth_hyps i2 h with | EqTerm (Tint Z0) b2 => - match eq_term b1 (scalar_norm t (Tmult b2 (Tint (-1)))) with + match eq_term b1 (scalar_norm t (b2 * Tint (-1))%term) with | true => absurd | false => h end @@ -1732,11 +1708,11 @@ unfold valid_hyps, negate_contradict_inv in |- *; intros t i j ep e l H; auto; intros z; case z; auto; case (nth_hyps j l); auto; intros t3 t4; case t3; auto; intros z'; case z'; auto; simpl in |- *; intros H1 H2; - (pattern (eq_term t2 (scalar_norm t (Tmult t4 (Tint (-1))))) in |- *; + (pattern (eq_term t2 (scalar_norm t (t4 * Tint (-1))%term)) in |- *; apply bool_ind2; intro Aux; - [ generalize (eq_term_true t2 (scalar_norm t (Tmult t4 (Tint (-1)))) Aux); + [ generalize (eq_term_true t2 (scalar_norm t (t4 * Tint (-1))%term) Aux); clear Aux - | generalize (eq_term_false t2 (scalar_norm t (Tmult t4 (Tint (-1)))) Aux); + | generalize (eq_term_false t2 (scalar_norm t (t4 * Tint (-1))%term) Aux); clear Aux ]); [ intro H3; elim H1; generalize H2; rewrite H3; rewrite <- (scalar_norm_stable t e); simpl in |- *; @@ -1762,32 +1738,28 @@ Definition sum (k1 k2 : Z) (trace : list t_fusion) | EqTerm (Tint Z0) b1 => match prop2 with | EqTerm (Tint Z0) b2 => - EqTerm (Tint 0) - (fusion trace (Tplus (Tmult b1 (Tint k1)) (Tmult b2 (Tint k2)))) + EqTerm (Tint 0) (fusion trace (b1 * Tint k1 + b2 * Tint k2)%term) | LeqTerm (Tint Z0) b2 => - match (k2 ?= 0)%Z with - | Datatypes.Gt => + match k2 ?= 0 with + | Gt => LeqTerm (Tint 0) - (fusion trace - (Tplus (Tmult b1 (Tint k1)) (Tmult b2 (Tint k2)))) + (fusion trace (b1 * Tint k1 + b2 * Tint k2)%term) | _ => TrueTerm end | _ => TrueTerm end | LeqTerm (Tint Z0) b1 => - match (k1 ?= 0)%Z with - | Datatypes.Gt => + match k1 ?= 0 with + | Gt => match prop2 with | EqTerm (Tint Z0) b2 => LeqTerm (Tint 0) - (fusion trace - (Tplus (Tmult b1 (Tint k1)) (Tmult b2 (Tint k2)))) + (fusion trace (b1 * Tint k1 + b2 * Tint k2)%term) | LeqTerm (Tint Z0) b2 => - match (k2 ?= 0)%Z with - | Datatypes.Gt => + match k2 ?= 0 with + | Gt => LeqTerm (Tint 0) - (fusion trace - (Tplus (Tmult b1 (Tint k1)) (Tmult b2 (Tint k2)))) + (fusion trace (b1 * Tint k1 + b2 * Tint k2)%term) | _ => TrueTerm end | _ => TrueTerm @@ -1801,23 +1773,20 @@ Definition sum (k1 k2 : Z) (trace : list t_fusion) | true => TrueTerm | false => NeqTerm (Tint 0) - (fusion trace - (Tplus (Tmult b1 (Tint k1)) (Tmult b2 (Tint k2)))) + (fusion trace (b1 * Tint k1 + b2 * Tint k2)%term) end | _ => TrueTerm end | _ => TrueTerm end. -Theorem sum1 : - forall a b c d : Z, 0%Z = a -> 0%Z = b -> 0%Z = (a * c + b * d)%Z. +Theorem sum1 : forall a b c d : Z, 0 = a -> 0 = b -> 0 = a * c + b * d. intros; elim H; elim H0; simpl in |- *; auto. Qed. Theorem sum2 : - forall a b c d : Z, - (0 <= d)%Z -> 0%Z = a -> (0 <= b)%Z -> (0 <= a * c + b * d)%Z. + forall a b c d : Z, 0 <= d -> 0 = a -> 0 <= b -> 0 <= a * c + b * d. intros; elim H0; simpl in |- *; generalize H H1; case b; case d; unfold Zle in |- *; simpl in |- *; auto. @@ -1825,21 +1794,19 @@ Qed. Theorem sum3 : forall a b c d : Z, - (0 <= c)%Z -> - (0 <= d)%Z -> (0 <= a)%Z -> (0 <= b)%Z -> (0 <= a * c + b * d)%Z. + 0 <= c -> 0 <= d -> 0 <= a -> 0 <= b -> 0 <= a * c + b * d. intros a b c d; case a; case b; case c; case d; unfold Zle in |- *; simpl in |- *; auto. Qed. -Theorem sum4 : forall k : Z, (k ?= 0)%Z = Datatypes.Gt -> (0 <= k)%Z. +Theorem sum4 : forall k : Z, (k ?= 0) = Gt -> 0 <= k. intro; case k; unfold Zle in |- *; simpl in |- *; auto; intros; discriminate. Qed. Theorem sum5 : - forall a b c d : Z, - c <> 0%Z -> 0%Z <> a -> 0%Z = b -> 0%Z <> (a * c + b * d)%Z. + forall a b c d : Z, c <> 0 -> 0 <> a -> 0 = b -> 0 <> a * c + b * d. intros a b c d H1 H2 H3; elim H3; simpl in |- *; rewrite Zplus_comm; simpl in |- *; generalize H1 H2; case a; case c; simpl in |- *; @@ -1857,9 +1824,8 @@ unfold valid2 in |- *; intros k1 k2 t ep e p1 p2; unfold sum in |- *; | apply sum2; try assumption; apply sum4; assumption | rewrite Zplus_comm; apply sum2; try assumption; apply sum4; assumption | apply sum3; try assumption; apply sum4; assumption - | elim_eq_Z k1 0%Z; simpl in |- *; auto; elim (fusion_stable t); - simpl in |- *; intros; unfold Zne in |- *; apply sum5; - assumption ]. + | elim_eq_Z k1 0; simpl in |- *; auto; elim (fusion_stable t); simpl in |- *; + intros; unfold Zne in |- *; apply sum5; assumption ]. Qed. (* \paragraph{[O_EXACT_DIVIDE]} @@ -1869,7 +1835,7 @@ Definition exact_divide (k : Z) (body : term) (t : nat) (prop : proposition) := match prop with | EqTerm (Tint Z0) b => - match eq_term (scalar_norm t (Tmult body (Tint k))) b with + match eq_term (scalar_norm t (body * Tint k)%term) b with | true => match eq_Z k 0 with | true => TrueTerm @@ -1885,13 +1851,13 @@ Theorem exact_divide_valid : unfold valid1, exact_divide in |- *; intros k1 k2 t ep e p1; Simplify; - simpl in |- *; auto; elim_eq_term (scalar_norm t (Tmult k2 (Tint k1))) t1; - simpl in |- *; auto; elim_eq_Z k1 0%Z; simpl in |- *; + simpl in |- *; auto; elim_eq_term (scalar_norm t (k2 * Tint k1)%term) t1; + simpl in |- *; auto; elim_eq_Z k1 0; simpl in |- *; auto; intros H1 H2; elim H2; elim scalar_norm_stable; simpl in |- *; generalize H1; case (interp_term e k2); try trivial; (case k1; simpl in |- *; - [ intros; absurd (0%Z = 0%Z); assumption + [ intros; absurd (0 = 0); assumption | intros p2 p3 H3 H4; discriminate H4 | intros p2 p3 H3 H4; discriminate H4 ]). @@ -1908,14 +1874,13 @@ Definition divide_and_approx (k1 k2 : Z) (body : term) match prop with | LeqTerm (Tint Z0) b => match - eq_term (scalar_norm_add t (Tplus (Tmult body (Tint k1)) (Tint k2))) - b + eq_term (scalar_norm_add t (body * Tint k1 + Tint k2)%term) b with | true => - match (k1 ?= 0)%Z with - | Datatypes.Gt => - match (k1 ?= k2)%Z with - | Datatypes.Gt => LeqTerm (Tint 0) body + match k1 ?= 0 with + | Gt => + match k1 ?= k2 with + | Gt => LeqTerm (Tint 0) body | _ => prop end | _ => prop @@ -1931,7 +1896,7 @@ Theorem divide_and_approx_valid : unfold valid1, divide_and_approx in |- *; intros k1 k2 body t ep e p1; Simplify; - elim_eq_term (scalar_norm_add t (Tplus (Tmult body (Tint k1)) (Tint k2))) t1; + elim_eq_term (scalar_norm_add t (body * Tint k1 + Tint k2)%term) t1; Simplify; auto; intro E; elim E; simpl in |- *; elim (scalar_norm_add_stable t e); simpl in |- *; intro H1; apply Zmult_le_approx with (3 := H1); assumption. @@ -1944,7 +1909,7 @@ Definition merge_eq (t : nat) (prop1 prop2 : proposition) := | LeqTerm (Tint Z0) b1 => match prop2 with | LeqTerm (Tint Z0) b2 => - match eq_term b1 (scalar_norm t (Tmult b2 (Tint (-1)))) with + match eq_term b1 (scalar_norm t (b2 * Tint (-1))%term) with | true => EqTerm (Tint 0) b1 | false => TrueTerm end @@ -1965,7 +1930,7 @@ Qed. (* \paragraph{[O_CONSTANT_NUL]} *) -Definition constant_nul (i : nat) (h : list proposition) := +Definition constant_nul (i : nat) (h : hyps) := match nth_hyps i h with | NeqTerm (Tint Z0) (Tint Z0) => absurd | _ => h @@ -1975,8 +1940,7 @@ Theorem constant_nul_valid : forall i : nat, valid_hyps (constant_nul i). unfold valid_hyps, constant_nul in |- *; intros; generalize (nth_valid ep e i lp); Simplify; simpl in |- *; - unfold Zne in |- *; intro H1; absurd (0%Z = 0%Z); - auto. + unfold Zne in |- *; intro H1; absurd (0 = 0); auto. Qed. (* \paragraph{[O_STATE]} *) @@ -1985,9 +1949,8 @@ Definition state (m : Z) (s : step) (prop1 prop2 : proposition) := match prop1 with | EqTerm (Tint Z0) b1 => match prop2 with - | EqTerm (Tint Z0) (Tplus b2 (Topp b3)) => - EqTerm (Tint 0) - (rewrite s (Tplus b1 (Tmult (Tplus (Topp b3) b2) (Tint m)))) + | EqTerm (Tint Z0) (b2 + - b3)%term => + EqTerm (Tint 0) (rewrite s (b1 + (- b3 + b2) * Tint m)%term) | _ => TrueTerm end | _ => TrueTerm @@ -2007,21 +1970,19 @@ Qed. \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 : list proposition -> list (list proposition)) - (l : list proposition) := +Definition split_ineq (i t : nat) (f1 f2 : hyps -> lhyps) + (l : hyps) := match nth_hyps i l with | NeqTerm (Tint Z0) b1 => - f1 (LeqTerm (Tint 0) (add_norm t (Tplus b1 (Tint (-1)))) :: l) ++ + f1 (LeqTerm (Tint 0) (add_norm t (b1 + Tint (-1))%term) :: l) ++ f2 (LeqTerm (Tint 0) - (scalar_norm_add t (Tplus (Tmult b1 (Tint (-1))) (Tint (-1)))) - :: l) + (scalar_norm_add t (b1 * Tint (-1) + Tint (-1))%term) :: l) | _ => l :: nil end. Theorem split_ineq_valid : - forall (i t : nat) (f1 f2 : list proposition -> list (list proposition)), + 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). @@ -2041,34 +2002,27 @@ Qed. (* \subsection{La fonction de rejeu de la trace} *) -Fixpoint execute_omega (t : t_omega) (l : list proposition) {struct t} : - list (list proposition) := +Fixpoint execute_omega (t : t_omega) (l : hyps) {struct t} : lhyps := match t with - | O_CONSTANT_NOT_NUL n => - (fun a : list proposition => a :: nil) (constant_not_nul n l) - | O_CONSTANT_NEG n => - (fun a : list proposition => a :: nil) (constant_neg n l) + | 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 => - (fun a : list proposition => a :: nil) - (not_exact_divide k1 k2 body t i l) + 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 => - (fun a : list proposition => a :: nil) (contradiction t i j 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 => - (fun a : list proposition => a :: nil) (constant_nul i l) - | O_NEGATE_CONTRADICT i j => - (fun a : list proposition => a :: nil) (negate_contradict i j 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 => - (fun a : list proposition => a :: nil) (negate_contradict_inv t i j l) + 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. @@ -2126,14 +2080,12 @@ Qed. Definition move_right (s : step) (p : proposition) := match p with - | EqTerm t1 t2 => EqTerm (Tint 0) (rewrite s (Tplus t1 (Topp t2))) - | LeqTerm t1 t2 => LeqTerm (Tint 0) (rewrite s (Tplus t2 (Topp t1))) - | GeqTerm t1 t2 => LeqTerm (Tint 0) (rewrite s (Tplus t1 (Topp t2))) - | LtTerm t1 t2 => - LeqTerm (Tint 0) (rewrite s (Tplus (Tplus t2 (Tint (-1))) (Topp t1))) - | GtTerm t1 t2 => - LeqTerm (Tint 0) (rewrite s (Tplus (Tplus t1 (Tint (-1))) (Topp t2))) - | NeqTerm t1 t2 => NeqTerm (Tint 0) (rewrite s (Tplus t1 (Topp t2))) + | 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. @@ -2165,7 +2117,7 @@ intros; unfold do_normalize in |- *; apply apply_oper_1_valid; Qed. Fixpoint do_normalize_list (l : list step) (i : nat) - (h : list proposition) {struct l} : list proposition := + (h : hyps) {struct l} : hyps := match l with | s :: l' => do_normalize_list l' (S i) (do_normalize i s h) | nil => h @@ -2181,11 +2133,8 @@ simple induction l; simpl in |- *; unfold valid_hyps in |- *; Qed. Theorem normalize_goal : - forall (s : list step) (ep : PropList) (env : list Z) (l : list proposition), - (fun (envp : PropList) (env : list Z) (l : list proposition) => - interp_goal_concl envp env FalseTerm l) ep env (do_normalize_list s 0 l) -> - (fun (envp : PropList) (env : list Z) (l : list proposition) => - interp_goal_concl envp env FalseTerm l) ep env l. + forall (s : list step) (ep : PropList) (env : list Z) (l : hyps), + interp_goal ep env (do_normalize_list s 0 l) -> interp_goal ep env l. intros; apply valid_goal with (2 := H); apply do_normalize_list_valid. Qed. @@ -2193,17 +2142,15 @@ Qed. (* \subsubsection{Exécution de la trace} *) Theorem execute_goal : - forall (t : t_omega) (ep : PropList) (env : list Z) (l : list proposition), - interp_list_goal ep env (execute_omega t l) -> - (fun (envp : PropList) (env : list Z) (l : list proposition) => - interp_goal_concl envp env FalseTerm l) ep env l. + forall (t : t_omega) (ep : PropList) (env : list Z) (l : hyps), + interp_list_goal ep env (execute_omega t l) -> interp_goal ep env l. intros; apply (goal_valid (execute_omega t) (omega_valid t) ep env l H). Qed. Theorem append_goal : - forall (ep : PropList) (e : list Z) (l1 l2 : list (list proposition)), + forall (ep : PropList) (e : list Z) (l1 l2 : lhyps), interp_list_goal ep e l1 /\ interp_list_goal ep e l2 -> interp_list_goal ep e (l1 ++ l2). @@ -2262,15 +2209,15 @@ Qed. conclusion. We use an intermediate fixpoint. *) Fixpoint interp_full_goal (envp : PropList) (env : list Z) - (c : proposition) (l : list proposition) {struct l} : Prop := + (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 : PropList) (e : list Z) - (lc : list proposition * proposition) : Prop := +Definition interp_full (ep : PropList) (e : list Z) + (lc : hyps * proposition) : Prop := match lc with | (l, c) => interp_full_goal ep e c l end. @@ -2279,7 +2226,7 @@ Definition interp_full (ep : PropList) (e : list Z) of its hypothesis and conclusion *) Theorem interp_full_false : - forall (ep : PropList) (e : list Z) (l : list proposition) (c : proposition), + forall (ep : PropList) (e : list Z) (l : hyps) (c : proposition), (interp_hyps ep e l -> interp_proposition ep e c) -> interp_full ep e (l, c). simple induction l; unfold interp_full in |- *; simpl in |- *; @@ -2291,7 +2238,7 @@ Qed. If the decidability cannot be "proven", then just forget about the conclusion (equivalent of replacing it with false) *) -Definition to_contradict (lc : list proposition * proposition) := +Definition to_contradict (lc : hyps * proposition) := match lc with | (l, c) => if decidability c then Tnot c :: l else l end. @@ -2300,10 +2247,8 @@ Definition to_contradict (lc : list proposition * proposition) := hypothesis implies the original goal *) Theorem to_contradict_valid : - forall (ep : PropList) (e : list Z) (lc : list proposition * proposition), - (fun (envp : PropList) (env : list Z) (l : list proposition) => - interp_goal_concl envp env FalseTerm l) ep e (to_contradict lc) -> - interp_full ep e lc. + forall (ep : PropList) (e : list Z) (lc : hyps * proposition), + interp_goal ep e (to_contradict lc) -> interp_full ep e lc. intros ep e lc; case lc; intros l c; simpl in |- *; pattern (decidability c) in |- *; apply bool_ind2; @@ -2336,8 +2281,7 @@ Fixpoint map_cons (A : Set) (x : A) (l : list (list A)) {struct l} : hypothesis will get desynchronised and this will be a mess. *) -Fixpoint destructure_hyps (nn : nat) (ll : list proposition) {struct nn} : - list (list proposition) := +Fixpoint destructure_hyps (nn : nat) (ll : hyps) {struct nn} : lhyps := match nn with | O => ll :: nil | S n => @@ -2371,8 +2315,7 @@ Fixpoint destructure_hyps (nn : nat) (ll : list proposition) {struct nn} : end. Theorem map_cons_val : - forall (ep : PropList) (e : list Z) (p : proposition) - (l : list (list proposition)), + forall (ep : PropList) (e : list Z) (p : proposition) (l : lhyps), interp_proposition ep e p -> interp_list_hyps ep e l -> interp_list_hyps ep e (map_cons _ p l). @@ -2514,7 +2457,7 @@ unfold prop_stable in |- *; intros f H ep e p; split; unfold decidable, Zne in |- *; tauto ]). Qed. -Theorem Zlt_left_inv : forall x y : Z, (0 <= y + -1 + - x)%Z -> (x < y)%Z. +Theorem Zlt_left_inv : forall x y : Z, 0 <= y + -1 + - x -> x < y. intros; apply Zsucc_lt_reg; apply Zle_lt_succ; apply (fun a b : Z => Zplus_le_reg_r a b (-1 + - x)); @@ -2570,8 +2513,7 @@ simple induction s; simpl in |- *; | unfold prop_stable in |- *; simpl in |- *; intros; split; auto ]. Qed. -Fixpoint normalize_hyps (l : list h_step) (lh : list proposition) {struct l} - : list proposition := +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) @@ -2590,12 +2532,8 @@ simple induction l; unfold valid_hyps in |- *; simpl in |- *; Qed. Theorem normalize_hyps_goal : - forall (s : list h_step) (ep : PropList) (env : list Z) - (l : list proposition), - (fun (envp : PropList) (env : list Z) (l : list proposition) => - interp_goal_concl envp env FalseTerm l) ep env (normalize_hyps s l) -> - (fun (envp : PropList) (env : list Z) (l : list proposition) => - interp_goal_concl envp env FalseTerm l) ep env l. + forall (s : list h_step) (ep : PropList) (env : list Z) (l : hyps), + interp_goal ep env (normalize_hyps s l) -> interp_goal ep env l. intros; apply valid_goal with (2 := H); apply normalize_hyps_valid. Qed. @@ -2675,8 +2613,7 @@ unfold valid1, co_valid1 in |- *; simple induction s; Qed. -Fixpoint decompose_solve (s : e_step) (h : list proposition) {struct s} : - list (list proposition) := +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 @@ -2687,6 +2624,10 @@ Fixpoint decompose_solve (s : e_step) (h : list proposition) {struct s} : 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 => @@ -2710,28 +2651,32 @@ intro s; apply goal_valid; unfold valid_list_hyps in |- *; elim s; | 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 H3; right; apply H0; simpl in |- *; auto ] + | intros p1 p2 H2; + pattern (decidability p1) in |- *; apply bool_ind2; + [ 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 : list (list proposition) -> list (list proposition)) := - forall (ep : PropList) (e : list Z) (lp : list (list proposition)), +Definition valid_lhyps (f : lhyps -> lhyps) := + forall (ep : PropList) (e : list Z) (lp : lhyps), interp_list_hyps ep e lp -> interp_list_hyps ep e (f lp). -Fixpoint reduce_lhyps (lp : list (list proposition)) : - list (list proposition) := +Fixpoint reduce_lhyps (lp : lhyps) : lhyps := match lp with | (FalseTerm :: nil) :: lp' => reduce_lhyps lp' | x :: lp' => x :: reduce_lhyps lp' - | nil => nil (A:=list proposition) + | nil => nil (A:=hyps) end. Theorem reduce_lhyps_valid : valid_lhyps reduce_lhyps. @@ -2744,7 +2689,7 @@ unfold valid_lhyps in |- *; intros ep e lp; elim lp; Qed. Theorem do_reduce_lhyps : - forall (envp : PropList) (env : list Z) (l : list (list proposition)), + forall (envp : PropList) (env : list Z) (l : lhyps), interp_list_goal envp env (reduce_lhyps l) -> interp_list_goal envp env l. intros envp env l H; apply list_goal_to_hyps; intro H1; @@ -2756,13 +2701,11 @@ Definition concl_to_hyp (p : proposition) := if decidability p then Tnot p else TrueTerm. Definition do_concl_to_hyp : - forall (envp : PropList) (env : list Z) (c : proposition) - (l : list proposition), - (fun (envp : PropList) (env : list Z) (l : list proposition) => - interp_goal_concl envp env FalseTerm l) envp env ( - concl_to_hyp c :: l) -> interp_goal_concl envp env c l. + forall (envp : PropList) (env : list Z) (c : proposition) (l : hyps), + interp_goal envp env (concl_to_hyp c :: l) -> + interp_goal_concl c envp env l. -simpl in |- *; intros envp env c l; induction l as [| a l Hrecl]; +simpl in |- *; intros envp env c l; induction l as [| a l Hrecl]; [ simpl in |- *; unfold concl_to_hyp in |- *; pattern (decidability c) in |- *; apply bool_ind2; [ intro H; generalize (decidable_correct envp env c H); @@ -2772,16 +2715,16 @@ simpl in |- *; intros envp env c l; induction l as [| a l Hrecl]; Qed. Definition omega_tactic (t1 : e_step) (t2 : list h_step) - (c : proposition) (l : list proposition) := + (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 : PropList) - (env : list Z) (c : proposition) (l : list proposition), + (env : list Z) (c : proposition) (l : hyps), interp_list_goal envp env (omega_tactic t1 t2 c l) -> - interp_goal_concl envp env c l. + interp_goal_concl c envp env l. 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.
\ No newline at end of file +Qed. diff --git a/contrib/romega/const_omega.ml b/contrib/romega/const_omega.ml index 3b2a7d31..69b4b2de 100644 --- a/contrib/romega/const_omega.ml +++ b/contrib/romega/const_omega.ml @@ -17,7 +17,6 @@ type result = let destructurate t = let c, args = Term.decompose_app t in - let env = Global.env() in match Term.kind_of_term c, args with | Term.Const sp, args -> Kapp (Names.string_of_id @@ -43,7 +42,7 @@ 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.Const sp -> Libnames.ConstRef sp | Term.Construct csp -> Libnames.ConstructRef csp | Term.Ind isp -> Libnames.IndRef isp | _ -> raise Destruct @@ -53,14 +52,16 @@ let recognize_number t = let rec loop t = let f,l = dest_const_apply t in match Names.string_of_id f,l with - "xI",[t] -> 1 + 2 * loop t - | "xO",[t] -> 2 * loop t - | "xH",[] -> 1 + "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] -> - (loop t) | "Z0",[] -> 0 - | _ -> failwith "not a number";; + "Zpos",[t] -> loop t + | "Zneg",[t] -> Bigint.neg (loop t) + | "Z0",[] -> Bigint.zero + | _ -> failwith "not a number";; let logic_dir = ["Coq";"Logic";"Decidable"] @@ -68,7 +69,7 @@ let logic_dir = ["Coq";"Logic";"Decidable"] let coq_modules = Coqlib.init_modules @ [logic_dir] @ Coqlib.arith_modules @ Coqlib.zarith_base_modules @ [["Coq"; "omega"; "OmegaLemmas"]] - @ [["Coq"; "Lists"; (if !Options.v7 then "PolyList" else "List")]] + @ [["Coq"; "Lists"; "List"]] @ [module_refl_path] @@ -77,23 +78,23 @@ let constant = Coqlib.gen_constant_in_modules "Omega" coq_modules let coq_xH = lazy (constant "xH") let coq_xO = lazy (constant "xO") let coq_xI = lazy (constant "xI") -let coq_ZERO = lazy (constant "Z0") -let coq_POS = lazy (constant "Zpos") -let coq_NEG = lazy (constant "Zneg") +let coq_Z0 = lazy (constant "Z0") +let coq_Zpos = lazy (constant "Zpos") +let coq_Zneg = lazy (constant "Zneg") let coq_Z = lazy (constant "Z") -let coq_relation = lazy (constant "comparison") -let coq_SUPERIEUR = lazy (constant "SUPERIEUR") -let coq_INFEEIEUR = lazy (constant "INFERIEUR") -let coq_EGAL = lazy (constant "EGAL") +let coq_comparison = lazy (constant "comparison") +let coq_Gt = lazy (constant "Gt") +let coq_Lt = lazy (constant "Lt") +let coq_Eq = lazy (constant "Eq") let coq_Zplus = lazy (constant "Zplus") let coq_Zmult = lazy (constant "Zmult") let coq_Zopp = lazy (constant "Zopp") let coq_Zminus = lazy (constant "Zminus") -let coq_Zs = lazy (constant "Zs") +let coq_Zsucc = lazy (constant "Zsucc") let coq_Zgt = lazy (constant "Zgt") let coq_Zle = lazy (constant "Zle") -let coq_inject_nat = lazy (constant "inject_nat") +let coq_Z_of_nat = lazy (constant "Z_of_nat") (* Peano *) let coq_le = lazy(constant "le") @@ -111,8 +112,8 @@ let coq_refl_equal = lazy(constant "refl_equal") let coq_and = lazy(constant "and") let coq_not = lazy(constant "not") let coq_or = lazy(constant "or") -let coq_true = lazy(constant "true") -let coq_false = lazy(constant "false") +let coq_True = lazy(constant "True") +let coq_False = lazy(constant "False") let coq_ex = lazy(constant "ex") let coq_I = lazy(constant "I") @@ -159,8 +160,7 @@ let coq_normalize_sequent = lazy (constant "normalize_goal") let coq_execute_sequent = lazy (constant "execute_goal") let coq_do_concl_to_hyp = lazy (constant "do_concl_to_hyp") let coq_sequent_to_hyps = lazy (constant "goal_to_hyps") -let coq_normalize_hyps_goal = - lazy (constant "normalize_hyps_goal") +let coq_normalize_hyps_goal = lazy (constant "normalize_hyps_goal") (* Constructors for shuffle tactic *) let coq_t_fusion = lazy (constant "t_fusion") @@ -187,7 +187,7 @@ 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_sym = lazy (constant "C_PLUS_SYM") +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") @@ -199,7 +199,7 @@ 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_sym = lazy (constant "C_MULT_SYM") +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") @@ -230,184 +230,6 @@ let coq_decompose_solve_valid = let coq_do_reduce_lhyps = lazy (constant "do_reduce_lhyps") let coq_do_omega = lazy (constant "do_omega") -(** -let constant dir s = - try - Libnames.constr_of_reference - (Nametab.absolute_reference - (Libnames.make_path - (Names.make_dirpath (List.map Names.id_of_string (List.rev dir))) - (Names.id_of_string s))) - with e -> print_endline (String.concat "." dir); print_endline s; - raise e - -let path_fast_integer = ["Coq"; "ZArith"; "fast_integer"] -let path_zarith_aux = ["Coq"; "ZArith"; "zarith_aux"] -let path_logic = ["Coq"; "Init";"Logic"] -let path_datatypes = ["Coq"; "Init";"Datatypes"] -let path_peano = ["Coq"; "Init"; "Peano"] -let path_list = ["Coq"; "Lists"; "PolyList"] - -let coq_xH = lazy (constant path_fast_integer "xH") -let coq_xO = lazy (constant path_fast_integer "xO") -let coq_xI = lazy (constant path_fast_integer "xI") -let coq_ZERO = lazy (constant path_fast_integer "ZERO") -let coq_POS = lazy (constant path_fast_integer "POS") -let coq_NEG = lazy (constant path_fast_integer "NEG") -let coq_Z = lazy (constant path_fast_integer "Z") -let coq_relation = lazy (constant path_fast_integer "relation") -let coq_SUPERIEUR = lazy (constant path_fast_integer "SUPERIEUR") -let coq_INFEEIEUR = lazy (constant path_fast_integer "INFERIEUR") -let coq_EGAL = lazy (constant path_fast_integer "EGAL") -let coq_Zplus = lazy (constant path_fast_integer "Zplus") -let coq_Zmult = lazy (constant path_fast_integer "Zmult") -let coq_Zopp = lazy (constant path_fast_integer "Zopp") - -(* auxiliaires zarith *) -let coq_Zminus = lazy (constant path_zarith_aux "Zminus") -let coq_Zs = lazy (constant path_zarith_aux "Zs") -let coq_Zgt = lazy (constant path_zarith_aux "Zgt") -let coq_Zle = lazy (constant path_zarith_aux "Zle") -let coq_inject_nat = lazy (constant path_zarith_aux "inject_nat") - -(* Peano *) -let coq_le = lazy(constant path_peano "le") -let coq_gt = lazy(constant path_peano "gt") - -(* Integers *) -let coq_nat = lazy(constant path_datatypes "nat") -let coq_S = lazy(constant path_datatypes "S") -let coq_O = lazy(constant path_datatypes "O") - -(* Minus *) -let coq_minus = lazy(constant ["Arith"; "Minus"] "minus") - -(* Logic *) -let coq_eq = lazy(constant path_logic "eq") -let coq_refl_equal = lazy(constant path_logic "refl_equal") -let coq_and = lazy(constant path_logic "and") -let coq_not = lazy(constant path_logic "not") -let coq_or = lazy(constant path_logic "or") -let coq_true = lazy(constant path_logic "true") -let coq_false = lazy(constant path_logic "false") -let coq_ex = lazy(constant path_logic "ex") -let coq_I = lazy(constant path_logic "I") - -(* Lists *) -let coq_cons = lazy (constant path_list "cons") -let coq_nil = lazy (constant path_list "nil") - -let coq_pcons = lazy (constant module_refl_path "Pcons") -let coq_pnil = lazy (constant module_refl_path "Pnil") - -let coq_h_step = lazy (constant module_refl_path "h_step") -let coq_pair_step = lazy (constant module_refl_path "pair_step") -let coq_p_left = lazy (constant module_refl_path "P_LEFT") -let coq_p_right = lazy (constant module_refl_path "P_RIGHT") -let coq_p_invert = lazy (constant module_refl_path "P_INVERT") -let coq_p_step = lazy (constant module_refl_path "P_STEP") -let coq_p_nop = lazy (constant module_refl_path "P_NOP") - - -let coq_t_int = lazy (constant module_refl_path "Tint") -let coq_t_plus = lazy (constant module_refl_path "Tplus") -let coq_t_mult = lazy (constant module_refl_path "Tmult") -let coq_t_opp = lazy (constant module_refl_path "Topp") -let coq_t_minus = lazy (constant module_refl_path "Tminus") -let coq_t_var = lazy (constant module_refl_path "Tvar") - -let coq_p_eq = lazy (constant module_refl_path "EqTerm") -let coq_p_leq = lazy (constant module_refl_path "LeqTerm") -let coq_p_geq = lazy (constant module_refl_path "GeqTerm") -let coq_p_lt = lazy (constant module_refl_path "LtTerm") -let coq_p_gt = lazy (constant module_refl_path "GtTerm") -let coq_p_neq = lazy (constant module_refl_path "NeqTerm") -let coq_p_true = lazy (constant module_refl_path "TrueTerm") -let coq_p_false = lazy (constant module_refl_path "FalseTerm") -let coq_p_not = lazy (constant module_refl_path "Tnot") -let coq_p_or = lazy (constant module_refl_path "Tor") -let coq_p_and = lazy (constant module_refl_path "Tand") -let coq_p_imp = lazy (constant module_refl_path "Timp") -let coq_p_prop = lazy (constant module_refl_path "Tprop") - -let coq_proposition = lazy (constant module_refl_path "proposition") -let coq_interp_sequent = lazy (constant module_refl_path "interp_goal_concl") -let coq_normalize_sequent = lazy (constant module_refl_path "normalize_goal") -let coq_execute_sequent = lazy (constant module_refl_path "execute_goal") -let coq_do_concl_to_hyp = lazy (constant module_refl_path "do_concl_to_hyp") -let coq_sequent_to_hyps = lazy (constant module_refl_path "goal_to_hyps") -let coq_normalize_hyps_goal = - lazy (constant module_refl_path "normalize_hyps_goal") - -(* Constructors for shuffle tactic *) -let coq_t_fusion = lazy (constant module_refl_path "t_fusion") -let coq_f_equal = lazy (constant module_refl_path "F_equal") -let coq_f_cancel = lazy (constant module_refl_path "F_cancel") -let coq_f_left = lazy (constant module_refl_path "F_left") -let coq_f_right = lazy (constant module_refl_path "F_right") - -(* Constructors for reordering tactics *) -let coq_step = lazy (constant module_refl_path "step") -let coq_c_do_both = lazy (constant module_refl_path "C_DO_BOTH") -let coq_c_do_left = lazy (constant module_refl_path "C_LEFT") -let coq_c_do_right = lazy (constant module_refl_path "C_RIGHT") -let coq_c_do_seq = lazy (constant module_refl_path "C_SEQ") -let coq_c_nop = lazy (constant module_refl_path "C_NOP") -let coq_c_opp_plus = lazy (constant module_refl_path "C_OPP_PLUS") -let coq_c_opp_opp = lazy (constant module_refl_path "C_OPP_OPP") -let coq_c_opp_mult_r = lazy (constant module_refl_path "C_OPP_MULT_R") -let coq_c_opp_one = lazy (constant module_refl_path "C_OPP_ONE") -let coq_c_reduce = lazy (constant module_refl_path "C_REDUCE") -let coq_c_mult_plus_distr = lazy (constant module_refl_path "C_MULT_PLUS_DISTR") -let coq_c_opp_left = lazy (constant module_refl_path "C_MULT_OPP_LEFT") -let coq_c_mult_assoc_r = lazy (constant module_refl_path "C_MULT_ASSOC_R") -let coq_c_plus_assoc_r = lazy (constant module_refl_path "C_PLUS_ASSOC_R") -let coq_c_plus_assoc_l = lazy (constant module_refl_path "C_PLUS_ASSOC_L") -let coq_c_plus_permute = lazy (constant module_refl_path "C_PLUS_PERMUTE") -let coq_c_plus_sym = lazy (constant module_refl_path "C_PLUS_SYM") -let coq_c_red0 = lazy (constant module_refl_path "C_RED0") -let coq_c_red1 = lazy (constant module_refl_path "C_RED1") -let coq_c_red2 = lazy (constant module_refl_path "C_RED2") -let coq_c_red3 = lazy (constant module_refl_path "C_RED3") -let coq_c_red4 = lazy (constant module_refl_path "C_RED4") -let coq_c_red5 = lazy (constant module_refl_path "C_RED5") -let coq_c_red6 = lazy (constant module_refl_path "C_RED6") -let coq_c_mult_opp_left = lazy (constant module_refl_path "C_MULT_OPP_LEFT") -let coq_c_mult_assoc_reduced = - lazy (constant module_refl_path "C_MULT_ASSOC_REDUCED") -let coq_c_minus = lazy (constant module_refl_path "C_MINUS") -let coq_c_mult_sym = lazy (constant module_refl_path "C_MULT_SYM") - -let coq_s_constant_not_nul = lazy (constant module_refl_path "O_CONSTANT_NOT_NUL") -let coq_s_constant_neg = lazy (constant module_refl_path "O_CONSTANT_NEG") -let coq_s_div_approx = lazy (constant module_refl_path "O_DIV_APPROX") -let coq_s_not_exact_divide = lazy (constant module_refl_path "O_NOT_EXACT_DIVIDE") -let coq_s_exact_divide = lazy (constant module_refl_path "O_EXACT_DIVIDE") -let coq_s_sum = lazy (constant module_refl_path "O_SUM") -let coq_s_state = lazy (constant module_refl_path "O_STATE") -let coq_s_contradiction = lazy (constant module_refl_path "O_CONTRADICTION") -let coq_s_merge_eq = lazy (constant module_refl_path "O_MERGE_EQ") -let coq_s_split_ineq =lazy (constant module_refl_path "O_SPLIT_INEQ") -let coq_s_constant_nul =lazy (constant module_refl_path "O_CONSTANT_NUL") -let coq_s_negate_contradict =lazy (constant module_refl_path "O_NEGATE_CONTRADICT") -let coq_s_negate_contradict_inv =lazy (constant module_refl_path "O_NEGATE_CONTRADICT_INV") - -(* construction for the [extract_hyp] tactic *) -let coq_direction = lazy (constant module_refl_path "direction") -let coq_d_left = lazy (constant module_refl_path "D_left") -let coq_d_right = lazy (constant module_refl_path "D_right") -let coq_d_mono = lazy (constant module_refl_path "D_mono") - -let coq_e_split = lazy (constant module_refl_path "E_SPLIT") -let coq_e_extract = lazy (constant module_refl_path "E_EXTRACT") -let coq_e_solve = lazy (constant module_refl_path "E_SOLVE") - -let coq_decompose_solve_valid = - lazy (constant module_refl_path "decompose_solve_valid") -let coq_do_reduce_lhyps = lazy (constant module_refl_path "do_reduce_lhyps") -let coq_do_omega = lazy (constant module_refl_path "do_omega") - -*) (* \subsection{Construction d'expressions} *) @@ -423,8 +245,8 @@ let mk_and t1 t2 = Term.mkApp (Lazy.force coq_and, [|t1; t2 |]) let mk_or t1 t2 = Term.mkApp (Lazy.force coq_or, [|t1; t2 |]) let mk_not t = Term.mkApp (Lazy.force coq_not, [|t |]) let mk_eq_rel t1 t2 = Term.mkApp (Lazy.force coq_eq, [| - Lazy.force coq_relation; t1; t2 |]) -let mk_inj t = Term.mkApp (Lazy.force coq_inject_nat, [|t |]) + Lazy.force coq_comparison; t1; t2 |]) +let mk_inj t = Term.mkApp (Lazy.force coq_Z_of_nat, [|t |]) let do_left t = @@ -450,16 +272,20 @@ let rec do_list = function | [x] -> x | (x::l) -> do_seq x (do_list l) - let mk_integer n = let rec loop n = - if n=1 then Lazy.force coq_xH else - Term.mkApp ((if n mod 2 = 0 then Lazy.force coq_xO else Lazy.force coq_xI), - [| loop (n/2) |]) in + 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), + [| loop q |]) in - if n = 0 then Lazy.force coq_ZERO - else Term.mkApp ((if n > 0 then Lazy.force coq_POS else Lazy.force coq_NEG), - [| loop (abs n) |]) + if n = Bigint.zero then Lazy.force coq_Z0 + else + if Bigint.is_strictly_pos n then + Term.mkApp (Lazy.force coq_Zpos, [| loop n |]) + else + Term.mkApp (Lazy.force coq_Zneg, [| loop (Bigint.neg n) |]) let mk_Z = mk_integer diff --git a/contrib/romega/g_romega.ml4 b/contrib/romega/g_romega.ml4 index 386f7f28..7cfc50f8 100644 --- a/contrib/romega/g_romega.ml4 +++ b/contrib/romega/g_romega.ml4 @@ -10,6 +10,6 @@ open Refl_omega -TACTIC EXTEND ROmega - [ "ROmega" ] -> [ total_reflexive_omega_tactic ] +TACTIC EXTEND romelga + [ "romega" ] -> [ total_reflexive_omega_tactic ] END diff --git a/contrib/romega/omega2.ml b/contrib/romega/omega2.ml deleted file mode 100644 index 91aefc60..00000000 --- a/contrib/romega/omega2.ml +++ /dev/null @@ -1,675 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) -(**************************************************************************) -(* *) -(* Omega: a solver of quantifier-free problems in Presburger Arithmetic *) -(* *) -(* Pierre Crégut (CNET, Lannion, France) *) -(* *) -(* 13/10/2002 : modified to cope with an external numbering of equations *) -(* and hypothesis. Its use for Omega is not more complex and it makes *) -(* things much simpler for the reflexive version where we should limit *) -(* the number of source of numbering. *) -(**************************************************************************) - -open Names - -let flat_map f = - let rec flat_map_f = function - | [] -> [] - | x :: l -> f x @ flat_map_f l - in - flat_map_f - -let pp i = print_int i; print_newline (); flush stdout - -let debug = ref false - -let filter = List.partition - -let push v l = l := v :: !l - -let rec pgcd x y = if y = 0 then x else pgcd y (x mod y) - -let pgcd_l = function - | [] -> failwith "pgcd_l" - | x :: l -> List.fold_left pgcd x l - -let floor_div a b = - match a >=0 , b > 0 with - | true,true -> a / b - | false,false -> a / b - | true, false -> (a-1) / b - 1 - | false,true -> (a+1) / b - 1 - -type coeff = {c: int ; v: int} - -type linear = coeff list - -type eqn_kind = EQUA | INEQ | DISE - -type afine = { - (* a number uniquely identifying the equation *) - id: int ; - (* a boolean true for an eq, false for an ineq (Sigma a_i x_i >= 0) *) - kind: eqn_kind; - (* the variables and their coefficient *) - body: coeff list; - (* a constant *) - constant: int } - -type state_action = { - st_new_eq : afine; - st_def : afine; - st_orig : afine; - st_coef : int; - st_var : int } - -type action = - | DIVIDE_AND_APPROX of afine * afine * int * int - | NOT_EXACT_DIVIDE of afine * int - | FORGET_C of int - | EXACT_DIVIDE of afine * int - | SUM of int * (int * afine) * (int * afine) - | STATE of state_action - | HYP of afine - | FORGET of int * int - | FORGET_I of int * int - | CONTRADICTION of afine * afine - | NEGATE_CONTRADICT of afine * afine * bool - | MERGE_EQ of int * afine * int - | CONSTANT_NOT_NUL of int * int - | CONSTANT_NUL of int - | CONSTANT_NEG of int * int - | SPLIT_INEQ of afine * (int * action list) * (int * action list) - | WEAKEN of int * int - -exception UNSOLVABLE - -exception NO_CONTRADICTION - -let display_eq print_var (l,e) = - let _ = - List.fold_left - (fun not_first f -> - print_string - (if f.c < 0 then "- " else if not_first then "+ " else ""); - let c = abs f.c in - if c = 1 then - Printf.printf "%s " (print_var f.v) - else - Printf.printf "%d %s " c (print_var f.v); - true) - false l - in - if e > 0 then - Printf.printf "+ %d " e - else if e < 0 then - Printf.printf "- %d " (abs e) - -let rec trace_length l = - let action_length accu = function - | SPLIT_INEQ (_,(_,l1),(_,l2)) -> - accu + 1 + trace_length l1 + trace_length l2 - | _ -> accu + 1 in - List.fold_left action_length 0 l - -let operator_of_eq = function - | EQUA -> "=" | DISE -> "!=" | INEQ -> ">=" - -let kind_of = function - | EQUA -> "equation" | DISE -> "disequation" | INEQ -> "inequation" - -let display_system print_var l = - List.iter - (fun { kind=b; body=e; constant=c; id=id} -> - print_int id; print_string ": "; - display_eq print_var (e,c); print_string (operator_of_eq b); - print_string "0\n") - l; - print_string "------------------------\n\n" - -let display_inequations print_var l = - List.iter (fun e -> display_eq print_var e;print_string ">= 0\n") l; - print_string "------------------------\n\n" - -let rec display_action print_var = function - | act :: l -> begin match act with - | DIVIDE_AND_APPROX (e1,e2,k,d) -> - Printf.printf - "Inequation E%d is divided by %d and the constant coefficient is \ - rounded by substracting %d.\n" e1.id k d - | NOT_EXACT_DIVIDE (e,k) -> - Printf.printf - "Constant in equation E%d is not divisible by the pgcd \ - %d of its other coefficients.\n" e.id k - | EXACT_DIVIDE (e,k) -> - Printf.printf - "Equation E%d is divided by the pgcd \ - %d of its coefficients.\n" e.id k - | WEAKEN (e,k) -> - Printf.printf - "To ensure a solution in the dark shadow \ - the equation E%d is weakened by %d.\n" e k - | SUM (e,(c1,e1),(c2,e2)) -> - Printf.printf - "We state %s E%d = %d %s E%d + %d %s E%d.\n" - (kind_of e1.kind) e c1 (kind_of e1.kind) e1.id c2 - (kind_of e2.kind) e2.id - | STATE { st_new_eq = e; st_coef = x} -> - Printf.printf "We define a new equation %d :" e.id; - display_eq print_var (e.body,e.constant); - print_string (operator_of_eq e.kind); print_string " 0\n" - | HYP e -> - Printf.printf "We define %d :" e.id; - display_eq print_var (e.body,e.constant); - print_string (operator_of_eq e.kind); print_string " 0\n" - | FORGET_C e -> Printf.printf "E%d is trivially satisfiable.\n" e - | FORGET (e1,e2) -> Printf.printf "E%d subsumes E%d.\n" e1 e2 - | FORGET_I (e1,e2) -> Printf.printf "E%d subsumes E%d.\n" e1 e2 - | MERGE_EQ (e,e1,e2) -> - Printf.printf "E%d and E%d can be merged into E%d.\n" e1.id e2 e - | CONTRADICTION (e1,e2) -> - Printf.printf - "equations E%d and E%d implie a contradiction on their \ - constant factors.\n" e1.id e2.id - | NEGATE_CONTRADICT(e1,e2,b) -> - Printf.printf - "Eqations E%d and E%d state that their body is at the same time - equal and different\n" e1.id e2.id - | CONSTANT_NOT_NUL (e,k) -> - Printf.printf "equation E%d states %d=0.\n" e k - | CONSTANT_NEG(e,k) -> - Printf.printf "equation E%d states %d >= 0.\n" e k - | CONSTANT_NUL e -> - Printf.printf "inequation E%d states 0 != 0.\n" e - | SPLIT_INEQ (e,(e1,l1),(e2,l2)) -> - Printf.printf "equation E%d is split in E%d and E%d\n\n" e.id e1 e2; - display_action print_var l1; - print_newline (); - display_action print_var l2; - print_newline () - end; display_action print_var l - | [] -> - flush stdout - -(*""*) -let default_print_var v = Printf.sprintf "XX%d" v - -let add_event, history, clear_history = - let accu = ref [] in - (fun (v:action) -> if !debug then display_action default_print_var [v]; push v accu), - (fun () -> !accu), - (fun () -> accu := []) - -let nf_linear = Sort.list (fun x y -> x.v > y.v) - -let nf ((b : bool),(e,(x : int))) = (b,(nf_linear e,x)) - -let map_eq_linear f = - let rec loop = function - | x :: l -> let c = f x.c in if c=0 then loop l else {v=x.v; c=c} :: loop l - | [] -> [] - in - loop - -let map_eq_afine f e = - { id = e.id; kind = e.kind; body = map_eq_linear f e.body; - constant = f e.constant } - -let negate_eq = map_eq_afine (fun x -> -x) - -let rec sum p0 p1 = match (p0,p1) with - | ([], l) -> l | (l, []) -> l - | (((x1::l1) as l1'), ((x2::l2) as l2')) -> - if x1.v = x2.v then - let c = x1.c + x2.c in - if c = 0 then sum l1 l2 else {v=x1.v;c=c} :: sum l1 l2 - else if x1.v > x2.v then - x1 :: sum l1 l2' - else - x2 :: sum l1' l2 - -let sum_afine new_eq_id eq1 eq2 = - { kind = eq1.kind; id = new_eq_id (); - body = sum eq1.body eq2.body; constant = eq1.constant + eq2.constant } - -exception FACTOR1 - -let rec chop_factor_1 = function - | x :: l -> - if abs x.c = 1 then x,l else let (c',l') = chop_factor_1 l in (c',x::l') - | [] -> raise FACTOR1 - -exception CHOPVAR - -let rec chop_var v = function - | f :: l -> if f.v = v then f,l else let (f',l') = chop_var v l in (f',f::l') - | [] -> raise CHOPVAR - -let normalize ({id=id; kind=eq_flag; body=e; constant =x} as eq) = - if e = [] then begin - match eq_flag with - | EQUA -> - if x =0 then [] else begin - add_event (CONSTANT_NOT_NUL(id,x)); raise UNSOLVABLE - end - | DISE -> - if x <> 0 then [] else begin - add_event (CONSTANT_NUL id); raise UNSOLVABLE - end - | INEQ -> - if x >= 0 then [] else begin - add_event (CONSTANT_NEG(id,x)); raise UNSOLVABLE - end - end else - let gcd = pgcd_l (List.map (fun f -> abs f.c) e) in - if eq_flag=EQUA & x mod gcd <> 0 then begin - add_event (NOT_EXACT_DIVIDE (eq,gcd)); raise UNSOLVABLE - end else if eq_flag=DISE & x mod gcd <> 0 then begin - add_event (FORGET_C eq.id); [] - end else if gcd <> 1 then begin - let c = floor_div x gcd in - let d = x - c * gcd in - let new_eq = {id=id; kind=eq_flag; constant=c; - body=map_eq_linear (fun c -> c / gcd) e} in - add_event (if eq_flag=EQUA or eq_flag = DISE then EXACT_DIVIDE(eq,gcd) - else DIVIDE_AND_APPROX(eq,new_eq,gcd,d)); - [new_eq] - end else [eq] - -let eliminate_with_in new_eq_id {v=v;c=c_unite} eq2 - ({body=e1; constant=c1} as eq1) = - try - let (f,_) = chop_var v e1 in - let coeff = if c_unite=1 then -f.c else if c_unite= -1 then f.c - else failwith "eliminate_with_in" in - let res = sum_afine new_eq_id eq1 (map_eq_afine (fun c -> c * coeff) eq2) in - add_event (SUM (res.id,(1,eq1),(coeff,eq2))); res - with CHOPVAR -> eq1 - -let omega_mod a b = a - b * floor_div (2 * a + b) (2 * b) -let banerjee_step (new_eq_id,new_var_id,print_var) original l1 l2 = - let e = original.body in - let sigma = new_var_id () in - let smallest,var = - try - List.fold_left (fun (v,p) c -> if v > (abs c.c) then abs c.c,c.v else (v,p)) - (abs (List.hd e).c, (List.hd e).v) (List.tl e) - with Failure "tl" -> display_system print_var [original] ; failwith "TL" in - let m = smallest + 1 in - let new_eq = - { constant = omega_mod original.constant m; - body = {c= -m;v=sigma} :: - map_eq_linear (fun a -> omega_mod a m) original.body; - id = new_eq_id (); kind = EQUA } in - let definition = - { constant = - floor_div (2 * original.constant + m) (2 * m); - body = map_eq_linear (fun a -> - floor_div (2 * a + m) (2 * m)) - original.body; - id = new_eq_id (); kind = EQUA } in - add_event (STATE {st_new_eq = new_eq; st_def = definition; - st_orig =original; st_coef = m; st_var = sigma}); - let new_eq = List.hd (normalize new_eq) in - let eliminated_var, def = chop_var var new_eq.body in - let other_equations = - flat_map (fun e -> normalize (eliminate_with_in new_eq_id eliminated_var new_eq e)) - l1 in - let inequations = - flat_map (fun e -> normalize (eliminate_with_in new_eq_id eliminated_var new_eq e)) - l2 in - let original' = eliminate_with_in new_eq_id eliminated_var new_eq original in - let mod_original = map_eq_afine (fun c -> c / m) original' in - add_event (EXACT_DIVIDE (original',m)); - List.hd (normalize mod_original),other_equations,inequations - -let rec eliminate_one_equation ((new_eq_id,new_var_id,print_var) as new_ids) (e,other,ineqs) = - if !debug then display_system print_var (e::other); - try - let v,def = chop_factor_1 e.body in - (flat_map (fun e' -> normalize (eliminate_with_in new_eq_id v e e')) other, - flat_map (fun e' -> normalize (eliminate_with_in new_eq_id v e e')) ineqs) - with FACTOR1 -> - eliminate_one_equation new_ids (banerjee_step new_ids e other ineqs) - -let rec banerjee ((_,_,print_var) as new_ids) (sys_eq,sys_ineq) = - let rec fst_eq_1 = function - (eq::l) -> - if List.exists (fun x -> abs x.c = 1) eq.body then eq,l - else let (eq',l') = fst_eq_1 l in (eq',eq::l') - | [] -> raise Not_found in - match sys_eq with - [] -> if !debug then display_system print_var sys_ineq; sys_ineq - | (e1::rest) -> - let eq,other = try fst_eq_1 sys_eq with Not_found -> (e1,rest) in - if eq.body = [] then - if eq.constant = 0 then begin - add_event (FORGET_C eq.id); banerjee new_ids (other,sys_ineq) - end else begin - add_event (CONSTANT_NOT_NUL(eq.id,eq.constant)); raise UNSOLVABLE - end - else - banerjee new_ids - (eliminate_one_equation new_ids (eq,other,sys_ineq)) - -type kind = INVERTED | NORMAL - -let redundancy_elimination new_eq_id system = - let normal = function - ({body=f::_} as e) when f.c < 0 -> negate_eq e, INVERTED - | e -> e,NORMAL in - let table = Hashtbl.create 7 in - List.iter - (fun e -> - let ({body=ne} as nx) ,kind = normal e in - if ne = [] then - if nx.constant < 0 then begin - add_event (CONSTANT_NEG(nx.id,nx.constant)); raise UNSOLVABLE - end else add_event (FORGET_C nx.id) - else - try - let (optnormal,optinvert) = Hashtbl.find table ne in - let final = - if kind = NORMAL then begin - match optnormal with - Some v -> - let kept = - if v.constant < nx.constant - then begin add_event (FORGET (v.id,nx.id));v end - else begin add_event (FORGET (nx.id,v.id));nx end in - (Some(kept),optinvert) - | None -> Some nx,optinvert - end else begin - match optinvert with - Some v -> - let kept = - if v.constant > nx.constant - then begin add_event (FORGET_I (v.id,nx.id));v end - else begin add_event (FORGET_I (nx.id,v.id));nx end in - (optnormal,Some(if v.constant > nx.constant then v else nx)) - | None -> optnormal,Some nx - end in - begin match final with - (Some high, Some low) -> - if high.constant < low.constant then begin - add_event(CONTRADICTION (high,negate_eq low)); - raise UNSOLVABLE - end - | _ -> () end; - Hashtbl.remove table ne; - Hashtbl.add table ne final - with Not_found -> - Hashtbl.add table ne - (if kind = NORMAL then (Some nx,None) else (None,Some nx))) - system; - let accu_eq = ref [] in - let accu_ineq = ref [] in - Hashtbl.iter - (fun p0 p1 -> match (p0,p1) with - | (e, (Some x, Some y)) when x.constant = y.constant -> - let id=new_eq_id () in - add_event (MERGE_EQ(id,x,y.id)); - push {id=id; kind=EQUA; body=x.body; constant=x.constant} accu_eq - | (e, (optnorm,optinvert)) -> - begin match optnorm with - Some x -> push x accu_ineq | _ -> () end; - begin match optinvert with - Some x -> push (negate_eq x) accu_ineq | _ -> () end) - table; - !accu_eq,!accu_ineq - -exception SOLVED_SYSTEM - -let select_variable system = - let table = Hashtbl.create 7 in - let push v c= - try let r = Hashtbl.find table v in r := max !r (abs c) - with Not_found -> Hashtbl.add table v (ref (abs c)) in - List.iter (fun {body=l} -> List.iter (fun f -> push f.v f.c) l) system; - let vmin,cmin = ref (-1), ref 0 in - let var_cpt = ref 0 in - Hashtbl.iter - (fun v ({contents = c}) -> - incr var_cpt; - if c < !cmin or !vmin = (-1) then begin vmin := v; cmin := c end) - table; - if !var_cpt < 1 then raise SOLVED_SYSTEM; - !vmin - -let classify v system = - List.fold_left - (fun (not_occ,below,over) eq -> - try let f,eq' = chop_var v eq.body in - if f.c >= 0 then (not_occ,((f.c,eq) :: below),over) - else (not_occ,below,((-f.c,eq) :: over)) - with CHOPVAR -> (eq::not_occ,below,over)) - ([],[],[]) system - -let product new_eq_id dark_shadow low high = - List.fold_left - (fun accu (a,eq1) -> - List.fold_left - (fun accu (b,eq2) -> - let eq = - sum_afine new_eq_id (map_eq_afine (fun c -> c * b) eq1) - (map_eq_afine (fun c -> c * a) eq2) in - add_event(SUM(eq.id,(b,eq1),(a,eq2))); - match normalize eq with - | [eq] -> - let final_eq = - if dark_shadow then - let delta = (a - 1) * (b - 1) in - add_event(WEAKEN(eq.id,delta)); - {id = eq.id; kind=INEQ; body = eq.body; - constant = eq.constant - delta} - else eq - in final_eq :: accu - | (e::_) -> failwith "Product dardk" - | [] -> accu) - accu high) - [] low - -let fourier_motzkin (_,new_eq_id,print_var) dark_shadow system = - let v = select_variable system in - let (ineq_out, ineq_low,ineq_high) = classify v system in - let expanded = ineq_out @ product new_eq_id dark_shadow ineq_low ineq_high in - if !debug then display_system print_var expanded; expanded - -let simplify ((new_eq_id,new_var_id,print_var) as new_ids) dark_shadow system = - if List.exists (fun e -> e.kind = DISE) system then - failwith "disequation in simplify"; - clear_history (); - List.iter (fun e -> add_event (HYP e)) system; - let system = flat_map normalize system in - let eqs,ineqs = filter (fun e -> e.kind=EQUA) system in - let simp_eq,simp_ineq = redundancy_elimination new_eq_id ineqs in - let system = (eqs @ simp_eq,simp_ineq) in - let rec loop1a system = - let sys_ineq = banerjee new_ids system in - loop1b sys_ineq - and loop1b sys_ineq = - let simp_eq,simp_ineq = redundancy_elimination new_eq_id sys_ineq in - if simp_eq = [] then simp_ineq else loop1a (simp_eq,simp_ineq) - in - let rec loop2 system = - try - let expanded = fourier_motzkin new_ids dark_shadow system in - loop2 (loop1b expanded) - with SOLVED_SYSTEM -> - if !debug then display_system print_var system; system - in - loop2 (loop1a system) - -let rec depend relie_on accu = function - | act :: l -> - begin match act with - | DIVIDE_AND_APPROX (e,_,_,_) -> - if List.mem e.id relie_on then depend relie_on (act::accu) l - else depend relie_on accu l - | EXACT_DIVIDE (e,_) -> - if List.mem e.id relie_on then depend relie_on (act::accu) l - else depend relie_on accu l - | WEAKEN (e,_) -> - if List.mem e relie_on then depend relie_on (act::accu) l - else depend relie_on accu l - | SUM (e,(_,e1),(_,e2)) -> - if List.mem e relie_on then - depend (e1.id::e2.id::relie_on) (act::accu) l - else - depend relie_on accu l - | STATE {st_new_eq=e} -> - if List.mem e.id relie_on then depend relie_on (act::accu) l - else depend relie_on accu l - | HYP e -> - if List.mem e.id relie_on then depend relie_on (act::accu) l - else depend relie_on accu l - | FORGET_C _ -> depend relie_on accu l - | FORGET _ -> depend relie_on accu l - | FORGET_I _ -> depend relie_on accu l - | MERGE_EQ (e,e1,e2) -> - if List.mem e relie_on then - depend (e1.id::e2::relie_on) (act::accu) l - else - depend relie_on accu l - | NOT_EXACT_DIVIDE (e,_) -> depend (e.id::relie_on) (act::accu) l - | CONTRADICTION (e1,e2) -> - depend (e1.id::e2.id::relie_on) (act::accu) l - | CONSTANT_NOT_NUL (e,_) -> depend (e::relie_on) (act::accu) l - | CONSTANT_NEG (e,_) -> depend (e::relie_on) (act::accu) l - | CONSTANT_NUL e -> depend (e::relie_on) (act::accu) l - | NEGATE_CONTRADICT (e1,e2,_) -> - depend (e1.id::e2.id::relie_on) (act::accu) l - | SPLIT_INEQ _ -> failwith "depend" - end - | [] -> relie_on, accu - -(* -let depend relie_on accu trace = - Printf.printf "Longueur de la trace initiale : %d\n" - (trace_length trace + trace_length accu); - let rel',trace' = depend relie_on accu trace in - Printf.printf "Longueur de la trace simplifiée : %d\n" (trace_length trace'); - rel',trace' -*) - -let solve (new_eq_id,new_eq_var,print_var) system = - try let _ = simplify new_eq_id false system in failwith "no contradiction" - with UNSOLVABLE -> display_action print_var (snd (depend [] [] (history ()))) - -let negation (eqs,ineqs) = - let diseq,_ = filter (fun e -> e.kind = DISE) ineqs in - let normal = function - | ({body=f::_} as e) when f.c < 0 -> negate_eq e, INVERTED - | e -> e,NORMAL in - let table = Hashtbl.create 7 in - List.iter (fun e -> - let {body=ne;constant=c} ,kind = normal e in - Hashtbl.add table (ne,c) (kind,e)) diseq; - List.iter (fun e -> - if e.kind <> EQUA then pp 9999; - let {body=ne;constant=c},kind = normal e in - try - let (kind',e') = Hashtbl.find table (ne,c) in - add_event (NEGATE_CONTRADICT (e,e',kind=kind')); - raise UNSOLVABLE - with Not_found -> ()) eqs - -exception FULL_SOLUTION of action list * int list - -let simplify_strong ((new_eq_id,new_var_id,print_var) as new_ids) system = - clear_history (); - List.iter (fun e -> add_event (HYP e)) system; - (* Initial simplification phase *) - let rec loop1a system = - negation system; - let sys_ineq = banerjee new_ids system in - loop1b sys_ineq - and loop1b sys_ineq = - let dise,ine = filter (fun e -> e.kind = DISE) sys_ineq in - let simp_eq,simp_ineq = redundancy_elimination new_eq_id ine in - if simp_eq = [] then dise @ simp_ineq - else loop1a (simp_eq,dise @ simp_ineq) - in - let rec loop2 system = - try - let expanded = fourier_motzkin new_ids false system in - loop2 (loop1b expanded) - with SOLVED_SYSTEM -> if !debug then display_system print_var system; system - in - let rec explode_diseq = function - | (de::diseq,ineqs,expl_map) -> - let id1 = new_eq_id () - and id2 = new_eq_id () in - let e1 = - {id = id1; kind=INEQ; body = de.body; constant = de.constant - 1} in - let e2 = - {id = id2; kind=INEQ; body = map_eq_linear (fun x -> -x) de.body; - constant = - de.constant - 1} in - let new_sys = - List.map (fun (what,sys) -> ((de.id,id1,true)::what, e1::sys)) - ineqs @ - List.map (fun (what,sys) -> ((de.id,id2,false)::what,e2::sys)) - ineqs - in - explode_diseq (diseq,new_sys,(de.id,(de,id1,id2))::expl_map) - | ([],ineqs,expl_map) -> ineqs,expl_map - in - try - let system = flat_map normalize system in - let eqs,ineqs = filter (fun e -> e.kind=EQUA) system in - let dise,ine = filter (fun e -> e.kind = DISE) ineqs in - let simp_eq,simp_ineq = redundancy_elimination new_eq_id ine in - let system = (eqs @ simp_eq,simp_ineq @ dise) in - let system' = loop1a system in - let diseq,ineq = filter (fun e -> e.kind = DISE) system' in - let first_segment = history () in - let sys_exploded,explode_map = explode_diseq (diseq,[[],ineq],[]) in - let all_solutions = - List.map - (fun (decomp,sys) -> - clear_history (); - try let _ = loop2 sys in raise NO_CONTRADICTION - with UNSOLVABLE -> - let relie_on,path = depend [] [] (history ()) in - let dc,_ = filter (fun (_,id,_) -> List.mem id relie_on) decomp in - let red = List.map (fun (x,_,_) -> x) dc in - (red,relie_on,decomp,path)) - sys_exploded - in - let max_count sys = - let tbl = Hashtbl.create 7 in - let augment x = - try incr (Hashtbl.find tbl x) - with Not_found -> Hashtbl.add tbl x (ref 1) in - let eq = ref (-1) and c = ref 0 in - List.iter (function - | ([],r_on,_,path) -> raise (FULL_SOLUTION (path,r_on)) - | (l,_,_,_) -> List.iter augment l) sys; - Hashtbl.iter (fun x v -> if !v > !c then begin eq := x; c := !v end) tbl; - !eq - in - let rec solve systems = - try - let id = max_count systems in - let rec sign = function - | ((id',_,b)::l) -> if id=id' then b else sign l - | [] -> failwith "solve" in - let s1,s2 = filter (fun (_,_,decomp,_) -> sign decomp) systems in - let s1' = - List.map (fun (dep,ro,dc,pa) -> (Util.list_except id dep,ro,dc,pa)) s1 in - let s2' = - List.map (fun (dep,ro,dc,pa) -> (Util.list_except id dep,ro,dc,pa)) s2 in - let (r1,relie1) = solve s1' - and (r2,relie2) = solve s2' in - let (eq,id1,id2) = List.assoc id explode_map in - [SPLIT_INEQ(eq,(id1,r1),(id2, r2))], eq.id :: Util.list_union relie1 relie2 - with FULL_SOLUTION (x0,x1) -> (x0,x1) - in - let act,relie_on = solve all_solutions in - snd(depend relie_on act first_segment) - with UNSOLVABLE -> snd (depend [] [] (history ())) diff --git a/contrib/romega/refl_omega.ml b/contrib/romega/refl_omega.ml index ef68c587..285fc0ca 100644 --- a/contrib/romega/refl_omega.ml +++ b/contrib/romega/refl_omega.ml @@ -7,7 +7,8 @@ *************************************************************************) open Const_omega - +module OmegaSolver = Omega.MakeOmegaSolver (Bigint) +open OmegaSolver (* \section{Useful functions and flags} *) (* Especially useful debugging functions *) @@ -25,7 +26,7 @@ let (>>) = Tacticals.tclTHEN let list_index t = let rec loop i = function - | (u::l) -> if u = t then i else loop (i+1) l + | (u::l) -> if u = t then i else loop (succ i) l | [] -> raise Not_found in loop 0 @@ -101,7 +102,7 @@ type occurence = {o_hyp : Names.identifier; o_path : occ_path} (* \subsection{refiable formulas} *) type oformula = (* integer *) - | Oint of int + | Oint of Bigint.bigint (* recognized binary and unary operations *) | Oplus of oformula * oformula | Omult of oformula * oformula @@ -139,7 +140,7 @@ and oequation = { 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: Omega2.afine (* la fonction normalisée *) + e_omega: afine (* la fonction normalisée *) } (* \subsection{Proof context} @@ -172,7 +173,7 @@ type environment = { type solution = { s_index : int; s_equa_deps : int list; - s_trace : Omega2.action list } + s_trace : action list } (* Arbre de solution résolvant complètement un ensemble de systèmes *) type solution_tree = @@ -203,8 +204,8 @@ let new_environment () = { } (* Génération d'un nom d'équation *) -let new_eq_id env = - env.cnt_connectors <- env.cnt_connectors + 1; env.cnt_connectors +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 @@ -215,21 +216,36 @@ 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" + [] -> Printf.printf " ===============================\n\n" | t :: l -> - Printf.printf "(%c%02d) : " c i; - Pp.ppnl (Printer.prterm t); + Printf.printf " (%c%02d) := " c i; + Pp.ppnl (Printer.pr_lconstr t); Pp.flush_all (); - loop c (i+1) l in - Printf.printf "PROPOSITIONS :\n\n"; loop 'P' 0 env.props; - Printf.printf "TERMES :\n\n"; loop 'V' 0 env.terms + 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_id = let cpt = ref 0 in function () -> incr cpt; !cpt + +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_id i = Printf.sprintf "O%d" i + +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) *) @@ -237,12 +253,12 @@ let display_omega_id i = Printf.sprintf "O%d" i let intern_omega env t = begin try List.assoc t env.om_vars with Not_found -> - let v = new_omega_id () in + 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 Omega. Cas ou la - variable est crée par Omega et ou il faut la lier après coup a un atome +(* 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 @@ -281,7 +297,7 @@ 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.Omega2.id in + let id = e.e_omega.id in try let _ = Hashtbl.find env.equations id in () with Not_found -> Hashtbl.add env.equations id e @@ -292,7 +308,7 @@ let get_equation env id = (* Affichage des termes réifiés *) let rec oprint ch = function - | Oint n -> Printf.fprintf ch "%d" n + | 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 @@ -304,7 +320,7 @@ let rec pprint ch = function Pequa (_,{ e_comp=comp; e_left=t1; e_right=t2 }) -> let connector = match comp with - Eq -> "=" | Leq -> "=<" | Geq -> ">=" + Eq -> "=" | Leq -> "<=" | Geq -> ">=" | Gt -> ">" | Lt -> "<" | Neq -> "!=" in Printf.fprintf ch "%a %s %a" oprint t1 connector oprint t2 | Ptrue -> Printf.fprintf ch "TT" @@ -331,12 +347,12 @@ let rec weight env = function let omega_of_oformula env kind = let rec loop accu = function | Oplus(Omult(v,Oint n),r) -> - loop ({Omega2.v=intern_omega env v; Omega2.c=n} :: accu) r + loop ({v=intern_omega env v; c=n} :: accu) r | Oint n -> - let id = new_omega_id () in + let id = new_omega_eq () in (*i tag_equation name id; i*) - {Omega2.kind = kind; Omega2.body = List.rev accu; - Omega2.constant = n; Omega2.id = id} + {kind = kind; body = List.rev accu; + constant = n; id = id} | t -> print_string "CO"; oprint stdout t; failwith "compile_equation" in loop [] @@ -351,10 +367,10 @@ let reified_of_atom env i = let rec oformula_of_omega env af = let rec loop = function - | ({Omega2.v=v; Omega2.c=n}::r) -> + | ({v=v; c=n}::r) -> Oplus(Omult(unintern_omega env v,Oint n),loop r) - | [] -> Oint af.Omega2.constant in - loop af.Omega2.body + | [] -> Oint af.constant in + loop af.body let app f v = mkApp(Lazy.force f,v) @@ -429,7 +445,7 @@ let reified_of_proposition env f = let reified_of_omega env body constant = let coeff_constant = app coq_t_int [| mk_Z constant |] in - let mk_coeff {Omega2.c=c; Omega2.v=v} t = + let mk_coeff {c=c; v=v} t = let coef = app coq_t_mult [| reified_of_formula env (unintern_omega env v); @@ -441,7 +457,7 @@ let reified_of_omega env body c = begin try reified_of_omega env body c with e -> - Omega2.display_eq display_omega_id (body,c); raise e + display_eq display_omega_var (body,c); raise e end (* \section{Opérations sur les équations} @@ -475,7 +491,7 @@ let rec scalar n = function 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(-n)) + 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) -> @@ -496,12 +512,12 @@ let rec negate = function | 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 (-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(-1)) - | Oint i -> do_list [Lazy.force coq_c_reduce] ,Oint(-i) + 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" @@ -511,10 +527,10 @@ let rec norm l = (List.length l) (* \subsubsection{Version avec coefficients} *) let rec shuffle_path k1 e1 k2 e2 = let rec loop = function - (({Omega2.c=c1;Omega2.v=v1}::l1) as l1'), - (({Omega2.c=c2;Omega2.v=v2}::l2) as l2') -> + (({c=c1;v=v1}::l1) as l1'), + (({c=c2;v=v2}::l2) as l2') -> if v1 = v2 then - if k1*c1 + k2 * c2 = 0 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) ) @@ -522,9 +538,9 @@ let rec shuffle_path k1 e1 k2 e2 = Lazy.force coq_f_left :: loop(l1,l2')) else ( Lazy.force coq_f_right :: loop(l1',l2)) - | ({Omega2.c=c1;Omega2.v=v1}::l1), [] -> + | ({c=c1;v=v1}::l1), [] -> Lazy.force coq_f_left :: loop(l1,[]) - | [],({Omega2.c=c2;Omega2.v=v2}::l2) -> + | [],({c=c2;v=v2}::l2) -> Lazy.force coq_f_right :: loop([],l2) | [],[] -> flush stdout; [] in mk_shuffle_list (loop (e1,e2)) @@ -543,7 +559,7 @@ let rec shuffle env (t1,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_sym], Oplus(t2,t1) + 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 @@ -553,7 +569,7 @@ let rec shuffle env (t1,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_sym], Oplus(t2,t1) + do_list [Lazy.force coq_c_plus_comm], Oplus(t2,t1) else do_list [],Oplus(t1,t2) (* \subsection{Fusion avec réduction} *) @@ -561,11 +577,11 @@ let rec shuffle env (t1,t2) = let shrink_pair f1 f2 = begin match f1,f2 with Oatom v,Oatom _ -> - Lazy.force coq_c_red1, Omult(Oatom v,Oint 2) + 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 1)) + 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 1)) + 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 -> @@ -577,7 +593,7 @@ let shrink_pair f1 f2 = let reduce_factor = function Oatom v -> - let r = Omult(Oatom v,Oint 1) in + 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) -> @@ -588,7 +604,7 @@ let reduce_factor = function [Lazy.force coq_c_reduce], Omult(Oatom v,Oint(compute c)) | t -> Util.error "reduce_factor.1" -(* \subsection{Réordonancement} *) +(* \subsection{Réordonnancement} *) let rec condense env = function Oplus(f1,(Oplus(f2,r) as t)) -> @@ -602,7 +618,7 @@ let rec condense env = function let tac',t' = condense env t in [do_both (do_list tac) (do_list tac')], Oplus(f,t') end - | (Oplus(f1,Oint n) as t) -> + | Oplus(f1,Oint n) -> let tac,f1' = reduce_factor f1 in [do_left (do_list tac)],Oplus(f1',Oint n) | Oplus(f1,f2) -> @@ -618,13 +634,13 @@ let rec condense env = function | (Oint _ as t)-> [],t | t -> let tac,t' = reduce_factor t in - let final = Oplus(t',Oint 0) 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 0),r) -> + 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) -> @@ -652,7 +668,7 @@ let rec reduce env = function 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_sym; tac] + t', do_list [do_both trace1 trace2; Lazy.force coq_c_mult_comm; tac] | _ -> Oufo t, Lazy.force coq_c_nop end | Oopp t -> @@ -681,25 +697,36 @@ let normalize_equation env (negated,depends,origin,path) (oper,t1,t2) = 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)) Omega2.EQUA - | Neq -> mk_step t1 t2 (fun o1 o2 -> Oplus (o1,Oopp o2)) Omega2.DISE - | Leq -> mk_step t1 t2 (fun o1 o2 -> Oplus (o2,Oopp o1)) Omega2.INEQ - | Geq -> mk_step t1 t2 (fun o1 o2 -> Oplus (o1,Oopp o2)) Omega2.INEQ + | 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 (-1)),Oopp o1)) - Omega2.INEQ + 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 (-1)),Oopp o2)) - Omega2.INEQ + 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 is_scalar t = + let rec aux t = match destructurate t with + | Kapp(("Zplus"|"Zminus"|"Zmult"),[t1;t2]) -> aux t1 & aux t2 + | Kapp(("Zopp"|"Zsucc"),[t]) -> aux t + | Kapp(("Zpos"|"Zneg"|"Z0"),_) -> let _ = recognize_number t in true + | _ -> false in + try aux t with _ -> false + let rec oformula_of_constr env t = try match destructurate t with | Kapp("Zplus",[t1;t2]) -> binop env (fun x y -> Oplus(x,y)) t1 t2 - | Kapp("Zminus",[t1;t2]) ->binop env (fun x y -> Ominus(x,y)) t1 t2 - | Kapp("Zmult",[t1;t2]) ->binop env (fun x y -> Omult(x,y)) t1 t2 + | Kapp("Zminus",[t1;t2]) -> binop env (fun x y -> Ominus(x,y)) t1 t2 + | Kapp("Zmult",[t1;t2]) when is_scalar t1 or is_scalar t2 -> + binop env (fun x y -> Omult(x,y)) t1 t2 + | Kapp("Zopp",[t]) -> Oopp(oformula_of_constr env t) + | Kapp("Zsucc",[t]) -> Oplus(oformula_of_constr env t, Oint one) | Kapp(("Zpos"|"Zneg"|"Z0"),_) -> begin try Oint(recognize_number t) with _ -> Oatom (add_reified_atom t env) end @@ -715,7 +742,7 @@ and binop env c t1 t2 = and binprop env (neg2,depends,origin,path) add_to_depends neg1 gl c t1 t2 = - let i = new_eq_id env in + 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 @@ -775,13 +802,14 @@ let reify_gl env gl = let t_concl = Pnot (oproposition_of_constr env (true,[],id_concl,[O_mono]) gl concl) in if !debug then begin - Printf.printf "CONCL: "; pprint stdout t_concl; Printf.printf "\n" + 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); + Printf.printf " %s: " (Names.string_of_id i); pprint stdout t'; Printf.printf "\n" end; @@ -859,11 +887,11 @@ let display_depend = function let display_systems syst_list = let display_omega om_e = - Printf.printf "%d : %a %s 0\n" - om_e.Omega2.id - (fun _ -> Omega2.display_eq display_omega_id) - (om_e.Omega2.body, om_e.Omega2.constant) - (Omega2.operator_of_eq om_e.Omega2.kind) in + 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 (); @@ -874,12 +902,12 @@ let display_systems syst_list = (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" + 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 "false") in + (if oformula_eq.e_negated then "yes" else "no") in let display_system syst = - Printf.printf "=SYSTEME==================================\n"; + Printf.printf "=SYSTEM===================================\n"; List.iter display_equation syst in List.iter display_system syst_list @@ -889,8 +917,8 @@ let display_systems syst_list = let rec hyps_used_in_trace = function | act :: l -> begin match act with - | Omega2.HYP e -> e.Omega2.id :: hyps_used_in_trace l - | Omega2.SPLIT_INEQ (_,(_,act1),(_,act2)) -> + | 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 @@ -903,11 +931,11 @@ let rec hyps_used_in_trace = function let rec variable_stated_in_trace = function | act :: l -> begin match act with - | Omega2.STATE action -> + | STATE action -> (*i nlle_equa: afine, def: afine, eq_orig: afine, i*) (*i coef: int, var:int i*) action :: variable_stated_in_trace l - | Omega2.SPLIT_INEQ (_,(_,act1),(_,act2)) -> + | SPLIT_INEQ (_,(_,act1),(_,act2)) -> variable_stated_in_trace act1 @ variable_stated_in_trace act2 | _ -> variable_stated_in_trace l end @@ -922,10 +950,10 @@ 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 = - List.sort (fun x y -> x.Omega2.st_var - y.Omega2.st_var) (loop tree) in + List.sort (fun x y -> Pervasives.(-) x.st_var y.st_var) (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.Omega2.st_def in + 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 @@ -936,8 +964,8 @@ let add_stated_equations env tree = * 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.Omega2.st_var; - (v, term_to_generalize,term_to_reify,st.Omega2.st_def.Omega2.id) in + 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 @@ -950,7 +978,7 @@ let rec get_eclatement env = function | [] -> [] let select_smaller l = - let comp (_,x) (_,y) = List.length x - List.length y in + 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 = @@ -968,11 +996,15 @@ let rec equas_of_solution_tree = function | Leaf s -> s.s_equa_deps +(* Because of really_useful_prop, decidable formulas such as Pfalse + and Ptrue are moved to Pprop, thus breaking the decidability check + in ReflOmegaCore.concl_to_hyp... *) + let really_useful_prop l_equa c = let rec real_of = function Pequa(t,_) -> t - | Ptrue -> app coq_true [||] - | Pfalse -> app coq_false [||] + | 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|] @@ -982,7 +1014,7 @@ let really_useful_prop l_equa c = let rec loop c = match c with Pequa(_,e) -> - if List.mem e.e_omega.Omega2.id l_equa then Some c else None + if List.mem e.e_omega.id l_equa then Some c else None | Ptrue -> None | Pfalse -> None | Pnot t1 -> @@ -1041,9 +1073,9 @@ let find_path {o_hyp=id;o_path=p} env = 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 (i+1) l + | None -> loop_id (succ i) l end - | _ :: l -> loop_id (i+1) l + | _ :: l -> loop_id (succ i) l | [] -> failwith "find_path" in loop_id 0 env @@ -1062,59 +1094,59 @@ let get_hyp env_hyp i = let replay_history env env_hyp = let rec loop env_hyp t = match t with - | Omega2.CONTRADICTION (e1,e2) :: l -> - let trace = mk_nat (List.length e1.Omega2.body) in + | 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.Omega2.id); - mk_nat (get_hyp env_hyp e2.Omega2.id) |]) - | Omega2.DIVIDE_AND_APPROX (e1,e2,k,d) :: l -> + [| 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, [| mk_Z k; mk_Z d; - reified_of_omega env e2.Omega2.body e2.Omega2.constant; - mk_nat (List.length e2.Omega2.body); - loop env_hyp l; mk_nat (get_hyp env_hyp e1.Omega2.id) |]) - | Omega2.NOT_EXACT_DIVIDE (e1,k) :: l -> - let e2_constant = Omega2.floor_div e1.Omega2.constant k in - let d = e1.Omega2.constant - e2_constant * k in - let e2_body = Omega2.map_eq_linear (fun c -> c / k) e1.Omega2.body in + 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, [|mk_Z k; mk_Z d; reified_of_omega env e2_body e2_constant; mk_nat (List.length e2_body); - mk_nat (get_hyp env_hyp e1.Omega2.id)|]) - | Omega2.EXACT_DIVIDE (e1,k) :: l -> + mk_nat (get_hyp env_hyp e1.id)|]) + | EXACT_DIVIDE (e1,k) :: l -> let e2_body = - Omega2.map_eq_linear (fun c -> c / k) e1.Omega2.body in - let e2_constant = Omega2.floor_div e1.Omega2.constant k in + 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, [|mk_Z 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.Omega2.id)|]) - | (Omega2.MERGE_EQ(e3,e1,e2)) :: l -> - let n1 = get_hyp env_hyp e1.Omega2.id and n2 = get_hyp env_hyp e2 in + 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.Omega2.body); + [| mk_nat (List.length e1.body); mk_nat n1; mk_nat n2; loop (CCEqua e3:: env_hyp) l |]) - | Omega2.SUM(e3,(k1,e1),(k2,e2)) :: l -> - let n1 = get_hyp env_hyp e1.Omega2.id - and n2 = get_hyp env_hyp e2.Omega2.id in - let trace = shuffle_path k1 e1.Omega2.body k2 e2.Omega2.body in + | 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, [| mk_Z k1; mk_nat n1; mk_Z k2; mk_nat n2; trace; (loop (CCEqua e3 :: env_hyp) l) |]) - | Omega2.CONSTANT_NOT_NUL(e,k) :: l -> + | CONSTANT_NOT_NUL(e,k) :: l -> mkApp (Lazy.force coq_s_constant_not_nul, [| mk_nat (get_hyp env_hyp e) |]) - | Omega2.CONSTANT_NEG(e,k) :: l -> + | CONSTANT_NEG(e,k) :: l -> mkApp (Lazy.force coq_s_constant_neg, [| mk_nat (get_hyp env_hyp e) |]) - | Omega2.STATE {Omega2.st_new_eq=new_eq; Omega2.st_def =def; - Omega2.st_orig=orig; Omega2.st_coef=m; - Omega2.st_var=sigma } :: l -> - let n1 = get_hyp env_hyp orig.Omega2.id - and n2 = get_hyp env_hyp def.Omega2.id in + | 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 @@ -1123,24 +1155,24 @@ let replay_history env env_hyp = let trace,_ = normalize_linear_term env body in mkApp (Lazy.force coq_s_state, [| mk_Z m; trace; mk_nat n1; mk_nat n2; - loop (CCEqua new_eq.Omega2.id :: env_hyp) l |]) - | Omega2.HYP _ :: l -> loop env_hyp l - | Omega2.CONSTANT_NUL e :: l -> + 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) |]) - | Omega2.NEGATE_CONTRADICT(e1,e2,b) :: l -> + | NEGATE_CONTRADICT(e1,e2,b) :: l -> mkApp (Lazy.force coq_s_negate_contradict, - [| mk_nat (get_hyp env_hyp e1.Omega2.id); - mk_nat (get_hyp env_hyp e2.Omega2.id) |]) - | Omega2.SPLIT_INEQ(e,(e1,l1),(e2,l2)) :: l -> - let i = get_hyp env_hyp e.Omega2.id in + [| 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.Omega2.body); mk_nat i; r1 ; r2 |]) - | (Omega2.FORGET_C _ | Omega2.FORGET _ | Omega2.FORGET_I _) :: l -> + [| mk_nat (List.length e.body); mk_nat i; r1 ; r2 |]) + | (FORGET_C _ | FORGET _ | FORGET_I _) :: l -> loop env_hyp l - | (Omega2.WEAKEN _ ) :: l -> failwith "not_treated" + | (WEAKEN _ ) :: l -> failwith "not_treated" | [] -> failwith "no contradiction" in loop env_hyp @@ -1171,7 +1203,7 @@ and decompose_tree_hyps trace env ctxt = function 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.Omega2.id :: ctxt) l in + (CCEqua equation.e_omega.id :: ctxt) l in app coq_e_extract [|mk_nat index; mk_direction_list full_path; cont |] @@ -1190,15 +1222,15 @@ let resolution env full_reified_goal systems_list = let index = !num in let system = List.map (fun eq -> eq.e_omega) list_eq in let trace = - Omega2.simplify_strong - ((fun () -> new_eq_id env),new_omega_id,display_omega_id) + 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; - Omega2.display_action display_omega_id trace; + display_action display_omega_var trace; print_string "\n Depend :"; List.iter (fun i -> Printf.printf " %d" i) vars; print_string "\n Split points :"; @@ -1236,7 +1268,7 @@ let resolution env full_reified_goal systems_list = let rec loop i = function var :: l -> let t = get_reified_atom env var in - Hashtbl.add env.real_indices var i; t :: loop (i+1) l + 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 coq_Z) basic_env in @@ -1262,7 +1294,7 @@ let resolution env full_reified_goal systems_list = (l_reified_stated @ l_reified_terms) in let reified = app coq_interp_sequent - [| env_props_reified;env_terms_reified;reified_concl;reified_goal |] in + [| 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) @@ -1286,20 +1318,26 @@ let resolution env full_reified_goal systems_list = Tactics.change_in_concl None reified >> Tactics.apply (app coq_do_omega [|decompose_tactic; normalization_trace|]) >> show_goal >> - Tactics.normalise_in_concl >> + 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 = - if !Options.v7 then Util.error "ROmega does not work in v7 mode"; + 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 begin - display_systems systems_list - end; + if !debug then display_systems systems_list; resolution env full_reified_goal systems_list gl - with Omega2.NO_CONTRADICTION -> Util.error "ROmega can't solve this system" + with NO_CONTRADICTION -> Util.error "ROmega can't solve this system" (*i let tester = Tacmach.hide_atomic_tactic "TestOmega" test_tactic i*) |