diff options
58 files changed, 1266 insertions, 1140 deletions
diff --git a/Makefile.checker b/Makefile.checker index 5c55ccf489..90c73a496d 100644 --- a/Makefile.checker +++ b/Makefile.checker @@ -43,7 +43,7 @@ checker/check.cmxa $(LIBCOQRUN) checker/coqchk.mli checker/coqchk.ml $(CODESIGN_HIDE) $@ else $(CHICKEN): $(CHICKENBYTE) - cp $< $@ + rm -f $@ && cp $< $@ endif $(CHICKENBYTE): config/config.cma clib/clib.cma lib/lib.cma kernel/kernel.cma \ diff --git a/Makefile.ide b/Makefile.ide index 39c6c8ad1e..bd72494289 100644 --- a/Makefile.ide +++ b/Makefile.ide @@ -110,7 +110,7 @@ $(COQIDE): $(LINKIDEOPT) $(STRIP_HIDE) $@ else $(COQIDE): $(COQIDEBYTE) - cp $< $@ + rm -f $@ && cp $< $@ endif $(COQIDEBYTE): $(LINKIDE) @@ -119,9 +119,7 @@ $(COQIDEBYTE): $(LINKIDE) -linkpkg -package str,unix,dynlink,threads,lablgtk3-sourceview3 $(IDEFLAGS) $(IDECDEPSFLAGS) $^ ide/coqide_os_specific.ml: ide/coqide_$(IDEINT).ml.in config/Makefile - @rm -f $@ - cp $< $@ - @chmod a-w $@ + rm -f $@ && cp $< $@ && chmod a-w $@ ide/%.cmi: ide/%.mli $(SHOW)'OCAMLC $<' @@ -150,7 +148,7 @@ IDETOPCMX:=$(IDETOPCMA:.cma=.cmxa) # Special rule for coqidetop $(IDETOPEXE): $(IDETOP:.opt=.$(BEST)) - cp $< $@ + rm -f $@ && cp $< $@ $(IDETOP): ide/idetop.ml $(LINKCMX) $(LIBCOQRUN) $(IDETOPCMX) $(SHOW)'COQMKTOP -o $@' diff --git a/doc/changelog/02-specification-language/10985-about-arguments.rst b/doc/changelog/02-specification-language/10985-about-arguments.rst new file mode 100644 index 0000000000..1e05b0b0fe --- /dev/null +++ b/doc/changelog/02-specification-language/10985-about-arguments.rst @@ -0,0 +1,5 @@ +- The output of the :cmd:`Print` and :cmd:`About` commands has + changed. Arguments meta-data is now displayed as the corresponding + :cmd:`Arguments <Arguments (implicits)>` command instead of the + human-targeted prose used in previous Coq versions. (`#10985 + <https://github.com/coq/coq/pull/10985>`_, by Gaëtan Gilbert). diff --git a/doc/changelog/02-specification-language/10997-unsupport-atts-warn.rst b/doc/changelog/02-specification-language/10997-unsupport-atts-warn.rst new file mode 100644 index 0000000000..43a748b365 --- /dev/null +++ b/doc/changelog/02-specification-language/10997-unsupport-atts-warn.rst @@ -0,0 +1,3 @@ +- The unsupported attribute error is now an error-by-default warning, + meaning it can be disabled (`#10997 + <https://github.com/coq/coq/pull/10997>`_, by Gaëtan Gilbert). diff --git a/doc/changelog/03-notations/09883-numeral-notations-sorts.rst b/doc/changelog/03-notations/09883-numeral-notations-sorts.rst new file mode 100644 index 0000000000..abc5a516ae --- /dev/null +++ b/doc/changelog/03-notations/09883-numeral-notations-sorts.rst @@ -0,0 +1,4 @@ +- Numeral Notations now support sorts in the input to printing + functions (e.g., numeral notations can be defined for terms + containing things like `@cons Set nat nil`). (`#9883 + <https://github.com/coq/coq/pull/9883>`_, by Jason Gross). diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst index f477bf239d..f50cf9340c 100644 --- a/doc/sphinx/language/gallina-extensions.rst +++ b/doc/sphinx/language/gallina-extensions.rst @@ -1927,9 +1927,11 @@ Renaming implicit arguments This command is used to redefine the names of implicit arguments. -With the assert flag, ``Arguments`` can be used to assert that a given -object has the expected number of arguments and that these arguments -are named as expected. +.. cmd:: Arguments @qualid {* @name} : assert + :name: Arguments (assert) + + This command is used to assert that a given object has the expected + number of arguments and that these arguments are named as expected. .. example:: (continued) diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst index ae9d284661..dd65d4aeb3 100644 --- a/doc/sphinx/language/gallina-specification-language.rst +++ b/doc/sphinx/language/gallina-specification-language.rst @@ -1556,6 +1556,11 @@ the following attributes names are recognized: now foo. Abort. +.. warn:: Unsupported attribute + + This warning is an error by default. It is caused by using a + command with some attribute it does not understand. + .. [1] This is similar to the expression “*entry* :math:`\{` sep *entry* :math:`\}`” in standard BNF, or “*entry* :math:`(` sep *entry* diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index a28ce600ca..02910e603a 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -1442,8 +1442,8 @@ Numeral notations of the resulting term will be refreshed. Note that only fully-reduced ground terms (terms containing only - function application, constructors, inductive type families, and - primitive integers) will be considered for printing. + function application, constructors, inductive type families, + sorts, and primitive integers) will be considered for printing. .. cmdv:: Numeral Notation @ident__1 @ident__2 @ident__3 : @scope (warning after @num). @@ -1592,8 +1592,8 @@ String notations of the resulting term will be refreshed. Note that only fully-reduced ground terms (terms containing only - function application, constructors, inductive type families, and - primitive integers) will be considered for printing. + function application, constructors, inductive type families, + sorts, and primitive integers) will be considered for printing. .. exn:: Cannot interpret this string as a value of type @type diff --git a/interp/notation.ml b/interp/notation.ml index 70d3e4175e..c157cf43fb 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -503,6 +503,9 @@ let rec constr_of_glob env sigma g = match DAst.get g with let sigma,cl = List.fold_left_map (constr_of_glob env) sigma gcl in sigma,mkApp (c, Array.of_list cl) | Glob_term.GInt i -> sigma, mkInt i + | Glob_term.GSort gs -> + let sigma,c = Evd.fresh_sort_in_family sigma (Glob_ops.glob_sort_family gs) in + sigma,mkSort c | _ -> raise NotAValidPrimToken @@ -516,6 +519,10 @@ let rec glob_of_constr token_kind ?loc env sigma c = match Constr.kind c with | Ind (ind, _) -> DAst.make ?loc (Glob_term.GRef (GlobRef.IndRef ind, None)) | Var id -> DAst.make ?loc (Glob_term.GRef (GlobRef.VarRef id, None)) | Int i -> DAst.make ?loc (Glob_term.GInt i) + | Sort Sorts.SProp -> DAst.make ?loc (Glob_term.GSort (Glob_term.UNamed [Glob_term.GSProp, 0])) + | Sort Sorts.Prop -> DAst.make ?loc (Glob_term.GSort (Glob_term.UNamed [Glob_term.GProp, 0])) + | Sort Sorts.Set -> DAst.make ?loc (Glob_term.GSort (Glob_term.UNamed [Glob_term.GSet, 0])) + | Sort (Sorts.Type _) -> DAst.make ?loc (Glob_term.GSort (Glob_term.UAnonymous {rigid=true})) | _ -> Loc.raise ?loc (PrimTokenNotationError(token_kind,env,sigma,UnexpectedTerm c)) let no_such_prim_token uninterpreted_token_kind ?loc ty = diff --git a/printing/printing.mllib b/printing/printing.mllib index deb52ad270..5b5b6590a4 100644 --- a/printing/printing.mllib +++ b/printing/printing.mllib @@ -4,4 +4,3 @@ Ppconstr Proof_diffs Printer Printmod -Prettyp diff --git a/test-suite/output/Arguments.out b/test-suite/output/Arguments.out index 3c1e27ba9d..6704337f80 100644 --- a/test-suite/output/Arguments.out +++ b/test-suite/output/Arguments.out @@ -1,14 +1,14 @@ Nat.sub : nat -> nat -> nat Nat.sub is not universe polymorphic -Argument scopes are [nat_scope nat_scope] +Arguments Nat.sub _%nat_scope _%nat_scope : simpl nomatch The reduction tactics unfold Nat.sub but avoid exposing match constructs Nat.sub is transparent Expands to: Constant Coq.Init.Nat.sub Nat.sub : nat -> nat -> nat Nat.sub is not universe polymorphic -Argument scopes are [nat_scope nat_scope] +Arguments Nat.sub _%nat_scope / _%nat_scope : simpl nomatch The reduction tactics unfold Nat.sub when applied to 1 argument but avoid exposing match constructs Nat.sub is transparent @@ -16,7 +16,7 @@ Expands to: Constant Coq.Init.Nat.sub Nat.sub : nat -> nat -> nat Nat.sub is not universe polymorphic -Argument scopes are [nat_scope nat_scope] +Arguments Nat.sub !_%nat_scope / _%nat_scope : simpl nomatch The reduction tactics unfold Nat.sub when the 1st argument evaluates to a constructor and when applied to 1 argument but avoid exposing match constructs @@ -25,7 +25,7 @@ Expands to: Constant Coq.Init.Nat.sub Nat.sub : nat -> nat -> nat Nat.sub is not universe polymorphic -Argument scopes are [nat_scope nat_scope] +Arguments Nat.sub !_%nat_scope !_%nat_scope / The reduction tactics unfold Nat.sub when the 1st and 2nd arguments evaluate to a constructor and when applied to 2 arguments Nat.sub is transparent @@ -33,7 +33,7 @@ Expands to: Constant Coq.Init.Nat.sub Nat.sub : nat -> nat -> nat Nat.sub is not universe polymorphic -Argument scopes are [nat_scope nat_scope] +Arguments Nat.sub !_%nat_scope !_%nat_scope The reduction tactics unfold Nat.sub when the 1st and 2nd arguments evaluate to a constructor Nat.sub is transparent @@ -43,37 +43,34 @@ forall D1 C1 : Type, (D1 -> C1) -> forall D2 C2 : Type, (D2 -> C2) -> D1 * D2 -> C1 * C2 pf is not universe polymorphic -Arguments D2, C2 are implicit -Arguments D1, C1 are implicit and maximally inserted -Argument scopes are [foo_scope type_scope _ _ _ _ _] +Arguments pf {D1%foo_scope} {C1%type_scope} _ [D2] [C2] : simpl never The reduction tactics never unfold pf pf is transparent Expands to: Constant Arguments.pf fcomp : forall A B C : Type, (B -> C) -> (A -> B) -> A -> C fcomp is not universe polymorphic -Arguments A, B, C are implicit and maximally inserted -Argument scopes are [type_scope type_scope type_scope _ _ _] +Arguments fcomp {A%type_scope} {B%type_scope} {C%type_scope} _ _ _ / The reduction tactics unfold fcomp when applied to 6 arguments fcomp is transparent Expands to: Constant Arguments.fcomp volatile : nat -> nat volatile is not universe polymorphic -Argument scope is [nat_scope] +Arguments volatile / _%nat_scope The reduction tactics always unfold volatile volatile is transparent Expands to: Constant Arguments.volatile f : T1 -> T2 -> nat -> unit -> nat -> nat f is not universe polymorphic -Argument scopes are [_ _ nat_scope _ nat_scope] +Arguments f _ _ _%nat_scope _ _%nat_scope f is transparent Expands to: Constant Arguments.S1.S2.f f : T1 -> T2 -> nat -> unit -> nat -> nat f is not universe polymorphic -Argument scopes are [_ _ nat_scope _ nat_scope] +Arguments f _ _ !_%nat_scope !_ !_%nat_scope The reduction tactics unfold f when the 3rd, 4th and 5th arguments evaluate to a constructor f is transparent @@ -81,8 +78,7 @@ Expands to: Constant Arguments.S1.S2.f f : forall T2 : Type, T1 -> T2 -> nat -> unit -> nat -> nat f is not universe polymorphic -Argument T2 is implicit -Argument scopes are [type_scope _ _ nat_scope _ nat_scope] +Arguments f [T2%type_scope] _ _ !_%nat_scope !_ !_%nat_scope The reduction tactics unfold f when the 4th, 5th and 6th arguments evaluate to a constructor f is transparent @@ -90,8 +86,7 @@ Expands to: Constant Arguments.S1.f f : forall T1 T2 : Type, T1 -> T2 -> nat -> unit -> nat -> nat f is not universe polymorphic -Arguments T1, T2 are implicit -Argument scopes are [type_scope type_scope _ _ nat_scope _ nat_scope] +Arguments f [T1%type_scope] [T2%type_scope] _ _ !_%nat_scope !_ !_%nat_scope The reduction tactics unfold f when the 5th, 6th and 7th arguments evaluate to a constructor f is transparent @@ -103,6 +98,7 @@ Expands to: Constant Arguments.f f : forall T1 T2 : Type, T1 -> T2 -> nat -> unit -> nat -> nat f is not universe polymorphic +Arguments f _ _ _ _ !_ !_ !_ The reduction tactics unfold f when the 5th, 6th and 7th arguments evaluate to a constructor f is transparent @@ -118,7 +114,7 @@ Extra arguments: _, _. volatilematch : nat -> nat volatilematch is not universe polymorphic -Argument scope is [nat_scope] +Arguments volatilematch / _%nat_scope : simpl nomatch The reduction tactics always unfold volatilematch but avoid exposing match constructs volatilematch is transparent diff --git a/test-suite/output/ArgumentsScope.out b/test-suite/output/ArgumentsScope.out index 69ba329ff1..7b25fd40f8 100644 --- a/test-suite/output/ArgumentsScope.out +++ b/test-suite/output/ArgumentsScope.out @@ -1,29 +1,29 @@ a : bool -> bool a is not universe polymorphic -Argument scope is [bool_scope] +Arguments a _%bool_scope Expands to: Variable a b : bool -> bool b is not universe polymorphic -Argument scope is [bool_scope] +Arguments b _%bool_scope Expands to: Variable b negb'' : bool -> bool negb'' is not universe polymorphic -Argument scope is [bool_scope] +Arguments negb'' _%bool_scope negb'' is transparent Expands to: Constant ArgumentsScope.A.B.negb'' negb' : bool -> bool negb' is not universe polymorphic -Argument scope is [bool_scope] +Arguments negb' _%bool_scope negb' is transparent Expands to: Constant ArgumentsScope.A.negb' negb : bool -> bool negb is not universe polymorphic -Argument scope is [bool_scope] +Arguments negb _%bool_scope negb is transparent Expands to: Constant Coq.Init.Datatypes.negb a : bool -> bool diff --git a/test-suite/output/Arguments_renaming.out b/test-suite/output/Arguments_renaming.out index 65c902202d..53d5624f6f 100644 --- a/test-suite/output/Arguments_renaming.out +++ b/test-suite/output/Arguments_renaming.out @@ -13,36 +13,21 @@ where ?y : [ |- nat] Inductive eq (A : Type) (x : A) : A -> Prop := eq_refl : x = x -For eq_refl: Arguments are renamed to B, y -For eq: Argument A is implicit and maximally inserted -For eq_refl, when applied to no arguments: - Arguments B, y are implicit and maximally inserted -For eq_refl, when applied to 1 argument: - Argument B is implicit -For eq: Argument scopes are [type_scope _ _] -For eq_refl: Argument scopes are [type_scope _] +Arguments eq {A%type_scope} +Arguments eq_refl {B%type_scope} {y}, [B] _ eq_refl : forall (A : Type) (x : A), x = x eq_refl is not universe polymorphic -Arguments are renamed to B, y -When applied to no arguments: - Arguments B, y are implicit and maximally inserted -When applied to 1 argument: - Argument B is implicit -Argument scopes are [type_scope _] +Arguments eq_refl {B%type_scope} {y}, [B] _ Expands to: Constructor Coq.Init.Logic.eq_refl Inductive myEq (B : Type) (x : A) : A -> Prop := myrefl : B -> myEq B x x -For myrefl: Arguments are renamed to C, x, _ -For myrefl: Argument C is implicit and maximally inserted -For myEq: Argument scopes are [type_scope _ _] -For myrefl: Argument scopes are [type_scope _ _] +Arguments myEq _%type_scope +Arguments myrefl {C%type_scope} x : rename myrefl : forall (B : Type) (x : A), B -> myEq B x x myrefl is not universe polymorphic -Arguments are renamed to C, x, _ -Argument C is implicit and maximally inserted -Argument scopes are [type_scope _ _] +Arguments myrefl {C%type_scope} x : rename Expands to: Constructor Arguments_renaming.Test1.myrefl myplus = fix myplus (T : Type) (t : T) (n m : nat) {struct n} : nat := @@ -52,15 +37,11 @@ fix myplus (T : Type) (t : T) (n m : nat) {struct n} : nat := end : forall T : Type, T -> nat -> nat -> nat -Arguments are renamed to Z, t, n, m -Argument Z is implicit and maximally inserted -Argument scopes are [type_scope _ nat_scope nat_scope] +Arguments myplus {Z%type_scope} !t !n%nat_scope m%nat_scope : rename myplus : forall T : Type, T -> nat -> nat -> nat myplus is not universe polymorphic -Arguments are renamed to Z, t, n, m -Argument Z is implicit and maximally inserted -Argument scopes are [type_scope _ nat_scope nat_scope] +Arguments myplus {Z%type_scope} !t !n%nat_scope m%nat_scope : rename The reduction tactics unfold myplus when the 2nd and 3rd arguments evaluate to a constructor myplus is transparent @@ -70,16 +51,12 @@ Expands to: Constant Arguments_renaming.Test1.myplus Inductive myEq (A B : Type) (x : A) : A -> Prop := myrefl : B -> myEq A B x x -For myrefl: Arguments are renamed to A, C, x, _ -For myrefl: Argument C is implicit and maximally inserted -For myEq: Argument scopes are [type_scope type_scope _ _] -For myrefl: Argument scopes are [type_scope type_scope _ _] +Arguments myEq _%type_scope _%type_scope +Arguments myrefl A%type_scope {C%type_scope} x : rename myrefl : forall (A B : Type) (x : A), B -> myEq A B x x myrefl is not universe polymorphic -Arguments are renamed to A, C, x, _ -Argument C is implicit and maximally inserted -Argument scopes are [type_scope type_scope _ _] +Arguments myrefl A%type_scope {C%type_scope} x : rename Expands to: Constructor Arguments_renaming.myrefl myrefl : forall (A C : Type) (x : A), C -> myEq A C x x @@ -91,15 +68,11 @@ fix myplus (T : Type) (t : T) (n m : nat) {struct n} : nat := end : forall T : Type, T -> nat -> nat -> nat -Arguments are renamed to Z, t, n, m -Argument Z is implicit and maximally inserted -Argument scopes are [type_scope _ nat_scope nat_scope] +Arguments myplus {Z%type_scope} !t !n%nat_scope m%nat_scope : rename myplus : forall T : Type, T -> nat -> nat -> nat myplus is not universe polymorphic -Arguments are renamed to Z, t, n, m -Argument Z is implicit and maximally inserted -Argument scopes are [type_scope _ nat_scope nat_scope] +Arguments myplus {Z%type_scope} !t !n%nat_scope m%nat_scope : rename The reduction tactics unfold myplus when the 2nd and 3rd arguments evaluate to a constructor myplus is transparent diff --git a/test-suite/output/Cases.out b/test-suite/output/Cases.out index cb835ab48d..7489b8987e 100644 --- a/test-suite/output/Cases.out +++ b/test-suite/output/Cases.out @@ -7,7 +7,7 @@ fix F (t : t) : P t := : forall P : t -> Type, (let x := t in forall x0 : x, P x0 -> P (k x0)) -> forall t : t, P t -Argument scopes are [function_scope function_scope _] +Arguments t_rect _%function_scope _%function_scope = fun d : TT => match d with | {| f3 := b |} => b end @@ -26,7 +26,7 @@ match Nat.eq_dec x y with end : forall (x y : nat) (P : nat -> Type), P x -> P y -> P y -Argument scopes are [nat_scope nat_scope function_scope _ _] +Arguments proj _%nat_scope _%nat_scope _%function_scope foo = fix foo (A : Type) (l : list A) {struct l} : option A := match l with @@ -36,14 +36,14 @@ fix foo (A : Type) (l : list A) {struct l} : option A := end : forall A : Type, list A -> option A -Argument scopes are [type_scope list_scope] +Arguments foo _%type_scope _%list_scope uncast = fun (A : Type) (x : I A) => match x with | x0 <: _ => x0 end : forall A : Type, I A -> A -Argument scopes are [type_scope _] +Arguments uncast _%type_scope foo' = if A 0 then true else false : bool f = @@ -82,7 +82,7 @@ lem2 = fun dd : bool => if dd as aa return (aa = aa) then eq_refl else eq_refl : forall k : bool, k = k -Argument scope is [bool_scope] +Arguments lem2 _%bool_scope lem3 = fun dd : nat * nat => let (bb, cc) as aa return (aa = aa) := dd in eq_refl : forall k : nat * nat, k = k diff --git a/test-suite/output/Implicit.out b/test-suite/output/Implicit.out index 3b65003c29..d65d2a8f55 100644 --- a/test-suite/output/Implicit.out +++ b/test-suite/output/Implicit.out @@ -5,8 +5,7 @@ ex_intro (P:=fun _ : nat => True) (x:=0) I d2 = fun x : nat => d1 (y:=x) : forall x x0 : nat, x0 = x -> x0 = x -Arguments x, x0 are implicit -Argument scopes are [nat_scope nat_scope _] +Arguments d2 [x%nat_scope] [x0%nat_scope] map id (1 :: nil) : list nat map id' (1 :: nil) diff --git a/test-suite/output/Inductive.out b/test-suite/output/Inductive.out index af202ea01c..8ff571ae55 100644 --- a/test-suite/output/Inductive.out +++ b/test-suite/output/Inductive.out @@ -3,5 +3,5 @@ Last occurrence of "list'" must have "A" as 1st argument in "A -> list' A -> list' (A * A)%type". Inductive foo (A : Type) (x : A) (y : A := x) : Prop := Foo : foo A x -For foo: Argument scopes are [type_scope _] -For Foo: Argument scopes are [type_scope _] +Arguments foo _%type_scope +Arguments Foo _%type_scope diff --git a/test-suite/output/InitSyntax.out b/test-suite/output/InitSyntax.out index c17c63e724..ce058a6d34 100644 --- a/test-suite/output/InitSyntax.out +++ b/test-suite/output/InitSyntax.out @@ -1,11 +1,8 @@ Inductive sig2 (A : Type) (P Q : A -> Prop) : Type := exist2 : forall x : A, P x -> Q x -> {x : A | P x & Q x} -For sig2: Argument A is implicit -For exist2: Argument A is implicit -For sig2: Argument scopes are [type_scope type_scope type_scope] -For exist2: Argument scopes are [type_scope function_scope function_scope _ _ - _] +Arguments sig2 [A%type_scope] _%type_scope _%type_scope +Arguments exist2 [A%type_scope] _%function_scope _%function_scope exists x : nat, x = x : Prop fun b : bool => if b then b else b diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out index d32cf67e28..abada44da7 100644 --- a/test-suite/output/Notations3.out +++ b/test-suite/output/Notations3.out @@ -230,7 +230,7 @@ fun l : list nat => match l with end : list nat -> list nat -Argument scope is [list_scope] +Arguments foo _%list_scope Notation "'exists' x .. y , p" := ex (fun x => .. (ex (fun y => p)) ..) : type_scope (default interpretation) diff --git a/test-suite/output/NumeralNotations.out b/test-suite/output/NumeralNotations.out index 460c77879c..505dc52ebe 100644 --- a/test-suite/output/NumeralNotations.out +++ b/test-suite/output/NumeralNotations.out @@ -180,3 +180,41 @@ let v := 4%Zlike in v : Zlike : Zlike 0%Zlike : Zlike +let v := 0%kt in v : ty + : ty +let v := 1%kt in v : ty + : ty +let v := 2%kt in v : ty + : ty +let v := 3%kt in v : ty + : ty +let v := 4%kt in v : ty + : ty +let v := 5%kt in v : ty + : ty +The command has indeed failed with message: +Cannot interpret this number as a value of type ty + = 0%kt + : ty + = 1%kt + : ty + = 2%kt + : ty + = 3%kt + : ty + = 4%kt + : ty + = 5%kt + : ty +let v : ty := Build_ty Empty_set zero in v : ty + : ty +let v : ty := Build_ty unit one in v : ty + : ty +let v : ty := Build_ty bool two in v : ty + : ty +let v : ty := Build_ty Prop prop in v : ty + : ty +let v : ty := Build_ty Set set in v : ty + : ty +let v : ty := Build_ty Type type in v : ty + : ty diff --git a/test-suite/output/NumeralNotations.v b/test-suite/output/NumeralNotations.v index 44805ad09d..c306b15ef3 100644 --- a/test-suite/output/NumeralNotations.v +++ b/test-suite/output/NumeralNotations.v @@ -391,3 +391,68 @@ Module Test19. Check {| summands := (cons 1 (cons 2 (cons (-1) nil)))%Z |}. Check {| summands := nil |}. End Test19. + +Module Test20. + (** Test Sorts *) + Local Set Universe Polymorphism. + Inductive known_type : Type -> Type := + | prop : known_type Prop + | set : known_type Set + | type : known_type Type + | zero : known_type Empty_set + | one : known_type unit + | two : known_type bool. + + Existing Class known_type. + Existing Instances zero one two prop. + Existing Instance set | 2. + Existing Instance type | 4. + + Record > ty := { t : Type ; kt : known_type t }. + + Definition ty_of_uint (x : Decimal.uint) : option ty + := match Nat.of_uint x with + | 0 => @Some ty zero + | 1 => @Some ty one + | 2 => @Some ty two + | 3 => @Some ty prop + | 4 => @Some ty set + | 5 => @Some ty type + | _ => None + end. + Definition uint_of_ty (x : ty) : Decimal.uint + := Nat.to_uint match kt x with + | prop => 3 + | set => 4 + | type => 5 + | zero => 0 + | one => 1 + | two => 2 + end. + + Declare Scope kt_scope. + Delimit Scope kt_scope with kt. + + Numeral Notation ty ty_of_uint uint_of_ty : kt_scope. + + Check let v := 0%kt in v : ty. + Check let v := 1%kt in v : ty. + Check let v := 2%kt in v : ty. + Check let v := 3%kt in v : ty. + Check let v := 4%kt in v : ty. + Check let v := 5%kt in v : ty. + Fail Check let v := 6%kt in v : ty. + Eval cbv in (_ : known_type Empty_set) : ty. + Eval cbv in (_ : known_type unit) : ty. + Eval cbv in (_ : known_type bool) : ty. + Eval cbv in (_ : known_type Prop) : ty. + Eval cbv in (_ : known_type Set) : ty. + Eval cbv in (_ : known_type Type) : ty. + Local Set Printing All. + Check let v := 0%kt in v : ty. + Check let v := 1%kt in v : ty. + Check let v := 2%kt in v : ty. + Check let v := 3%kt in v : ty. + Check let v := 4%kt in v : ty. + Check let v := 5%kt in v : ty. +End Test20. diff --git a/test-suite/output/PatternsInBinders.out b/test-suite/output/PatternsInBinders.out index 8a6d94c732..2952b6d94b 100644 --- a/test-suite/output/PatternsInBinders.out +++ b/test-suite/output/PatternsInBinders.out @@ -15,8 +15,7 @@ swap = fun (A B : Type) '(x, y) => (y, x) : forall A B : Type, A * B -> B * A -Arguments A, B are implicit and maximally inserted -Argument scopes are [type_scope type_scope _] +Arguments swap {A%type_scope} {B%type_scope} fun (A B : Type) '(x, y) => swap (x, y) = (y, x) : forall A B : Type, A * B -> Prop forall (A B : Type) '(x, y), swap (x, y) = (y, x) @@ -42,6 +41,6 @@ fun (pat : nat) '(x, y) => x + y = pat f = fun x : nat => x + x : nat -> nat -Argument scope is [nat_scope] +Arguments f _%nat_scope fun x : nat => x + x : nat -> nat diff --git a/test-suite/output/PrintInfos.out b/test-suite/output/PrintInfos.out index e788977fb7..7d0d81a3e8 100644 --- a/test-suite/output/PrintInfos.out +++ b/test-suite/output/PrintInfos.out @@ -1,36 +1,24 @@ existT : forall (A : Type) (P : A -> Type) (x : A), P x -> {x : A & P x} existT is template universe polymorphic on sigT.u0 sigT.u1 -Argument A is implicit -Argument scopes are [type_scope function_scope _ _] +Arguments existT [A%type_scope] _%function_scope Expands to: Constructor Coq.Init.Specif.existT Inductive sigT (A : Type) (P : A -> Type) : Type := existT : forall x : A, P x -> {x : A & P x} -For sigT: Argument A is implicit -For existT: Argument A is implicit -For sigT: Argument scopes are [type_scope type_scope] -For existT: Argument scopes are [type_scope function_scope _ _] +Arguments sigT [A%type_scope] _%type_scope +Arguments existT [A%type_scope] _%function_scope existT : forall (A : Type) (P : A -> Type) (x : A), P x -> {x : A & P x} Argument A is implicit Inductive eq (A : Type) (x : A) : A -> Prop := eq_refl : x = x -For eq: Argument A is implicit and maximally inserted -For eq_refl, when applied to no arguments: - Arguments A, x are implicit and maximally inserted -For eq_refl, when applied to 1 argument: - Argument A is implicit -For eq: Argument scopes are [type_scope _ _] -For eq_refl: Argument scopes are [type_scope _] +Arguments eq {A%type_scope} +Arguments eq_refl {A%type_scope} {x}, [A] _ eq_refl : forall (A : Type) (x : A), x = x eq_refl is not universe polymorphic -When applied to no arguments: - Arguments A, x are implicit and maximally inserted -When applied to 1 argument: - Argument A is implicit -Argument scopes are [type_scope _] +Arguments eq_refl {A%type_scope} {x}, [A] _ Expands to: Constructor Coq.Init.Logic.eq_refl eq_refl : forall (A : Type) (x : A), x = x @@ -46,11 +34,11 @@ fix add (n m : nat) {struct n} : nat := end : nat -> nat -> nat -Argument scopes are [nat_scope nat_scope] +Arguments Nat.add _%nat_scope _%nat_scope Nat.add : nat -> nat -> nat Nat.add is not universe polymorphic -Argument scopes are [nat_scope nat_scope] +Arguments Nat.add _%nat_scope _%nat_scope Nat.add is transparent Expands to: Constant Coq.Init.Nat.add Nat.add : nat -> nat -> nat @@ -58,17 +46,15 @@ Nat.add : nat -> nat -> nat plus_n_O : forall n : nat, n = n + 0 plus_n_O is not universe polymorphic -Argument scope is [nat_scope] +Arguments plus_n_O _%nat_scope plus_n_O is opaque Expands to: Constant Coq.Init.Peano.plus_n_O Inductive le (n : nat) : nat -> Prop := le_n : n <= n | le_S : forall m : nat, n <= m -> n <= S m -For le_S: Argument m is implicit -For le_S: Argument n is implicit and maximally inserted -For le: Argument scopes are [nat_scope nat_scope] -For le_n: Argument scope is [nat_scope] -For le_S: Argument scopes are [nat_scope nat_scope _] +Arguments le _%nat_scope _%nat_scope +Arguments le_n _%nat_scope +Arguments le_S {n%nat_scope} [m%nat_scope] comparison : Set comparison is not universe polymorphic @@ -81,26 +67,21 @@ bar is not universe polymorphic Expanded type for implicit arguments bar : forall x : nat, x = 0 -Argument x is implicit and maximally inserted +Arguments bar {x} Expands to: Constant PrintInfos.bar *** [ bar : foo ] Expanded type for implicit arguments bar : forall x : nat, x = 0 -Argument x is implicit and maximally inserted +Arguments bar {x} Module Coq.Init.Peano Notation sym_eq := eq_sym Expands to: Notation Coq.Init.Logic.sym_eq Inductive eq (A : Type) (x : A) : A -> Prop := eq_refl : x = x -For eq: Argument A is implicit and maximally inserted -For eq_refl, when applied to no arguments: - Arguments A, x are implicit and maximally inserted -For eq_refl, when applied to 1 argument: - Argument A is implicit and maximally inserted -For eq: Argument scopes are [type_scope _ _] -For eq_refl: Argument scopes are [type_scope _] +Arguments eq {A%type_scope} +Arguments eq_refl {A%type_scope} {x}, {A} _ n:nat Hypothesis of the goal context. diff --git a/test-suite/output/StringSyntax.out b/test-suite/output/StringSyntax.out index 9366113c0c..e9cf4282dc 100644 --- a/test-suite/output/StringSyntax.out +++ b/test-suite/output/StringSyntax.out @@ -433,7 +433,7 @@ end P "167" -> P "168" -> P "169" -> P "170" -> P "171" -> P "172" -> P "173" -> P "174" -> P "175" -> P "176" -> P "177" -> P "178" -> P "179" -> P "180" -> P "181" -> P "182" -> P "183" -> P "184" -> P "185" -> P "186" -> P "187" -> P "188" -> P "189" -> P "190" -> P "191" -> P "192" -> P "193" -> P "194" -> P "195" -> P "196" -> P "197" -> P "198" -> P "199" -> P "200" -> P "201" -> P "202" -> P "203" -> P "204" -> P "205" -> P "206" -> P "207" -> P "208" -> P "209" -> P "210" -> P "211" -> P "212" -> P "213" -> P "214" -> P "215" -> P "216" -> P "217" -> P "218" -> P "219" -> P "220" -> P "221" -> P "222" -> P "223" -> P "224" -> P "225" -> P "226" -> P "227" -> P "228" -> P "229" -> P "230" -> P "231" -> P "232" -> P "233" -> P "234" -> P "235" -> P "236" -> P "237" -> P "238" -> P "239" -> P "240" -> P "241" -> P "242" -> P "243" -> P "244" -> P "245" -> P "246" -> P "247" -> P "248" -> P "249" -> P "250" -> P "251" -> P "252" -> P "253" -> P "254" -> P "255" -> forall b : byte, P b -Argument scopes are [function_scope _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ byte_scope] +Arguments byte_rect _%function_scope _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _%byte_scope byte_rec = fun P : byte -> Set => byte_rect P : forall P : byte -> Set, @@ -607,7 +607,7 @@ fun P : byte -> Set => byte_rect P P "167" -> P "168" -> P "169" -> P "170" -> P "171" -> P "172" -> P "173" -> P "174" -> P "175" -> P "176" -> P "177" -> P "178" -> P "179" -> P "180" -> P "181" -> P "182" -> P "183" -> P "184" -> P "185" -> P "186" -> P "187" -> P "188" -> P "189" -> P "190" -> P "191" -> P "192" -> P "193" -> P "194" -> P "195" -> P "196" -> P "197" -> P "198" -> P "199" -> P "200" -> P "201" -> P "202" -> P "203" -> P "204" -> P "205" -> P "206" -> P "207" -> P "208" -> P "209" -> P "210" -> P "211" -> P "212" -> P "213" -> P "214" -> P "215" -> P "216" -> P "217" -> P "218" -> P "219" -> P "220" -> P "221" -> P "222" -> P "223" -> P "224" -> P "225" -> P "226" -> P "227" -> P "228" -> P "229" -> P "230" -> P "231" -> P "232" -> P "233" -> P "234" -> P "235" -> P "236" -> P "237" -> P "238" -> P "239" -> P "240" -> P "241" -> P "242" -> P "243" -> P "244" -> P "245" -> P "246" -> P "247" -> P "248" -> P "249" -> P "250" -> P "251" -> P "252" -> P "253" -> P "254" -> P "255" -> forall b : byte, P b -Argument scopes are [function_scope _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ byte_scope] +Arguments byte_rec _%function_scope _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _%byte_scope byte_ind = fun (P : byte -> Prop) (f : P "000") (f0 : P "001") (f1 : P "002") (f2 : P "003") (f3 : P "004") (f4 : P "005") (f5 : P "006") (f6 : P "007") (f7 : P "008") (f8 : P "009") (f9 : P "010") (f10 : P "011") (f11 : P "012") (f12 : P "013") (f13 : P "014") (f14 : P "015") (f15 : P "016") (f16 : P "017") (f17 : P "018") (f18 : P "019") (f19 : P "020") (f20 : P "021") (f21 : P "022") (f22 : P "023") (f23 : P "024") (f24 : P "025") (f25 : P "026") (f26 : P "027") (f27 : P "028") (f28 : P "029") (f29 : P "030") (f30 : P "031") (f31 : P " ") (f32 : P "!") (f33 : P """") (f34 : P "#") (f35 : P "$") (f36 : P "%") (f37 : P "&") (f38 : P "'") (f39 : P "(") (f40 : P ")") (f41 : P "*") (f42 : P "+") (f43 : P ",") (f44 : P "-") (f45 : P ".") (f46 : P "/") (f47 : P "0") (f48 : P "1") (f49 : P "2") (f50 : P "3") (f51 : P "4") (f52 : P "5") (f53 : P "6") (f54 : P "7") (f55 : P "8") (f56 : P "9") (f57 : P ":") (f58 : P ";") (f59 : P "<") (f60 : P "=") (f61 : P ">") (f62 : P "?") (f63 : P "@") (f64 : P "A") (f65 : P "B") (f66 : P "C") (f67 : P "D") (f68 : P "E") (f69 : P "F") (f70 : P "G") (f71 : P "H") (f72 : P "I") (f73 : P "J") (f74 : P "K") (f75 : P "L") (f76 : P "M") (f77 : P "N") (f78 : P "O") (f79 : P "P") (f80 : P "Q") (f81 : P "R") (f82 : P "S") (f83 : P "T") (f84 : P "U") (f85 : P "V") (f86 : P "W") (f87 : P "X") (f88 : P "Y") (f89 : P "Z") (f90 : P "[") (f91 : P "\") (f92 : P "]") (f93 : P "^") (f94 : P "_") (f95 : P "`") (f96 : P "a") (f97 : P "b") (f98 : P "c") (f99 : P "d") (f100 : P "e") (f101 : P "f") (f102 : P "g") (f103 : P "h") (f104 : P "i") (f105 : P "j") (f106 : P "k") (f107 : P "l") (f108 : P "m") (f109 : P "n") (f110 : P "o") (f111 : P "p") (f112 : P "q") (f113 : P "r") (f114 : P "s") (f115 : P "t") (f116 : P "u") (f117 : P "v") (f118 : P "w") (f119 : P "x") (f120 : P "y") (f121 : P "z") (f122 : P "{") (f123 : P "|") (f124 : P "}") (f125 : P "~") (f126 : P "127") (f127 : P "128") (f128 : P "129") (f129 : P "130") @@ -1043,7 +1043,7 @@ end P "167" -> P "168" -> P "169" -> P "170" -> P "171" -> P "172" -> P "173" -> P "174" -> P "175" -> P "176" -> P "177" -> P "178" -> P "179" -> P "180" -> P "181" -> P "182" -> P "183" -> P "184" -> P "185" -> P "186" -> P "187" -> P "188" -> P "189" -> P "190" -> P "191" -> P "192" -> P "193" -> P "194" -> P "195" -> P "196" -> P "197" -> P "198" -> P "199" -> P "200" -> P "201" -> P "202" -> P "203" -> P "204" -> P "205" -> P "206" -> P "207" -> P "208" -> P "209" -> P "210" -> P "211" -> P "212" -> P "213" -> P "214" -> P "215" -> P "216" -> P "217" -> P "218" -> P "219" -> P "220" -> P "221" -> P "222" -> P "223" -> P "224" -> P "225" -> P "226" -> P "227" -> P "228" -> P "229" -> P "230" -> P "231" -> P "232" -> P "233" -> P "234" -> P "235" -> P "236" -> P "237" -> P "238" -> P "239" -> P "240" -> P "241" -> P "242" -> P "243" -> P "244" -> P "245" -> P "246" -> P "247" -> P "248" -> P "249" -> P "250" -> P "251" -> P "252" -> P "253" -> P "254" -> P "255" -> forall b : byte, P b -Argument scopes are [function_scope _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ byte_scope] +Arguments byte_ind _%function_scope _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _%byte_scope "000" : byte "a" diff --git a/test-suite/output/UnivBinders.out b/test-suite/output/UnivBinders.out index d48d8b900f..298a0789c4 100644 --- a/test-suite/output/UnivBinders.out +++ b/test-suite/output/UnivBinders.out @@ -4,37 +4,36 @@ Record PWrap (A : Type@{u}) : Type@{u} := pwrap { punwrap : A } (* u |= *) PWrap has primitive projections with eta conversion. -For PWrap: Argument scope is [type_scope] -For pwrap: Argument scopes are [type_scope _] +Arguments PWrap _%type_scope +Arguments pwrap _%type_scope punwrap@{u} = fun (A : Type@{u}) (p : PWrap@{u} A) => punwrap _ p : forall A : Type@{u}, PWrap@{u} A -> A (* u |= *) -Argument scopes are [type_scope _] +Arguments punwrap _%type_scope Record RWrap (A : Type@{u}) : Type@{u} := rwrap { runwrap : A } (* u |= *) -For RWrap: Argument scope is [type_scope] -For rwrap: Argument scopes are [type_scope _] +Arguments RWrap _%type_scope +Arguments rwrap _%type_scope runwrap@{u} = fun (A : Type@{u}) (r : RWrap@{u} A) => let (runwrap) := r in runwrap : forall A : Type@{u}, RWrap@{u} A -> A (* u |= *) -Argument scopes are [type_scope _] +Arguments runwrap _%type_scope Wrap@{u} = fun A : Type@{u} => A : Type@{u} -> Type@{u} (* u |= *) -Argument scope is [type_scope] +Arguments Wrap _%type_scope wrap@{u} = fun (A : Type@{u}) (Wrap : Wrap@{u} A) => Wrap : forall A : Type@{u}, Wrap@{u} A -> A (* u |= *) -Arguments A, Wrap are implicit and maximally inserted -Argument scopes are [type_scope _] +Arguments wrap {A%type_scope} {Wrap} bar@{u} = nat : Wrap@{u} Set (* u |= Set < u *) @@ -87,13 +86,13 @@ Record PWrap (A : Type@{E}) : Type@{E} := pwrap { punwrap : A } (* E |= *) PWrap has primitive projections with eta conversion. -For PWrap: Argument scope is [type_scope] -For pwrap: Argument scopes are [type_scope _] +Arguments PWrap _%type_scope +Arguments pwrap _%type_scope punwrap@{K} : forall A : Type@{K}, PWrap@{K} A -> A (* K |= *) punwrap is universe polymorphic -Argument scopes are [type_scope _] +Arguments punwrap _%type_scope punwrap is transparent Expands to: Constant UnivBinders.punwrap The command has indeed failed with message: @@ -118,7 +117,7 @@ Inductive insecind@{k} : Type@{k+1} := inseccstr : Type@{k} -> insecind@{k} (* k |= *) -For inseccstr: Argument scope is [type_scope] +Arguments inseccstr _%type_scope insec@{u v} = Type@{u} -> Type@{v} : Type@{max(u+1,v+1)} (* u v |= *) @@ -126,7 +125,7 @@ Inductive insecind@{u k} : Type@{k+1} := inseccstr : Type@{k} -> insecind@{u k} (* u k |= *) -For inseccstr: Argument scope is [type_scope] +Arguments inseccstr _%type_scope insec2@{u} = Prop : Type@{Set+1} (* u |= *) @@ -148,24 +147,24 @@ Type@{UnivBinders.59} -> Type@{i} (* i UnivBinders.59 UnivBinders.60 |= *) axfoo is universe polymorphic -Argument scope is [type_scope] +Arguments axfoo _%type_scope Expands to: Constant UnivBinders.axfoo axbar@{i UnivBinders.59 UnivBinders.60} : Type@{UnivBinders.60} -> Type@{i} (* i UnivBinders.59 UnivBinders.60 |= *) axbar is universe polymorphic -Argument scope is [type_scope] +Arguments axbar _%type_scope Expands to: Constant UnivBinders.axbar axfoo' : Type@{axfoo'.u0} -> Type@{axfoo'.i} axfoo' is not universe polymorphic -Argument scope is [type_scope] +Arguments axfoo' _%type_scope Expands to: Constant UnivBinders.axfoo' axbar' : Type@{axfoo'.u0} -> Type@{axfoo'.i} axbar' is not universe polymorphic -Argument scope is [type_scope] +Arguments axbar' _%type_scope Expands to: Constant UnivBinders.axbar' The command has indeed failed with message: When declaring multiple axioms in one command, only the first is allowed a universe binder (which will be shared by the whole block). diff --git a/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v b/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v index daca0ee5dc..44784675b0 100644 --- a/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v +++ b/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v @@ -18,6 +18,7 @@ Set Implicit Arguments. Require Import ZArith. +Require Import Lia. Require Import Znumtheory. Require Import Zpow_facts. Require Import DoubleType. @@ -298,8 +299,7 @@ Module ZnZ. replace (base digits) with (1 * base digits + 0) by ring. rewrite Hp1. apply Z.add_le_mono. - apply Z.mul_le_mono_nonneg; auto with zarith. - case p1; simpl; intros; red; simpl; intros; discriminate. + apply Z.mul_le_mono_nonneg. 1-2, 4: lia. unfold base; auto with zarith. case (spec_to_Z w1); auto with zarith. Qed. @@ -314,7 +314,7 @@ Module ZnZ. forall p, 0 <= p < base digits -> [|of_Z p|] = p. Proof. intros p; case p; simpl; try rewrite spec_0; auto. - intros; rewrite of_pos_correct; auto with zarith. + intros; rewrite of_pos_correct; lia. intros p1 (H1, _); contradict H1; apply Z.lt_nge; red; simpl; auto. Qed. @@ -423,7 +423,7 @@ Lemma eqb_eq : forall x y, eqb x y = true <-> x == y. Proof. intros. unfold eqb, eq. rewrite ZnZ.spec_compare. - case Z.compare_spec; intuition; try discriminate. + case Z.compare_spec; split; (easy || lia). Qed. Lemma eqb_correct : forall x y, eqb x y = true -> x==y. diff --git a/theories/Numbers/Cyclic/Abstract/NZCyclic.v b/theories/Numbers/Cyclic/Abstract/NZCyclic.v index 53a71ce0c9..4fd2cc0564 100644 --- a/theories/Numbers/Cyclic/Abstract/NZCyclic.v +++ b/theories/Numbers/Cyclic/Abstract/NZCyclic.v @@ -15,6 +15,7 @@ Require Import ZArith. Require Import Zpow_facts. Require Import DoubleType. Require Import CyclicAxioms. +Require Import Lia. (** * From [CyclicType] to [NZAxiomsSig] *) @@ -59,7 +60,8 @@ Ltac zcongruence := repeat red; intros; zify; congruence. Instance eq_equiv : Equivalence eq. Proof. -unfold eq. firstorder. + split. 1-2: firstorder. + intros x y z; apply eq_trans. Qed. Local Obligation Tactic := zcongruence. @@ -77,7 +79,7 @@ Qed. Theorem gt_wB_0 : 0 < wB. Proof. -pose proof gt_wB_1; auto with zarith. +pose proof gt_wB_1; lia. Qed. Lemma one_mod_wB : 1 mod wB = 1. @@ -138,8 +140,8 @@ intros n H1 H2 H3. unfold B in *. apply AS in H3. setoid_replace (ZnZ.of_Z (n + 1)) with (S (ZnZ.of_Z n)). assumption. zify. -rewrite 2 ZnZ.of_Z_correct; auto with zarith. -symmetry; apply Zmod_small; auto with zarith. +rewrite 2 ZnZ.of_Z_correct. 2-3: lia. +symmetry; apply Zmod_small; lia. Qed. Theorem Zbounded_induction : @@ -155,8 +157,8 @@ apply natlike_rec2; unfold Q'. destruct (Z.le_gt_cases b 0) as [H | H]. now right. left; now split. intros n H IH. destruct IH as [[IH1 IH2] | IH]. destruct (Z.le_gt_cases (b - 1) n) as [H1 | H1]. -right; auto with zarith. -left. split; [auto with zarith | now apply (QS n)]. +right; lia. +left. split; [ lia | now apply (QS n)]. right; auto with zarith. unfold Q' in *; intros n H1 H2. destruct (H n H1) as [[H3 H4] | H3]. assumption. now apply Z.le_ngt in H3. diff --git a/theories/Numbers/Cyclic/Int31/Cyclic31.v b/theories/Numbers/Cyclic/Int31/Cyclic31.v index e878fa289e..a1e7b2ff85 100644 --- a/theories/Numbers/Cyclic/Int31/Cyclic31.v +++ b/theories/Numbers/Cyclic/Int31/Cyclic31.v @@ -110,7 +110,7 @@ Section Basics. nshiftr x k = 0. Proof. intros. - replace k with ((k-size)+size)%nat by omega. + replace k with ((k-size)+size)%nat by lia. induction (k-size)%nat; auto. rewrite nshiftr_size; auto. simpl; rewrite IHn; auto. @@ -147,7 +147,7 @@ Section Basics. nshiftl x k = 0. Proof. intros. - replace k with ((k-size)+size)%nat by omega. + replace k with ((k-size)+size)%nat by lia. induction (k-size)%nat; auto. rewrite nshiftl_size; auto. simpl; rewrite IHn; auto. @@ -177,7 +177,7 @@ Section Basics. nshiftr x n = 0 -> nshiftr x p = 0. Proof. intros. - replace p with ((p-n)+n)%nat by omega. + replace p with ((p-n)+n)%nat by lia. induction (p-n)%nat. simpl; auto. simpl; rewrite IHn0; auto. @@ -188,7 +188,7 @@ Section Basics. Proof. intros. apply nshiftr_predsize_0_firstl. - apply nshiftr_0_propagates with n; auto; omega. + apply nshiftr_0_propagates with n; auto; lia. Qed. (** * Some induction principles over [int31] *) @@ -207,8 +207,8 @@ Section Basics. rewrite sneakl_shiftr. apply H0. change (P (nshiftr x (S (size - S n)))). - replace (S (size - S n))%nat with (size - n)%nat by omega. - apply IHn; omega. + replace (S (size - S n))%nat with (size - n)%nat by lia. + apply IHn; lia. change x with (nshiftr x (size-size)); auto. Qed. @@ -253,7 +253,7 @@ Section Basics. destruct (iszero (nshiftr x (size - S n))); auto. f_equal. change (shiftr (nshiftr x (size - S n))) with (nshiftr x (S (size - S n))). - replace (S (size - S n))%nat with (size - n)%nat by omega. + replace (S (size - S n))%nat with (size - n)%nat by lia. apply IHn; auto with arith. Qed. @@ -434,8 +434,8 @@ Section Basics. unfold phibis_aux, recrbis_aux; fold recrbis_aux; fold (phibis_aux n (shiftr x)). destruct (firstr x). - specialize IHn with (shiftr x); rewrite Z.double_spec; omega. - specialize IHn with (shiftr x); rewrite Z.succ_double_spec; omega. + specialize IHn with (shiftr x); rewrite Z.double_spec; lia. + specialize IHn with (shiftr x); rewrite Z.succ_double_spec; lia. Qed. Lemma phibis_aux_bounded : @@ -448,16 +448,16 @@ Section Basics. unfold phibis_aux, recrbis_aux; fold recrbis_aux; fold (phibis_aux n (shiftr (nshiftr x (size - S n)))). assert (shiftr (nshiftr x (size - S n)) = nshiftr x (size-n)). - replace (size - n)%nat with (S (size - (S n))) by omega. + replace (size - n)%nat with (S (size - (S n))) by lia. simpl; auto. rewrite H0. - assert (H1 : n <= size) by omega. + assert (H1 : n <= size) by lia. specialize (IHn x H1). set (y:=phibis_aux n (nshiftr x (size - n))) in *. rewrite Nat2Z.inj_succ, Z.pow_succ_r; auto with zarith. case_eq (firstr (nshiftr x (size - S n))); intros. - rewrite Z.double_spec; auto with zarith. - rewrite Z.succ_double_spec; auto with zarith. + rewrite Z.double_spec. lia. + rewrite Z.succ_double_spec; lia. Qed. Lemma phi_nonneg : forall x, (0 <= phi x)%Z. @@ -485,7 +485,7 @@ Section Basics. intros. unfold nshiftr in H; simpl in *. unfold phibis_aux, recrbis_aux. - rewrite H, Z.succ_double_spec; omega. + rewrite H, Z.succ_double_spec; lia. intros. remember (S n) as m. @@ -499,8 +499,8 @@ Section Basics. destruct (firstr x). change (Z.double (phibis_aux (S n) (shiftr x))) with (2*(phibis_aux (S n) (shiftr x)))%Z. - omega. - rewrite Z.succ_double_spec; omega. + lia. + rewrite Z.succ_double_spec; lia. Qed. Lemma phi_lowerbound : @@ -536,7 +536,7 @@ Section Basics. EqShiftL k x y -> EqShiftL k' x y. Proof. unfold EqShiftL; intros. - replace k' with ((k'-k)+k)%nat by omega. + replace k' with ((k'-k)+k)%nat by lia. remember (k'-k)%nat as n. clear Heqn H k'. induction n; simpl; auto. @@ -627,18 +627,18 @@ Section Basics. unfold shiftl; rewrite i2l_sneakl. simpl cstlist. rewrite <- app_comm_cons; f_equal. - rewrite IHn; [ | omega]. + rewrite IHn; [ | lia]. rewrite removelast_app. apply f_equal. - replace (size-n)%nat with (S (size - S n))%nat by omega. + replace (size-n)%nat with (S (size - S n))%nat by lia. rewrite removelast_firstn; auto. - rewrite i2l_length; omega. + rewrite i2l_length; lia. generalize (firstn_length (size-n) (i2l x)). rewrite i2l_length. intros H0 H1. rewrite H1 in H0. - rewrite min_l in H0 by omega. + rewrite min_l in H0 by lia. simpl length in H0. - omega. + lia. Qed. (** [i2l] can be used to define a relation equivalent to [EqShiftL] *) @@ -649,12 +649,12 @@ Section Basics. intros. destruct (le_lt_dec size k) as [Hle|Hlt]. split; intros. - replace (size-k)%nat with O by omega. + replace (size-k)%nat with O by lia. unfold firstn; auto. apply EqShiftL_size; auto. unfold EqShiftL. - assert (k <= size) by omega. + assert (k <= size) by lia. split; intros. assert (i2l (nshiftl x k) = i2l (nshiftl y k)) by (f_equal; auto). rewrite 2 i2l_nshiftl in H1; auto. @@ -679,7 +679,7 @@ Section Basics. rewrite 2 EqShiftL_i2l. unfold twice_plus_one. rewrite 2 i2l_sneakl. - replace (size-k)%nat with (S (size - S k))%nat by omega. + replace (size-k)%nat with (S (size - S k))%nat by lia. remember (size - S k)%nat as n. remember (i2l x) as lx. remember (i2l y) as ly. @@ -688,8 +688,8 @@ Section Basics. split; intros. injection H; auto. f_equal; auto. - subst ly n; rewrite i2l_length; omega. - subst lx n; rewrite i2l_length; omega. + subst ly n; rewrite i2l_length; lia. + subst lx n; rewrite i2l_length; lia. Qed. Lemma EqShiftL_shiftr : forall k x y, EqShiftL k x y -> @@ -704,13 +704,13 @@ Section Basics. rewrite <- sneakl_shiftr. rewrite (EqShiftL_firstr k x y); auto. rewrite <- sneakl_shiftr; auto. - omega. + lia. rewrite <- EqShiftL_twice_plus_one. unfold twice_plus_one; rewrite <- H0. rewrite <- sneakl_shiftr. rewrite (EqShiftL_firstr k x y); auto. rewrite <- sneakl_shiftr; auto. - omega. + lia. Qed. Lemma EqShiftL_incrbis : forall n k x y, n<=size -> @@ -725,13 +725,13 @@ Section Basics. unfold incrbis_aux; simpl; fold (incrbis_aux n (shiftr x)); fold (incrbis_aux n (shiftr y)). - rewrite (EqShiftL_firstr k x y); auto; try omega. + rewrite (EqShiftL_firstr k x y); auto; try lia. case_eq (firstr y); intros. rewrite EqShiftL_twice_plus_one. apply EqShiftL_shiftr; auto. rewrite EqShiftL_twice. - apply IHn; try omega. + apply IHn; try lia. apply EqShiftL_shiftr; auto. Qed. @@ -840,18 +840,18 @@ Section Basics. unfold phibis_aux, recrbis_aux; fold recrbis_aux; fold (phibis_aux n (shiftr (nshiftr x (size-S n)))). assert (shiftr (nshiftr x (size - S n)) = nshiftr x (size-n)). - replace (size - n)%nat with (S (size - (S n))); auto; omega. + replace (size - n)%nat with (S (size - (S n))); auto; lia. rewrite H0. case_eq (firstr (nshiftr x (size - S n))); intros. rewrite phi_inv_double. - rewrite IHn by omega. + rewrite IHn by lia. rewrite <- H0. remember (nshiftr x (size - S n)) as y. destruct y; simpl in H1; rewrite H1; auto. rewrite phi_inv_double_plus_one. - rewrite IHn by omega. + rewrite IHn by lia. rewrite <- H0. remember (nshiftr x (size - S n)) as y. destruct y; simpl in H1; rewrite H1; auto. @@ -928,7 +928,7 @@ Section Basics. (rewrite <- Z.pow_succ_r, <- Zpos_P_of_succ_nat; auto with zarith). rewrite (Z.mul_comm 2). - assert (n<=size)%nat by omega. + assert (n<=size)%nat by lia. destruct p; simpl; [ | | auto]; specialize (IHn p H0); generalize (p2ibis_bounded n p); @@ -937,13 +937,13 @@ Section Basics. change (Zpos p~1) with (2*Zpos p + 1)%Z. rewrite phi_twice_plus_one_firstl, Z.succ_double_spec. rewrite IHn; ring. - apply (nshiftr_0_firstl n); auto; try omega. + apply (nshiftr_0_firstl n); auto; try lia. change (Zpos p~0) with (2*Zpos p)%Z. rewrite phi_twice_firstl. change (Z.double (phi i)) with (2*(phi i))%Z. rewrite IHn; ring. - apply (nshiftr_0_firstl n); auto; try omega. + apply (nshiftr_0_firstl n); auto; try lia. Qed. (** We now prove that this [p2ibis] is related to [phi_inv_positive] *) @@ -959,8 +959,8 @@ Section Basics. specialize IHn with p; destruct (p2ibis n p); simpl @snd in *; simpl phi_inv_positive; rewrite ?EqShiftL_twice_plus_one, ?EqShiftL_twice; - replace (S (size - S n))%nat with (size - n)%nat by omega; - apply IHn; omega. + replace (S (size - S n))%nat with (size - n)%nat by lia; + apply IHn; lia. Qed. (** This gives the expected result about [phi o phi_inv], at least @@ -1008,12 +1008,12 @@ Section Basics. induction n; simpl; auto; intros. destruct p; auto; specialize IHn with p; generalize (p2ibis_bounded n p); - rewrite IHn; try omega; destruct (p2ibis n p); simpl; intros; + rewrite IHn; try lia; destruct (p2ibis n p); simpl; intros; f_equal; auto. apply double_twice_plus_one_firstl. - apply (nshiftr_0_firstl n); auto; omega. + apply (nshiftr_0_firstl n); auto; lia. apply double_twice_firstl. - apply (nshiftr_0_firstl n); auto; omega. + apply (nshiftr_0_firstl n); auto; lia. Qed. Lemma positive_to_int31_phi_inv_positive : forall p, @@ -1046,7 +1046,7 @@ Section Basics. pattern x at 1; rewrite <- (phi_inv_phi x). rewrite <- phi_inv_double. assert (0 <= Z.double (phi x)). - rewrite Z.double_spec; generalize (phi_bounded x); omega. + rewrite Z.double_spec; generalize (phi_bounded x); lia. destruct (Z.double (phi x)). simpl; auto. apply phi_phi_inv_positive. @@ -1060,7 +1060,7 @@ Section Basics. pattern x at 1; rewrite <- (phi_inv_phi x). rewrite <- phi_inv_double_plus_one. assert (0 <= Z.succ_double (phi x)). - rewrite Z.succ_double_spec; generalize (phi_bounded x); omega. + rewrite Z.succ_double_spec; generalize (phi_bounded x); lia. destruct (Z.succ_double (phi x)). simpl; auto. apply phi_phi_inv_positive. @@ -1075,7 +1075,7 @@ Section Basics. rewrite <- phi_inv_incr. assert (0 <= Z.succ (phi x)). change (Z.succ (phi x)) with ((phi x)+1)%Z; - generalize (phi_bounded x); omega. + generalize (phi_bounded x); lia. destruct (Z.succ (phi x)). simpl; auto. apply phi_phi_inv_positive. @@ -1095,7 +1095,7 @@ Section Basics. rewrite incr_twice, phi_twice_plus_one. remember (phi (complement_negative p)) as q. rewrite Z.succ_double_spec. - replace (2*q+1) with (2*(Z.succ q)-1) by omega. + replace (2*q+1) with (2*(Z.succ q)-1) by lia. rewrite <- Zminus_mod_idemp_l, <- Zmult_mod_idemp_r, IHp. rewrite Zmult_mod_idemp_r, Zminus_mod_idemp_l; auto with zarith. @@ -1203,9 +1203,7 @@ Section Int31_Specs. Qed. Lemma spec_more_than_1_digit: 1 < 31. - Proof. - auto with zarith. - Qed. + Proof. reflexivity. Qed. Lemma spec_0 : [| 0 |] = 0. Proof. @@ -1237,7 +1235,7 @@ Section Int31_Specs. assert ((X+Y) mod wB ?= X+Y <> Eq -> [+|C1 (phi_inv (X+Y))|] = X+Y). unfold interp_carry; rewrite phi_phi_inv, Z.compare_eq_iff; intros. destruct (Z_lt_le_dec (X+Y) wB). - contradict H1; auto using Zmod_small with zarith. + contradict H1; apply Zmod_small; lia. rewrite <- (Z_mod_plus_full (X+Y) (-1) wB). rewrite Zmod_small; lia. @@ -1261,7 +1259,7 @@ Section Int31_Specs. assert ((X+Y+1) mod wB ?= X+Y+1 <> Eq -> [+|C1 (phi_inv (X+Y+1))|] = X+Y+1). unfold interp_carry; rewrite phi_phi_inv, Z.compare_eq_iff; intros. destruct (Z_lt_le_dec (X+Y+1) wB). - contradict H1; auto using Zmod_small with zarith. + contradict H1; apply Zmod_small; lia. rewrite <- (Z_mod_plus_full (X+Y+1) (-1) wB). rewrite Zmod_small; lia. @@ -1399,8 +1397,7 @@ Section Int31_Specs. rewrite phi2_phi_inv2. apply Zmod_small. generalize (phi_bounded x)(phi_bounded y); intros. - change (wB^2) with (wB * wB). - auto using Z.mul_lt_mono_nonneg with zarith. + nia. Qed. Lemma spec_mul : forall x y, [|x*y|] = ([|x|] * [|y|]) mod wB. @@ -1424,7 +1421,7 @@ Section Int31_Specs. Proof. unfold div3121; intros. generalize (phi_bounded a1)(phi_bounded a2)(phi_bounded b); intros. - assert ([|b|]>0) by (auto with zarith). + assert ([|b|]>0) by lia. generalize (Z_div_mod (phi2 a1 a2) [|b|] H4) (Z_div_pos (phi2 a1 a2) [|b|] H4). unfold Z.div; destruct (Z.div_eucl (phi2 a1 a2) [|b|]). rewrite ?phi_phi_inv. @@ -1433,19 +1430,19 @@ Section Int31_Specs. change base with wB; change base with wB in H5. change (Z.pow_pos 2 31) with wB; change (Z.pow_pos 2 31) with wB in H. rewrite H5, Z.mul_comm. - replace (z0 mod wB) with z0 by (symmetry; apply Zmod_small; omega). + replace (z0 mod wB) with z0 by (symmetry; apply Zmod_small; lia). replace (z mod wB) with z; auto with zarith. symmetry; apply Zmod_small. split. - apply H7; change base with wB; auto with zarith. - apply Z.mul_lt_mono_pos_r with [|b|]; [omega| ]. + apply H7; change base with wB. nia. + apply Z.mul_lt_mono_pos_r with [|b|]; [lia| ]. rewrite Z.mul_comm. - apply Z.le_lt_trans with ([|b|]*z+z0); [omega| ]. + apply Z.le_lt_trans with ([|b|]*z+z0); [lia| ]. rewrite <- H5. - apply Z.le_lt_trans with ([|a1|]*wB+(wB-1)); [omega | ]. + apply Z.le_lt_trans with ([|a1|]*wB+(wB-1)); [lia | ]. replace ([|a1|]*wB+(wB-1)) with (wB*([|a1|]+1)-1) by ring. - assert (wB*([|a1|]+1) <= wB*[|b|]); try omega. - apply Z.mul_le_mono_nonneg; omega. + assert (wB*([|a1|]+1) <= wB*[|b|]); try lia. + apply Z.mul_le_mono_nonneg; lia. Qed. Lemma spec_div : forall a b, 0 < [|b|] -> @@ -1461,15 +1458,15 @@ Section Int31_Specs. destruct 1; intros. rewrite H1, Z.mul_comm. generalize (phi_bounded a)(phi_bounded b); intros. - replace (z0 mod wB) with z0 by (symmetry; apply Zmod_small; omega). + replace (z0 mod wB) with z0 by (symmetry; apply Zmod_small; lia). replace (z mod wB) with z; auto with zarith. symmetry; apply Zmod_small. - split; auto with zarith. - apply Z.le_lt_trans with [|a|]; auto with zarith. + split. lia. + apply Z.le_lt_trans with [|a|]. 2: lia. rewrite H1. - apply Z.le_trans with ([|b|]*z); try omega. + apply Z.le_trans with ([|b|]*z); try lia. rewrite <- (Z.mul_1_l z) at 1. - apply Z.mul_le_mono_nonneg; auto with zarith. + nia. Qed. Lemma spec_mod : forall a b, 0 < [|b|] -> @@ -1483,7 +1480,7 @@ Section Int31_Specs. rewrite ?phi_phi_inv. destruct 1; intros. generalize (phi_bounded b); intros. - apply Zmod_small; omega. + apply Zmod_small; lia. Qed. Lemma phi_gcd : forall i j, @@ -1498,7 +1495,7 @@ Section Int31_Specs. generalize (phi_bounded j)(phi_bounded i); intros. case_eq [|j|]; intros. simpl; intros. - generalize (Zabs_spec [|i|]); omega. + generalize (Zabs_spec [|i|]); lia. simpl. rewrite IHn, H1; f_equal. rewrite spec_mod, H1; auto. rewrite H1; compute; auto. @@ -1514,9 +1511,9 @@ Section Int31_Specs. unfold Zgcd_bound. generalize (phi_bounded b). destruct [|b|]. - unfold size; auto with zarith. + unfold size; lia. intros (_,H). - cut (Pos.size_nat p <= size)%nat; [ omega | rewrite <- Zpower2_Psize; auto]. + cut (Pos.size_nat p <= size)%nat; [ lia | rewrite <- Zpower2_Psize; auto]. intros (H,_); compute in H; elim H; auto. Qed. @@ -1544,9 +1541,7 @@ Section Int31_Specs. change (iter_nat (S (Z.abs_nat z) + (Z.abs_nat z))%nat A f a = iter_nat (Z.abs_nat (Z.succ_double z)) A f a); f_equal. rewrite Z.succ_double_spec, <- Z.add_diag. - rewrite Zabs2Nat.inj_add; auto with zarith. - rewrite Zabs2Nat.inj_add; auto with zarith. - change (Z.abs_nat 1) with 1%nat; omega. + lia. Qed. Fixpoint addmuldiv31_alt n i j := @@ -1594,7 +1589,7 @@ Section Int31_Specs. symmetry; apply Zdiv_small; apply phi_bounded. simpl addmuldiv31_alt; intros. - rewrite IHn; [ | omega ]. + rewrite IHn; [ | lia ]. case_eq (firstl y); intros. rewrite phi_twice, Z.double_spec. @@ -1606,8 +1601,9 @@ Section Int31_Specs. f_equal. ring. replace (31-Z.of_nat n) with (Z.succ(31-Z.succ(Z.of_nat n))) by ring. - rewrite Z.pow_succ_r, <- Zdiv_Zdiv; auto with zarith. + rewrite Z.pow_succ_r, <- Zdiv_Zdiv. rewrite Z.mul_comm, Z_div_mult; auto with zarith. + lia. auto with zarith. lia. rewrite phi_twice_plus_one, Z.succ_double_spec. rewrite phi_twice; auto. @@ -1622,49 +1618,49 @@ Section Int31_Specs. clear - H. symmetry. apply Zmod_unique with 1; [ | ring ]. generalize (phi_lowerbound _ H) (phi_bounded y). set (wB' := 2^Z.of_nat (pred size)). - replace wB with (2*wB'); [ omega | ]. + replace wB with (2*wB'); [ lia | ]. unfold wB'. rewrite <- Z.pow_succ_r, <- Nat2Z.inj_succ by (auto with zarith). f_equal. rewrite H1. replace wB with (2^(Z.of_nat n)*2^(31-Z.of_nat n)) by - (rewrite <- Zpower_exp; auto with zarith; f_equal; unfold size; ring). + (rewrite <- Zpower_exp by lia; f_equal; unfold size; ring). unfold Z.sub; rewrite <- Z.mul_opp_l. - rewrite Z_div_plus; auto with zarith. + rewrite Z_div_plus. ring_simplify. replace (31+-Z.of_nat n) with (Z.succ(31-Z.succ(Z.of_nat n))) by ring. - rewrite Z.pow_succ_r, <- Zdiv_Zdiv; auto with zarith. + rewrite Z.pow_succ_r, <- Zdiv_Zdiv. rewrite Z.mul_comm, Z_div_mult; auto with zarith. + lia. auto with zarith. lia. + apply Z.lt_gt; apply Z.pow_pos_nonneg; lia. Qed. Lemma shift_unshift_mod_2 : forall n p a, 0 <= p <= n -> ((a * 2 ^ (n - p)) mod (2^n) / 2 ^ (n - p)) mod (2^n) = a mod 2 ^ p. Proof. - intros. + intros n p a H. + assert (2 ^ n > 0 /\ 2 ^ p > 0 /\ 2 ^ (n - p) > 0) as [ X [ Y Z ] ] + by (split; [ | split ]; apply Z.lt_gt, Z.pow_pos_nonneg; lia). rewrite Zmod_small. - rewrite Zmod_eq by (auto with zarith). + rewrite Zmod_eq by assumption. unfold Z.sub at 1. - rewrite Z_div_plus_full_l - by (cut (0 < 2^(n-p)); auto with zarith). + rewrite Z_div_plus_full_l by lia. assert (2^n = 2^(n-p)*2^p). - rewrite <- Zpower_exp by (auto with zarith). - replace (n-p+p) with n; auto with zarith. + rewrite <- Zpower_exp by lia. + replace (n-p+p) with n; lia. rewrite H0. - rewrite <- Zdiv_Zdiv, Z_div_mult by (auto with zarith). + rewrite <- Zdiv_Zdiv, Z_div_mult; auto with zarith. rewrite (Z.mul_comm (2^(n-p))), Z.mul_assoc. rewrite <- Z.mul_opp_l. - rewrite Z_div_mult by (auto with zarith). + rewrite Z_div_mult by assumption. symmetry; apply Zmod_eq; auto with zarith. remember (a * 2 ^ (n - p)) as b. destruct (Z_mod_lt b (2^n)); auto with zarith. split. apply Z_div_pos; auto with zarith. - apply Zdiv_lt_upper_bound; auto with zarith. - apply Z.lt_le_trans with (2^n); auto with zarith. - rewrite <- (Z.mul_1_r (2^n)) at 1. - apply Z.mul_le_mono_nonneg; auto with zarith. - cut (0 < 2 ^ (n-p)); auto with zarith. + apply Zdiv_lt_upper_bound. lia. + nia. Qed. Lemma spec_pos_mod : forall w p, @@ -1676,28 +1672,28 @@ Section Int31_Specs. intros. generalize (phi_bounded w). symmetry; apply Zmod_small. - split; auto with zarith. - apply Z.lt_le_trans with wB; auto with zarith. + split. lia. + apply Z.lt_le_trans with wB. lia. apply Zpower_le_monotone; auto with zarith. intros. case_eq ([|p|] ?= 31); intros; [ apply H; rewrite (Z.compare_eq _ _ H0); auto with zarith | | - apply H; change ([|p|]>31)%Z in H0; auto with zarith ]. + apply H; change ([|p|]>31)%Z in H0; lia ]. change ([|p|]<31) in H0. - rewrite spec_add_mul_div by auto with zarith. + rewrite spec_add_mul_div by lia. change [|0|] with 0%Z; rewrite Z.mul_0_l, Z.add_0_l. generalize (phi_bounded p)(phi_bounded w); intros. assert (31-[|p|]<wB). - apply Z.le_lt_trans with 31%Z; auto with zarith. + apply Z.le_lt_trans with 31%Z. lia. compute; auto. assert ([|31-p|]=31-[|p|]). unfold sub31; rewrite phi_phi_inv. change [|31|] with 31%Z. - apply Zmod_small; auto with zarith. - rewrite spec_add_mul_div by (rewrite H4; auto with zarith). + apply Zmod_small. lia. + rewrite spec_add_mul_div by (rewrite H4; lia). change [|0|] with 0%Z; rewrite Zdiv_0_l, Z.add_0_r. rewrite H4. - apply shift_unshift_mod_2; simpl; auto with zarith. + apply shift_unshift_mod_2; simpl; lia. Qed. @@ -1744,20 +1740,20 @@ Section Int31_Specs. rewrite phi_phi_inv. apply Zmod_small. split. - change 0 with (Z.of_nat O); apply inj_le; omega. + change 0 with (Z.of_nat O); apply inj_le; lia. apply Z.le_lt_trans with (Z.of_nat 31). - apply inj_le; omega. + apply inj_le; lia. compute; auto. case_eq (firstl x); intros; auto. rewrite plus_Sn_m, plus_n_Sm. - replace (S (31 - S n)) with (31 - n)%nat by omega. - rewrite <- IHn; [ | omega | ]. + replace (S (31 - S n)) with (31 - n)%nat by lia. + rewrite <- IHn; [ | lia | ]. f_equal; f_equal. unfold add31. rewrite H1. f_equal. change [|In|] with 1. - replace (31-n)%nat with (S (31 - S n))%nat by omega. + replace (31-n)%nat with (S (31 - S n))%nat by lia. rewrite Nat2Z.inj_succ; ring. clear - H H2. @@ -1774,7 +1770,7 @@ Section Int31_Specs. assert ([|x|]<>0%Z). contradict H. rewrite <- (phi_inv_phi x); rewrite H; auto. - generalize (phi_bounded x); auto with zarith. + generalize (phi_bounded x); lia. Qed. Lemma spec_head0 : forall x, 0 < [|x|] -> @@ -1806,7 +1802,7 @@ Section Int31_Specs. rewrite <- nshiftl_S_tail; auto. change (2^(Z.of_nat 0)) with 1; rewrite Z.mul_1_l. - generalize (phi_bounded x); unfold size; split; auto with zarith. + generalize (phi_bounded x); unfold size; split. 2: lia. change (2^(Z.of_nat 31)/2) with (2^(Z.of_nat (pred size))). apply phi_lowerbound; auto. Qed. @@ -1852,20 +1848,20 @@ Section Int31_Specs. rewrite phi_phi_inv. apply Zmod_small. split. - change 0 with (Z.of_nat O); apply inj_le; omega. + change 0 with (Z.of_nat O); apply inj_le; lia. apply Z.le_lt_trans with (Z.of_nat 31). - apply inj_le; omega. + apply inj_le; lia. compute; auto. case_eq (firstr x); intros; auto. rewrite plus_Sn_m, plus_n_Sm. - replace (S (31 - S n)) with (31 - n)%nat by omega. - rewrite <- IHn; [ | omega | ]. + replace (S (31 - S n)) with (31 - n)%nat by lia. + rewrite <- IHn; [ | lia | ]. f_equal; f_equal. unfold add31. rewrite H1. f_equal. change [|In|] with 1. - replace (31-n)%nat with (S (31 - S n))%nat by omega. + replace (31-n)%nat with (S (31 - S n))%nat by lia. rewrite Nat2Z.inj_succ; ring. clear - H H2. @@ -1905,7 +1901,7 @@ Section Int31_Specs. exists [|shiftr x|]. split. - generalize (phi_bounded (shiftr x)); auto with zarith. + generalize (phi_bounded (shiftr x)); lia. rewrite phi_eqn2; auto. rewrite Z.succ_double_spec; simpl; ring. Qed. @@ -1918,7 +1914,7 @@ Section Int31_Specs. Lemma quotient_by_2 a: a - 1 <= (a/2) + (a/2). Proof. case (Z_mod_lt a 2); auto with zarith. - intros H1; rewrite Zmod_eq_full; auto with zarith. + intros H1; rewrite Zmod_eq_full; lia. Qed. Lemma sqrt_main_trick j k: 0 <= j -> 0 <= k -> @@ -1933,16 +1929,16 @@ Section Int31_Specs. generalize (sqr_pos (Z.succ j / 2)) (quotient_by_2 (Z.succ j)); unfold Z.succ. rewrite Z.pow_2_r, Z.mul_add_distr_r; repeat rewrite Z.mul_add_distr_l. - auto with zarith. + lia. intros k Hk _. replace ((Z.succ j + Z.succ k) / 2) with ((j + k)/2 + 1). generalize (Hrec Hj k Hk) (quotient_by_2 (j + k)). unfold Z.succ; repeat rewrite Z.pow_2_r; repeat rewrite Z.mul_add_distr_r; repeat rewrite Z.mul_add_distr_l. repeat rewrite Z.mul_1_l; repeat rewrite Z.mul_1_r. - auto with zarith. - rewrite Z.add_comm, <- Z_div_plus_full_l; auto with zarith. - apply f_equal2 with (f := Z.div); auto with zarith. + lia. + rewrite Z.add_comm, <- Z_div_plus_full_l by lia. + apply f_equal2 with (f := Z.div); lia. Qed. Lemma sqrt_main i j: 0 <= i -> 0 < j -> i < ((j + (i/j))/2 + 1) ^ 2. @@ -1956,25 +1952,25 @@ Section Int31_Specs. Lemma sqrt_init i: 1 < i -> i < (i/2 + 1) ^ 2. Proof. intros Hi. - assert (H1: 0 <= i - 2) by auto with zarith. - assert (H2: 1 <= (i / 2) ^ 2); auto with zarith. - replace i with (1* 2 + (i - 2)); auto with zarith. - rewrite Z.pow_2_r, Z_div_plus_full_l; auto with zarith. + assert (H1: 0 <= i - 2) by lia. + assert (H2: 1 <= (i / 2) ^ 2). + replace i with (1* 2 + (i - 2)) by lia. + rewrite Z.pow_2_r, Z_div_plus_full_l by lia. generalize (sqr_pos ((i - 2)/ 2)) (Z_div_pos (i - 2) 2). rewrite Z.mul_add_distr_r; repeat rewrite Z.mul_add_distr_l. - auto with zarith. + lia. generalize (quotient_by_2 i). rewrite Z.pow_2_r in H2 |- *; repeat (rewrite Z.mul_add_distr_r || rewrite Z.mul_add_distr_l || rewrite Z.mul_1_l || rewrite Z.mul_1_r). - auto with zarith. + lia. Qed. Lemma sqrt_test_true i j: 0 <= i -> 0 < j -> i/j >= j -> j ^ 2 <= i. Proof. intros Hi Hj Hd; rewrite Z.pow_2_r. - apply Z.le_trans with (j * (i/j)); auto with zarith. + apply Z.le_trans with (j * (i/j)). nia. apply Z_mult_div_ge; auto with zarith. Qed. @@ -1982,7 +1978,7 @@ Section Int31_Specs. Proof. intros Hi Hj H; case (Z.le_gt_cases j ((j + (i/j))/2)); auto. intros H1; contradict H; apply Z.le_ngt. - assert (2 * j <= j + (i/j)); auto with zarith. + assert (2 * j <= j + (i/j)). 2: lia. apply Z.le_trans with (2 * ((j + (i/j))/2)); auto with zarith. apply Z_mult_div_ge; auto with zarith. Qed. @@ -2001,8 +1997,7 @@ Section Int31_Specs. Lemma div31_phi i j: 0 < [|j|] -> [|fst (i/j)%int31|] = [|i|]/[|j|]. intros Hj; generalize (spec_div i j Hj). case div31; intros q r; simpl @fst. - intros (H1,H2); apply Zdiv_unique with [|r|]; auto with zarith. - rewrite H1; ring. + intros (H1,H2); apply Zdiv_unique with [|r|]; lia. Qed. Lemma sqrt31_step_correct rec i j: @@ -2016,24 +2011,27 @@ Section Int31_Specs. assert (Hp2: 0 < [|2|]) by exact (eq_refl Lt). intros Hi Hj Hij H31 Hrec; rewrite sqrt31_step_def. rewrite spec_compare, div31_phi; auto. - case Z.compare_spec; auto; intros Hc; - try (split; auto; apply sqrt_test_true; auto with zarith; fail). + case Z.compare_spec; intros Hc. + 1, 3: split; [ apply sqrt_test_true; lia | assumption ]. assert (E : [|(j + fst (i / j)%int31)|] = [|j|] + [|i|] / [|j|]). - { rewrite spec_add, div31_phi; auto using Z.mod_small with zarith. } - apply Hrec; rewrite !div31_phi, E; auto using sqrt_main with zarith. - split; try apply sqrt_test_false; auto with zarith. + { rewrite spec_add, div31_phi by lia. apply Z.mod_small. split. 2: lia. + generalize (Z.div_pos [|i|] [|j|]); lia. } + apply Hrec; rewrite !div31_phi, E; auto. + 2: apply sqrt_main; lia. + split. 2: apply sqrt_test_false; lia. apply Z.le_succ_l in Hj. change (1 <= [|j|]) in Hj. Z.le_elim Hj. - replace ([|j|] + [|i|]/[|j|]) with (1 * 2 + (([|j|] - 2) + [|i|] / [|j|])) by ring. - rewrite Z_div_plus_full_l; auto with zarith. - assert (0 <= [|i|]/ [|j|]) by auto with zarith. - assert (0 <= ([|j|] - 2 + [|i|] / [|j|]) / [|2|]); auto with zarith. + rewrite Z_div_plus_full_l by lia. + assert (0 <= [|i|]/ [|j|]) by (generalize (Z.div_pos [|i|] [|j|]); lia). + assert (0 <= ([|j|] - 2 + [|i|] / [|j|]) / [|2|]). 2: lia. + apply Z.div_pos; lia. - rewrite <- Hj, Zdiv_1_r. replace (1 + [|i|]) with (1 * 2 + ([|i|] - 1)) by ring. - rewrite Z_div_plus_full_l; auto with zarith. - assert (0 <= ([|i|] - 1) /2) by auto with zarith. - change ([|2|]) with 2; auto with zarith. + rewrite Z_div_plus_full_l by lia. + assert (0 <= ([|i|] - 1) /2) by (apply Z.div_pos; lia). + change [|2|] with 2. lia. Qed. Lemma iter31_sqrt_correct n rec i j: 0 < [|i|] -> 0 < [|j|] -> @@ -2044,18 +2042,16 @@ Section Int31_Specs. [|iter31_sqrt n rec i j|] ^ 2 <= [|i|] < ([|iter31_sqrt n rec i j|] + 1) ^ 2. Proof. revert rec i j; elim n; unfold iter31_sqrt; fold iter31_sqrt; clear n. - intros rec i j Hi Hj Hij H31 Hrec; apply sqrt31_step_correct; auto with zarith. - intros; apply Hrec; auto with zarith. - rewrite Z.pow_0_r; auto with zarith. + intros rec i j Hi Hj Hij H31 Hrec; apply sqrt31_step_correct; auto. + intros; apply Hrec. 2: rewrite Z.pow_0_r. 1-4: lia. intros n Hrec rec i j Hi Hj Hij H31 HHrec. apply sqrt31_step_correct; auto. - intros j1 Hj1 Hjp1; apply Hrec; auto with zarith. + intros j1 Hj1 Hjp1; apply Hrec. 1-4: lia. intros j2 Hj2 H2j2 Hjp2 Hj31; apply Hrec; auto with zarith. intros j3 Hj3 Hpj3. apply HHrec; auto. - rewrite Nat2Z.inj_succ, Z.pow_succ_r. - apply Z.le_trans with (2 ^Z.of_nat n + [|j2|]); auto with zarith. - apply Nat2Z.is_nonneg. + rewrite Nat2Z.inj_succ, Z.pow_succ_r by lia. + apply Z.le_trans with (2 ^Z.of_nat n + [|j2|]); lia. Qed. Lemma spec_sqrt : forall x, @@ -2063,13 +2059,13 @@ Section Int31_Specs. Proof. intros i; unfold sqrt31. rewrite spec_compare. case Z.compare_spec; change [|1|] with 1; - intros Hi; auto with zarith. - repeat rewrite Z.pow_2_r; auto with zarith. - apply iter31_sqrt_correct; auto with zarith. - rewrite div31_phi; change ([|2|]) with 2; auto with zarith. + intros Hi. lia. + 2: case (phi_bounded i); repeat rewrite Z.pow_2_r; auto with zarith. + apply iter31_sqrt_correct. lia. + rewrite div31_phi; change ([|2|]) with 2. 2: lia. replace ([|i|]) with (1 * 2 + ([|i|] - 2))%Z; try ring. - assert (0 <= ([|i|] - 2)/2)%Z by (apply Z_div_pos; auto with zarith). - rewrite Z_div_plus_full_l; auto with zarith. + assert (0 <= ([|i|] - 2)/2)%Z by (apply Z_div_pos; lia). + rewrite Z_div_plus_full_l; lia. rewrite div31_phi; change ([|2|]) with 2; auto with zarith. apply sqrt_init; auto. rewrite div31_phi; change ([|2|]) with 2; auto with zarith. @@ -2078,13 +2074,9 @@ Section Int31_Specs. case (phi_bounded i); auto. intros j2 H1 H2; contradict H2; apply Z.lt_nge. rewrite div31_phi; change ([|2|]) with 2; auto with zarith. - apply Z.le_lt_trans with ([|i|]); auto with zarith. - assert (0 <= [|i|]/2)%Z by (apply Z_div_pos; auto with zarith). - apply Z.le_trans with (2 * ([|i|]/2)); auto with zarith. - apply Z_mult_div_ge; auto with zarith. - case (phi_bounded i); unfold size; auto with zarith. - change [|0|] with 0; auto with zarith. - case (phi_bounded i); repeat rewrite Z.pow_2_r; auto with zarith. + case (phi_bounded i); unfold size; intros X Y. + apply Z.lt_le_trans with ([|i|]). apply Z.div_lt; lia. + lia. Qed. Lemma sqrt312_step_def rec ih il j: @@ -2113,12 +2105,12 @@ Section Int31_Specs. case (phi_bounded j); intros Hbj _. case (phi_bounded il); intros Hbil _. case (phi_bounded ih); intros Hbih Hbih1. - assert ([|ih|] < [|j|] + 1); auto with zarith. + assert ([|ih|] < [|j|] + 1). 2: lia. apply Z.square_lt_simpl_nonneg; auto with zarith. rewrite <- ?Z.pow_2_r; apply Z.le_lt_trans with (2 := H1). apply Z.le_trans with ([|ih|] * wB). - - rewrite ? Z.pow_2_r; auto with zarith. - - unfold phi2. change base with wB; auto with zarith. + - rewrite ? Z.pow_2_r; nia. + - unfold phi2. change base with wB; lia. Qed. Lemma div312_phi ih il j: (2^30 <= [|j|] -> [|ih|] < [|j|] -> @@ -2145,59 +2137,59 @@ Section Int31_Specs. case (phi_bounded il); intros Hil1 _. case (phi_bounded j); intros _ Hj1. assert (Hp3: (0 < phi2 ih il)). - { unfold phi2; apply Z.lt_le_trans with ([|ih|] * base); auto with zarith. - apply Z.mul_pos_pos; auto with zarith. - apply Z.lt_le_trans with (2:= Hih); auto with zarith. } + { unfold phi2; apply Z.lt_le_trans with ([|ih|] * base). 2: lia. + apply Z.mul_pos_pos. lia. auto with zarith. } rewrite spec_compare. case Z.compare_spec; intros Hc1. - split; auto. apply sqrt_test_true; auto. + unfold phi2, base; auto with zarith. + unfold phi2; rewrite Hc1. assert (0 <= [|il|]/[|j|]) by (apply Z_div_pos; auto with zarith). - rewrite Z.mul_comm, Z_div_plus_full_l; auto with zarith. - change base with wB. auto with zarith. + rewrite Z.mul_comm, Z_div_plus_full_l by lia. + change base with wB. lia. - case (Z.le_gt_cases (2 ^ 30) [|j|]); intros Hjj. + rewrite spec_compare; case Z.compare_spec; - rewrite div312_phi; auto; intros Hc; - try (split; auto; apply sqrt_test_true; auto with zarith; fail). + rewrite div312_phi; auto; intros Hc. + 1, 3: split; auto; apply sqrt_test_true; lia. apply Hrec. - * assert (Hf1: 0 <= phi2 ih il/ [|j|]) by auto with zarith. + * assert (Hf1: 0 <= phi2 ih il/ [|j|]). { apply Z.div_pos; lia. } apply Z.le_succ_l in Hj. change (1 <= [|j|]) in Hj. Z.le_elim Hj; [ | contradict Hc; apply Z.le_ngt; - rewrite <- Hj, Zdiv_1_r; auto with zarith ]. + rewrite <- Hj, Zdiv_1_r; lia ]. assert (Hf3: 0 < ([|j|] + phi2 ih il / [|j|]) / 2). { replace ([|j|] + phi2 ih il/ [|j|]) with - (1 * 2 + (([|j|] - 2) + phi2 ih il / [|j|])); try ring. - rewrite Z_div_plus_full_l; auto with zarith. - assert (0 <= ([|j|] - 2 + phi2 ih il / [|j|]) / 2) ; - auto with zarith. } + (1 * 2 + (([|j|] - 2) + phi2 ih il / [|j|])) by ring. + rewrite Z_div_plus_full_l by lia. + assert (0 <= ([|j|] - 2 + phi2 ih il / [|j|]) / 2). + apply Z.div_pos; lia. + lia. } assert (Hf4: ([|j|] + phi2 ih il / [|j|]) / 2 < [|j|]). - { apply sqrt_test_false; auto with zarith. } + { apply sqrt_test_false; lia. } generalize (spec_add_c j (fst (div3121 ih il j))). unfold interp_carry; case add31c; intros r; - rewrite div312_phi; auto with zarith. + rewrite div312_phi by lia. { rewrite div31_phi; change [|2|] with 2; auto with zarith. intros HH; rewrite HH; clear HH; auto with zarith. } { rewrite spec_add, div31_phi; change [|2|] with 2; auto. rewrite Z.mul_1_l; intros HH. - rewrite Z.add_comm, <- Z_div_plus_full_l; auto with zarith. + rewrite Z.add_comm, <- Z_div_plus_full_l by lia. change (phi v30 * 2) with (2 ^ Z.of_nat size). - rewrite HH, Zmod_small; auto with zarith. } + rewrite HH, Zmod_small; lia. } * replace (phi _) with (([|j|] + (phi2 ih il)/([|j|]))/2); - [ apply sqrt_main; auto with zarith | ]. + [ apply sqrt_main; lia | ]. generalize (spec_add_c j (fst (div3121 ih il j))). unfold interp_carry; case add31c; intros r; - rewrite div312_phi; auto with zarith. + rewrite div312_phi by lia. { rewrite div31_phi; auto with zarith. intros HH; rewrite HH; auto with zarith. } { intros HH; rewrite <- HH. change (1 * 2 ^ Z.of_nat size) with (phi (v30) * 2). - rewrite Z_div_plus_full_l; auto with zarith. + rewrite Z_div_plus_full_l by lia. rewrite Z.add_comm. rewrite spec_add, Zmod_small. - rewrite div31_phi; auto. - - split; auto with zarith. + - split. + case (phi_bounded (fst (r/2)%int31)); case (phi_bounded v30); auto with zarith. + rewrite div31_phi; change (phi 2) with 2; auto. @@ -2209,20 +2201,20 @@ Section Int31_Specs. * rewrite Z.mul_comm; apply Z_mult_div_ge; auto with zarith. * case (phi_bounded r); auto with zarith. } + contradict Hij; apply Z.le_ngt. - assert ((1 + [|j|]) <= 2 ^ 30); auto with zarith. + assert ((1 + [|j|]) <= 2 ^ 30). lia. apply Z.le_trans with ((2 ^ 30) * (2 ^ 30)); auto with zarith. - * assert (0 <= 1 + [|j|]); auto with zarith. - apply Z.mul_le_mono_nonneg; auto with zarith. + * assert (0 <= 1 + [|j|]). lia. + apply Z.mul_le_mono_nonneg; lia. * change ((2 ^ 30) * (2 ^ 30)) with ((2 ^ 29) * base). apply Z.le_trans with ([|ih|] * base); - change wB with base in *; auto with zarith. - unfold phi2, base; auto with zarith. + change wB with base in *; + unfold phi2, base; lia. - split; auto. apply sqrt_test_true; auto. + unfold phi2, base; auto with zarith. + apply Z.le_ge; apply Z.le_trans with (([|j|] * base)/[|j|]). - * rewrite Z.mul_comm, Z_div_mult; auto with zarith. - * apply Z.ge_le; apply Z_div_ge; auto with zarith. + * rewrite Z.mul_comm, Z_div_mult; lia. + * apply Z.ge_le; apply Z_div_ge; lia. Qed. Lemma iter312_sqrt_correct n rec ih il j: @@ -2235,17 +2227,15 @@ Section Int31_Specs. Proof. revert rec ih il j; elim n; unfold iter312_sqrt; fold iter312_sqrt; clear n. intros rec ih il j Hi Hj Hij Hrec; apply sqrt312_step_correct; auto with zarith. - intros; apply Hrec; auto with zarith. - rewrite Z.pow_0_r; auto with zarith. + intros; apply Hrec. 2: rewrite Z.pow_0_r. 1-3: lia. intros n Hrec rec ih il j Hi Hj Hij HHrec. apply sqrt312_step_correct; auto. - intros j1 Hj1 Hjp1; apply Hrec; auto with zarith. + intros j1 Hj1 Hjp1; apply Hrec. 1-3: lia. intros j2 Hj2 H2j2 Hjp2; apply Hrec; auto with zarith. intros j3 Hj3 Hpj3. apply HHrec; auto. - rewrite Nat2Z.inj_succ, Z.pow_succ_r. - apply Z.le_trans with (2 ^Z.of_nat n + [|j2|]); auto with zarith. - apply Nat2Z.is_nonneg. + rewrite Nat2Z.inj_succ, Z.pow_succ_r by lia. + lia. Qed. (* Avoid expanding [iter312_sqrt] before variables in the context. *) @@ -2264,18 +2254,18 @@ Section Int31_Specs. assert (Hb: 0 <= base) by (red; intros HH; discriminate). assert (Hi2: phi2 ih il < (phi Tn + 1) ^ 2). { change ((phi Tn + 1) ^ 2) with (2^62). - apply Z.le_lt_trans with ((2^31 -1) * base + (2^31 - 1)); auto with zarith. - 2: simpl; unfold Z.pow_pos; simpl; auto with zarith. + apply Z.le_lt_trans with ((2^31 -1) * base + (2^31 - 1)). + 2: simpl; unfold Z.pow_pos; simpl; lia. case (phi_bounded ih); case (phi_bounded il); intros H1 H2 H3 H4. unfold base, Z.pow, Z.pow_pos in H2,H4; simpl in H2,H4. - unfold phi2. cbn [Z.pow Z.pow_pos Pos.iter]. auto with zarith. } + unfold phi2. nia. } case (iter312_sqrt_correct 31 (fun _ _ j => j) ih il Tn); auto with zarith. change [|Tn|] with 2147483647; auto with zarith. intros j1 _ HH; contradict HH. apply Z.lt_nge. change [|Tn|] with 2147483647; auto with zarith. change (2 ^ Z.of_nat 31) with 2147483648; auto with zarith. - case (phi_bounded j1); auto with zarith. + case (phi_bounded j1); lia. set (s := iter312_sqrt 31 (fun _ _ j : int31 => j) ih il Tn). intros Hs1 Hs2. generalize (spec_mul_c s s); case mul31c. @@ -2287,22 +2277,22 @@ Section Int31_Specs. apply Z.le_trans with (2 ^ Z.of_nat size / 4 * base). simpl; auto with zarith. apply Z.le_trans with ([|ih|] * base); auto with zarith. - unfold phi2; case (phi_bounded il); auto with zarith. + unfold phi2; case (phi_bounded il); lia. intros ih1 il1. change [||WW ih1 il1||] with (phi2 ih1 il1). intros Hihl1. generalize (spec_sub_c il il1). case sub31c; intros il2 Hil2. - rewrite spec_compare; case Z.compare_spec. - unfold interp_carry in *. + - rewrite spec_compare; case Z.compare_spec. + + unfold interp_carry in *. intros H1; split. rewrite Z.pow_2_r, <- Hihl1. unfold phi2; ring[Hil2 H1]. replace [|il2|] with (phi2 ih il - phi2 ih1 il1). rewrite Hihl1. - rewrite <-Hbin in Hs2; auto with zarith. + rewrite <-Hbin in Hs2; lia. unfold phi2; rewrite H1, Hil2; ring. - unfold interp_carry. + + unfold interp_carry. intros H1; contradict Hs1. apply Z.lt_nge; rewrite Z.pow_2_r, <-Hihl1. unfold phi2. @@ -2310,39 +2300,39 @@ Section Int31_Specs. apply Z.lt_le_trans with (([|ih|] + 1) * base + 0). rewrite Z.mul_add_distr_r, Z.add_0_r; auto with zarith. case (phi_bounded il1); intros H3 _. - apply Z.add_le_mono; auto with zarith. - unfold interp_carry in *; change (1 * 2 ^ Z.of_nat size) with base. + nia. + + unfold interp_carry in *; change (1 * 2 ^ Z.of_nat size) with base. rewrite Z.pow_2_r, <- Hihl1, Hil2. intros H1. rewrite <- Z.le_succ_l, <- Z.add_1_r in H1. Z.le_elim H1. - contradict Hs2; apply Z.le_ngt. + * contradict Hs2; apply Z.le_ngt. replace (([|s|] + 1) ^ 2) with (phi2 ih1 il1 + 2 * [|s|] + 1). unfold phi2. case (phi_bounded il); intros Hpil _. assert (Hl1l: [|il1|] <= [|il|]). - { case (phi_bounded il2); rewrite Hil2; auto with zarith. } - assert ([|ih1|] * base + 2 * [|s|] + 1 <= [|ih|] * base); auto with zarith. + { case (phi_bounded il2); rewrite Hil2; lia. } + assert ([|ih1|] * base + 2 * [|s|] + 1 <= [|ih|] * base). 2: lia. case (phi_bounded s); change (2 ^ Z.of_nat size) with base; intros _ Hps. case (phi_bounded ih1); intros Hpih1 _; auto with zarith. - apply Z.le_trans with (([|ih1|] + 2) * base); auto with zarith. + apply Z.le_trans with (([|ih1|] + 2) * base). lia. rewrite Z.mul_add_distr_r. - assert (2 * [|s|] + 1 <= 2 * base); auto with zarith. + nia. rewrite Hihl1, Hbin; auto. - split. + * split. unfold phi2; rewrite <- H1; ring. replace (base + ([|il|] - [|il1|])) with (phi2 ih il - ([|s|] * [|s|])). - rewrite <-Hbin in Hs2; auto with zarith. + rewrite <-Hbin in Hs2; lia. rewrite <- Hihl1; unfold phi2; rewrite <- H1; ring. - unfold interp_carry in Hil2 |- *. + - unfold interp_carry in Hil2 |- *. unfold interp_carry; change (1 * 2 ^ Z.of_nat size) with base. assert (Hsih: [|ih - 1|] = [|ih|] - 1). { rewrite spec_sub, Zmod_small; auto; change [|1|] with 1. case (phi_bounded ih); intros H1 H2. generalize Hih; change (2 ^ Z.of_nat size / 4) with 536870912. - split; auto with zarith. } + lia. } rewrite spec_compare; case Z.compare_spec. - rewrite Hsih. + + rewrite Hsih. intros H1; split. rewrite Z.pow_2_r, <- Hihl1. unfold phi2; rewrite <-H1. @@ -2352,7 +2342,7 @@ Section Int31_Specs. change (2 ^ Z.of_nat size) with base; ring. replace [|il2|] with (phi2 ih il - phi2 ih1 il1). rewrite Hihl1. - rewrite <-Hbin in Hs2; auto with zarith. + rewrite <-Hbin in Hs2; lia. unfold phi2. rewrite <-H1. ring_simplify. @@ -2360,9 +2350,9 @@ Section Int31_Specs. ring. rewrite <-Hil2. change (2 ^ Z.of_nat size) with base; ring. - rewrite Hsih; intros H1. + + rewrite Hsih; intros H1. assert (He: [|ih|] = [|ih1|]). - { apply Z.le_antisymm; auto with zarith. + { apply Z.le_antisymm. lia. case (Z.le_gt_cases [|ih1|] [|ih|]); auto; intros H2. contradict Hs1; apply Z.lt_nge; rewrite Z.pow_2_r, <-Hihl1. unfold phi2. @@ -2371,42 +2361,41 @@ Section Int31_Specs. apply Z.lt_le_trans with (([|ih|] + 1) * base). rewrite Z.mul_add_distr_r, Z.mul_1_l; auto with zarith. case (phi_bounded il1); intros Hpil2 _. - apply Z.le_trans with (([|ih1|]) * base); auto with zarith. } + nia. } rewrite Z.pow_2_r, <-Hihl1; unfold phi2; rewrite <-He. contradict Hs1; apply Z.lt_nge; rewrite Z.pow_2_r, <-Hihl1. unfold phi2; rewrite He. - assert (phi il - phi il1 < 0); auto with zarith. + assert (phi il - phi il1 < 0). 2: lia. rewrite <-Hil2. - case (phi_bounded il2); auto with zarith. - intros H1. + case (phi_bounded il2); lia. + + intros H1. rewrite Z.pow_2_r, <-Hihl1. - assert (H2 : [|ih1|]+2 <= [|ih|]); auto with zarith. + assert (H2 : [|ih1|]+2 <= [|ih|]). lia. Z.le_elim H2. - contradict Hs2; apply Z.le_ngt. + * contradict Hs2; apply Z.le_ngt. replace (([|s|] + 1) ^ 2) with (phi2 ih1 il1 + 2 * [|s|] + 1). unfold phi2. - assert ([|ih1|] * base + 2 * phi s + 1 <= [|ih|] * base + ([|il|] - [|il1|])); - auto with zarith. + assert ([|ih1|] * base + 2 * phi s + 1 <= [|ih|] * base + ([|il|] - [|il1|])). + 2: lia. rewrite <-Hil2. change (-1 * 2 ^ Z.of_nat size) with (-base). case (phi_bounded il2); intros Hpil2 _. - apply Z.le_trans with ([|ih|] * base + - base); auto with zarith. + apply Z.le_trans with ([|ih|] * base + - base). 2: lia. case (phi_bounded s); change (2 ^ Z.of_nat size) with base; intros _ Hps. - assert (2 * [|s|] + 1 <= 2 * base); auto with zarith. - apply Z.le_trans with ([|ih1|] * base + 2 * base); auto with zarith. - assert (Hi: ([|ih1|] + 3) * base <= [|ih|] * base); auto with zarith. - rewrite Z.mul_add_distr_r in Hi; auto with zarith. + assert (2 * [|s|] + 1 <= 2 * base). lia. + apply Z.le_trans with ([|ih1|] * base + 2 * base). lia. + assert (Hi: ([|ih1|] + 3) * base <= [|ih|] * base). nia. lia. rewrite Hihl1, Hbin; auto. - unfold phi2; rewrite <-H2. + * unfold phi2; rewrite <-H2. split. - replace [|il|] with (([|il|] - [|il1|]) + [|il1|]); try ring. + replace [|il|] with (([|il|] - [|il1|]) + [|il1|]) by ring. rewrite <-Hil2. change (-1 * 2 ^ Z.of_nat size) with (-base); ring. replace (base + [|il2|]) with (phi2 ih il - phi2 ih1 il1). rewrite Hihl1. - rewrite <-Hbin in Hs2; auto with zarith. + rewrite <-Hbin in Hs2; lia. unfold phi2; rewrite <-H2. - replace [|il|] with (([|il|] - [|il1|]) + [|il1|]); try ring. + replace [|il|] with (([|il|] - [|il1|]) + [|il1|]) by ring. rewrite <-Hil2. change (-1 * 2 ^ Z.of_nat size) with (-base); ring. Qed. @@ -2436,8 +2425,8 @@ Qed. destruct H; auto with zarith. replace ([|x|] mod 2) with [|r|]. destruct H; auto with zarith. - case Z.compare_spec; auto with zarith. - apply Zmod_unique with [|q|]; auto with zarith. + case Z.compare_spec; lia. + apply Zmod_unique with [|q|]; lia. Qed. (* Bitwise *) diff --git a/theories/Numbers/Cyclic/Int31/Ring31.v b/theories/Numbers/Cyclic/Int31/Ring31.v index 890f42d301..1069a79e76 100644 --- a/theories/Numbers/Cyclic/Int31/Ring31.v +++ b/theories/Numbers/Cyclic/Int31/Ring31.v @@ -13,7 +13,7 @@ (** * Int31 numbers defines Z/(2^31)Z, and can hence be equipped with a ring structure and a ring tactic *) -Require Import Int31 Cyclic31 CyclicAxioms. +Require Import Lia Int31 Cyclic31 CyclicAxioms. Local Open Scope int31_scope. @@ -85,10 +85,11 @@ Qed. Lemma eqb31_eq : forall x y, eqb31 x y = true <-> x=y. Proof. unfold eqb31. intros x y. -rewrite Cyclic31.spec_compare. case Z.compare_spec. -intuition. apply Int31_canonic; auto. -intuition; subst; auto with zarith; try discriminate. -intuition; subst; auto with zarith; try discriminate. +rewrite Cyclic31.spec_compare. +split. +case Z.compare_spec. +intuition. apply Int31_canonic; auto. 1-2: easy. +now intros ->; rewrite Z.compare_refl. Qed. Lemma eqb31_correct : forall x y, eqb31 x y = true -> x=y. diff --git a/theories/Numbers/Cyclic/Int63/Int63.v b/theories/Numbers/Cyclic/Int63/Int63.v index aba064a556..febf4fa1be 100644 --- a/theories/Numbers/Cyclic/Int63/Int63.v +++ b/theories/Numbers/Cyclic/Int63/Int63.v @@ -1355,8 +1355,8 @@ Lemma sqrt_spec : forall x, Proof. intros i; unfold sqrt. rewrite compare_spec. case Z.compare_spec; rewrite to_Z_1; - intros Hi; auto with zarith. - repeat rewrite Z.pow_2_r; auto with zarith. + intros Hi. + lia. apply iter_sqrt_correct; auto with zarith; rewrite lsr_spec, to_Z_1; change (2^1) with 2; auto with zarith. replace [|i|] with (1 * 2 + ([|i|] - 2))%Z; try ring. @@ -1572,12 +1572,11 @@ Lemma sqrt2_spec : forall x y, case (to_Z_bounded il); intros Hpil _. assert (Hl1l: [|il1|] <= [|il|]). case (to_Z_bounded il2); rewrite Hil2; auto with zarith. - assert ([|ih1|] * wB + 2 * [|s|] + 1 <= [|ih|] * wB); auto with zarith. + enough ([|ih1|] * wB + 2 * [|s|] + 1 <= [|ih|] * wB) by lia. case (to_Z_bounded s); intros _ Hps. - case (to_Z_bounded ih1); intros Hpih1 _; auto with zarith. - apply Z.le_trans with (([|ih1|] + 2) * wB); auto with zarith. - rewrite Zmult_plus_distr_l. - assert (2 * [|s|] + 1 <= 2 * wB); auto with zarith. + case (to_Z_bounded ih1); intros Hpih1 _. + apply Z.le_trans with (([|ih1|] + 2) * wB). lia. + auto with zarith. unfold zn2z_to_Z; rewrite <-Hihl1, Hbin; auto. intros H2; split. unfold zn2z_to_Z; rewrite <- H2; ring. @@ -1622,8 +1621,8 @@ Lemma sqrt2_spec : forall x y, case (to_Z_bounded s); intros _ Hps. assert (2 * [|s|] + 1 <= 2 * wB); auto with zarith. apply Z.le_trans with ([|ih1|] * wB + 2 * wB); auto with zarith. - assert (Hi: ([|ih1|] + 3) * wB <= [|ih|] * wB); auto with zarith. - rewrite Zmult_plus_distr_l in Hi; auto with zarith. + assert (Hi: ([|ih1|] + 3) * wB <= [|ih|] * wB) by auto with zarith. + lia. unfold zn2z_to_Z; rewrite <-Hihl1, Hbin; auto. intros H2; unfold zn2z_to_Z; rewrite <-H2. split. diff --git a/theories/Numbers/Cyclic/ZModulo/ZModulo.v b/theories/Numbers/Cyclic/ZModulo/ZModulo.v index 2785e89c5d..cf3e6668a5 100644 --- a/theories/Numbers/Cyclic/ZModulo/ZModulo.v +++ b/theories/Numbers/Cyclic/ZModulo/ZModulo.v @@ -23,6 +23,7 @@ Require Import Znumtheory. Require Import Zpow_facts. Require Import DoubleType. Require Import CyclicAxioms. +Require Import Lia. Local Open Scope Z_scope. @@ -113,7 +114,7 @@ Section ZModulo. Lemma spec_0 : [|zero|] = 0. Proof. unfold to_Z, zero. - apply Zmod_small; generalize wB_pos; auto with zarith. + apply Zmod_small; generalize wB_pos. lia. Qed. Lemma spec_1 : [|one|] = 1. @@ -128,10 +129,10 @@ Section ZModulo. Lemma spec_Bm1 : [|minus_one|] = wB - 1. Proof. unfold to_Z, minus_one. - apply Zmod_small; split; auto with zarith. + apply Zmod_small; split. 2: lia. unfold wB, base. - cut (1 <= 2 ^ Zpos digits); auto with zarith. - apply Z.le_trans with (Zpos digits); auto with zarith. + cut (1 <= 2 ^ Zpos digits). lia. + apply Z.le_trans with (Zpos digits). lia. apply Zpower2_le_lin; auto with zarith. Qed. @@ -162,7 +163,7 @@ Section ZModulo. assert (x mod wB <> 0). unfold eq0, to_Z in H. intro H0; rewrite H0 in H; discriminate. - rewrite Z_mod_nz_opp_full; auto with zarith. + rewrite Z_mod_nz_opp_full; lia. Qed. Lemma spec_opp : forall x, [|opp x|] = (-[|x|]) mod wB. @@ -175,14 +176,14 @@ Section ZModulo. Lemma spec_opp_carry : forall x, [|opp_carry x|] = wB - [|x|] - 1. Proof. intros; unfold opp_carry, to_Z; auto. - replace (- x - 1) with (- 1 - x) by omega. + replace (- x - 1) with (- 1 - x) by lia. rewrite <- Zminus_mod_idemp_r. - replace ( -1 - x mod wB) with (0 + ( -1 - x mod wB)) by omega. + replace ( -1 - x mod wB) with (0 + ( -1 - x mod wB)) by lia. rewrite <- (Z_mod_same_full wB). rewrite Zplus_mod_idemp_l. - replace (wB + (-1 - x mod wB)) with (wB - x mod wB -1) by omega. + replace (wB + (-1 - x mod wB)) with (wB - x mod wB -1) by lia. apply Zmod_small. - generalize (Z_mod_lt x wB wB_pos); omega. + generalize (Z_mod_lt x wB wB_pos); lia. Qed. Definition succ_c x := @@ -221,7 +222,7 @@ Section ZModulo. symmetry. rewrite Z.add_move_r. assert ((x+1) mod wB = 0) by (apply spec_eq0; auto). replace (wB-1) with ((wB-1) mod wB) by - (apply Zmod_small; generalize wB_pos; omega). + (apply Zmod_small; generalize wB_pos; lia). rewrite <- Zminus_mod_idemp_l; rewrite Z_mod_same; simpl; auto. apply Zmod_equal; auto. @@ -231,10 +232,10 @@ Section ZModulo. contradict H0. rewrite Z.add_move_r in H0; simpl in H0. rewrite <- Zplus_mod_idemp_l; rewrite H0. - replace (wB-1+1) with wB; auto with zarith; apply Z_mod_same; auto. + replace (wB-1+1) with wB by lia; apply Z_mod_same; auto. rewrite <- Zplus_mod_idemp_l. apply Zmod_small. - generalize (Z_mod_lt x wB wB_pos); omega. + generalize (Z_mod_lt x wB wB_pos); lia. Qed. Lemma spec_add_c : forall x y, [+|add_c x y|] = [|x|] + [|y|]. @@ -242,10 +243,10 @@ Section ZModulo. intros; unfold add_c, to_Z, interp_carry. destruct Z_lt_le_dec. apply Zmod_small; - generalize (Z_mod_lt x wB wB_pos) (Z_mod_lt y wB wB_pos); omega. + generalize (Z_mod_lt x wB wB_pos) (Z_mod_lt y wB wB_pos); lia. rewrite Z.mul_1_l, Z.add_comm, Z.add_move_r. apply Zmod_small; - generalize (Z_mod_lt x wB wB_pos) (Z_mod_lt y wB wB_pos); omega. + generalize (Z_mod_lt x wB wB_pos) (Z_mod_lt y wB wB_pos); lia. Qed. Lemma spec_add_carry_c : forall x y, [+|add_carry_c x y|] = [|x|] + [|y|] + 1. @@ -253,10 +254,10 @@ Section ZModulo. intros; unfold add_carry_c, to_Z, interp_carry. destruct Z_lt_le_dec. apply Zmod_small; - generalize (Z_mod_lt x wB wB_pos) (Z_mod_lt y wB wB_pos); omega. + generalize (Z_mod_lt x wB wB_pos) (Z_mod_lt y wB wB_pos); lia. rewrite Z.mul_1_l, Z.add_comm, Z.add_move_r. apply Zmod_small; - generalize (Z_mod_lt x wB wB_pos) (Z_mod_lt y wB wB_pos); omega. + generalize (Z_mod_lt x wB wB_pos) (Z_mod_lt y wB wB_pos); lia. Qed. Lemma spec_succ : forall x, [|succ x|] = ([|x|] + 1) mod wB. @@ -299,14 +300,14 @@ Section ZModulo. intros; unfold pred_c, to_Z, interp_carry. case_eq (eq0 x); intros. fold [|x|]; rewrite spec_eq0; auto. - replace ((wB-1) mod wB) with (wB-1); auto with zarith. - symmetry; apply Zmod_small; generalize wB_pos; omega. + replace ((wB-1) mod wB) with (wB-1). lia. + symmetry; apply Zmod_small; generalize wB_pos; lia. assert (x mod wB <> 0). unfold eq0, to_Z in *; now destruct (x mod wB). rewrite <- Zminus_mod_idemp_l. apply Zmod_small. - generalize (Z_mod_lt x wB wB_pos); omega. + generalize (Z_mod_lt x wB wB_pos); lia. Qed. Lemma spec_sub_c : forall x y, [-|sub_c x y|] = [|x|] - [|y|]. @@ -315,12 +316,12 @@ Section ZModulo. destruct Z_lt_le_dec. replace ((wB + (x mod wB - y mod wB)) mod wB) with (wB + (x mod wB - y mod wB)). - omega. + lia. symmetry; apply Zmod_small. - generalize wB_pos (Z_mod_lt x wB wB_pos) (Z_mod_lt y wB wB_pos); omega. + generalize wB_pos (Z_mod_lt x wB wB_pos) (Z_mod_lt y wB wB_pos); lia. apply Zmod_small. - generalize wB_pos (Z_mod_lt x wB wB_pos) (Z_mod_lt y wB wB_pos); omega. + generalize wB_pos (Z_mod_lt x wB wB_pos) (Z_mod_lt y wB wB_pos); lia. Qed. Lemma spec_sub_carry_c : forall x y, [-|sub_carry_c x y|] = [|x|] - [|y|] - 1. @@ -329,12 +330,12 @@ Section ZModulo. destruct Z_lt_le_dec. replace ((wB + (x mod wB - y mod wB - 1)) mod wB) with (wB + (x mod wB - y mod wB -1)). - omega. + lia. symmetry; apply Zmod_small. - generalize wB_pos (Z_mod_lt x wB wB_pos) (Z_mod_lt y wB wB_pos); omega. + generalize wB_pos (Z_mod_lt x wB wB_pos) (Z_mod_lt y wB wB_pos); lia. apply Zmod_small. - generalize wB_pos (Z_mod_lt x wB wB_pos) (Z_mod_lt y wB wB_pos); omega. + generalize wB_pos (Z_mod_lt x wB wB_pos) (Z_mod_lt y wB wB_pos); lia. Qed. Lemma spec_pred : forall x, [|pred x|] = ([|x|] - 1) mod wB. @@ -381,12 +382,12 @@ Section ZModulo. subst h. split. apply Z_div_pos; auto with zarith. - apply Zdiv_lt_upper_bound; auto with zarith. + apply Zdiv_lt_upper_bound. lia. apply Z.mul_lt_mono_nonneg; auto with zarith. clear H H0 H1 H2. case_eq (eq0 h); simpl; intros. case_eq (eq0 l); simpl; intros. - rewrite <- H3, <- H4, (spec_eq0 h), (spec_eq0 l); auto with zarith. + rewrite <- H3, <- H4, (spec_eq0 h), (spec_eq0 l); auto. lia. rewrite H3, H4; auto with zarith. rewrite H3, H4; auto with zarith. Qed. @@ -409,7 +410,7 @@ Section ZModulo. 0 <= [|r|] < [|b|]. Proof. intros; unfold div. - assert ([|b|]>0) by auto with zarith. + assert ([|b|]>0) by lia. assert (Z.div_eucl [|a|] [|b|] = ([|a|]/[|b|], [|a|] mod [|b|])). unfold Z.modulo, Z.div; destruct Z.div_eucl; auto. generalize (Z_div_mod [|a|] [|b|] H0). @@ -417,7 +418,7 @@ Section ZModulo. injection H1 as [= ? ?]. assert ([|r|]=r). apply Zmod_small; generalize (Z_mod_lt b wB wB_pos); fold [|b|]; - auto with zarith. + lia. assert ([|q|]=q). apply Zmod_small. subst q. @@ -426,7 +427,7 @@ Section ZModulo. apply Zdiv_lt_upper_bound; auto with zarith. apply Z.lt_le_trans with (wB*1). rewrite Z.mul_1_r; auto with zarith. - apply Z.mul_le_mono_nonneg; generalize wB_pos; auto with zarith. + apply Z.mul_le_mono_nonneg; generalize wB_pos; lia. rewrite H5, H6; rewrite Z.mul_comm; auto with zarith. Qed. @@ -449,9 +450,9 @@ Section ZModulo. Proof. intros; unfold modulo. apply Zmod_small. - assert ([|b|]>0) by auto with zarith. + assert ([|b|]>0) by lia. generalize (Z_mod_lt [|a|] [|b|] H0) (Z_mod_lt b wB wB_pos). - fold [|b|]; omega. + fold [|b|]; lia. Qed. Lemma spec_modulo_gt : forall a b, [|a|] > [|b|] -> 0 < [|b|] -> @@ -470,19 +471,19 @@ Section ZModulo. destruct H2 as (q,H2); destruct H3 as (q',H3); clear H4. assert (H4:=Z.gcd_nonneg a b). destruct (Z.eq_dec (Z.gcd a b) 0) as [->|Hneq]. - generalize (Zmax_spec a b); omega. + generalize (Zmax_spec a b); lia. assert (0 <= q). - apply Z.mul_le_mono_pos_r with (Z.gcd a b); auto with zarith. + apply Z.mul_le_mono_pos_r with (Z.gcd a b); lia. destruct (Z.eq_dec q 0). subst q; simpl in *; subst a; simpl; auto. - generalize (Zmax_spec 0 b) (Zabs_spec b); omega. + generalize (Zmax_spec 0 b) (Zabs_spec b); lia. apply Z.le_trans with a. rewrite H2 at 2. rewrite <- (Z.mul_1_l (Z.gcd a b)) at 1. - apply Z.mul_le_mono_nonneg; auto with zarith. - generalize (Zmax_spec a b); omega. + apply Z.mul_le_mono_nonneg; lia. + generalize (Zmax_spec a b); lia. Qed. Lemma spec_gcd : forall a b, Zis_gcd [|a|] [|b|] [|gcd a b|]. @@ -497,7 +498,7 @@ Section ZModulo. apply Z.gcd_nonneg. apply Z.le_lt_trans with (Z.max [|a|] [|b|]). apply Zgcd_bound; auto with zarith. - generalize (Zmax_spec [|a|] [|b|]); omega. + generalize (Zmax_spec [|a|] [|b|]); lia. Qed. Lemma spec_gcd_gt : forall a b, [|a|] > [|b|] -> @@ -519,7 +520,7 @@ Section ZModulo. intros; unfold div21. generalize (Z_mod_lt a1 wB wB_pos); fold [|a1|]; intros. generalize (Z_mod_lt a2 wB wB_pos); fold [|a2|]; intros. - assert ([|b|]>0) by auto with zarith. + assert ([|b|]>0) by lia. remember ([|a1|]*wB+[|a2|]) as a. assert (Z.div_eucl a [|b|] = (a/[|b|], a mod [|b|])). unfold Z.modulo, Z.div; destruct Z.div_eucl; auto. @@ -528,18 +529,17 @@ Section ZModulo. injection H4 as [= ? ?]. assert ([|r|]=r). apply Zmod_small; generalize (Z_mod_lt b wB wB_pos); fold [|b|]; - auto with zarith. + lia. assert ([|q|]=q). apply Zmod_small. subst q. split. - apply Z_div_pos; auto with zarith. - subst a; auto with zarith. - apply Zdiv_lt_upper_bound; auto with zarith. + apply Z_div_pos. lia. + subst a. nia. + apply Zdiv_lt_upper_bound; nia. subst a. replace (wB*[|b|]) with (([|b|]-1)*wB + wB) by ring. - apply Z.lt_le_trans with ([|a1|]*wB+wB); auto with zarith. - rewrite H8, H9; rewrite Z.mul_comm; auto with zarith. + lia. Qed. Definition add_mul_div p x y := @@ -573,7 +573,7 @@ Section ZModulo. if is_even x then [|x|] mod 2 = 0 else [|x|] mod 2 = 1. Proof. intros; unfold is_even; destruct Z.eq_dec; auto. - generalize (Z_mod_lt [|x|] 2); omega. + generalize (Z_mod_lt [|x|] 2); lia. Qed. Definition sqrt x := Z.sqrt [|x|]. @@ -611,33 +611,33 @@ Section ZModulo. simpl zn2z_to_Z. remember ([|x|]*wB+[|y|]) as z. destruct z. - auto with zarith. - generalize (Z.sqrtrem_spec (Zpos p)). - destruct Z.sqrtrem as (s,r); intros [U V]; auto with zarith. + - auto with zarith. + - generalize (Z.sqrtrem_spec (Zpos p)). + destruct Z.sqrtrem as (s,r); intros [U V]. lia. assert (s < wB). + { destruct (Z_lt_le_dec s wB); auto. assert (wB * wB <= Zpos p). - rewrite U. - apply Z.le_trans with (s*s); try omega. - apply Z.mul_le_mono_nonneg; generalize wB_pos; auto with zarith. + apply Z.le_trans with (s*s). 2: lia. + apply Z.mul_le_mono_nonneg; generalize wB_pos; lia. assert (Zpos p < wB*wB). rewrite Heqz. replace (wB*wB) with ((wB-1)*wB+wB) by ring. - apply Z.add_le_lt_mono; auto with zarith. - apply Z.mul_le_mono_nonneg; auto with zarith. - generalize (spec_to_Z x); auto with zarith. - generalize wB_pos; auto with zarith. - omega. - replace [|s|] with s by (symmetry; apply Zmod_small; auto with zarith). + apply Z.add_le_lt_mono. 2: auto with zarith. + apply Z.mul_le_mono_nonneg. 1, 3-5: auto with zarith. + generalize wB_pos; lia. + generalize (spec_to_Z x); lia. + } + replace [|s|] with s by (symmetry; apply Zmod_small; lia). destruct Z_lt_le_dec; unfold interp_carry. - replace [|r|] with r by (symmetry; apply Zmod_small; auto with zarith). - rewrite Z.pow_2_r; auto with zarith. - replace [|r-wB|] with (r-wB) by (symmetry; apply Zmod_small; auto with zarith). - rewrite Z.pow_2_r; omega. + replace [|r|] with r by (symmetry; apply Zmod_small; lia). + rewrite Z.pow_2_r; lia. + replace [|r-wB|] with (r-wB) by (symmetry; apply Zmod_small; lia). + rewrite Z.pow_2_r; lia. - assert (0<=Zneg p). - rewrite Heqz; generalize wB_pos; auto with zarith. - compute in H0; elim H0; auto. + - assert (0<=Zneg p). + generalize (spec_to_Z x) (spec_to_Z y); nia. + lia. Qed. Lemma two_p_power2 : forall x, x>=0 -> two_p x = 2 ^ x. @@ -669,12 +669,12 @@ Section ZModulo. intros. assert (0 <= zdigits - Z.log2 (Zpos p) - 1 < wB) as Hrange. split. - cut (Z.log2 (Zpos p) < zdigits). omega. + cut (Z.log2 (Zpos p) < zdigits). lia. unfold zdigits. unfold wB, base in *. apply Z.log2_lt_pow2; intuition. apply Z.lt_trans with zdigits. - omega. + lia. unfold zdigits, wB, base; apply Zpower2_lt_lin; auto with zarith. unfold to_Z; rewrite (Zmod_small _ _ Hrange). @@ -728,7 +728,7 @@ Section ZModulo. rewrite Z.mul_comm. rewrite <- Z.pow_succ_r; auto with zarith. rewrite H1; auto. - rewrite <- H1; omega. + rewrite <- H1; lia. Qed. Definition tail0 x := diff --git a/theories/Reals/Cos_plus.v b/theories/Reals/Cos_plus.v index d09b3248ef..b411c4953a 100644 --- a/theories/Reals/Cos_plus.v +++ b/theories/Reals/Cos_plus.v @@ -14,7 +14,7 @@ Require Import SeqSeries. Require Import Rtrigo_def. Require Import Cos_rel. Require Import Max. -Require Import Omega. +Require Import Lia. Local Open Scope nat_scope. Local Open Scope R_scope. @@ -213,7 +213,7 @@ Proof. apply le_n_S. apply plus_le_compat_l; assumption. rewrite pred_of_minus. - omega. + lia. apply Rle_trans with (sum_f_R0 (fun k:nat => @@ -236,7 +236,7 @@ Proof. apply Rmult_le_compat_l. left; apply Rinv_0_lt_compat; apply INR_fact_lt_0. apply C_maj. - omega. + lia. right. unfold Rdiv; rewrite Rmult_comm. unfold Binomial.C. @@ -248,7 +248,7 @@ Proof. unfold Rsqr; reflexivity. apply INR_fact_neq_0. apply INR_fact_neq_0. - omega. + lia. apply INR_fact_neq_0. unfold Rdiv; rewrite Rmult_comm. unfold Binomial.C. @@ -258,7 +258,7 @@ Proof. replace (2 * S (N + n) - 2 * S (n0 + n))%nat with (2 * (N - n0))%nat. rewrite mult_INR. reflexivity. - omega. + lia. apply INR_fact_neq_0. apply Rle_trans with (sum_f_R0 (fun k:nat => INR N / INR (fact (S N)) * C ^ (4 * N)) (pred N)). @@ -279,7 +279,7 @@ Proof. apply Rmult_le_compat_l. apply Rle_0_sqr. apply le_INR. - omega. + lia. rewrite Rmult_comm; unfold Rdiv; apply Rmult_le_compat_l. apply pos_INR. apply Rle_trans with (/ INR (fact (S (N + n)))). @@ -458,7 +458,7 @@ Proof. (2 * (N - n0) + 1 + (2 * S (n0 + n) + 1))%nat. repeat rewrite pow_add. ring. - omega. + lia. apply INR_fact_neq_0. apply INR_fact_neq_0. apply Rle_ge; left; apply Rinv_0_lt_compat. @@ -517,7 +517,7 @@ Proof. replace (2 * S (S (n0 + n)))%nat with (S (2 * S (n0 + n) + 1)). apply le_n_Sn. ring. - omega. + lia. right. unfold Rdiv; rewrite Rmult_comm. unfold Binomial.C. @@ -529,7 +529,7 @@ Proof. unfold Rsqr; reflexivity. apply INR_fact_neq_0. apply INR_fact_neq_0. - omega. + lia. apply INR_fact_neq_0. unfold Rdiv; rewrite Rmult_comm. unfold Binomial.C. @@ -540,7 +540,7 @@ Proof. (2 * (N - n0) + 1)%nat. rewrite mult_INR. reflexivity. - omega. + lia. apply INR_fact_neq_0. apply Rle_trans with (sum_f_R0 (fun k:nat => INR N / INR (fact (S (S N))) * C ^ (4 * S N)) @@ -563,8 +563,8 @@ Proof. apply Rle_0_sqr. replace (S (pred (N - n))) with (N - n)%nat. apply le_INR. - omega. - omega. + lia. + lia. rewrite Rmult_comm; unfold Rdiv; apply Rmult_le_compat_l. apply pos_INR. apply Rle_trans with (/ INR (fact (S (S (N + n))))). @@ -592,7 +592,7 @@ Proof. rewrite Rmult_1_r. apply le_INR. apply fact_le. - omega. + lia. apply INR_fact_neq_0. apply INR_fact_neq_0. rewrite sum_cte. diff --git a/theories/Reals/Cos_rel.v b/theories/Reals/Cos_rel.v index d5086db6cf..4ce5cd6b1c 100644 --- a/theories/Reals/Cos_rel.v +++ b/theories/Reals/Cos_rel.v @@ -12,7 +12,7 @@ Require Import Rbase. Require Import Rfunctions. Require Import SeqSeries. Require Import Rtrigo_def. -Require Import OmegaTactic. +Require Import Lia. Local Open Scope R_scope. Definition A1 (x:R) (N:nat) : R := @@ -149,13 +149,13 @@ unfold Wn. apply Rmult_eq_compat_l. replace (2 * S i - S (2 * i0))%nat with (S (2 * (i - i0))). reflexivity. -omega. +lia. apply sum_eq; intros. unfold Wn. apply Rmult_eq_compat_l. replace (2 * S i - 2 * i0)%nat with (2 * (S i - i0))%nat. reflexivity. -omega. +lia. replace (- sum_f_R0 @@ -211,7 +211,7 @@ replace (S (2 * i0)) with (2 * i0 + 1)%nat; [ apply Rmult_eq_compat_l | ring ]. replace (2 * S i - (2 * i0 + 1))%nat with (2 * (i - i0) + 1)%nat. reflexivity. -omega. +lia. apply INR_fact_neq_0. apply INR_fact_neq_0. apply INR_fact_neq_0. @@ -240,7 +240,7 @@ rewrite Rmult_1_l. rewrite Rinv_mult_distr. replace (2 * i - 2 * i0)%nat with (2 * (i - i0))%nat. reflexivity. -omega. +lia. apply INR_fact_neq_0. apply INR_fact_neq_0. apply INR_fact_neq_0. diff --git a/theories/Reals/DiscrR.v b/theories/Reals/DiscrR.v index 9205df1bb7..2ae93c8705 100644 --- a/theories/Reals/DiscrR.v +++ b/theories/Reals/DiscrR.v @@ -9,7 +9,7 @@ (************************************************************************) Require Import RIneq. -Require Import Omega. +Require Import Lia. Local Open Scope R_scope. Lemma Rlt_R0_R2 : 0 < 2. @@ -49,7 +49,7 @@ Ltac omega_sup := repeat rewrite <- plus_IZR || rewrite <- mult_IZR || rewrite <- Ropp_Ropp_IZR || rewrite Z_R_minus; - apply IZR_lt; omega. + apply IZR_lt; lia. Ltac prove_sup := match goal with diff --git a/theories/Reals/Exp_prop.v b/theories/Reals/Exp_prop.v index 1636d81d25..2c822da055 100644 --- a/theories/Reals/Exp_prop.v +++ b/theories/Reals/Exp_prop.v @@ -17,7 +17,7 @@ Require Import PSeries_reg. Require Import Div2. Require Import Even. Require Import Max. -Require Import Omega. +Require Import Lia. Local Open Scope nat_scope. Local Open Scope R_scope. @@ -488,8 +488,8 @@ Proof. rewrite div2_S_double. apply S_pred with 0%nat; apply H3. reflexivity. - omega. - omega. + lia. + lia. rewrite H2. replace (pred (S (2 * N0))) with (2 * N0)%nat; [ idtac | reflexivity ]. replace (S (S (2 * N0))) with (2 * S N0)%nat. @@ -549,15 +549,15 @@ Proof. rewrite H6. replace (pred (2 * N1)) with (S (2 * pred N1)). rewrite div2_S_double. - omega. - omega. + lia. + lia. assert (0 < n)%nat. apply lt_le_trans with 2%nat. apply lt_O_Sn. apply le_trans with (max (2 * S N0) 2). apply le_max_r. apply H3. - omega. + lia. rewrite H6. replace (pred (S (2 * N1))) with (2 * N1)%nat. rewrite div2_double. diff --git a/theories/Reals/Machin.v b/theories/Reals/Machin.v index 08bc38a085..d5a39f527f 100644 --- a/theories/Reals/Machin.v +++ b/theories/Reals/Machin.v @@ -8,7 +8,7 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -Require Import Omega. +Require Import Lia. Require Import Lra. Require Import Rbase. Require Import Rtrigo1. @@ -163,8 +163,8 @@ assert (cv : Un_cv PI_2_3_7_tg 0). rewrite <- (Rmult_0_r 2), <- Ropp_mult_distr_r_reverse. rewrite <- Rmult_plus_distr_l, Rabs_mult, (Rabs_pos_eq 2);[|lra]. rewrite Rmult_assoc; apply Rmult_lt_compat_l;[lra | ]. - apply (Pn1 n); omega. - apply (Pn2 n); omega. + apply (Pn1 n); lia. + apply (Pn2 n); lia. rewrite Machin_2_3_7. rewrite !atan_eq_ps_atan; try (split; lra). unfold ps_atan; destruct (in_int (/3)); destruct (in_int (/7)); diff --git a/theories/Reals/RIneq.v b/theories/Reals/RIneq.v index 7813c7b975..229e6018ca 100644 --- a/theories/Reals/RIneq.v +++ b/theories/Reals/RIneq.v @@ -19,7 +19,7 @@ Require Export Raxioms. Require Import Rpow_def. Require Import Zpower. Require Export ZArithRing. -Require Import Omega. +Require Import Lia. Require Export RealField. Local Open Scope Z_scope. @@ -1875,7 +1875,7 @@ Lemma eq_IZR : forall n m:Z, IZR n = IZR m -> n = m. Proof. intros z1 z2 H; generalize (Rminus_diag_eq (IZR z1) (IZR z2) H); rewrite (Z_R_minus z1 z2); intro; generalize (eq_IZR_R0 (z1 - z2) H0); - intro; omega. + intro; lia. Qed. (**********) @@ -1913,21 +1913,21 @@ Qed. Lemma IZR_ge : forall n m:Z, (n >= m)%Z -> IZR n >= IZR m. Proof. intros m n H; apply Rnot_lt_ge; red; intro. - generalize (lt_IZR m n H0); intro; omega. + generalize (lt_IZR m n H0); intro; lia. Qed. Lemma IZR_le : forall n m:Z, (n <= m)%Z -> IZR n <= IZR m. Proof. intros m n H; apply Rnot_gt_le; red; intro. - unfold Rgt in H0; generalize (lt_IZR n m H0); intro; omega. + unfold Rgt in H0; generalize (lt_IZR n m H0); intro; lia. Qed. Lemma IZR_lt : forall n m:Z, (n < m)%Z -> IZR n < IZR m. Proof. intros m n H; cut (m <= n)%Z. intro H0; elim (IZR_le m n H0); intro; auto. - generalize (eq_IZR m n H1); intro; exfalso; omega. - omega. + generalize (eq_IZR m n H1); intro; exfalso; lia. + lia. Qed. Lemma IZR_neq : forall z1 z2:Z, z1 <> z2 -> IZR z1 <> IZR z2. @@ -1954,7 +1954,7 @@ Lemma one_IZR_r_R1 : forall r (n m:Z), r < IZR n <= r + 1 -> r < IZR m <= r + 1 -> n = m. Proof. intros r z x [H1 H2] [H3 H4]. - cut ((z - x)%Z = 0%Z); auto with zarith. + cut ((z - x)%Z = 0%Z). lia. apply one_IZR_lt1. rewrite <- Z_R_minus; split. replace (-1) with (r - (r + 1)). diff --git a/theories/Reals/R_Ifp.v b/theories/Reals/R_Ifp.v index 5365e04000..5f0747d869 100644 --- a/theories/Reals/R_Ifp.v +++ b/theories/Reals/R_Ifp.v @@ -14,7 +14,7 @@ (**********************************************************) Require Import Rbase. -Require Import Omega. +Require Import Lia. Local Open Scope R_scope. (*********************************************************) @@ -60,7 +60,7 @@ Proof. apply lt_IZR in H1. rewrite <- minus_IZR in H2. apply le_IZR in H2. - omega. + lia. Qed. (**********) @@ -230,7 +230,7 @@ Proof. rewrite <- (plus_IZR (Int_part r1 - Int_part r2) 1) in H; generalize (up_tech (r1 - r2) (Int_part r1 - Int_part r2) H0 H); intros; clear H H0; unfold Int_part at 1; - omega. + lia. Qed. (**********) @@ -314,7 +314,7 @@ Proof. in H0; fold (IZR (Int_part r1) - IZR (Int_part r2) - 1) in H0; rewrite (Z_R_minus (Int_part r1) (Int_part r2)) in H0; rewrite (Z_R_minus (Int_part r1) (Int_part r2)) in H; - auto with zarith real. + auto with real. change (_ + -1) with (IZR (Int_part r1 - Int_part r2) - 1) in H; rewrite (Z_R_minus (Int_part r1 - Int_part r2) 1) in H; rewrite (Z_R_minus (Int_part r1 - Int_part r2) 1) in H0; @@ -323,7 +323,7 @@ Proof. intro; clear H; generalize (up_tech (r1 - r2) (Int_part r1 - Int_part r2 - 1) H1 H0); intros; clear H0 H1; unfold Int_part at 1; - omega. + lia. Qed. (**********) @@ -430,14 +430,14 @@ Proof. clear a b; change 2 with (1 + 1) in H0; rewrite <- (Rplus_assoc (IZR (Int_part r1) + IZR (Int_part r2)) 1 1) in H0; - auto with zarith real. + auto with real. rewrite <- (plus_IZR (Int_part r1) (Int_part r2)) in H; rewrite <- (plus_IZR (Int_part r1) (Int_part r2)) in H0; rewrite <- (plus_IZR (Int_part r1 + Int_part r2) 1) in H; rewrite <- (plus_IZR (Int_part r1 + Int_part r2) 1) in H0; rewrite <- (plus_IZR (Int_part r1 + Int_part r2 + 1) 1) in H0; generalize (up_tech (r1 + r2) (Int_part r1 + Int_part r2 + 1) H H0); - intro; clear H H0; unfold Int_part at 1; omega. + intro; clear H H0; unfold Int_part at 1; lia. Qed. (**********) @@ -499,7 +499,7 @@ Proof. rewrite <- (plus_IZR (Int_part r1 + Int_part r2) 1) in H1; generalize (up_tech (r1 + r2) (Int_part r1 + Int_part r2) H0 H1); intro; clear H0 H1; unfold Int_part at 1; - omega. + lia. Qed. (**********) @@ -522,7 +522,7 @@ Proof. rewrite (Rplus_assoc (r1 + r2) (- (IZR (Int_part r1) + IZR (Int_part r2))) (-(1))) ; rewrite <- (Ropp_plus_distr (IZR (Int_part r1) + IZR (Int_part r2)) 1); - trivial with zarith real. + trivial with real. Qed. (**********) diff --git a/theories/Reals/Ranalysis2.v b/theories/Reals/Ranalysis2.v index 7a838f2772..3f560f202e 100644 --- a/theories/Reals/Ranalysis2.v +++ b/theories/Reals/Ranalysis2.v @@ -11,7 +11,6 @@ Require Import Rbase. Require Import Rfunctions. Require Import Ranalysis1. -Require Import Omega. Local Open Scope R_scope. (**********) diff --git a/theories/Reals/Ranalysis5.v b/theories/Reals/Ranalysis5.v index ca82222c25..11835bd24a 100644 --- a/theories/Reals/Ranalysis5.v +++ b/theories/Reals/Ranalysis5.v @@ -16,7 +16,7 @@ Require Import Lra. Require Import RiemannInt. Require Import SeqProp. Require Import Max. -Require Import Omega. +Require Import Lia. Require Import Lra. Local Open Scope R_scope. @@ -1095,11 +1095,11 @@ assert (Main : Rabs ((f (x+h) - fn N (x+h)) - (f x - fn N x) + (fn N (x+h) - fn apply Rlt_trans with (Rabs h * eps / 4 + Rabs (f x - fn N x) + Rabs h * Rabs (fn' N c - g x)). apply Rplus_lt_compat_r ; apply Rplus_lt_compat_r ; unfold R_dist in fnxh_CV_fxh ; rewrite Rabs_minus_sym ; apply fnxh_CV_fxh. - unfold N; omega. + unfold N; lia. apply Rlt_trans with (Rabs h * eps / 4 + Rabs h * eps / 4 + Rabs h * Rabs (fn' N c - g x)). apply Rplus_lt_compat_r ; apply Rplus_lt_compat_l. unfold R_dist in fnx_CV_fx ; rewrite Rabs_minus_sym ; apply fnx_CV_fx. - unfold N ; omega. + unfold N ; lia. replace (fn' N c - g x) with ((fn' N c - g c) + (g c - g x)) by field. apply Rle_lt_trans with (Rabs h * eps / 4 + Rabs h * eps / 4 + Rabs h * Rabs (fn' N c - g c) + Rabs h * Rabs (g c - g x)). @@ -1113,7 +1113,7 @@ assert (Main : Rabs ((f (x+h) - fn N (x+h)) - (f x - fn N x) + (fn N (x+h) - fn apply Rplus_lt_compat_r; apply Rplus_lt_compat_l; apply Rmult_lt_compat_l. apply Rabs_pos_lt ; assumption. rewrite Rabs_minus_sym ; apply fn'c_CVU_gc. - unfold N ; omega. + unfold N ; lia. assert (t : Boule x delta c). destruct P. apply Rabs_def2 in xhinbxdelta; destruct xhinbxdelta. @@ -1201,11 +1201,11 @@ assert (Main : Rabs ((f (x+h) - fn N (x+h)) - (f x - fn N x) + (fn N (x+h) - fn apply Rlt_trans with (Rabs h * eps / 4 + Rabs (f x - fn N x) + Rabs h * Rabs (fn' N c - g x)). apply Rplus_lt_compat_r ; apply Rplus_lt_compat_r ; unfold R_dist in fnxh_CV_fxh ; rewrite Rabs_minus_sym ; apply fnxh_CV_fxh. - unfold N; omega. + unfold N; lia. apply Rlt_trans with (Rabs h * eps / 4 + Rabs h * eps / 4 + Rabs h * Rabs (fn' N c - g x)). apply Rplus_lt_compat_r ; apply Rplus_lt_compat_l. unfold R_dist in fnx_CV_fx ; rewrite Rabs_minus_sym ; apply fnx_CV_fx. - unfold N ; omega. + unfold N ; lia. replace (fn' N c - g x) with ((fn' N c - g c) + (g c - g x)) by field. apply Rle_lt_trans with (Rabs h * eps / 4 + Rabs h * eps / 4 + Rabs h * Rabs (fn' N c - g c) + Rabs h * Rabs (g c - g x)). @@ -1219,7 +1219,7 @@ assert (Main : Rabs ((f (x+h) - fn N (x+h)) - (f x - fn N x) + (fn N (x+h) - fn apply Rplus_lt_compat_r; apply Rplus_lt_compat_l; apply Rmult_lt_compat_l. apply Rabs_pos_lt ; assumption. rewrite Rabs_minus_sym ; apply fn'c_CVU_gc. - unfold N ; omega. + unfold N ; lia. assert (t : Boule x delta c). destruct P. apply Rabs_def2 in xhinbxdelta; destruct xhinbxdelta. diff --git a/theories/Reals/Ratan.v b/theories/Reals/Ratan.v index 57bc89b7e5..e822b87cc6 100644 --- a/theories/Reals/Ratan.v +++ b/theories/Reals/Ratan.v @@ -20,7 +20,7 @@ Require Import SeqProp. Require Import Ranalysis5. Require Import SeqSeries. Require Import PartSum. -Require Import Omega. +Require Import Lia. Local Open Scope R_scope. @@ -76,30 +76,30 @@ clear. intros [ | n] P Hs Ho;[solve[apply Ho, Hs] | apply Hs; auto with arith]. intros N; pattern N; apply WLOG; clear N. intros [ | N] Npos n decr to0 cv nN. - clear -Npos; elimtype False; omega. + lia. assert (decr' : Un_decreasing (fun i => f (S N + i)%nat)). intros k; replace (S N+S k)%nat with (S (S N+k)) by ring. apply (decr (S N + k)%nat). assert (to' : Un_cv (fun i => f (S N + i)%nat) 0). intros eps ep; destruct (to0 eps ep) as [M PM]. - exists M; intros k kM; apply PM; omega. + exists M; intros k kM; apply PM; lia. assert (cv' : Un_cv (sum_f_R0 (tg_alt (fun i => ((-1) ^ S N * f(S N + i)%nat)))) (l - sum_f_R0 (tg_alt f) N)). intros eps ep; destruct (cv eps ep) as [M PM]; exists M. intros n' nM. match goal with |- ?C => set (U := C) end. - assert (nM' : (n' + S N >= M)%nat) by omega. + assert (nM' : (n' + S N >= M)%nat) by lia. generalize (PM _ nM'); unfold R_dist. rewrite (tech2 (tg_alt f) N (n' + S N)). assert (t : forall a b c, (a + b) - c = b - (c - a)) by (intros; ring). rewrite t; clear t; unfold U, R_dist; clear U. - replace (n' + S N - S N)%nat with n' by omega. + replace (n' + S N - S N)%nat with n' by lia. rewrite <- (sum_eq (tg_alt (fun i => (-1) ^ S N * f(S N + i)%nat))). tauto. intros i _; unfold tg_alt. rewrite <- Rmult_assoc, <- pow_add, !(plus_comm i); reflexivity. - omega. + lia. assert (cv'' : Un_cv (sum_f_R0 (tg_alt (fun i => f (S N + i)%nat))) ((-1) ^ S N * (l - sum_f_R0 (tg_alt f) N))). apply (Un_cv_ext (fun n => (-1) ^ S N * @@ -118,7 +118,7 @@ intros [ | N] Npos n decr to0 cv nN. rewrite neven. destruct (alternated_series_ineq _ _ p' decr to0 cv) as [D E]. unfold R_dist; rewrite Rabs_pos_eq;[ | lra]. - assert (dist : (p <= p')%nat) by omega. + assert (dist : (p <= p')%nat) by lia. assert (t := decreasing_prop _ _ _ (CV_ALT_step1 f decr) dist). apply Rle_trans with (sum_f_R0 (tg_alt f) (2 * p) - l). unfold Rminus; apply Rplus_le_compat_r; exact t. @@ -129,7 +129,7 @@ intros [ | N] Npos n decr to0 cv nN. rewrite nodd; destruct (alternated_series_ineq _ _ p' decr to0 cv) as [D E]. unfold R_dist; rewrite <- Rabs_Ropp, Rabs_pos_eq, Ropp_minus_distr; [ | lra]. - assert (dist : (p <= p')%nat) by omega. + assert (dist : (p <= p')%nat) by lia. apply Rle_trans with (l - sum_f_R0 (tg_alt f) (S (2 * p))). unfold Rminus; apply Rplus_le_compat_l, Ropp_le_contravar. solve[apply Rge_le, (growing_prop _ _ _ (CV_ALT_step0 f decr) dist)]. @@ -142,11 +142,11 @@ intros [ | N] Npos n decr to0 cv nN. rewrite neven; destruct (alternated_series_ineq _ _ p' decr to0 cv) as [D E]. unfold R_dist; rewrite Rabs_pos_eq;[ | lra]. - assert (dist : (S p < S p')%nat) by omega. + assert (dist : (S p < S p')%nat) by lia. apply Rle_trans with (sum_f_R0 (tg_alt f) (2 * S p) - l). unfold Rminus; apply Rplus_le_compat_r, (decreasing_prop _ _ _ (CV_ALT_step1 f decr)). - omega. + lia. rewrite keep, tech5; unfold tg_alt at 2; rewrite <- keep, pow_1_even. lra. rewrite nodd; destruct (alternated_series_ineq _ _ p' decr to0 cv) as [D E]. @@ -154,7 +154,7 @@ intros [ | N] Npos n decr to0 cv nN. rewrite Ropp_minus_distr. apply Rle_trans with (l - sum_f_R0 (tg_alt f) (S (2 * p))). unfold Rminus; apply Rplus_le_compat_l, Ropp_le_contravar, Rge_le, - (growing_prop _ _ _ (CV_ALT_step0 f decr)); omega. + (growing_prop _ _ _ (CV_ALT_step0 f decr)); lia. generalize C; rewrite keep, tech5; unfold tg_alt. rewrite <- keep, pow_1_even. assert (t : forall a b c, a <= b + 1 * c -> a - b <= c) by (intros; lra). @@ -166,7 +166,7 @@ clear WLOG; intros Hyp [ | n] decr to0 cv _. intros [A B]; rewrite Rabs_pos_eq; lra. apply Rle_trans with (f 1%nat). apply (Hyp 1%nat (le_n 1) (S n) decr to0 cv). - omega. + lia. solve[apply decr]. Qed. @@ -746,7 +746,7 @@ intros x Hx n. apply Rlt_le. apply Rinv_0_lt_compat. apply lt_INR_0. - omega. + lia. destruct (proj1 Hx) as [Hx1|Hx1]. destruct (proj2 Hx) as [Hx2|Hx2]. (* . 0 < x < 1 *) @@ -762,7 +762,7 @@ intros x Hx n. rewrite Rmult_1_r. exact Hx1. exact Hx2. - omega. + lia. apply Rgt_not_eq. exact Hx1. (* . x = 1 *) @@ -771,13 +771,13 @@ intros x Hx n. apply Rle_refl. (* . x = 0 *) rewrite <- Hx1. - do 2 (rewrite pow_i ; [ idtac | omega ]). + do 2 (rewrite pow_i ; [ idtac | lia ]). apply Rle_refl. apply Rlt_le. apply Rinv_lt_contravar. - apply Rmult_lt_0_compat ; apply lt_INR_0 ; omega. + apply Rmult_lt_0_compat ; apply lt_INR_0 ; lia. apply lt_INR. - omega. + lia. Qed. Lemma Ratan_seq_converging : forall x, (0 <= x <= 1)%R -> Un_cv (Ratan_seq x) 0. @@ -808,7 +808,7 @@ intros x Hx eps Heps. apply Rlt_le. apply Rinv_0_lt_compat. apply lt_INR_0. - omega. + lia. apply pow_incr. exact Hx. rewrite pow1. @@ -817,15 +817,15 @@ intros x Hx eps Heps. rewrite Rmult_1_l. apply Rinv_le_contravar. apply lt_INR_0. - omega. + lia. apply le_INR. - omega. + lia. rewrite <- (Rinv_involutive eps). apply Rinv_lt_contravar. apply Rmult_lt_0_compat. auto with real. apply lt_INR_0. - omega. + lia. apply Rlt_trans with (INR N). destruct (archimed (/ eps)) as (H,_). assert (0 < up (/ eps))%Z. @@ -837,7 +837,7 @@ intros x Hx eps Heps. rewrite INR_IZR_INZ, positive_nat_Z. exact HN. apply lt_INR. - omega. + lia. apply Rgt_not_eq. exact Heps. apply Rle_ge. @@ -848,7 +848,7 @@ intros x Hx eps Heps. apply Rlt_le. apply Rinv_0_lt_compat. apply lt_INR_0. - omega. + lia. Qed. Definition ps_atan_exists_01 (x : R) (Hx:0 <= x <= 1) : @@ -1045,7 +1045,7 @@ intros x n x_lb ; unfold Datan_seq ; induction n. apply Rmult_gt_0_compat. replace (x^2) with (x*x) by field ; apply Rmult_gt_0_compat ; assumption. assumption. - replace (2 * S n)%nat with (S (S (2 * n))) by intuition. + replace (2 * S n)%nat with (S (S (2 * n))) by lia. simpl ; field. Qed. @@ -1067,8 +1067,7 @@ Lemma Datan_seq_increasing : forall x y n, (n > 0)%nat -> 0 <= x < y -> Datan_se Proof. intros x y n n_lb x_encad ; assert (x_pos : x >= 0) by intuition. assert (y_pos : y > 0). apply Rle_lt_trans with (r2:=x) ; intuition. - induction n. - apply False_ind ; intuition. + induction n. lia. clear -x_encad x_pos y_pos ; induction n ; unfold Datan_seq. case x_pos ; clear x_pos ; intro x_pos. simpl ; apply Rmult_gt_0_lt_compat ; intuition. lra. @@ -1077,14 +1076,14 @@ intros x y n n_lb x_encad ; assert (x_pos : x >= 0) by intuition. simpl ; field. intuition. assert (Hrew : forall a, a^(2 * S (S n)) = (a ^ 2) * (a ^ (2 * S n))). - clear ; intro a ; replace (2 * S (S n))%nat with (S (S (2 * S n)))%nat by intuition. + clear ; intro a ; replace (2 * S (S n))%nat with (S (S (2 * S n)))%nat by lia. simpl ; field. case x_pos ; clear x_pos ; intro x_pos. rewrite Hrew ; rewrite Hrew. apply Rmult_gt_0_lt_compat ; intuition. apply Rmult_gt_0_lt_compat ; intuition ; lra. rewrite x_pos. - rewrite pow_i ; intuition. + rewrite pow_i. intuition. lia. Qed. Lemma Datan_seq_decreasing : forall x, -1 < x -> x < 1 -> Un_decreasing (Datan_seq x). @@ -1101,7 +1100,7 @@ assert (intabs : 0 <= Rabs x < 1). split;[apply Rabs_pos | apply Rabs_def1]; tauto. apply (pow_lt_1_compat (Rabs x) 2) in intabs. tauto. -omega. +lia. Qed. Lemma Datan_seq_CV_0 : forall x, -1 < x -> x < 1 -> Un_cv (Datan_seq x) 0. @@ -1112,7 +1111,7 @@ assert (x_ub2 : Rabs (x^2) < 1). rewrite <- pow2_abs. assert (H: 0 <= Rabs x < 1) by (split;[apply Rabs_pos | apply Rabs_def1; auto]). - apply (pow_lt_1_compat _ 2) in H;[tauto | omega]. + apply (pow_lt_1_compat _ 2) in H;[tauto | lia]. elim (pow_lt_1_zero (x^2) x_ub2 eps eps_pos) ; intros N HN ; exists N ; intros n Hn. unfold R_dist, Datan_seq. replace (x ^ (2 * n) - 0) with ((x ^ 2) ^ n). apply HN ; assumption. @@ -1130,7 +1129,7 @@ assert (Tool2 : / (1 + x ^ 2) > 0). apply Rinv_0_lt_compat ; tauto. assert (x_ub2' : 0<= Rabs (x^2) < 1). rewrite Rabs_pos_eq, <- pow2_abs;[ | apply pow2_ge_0]. - apply pow_lt_1_compat;[split;[apply Rabs_pos | ] | omega]. + apply pow_lt_1_compat;[split;[apply Rabs_pos | ] | lia]. apply Rabs_def1; assumption. assert (x_ub2 : Rabs (x^2) < 1) by tauto. assert (eps'_pos : ((1+x^2)*eps) > 0). @@ -1164,7 +1163,7 @@ assert (tool : forall a b c, 0 < b -> a < b * c -> a * / b < c). assumption. field; apply Rgt_not_eq; exact bp. apply tool;[exact Tool1 | ]. -apply HN; omega. +apply HN; lia. Qed. Lemma Datan_CVU_prelim : forall c (r : posreal), Rabs c + r < 1 -> @@ -1187,7 +1186,7 @@ apply (Alt_CVU (fun x n => Datan_seq n x) intros x [ | n] inb. solve[unfold Datan_seq; apply Rle_refl]. rewrite <- (Datan_seq_Rabs x); apply Rlt_le, Datan_seq_increasing. - omega. + lia. apply Boule_lt in inb; intuition. solve[apply Rabs_pos]. apply Datan_seq_CV_0. @@ -1212,7 +1211,7 @@ assert (Tool : forall N, (-1) ^ (S (2 * N)) = - 1). rewrite <- pow_add. replace (2 + S (2 * n))%nat with (S (2 * S n))%nat. reflexivity. - intuition. + lia. intros N x x_lb x_ub. induction N. unfold Datan_seq, Ratan_seq, tg_alt ; simpl. @@ -1251,10 +1250,10 @@ intros N x x_lb x_ub. apply Rabs_pos_lt ; assumption. rewrite Rabs_right. replace 1 with (/1) by field. - apply Rinv_1_lt_contravar ; intuition. + apply Rinv_1_lt_contravar. lra. apply lt_1_INR; lia. apply Rgt_ge ; replace (INR (2 * S N + 1)) with (INR (2*S N) + 1) ; [apply RiemannInt.RinvN_pos | ]. - replace (2 * S N + 1)%nat with (S (2 * S N))%nat by intuition ; + replace (2 * S N + 1)%nat with (S (2 * S N))%nat by lia. rewrite S_INR ; reflexivity. apply Hdelta ; assumption. rewrite Rmult_minus_distr_l. @@ -1266,7 +1265,7 @@ intros N x x_lb x_ub. - (x ^ (2 * S N + 1) / INR (2 * S N + 1))) / h)) by intuition. apply Rplus_eq_compat_l. field. split ; [apply Rgt_not_eq|] ; intuition. - clear ; replace (pred (2 * S N + 1)) with (2 * S N)%nat by intuition. + clear ; replace (pred (2 * S N + 1)) with (2 * S N)%nat by lia. field ; apply Rgt_not_eq ; intuition. field ; split ; [apply Rgt_not_eq |] ; intuition. elim (Main (eps/3) eps_3_pos) ; intros delta2 Hdelta2. @@ -1314,7 +1313,7 @@ apply (Alt_CVU (fun i r => Ratan_seq r i) ps_atan PI_tg (/2) pos_half); intros x n b; apply Boule_half_to_interval in b. rewrite <- (Rmult_1_l (PI_tg n)); unfold Ratan_seq, PI_tg. apply Rmult_le_compat_r. - apply Rlt_le, Rinv_0_lt_compat, (lt_INR 0); omega. + apply Rlt_le, Rinv_0_lt_compat, (lt_INR 0); lia. rewrite <- (pow1 (2 * n + 1)); apply pow_incr; assumption. exact PI_tg_cv. Qed. @@ -1458,10 +1457,10 @@ rewrite Rplus_assoc ; apply Rabs_triang. apply Halpha ; split. unfold D_x, no_cond ; split ; [ | apply Rgt_not_eq ] ; intuition. intuition. - apply HN2; unfold N; omega. + apply HN2; unfold N; lia. lra. rewrite <- Rabs_Ropp, Ropp_minus_distr; apply HN1. - unfold N; omega. + unfold N; lia. lra. assumption. field. diff --git a/theories/Reals/Rderiv.v b/theories/Reals/Rderiv.v index effbc3a404..69a41db4db 100644 --- a/theories/Reals/Rderiv.v +++ b/theories/Reals/Rderiv.v @@ -17,7 +17,7 @@ Require Import Rbase. Require Import Rfunctions. Require Import Rlimit. Require Import Lra. -Require Import Omega. +Require Import Lia. Local Open Scope R_scope. (*********) @@ -341,7 +341,7 @@ Proof. rewrite cond in H2; rewrite cond; simpl in H2; simpl; cut (1 + x0 * 1 * 0 = 1 * 1); [ intro A; rewrite A in H2; assumption | ring ]. - cut (n0 <> 0%nat -> S (n0 - 1) = n0); [ intro | omega ]; + cut (n0 <> 0%nat -> S (n0 - 1) = n0); [ intro | lia ]; rewrite (H3 cond) in H2; rewrite (Rmult_comm (x0 ^ n0) (INR n0)) in H2; rewrite (tech_pow_Rplus x0 n0 n0) in H2; assumption. Qed. diff --git a/theories/Reals/Rfunctions.v b/theories/Reals/Rfunctions.v index 17b39d22cb..7f9e019c5b 100644 --- a/theories/Reals/Rfunctions.v +++ b/theories/Reals/Rfunctions.v @@ -25,7 +25,7 @@ Require Export R_sqr. Require Export SplitAbsolu. Require Export SplitRmult. Require Export ArithProp. -Require Import Omega. +Require Import Lia. Require Import Zpower. Local Open Scope nat_scope. Local Open Scope R_scope. @@ -122,7 +122,7 @@ Hint Resolve pow_lt: real. Lemma Rlt_pow_R1 : forall (x:R) (n:nat), 1 < x -> (0 < n)%nat -> 1 < x ^ n. Proof. intros x n; elim n; simpl; auto with real. - intros H' H'0; exfalso; omega. + intros H' H'0; exfalso; lia. intros n0; case n0. simpl; rewrite Rmult_1_r; auto. intros n1 H' H'0 H'1. @@ -262,14 +262,14 @@ Proof. elim (IZN (up (b * / (Rabs x - 1))) H2); intros; exists x0; apply (Rge_trans (INR x0) (IZR (up (b * / (Rabs x - 1)))) (b * / (Rabs x - 1))). - rewrite INR_IZR_INZ; apply IZR_ge; omega. + rewrite INR_IZR_INZ; apply IZR_ge; lia. unfold Rge; left; assumption. exists 0%nat; apply (Rge_trans (INR 0) (IZR (up (b * / (Rabs x - 1)))) (b * / (Rabs x - 1))). - rewrite INR_IZR_INZ; apply IZR_ge; simpl; omega. + rewrite INR_IZR_INZ; apply IZR_ge; simpl; lia. unfold Rge; left; assumption. - omega. + lia. Qed. Lemma pow_ne_zero : forall n:nat, n <> 0%nat -> 0 ^ n = 0. @@ -745,7 +745,7 @@ Proof. - now simpl; rewrite Rmult_1_l. - now rewrite <- !pow_powerRZ, Rpow_mult_distr. - destruct Hmxy as [H|H]. - + assert(m = 0) as -> by now omega. + + assert(m = 0) as -> by now lia. now rewrite <- Hm, Rmult_1_l. + assert(x0 <> 0)%R by now intros ->; apply H; rewrite Rmult_0_l. assert(y0 <> 0)%R by now intros ->; apply H; rewrite Rmult_0_r. @@ -808,7 +808,7 @@ Proof. ring. rewrite Rmult_plus_distr_r; rewrite Hrecn; cut ((n + 1)%nat = S n). intro H; rewrite H; simpl; ring. - omega. + lia. Qed. Lemma sum_f_R0_triangle : diff --git a/theories/Reals/Rprod.v b/theories/Reals/Rprod.v index 15ec7891f7..ed2c953449 100644 --- a/theories/Reals/Rprod.v +++ b/theories/Reals/Rprod.v @@ -14,7 +14,7 @@ Require Import Rfunctions. Require Import Rseries. Require Import PartSum. Require Import Binomial. -Require Import Omega. +Require Import Lia. Local Open Scope R_scope. (** TT Ak; 0<=k<=N *) @@ -34,16 +34,16 @@ Lemma prod_SO_split : prod_f_R0 An k * prod_f_R0 (fun l:nat => An (k +1+l)%nat) (n - k -1). Proof. intros; induction n as [| n Hrecn]. - absurd (k < 0)%nat; omega. - cut (k = n \/ (k < n)%nat);[intro; elim H0; intro|omega]. - replace (S n - k - 1)%nat with O; [rewrite H1; simpl|omega]. + absurd (k < 0)%nat; lia. + cut (k = n \/ (k < n)%nat);[intro; elim H0; intro|lia]. + replace (S n - k - 1)%nat with O; [rewrite H1; simpl|lia]. replace (n+1+0)%nat with (S n); ring. - replace (S n - k-1)%nat with (S (n - k-1));[idtac|omega]. + replace (S n - k-1)%nat with (S (n - k-1));[idtac|lia]. simpl; replace (k + S (n - k))%nat with (S n). replace (k + 1 + S (n - k - 1))%nat with (S n). rewrite Hrecn; [ ring | assumption ]. - omega. - omega. + lia. + lia. Qed. (**********) @@ -116,11 +116,11 @@ Proof. assert (forall (n:nat), (0 < n)%nat -> (if eq_nat_dec n 0 then 1 else INR n) = INR n). intros n; case (eq_nat_dec n 0); auto with real. - intros; absurd (0 < n)%nat; omega. + intros; absurd (0 < n)%nat; lia. intros; unfold Rsqr; repeat rewrite fact_prodSO. cut ((k=N)%nat \/ (k < N)%nat \/ (N < k)%nat). intro H2; elim H2; intro H3. - rewrite H3; replace (2*N-N)%nat with N;[right; ring|omega]. + rewrite H3; replace (2*N-N)%nat with N;[right; ring|lia]. case H3; intro; clear H2 H3. rewrite (prod_SO_split (fun l:nat => if eq_nat_dec l 0 then 1 else INR l) (2 * N - k) N). rewrite Rmult_assoc; apply Rmult_le_compat_l. @@ -133,12 +133,12 @@ Proof. apply prod_SO_Rle; intros; split; auto. rewrite H0. rewrite H0. - apply le_INR; omega. - omega. - omega. + apply le_INR; lia. + lia. + lia. assumption. - omega. - omega. + lia. + lia. rewrite <- (Rmult_comm (prod_f_R0 (fun l:nat => if eq_nat_dec l 0 then 1 else INR l) k)); rewrite (prod_SO_split (fun l:nat => @@ -154,13 +154,13 @@ Proof. apply prod_SO_Rle; intros; split; auto. rewrite H0. rewrite H0. - apply le_INR; omega. - omega. - omega. - omega. - omega. + apply le_INR; lia. + lia. + lia. + lia. + lia. assumption. - omega. + lia. Qed. @@ -192,5 +192,5 @@ Proof. reflexivity. rewrite mult_INR; apply prod_neq_R0; apply INR_fact_neq_0. apply prod_neq_R0; apply INR_fact_neq_0. - omega. + lia. Qed. diff --git a/theories/Reals/Rsigma.v b/theories/Reals/Rsigma.v index 2a9c6953c5..7577c4b7b0 100644 --- a/theories/Reals/Rsigma.v +++ b/theories/Reals/Rsigma.v @@ -12,7 +12,7 @@ Require Import Rbase. Require Import Rfunctions. Require Import Rseries. Require Import PartSum. -Require Import Omega. +Require Import Lia. Local Open Scope R_scope. Set Implicit Arguments. @@ -57,12 +57,12 @@ Section Sigma. ring. replace (high - S (S k))%nat with (high - S k - 1)%nat. apply pred_of_minus. - omega. + lia. unfold sigma; replace (S k - low)%nat with (S (k - low)). pattern (S k) at 1; replace (S k) with (low + S (k - low))%nat. symmetry ; apply (tech5 (fun i:nat => f (low + i))). - omega. - omega. + lia. + lia. rewrite <- H2; unfold sigma; rewrite <- minus_n_n; simpl; replace (high - S low)%nat with (pred (high - low)). replace (sum_f_R0 (fun k0:nat => f (S (low + k0))) (pred (high - low))) with @@ -73,7 +73,7 @@ Section Sigma. apply sum_eq; intros; replace (S (low + i)) with (low + S i)%nat. reflexivity. ring. - omega. + lia. inversion H; [ right; reflexivity | left; assumption ]. Qed. diff --git a/theories/Reals/Rtrigo1.v b/theories/Reals/Rtrigo1.v index 0df1442f46..c2651d4120 100644 --- a/theories/Reals/Rtrigo1.v +++ b/theories/Reals/Rtrigo1.v @@ -18,7 +18,7 @@ Require Export Cos_rel. Require Export Cos_plus. Require Import ZArith_base. Require Import Zcomplements. -Import Omega. +Require Import Lia. Require Import Lra. Require Import Ranalysis1. Require Import Rsqrt_def. @@ -1741,7 +1741,7 @@ Proof. replace (3*(PI/2)) with (PI/2 + PI) in GT by field. rewrite Rplus_comm in GT. now apply Rplus_lt_reg_l in GT. } - omega. + lia. Qed. Lemma cos_eq_0_2PI_1 (x:R) : diff --git a/theories/Reals/SeqProp.v b/theories/Reals/SeqProp.v index d73f6ce0f3..34ea323a95 100644 --- a/theories/Reals/SeqProp.v +++ b/theories/Reals/SeqProp.v @@ -12,7 +12,7 @@ Require Import Rbase. Require Import Rfunctions. Require Import Rseries. Require Import Max. -Require Import Omega. +Require Import Lia. Local Open Scope R_scope. (*****************************************************************) @@ -1155,7 +1155,7 @@ Proof. rewrite Rmult_1_r; apply Rle_trans with (INR M_nat). left; rewrite INR_IZR_INZ. rewrite <- H4; assert (H8 := archimed (Rabs x)); elim H8; intros; assumption. - apply le_INR; omega. + apply le_INR; lia. apply INR_fact_neq_0. apply INR_fact_neq_0. ring. diff --git a/toplevel/coqc.ml b/toplevel/coqc.ml index 642dc94ab2..98206fb341 100644 --- a/toplevel/coqc.ml +++ b/toplevel/coqc.ml @@ -53,11 +53,7 @@ let coqc_main copts ~opts = if opts.Coqargs.post.Coqargs.output_context then begin let sigma, env = let e = Global.env () in Evd.from_env e, e in - let library_accessor = Library.indirect_accessor in - let mod_ops = { Printmod.import_module = Declaremods.import_module - ; process_module_binding = Declaremods.process_module_binding - } in - Feedback.msg_notice Pp.(Flags.(with_option raw_print (Prettyp.print_full_pure_context ~mod_ops ~library_accessor env) sigma) ++ fnl ()) + Feedback.msg_notice Pp.(Flags.(with_option raw_print (Prettyp.print_full_pure_context env) sigma) ++ fnl ()) end; CProfile.print_profile () diff --git a/vernac/attributes.ml b/vernac/attributes.ml index 6af454eee5..b7a3b002bd 100644 --- a/vernac/attributes.ml +++ b/vernac/attributes.ml @@ -18,13 +18,17 @@ and vernac_flag_value = | VernacFlagLeaf of string | VernacFlagList of vernac_flags +let warn_unsupported_attributes = + CWarnings.create ~name:"unsupported-attributes" ~category:"parsing" ~default:CWarnings.AsError + (fun atts -> + let keys = List.map fst atts in + let keys = List.sort_uniq String.compare keys in + let conj = match keys with [_] -> "this attribute: " | _ -> "these attributes: " in + Pp.(str "This command does not support " ++ str conj ++ prlist str keys ++ str".")) + let unsupported_attributes = function | [] -> () - | atts -> - let keys = List.map fst atts in - let keys = List.sort_uniq String.compare keys in - let conj = match keys with [_] -> "this attribute: " | _ -> "these attributes: " in - user_err Pp.(str "This command does not support " ++ str conj ++ prlist str keys ++ str".") + | atts -> warn_unsupported_attributes atts type 'a key_parser = 'a option -> vernac_flag_value -> 'a diff --git a/vernac/comArguments.ml b/vernac/comArguments.ml new file mode 100644 index 0000000000..737e0427ec --- /dev/null +++ b/vernac/comArguments.ml @@ -0,0 +1,306 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +open CAst +open Util +open Names +open Vernacexpr + +let smart_global r = + let gr = Smartlocate.smart_global r in + Dumpglob.add_glob ?loc:r.loc gr; + gr + +let cache_bidi_hints (_name, (gr, ohint)) = + match ohint with + | None -> Pretyping.clear_bidirectionality_hint gr + | Some nargs -> Pretyping.add_bidirectionality_hint gr nargs + +let load_bidi_hints _ r = + cache_bidi_hints r + +let subst_bidi_hints (subst, (gr, ohint as orig)) = + let gr' = Globnames.subst_global_reference subst gr in + if gr == gr' then orig else (gr', ohint) + +let discharge_bidi_hints (_name, (gr, ohint)) = + if Globnames.isVarRef gr && Lib.is_in_section gr then None + else + let vars = Lib.variable_section_segment_of_reference gr in + let n = List.length vars in + Some (gr, Option.map ((+) n) ohint) + +let inBidiHints = + let open Libobject in + declare_object { (default_object "BIDIRECTIONALITY-HINTS" ) with + load_function = load_bidi_hints; + cache_function = cache_bidi_hints; + classify_function = (fun o -> Substitute o); + subst_function = subst_bidi_hints; + discharge_function = discharge_bidi_hints; + } + + +let warn_arguments_assert = + CWarnings.create ~name:"arguments-assert" ~category:"vernacular" + Pp.(fun sr -> + strbrk "This command is just asserting the names of arguments of " ++ + Printer.pr_global sr ++ strbrk". If this is what you want add " ++ + strbrk "': assert' to silence the warning. If you want " ++ + strbrk "to clear implicit arguments add ': clear implicits'. " ++ + strbrk "If you want to clear notation scopes add ': clear scopes'") + +(* [nargs_for_red] is the number of arguments required to trigger reduction, + [args] is the main list of arguments statuses, + [more_implicits] is a list of extra lists of implicit statuses *) +let vernac_arguments ~section_local reference args more_implicits nargs_for_red nargs_before_bidi flags = + let env = Global.env () in + let sigma = Evd.from_env env in + let assert_flag = List.mem `Assert flags in + let rename_flag = List.mem `Rename flags in + let clear_scopes_flag = List.mem `ClearScopes flags in + let extra_scopes_flag = List.mem `ExtraScopes flags in + let clear_implicits_flag = List.mem `ClearImplicits flags in + let default_implicits_flag = List.mem `DefaultImplicits flags in + let never_unfold_flag = List.mem `ReductionNeverUnfold flags in + let nomatch_flag = List.mem `ReductionDontExposeCase flags in + let clear_bidi_hint = List.mem `ClearBidiHint flags in + + let err_incompat x y = + CErrors.user_err Pp.(str ("Options \""^x^"\" and \""^y^"\" are incompatible.")) in + + if assert_flag && rename_flag then + err_incompat "assert" "rename"; + if clear_scopes_flag && extra_scopes_flag then + err_incompat "clear scopes" "extra scopes"; + if clear_implicits_flag && default_implicits_flag then + err_incompat "clear implicits" "default implicits"; + + let sr = smart_global reference in + let inf_names = + let ty, _ = Typeops.type_of_global_in_context env sr in + Impargs.compute_implicits_names env sigma (EConstr.of_constr ty) + in + let prev_names = + try Arguments_renaming.arguments_names sr with Not_found -> inf_names + in + let num_args = List.length inf_names in + assert (Int.equal num_args (List.length prev_names)); + + let names_of args = List.map (fun a -> a.name) args in + + (* Checks *) + + let err_extra_args names = + CErrors.user_err ~hdr:"vernac_declare_arguments" + Pp.(strbrk "Extra arguments: " ++ + prlist_with_sep pr_comma Name.print names ++ str ".") + in + let err_missing_args names = + CErrors.user_err ~hdr:"vernac_declare_arguments" + Pp.(strbrk "The following arguments are not declared: " ++ + prlist_with_sep pr_comma Name.print names ++ str ".") + in + + let rec check_extra_args extra_args = + match extra_args with + | [] -> () + | { notation_scope = None } :: _ -> + CErrors.user_err Pp.(str"Extra arguments should specify a scope.") + | { notation_scope = Some _ } :: args -> check_extra_args args + in + + let args, scopes = + let scopes = List.map (fun { notation_scope = s } -> s) args in + if List.length args > num_args then + let args, extra_args = List.chop num_args args in + if extra_scopes_flag then + (check_extra_args extra_args; (args, scopes)) + else err_extra_args (names_of extra_args) + else args, scopes + in + + if Option.cata (fun n -> n > num_args) false nargs_for_red then + CErrors.user_err Pp.(str "The \"/\" modifier should be put before any extra scope."); + + if Option.cata (fun n -> n > num_args) false nargs_before_bidi then + CErrors.user_err Pp.(str "The \"&\" modifier should be put before any extra scope."); + + let scopes_specified = List.exists Option.has_some scopes in + + if scopes_specified && clear_scopes_flag then + CErrors.user_err Pp.(str "The \"clear scopes\" flag is incompatible with scope annotations."); + + let names = List.map (fun { name } -> name) args in + let names = names :: List.map (List.map fst) more_implicits in + + let rename_flag_required = ref false in + let example_renaming = ref None in + let save_example_renaming renaming = + rename_flag_required := !rename_flag_required + || not (Name.equal (fst renaming) Anonymous); + if Option.is_empty !example_renaming then + example_renaming := Some renaming + in + + let rec names_union names1 names2 = + match names1, names2 with + | [], [] -> [] + | _ :: _, [] -> names1 + | [], _ :: _ -> names2 + | (Name _ as name) :: names1, Anonymous :: names2 + | Anonymous :: names1, (Name _ as name) :: names2 -> + name :: names_union names1 names2 + | name1 :: names1, name2 :: names2 -> + if Name.equal name1 name2 then + name1 :: names_union names1 names2 + else CErrors.user_err Pp.(str "Argument lists should agree on the names they provide.") + in + + let names = List.fold_left names_union [] names in + + let rec rename prev_names names = + match prev_names, names with + | [], [] -> [] + | [], _ :: _ -> err_extra_args names + | _ :: _, [] when assert_flag -> + (* Error messages are expressed in terms of original names, not + renamed ones. *) + err_missing_args (List.lastn (List.length prev_names) inf_names) + | _ :: _, [] -> prev_names + | prev :: prev_names, Anonymous :: names -> + prev :: rename prev_names names + | prev :: prev_names, (Name id as name) :: names -> + if not (Name.equal prev name) then save_example_renaming (prev,name); + name :: rename prev_names names + in + + let names = rename prev_names names in + let renaming_specified = Option.has_some !example_renaming in + + if !rename_flag_required && not rename_flag then begin + let msg = let open Pp in + match !example_renaming with + | None -> + strbrk "To rename arguments the \"rename\" flag must be specified." + | Some (o,n) -> + strbrk "Flag \"rename\" expected to rename " ++ Name.print o ++ + strbrk " into " ++ Name.print n ++ str "." + in CErrors.user_err ~hdr:"vernac_declare_arguments" msg + end; + + let duplicate_names = + List.duplicates Name.equal (List.filter ((!=) Anonymous) names) + in + if not (List.is_empty duplicate_names) then begin + CErrors.user_err Pp.(strbrk "Some argument names are duplicated: " ++ + prlist_with_sep pr_comma Name.print duplicate_names) + end; + + let implicits = + List.map (fun { name; implicit_status = i } -> (name,i)) args + in + let implicits = implicits :: more_implicits in + + let implicits = List.map (List.map snd) implicits in + let implicits_specified = match implicits with + | [l] -> List.exists (function Impargs.NotImplicit -> false | _ -> true) l + | _ -> true in + + if implicits_specified && clear_implicits_flag then + CErrors.user_err Pp.(str "The \"clear implicits\" flag is incompatible with implicit annotations"); + + if implicits_specified && default_implicits_flag then + CErrors.user_err Pp.(str "The \"default implicits\" flag is incompatible with implicit annotations"); + + let rargs = + Util.List.map_filter (function (n, true) -> Some n | _ -> None) + (Util.List.map_i (fun i { recarg_like = b } -> i, b) 0 args) + in + + let red_behavior = + let open Reductionops.ReductionBehaviour in + match never_unfold_flag, nomatch_flag, rargs, nargs_for_red with + | true, false, [], None -> Some NeverUnfold + | true, true, _, _ -> err_incompat "simpl never" "simpl nomatch" + | true, _, _::_, _ -> err_incompat "simpl never" "!" + | true, _, _, Some _ -> err_incompat "simpl never" "/" + | false, false, [], None -> None + | false, false, _, _ -> Some (UnfoldWhen { nargs = nargs_for_red; + recargs = rargs; + }) + | false, true, _, _ -> Some (UnfoldWhenNoMatch { nargs = nargs_for_red; + recargs = rargs; + }) + in + + + let red_modifiers_specified = Option.has_some red_behavior in + + let bidi_hint_specified = Option.has_some nargs_before_bidi in + + if bidi_hint_specified && clear_bidi_hint then + err_incompat "clear bidirectionality hint" "&"; + + + (* Actions *) + + if renaming_specified then begin + Arguments_renaming.rename_arguments section_local sr names + end; + + if scopes_specified || clear_scopes_flag then begin + let scopes = List.map (Option.map (fun {loc;v=k} -> + try ignore (Notation.find_scope k); k + with CErrors.UserError _ -> + Notation.find_delimiters_scope ?loc k)) scopes + in + Notation.declare_arguments_scope section_local (smart_global reference) scopes + end; + + if implicits_specified || clear_implicits_flag then + Impargs.set_implicits section_local (smart_global reference) implicits; + + if default_implicits_flag then + Impargs.declare_implicits section_local (smart_global reference); + + if red_modifiers_specified then begin + match sr with + | GlobRef.ConstRef _ -> + Reductionops.ReductionBehaviour.set + ~local:section_local sr (Option.get red_behavior) + + | _ -> + CErrors.user_err + Pp.(strbrk "Modifiers of the behavior of the simpl tactic "++ + strbrk "are relevant for constants only.") + end; + + if bidi_hint_specified then begin + let n = Option.get nargs_before_bidi in + if section_local then + Pretyping.add_bidirectionality_hint sr n + else + Lib.add_anonymous_leaf (inBidiHints (sr, Some n)) + end; + + if clear_bidi_hint then begin + if section_local then + Pretyping.clear_bidirectionality_hint sr + else + Lib.add_anonymous_leaf (inBidiHints (sr, None)) + end; + + if not (renaming_specified || + implicits_specified || + scopes_specified || + red_modifiers_specified || + bidi_hint_specified) && (List.is_empty flags) then + warn_arguments_assert sr diff --git a/vernac/comArguments.mli b/vernac/comArguments.mli new file mode 100644 index 0000000000..f78e01a11f --- /dev/null +++ b/vernac/comArguments.mli @@ -0,0 +1,19 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +val vernac_arguments + : section_local:bool + -> Libnames.qualid Constrexpr.or_by_notation + -> Vernacexpr.vernac_argument_status list + -> (Names.Name.t * Impargs.implicit_kind) list list + -> int option + -> int option + -> Vernacexpr.arguments_modifier list + -> unit diff --git a/vernac/declaremods.ml b/vernac/declaremods.ml index c7b68d18c2..65cd4cd6a4 100644 --- a/vernac/declaremods.ml +++ b/vernac/declaremods.ml @@ -1068,3 +1068,9 @@ let debug_print_modtab _ = in let modules = MPmap.fold pr_modinfo (ModObjs.all ()) (mt ()) in hov 0 modules + + +let mod_ops = { + Printmod.import_module = import_module; + process_module_binding = process_module_binding; +} diff --git a/vernac/declaremods.mli b/vernac/declaremods.mli index ae84704656..23f25bc597 100644 --- a/vernac/declaremods.mli +++ b/vernac/declaremods.mli @@ -126,3 +126,5 @@ val debug_print_modtab : unit -> Pp.t val process_module_binding : MBId.t -> Declarations.module_alg_expr -> unit + +val mod_ops : Printmod.mod_ops diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml index f91983d31c..3dbf7afb78 100644 --- a/vernac/ppvernac.ml +++ b/vernac/ppvernac.ml @@ -1082,8 +1082,13 @@ let string_of_definition_object_kind = let open Decls in function let rec print_arguments n nbidi l = match n, nbidi, l with | Some 0, _, l -> spc () ++ str"/" ++ print_arguments None nbidi l - | _, Some 0, l -> spc () ++ str"|" ++ print_arguments n None l - | _, _, [] -> mt() + | _, Some 0, l -> spc () ++ str"&" ++ print_arguments n None l + | None, None, [] -> mt() + | _, _, [] -> + let dummy = {name=Anonymous; recarg_like=false; + notation_scope=None; implicit_status=Impargs.NotImplicit} + in + print_arguments n nbidi [dummy] | n, nbidi, { name = id; recarg_like = k; notation_scope = s; implicit_status = imp } :: tl -> diff --git a/printing/prettyp.ml b/vernac/prettyp.ml index c995887f31..5ebc89892c 100644 --- a/printing/prettyp.ml +++ b/vernac/prettyp.ml @@ -17,7 +17,6 @@ open CErrors open Util open CAst open Names -open Nameops open Termops open Declarations open Environ @@ -30,25 +29,27 @@ open Printer open Printmod open Context.Rel.Declaration -(* module RelDecl = Context.Rel.Declaration *) +module RelDecl = Context.Rel.Declaration module NamedDecl = Context.Named.Declaration type object_pr = { print_inductive : MutInd.t -> UnivNames.univ_name_list option -> Pp.t; - print_constant_with_infos : Opaqueproof.indirect_accessor -> Constant.t -> UnivNames.univ_name_list option -> Pp.t; + print_constant_with_infos : Constant.t -> UnivNames.univ_name_list option -> Pp.t; print_section_variable : env -> Evd.evar_map -> variable -> Pp.t; print_syntactic_def : env -> KerName.t -> Pp.t; - print_module : mod_ops:Printmod.mod_ops -> bool -> ModPath.t -> Pp.t; - print_modtype : mod_ops:Printmod.mod_ops -> ModPath.t -> Pp.t; + print_module : bool -> ModPath.t -> Pp.t; + print_modtype : ModPath.t -> Pp.t; print_named_decl : env -> Evd.evar_map -> Constr.named_declaration -> Pp.t; - print_library_entry : mod_ops:Printmod.mod_ops -> Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> bool -> (object_name * Lib.node) -> Pp.t option; - print_context : mod_ops:Printmod.mod_ops -> Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> bool -> int option -> Lib.library_segment -> Pp.t; + print_library_entry : env -> Evd.evar_map -> bool -> (object_name * Lib.node) -> Pp.t option; + print_context : env -> Evd.evar_map -> bool -> int option -> Lib.library_segment -> Pp.t; print_typed_value_in_env : Environ.env -> Evd.evar_map -> EConstr.constr * EConstr.types -> Pp.t; print_eval : Reductionops.reduction_function -> env -> Evd.evar_map -> Constrexpr.constr_expr -> EConstr.unsafe_judgment -> Pp.t; } -let gallina_print_module = print_module -let gallina_print_modtype = print_modtype +let gallina_print_module = print_module ~mod_ops:Declaremods.mod_ops +let gallina_print_modtype = print_modtype ~mod_ops:Declaremods.mod_ops + + (**************) (** Utilities *) @@ -94,7 +95,7 @@ let print_ref reduce ref udecl = else mt () in let priv = None in (* We deliberately don't print private univs in About. *) - hov 0 (pr_global ref ++ inst ++ str " :" ++ spc () ++ pr_letype_env env sigma typ ++ + hov 0 (pr_global ref ++ inst ++ str " :" ++ spc () ++ pr_letype_env env sigma typ ++ Printer.pr_abstract_universe_ctx sigma ?variance univs ?priv) (********************************) @@ -123,25 +124,20 @@ let print_impargs_list prefix l = List.flatten (List.map (fun (cond,imps) -> match cond with | None -> - List.map (fun pp -> add_colon prefix ++ pp) - (print_one_impargs_list imps) + List.map (fun pp -> add_colon prefix ++ pp) + (print_one_impargs_list imps) | Some (n1,n2) -> [v 2 (prlist_with_sep cut (fun x -> x) - [(if ismt prefix then str "When" else prefix ++ str ", when") ++ - str " applied to " ++ - (if Int.equal n1 n2 then int_or_no n2 else - if Int.equal n1 0 then str "no more than " ++ int n2 - else int n1 ++ str " to " ++ int_or_no n2) ++ - str (String.plural n2 " argument") ++ str ":"; + [(if ismt prefix then str "When" else prefix ++ str ", when") ++ + str " applied to " ++ + (if Int.equal n1 n2 then int_or_no n2 else + if Int.equal n1 0 then str "no more than " ++ int n2 + else int n1 ++ str " to " ++ int_or_no n2) ++ + str (String.plural n2 " argument") ++ str ":"; v 0 (prlist_with_sep cut (fun x -> x) - (if List.exists is_status_implicit imps - then print_one_impargs_list imps - else [str "No implicit arguments"]))])]) l) - -let print_renames_list prefix l = - if List.is_empty l then [] else - [add_colon prefix ++ str "Arguments are renamed to " ++ - hv 2 (prlist_with_sep pr_comma (fun x -> x) (List.map Name.print l))] + (if List.exists is_status_implicit imps + then print_one_impargs_list imps + else [str "No implicit arguments"]))])]) l) let need_expansion impl ref = let typ, _ = Typeops.type_of_global_in_context (Global.env ()) ref in @@ -163,19 +159,6 @@ let print_impargs ref = else [str "No implicit arguments"])) (*********************) -(** Printing Scopes *) - -let print_argument_scopes prefix = function - | [Some sc] -> - [add_colon prefix ++ str"Argument scope is [" ++ str sc ++ str"]"] - | l when not (List.for_all Option.is_empty l) -> - [add_colon prefix ++ hov 2 (str"Argument scopes are" ++ spc() ++ - str "[" ++ - pr_sequence (function Some sc -> str sc | None -> str "_") l ++ - str "]")] - | _ -> [] - -(*********************) (** Printing Opacity *) type opacity = @@ -191,8 +174,8 @@ let opacity env = let cb = Environ.lookup_constant cst env in (match cb.const_body with | Undef _ | Primitive _ -> None - | OpaqueDef _ -> Some FullyOpaque - | Def _ -> Some + | OpaqueDef _ -> Some FullyOpaque + | Def _ -> Some (TransparentMaybeOpacified (Conv_oracle.get_strategy (Environ.oracle env) (ConstKey cst)))) | _ -> None @@ -254,19 +237,91 @@ let print_primitive_record recflag mipv = function | FakeRecord | NotRecord -> [] let print_primitive ref = - match ref with + match ref with | GlobRef.IndRef ind -> let mib,_ = Global.lookup_inductive ind in print_primitive_record mib.mind_finite mib.mind_packets mib.mind_record | _ -> [] -let print_name_infos ref = - let impls = implicits_of_global ref in +let needs_extra_scopes ref scopes = + let open Constr in + let rec aux env t = function + | [] -> false + | _::scopes -> match kind (Reduction.whd_all env t) with + | Prod (na,dom,codom) -> aux (push_rel (RelDecl.LocalAssum (na,dom)) env) codom scopes + | _ -> true + in + let env = Global.env() in + let ty, _ctx = Typeops.type_of_global_in_context env ref in + aux env ty scopes + +let implicit_kind_of_status = function + | None -> Anonymous, NotImplicit + | Some (id,_,(maximal,_)) -> Name id, if maximal then MaximallyImplicit else Implicit + +let is_dummy {Vernacexpr.implicit_status; name; recarg_like; notation_scope} = + name = Anonymous && not recarg_like && notation_scope = None && implicit_status = NotImplicit + +let rec main_implicits i renames recargs scopes impls = + if renames = [] && recargs = [] && scopes = [] && impls = [] then [] + else + let recarg_like, recargs = match recargs with + | j :: recargs when i = j -> true, recargs + | _ -> false, recargs + in + let (name, implicit_status) = + match renames, impls with + | _, (Some _ as i) :: _ -> implicit_kind_of_status i + | name::_, _ -> (name,NotImplicit) + | [], (None::_ | []) -> (Anonymous, NotImplicit) + in + let notation_scope = match scopes with + | scope :: _ -> Option.map CAst.make scope + | [] -> None + in + let status = {Vernacexpr.implicit_status; name; recarg_like; notation_scope} in + let tl = function [] -> [] | _::tl -> tl in + (* recargs is special -> tl handled above *) + let rest = main_implicits (i+1) (tl renames) recargs (tl scopes) (tl impls) in + if is_dummy status && rest = [] + then [] (* we may have a trail of dummies due to eg "clear scopes" *) + else status :: rest + +let print_arguments ref = + let qid = Nametab.shortest_qualid_of_global Id.Set.empty ref in + let flags, recargs, nargs_for_red = + let open Reductionops.ReductionBehaviour in + match get ref with + | None -> [], [], None + | Some NeverUnfold -> [`ReductionNeverUnfold], [], None + | Some (UnfoldWhen { nargs; recargs }) -> [], recargs, nargs + | Some (UnfoldWhenNoMatch { nargs; recargs }) -> [`ReductionDontExposeCase], recargs, nargs + in + let flags, renames = match Arguments_renaming.arguments_names ref with + | exception Not_found -> flags, [] + | [] -> flags, [] + | renames -> `Rename::flags, renames + in let scopes = Notation.find_arguments_scope ref in - let renames = - try Arguments_renaming.arguments_names ref with Not_found -> [] in + let flags = if needs_extra_scopes ref scopes then `ExtraScopes::flags else flags in + let impls = Impargs.extract_impargs_data (Impargs.implicits_of_global ref) in + let impls, moreimpls = match impls with + | (_, impls) :: rest -> impls, rest + | [] -> assert false + in + let impls = main_implicits 0 renames recargs scopes impls in + let moreimpls = List.map (fun (_,i) -> List.map implicit_kind_of_status i) moreimpls in + let bidi = Pretyping.get_bidirectionality_hint ref in + if impls = [] && moreimpls = [] && nargs_for_red = None && bidi = None && flags = [] then [] + else + let open Constrexpr in + let open Vernacexpr in + [Ppvernac.pr_vernac_expr + (VernacArguments (CAst.make (AN qid), impls, moreimpls, nargs_for_red, bidi, flags))] + +let print_name_infos ref = let type_info_for_implicit = - if need_expansion (select_impargs_size 0 impls) ref then + if need_expansion (select_impargs_size 0 (implicits_of_global ref)) ref then (* Need to reduce since implicits are computed with products flattened *) [str "Expanded type for implicit arguments"; print_ref true ref None; blankline] @@ -275,42 +330,15 @@ let print_name_infos ref = print_type_in_type ref @ print_primitive ref @ type_info_for_implicit @ - print_renames_list (mt()) renames @ - print_impargs_list (mt()) impls @ - print_argument_scopes (mt()) scopes @ + print_arguments ref @ print_if_is_coercion ref -let print_id_args_data test pr id l = - if List.exists test l then - pr (str "For " ++ Id.print id) l - else - [] - -let print_args_data_of_inductive_ids get test pr sp mipv = - List.flatten (Array.to_list (Array.mapi - (fun i mip -> - print_id_args_data test pr mip.mind_typename (get (GlobRef.IndRef (sp,i))) @ - List.flatten (Array.to_list (Array.mapi - (fun j idc -> - print_id_args_data test pr idc (get (GlobRef.ConstructRef ((sp,i),j+1)))) - mip.mind_consnames))) - mipv)) - -let print_inductive_implicit_args = - print_args_data_of_inductive_ids - implicits_of_global (fun l -> not (List.is_empty (positions_of_implicits l))) - print_impargs_list - -let print_inductive_renames = - print_args_data_of_inductive_ids - (fun r -> - try Arguments_renaming.arguments_names r with Not_found -> []) - ((!=) Anonymous) - print_renames_list - -let print_inductive_argument_scopes = - print_args_data_of_inductive_ids - Notation.find_arguments_scope (Option.has_some) print_argument_scopes +let print_inductive_args sp mipv = + let flatmapi f v = List.flatten (Array.to_list (Array.mapi f v)) in + flatmapi + (fun i mip -> print_arguments (GlobRef.IndRef (sp,i)) @ + flatmapi (fun j _ -> print_arguments (GlobRef.ConstructRef ((sp,i),j+1))) + mip.mind_consnames) mipv let print_bidi_hints gr = match Pretyping.get_bidirectionality_hint gr with @@ -367,10 +395,10 @@ let locate_any_name qid = let pr_located_qualid = function | Term ref -> let ref_str = let open GlobRef in match ref with - ConstRef _ -> "Constant" - | IndRef _ -> "Inductive" - | ConstructRef _ -> "Constructor" - | VarRef _ -> "Variable" in + ConstRef _ -> "Constant" + | IndRef _ -> "Inductive" + | ConstructRef _ -> "Constructor" + | VarRef _ -> "Variable" in str ref_str ++ spc () ++ pr_path (Nametab.path_of_global ref) | Syntactic kn -> str "Notation" ++ spc () ++ pr_path (Nametab.path_of_syndef kn) @@ -470,19 +498,19 @@ let print_located_qualid name flags qid = in match located with | [] -> - let (dir,id) = repr_qualid qid in - if DirPath.is_empty dir then - str "No " ++ str name ++ str " of basename" ++ spc () ++ Id.print id - else - str "No " ++ str name ++ str " of suffix" ++ spc () ++ pr_qualid qid + let (dir,id) = repr_qualid qid in + if DirPath.is_empty dir then + str "No " ++ str name ++ str " of basename" ++ spc () ++ Id.print id + else + str "No " ++ str name ++ str " of suffix" ++ spc () ++ pr_qualid qid | l -> - prlist_with_sep fnl - (fun (o,oqid) -> - hov 2 (pr_located_qualid o ++ - (if not (qualid_eq oqid qid) then - spc() ++ str "(shorter name to refer to it in current context is " + prlist_with_sep fnl + (fun (o,oqid) -> + hov 2 (pr_located_qualid o ++ + (if not (qualid_eq oqid qid) then + spc() ++ str "(shorter name to refer to it in current context is " ++ pr_qualid oqid ++ str")" - else mt ()) ++ + else mt ()) ++ display_alias o)) l let print_located_term ref = print_located_qualid "term" LocTerm ref @@ -509,8 +537,8 @@ let print_named_def env sigma name body typ = let pbody = if Constr.isCast body then surround pbody else pbody in (str "*** [" ++ str name ++ str " " ++ hov 0 (str ":=" ++ brk (1,2) ++ pbody ++ spc () ++ - str ":" ++ brk (1,2) ++ ptyp) ++ - str "]") + str ":" ++ brk (1,2) ++ ptyp) ++ + str "]") let print_named_assum env sigma name typ = str "*** [" ++ str name ++ str " : " ++ pr_ltype_env env sigma typ ++ str "]" @@ -536,9 +564,7 @@ let gallina_print_inductive sp udecl = pr_mutual_inductive_body env sp mib udecl ++ with_line_skip (print_primitive_record mib.mind_finite mipv mib.mind_record @ - print_inductive_renames sp mipv @ - print_inductive_implicit_args sp mipv @ - print_inductive_argument_scopes sp mipv) + print_inductive_args sp mipv) let print_named_decl env sigma id = gallina_print_named_decl env sigma (Global.lookup_named id) ++ fnl () @@ -561,9 +587,9 @@ let print_instance sigma cb = pr_universe_instance sigma inst else mt() -let print_constant indirect_accessor with_values sep sp udecl = +let print_constant with_values sep sp udecl = let cb = Global.lookup_constant sp in - let val_0 = Global.body_of_constant_body indirect_accessor cb in + let val_0 = Global.body_of_constant_body Library.indirect_accessor cb in let typ = cb.const_type in let univs = let open Univ in @@ -571,7 +597,7 @@ let print_constant indirect_accessor with_values sep sp udecl = match cb.const_body with | Undef _ | Def _ | Primitive _ -> cb.const_universes | OpaqueDef o -> - let body_uctxs = Opaqueproof.force_constraints indirect_accessor otab o in + let body_uctxs = Opaqueproof.force_constraints Library.indirect_accessor otab o in match cb.const_universes with | Monomorphic ctx -> Monomorphic (ContextSet.union body_uctxs ctx) @@ -588,21 +614,21 @@ let print_constant indirect_accessor with_values sep sp udecl = hov 0 ( match val_0 with | None -> - str"*** [ " ++ - print_basename sp ++ print_instance sigma cb ++ str " : " ++ cut () ++ pr_ltype typ ++ - str" ]" ++ + str"*** [ " ++ + print_basename sp ++ print_instance sigma cb ++ str " : " ++ cut () ++ pr_ltype typ ++ + str" ]" ++ Printer.pr_universes sigma univs | Some (c, priv, ctx) -> let priv = match priv with | Opaqueproof.PrivateMonomorphic () -> None | Opaqueproof.PrivatePolymorphic (_, ctx) -> Some ctx in - print_basename sp ++ print_instance sigma cb ++ str sep ++ cut () ++ - (if with_values then print_typed_body env sigma (Some c,typ) else pr_ltype typ)++ + print_basename sp ++ print_instance sigma cb ++ str sep ++ cut () ++ + (if with_values then print_typed_body env sigma (Some c,typ) else pr_ltype typ)++ Printer.pr_universes sigma univs ?priv) -let gallina_print_constant_with_infos indirect_accessor sp udecl = - print_constant indirect_accessor true " = " sp udecl ++ +let gallina_print_constant_with_infos sp udecl = + print_constant true " = " sp udecl ++ with_line_skip (print_name_infos (GlobRef.ConstRef sp)) let gallina_print_syntactic_def env kn = @@ -618,38 +644,38 @@ let gallina_print_syntactic_def env kn = Constrextern.without_specific_symbols [Notation.SynDefRule kn] (pr_glob_constr_env env) c) -let gallina_print_leaf_entry ~mod_ops indirect_accessor env sigma with_values ((sp,kn as oname),lobj) = +let gallina_print_leaf_entry env sigma with_values ((sp,kn as oname),lobj) = let sep = if with_values then " = " else " : " in match lobj with | AtomicObject o -> let tag = object_tag o in begin match (oname,tag) with | (_,"VARIABLE") -> - (* Outside sections, VARIABLES still exist but only with universes + (* Outside sections, VARIABLES still exist but only with universes constraints *) (try Some(print_named_decl env sigma (basename sp)) with Not_found -> None) | (_,"CONSTANT") -> - Some (print_constant indirect_accessor with_values sep (Constant.make1 kn) None) + Some (print_constant with_values sep (Constant.make1 kn) None) | (_,"INDUCTIVE") -> Some (gallina_print_inductive (MutInd.make1 kn) None) | (_,("AUTOHINT"|"GRAMMAR"|"SYNTAXCONSTANT"|"PPSYNTAX"|"TOKEN"|"CLASS"| - "COERCION"|"REQUIRE"|"END-SECTION"|"STRUCTURE")) -> None + "COERCION"|"REQUIRE"|"END-SECTION"|"STRUCTURE")) -> None (* To deal with forgotten cases... *) | (_,s) -> None end | ModuleObject _ -> let (mp,l) = KerName.repr kn in - Some (print_module ~mod_ops with_values (MPdot (mp,l))) + Some (print_module with_values ~mod_ops:Declaremods.mod_ops (MPdot (mp,l))) | ModuleTypeObject _ -> let (mp,l) = KerName.repr kn in - Some (print_modtype ~mod_ops (MPdot (mp,l))) + Some (print_modtype ~mod_ops:Declaremods.mod_ops (MPdot (mp,l))) | _ -> None -let gallina_print_library_entry ~mod_ops indirect_accessor env sigma with_values ent = +let gallina_print_library_entry env sigma with_values ent = let pr_name (sp,_) = Id.print (basename sp) in match ent with | (oname,Lib.Leaf lobj) -> - gallina_print_leaf_entry ~mod_ops indirect_accessor env sigma with_values (oname,lobj) + gallina_print_leaf_entry env sigma with_values (oname,lobj) | (oname,Lib.OpenedSection (dir,_)) -> Some (str " >>>>>>> Section " ++ pr_name oname) | (_,Lib.CompilingLibrary { Nametab.obj_dir; _ }) -> @@ -657,10 +683,10 @@ let gallina_print_library_entry ~mod_ops indirect_accessor env sigma with_values | (oname,Lib.OpenedModule _) -> Some (str " >>>>>>> Module " ++ pr_name oname) -let gallina_print_context ~mod_ops indirect_accessor env sigma with_values = +let gallina_print_context env sigma with_values = let rec prec n = function | h::rest when Option.is_empty n || Option.get n > 0 -> - (match gallina_print_library_entry ~mod_ops indirect_accessor env sigma with_values h with + (match gallina_print_library_entry env sigma with_values h with | None -> prec n rest | Some pp -> prec (Option.map ((+) (-1)) n) rest ++ pp ++ fnl ()) | _ -> mt () @@ -698,8 +724,8 @@ let print_syntactic_def x = !object_pr.print_syntactic_def x let print_module x = !object_pr.print_module x let print_modtype x = !object_pr.print_modtype x let print_named_decl x = !object_pr.print_named_decl x -let print_library_entry ~mod_ops x = !object_pr.print_library_entry ~mod_ops x -let print_context ~mod_ops x = !object_pr.print_context ~mod_ops x +let print_library_entry x = !object_pr.print_library_entry x +let print_context x = !object_pr.print_context x let print_typed_value_in_env x = !object_pr.print_typed_value_in_env x let print_eval x = !object_pr.print_eval x @@ -720,30 +746,32 @@ let print_safe_judgment env sigma j = (*********************) (* *) -let print_full_context ~mod_ops indirect_accessor env sigma = - print_context ~mod_ops indirect_accessor env sigma true None (Lib.contents ()) -let print_full_context_typ ~mod_ops indirect_accessor env sigma = - print_context ~mod_ops indirect_accessor env sigma false None (Lib.contents ()) +let print_full_context env sigma = + print_context env sigma true None (Lib.contents ()) +let print_full_context_typ env sigma = + print_context env sigma false None (Lib.contents ()) -let print_full_pure_context ~mod_ops ~library_accessor env sigma = +let print_full_pure_context env sigma = let rec prec = function | ((_,kn),Lib.Leaf AtomicObject lobj)::rest -> let pp = match object_tag lobj with | "CONSTANT" -> - let con = Global.constant_of_delta_kn kn in - let cb = Global.lookup_constant con in - let typ = cb.const_type in - hov 0 ( - match cb.const_body with - | Undef _ -> - str "Parameter " ++ + let con = Global.constant_of_delta_kn kn in + let cb = Global.lookup_constant con in + let typ = cb.const_type in + hov 0 ( + match cb.const_body with + | Undef _ -> + str "Parameter " ++ print_basename con ++ str " : " ++ cut () ++ pr_ltype_env env sigma typ - | OpaqueDef lc -> - str "Theorem " ++ print_basename con ++ cut () ++ + | OpaqueDef lc -> + str "Theorem " ++ print_basename con ++ cut () ++ str " : " ++ pr_ltype_env env sigma typ ++ str "." ++ fnl () ++ - str "Proof " ++ pr_lconstr_env env sigma (fst (Opaqueproof.force_proof library_accessor (Global.opaque_tables ()) lc)) + str "Proof " ++ pr_lconstr_env env sigma + (fst (Opaqueproof.force_proof Library.indirect_accessor + (Global.opaque_tables ()) lc)) | Def c -> - str "Definition " ++ print_basename con ++ cut () ++ + str "Definition " ++ print_basename con ++ cut () ++ str " : " ++ pr_ltype_env env sigma typ ++ cut () ++ str " := " ++ pr_lconstr_env env sigma (Mod_subst.force_constr c) | Primitive _ -> @@ -751,20 +779,20 @@ let print_full_pure_context ~mod_ops ~library_accessor env sigma = print_basename con ++ str " : " ++ cut () ++ pr_ltype_env env sigma typ) ++ str "." ++ fnl () ++ fnl () | "INDUCTIVE" -> - let mind = Global.mind_of_delta_kn kn in - let mib = Global.lookup_mind mind in + let mind = Global.mind_of_delta_kn kn in + let mib = Global.lookup_mind mind in pr_mutual_inductive_body (Global.env()) mind mib None ++ - str "." ++ fnl () ++ fnl () + str "." ++ fnl () ++ fnl () | _ -> mt () in prec rest ++ pp | ((_,kn),Lib.Leaf ModuleObject _)::rest -> (* TODO: make it reparsable *) let (mp,l) = KerName.repr kn in - prec rest ++ print_module ~mod_ops true (MPdot (mp,l)) ++ str "." ++ fnl () ++ fnl () + prec rest ++ print_module true (MPdot (mp,l)) ++ str "." ++ fnl () ++ fnl () | ((_,kn),Lib.Leaf ModuleTypeObject _)::rest -> (* TODO: make it reparsable *) let (mp,l) = KerName.repr kn in - prec rest ++ print_modtype ~mod_ops (MPdot (mp,l)) ++ str "." ++ fnl () ++ fnl () + prec rest ++ print_modtype (MPdot (mp,l)) ++ str "." ++ fnl () ++ fnl () | _::rest -> prec rest | _ -> mt () in prec (Lib.contents ()) @@ -789,11 +817,11 @@ let read_sec_context qid = let cxt = Lib.contents () in List.rev (get_cxt [] cxt) -let print_sec_context ~mod_ops indirect_accessor env sigma sec = - print_context ~mod_ops indirect_accessor env sigma true None (read_sec_context sec) +let print_sec_context env sigma sec = + print_context env sigma true None (read_sec_context sec) -let print_sec_context_typ ~mod_ops indirect_accessor env sigma sec = - print_context ~mod_ops indirect_accessor env sigma false None (read_sec_context sec) +let print_sec_context_typ env sigma sec = + print_context env sigma false None (read_sec_context sec) let maybe_error_reject_univ_decl na udecl = let open GlobRef in @@ -803,19 +831,19 @@ let maybe_error_reject_univ_decl na udecl = (* TODO Print na somehow *) user_err ~hdr:"reject_univ_decl" (str "This object does not support universe names.") -let print_any_name ~mod_ops indirect_accessor env sigma na udecl = +let print_any_name env sigma na udecl = maybe_error_reject_univ_decl na udecl; let open GlobRef in match na with - | Term (ConstRef sp) -> print_constant_with_infos indirect_accessor sp udecl + | Term (ConstRef sp) -> print_constant_with_infos sp udecl | Term (IndRef (sp,_)) -> print_inductive sp udecl | Term (ConstructRef ((sp,_),_)) -> print_inductive sp udecl | Term (VarRef sp) -> print_section_variable env sigma sp | Syntactic kn -> print_syntactic_def env kn | Dir (Nametab.GlobDirRef.DirModule Nametab.{ obj_dir; obj_mp; _ } ) -> - print_module ~mod_ops (printable_body obj_dir) obj_mp + print_module (printable_body obj_dir) obj_mp | Dir _ -> mt () - | ModuleType mp -> print_modtype ~mod_ops mp + | ModuleType mp -> print_modtype mp | Other (obj, info) -> info.print obj | Undefined qid -> try (* Var locale de but, pas var de section... donc pas d'implicits *) @@ -827,23 +855,23 @@ let print_any_name ~mod_ops indirect_accessor env sigma na udecl = user_err ~hdr:"print_name" (pr_qualid qid ++ spc () ++ str "not a defined object.") -let print_name ~mod_ops indirect_accessor env sigma na udecl = +let print_name env sigma na udecl = match na with | {loc; v=Constrexpr.ByNotation (ntn,sc)} -> - print_any_name ~mod_ops indirect_accessor env sigma + print_any_name env sigma (Term (Notation.interp_notation_as_global_reference ?loc (fun _ -> true) ntn sc)) udecl | {loc; v=Constrexpr.AN ref} -> - print_any_name ~mod_ops indirect_accessor env sigma (locate_any_name ref) udecl + print_any_name env sigma (locate_any_name ref) udecl -let print_opaque_name indirect_accessor env sigma qid = +let print_opaque_name env sigma qid = let open GlobRef in match Nametab.global qid with | ConstRef cst -> let cb = Global.lookup_constant cst in if Declareops.constant_has_body cb then - print_constant_with_infos indirect_accessor cst None + print_constant_with_infos cst None else user_err Pp.(str "Not a defined constant.") | IndRef (sp,_) -> @@ -865,9 +893,9 @@ let print_about_any ?loc env sigma k udecl = pr_infos_list (print_ref false ref udecl :: blankline :: print_polymorphism ref @ - print_name_infos ref @ - (if Pp.ismt rb then [] else [rb]) @ - print_opacity ref @ + print_name_infos ref @ + (if Pp.ismt rb then [] else [rb]) @ + print_opacity ref @ print_bidi_hints ref @ [hov 0 (str "Expands to: " ++ pr_located_qualid k)]) | Syntactic kn -> @@ -891,8 +919,8 @@ let print_about env sigma na udecl = print_about_any ?loc env sigma (locate_any_name ref) udecl (* for debug *) -let inspect ~mod_ops indirect_accessor env sigma depth = - print_context ~mod_ops indirect_accessor env sigma false (Some depth) (Lib.contents ()) +let inspect env sigma depth = + print_context env sigma false (Some depth) (Lib.contents ()) (*************************************************************************) (* Pretty-printing functions coming from classops.ml *) @@ -938,7 +966,7 @@ let print_path_between cls clt = with Not_found -> user_err ~hdr:"index_cl_of_id" (str"No path between " ++ pr_class cls ++ str" and " ++ pr_class clt - ++ str ".") + ++ str ".") in print_path ((i,j),p) diff --git a/printing/prettyp.mli b/vernac/prettyp.mli index c8b361d95b..dc4280f286 100644 --- a/printing/prettyp.mli +++ b/vernac/prettyp.mli @@ -19,48 +19,31 @@ val assumptions_for_print : Name.t list -> Termops.names_context val print_closed_sections : bool ref val print_context - : mod_ops:Printmod.mod_ops - -> Opaqueproof.indirect_accessor - -> env -> Evd.evar_map + : env + -> Evd.evar_map -> bool -> int option -> Lib.library_segment -> Pp.t val print_library_entry - : mod_ops:Printmod.mod_ops - -> Opaqueproof.indirect_accessor - -> env -> Evd.evar_map - -> bool -> (Libobject.object_name * Lib.node) -> Pp.t option -val print_full_context - : mod_ops:Printmod.mod_ops - -> Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> Pp.t -val print_full_context_typ - : mod_ops:Printmod.mod_ops - -> Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> Pp.t - -val print_full_pure_context - : mod_ops:Printmod.mod_ops - -> library_accessor:Opaqueproof.indirect_accessor - -> env + : env -> Evd.evar_map - -> Pp.t + -> bool -> (Libobject.object_name * Lib.node) -> Pp.t option +val print_full_context : env -> Evd.evar_map -> Pp.t +val print_full_context_typ : env -> Evd.evar_map -> Pp.t + +val print_full_pure_context : env -> Evd.evar_map -> Pp.t -val print_sec_context - : mod_ops:Printmod.mod_ops - -> Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> qualid -> Pp.t -val print_sec_context_typ - : mod_ops:Printmod.mod_ops - -> Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> qualid -> Pp.t +val print_sec_context : env -> Evd.evar_map -> qualid -> Pp.t +val print_sec_context_typ : env -> Evd.evar_map -> qualid -> Pp.t val print_judgment : env -> Evd.evar_map -> EConstr.unsafe_judgment -> Pp.t val print_safe_judgment : env -> Evd.evar_map -> Safe_typing.judgment -> Pp.t val print_eval : reduction_function -> env -> Evd.evar_map -> Constrexpr.constr_expr -> EConstr.unsafe_judgment -> Pp.t -val print_name - : mod_ops:Printmod.mod_ops - -> Opaqueproof.indirect_accessor - -> env -> Evd.evar_map -> qualid Constrexpr.or_by_notation - -> UnivNames.univ_name_list option -> Pp.t -val print_opaque_name - : Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> qualid -> Pp.t +val print_name : env -> Evd.evar_map + -> qualid Constrexpr.or_by_notation + -> UnivNames.univ_name_list option + -> Pp.t +val print_opaque_name : env -> Evd.evar_map -> qualid -> Pp.t val print_about : env -> Evd.evar_map -> qualid Constrexpr.or_by_notation -> UnivNames.univ_name_list option -> Pp.t val print_impargs : qualid Constrexpr.or_by_notation -> Pp.t @@ -77,10 +60,7 @@ val print_typeclasses : unit -> Pp.t val print_instances : GlobRef.t -> Pp.t val print_all_instances : unit -> Pp.t -val inspect - : mod_ops:Printmod.mod_ops - -> Opaqueproof.indirect_accessor - -> env -> Evd.evar_map -> int -> Pp.t +val inspect : env -> Evd.evar_map -> int -> Pp.t (** {5 Locate} *) @@ -113,14 +93,14 @@ val print_located_other : string -> qualid -> Pp.t type object_pr = { print_inductive : MutInd.t -> UnivNames.univ_name_list option -> Pp.t; - print_constant_with_infos : Opaqueproof.indirect_accessor -> Constant.t -> UnivNames.univ_name_list option -> Pp.t; + print_constant_with_infos : Constant.t -> UnivNames.univ_name_list option -> Pp.t; print_section_variable : env -> Evd.evar_map -> variable -> Pp.t; print_syntactic_def : env -> KerName.t -> Pp.t; - print_module : mod_ops:Printmod.mod_ops -> bool -> ModPath.t -> Pp.t; - print_modtype : mod_ops:Printmod.mod_ops -> ModPath.t -> Pp.t; + print_module : bool -> ModPath.t -> Pp.t; + print_modtype : ModPath.t -> Pp.t; print_named_decl : env -> Evd.evar_map -> Constr.named_declaration -> Pp.t; - print_library_entry : mod_ops:Printmod.mod_ops -> Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> bool -> (Libobject.object_name * Lib.node) -> Pp.t option; - print_context : mod_ops:Printmod.mod_ops -> Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> bool -> int option -> Lib.library_segment -> Pp.t; + print_library_entry : env -> Evd.evar_map -> bool -> (Libobject.object_name * Lib.node) -> Pp.t option; + print_context : env -> Evd.evar_map -> bool -> int option -> Lib.library_segment -> Pp.t; print_typed_value_in_env : Environ.env -> Evd.evar_map -> EConstr.constr * EConstr.types -> Pp.t; print_eval : Reductionops.reduction_function -> env -> Evd.evar_map -> Constrexpr.constr_expr -> EConstr.unsafe_judgment -> Pp.t; } diff --git a/vernac/vernac.mllib b/vernac/vernac.mllib index 956b56e256..5226c2ba65 100644 --- a/vernac/vernac.mllib +++ b/vernac/vernac.mllib @@ -19,6 +19,7 @@ DeclareObl Canonical RecLemmas Library +Prettyp Lemmas Class Auto_ind_decl @@ -38,6 +39,7 @@ Assumptions Mltop Topfmt Loadpath +ComArguments Vernacentries Vernacstate Vernacinterp diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 684d8a3d90..edff80af00 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -15,7 +15,6 @@ open CErrors open CAst open Util open Names -open Nameops open Tacmach open Constrintern open Prettyp @@ -176,7 +175,7 @@ let print_module qid = let globdir = Nametab.locate_dir qid in match globdir with DirModule Nametab.{ obj_dir; obj_mp; _ } -> - Printmod.print_module (Printmod.printable_body obj_dir) obj_mp + Printmod.print_module ~mod_ops:Declaremods.mod_ops (Printmod.printable_body obj_dir) obj_mp | _ -> raise Not_found with Not_found -> user_err (str"Unknown Module " ++ pr_qualid qid) @@ -184,12 +183,12 @@ let print_module qid = let print_modtype qid = try let kn = Nametab.locate_modtype qid in - Printmod.print_modtype kn + Printmod.print_modtype ~mod_ops:Declaremods.mod_ops kn with Not_found -> (* Is there a module of this name ? If yes we display its type *) try let mp = Nametab.locate_module qid in - Printmod.print_module false mp + Printmod.print_module ~mod_ops:Declaremods.mod_ops false mp with Not_found -> user_err (str"Unknown Module Type or Module " ++ pr_qualid qid) @@ -448,9 +447,6 @@ let vernac_bind_scope ~module_local sc cll = let vernac_open_close_scope ~section_local (b,s) = Notation.open_close_scope (section_local,b,s) -let vernac_arguments_scope ~section_local r scl = - Notation.declare_arguments_scope section_local (smart_global r) scl - let vernac_infix ~atts = let module_local, deprecation = Attributes.(parse Notations.(module_locality ++ deprecation) atts) in Metasyntax.add_infix ~local:module_local deprecation (Global.env()) @@ -655,7 +651,7 @@ let vernac_record ~template udecl cum k poly finite records = let cumulative = should_treat_as_cumulative cum poly in let map ((coe, id), binders, sort, nameopt, cfs) = let const = match nameopt with - | None -> add_prefix "Build_" id.v + | None -> Nameops.add_prefix "Build_" id.v | Some lid -> let () = Dumpglob.dump_definition lid false "constr" in lid.v @@ -1213,292 +1209,6 @@ let vernac_syntactic_definition ~atts lid x compat = Dumpglob.dump_definition lid false "syndef"; Metasyntax.add_syntactic_definition ~local:module_local deprecation (Global.env()) lid.v x compat -let cache_bidi_hints (_name, (gr, ohint)) = - match ohint with - | None -> Pretyping.clear_bidirectionality_hint gr - | Some nargs -> Pretyping.add_bidirectionality_hint gr nargs - -let load_bidi_hints _ r = - cache_bidi_hints r - -let subst_bidi_hints (subst, (gr, ohint as orig)) = - let gr' = subst_global_reference subst gr in - if gr == gr' then orig else (gr', ohint) - -let discharge_bidi_hints (_name, (gr, ohint)) = - if isVarRef gr && Lib.is_in_section gr then None - else - let vars = Lib.variable_section_segment_of_reference gr in - let n = List.length vars in - Some (gr, Option.map ((+) n) ohint) - -let inBidiHints = - let open Libobject in - declare_object { (default_object "BIDIRECTIONALITY-HINTS" ) with - load_function = load_bidi_hints; - cache_function = cache_bidi_hints; - classify_function = (fun o -> Substitute o); - subst_function = subst_bidi_hints; - discharge_function = discharge_bidi_hints; - } - - -let warn_arguments_assert = - CWarnings.create ~name:"arguments-assert" ~category:"vernacular" - (fun sr -> - strbrk "This command is just asserting the names of arguments of " ++ - pr_global sr ++ strbrk". If this is what you want add " ++ - strbrk "': assert' to silence the warning. If you want " ++ - strbrk "to clear implicit arguments add ': clear implicits'. " ++ - strbrk "If you want to clear notation scopes add ': clear scopes'") - -(* [nargs_for_red] is the number of arguments required to trigger reduction, - [args] is the main list of arguments statuses, - [more_implicits] is a list of extra lists of implicit statuses *) -let vernac_arguments ~section_local reference args more_implicits nargs_for_red nargs_before_bidi flags = - let env = Global.env () in - let sigma = Evd.from_env env in - let assert_flag = List.mem `Assert flags in - let rename_flag = List.mem `Rename flags in - let clear_scopes_flag = List.mem `ClearScopes flags in - let extra_scopes_flag = List.mem `ExtraScopes flags in - let clear_implicits_flag = List.mem `ClearImplicits flags in - let default_implicits_flag = List.mem `DefaultImplicits flags in - let never_unfold_flag = List.mem `ReductionNeverUnfold flags in - let nomatch_flag = List.mem `ReductionDontExposeCase flags in - let clear_bidi_hint = List.mem `ClearBidiHint flags in - - let err_incompat x y = - user_err Pp.(str ("Options \""^x^"\" and \""^y^"\" are incompatible.")) in - - if assert_flag && rename_flag then - err_incompat "assert" "rename"; - if clear_scopes_flag && extra_scopes_flag then - err_incompat "clear scopes" "extra scopes"; - if clear_implicits_flag && default_implicits_flag then - err_incompat "clear implicits" "default implicits"; - - let sr = smart_global reference in - let inf_names = - let ty, _ = Typeops.type_of_global_in_context env sr in - Impargs.compute_implicits_names env sigma (EConstr.of_constr ty) - in - let prev_names = - try Arguments_renaming.arguments_names sr with Not_found -> inf_names - in - let num_args = List.length inf_names in - assert (Int.equal num_args (List.length prev_names)); - - let names_of args = List.map (fun a -> a.name) args in - - (* Checks *) - - let err_extra_args names = - user_err ~hdr:"vernac_declare_arguments" - (strbrk "Extra arguments: " ++ - prlist_with_sep pr_comma Name.print names ++ str ".") - in - let err_missing_args names = - user_err ~hdr:"vernac_declare_arguments" - (strbrk "The following arguments are not declared: " ++ - prlist_with_sep pr_comma Name.print names ++ str ".") - in - - let rec check_extra_args extra_args = - match extra_args with - | [] -> () - | { notation_scope = None } :: _ -> - user_err Pp.(str"Extra arguments should specify a scope.") - | { notation_scope = Some _ } :: args -> check_extra_args args - in - - let args, scopes = - let scopes = List.map (fun { notation_scope = s } -> s) args in - if List.length args > num_args then - let args, extra_args = List.chop num_args args in - if extra_scopes_flag then - (check_extra_args extra_args; (args, scopes)) - else err_extra_args (names_of extra_args) - else args, scopes - in - - if Option.cata (fun n -> n > num_args) false nargs_for_red then - user_err Pp.(str "The \"/\" modifier should be put before any extra scope."); - - if Option.cata (fun n -> n > num_args) false nargs_before_bidi then - user_err Pp.(str "The \"&\" modifier should be put before any extra scope."); - - let scopes_specified = List.exists Option.has_some scopes in - - if scopes_specified && clear_scopes_flag then - user_err Pp.(str "The \"clear scopes\" flag is incompatible with scope annotations."); - - let names = List.map (fun { name } -> name) args in - let names = names :: List.map (List.map fst) more_implicits in - - let rename_flag_required = ref false in - let example_renaming = ref None in - let save_example_renaming renaming = - rename_flag_required := !rename_flag_required - || not (Name.equal (fst renaming) Anonymous); - if Option.is_empty !example_renaming then - example_renaming := Some renaming - in - - let rec names_union names1 names2 = - match names1, names2 with - | [], [] -> [] - | _ :: _, [] -> names1 - | [], _ :: _ -> names2 - | (Name _ as name) :: names1, Anonymous :: names2 - | Anonymous :: names1, (Name _ as name) :: names2 -> - name :: names_union names1 names2 - | name1 :: names1, name2 :: names2 -> - if Name.equal name1 name2 then - name1 :: names_union names1 names2 - else user_err Pp.(str "Argument lists should agree on the names they provide.") - in - - let names = List.fold_left names_union [] names in - - let rec rename prev_names names = - match prev_names, names with - | [], [] -> [] - | [], _ :: _ -> err_extra_args names - | _ :: _, [] when assert_flag -> - (* Error messages are expressed in terms of original names, not - renamed ones. *) - err_missing_args (List.lastn (List.length prev_names) inf_names) - | _ :: _, [] -> prev_names - | prev :: prev_names, Anonymous :: names -> - prev :: rename prev_names names - | prev :: prev_names, (Name id as name) :: names -> - if not (Name.equal prev name) then save_example_renaming (prev,name); - name :: rename prev_names names - in - - let names = rename prev_names names in - let renaming_specified = Option.has_some !example_renaming in - - if !rename_flag_required && not rename_flag then begin - let msg = - match !example_renaming with - | None -> - strbrk "To rename arguments the \"rename\" flag must be specified." - | Some (o,n) -> - strbrk "Flag \"rename\" expected to rename " ++ Name.print o ++ - strbrk " into " ++ Name.print n ++ str "." - in user_err ~hdr:"vernac_declare_arguments" msg - end; - - let duplicate_names = - List.duplicates Name.equal (List.filter ((!=) Anonymous) names) - in - if not (List.is_empty duplicate_names) then begin - let duplicates = prlist_with_sep pr_comma Name.print duplicate_names in - user_err (strbrk "Some argument names are duplicated: " ++ duplicates) - end; - - let implicits = - List.map (fun { name; implicit_status = i } -> (name,i)) args - in - let implicits = implicits :: more_implicits in - - let implicits = List.map (List.map snd) implicits in - let implicits_specified = match implicits with - | [l] -> List.exists (function Impargs.NotImplicit -> false | _ -> true) l - | _ -> true in - - if implicits_specified && clear_implicits_flag then - user_err Pp.(str "The \"clear implicits\" flag is incompatible with implicit annotations"); - - if implicits_specified && default_implicits_flag then - user_err Pp.(str "The \"default implicits\" flag is incompatible with implicit annotations"); - - let rargs = - Util.List.map_filter (function (n, true) -> Some n | _ -> None) - (Util.List.map_i (fun i { recarg_like = b } -> i, b) 0 args) - in - - let red_behavior = - let open Reductionops.ReductionBehaviour in - match never_unfold_flag, nomatch_flag, rargs, nargs_for_red with - | true, false, [], None -> Some NeverUnfold - | true, true, _, _ -> err_incompat "simpl never" "simpl nomatch" - | true, _, _::_, _ -> err_incompat "simpl never" "!" - | true, _, _, Some _ -> err_incompat "simpl never" "/" - | false, false, [], None -> None - | false, false, _, _ -> Some (UnfoldWhen { nargs = nargs_for_red; - recargs = rargs; - }) - | false, true, _, _ -> Some (UnfoldWhenNoMatch { nargs = nargs_for_red; - recargs = rargs; - }) - in - - - let red_modifiers_specified = Option.has_some red_behavior in - - let bidi_hint_specified = Option.has_some nargs_before_bidi in - - if bidi_hint_specified && clear_bidi_hint then - err_incompat "clear bidirectionality hint" "&"; - - - (* Actions *) - - if renaming_specified then begin - Arguments_renaming.rename_arguments section_local sr names - end; - - if scopes_specified || clear_scopes_flag then begin - let scopes = List.map (Option.map (fun {loc;v=k} -> - try ignore (Notation.find_scope k); k - with UserError _ -> - Notation.find_delimiters_scope ?loc k)) scopes - in - vernac_arguments_scope ~section_local reference scopes - end; - - if implicits_specified || clear_implicits_flag then - Impargs.set_implicits section_local (smart_global reference) implicits; - - if default_implicits_flag then - Impargs.declare_implicits section_local (smart_global reference); - - if red_modifiers_specified then begin - match sr with - | GlobRef.ConstRef _ as c -> - Reductionops.ReductionBehaviour.set - ~local:section_local c (Option.get red_behavior) - - | _ -> user_err - (strbrk "Modifiers of the behavior of the simpl tactic "++ - strbrk "are relevant for constants only.") - end; - - if bidi_hint_specified then begin - let n = Option.get nargs_before_bidi in - if section_local then - Pretyping.add_bidirectionality_hint sr n - else - Lib.add_anonymous_leaf (inBidiHints (sr, Some n)) - end; - - if clear_bidi_hint then begin - if section_local then - Pretyping.clear_bidirectionality_hint sr - else - Lib.add_anonymous_leaf (inBidiHints (sr, None)) - end; - - if not (renaming_specified || - implicits_specified || - scopes_specified || - red_modifiers_specified || - bidi_hint_specified) && (List.is_empty flags) then - warn_arguments_assert sr - let default_env () = { Notation_term.ninterp_var_type = Id.Map.empty; ninterp_rec_vars = Id.Map.empty; @@ -1962,29 +1672,26 @@ let print_about_hyp_globs ~pstate ?loc ref_or_by_not udecl glopt = print_about env sigma ref_or_by_not udecl let vernac_print ~pstate ~atts = - let mod_ops = { Printmod.import_module = Declaremods.import_module - ; process_module_binding = Declaremods.process_module_binding - } in let sigma, env = get_current_or_global_context ~pstate in function | PrintTypingFlags -> pr_typing_flags (Environ.typing_flags (Global.env ())) | PrintTables -> print_tables () - | PrintFullContext-> print_full_context_typ ~mod_ops Library.indirect_accessor env sigma - | PrintSectionContext qid -> print_sec_context_typ ~mod_ops Library.indirect_accessor env sigma qid - | PrintInspect n -> inspect ~mod_ops Library.indirect_accessor env sigma n + | PrintFullContext-> print_full_context_typ env sigma + | PrintSectionContext qid -> print_sec_context_typ env sigma qid + | PrintInspect n -> inspect env sigma n | PrintGrammar ent -> Metasyntax.pr_grammar ent | PrintCustomGrammar ent -> Metasyntax.pr_custom_grammar ent | PrintLoadPath dir -> (* For compatibility ? *) print_loadpath dir | PrintModules -> print_modules () - | PrintModule qid -> print_module ~mod_ops qid - | PrintModuleType qid -> print_modtype ~mod_ops qid + | PrintModule qid -> print_module qid + | PrintModuleType qid -> print_modtype qid | PrintNamespace ns -> print_namespace ~pstate ns | PrintMLLoadPath -> Mltop.print_ml_path () | PrintMLModules -> Mltop.print_ml_modules () | PrintDebugGC -> Mltop.print_gc () | PrintName (qid,udecl) -> dump_global qid; - print_name ~mod_ops Library.indirect_accessor env sigma qid udecl + print_name env sigma qid udecl | PrintGraph -> Prettyp.print_graph () | PrintClasses -> Prettyp.print_classes() | PrintTypeClasses -> Prettyp.print_typeclasses() @@ -2453,7 +2160,8 @@ let translate_vernac ~atts v = let open Vernacextend in match v with VtDefault(fun () -> vernac_syntactic_definition ~atts id c b) | VernacArguments (qid, args, more_implicits, nargs, bidi, flags) -> VtDefault(fun () -> - with_section_locality ~atts (vernac_arguments qid args more_implicits nargs bidi flags)) + with_section_locality ~atts + (ComArguments.vernac_arguments qid args more_implicits nargs bidi flags)) | VernacReserve bl -> VtDefault(fun () -> unsupported_attributes atts; diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml index b712d7e264..564c55670d 100644 --- a/vernac/vernacexpr.ml +++ b/vernac/vernacexpr.ml @@ -257,6 +257,17 @@ type vernac_argument_status = { implicit_status : Impargs.implicit_kind; } +type arguments_modifier = + [ `Assert + | `ClearBidiHint + | `ClearImplicits + | `ClearScopes + | `DefaultImplicits + | `ExtraScopes + | `ReductionDontExposeCase + | `ReductionNeverUnfold + | `Rename ] + type extend_name = (* Name of the vernac entry where the tactic is defined, typically found after the VERNAC EXTEND statement in the source. *) @@ -365,16 +376,16 @@ type nonrec vernac_expr = | VernacCreateHintDb of string * bool | VernacRemoveHints of string list * qualid list | VernacHints of string list * Hints.hints_expr - | VernacSyntacticDefinition of lident * (Id.t list * constr_expr) * + | VernacSyntacticDefinition of + lident * (Id.t list * constr_expr) * onlyparsing_flag - | VernacArguments of qualid or_by_notation * + | VernacArguments of + qualid or_by_notation * vernac_argument_status list (* Main arguments status list *) * - (Name.t * Impargs.implicit_kind) list list (* Extra implicit status lists *) * + (Name.t * Impargs.implicit_kind) list list (* Extra implicit status lists *) * int option (* Number of args to trigger reduction *) * int option (* Number of args before bidirectional typing *) * - [ `ReductionDontExposeCase | `ReductionNeverUnfold | `Rename | - `ExtraScopes | `Assert | `ClearImplicits | `ClearScopes | `ClearBidiHint | - `DefaultImplicits ] list + arguments_modifier list | VernacReserve of simple_binder list | VernacGeneralizable of (lident list) option | VernacSetOpacity of (Conv_oracle.level * qualid or_by_notation list) |