Romega

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2014 85f007b7-540e-0410-9357-904b9bb8a0f7

4 files changed, 65 insertions, 4 deletions

diff --git a/contrib/romega/ReflOmegaCore.v b/contrib/romega/ReflOmegaCore.v
index 9a4b299b40..41e29d38e2 100644
--- a/contrib/romega/ReflOmegaCore.v
+++ b/contrib/romega/ReflOmegaCore.v
@@ -339,7 +339,7 @@ Fixpoint interp_hyps [env : (list Z); l: hyps] : Prop :=
    | (cons p' l') => (interp_proposition env p') /\ (interp_hyps env l')
   end.
 
-(* \paragraph{ous forme de but}
+(* \paragraph{Sous forme de but}
    C'est cette interpétation que l'on utilise sur le but (car on utilise
    [Generalize] et qu'une conjonction est forcément lourde (répétition des
    types dans les conjonctions intermédiaires) *)
@@ -394,7 +394,7 @@ Definition valid2 [f: proposition -> proposition -> proposition] :=
       (interp_proposition e (f p1 p2)).
 
 (* Dans cette notion de validité, la fonction prend directement une 
-   liste de propositions et rend une nouvelle liste de proposition. 
+   liste de propositions et rend une nouvelle liste de propositions. 
    On reste contravariant *)
 
 Definition valid_hyps [f: hyps -> hyps] :=
@@ -411,7 +411,7 @@ Intros; Apply goal_to_hyps; Intro H1; Apply (hyps_to_goal env (a l) H0);
 Apply H; Assumption.
 Save.
 
-(* \subsubsection{Généralisation a des listes de buts (disjonctions)} *)
+(* \subsubsection{Généralisation à des listes de buts (disjonctions)} *)
 
 Syntactic Definition lhyps := (list hyps).
 
@@ -1427,6 +1427,30 @@ Definition negate_contradict [i1,i2:nat; h:hyps]:=
   | _ => h
   end.
 
+Definition negate_contradict_inv [t:nat; i1,i2:nat; h:hyps]:=
+  Cases (nth_hyps i1 h) of
+    (EqTerm (Tint ZERO) b1) =>
+	Cases (nth_hyps i2 h) of
+           (NeqTerm (Tint ZERO) b2) =>
+              Cases (eq_term b1 (scalar_norm t (Tmult b2 (Tint `-1`)))) of
+	         true => absurd
+              |  false => h
+	    end
+        | _ => h
+        end
+  | (NeqTerm (Tint ZERO) b1) =>
+	Cases (nth_hyps i2 h) of
+           (EqTerm (Tint ZERO) b2) =>
+              Cases (eq_term b1 (scalar_norm t (Tmult b2 (Tint `-1`)))) of
+	         true => absurd
+              |  false => h
+	    end
+        | _ => h
+        end
+  | _ => h
+  end.
+
+
 Theorem negate_contradict_valid :
   (i,j:nat) (valid_hyps (negate_contradict i j)).
 
@@ -1441,6 +1465,31 @@ Auto; Simpl; Intros H1 H2; [
 
 Save.
 
+Theorem negate_contradict_inv_valid :
+  (t,i,j:nat) (valid_hyps (negate_contradict_inv t i j)).
+
+
+Unfold valid_hyps negate_contradict_inv; Intros t i j e l H;
+Generalize (nth_valid ? i ? H); Generalize (nth_valid ? j ? H);
+Case (nth_hyps i l); Auto; Intros t1 t2; Case t1; Auto; Intros z; Case z; Auto;
+Case (nth_hyps j l); Auto; Intros t3 t4; Case t3; Auto; Intros z'; Case z'; 
+Auto; Simpl; Intros H1 H2;
+(Pattern (eq_term t2 (scalar_norm t (Tmult t4 (Tint (NEG xH))))); Apply bool_ind2; Intro Aux; [
+  Generalize (eq_term_true t2 (scalar_norm t (Tmult t4 (Tint (NEG xH)))) Aux);
+  Clear Aux
+| Generalize (eq_term_false t2 (scalar_norm t (Tmult t4 (Tint (NEG xH)))) Aux);
+  Clear Aux ]); [
+   Intro H3; Elim H1; Generalize H2; Rewrite H3; 
+   Rewrite <- (scalar_norm_stable t e); Simpl; Elim (interp_term e t4) ; 
+   Simpl; Auto; Intros p H4; Discriminate H4
+ | Auto 
+ | Intro H3; Elim H2; Rewrite H3; Elim (scalar_norm_stable t e); Simpl;
+   Elim H1; Simpl; Trivial
+ | Auto ].
+
+Save.
+
+
 (* \subsubsection{Tactiques générant une nouvelle équation} *)
 (* \paragraph{[O_SUM]}
  C'est une oper2 valide mais elle traite plusieurs cas à la fois (suivant
@@ -1726,6 +1775,7 @@ Inductive t_omega : Set :=
  | O_SPLIT_INEQ : nat -> nat -> t_omega -> t_omega -> t_omega
  | O_CONSTANT_NUL : nat -> t_omega 
  | O_NEGATE_CONTRADICT : nat -> nat -> t_omega
+ | O_NEGATE_CONTRADICT_INV : nat -> nat -> nat -> t_omega
  | O_STATE : Z -> step -> nat -> nat -> t_omega -> t_omega.
 
 Syntactic Definition singleton :=  [a: hyps] (cons a (nil hyps)).
@@ -1751,6 +1801,7 @@ Fixpoint execute_omega [t: t_omega] : hyps -> lhyps :=
        (split_ineq i t (execute_omega cont1) (execute_omega cont2) l)
    | (O_CONSTANT_NUL i) => (singleton (constant_nul i l))
    | (O_NEGATE_CONTRADICT i j) =>  (singleton (negate_contradict i j l))
+   | (O_NEGATE_CONTRADICT_INV t i j) => (singleton (negate_contradict_inv t i j l))
    | (O_STATE m s i1 i2 cont) =>
        (execute_omega cont (apply_oper_2 i1 i2 (state m s) l))
   end.
@@ -1789,6 +1840,8 @@ Induction t; Simpl; [
   Apply (constant_nul_valid i e lp H)
 | Unfold valid_list_hyps; Simpl; Intros i j e lp H; Left; 
   Apply (negate_contradict_valid i j e lp H)
+| Unfold valid_list_hyps; Simpl; Intros n i j e lp H; Left; 
+  Apply (negate_contradict_inv_valid n i j e lp H)
 | Unfold valid_list_hyps valid_hyps; Intros m s i1 i2 t' Ht' e lp H; Apply Ht';
   Apply (apply_oper_2_valid i1 i2 (state m s) (state_valid m s) e lp H)
 ].
diff --git a/contrib/romega/const_omega.ml b/contrib/romega/const_omega.ml
index 9d7330a940..37fb01a4c6 100644
--- a/contrib/romega/const_omega.ml
+++ b/contrib/romega/const_omega.ml
@@ -184,6 +184,7 @@ 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")
 
 (* \subsection{Construction d'expressions} *)
 
diff --git a/contrib/romega/refl_omega.ml b/contrib/romega/refl_omega.ml
index f92e77e8b3..791a2fafa0 100644
--- a/contrib/romega/refl_omega.ml
+++ b/contrib/romega/refl_omega.ml
@@ -490,9 +490,16 @@ let replay_history env_hyp =
 	  mkApp (Lazy.force coq_s_constant_nul, 
 		 [|  mk_nat (get_hyp env_hyp e) |])
       |	Omega.NEGATE_CONTRADICT(e1,e2,b) :: l ->
+	  if b then
 	  mkApp (Lazy.force coq_s_negate_contradict, 
 		 [|  mk_nat (get_hyp env_hyp e1.Omega.id);
 		     mk_nat (get_hyp env_hyp e2.Omega.id) |])
+	  else
+	    mkApp (Lazy.force coq_s_negate_contradict_inv, 
+		   [|  mk_nat (List.length e1.Omega.body);
+                       mk_nat (get_hyp env_hyp e1.Omega.id);
+                       mk_nat (get_hyp env_hyp e2.Omega.id) |])
+
       | Omega.SPLIT_INEQ(e,(e1,l1),(e2,l2)) :: l ->
 	  let i =  get_hyp env_hyp e.Omega.id in
 	  let r1 = loop (e1 :: env_hyp) l1 in
diff --git a/kernel/names.ml b/kernel/names.ml
index b79a526083..b3a4ccba51 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -106,7 +106,7 @@ let check_ident_suffix i l s =
     let c = String.get s i in
     if not (is_letter c or is_digit c or c = '\'' or c = '_' or c = '@') then
       error
-	("Character "^(String.sub s i 1)^" is not allowed in an identifier")
+	("Character "^(String.sub s i 1)^" is not allowed in identifier "^s)
   done
 
 let check_ident s =