portage Omega (mais toujours pas Zpower et Zlogarithm)

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

13 files changed, 64 insertions, 67 deletions

diff --git a/.depend.coq b/.depend.coq
index 244665111..f8ba1f558 100644
--- a/.depend.coq
+++ b/.depend.coq
@@ -50,6 +50,11 @@ theories/Arith/Between.vo: theories/Arith/Between.v theories/Arith/Le.vo theorie
 theories/Arith/Arith.vo: theories/Arith/Arith.v theories/Arith/Le.vo theories/Arith/Lt.vo theories/Arith/Plus.vo theories/Arith/Gt.vo theories/Arith/Minus.vo theories/Arith/Mult.vo theories/Arith/Between.vo parsing/g_natsyntax.cmo
 test-suite/bench/lists_100.vo: test-suite/bench/lists_100.v
 test-suite/bench/lists-100.vo: test-suite/bench/lists-100.v
+contrib/omega/Zpower.vo: contrib/omega/Zpower.v contrib/omega/Omega.vo contrib/omega/Zcomplements.vo
+contrib/omega/Zlogarithm.vo: contrib/omega/Zlogarithm.v contrib/omega/Omega.vo contrib/omega/Zcomplements.vo contrib/omega/Zpower.vo
+contrib/omega/Zcomplements.vo: contrib/omega/Zcomplements.v contrib/omega/Omega.vo theories/Arith/Wf_nat.vo
+contrib/omega/OmegaSyntax.vo: contrib/omega/OmegaSyntax.v
+contrib/omega/Omega.vo: contrib/omega/Omega.v theories/Zarith/ZArith.vo theories/Arith/Minus.vo contrib/omega/omega.cmo contrib/omega/coq_omega.cmo contrib/omega/OmegaSyntax.vo
 tactics/Tauto.vo: tactics/Tauto.v
 tactics/Inv.vo: tactics/Inv.v tactics/Equality.vo
 tactics/Equality.vo: tactics/Equality.v
diff --git a/Makefile b/Makefile
index 1b97acbde..67626527a 100644
--- a/Makefile
+++ b/Makefile
@@ -129,7 +129,7 @@ CMX=$(CMO:.cmo=.cmx) $(ARITHSYNTAX:.cmo=.cmx)
 COQMKTOP=scripts/coqmktop
 COQC=scripts/coqc
 
-world: $(COQMKTOP) $(COQC) coqtop.byte coqtop.opt states theories tools
+world: $(COQMKTOP) $(COQC) coqtop.byte coqtop.opt states theories contrib tools
 
 coqtop.opt: $(COQMKTOP) $(CMX)
 	$(COQMKTOP) -opt -notactics $(OPTFLAGS) -o coqtop.opt
diff --git a/contrib/omega/Omega.v b/contrib/omega/Omega.v
index 185a85969..13a764253 100755
--- a/contrib/omega/Omega.v
+++ b/contrib/omega/Omega.v
@@ -6,6 +6,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
+(* $Id$ *)
+
 Require Export ZArith.
 (* The constant minus is required in coq_omega.ml *)
 Require Export Minus.
diff --git a/contrib/omega/OmegaSyntax.v b/contrib/omega/OmegaSyntax.v
index dccfc5e89..4028a1efb 100644
--- a/contrib/omega/OmegaSyntax.v
+++ b/contrib/omega/OmegaSyntax.v
@@ -6,6 +6,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
+(* $Id$ *)
+
 Grammar vernac vernac :=
   omega_sett [ "Set" "Omega" "Time" "." ] -> [(OmegaFlag "+time")]
 | omega_sets [ "Set" "Omega" "System" "." ] -> [(OmegaFlag "+system")]
diff --git a/contrib/omega/Zcomplements.v b/contrib/omega/Zcomplements.v
index 6bf081781..1cbf284a5 100644
--- a/contrib/omega/Zcomplements.v
+++ b/contrib/omega/Zcomplements.v
@@ -1,18 +1,7 @@
-(****************************************************************************)
-(*                 The Calculus of Inductive Constructions                  *)
-(*                                                                          *)
-(*                                Projet Coq                                *)
-(*                                                                          *)
-(*                     INRIA        LRI-CNRS        ENS-CNRS                *)
-(*              Rocquencourt         Orsay          Lyon                    *)
-(*                                                                          *)
-(*                                 Coq V6.3                                 *)
-(*                               July 1st 1999                              *)
-(*                                                                          *)
-(****************************************************************************)
-(*                              Zcomplements.v                              *)
-(****************************************************************************)
 
+(* $Id$ *)
+
+Require ZArith.
 Require Omega.
 Require Wf_nat.
 
@@ -95,7 +84,7 @@ Simpl; Do 2 Rewrite Zmult_n_1; Auto 1.
 Unfold Zs.
 Intros x0 Hx0; Repeat (Rewrite Zmult_plus_distr_r).
 Repeat Rewrite Zmult_n_1.
-Auto with zarith.
+Omega.
 Unfold Zpred; Omega.
 Save.
 
@@ -308,6 +297,3 @@ Destruct a;
 Save.
 
 End diveucl.
-
-(* $Id$ *)
-
diff --git a/contrib/omega/Zlogarithm.v b/contrib/omega/Zlogarithm.v
index 87f1f87c5..c5b36397f 100644
--- a/contrib/omega/Zlogarithm.v
+++ b/contrib/omega/Zlogarithm.v
@@ -1,17 +1,5 @@
-(****************************************************************************)
-(*                 The Calculus of Inductive Constructions                  *)
-(*                                                                          *)
-(*                                Projet Coq                                *)
-(*                                                                          *)
-(*                     INRIA        LRI-CNRS        ENS-CNRS                *)
-(*              Rocquencourt         Orsay          Lyon                    *)
-(*                                                                          *)
-(*                                 Coq V6.3                                 *)
-(*                               July 1st 1999                              *)
-(*                                                                          *)
-(****************************************************************************)
-(*                              Zlogarithm.v                                *)
-(****************************************************************************)
+
+(* $Id$ *)
 
 (****************************************************************************)
 (*  The integer logarithms with base 2. There are three logarithms,	    *)
diff --git a/contrib/omega/Zpower.v b/contrib/omega/Zpower.v
index 475638ce2..d56e607d5 100644
--- a/contrib/omega/Zpower.v
+++ b/contrib/omega/Zpower.v
@@ -1,18 +1,7 @@
-(****************************************************************************)
-(*                 The Calculus of Inductive Constructions                  *)
-(*                                                                          *)
-(*                                Projet Coq                                *)
-(*                                                                          *)
-(*                     INRIA        LRI-CNRS        ENS-CNRS                *)
-(*              Rocquencourt         Orsay          Lyon                    *)
-(*                                                                          *)
-(*                                 Coq V6.3                                 *)
-(*                               July 1st 1999                              *)
-(*                                                                          *)
-(****************************************************************************)
-(*                                  Zpower.v                                *)
-(****************************************************************************)
 
+(* $Id$ *)
+
+Require ZArith.
 Require Omega.
 Require Zcomplements.
 
@@ -82,7 +71,7 @@ Hints Unfold  Zpower_nat : zarith.
 
 Lemma Zpower_exp : (x:Z)(n,m:Z)
   `n >= 0` -> `m >= 0` -> `(Zpower x (n+m))=(Zpower x n)*(Zpower x m)`.
-Destruct n;  Destruct m; Auto with zarith.
+Destruct n; Destruct m; Auto with zarith.
 Simpl; Intros; Apply Zred_factor0.
 Simpl; Auto with zarith.
 Intros; Compute in H0; Absurd INFERIEUR=INFERIEUR; Auto with zarith.
@@ -392,5 +381,3 @@ Apply Zdiv_rest_proof with q:=y0 r:=y1; Assumption.
 Save.
 
 End power_div_with_rest.
-
-
diff --git a/parsing/lexer.mll b/parsing/lexer.mll
index 0f7b4938c..847b9a8fa 100644
--- a/parsing/lexer.mll
+++ b/parsing/lexer.mll
@@ -120,7 +120,7 @@ let identchar =
   ['$' 'A'-'Z' 'a'-'z' '_' '\192'-'\214' '\216'-'\246' '\248'-'\255' 
    '\'' '0'-'9']
 let symbolchar =
-  ['!' '$' '%' '&' '*' '+' '-' '<' '>' '/' '\\' ':' ',' ';' '=' '?' '@' '^'
+  ['!' '$' '%' '&' '*' '+' '-' '<' '>' '/' '\\' ':' ',' '=' '?' '@' '^'
    '|' '~' '#']
 let decimal_literal = ['0'-'9']+
 let hex_literal = '0' ['x' 'X'] ['0'-'9' 'A'-'F' 'a'-'f']+
@@ -135,15 +135,15 @@ rule token = parse
 	if is_keyword s then ("",s) else ("IDENT",s) }
   | decimal_literal | hex_literal | oct_literal | bin_literal
       { ("INT", Lexing.lexeme lexbuf) }
-  | "(" | ")" | "[" | "]" | "{" | "}" | "." | "_" 
+  | "(" | ")" | "[" | "]" | "{" | "}" | "." | "_" | ";" | "`" | "->"
       { ("", Lexing.lexeme lexbuf) }
-  | "->"
-      { ("", "->") }
   | symbolchar+
       { ("", Lexing.lexeme lexbuf) }
+  (***
   | '`' [^'`']* '`'
       { let s = Lexing.lexeme lexbuf in
 	("QUOTED", String.sub s 1 (String.length s - 2)) }
+  ***)
   | "\""
       { Buffer.reset string_buffer;
         let string_start = Lexing.lexeme_start lexbuf in
@@ -261,12 +261,12 @@ let token_text = function
   | (con, prm) -> con ^ " \"" ^ prm ^ "\""
 
 let tparse (p_con, p_prm) =
-  ifdef CAMLP4_300 then 
-    None
-  else
+  None
+  (*i etait en ocaml 2.xx :
     if p_prm = "" then
       parser [< '(con, prm) when con = p_con >] -> prm
     else
       parser [< '(con, prm) when con = p_con && prm = p_prm >] -> prm
+  i*)
 
 }
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index b0880065a..9191522dc 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -78,6 +78,7 @@ let pf_interp_type gls c =
   Astterm.interp_type evc (sig_it gls).evar_env c
 
 let pf_global gls id = Declare.construct_reference (sig_it gls).evar_env CCI id
+
 let pf_parse_const gls = compose (pf_global gls) id_of_string
 
 let pf_execute gls =
diff --git a/theories/Bool/Bool.v b/theories/Bool/Bool.v
index 7f8f52c4f..ab1a4b9e0 100755
--- a/theories/Bool/Bool.v
+++ b/theories/Bool/Bool.v
@@ -106,6 +106,7 @@ Lemma Is_true_eq_true2 : (x:bool)  x=true -> (Is_true x).
 Destruct x; Simpl; Auto with bool.
 Save.
 
+(***** TODO
 Lemma eqb_subst : 
   (P:bool->Prop)(b1,b2:bool)(eqb b1 b2)=true->(P b1)->(P b2).
 Unfold eqb .
@@ -121,7 +122,8 @@ Intros H.
 Inversion_clear H.
 Trivial with bool.
 Save.
- 
+*****)
+
 Lemma eqb_reflx : (b:bool)(eqb b b)=true.
 Intro b.
 Case b.
diff --git a/theories/Zarith/Wf_Z.v b/theories/Zarith/Wf_Z.v
index 389db702c..6b015c77f 100644
--- a/theories/Zarith/Wf_Z.v
+++ b/theories/Zarith/Wf_Z.v
@@ -25,7 +25,7 @@ Require Zsyntax.
   Then the  diagram will be closed and the theorem proved. *)
 
 Lemma inject_nat_complete :
-  (x:Z)`0 <= x` -> (Ex [n:nat](x=(inject_nat n))).
+  (x:Z)`0 <= x` -> (EX n:nat | x=(inject_nat n)).
 Destruct x; Intros;
 [ Exists  O; Auto with arith
 | Specialize (ZL4 p); Intros Hp; Elim Hp; Intros;
diff --git a/theories/Zarith/Zmisc.v b/theories/Zarith/Zmisc.v
index 888d2fb81..28c4cf208 100644
--- a/theories/Zarith/Zmisc.v
+++ b/theories/Zarith/Zmisc.v
@@ -207,28 +207,52 @@ Definition Zodd_bool :=
 
 Lemma Zeven_odd_dec : (z:Z) { (Zeven z) }+{ (Zodd z) }.
 Proof.
+  Intro z. Case z;
+  [ Left; Compute; Trivial
+  | Intro p; Case p; Intros; 
+    (Right; Compute; Exact I) Orelse (Left; Compute; Exact I)
+  | Intro p; Case p; Intros; 
+    (Right; Compute; Exact I) Orelse (Left; Compute; Exact I) ].
+  (*** was 
   Realizer Zeven_bool.
   Repeat Program; Compute; Trivial.
+  ***)
 Save.
 
 Lemma Zeven_dec : (z:Z) { (Zeven z) }+{ ~(Zeven z) }.
 Proof.
+  Intro z. Case z;
+  [ Left; Compute; Trivial
+  | Intro p; Case p; Intros; 
+    (Left; Compute; Exact I) Orelse (Right; Compute; Trivial) 
+  | Intro p; Case p; Intros; 
+    (Left; Compute; Exact I) Orelse (Right; Compute; Trivial) ].
+  (*** was 
   Realizer Zeven_bool.
   Repeat Program; Compute; Trivial.
+  ***)
 Save.
 
 Lemma Zodd_dec : (z:Z) { (Zodd z) }+{ ~(Zodd z) }.
 Proof.
+  Intro z. Case z;
+  [ Right; Compute; Trivial
+  | Intro p; Case p; Intros; 
+    (Left; Compute; Exact I) Orelse (Right; Compute; Trivial) 
+  | Intro p; Case p; Intros; 
+    (Left; Compute; Exact I) Orelse (Right; Compute; Trivial) ].
+  (*** was 
   Realizer Zodd_bool.
   Repeat Program; Compute; Trivial.
+  ***)
 Save.
 
-Lemma Zeven_not_Zodd : (z:Z)(Zeven z)->~(Zodd z).
+Lemma Zeven_not_Zodd : (z:Z)(Zeven z) -> ~(Zodd z).
 Proof.
   Destruct z; [ Idtac | Destruct p | Destruct p  ]; Compute; Trivial.
 Save.
 
-Lemma Zodd_not_Zeven : (z:Z)(Zodd z)->~(Zeven z).
+Lemma Zodd_not_Zeven : (z:Z)(Zodd z) -> ~(Zeven z).
 Proof.
   Destruct z; [ Idtac | Destruct p | Destruct p  ]; Compute; Trivial.
 Save.
@@ -320,7 +344,7 @@ Apply rename with x:=`x ?= y`; Intro r; Elim r;
 Save.
 
 Lemma Zcompare_x_x : (x:Z) `x ?= x` = EGAL.
-(Intro; Apply Case (Zcompare_EGAL x x) of [h1,h2:?]h2 end).
+(Intro; Apply Case (Zcompare_EGAL x x) of [h1,h2: ?]h2 end).
 Apply refl_equal.
 Save.
 
@@ -339,7 +363,7 @@ Save.
 Lemma Zcompare_eq_case : 
   (c1,c2,c3:Prop)(x,y:Z) c1 -> x=y -> (Case `x ?= y` of c1 c2 c3 end).
 Intros.
-Rewrite -> (Case (Zcompare_EGAL x y) of [h1,h2:?]h2 end H0).
+Rewrite -> (Case (Zcompare_EGAL x y) of [h1,h2: ?]h2 end H0).
 Assumption.
 Save.
 
diff --git a/theories/Zarith/Zsyntax.v b/theories/Zarith/Zsyntax.v
index 0fb1e6b72..350bcaa18 100644
--- a/theories/Zarith/Zsyntax.v
+++ b/theories/Zarith/Zsyntax.v
@@ -34,8 +34,8 @@ with formula :=
               -> [<<(Zlt $p $c)/\(Zle $c $c1)>>]
 | form_lt_lt [ expr($p) "<" expr($c) "<" expr($c1) ]
               -> [<<(Zlt $p $c)/\(Zlt $c $c1)>>]
-| form_neq  [ expr($p) "<>" expr($c) ] -> [<<~(eq Z $p $c)>>]
-| form_comp [ expr($p) "?" "=" expr($c) ] -> [<<(Zcompare $p $c)>>]
+| form_neq  [ expr($p) "<>" expr($c) ] -> [<< ~(eq Z $p $c)>>]
+| form_comp [ expr($p) "?=" expr($c) ] -> [<<(Zcompare $p $c)>>]
 
 with expr :=
   expr_plus [ expr($p) "+" expr($c) ] -> [<<(Zplus $p $c)>>]
@@ -60,7 +60,7 @@ with expr0 :=
 
 with application :=
   apply [ application($p) expr($c1) ] -> [<<($p $c1)>>]
-| pair [ expr($p) "," expr($c) ] -> [<<($p,$c)>>]
+| pair [ expr($p) "," expr($c) ] -> [<<($p, $c)>>]
 | appl0 [ expr($a) ] -> [$a]
 .
 
@@ -99,7 +99,7 @@ Syntax constr
       [[<hov 0> "`" (ZEXPR $n1) [1 0] "?= " (ZEXPR $n2) "`" ]]
   | Zeq [<<(eq Z $n1 $n2)>>] -> 
       [[<hov 0> "`" (ZEXPR $n1) [1 0] "= "(ZEXPR $n2)"`"]]
-  | Zneq [<<~(eq Z $n1 $n2)>>] ->
+  | Zneq [<< ~(eq Z $n1 $n2)>>] ->
       [[<hov 0> "`" (ZEXPR $n1) [1 0] "<> "(ZEXPR $n2) "`"]]
   | Zle_Zle [<<(Zle $n1 $n2)/\(Zle $n2 $n3)>>] ->
       [[<hov 0> "`" (ZEXPR $n1) [1 0] "<= " (ZEXPR $n2)