diff options
| -rw-r--r-- | .github/ISSUE_TEMPLATE.md | 21 | ||||
| -rw-r--r-- | CHANGES.md | 8 | ||||
| -rw-r--r-- | checker/checkInductive.ml | 5 | ||||
| -rw-r--r-- | doc/sphinx/addendum/micromega.rst | 12 | ||||
| -rw-r--r-- | engine/uState.ml | 226 | ||||
| -rw-r--r-- | plugins/micromega/coq_micromega.ml | 2 | ||||
| -rw-r--r-- | plugins/omega/PreOmega.v | 132 | ||||
| -rw-r--r-- | test-suite/bugs/closed/bug_9268.v | 46 | ||||
| -rw-r--r-- | test-suite/coqchk/inductive_functor_squash.v | 15 | ||||
| -rw-r--r-- | test-suite/success/Nia.v | 918 |
10 files changed, 1251 insertions, 134 deletions
diff --git a/.github/ISSUE_TEMPLATE.md b/.github/ISSUE_TEMPLATE.md index c9cb516cd3..aec6cd0a21 100644 --- a/.github/ISSUE_TEMPLATE.md +++ b/.github/ISSUE_TEMPLATE.md @@ -1,18 +1,11 @@ -<!-- Thank you for your contribution. - Please complete the following information when reporting a bug. --> +<!-- Thank you for reporting a bug to Coq! --> -#### Version - -<!-- You can get this information by running `coqtop -v`. --> - - -#### Operating system +#### Description of the problem +<!-- If you can, it's helpful to provide self-contained example of some code +that reproduces the bug. If not, a link to a larger example is also helpful. --> -#### Description of the problem +#### Coq Version -<!-- It is helpful to provide enough information so that we can reproduce the bug. - In particular, please include a code example which produces it. - If the example is small, you can include it here between ``` ```. - Otherwise, please provide a link to a repository, a gist (https://gist.github.com) - or drag-and-drop a `.zip` archive. --> +<!-- You can get this information by running `coqtop -v`. If relevant, please +also include your operating system. --> diff --git a/CHANGES.md b/CHANGES.md index 4d0063115b..9d912a63b1 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -83,6 +83,14 @@ Tactics foo : database`). When the database name is omitted, the hint is added to the core database (as previously), but a deprecation warning is emitted. +- There are now tactics in `PreOmega.v` called + `Z.div_mod_to_equations`, `Z.quot_rem_to_equations`, and + `Z.to_euclidean_division_equations` (which combines the `div_mod` + and `quot_rem` variants) which allow `lia`, `nia`, `romega`, etc to + support `Z.div` and `Z.modulo` (`Z.quot` and `Z.rem`, respectively), + by posing the specifying equation for `Z.div` and `Z.modulo` before + replacing them with atoms. + Vernacular commands - `Combined Scheme` can now work when inductive schemes are generated in sort diff --git a/checker/checkInductive.ml b/checker/checkInductive.ml index c823db956d..d2d1efcb2c 100644 --- a/checker/checkInductive.ml +++ b/checker/checkInductive.ml @@ -77,6 +77,9 @@ let check_arity env ar1 ar2 = match ar1, ar2 with (* template_level is inferred by indtypes, so functor application can produce a smaller one *) | (RegularArity _ | TemplateArity _), _ -> false +let check_kelim k1 k2 = + List.for_all (fun x -> List.mem_f Sorts.family_equal x k2) k1 + (* Use [eq_ind_chk] because when we rebuild the recargs we have lost the knowledge of who is the canonical version. Try with to see test-suite/coqchk/include.v *) @@ -102,7 +105,7 @@ let check_packet env mind ind check "mind_user_lc" (Array.equal Constr.equal ind.mind_user_lc mind_user_lc); check "mind_nrealargs" Int.(equal ind.mind_nrealargs mind_nrealargs); check "mind_nrealdecls" Int.(equal ind.mind_nrealdecls mind_nrealdecls); - check "mind_kelim" (List.equal Sorts.family_equal ind.mind_kelim mind_kelim); + check "mind_kelim" (check_kelim ind.mind_kelim mind_kelim); check "mind_nf_lc" (Array.equal Constr.equal ind.mind_nf_lc mind_nf_lc); (* NB: here syntactic equality is not just an optimisation, we also diff --git a/doc/sphinx/addendum/micromega.rst b/doc/sphinx/addendum/micromega.rst index e799677c59..b076aac1ed 100644 --- a/doc/sphinx/addendum/micromega.rst +++ b/doc/sphinx/addendum/micromega.rst @@ -145,7 +145,7 @@ weakness, the :tacn:`lia` tactic is using recursively a combination of: + linear *positivstellensatz* refutations; + cutting plane proofs; + case split. - + Cutting plane proofs ~~~~~~~~~~~~~~~~~~~~~~ @@ -250,6 +250,16 @@ obtain :math:`-1`. By Theorem :ref:`Psatz <psatz_thm>`, the goal is valid. .. [#] Support for :g:`nat` and :g:`N` is obtained by pre-processing the goal with the ``zify`` tactic. +.. [#] Support for :g:`Z.div` and :g:`Z.modulo` may be obtained by + pre-processing the goal with the ``Z.div_mod_to_equations`` tactic (you may + need to manually run ``zify`` first). +.. [#] Support for :g:`Z.quot` and :g:`Z.rem` may be obtained by pre-processing + the goal with the ``Z.quot_rem_to_equations`` tactic (you may need to manually + run ``zify`` first). +.. [#] Note that support for :g:`Z.div`, :g:`Z.modulo`, :g:`Z.quot`, and + :g:`Z.rem` may be simultaneously obtained by pre-processing the goal with the + ``Z.to_euclidean_division_equations`` tactic (you may need to manually run + ``zify`` first). .. [#] Sources and binaries can be found at https://projects.coin-or.org/Csdp .. [#] Variants deal with equalities and strict inequalities. .. [#] In practice, the oracle might fail to produce such a refutation. diff --git a/engine/uState.ml b/engine/uState.ml index 6969d2ba44..430a3a2fd9 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -12,6 +12,7 @@ open Pp open CErrors open Util open Names +open Univ module UNameMap = Names.Id.Map @@ -24,12 +25,12 @@ module UPairSet = UnivMinim.UPairSet (* 2nd part used to check consistency on the fly. *) type t = - { uctx_names : UnivNames.universe_binders * uinfo Univ.LMap.t; - uctx_local : Univ.ContextSet.t; (** The local context of variables *) - uctx_seff_univs : Univ.LSet.t; (** Local universes used through private constants *) + { uctx_names : UnivNames.universe_binders * uinfo LMap.t; + uctx_local : ContextSet.t; (** The local context of variables *) + uctx_seff_univs : LSet.t; (** Local universes used through private constants *) uctx_univ_variables : UnivSubst.universe_opt_subst; (** The local universes that are unification variables *) - uctx_univ_algebraic : Univ.LSet.t; + uctx_univ_algebraic : LSet.t; (** The subset of unification variables that can be instantiated with algebraic universes as they appear in inferred types only. *) uctx_universes : UGraph.t; (** The current graph extended with the local constraints *) @@ -38,11 +39,11 @@ type t = } let empty = - { uctx_names = UNameMap.empty, Univ.LMap.empty; - uctx_local = Univ.ContextSet.empty; - uctx_seff_univs = Univ.LSet.empty; - uctx_univ_variables = Univ.LMap.empty; - uctx_univ_algebraic = Univ.LSet.empty; + { uctx_names = UNameMap.empty, LMap.empty; + uctx_local = ContextSet.empty; + uctx_seff_univs = LSet.empty; + uctx_univ_variables = LMap.empty; + uctx_univ_algebraic = LSet.empty; uctx_universes = UGraph.initial_universes; uctx_initial_universes = UGraph.initial_universes; uctx_weak_constraints = UPairSet.empty; } @@ -52,8 +53,8 @@ let make u = uctx_universes = u; uctx_initial_universes = u} let is_empty ctx = - Univ.ContextSet.is_empty ctx.uctx_local && - Univ.LMap.is_empty ctx.uctx_univ_variables + ContextSet.is_empty ctx.uctx_local && + LMap.is_empty ctx.uctx_univ_variables let uname_union s t = if s == t then s @@ -67,29 +68,29 @@ let union ctx ctx' = if ctx == ctx' then ctx else if is_empty ctx' then ctx else - let local = Univ.ContextSet.union ctx.uctx_local ctx'.uctx_local in - let seff = Univ.LSet.union ctx.uctx_seff_univs ctx'.uctx_seff_univs in + let local = ContextSet.union ctx.uctx_local ctx'.uctx_local in + let seff = LSet.union ctx.uctx_seff_univs ctx'.uctx_seff_univs in let names = uname_union (fst ctx.uctx_names) (fst ctx'.uctx_names) in - let newus = Univ.LSet.diff (Univ.ContextSet.levels ctx'.uctx_local) - (Univ.ContextSet.levels ctx.uctx_local) in - let newus = Univ.LSet.diff newus (Univ.LMap.domain ctx.uctx_univ_variables) in + let newus = LSet.diff (ContextSet.levels ctx'.uctx_local) + (ContextSet.levels ctx.uctx_local) in + let newus = LSet.diff newus (LMap.domain ctx.uctx_univ_variables) in let weak = UPairSet.union ctx.uctx_weak_constraints ctx'.uctx_weak_constraints in let declarenew g = - Univ.LSet.fold (fun u g -> UGraph.add_universe u false g) newus g + LSet.fold (fun u g -> UGraph.add_universe u false g) newus g in - let names_rev = Univ.LMap.union (snd ctx.uctx_names) (snd ctx'.uctx_names) in + let names_rev = LMap.union (snd ctx.uctx_names) (snd ctx'.uctx_names) in { uctx_names = (names, names_rev); uctx_local = local; uctx_seff_univs = seff; uctx_univ_variables = - Univ.LMap.subst_union ctx.uctx_univ_variables ctx'.uctx_univ_variables; + LMap.subst_union ctx.uctx_univ_variables ctx'.uctx_univ_variables; uctx_univ_algebraic = - Univ.LSet.union ctx.uctx_univ_algebraic ctx'.uctx_univ_algebraic; + LSet.union ctx.uctx_univ_algebraic ctx'.uctx_univ_algebraic; uctx_initial_universes = declarenew ctx.uctx_initial_universes; uctx_universes = (if local == ctx.uctx_local then ctx.uctx_universes else - let cstrsr = Univ.ContextSet.constraints ctx'.uctx_local in + let cstrsr = ContextSet.constraints ctx'.uctx_local in UGraph.merge_constraints cstrsr (declarenew ctx.uctx_universes)); uctx_weak_constraints = weak} @@ -97,14 +98,14 @@ let context_set ctx = ctx.uctx_local let constraints ctx = snd ctx.uctx_local -let context ctx = Univ.ContextSet.to_context ctx.uctx_local +let context ctx = ContextSet.to_context ctx.uctx_local let const_univ_entry ~poly uctx = let open Entries in if poly then let (binders, _) = uctx.uctx_names in let uctx = context uctx in - let nas = UnivNames.compute_instance_binders (Univ.UContext.instance uctx) binders in + let nas = UnivNames.compute_instance_binders (UContext.instance uctx) binders in Polymorphic_const_entry (nas, uctx) else Monomorphic_const_entry (context_set uctx) @@ -114,7 +115,7 @@ let ind_univ_entry ~poly uctx = if poly then let (binders, _) = uctx.uctx_names in let uctx = context uctx in - let nas = UnivNames.compute_instance_binders (Univ.UContext.instance uctx) binders in + let nas = UnivNames.compute_instance_binders (UContext.instance uctx) binders in Polymorphic_ind_entry (nas, uctx) else Monomorphic_ind_entry (context_set uctx) @@ -132,19 +133,19 @@ let add_uctx_names ?loc s l (names, names_rev) = if UNameMap.mem s names then user_err ?loc ~hdr:"add_uctx_names" Pp.(str "Universe " ++ Names.Id.print s ++ str" already bound."); - (UNameMap.add s l names, Univ.LMap.add l { uname = Some s; uloc = loc } names_rev) + (UNameMap.add s l names, LMap.add l { uname = Some s; uloc = loc } names_rev) let add_uctx_loc l loc (names, names_rev) = match loc with | None -> (names, names_rev) - | Some _ -> (names, Univ.LMap.add l { uname = None; uloc = loc } names_rev) + | Some _ -> (names, LMap.add l { uname = None; uloc = loc } names_rev) let of_binders b = let ctx = empty in let rmap = UNameMap.fold (fun id l rmap -> - Univ.LMap.add l { uname = Some id; uloc = None } rmap) - b Univ.LMap.empty + LMap.add l { uname = Some id; uloc = None } rmap) + b LMap.empty in { ctx with uctx_names = b, rmap } @@ -157,7 +158,6 @@ let invent_name (named,cnt) u = aux cnt let universe_binders ctx = - let open Univ in let named, rev = ctx.uctx_names in let named, _ = LSet.fold (fun u named -> match LMap.find u rev with @@ -169,7 +169,7 @@ let universe_binders ctx = named let instantiate_variable l b v = - try v := Univ.LMap.set l (Some b) !v + try v := LMap.set l (Some b) !v with Not_found -> assert false exception UniversesDiffer @@ -177,7 +177,6 @@ exception UniversesDiffer let drop_weak_constraints = ref false let process_universe_constraints ctx cstrs = - let open Univ in let open UnivSubst in let open UnivProblem in let univs = ctx.uctx_universes in @@ -190,9 +189,9 @@ let process_universe_constraints ctx cstrs = | UEq (u, v) -> UEq (subst_univs_universe normalize u, subst_univs_universe normalize v) | ULe (u, v) -> ULe (subst_univs_universe normalize u, subst_univs_universe normalize v) in - let is_local l = Univ.LMap.mem l !vars in + let is_local l = LMap.mem l !vars in let varinfo x = - match Univ.Universe.level x with + match Universe.level x with | None -> Inl x | Some l -> Inr l in @@ -206,27 +205,27 @@ let process_universe_constraints ctx cstrs = else if not (UGraph.check_eq_level univs l' r') then (* Two rigid/global levels, none of them being local, one of them being Prop/Set, disallow *) - if Univ.Level.is_small l' || Univ.Level.is_small r' then - raise (Univ.UniverseInconsistency (Univ.Eq, l, r, None)) + if Level.is_small l' || Level.is_small r' then + raise (UniverseInconsistency (Eq, l, r, None)) else if fo then raise UniversesDiffer in - Univ.enforce_eq_level l' r' local + enforce_eq_level l' r' local in let equalize_universes l r local = match varinfo l, varinfo r with | Inr l', Inr r' -> equalize_variables false l l' r r' local | Inr l, Inl r | Inl r, Inr l -> - let alg = Univ.LSet.mem l ctx.uctx_univ_algebraic in - let inst = Univ.univ_level_rem l r r in + let alg = LSet.mem l ctx.uctx_univ_algebraic in + let inst = univ_level_rem l r r in if alg then (instantiate_variable l inst vars; local) else - let lu = Univ.Universe.make l in - if Univ.univ_level_mem l r then - Univ.enforce_leq inst lu local - else raise (Univ.UniverseInconsistency (Univ.Eq, lu, r, None)) + let lu = Universe.make l in + if univ_level_mem l r then + enforce_leq inst lu local + else raise (UniverseInconsistency (Eq, lu, r, None)) | Inl _, Inl _ (* both are algebraic *) -> if UGraph.check_eq univs l r then local - else raise (Univ.UniverseInconsistency (Univ.Eq, l, r, None)) + else raise (UniverseInconsistency (Eq, l, r, None)) in let unify_universes cst local = let cst = nf_constraint cst in @@ -237,29 +236,29 @@ let process_universe_constraints ctx cstrs = if UGraph.check_leq univs l r then (* Keep Prop/Set <= var around if var might be instantiated by prop or set later. *) - match Univ.Universe.level l, Univ.Universe.level r with + match Universe.level l, Universe.level r with | Some l, Some r -> - Univ.Constraint.add (l, Univ.Le, r) local + Constraint.add (l, Le, r) local | _ -> local else - begin match Univ.Universe.level r with + begin match Universe.level r with | None -> user_err Pp.(str "Algebraic universe on the right") | Some r' -> - if Univ.Level.is_small r' then - if not (Univ.Universe.is_levels l) + if Level.is_small r' then + if not (Universe.is_levels l) then - raise (Univ.UniverseInconsistency (Univ.Le, l, r, None)) + raise (UniverseInconsistency (Le, l, r, None)) else - let levels = Univ.Universe.levels l in + let levels = Universe.levels l in let fold l' local = - let l = Univ.Universe.make l' in - if Univ.Level.is_small l' || is_local l' then + let l = Universe.make l' in + if Level.is_small l' || is_local l' then equalize_variables false l l' r r' local - else raise (Univ.UniverseInconsistency (Univ.Le, l, r, None)) + else raise (UniverseInconsistency (Le, l, r, None)) in - Univ.LSet.fold fold levels local + LSet.fold fold levels local else - Univ.enforce_leq l r local + enforce_leq l r local end | ULub (l, r) -> equalize_variables true (Universe.make l) l (Universe.make r) r local @@ -268,26 +267,26 @@ let process_universe_constraints ctx cstrs = | UEq (l, r) -> equalize_universes l r local in let local = - UnivProblem.Set.fold unify_universes cstrs Univ.Constraint.empty + UnivProblem.Set.fold unify_universes cstrs Constraint.empty in !vars, !weak, local let add_constraints ctx cstrs = let univs, local = ctx.uctx_local in - let cstrs' = Univ.Constraint.fold (fun (l,d,r) acc -> - let l = Univ.Universe.make l and r = Univ.Universe.make r in + let cstrs' = Constraint.fold (fun (l,d,r) acc -> + let l = Universe.make l and r = Universe.make r in let cstr' = let open UnivProblem in match d with - | Univ.Lt -> - ULe (Univ.Universe.super l, r) - | Univ.Le -> ULe (l, r) - | Univ.Eq -> UEq (l, r) + | Lt -> + ULe (Universe.super l, r) + | Le -> ULe (l, r) + | Eq -> UEq (l, r) in UnivProblem.Set.add cstr' acc) cstrs UnivProblem.Set.empty in let vars, weak, local' = process_universe_constraints ctx cstrs' in { ctx with - uctx_local = (univs, Univ.Constraint.union local local'); + uctx_local = (univs, Constraint.union local local'); uctx_univ_variables = vars; uctx_universes = UGraph.merge_constraints local' ctx.uctx_universes; uctx_weak_constraints = weak; } @@ -299,7 +298,7 @@ let add_universe_constraints ctx cstrs = let univs, local = ctx.uctx_local in let vars, weak, local' = process_universe_constraints ctx cstrs in { ctx with - uctx_local = (univs, Univ.Constraint.union local local'); + uctx_local = (univs, Constraint.union local local'); uctx_univ_variables = vars; uctx_universes = UGraph.merge_constraints local' ctx.uctx_universes; uctx_weak_constraints = weak; } @@ -307,14 +306,14 @@ let add_universe_constraints ctx cstrs = let constrain_variables diff ctx = let univs, local = ctx.uctx_local in let univs, vars, local = - Univ.LSet.fold + LSet.fold (fun l (univs, vars, cstrs) -> try - match Univ.LMap.find l vars with + match LMap.find l vars with | Some u -> - (Univ.LSet.add l univs, - Univ.LMap.remove l vars, - Univ.Constraint.add (l, Univ.Eq, Option.get (Univ.Universe.level u)) cstrs) + (LSet.add l univs, + LMap.remove l vars, + Constraint.add (l, Eq, Option.get (Universe.level u)) cstrs) | None -> (univs, vars, cstrs) with Not_found | Option.IsNone -> (univs, vars, cstrs)) diff (univs, ctx.uctx_univ_variables, local) @@ -324,14 +323,14 @@ let constrain_variables diff ctx = let qualid_of_level uctx = let map, map_rev = uctx.uctx_names in fun l -> - try Some (Libnames.qualid_of_ident (Option.get (Univ.LMap.find l map_rev).uname)) + try Some (Libnames.qualid_of_ident (Option.get (LMap.find l map_rev).uname)) with Not_found | Option.IsNone -> UnivNames.qualid_of_level l let pr_uctx_level uctx l = match qualid_of_level uctx l with | Some qid -> Libnames.pr_qualid qid - | None -> Univ.Level.pr l + | None -> Level.pr l type ('a, 'b) gen_universe_decl = { univdecl_instance : 'a; (* Declared universes *) @@ -340,16 +339,15 @@ type ('a, 'b) gen_universe_decl = { univdecl_extensible_constraints : bool (* Can new constraints be added *) } type universe_decl = - (lident list, Univ.Constraint.t) gen_universe_decl + (lident list, Constraint.t) gen_universe_decl let default_univ_decl = { univdecl_instance = []; univdecl_extensible_instance = true; - univdecl_constraints = Univ.Constraint.empty; + univdecl_constraints = Constraint.empty; univdecl_extensible_constraints = true } let error_unbound_universes left uctx = - let open Univ in let n = LSet.cardinal left in let loc = try @@ -365,7 +363,6 @@ let error_unbound_universes left uctx = str" unbound.")) let universe_context ~names ~extensible uctx = - let open Univ in let levels = ContextSet.levels uctx.uctx_local in let newinst, left = List.fold_right @@ -388,7 +385,6 @@ let universe_context ~names ~extensible uctx = let check_universe_context_set ~names ~extensible uctx = if extensible then () else - let open Univ in let left = List.fold_left (fun left { CAst.loc; v = id } -> let l = try UNameMap.find id (fst uctx.uctx_names) @@ -415,7 +411,7 @@ let check_mono_univ_decl uctx decl = if not decl.univdecl_extensible_constraints then check_implication uctx decl.univdecl_constraints - (Univ.ContextSet.constraints uctx.uctx_local); + (ContextSet.constraints uctx.uctx_local); uctx.uctx_local let check_univ_decl ~poly uctx decl = @@ -425,7 +421,7 @@ let check_univ_decl ~poly uctx decl = if poly then let (binders, _) = uctx.uctx_names in let uctx = universe_context ~names ~extensible uctx in - let nas = UnivNames.compute_instance_binders (Univ.UContext.instance uctx) binders in + let nas = UnivNames.compute_instance_binders (UContext.instance uctx) binders in Entries.Polymorphic_const_entry (nas, uctx) else let () = check_universe_context_set ~names ~extensible uctx in @@ -434,11 +430,10 @@ let check_univ_decl ~poly uctx decl = if not decl.univdecl_extensible_constraints then check_implication uctx decl.univdecl_constraints - (Univ.ContextSet.constraints uctx.uctx_local); + (ContextSet.constraints uctx.uctx_local); ctx let restrict_universe_context (univs, csts) keep = - let open Univ in let removed = LSet.diff univs keep in if LSet.is_empty removed then univs, csts else @@ -453,8 +448,8 @@ let restrict_universe_context (univs, csts) keep = (LSet.inter univs keep, csts) let restrict ctx vars = - let vars = Univ.LSet.union vars ctx.uctx_seff_univs in - let vars = Names.Id.Map.fold (fun na l vars -> Univ.LSet.add l vars) + let vars = LSet.union vars ctx.uctx_seff_univs in + let vars = Names.Id.Map.fold (fun na l vars -> LSet.add l vars) (fst ctx.uctx_names) vars in let uctx' = restrict_universe_context ctx.uctx_local vars in @@ -465,7 +460,7 @@ let demote_seff_univs entry uctx = match entry.const_entry_universes with | Polymorphic_const_entry _ -> uctx | Monomorphic_const_entry (univs, _) -> - let seff = Univ.LSet.union uctx.uctx_seff_univs univs in + let seff = LSet.union uctx.uctx_seff_univs univs in { uctx with uctx_seff_univs = seff } type rigid = @@ -483,7 +478,6 @@ let univ_flexible_alg = UnivFlexible true or defined separately. In the later case, there is no extension, see [emit_side_effects] for example. *) let merge ?loc ~sideff ~extend rigid uctx ctx' = - let open Univ in let levels = ContextSet.levels ctx' in let uctx = if not extend then uctx else @@ -527,7 +521,7 @@ let merge ?loc ~sideff ~extend rigid uctx ctx' = uctx_initial_universes = initial } let merge_subst uctx s = - { uctx with uctx_univ_variables = Univ.LMap.subst_union uctx.uctx_univ_variables s } + { uctx with uctx_univ_variables = LMap.subst_union uctx.uctx_univ_variables s } let emit_side_effects eff u = let uctxs = Safe_typing.universes_of_private eff in @@ -536,14 +530,14 @@ let emit_side_effects eff u = let new_univ_variable ?loc rigid name ({ uctx_local = ctx; uctx_univ_variables = uvars; uctx_univ_algebraic = avars} as uctx) = let u = UnivGen.fresh_level () in - let ctx' = Univ.ContextSet.add_universe u ctx in + let ctx' = ContextSet.add_universe u ctx in let uctx', pred = match rigid with | UnivRigid -> uctx, true | UnivFlexible b -> - let uvars' = Univ.LMap.add u None uvars in + let uvars' = LMap.add u None uvars in if b then {uctx with uctx_univ_variables = uvars'; - uctx_univ_algebraic = Univ.LSet.add u avars}, false + uctx_univ_algebraic = LSet.add u avars}, false else {uctx with uctx_univ_variables = uvars'}, false in let names = @@ -574,12 +568,11 @@ let add_global_univ uctx u = let univs = UGraph.add_universe u true uctx.uctx_universes in - { uctx with uctx_local = Univ.ContextSet.add_universe u uctx.uctx_local; + { uctx with uctx_local = ContextSet.add_universe u uctx.uctx_local; uctx_initial_universes = initial; uctx_universes = univs } let make_flexible_variable ctx ~algebraic u = - let open Univ in let {uctx_local = cstrs; uctx_univ_variables = uvars; uctx_univ_algebraic = avars; uctx_universes=g; } = ctx in assert (try LMap.find u uvars == None with Not_found -> true); @@ -608,48 +601,47 @@ let make_flexible_variable ctx ~algebraic u = uctx_univ_algebraic = avars'} let make_nonalgebraic_variable ctx u = - { ctx with uctx_univ_algebraic = Univ.LSet.remove u ctx.uctx_univ_algebraic } + { ctx with uctx_univ_algebraic = LSet.remove u ctx.uctx_univ_algebraic } let make_flexible_nonalgebraic ctx = - {ctx with uctx_univ_algebraic = Univ.LSet.empty} + {ctx with uctx_univ_algebraic = LSet.empty} let is_sort_variable uctx s = match s with | Sorts.Type u -> - (match Univ.universe_level u with + (match universe_level u with | Some l as x -> - if Univ.LSet.mem l (Univ.ContextSet.levels uctx.uctx_local) then x + if LSet.mem l (ContextSet.levels uctx.uctx_local) then x else None | None -> None) | _ -> None let subst_univs_context_with_def def usubst (ctx, cst) = - (Univ.LSet.diff ctx def, UnivSubst.subst_univs_constraints usubst cst) + (LSet.diff ctx def, UnivSubst.subst_univs_constraints usubst cst) let is_trivial_leq (l,d,r) = - Univ.Level.is_prop l && (d == Univ.Le || (d == Univ.Lt && Univ.Level.is_set r)) + Level.is_prop l && (d == Le || (d == Lt && Level.is_set r)) (* Prop < i <-> Set+1 <= i <-> Set < i *) let translate_cstr (l,d,r as cstr) = - let open Univ in - if Level.equal Level.prop l && d == Univ.Lt && not (Level.equal Level.set r) then + if Level.equal Level.prop l && d == Lt && not (Level.equal Level.set r) then (Level.set, d, r) else cstr let refresh_constraints univs (ctx, cstrs) = let cstrs', univs' = - Univ.Constraint.fold (fun c (cstrs', univs as acc) -> + Constraint.fold (fun c (cstrs', univs as acc) -> let c = translate_cstr c in if is_trivial_leq c then acc - else (Univ.Constraint.add c cstrs', UGraph.enforce_constraint c univs)) - cstrs (Univ.Constraint.empty, univs) + else (Constraint.add c cstrs', UGraph.enforce_constraint c univs)) + cstrs (Constraint.empty, univs) in ((ctx, cstrs'), univs') let normalize_variables uctx = let normalized_variables, def, subst = UnivSubst.normalize_univ_variables uctx.uctx_univ_variables in - let ctx_local = subst_univs_context_with_def def (Univ.make_subst subst) uctx.uctx_local in + let ctx_local = subst_univs_context_with_def def (make_subst subst) uctx.uctx_local in let ctx_local', univs = refresh_constraints uctx.uctx_initial_universes ctx_local in subst, { uctx with uctx_local = ctx_local'; uctx_univ_variables = normalized_variables; @@ -657,17 +649,17 @@ let normalize_variables uctx = let abstract_undefined_variables uctx = let vars' = - Univ.LMap.fold (fun u v acc -> - if v == None then Univ.LSet.remove u acc + LMap.fold (fun u v acc -> + if v == None then LSet.remove u acc else acc) uctx.uctx_univ_variables uctx.uctx_univ_algebraic - in { uctx with uctx_local = Univ.ContextSet.empty; + in { uctx with uctx_local = ContextSet.empty; uctx_univ_algebraic = vars' } let fix_undefined_variables uctx = let algs', vars' = - Univ.LMap.fold (fun u v (algs, vars as acc) -> - if v == None then (Univ.LSet.remove u algs, Univ.LMap.remove u vars) + LMap.fold (fun u v (algs, vars as acc) -> + if v == None then (LSet.remove u algs, LMap.remove u vars) else acc) uctx.uctx_univ_variables (uctx.uctx_univ_algebraic, uctx.uctx_univ_variables) @@ -677,20 +669,20 @@ let fix_undefined_variables uctx = let refresh_undefined_univ_variables uctx = let subst, ctx' = UnivGen.fresh_universe_context_set_instance uctx.uctx_local in - let subst_fn u = Univ.subst_univs_level_level subst u in - let alg = Univ.LSet.fold (fun u acc -> Univ.LSet.add (subst_fn u) acc) - uctx.uctx_univ_algebraic Univ.LSet.empty + let subst_fn u = subst_univs_level_level subst u in + let alg = LSet.fold (fun u acc -> LSet.add (subst_fn u) acc) + uctx.uctx_univ_algebraic LSet.empty in let vars = - Univ.LMap.fold + LMap.fold (fun u v acc -> - Univ.LMap.add (subst_fn u) - (Option.map (Univ.subst_univs_level_universe subst) v) acc) - uctx.uctx_univ_variables Univ.LMap.empty + LMap.add (subst_fn u) + (Option.map (subst_univs_level_universe subst) v) acc) + uctx.uctx_univ_variables LMap.empty in let weak = UPairSet.fold (fun (u,v) acc -> UPairSet.add (subst_fn u, subst_fn v) acc) uctx.uctx_weak_constraints UPairSet.empty in - let declare g = Univ.LSet.fold (fun u g -> UGraph.add_universe u false g) - (Univ.ContextSet.levels ctx') g in + let declare g = LSet.fold (fun u g -> UGraph.add_universe u false g) + (ContextSet.levels ctx') g in let initial = declare uctx.uctx_initial_universes in let univs = declare UGraph.initial_universes in let uctx' = {uctx_names = uctx.uctx_names; @@ -708,7 +700,7 @@ let minimize uctx = normalize_context_set uctx.uctx_universes uctx.uctx_local uctx.uctx_univ_variables uctx.uctx_univ_algebraic uctx.uctx_weak_constraints in - if Univ.ContextSet.equal us' uctx.uctx_local then uctx + if ContextSet.equal us' uctx.uctx_local then uctx else let us', universes = refresh_constraints uctx.uctx_initial_universes us' diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml index d4bafe773f..7adae148bd 100644 --- a/plugins/micromega/coq_micromega.ml +++ b/plugins/micromega/coq_micromega.ml @@ -846,7 +846,7 @@ struct match env with | [] -> ([v],n) | e::l -> - if EConstr.eq_constr sigma e v + if EConstr.eq_constr_nounivs sigma e v then (env,n) else let (env,n) = _add l ( n+1) v in diff --git a/plugins/omega/PreOmega.v b/plugins/omega/PreOmega.v index 94a3d40441..695f000cb1 100644 --- a/plugins/omega/PreOmega.v +++ b/plugins/omega/PreOmega.v @@ -12,6 +12,120 @@ Require Import Arith Max Min BinInt BinNat Znat Nnat. Local Open Scope Z_scope. +(** * [Z.div_mod_to_equations], [Z.quot_rem_to_equations], [Z.to_euclidean_division_equations]: the tactics for preprocessing [Z.div] and [Z.modulo], [Z.quot] and [Z.rem] *) + +(** These tactic use the complete specification of [Z.div] and + [Z.modulo] ([Z.quot] and [Z.rem], respectively) to remove these + functions from the goal without losing information. The + [Z.euclidean_division_equations_cleanup] tactic removes needless + hypotheses, which makes tactics like [nia] run faster. The tactic + [Z.to_euclidean_division_equations] combines the handling of both variants + of division/quotient and modulo/remainder. *) + +Module Z. + Lemma mod_0_r_ext x y : y = 0 -> x mod y = 0. + Proof. intro; subst; destruct x; reflexivity. Qed. + Lemma div_0_r_ext x y : y = 0 -> x / y = 0. + Proof. intro; subst; destruct x; reflexivity. Qed. + + Lemma rem_0_r_ext x y : y = 0 -> Z.rem x y = x. + Proof. intro; subst; destruct x; reflexivity. Qed. + Lemma quot_0_r_ext x y : y = 0 -> Z.quot x y = 0. + Proof. intro; subst; destruct x; reflexivity. Qed. + + Lemma rem_bound_pos_pos x y : 0 < y -> 0 <= x -> 0 <= Z.rem x y < y. + Proof. intros; apply Z.rem_bound_pos; assumption. Qed. + Lemma rem_bound_neg_pos x y : y < 0 -> 0 <= x -> 0 <= Z.rem x y < -y. + Proof. rewrite <- Z.rem_opp_r'; intros; apply Z.rem_bound_pos; rewrite ?Z.opp_pos_neg; assumption. Qed. + Lemma rem_bound_pos_neg x y : 0 < y -> x <= 0 -> -y < Z.rem x y <= 0. + Proof. rewrite <- (Z.opp_involutive x), Z.rem_opp_l', <- Z.opp_lt_mono, and_comm, !Z.opp_nonpos_nonneg; apply rem_bound_pos_pos. Qed. + Lemma rem_bound_neg_neg x y : y < 0 -> x <= 0 -> y < Z.rem x y <= 0. + Proof. rewrite <- (Z.opp_involutive x), <- (Z.opp_involutive y), Z.rem_opp_l', <- Z.opp_lt_mono, and_comm, !Z.opp_nonpos_nonneg, Z.opp_involutive; apply rem_bound_neg_pos. Qed. + + Ltac div_mod_to_equations_generalize x y := + pose proof (Z.div_mod x y); + pose proof (Z.mod_pos_bound x y); + pose proof (Z.mod_neg_bound x y); + pose proof (div_0_r_ext x y); + pose proof (mod_0_r_ext x y); + let q := fresh "q" in + let r := fresh "r" in + set (q := x / y) in *; + set (r := x mod y) in *; + clearbody q r. + Ltac quot_rem_to_equations_generalize x y := + pose proof (Z.quot_rem' x y); + pose proof (rem_bound_pos_pos x y); + pose proof (rem_bound_pos_neg x y); + pose proof (rem_bound_neg_pos x y); + pose proof (rem_bound_neg_neg x y); + pose proof (quot_0_r_ext x y); + pose proof (rem_0_r_ext x y); + let q := fresh "q" in + let r := fresh "r" in + set (q := Z.quot x y) in *; + set (r := Z.rem x y) in *; + clearbody q r. + + Ltac div_mod_to_equations_step := + match goal with + | [ |- context[?x / ?y] ] => div_mod_to_equations_generalize x y + | [ |- context[?x mod ?y] ] => div_mod_to_equations_generalize x y + | [ H : context[?x / ?y] |- _ ] => div_mod_to_equations_generalize x y + | [ H : context[?x mod ?y] |- _ ] => div_mod_to_equations_generalize x y + end. + Ltac quot_rem_to_equations_step := + match goal with + | [ |- context[Z.quot ?x ?y] ] => quot_rem_to_equations_generalize x y + | [ |- context[Z.rem ?x ?y] ] => quot_rem_to_equations_generalize x y + | [ H : context[Z.quot ?x ?y] |- _ ] => quot_rem_to_equations_generalize x y + | [ H : context[Z.rem ?x ?y] |- _ ] => quot_rem_to_equations_generalize x y + end. + Ltac div_mod_to_equations' := repeat div_mod_to_equations_step. + Ltac quot_rem_to_equations' := repeat quot_rem_to_equations_step. + Ltac euclidean_division_equations_cleanup := + repeat match goal with + | [ H : ?x = ?x -> _ |- _ ] => specialize (H eq_refl) + | [ H : ?x <> ?x -> _ |- _ ] => clear H + | [ H : ?x < ?x -> _ |- _ ] => clear H + | [ H : ?T -> _, H' : ?T |- _ ] => specialize (H H') + | [ H : ?T -> _, H' : ~?T |- _ ] => clear H + | [ H : ~?T -> _, H' : ?T |- _ ] => clear H + | [ H : ?A -> ?x = ?x -> _ |- _ ] => specialize (fun a => H a eq_refl) + | [ H : ?A -> ?x <> ?x -> _ |- _ ] => clear H + | [ H : ?A -> ?x < ?x -> _ |- _ ] => clear H + | [ H : ?A -> ?B -> _, H' : ?B |- _ ] => specialize (fun a => H a H') + | [ H : ?A -> ?B -> _, H' : ~?B |- _ ] => clear H + | [ H : ?A -> ~?B -> _, H' : ?B |- _ ] => clear H + | [ H : 0 < ?x -> _, H' : ?x < 0 |- _ ] => clear H + | [ H : ?x < 0 -> _, H' : 0 < ?x |- _ ] => clear H + | [ H : ?A -> 0 < ?x -> _, H' : ?x < 0 |- _ ] => clear H + | [ H : ?A -> ?x < 0 -> _, H' : 0 < ?x |- _ ] => clear H + | [ H : 0 <= ?x -> _, H' : ?x < 0 |- _ ] => clear H + | [ H : ?x <= 0 -> _, H' : 0 < ?x |- _ ] => clear H + | [ H : ?A -> 0 <= ?x -> _, H' : ?x < 0 |- _ ] => clear H + | [ H : ?A -> ?x <= 0 -> _, H' : 0 < ?x |- _ ] => clear H + | [ H : 0 < ?x -> _, H' : ?x <= 0 |- _ ] => clear H + | [ H : ?x < 0 -> _, H' : 0 <= ?x |- _ ] => clear H + | [ H : ?A -> 0 < ?x -> _, H' : ?x <= 0 |- _ ] => clear H + | [ H : ?A -> ?x < 0 -> _, H' : 0 <= ?x |- _ ] => clear H + | [ H : 0 <= ?x -> _, H' : ?x <= 0 |- _ ] => specialize (fun pf => H (@Z.eq_le_incl 0 x (eq_sym pf))) + | [ H : ?A -> 0 <= ?x -> _, H' : ?x <= 0 |- _ ] => specialize (fun a pf => H a (@Z.eq_le_incl 0 x (eq_sym pf))) + | [ H : ?x <= 0 -> _, H' : 0 <= ?x |- _ ] => specialize (fun pf => H (@Z.eq_le_incl 0 x pf)) + | [ H : ?A -> ?x <= 0 -> _, H' : 0 <= ?x |- _ ] => specialize (fun a pf => H a (@Z.eq_le_incl x 0 pf)) + | [ H : ?x < ?y -> _, H' : ?x = ?y |- _ ] => clear H + | [ H : ?x < ?y -> _, H' : ?y = ?x |- _ ] => clear H + | [ H : ?A -> ?x < ?y -> _, H' : ?x = ?y |- _ ] => clear H + | [ H : ?A -> ?x < ?y -> _, H' : ?y = ?x |- _ ] => clear H + | [ H : ?x = ?y -> _, H' : ?x < ?y |- _ ] => clear H + | [ H : ?x = ?y -> _, H' : ?y < ?x |- _ ] => clear H + | [ H : ?A -> ?x = ?y -> _, H' : ?x < ?y |- _ ] => clear H + | [ H : ?A -> ?x = ?y -> _, H' : ?y < ?x |- _ ] => clear H + end. + Ltac div_mod_to_equations := div_mod_to_equations'; euclidean_division_equations_cleanup. + Ltac quot_rem_to_equations := quot_rem_to_equations'; euclidean_division_equations_cleanup. + Ltac to_euclidean_division_equations := div_mod_to_equations'; quot_rem_to_equations'; euclidean_division_equations_cleanup. +End Z. (** * zify: the Z-ification tactic *) @@ -411,6 +525,24 @@ Ltac zify_N_op := | |- context [ Z.of_N (N.mul ?a ?b) ] => pose proof (N2Z.is_nonneg (N.mul a b)); rewrite (N2Z.inj_mul a b) in * + (* N.div -> Z.div and a positivity hypothesis *) + | H : context [ Z.of_N (N.div ?a ?b) ] |- _ => + pose proof (N2Z.is_nonneg (N.div a b)); rewrite (N2Z.inj_div a b) in * + | |- context [ Z.of_N (N.div ?a ?b) ] => + pose proof (N2Z.is_nonneg (N.div a b)); rewrite (N2Z.inj_div a b) in * + + (* N.modulo -> Z.rem / Z.modulo and a positivity hypothesis (N.modulo agrees with Z.modulo on everything except 0; so we pose both the non-zero proof for this agreement, but also replace things with [Z.rem]) *) + | H : context [ Z.of_N (N.modulo ?a ?b) ] |- _ => + pose proof (N2Z.is_nonneg (N.modulo a b)); + pose proof (@Z.quot_div_nonneg (Z.of_N a) (Z.of_N b) (N2Z.is_nonneg a)); + pose proof (@Z.rem_mod_nonneg (Z.of_N a) (Z.of_N b) (N2Z.is_nonneg a)); + rewrite (N2Z.inj_rem a b) in * + | |- context [ Z.of_N (N.div ?a ?b) ] => + pose proof (N2Z.is_nonneg (N.modulo a b)); + pose proof (@Z.quot_div_nonneg (Z.of_N a) (Z.of_N b) (N2Z.is_nonneg a)); + pose proof (@Z.rem_mod_nonneg (Z.of_N a) (Z.of_N b) (N2Z.is_nonneg a)); + rewrite (N2Z.inj_rem a b) in * + (* atoms of type N : we add a positivity condition (if not already there) *) | _ : 0 <= Z.of_N ?a |- _ => hide_Z_of_N a | _ : context [ Z.of_N ?a ] |- _ => pose proof (N2Z.is_nonneg a); hide_Z_of_N a diff --git a/test-suite/bugs/closed/bug_9268.v b/test-suite/bugs/closed/bug_9268.v new file mode 100644 index 0000000000..02dd46f6d2 --- /dev/null +++ b/test-suite/bugs/closed/bug_9268.v @@ -0,0 +1,46 @@ +Require Import Coq.ZArith.ZArith. +Require Import Coq.micromega.Lia. + +Local Open Scope Z_scope. + +Definition Register := Z%type. + +Definition Opcode := Z%type. + +Inductive InstructionI : Type + := Lb : Register -> Register -> Z -> InstructionI + | InvalidI : InstructionI. + +Inductive Instruction : Type + := IInstruction : InstructionI -> Instruction. + +Definition funct3_LB : Z := 0. + +Definition opcode_LOAD : Opcode := 3. + +Set Universe Polymorphism. + +Definition MachineInt := Z. + +Definition funct3_JALR := 0. + +Axiom InstructionMapper: Type -> Type. + +Definition apply_InstructionMapper(mapper: InstructionMapper Z)(inst: Instruction): Z := + match inst with + | IInstruction InvalidI => 2 + | IInstruction (Lb rd rs1 oimm12) => 3 + end. + +Axiom Encoder: InstructionMapper MachineInt. + +Definition encode: Instruction -> MachineInt := apply_InstructionMapper Encoder. + +Lemma foo: forall (ins: InstructionI), + 0 <= encode (IInstruction ins) -> + 0 <= encode (IInstruction ins) . +Proof. + Set Printing Universes. + intros. + lia. +Qed. diff --git a/test-suite/coqchk/inductive_functor_squash.v b/test-suite/coqchk/inductive_functor_squash.v new file mode 100644 index 0000000000..9d33fafc4c --- /dev/null +++ b/test-suite/coqchk/inductive_functor_squash.v @@ -0,0 +1,15 @@ + + +Module Type T. + Parameter f : nat -> Type. +End T. + +Module F(A:T). + Inductive ind : Prop := + C : A.f 0 -> ind. +End F. + +Module A. Definition f (x:nat) := True. End A. + +Module M := F A. +(* M.ind could eliminate into Set/Type even though F.ind can't *) diff --git a/test-suite/success/Nia.v b/test-suite/success/Nia.v new file mode 100644 index 0000000000..62ecece792 --- /dev/null +++ b/test-suite/success/Nia.v @@ -0,0 +1,918 @@ +Require Import Coq.ZArith.ZArith. +Require Import Coq.micromega.Lia. +Open Scope Z_scope. + +(** Add [Z.to_euclidean_division_equations] to the end of [zify], just for this + file. *) +Ltac zify ::= repeat (zify_nat; zify_positive; zify_N); zify_op; Z.to_euclidean_division_equations. + +Lemma Z_zerop_or x : x = 0 \/ x <> 0. Proof. nia. Qed. +Lemma Z_eq_dec_or (x y : Z) : x = y \/ x <> y. Proof. nia. Qed. + +Ltac unique_pose_proof pf := + let T := type of pf in + lazymatch goal with + | [ H : T |- _ ] => fail + | _ => pose proof pf + end. + +Ltac saturate_mod_div := + repeat match goal with + | [ |- context[?x mod ?y] ] => unique_pose_proof (Z_zerop_or (x / y)) + | [ H : context[?x mod ?y] |- _ ] => unique_pose_proof (Z_zerop_or (x / y)) + | [ |- context[?x / ?y] ] => unique_pose_proof (Z_zerop_or y) + | [ H : context[?x / ?y] |- _ ] => unique_pose_proof (Z_zerop_or y) + | [ |- context[Z.rem ?x ?y] ] => unique_pose_proof (Z_zerop_or (Z.quot x y)) + | [ H : context[Z.rem ?x ?y] |- _ ] => unique_pose_proof (Z_zerop_or (Z.quot x y)) + | [ |- context[Z.quot ?x ?y] ] => unique_pose_proof (Z_zerop_or y) + | [ H : context[Z.quot ?x ?y] |- _ ] => unique_pose_proof (Z_zerop_or y) + end. + +Ltac t := intros; saturate_mod_div; try nia. + +Ltac destr_step := + match goal with + | [ H : and _ _ |- _ ] => destruct H + | [ H : or _ _ |- _ ] => destruct H + end. + +Example mod_0_l: forall x : Z, 0 mod x = 0. Proof. t. Qed. +Example mod_0_r: forall x : Z, x mod 0 = 0. Proof. intros; nia. Qed. +Example Z_mod_same_full: forall a : Z, a mod a = 0. Proof. t. Qed. +Example Zmod_0_l: forall a : Z, 0 mod a = 0. Proof. t. Qed. +Example Zmod_0_r: forall a : Z, a mod 0 = 0. Proof. intros; nia. Qed. +Example mod_mod_same: forall x y : Z, (x mod y) mod y = x mod y. Proof. t. Qed. +Example Zmod_mod: forall a n : Z, (a mod n) mod n = a mod n. Proof. t. Qed. +Example Zmod_1_r: forall a : Z, a mod 1 = 0. Proof. intros; nia. Qed. +Example Zmod_div: forall a b : Z, a mod b / b = 0. Proof. intros; nia. Qed. +Example Z_mod_1_r: forall a : Z, a mod 1 = 0. Proof. intros; nia. Qed. +Example Z_mod_same: forall a : Z, a > 0 -> a mod a = 0. Proof. t. Qed. +Example Z_mod_mult: forall a b : Z, (a * b) mod b = 0. +Proof. + intros a b. + assert (b = 0 \/ (a * b) / b = a) by nia. + nia. +Qed. +Example Z_mod_same': forall a : Z, a <> 0 -> a mod a = 0. Proof. t. Qed. +Example Z_mod_0_l: forall a : Z, a <> 0 -> 0 mod a = 0. Proof. t. Qed. +Example Zmod_opp_opp: forall a b : Z, - a mod - b = - (a mod b). +Proof. + intros a b. + pose proof (Z_eq_dec_or ((-a)/(-b)) (a/b)). + nia. +Qed. +Example Z_mod_le: forall a b : Z, 0 <= a -> 0 < b -> a mod b <= a. Proof. t. Qed. +Example Zmod_le: forall a b : Z, 0 < b -> 0 <= a -> a mod b <= a. Proof. t. Qed. +Example Zplus_mod_idemp_r: forall a b n : Z, (b + a mod n) mod n = (b + a) mod n. +Proof. + intros a b n. + destruct (Z_zerop n); [ subst; nia | ]. + assert ((b + a mod n) / n = (b / n) + (b mod n + a mod n) / n) + by nia. + assert ((b + a) / n = (b / n) + (a / n) + (b mod n + a mod n) / n) + by nia. + nia. +Qed. +Example Zplus_mod_idemp_l: forall a b n : Z, (a mod n + b) mod n = (a + b) mod n. +Proof. + intros a b n. + destruct (Z_zerop n); [ subst; nia | ]. + assert ((a mod n + b) / n = (b / n) + (b mod n + a mod n) / n) by nia. + assert ((a + b) / n = (b / n) + (a / n) + (b mod n + a mod n) / n) by nia. + nia. +Qed. +Example Zmult_mod_distr_r: forall a b c : Z, (a * c) mod (b * c) = a mod b * c. +Proof. + intros a b c. + destruct (Z_zerop c); try nia. + pose proof (Z_eq_dec_or ((a * c) / (b * c)) (a / b)). + nia. +Qed. +Example Z_mod_zero_opp_full: forall a b : Z, a mod b = 0 -> - a mod b = 0. +Proof. + intros a b. + pose proof (Z_eq_dec_or (a/b) (-(-a/b))). + nia. +Qed. +Example Zmult_mod_idemp_r: forall a b n : Z, (b * (a mod n)) mod n = (b * a) mod n. +Proof. + intros a b n. + destruct (Z_zerop n); [ subst; nia | ]. + assert ((b * (a mod n)) / n = (b / n) * (a mod n) + ((b mod n) * (a mod n)) / n) + by nia. + assert ((b * a) / n = (b / n) * (a / n) * n + (b / n) * (a mod n) + (b mod n) * (a / n) + ((b mod n) * (a mod n)) / n) + by nia. + nia. +Qed. +Example Zmult_mod_idemp_l: forall a b n : Z, (a mod n * b) mod n = (a * b) mod n. +Proof. + intros a b n. + destruct (Z_zerop n); [ subst; nia | ]. + assert (((a mod n) * b) / n = (b / n) * (a mod n) + ((b mod n) * (a mod n)) / n) + by nia. + assert ((a * b) / n = (b / n) * (a / n) * n + (b / n) * (a mod n) + (b mod n) * (a / n) + ((b mod n) * (a mod n)) / n) + by nia. + nia. +Qed. +Example Zminus_mod_idemp_r: forall a b n : Z, (a - b mod n) mod n = (a - b) mod n. +Proof. + intros a b n. + destruct (Z_zerop n); [ subst; nia | ]. + assert ((a - b mod n) / n = a / n + ((a mod n) - (b mod n)) / n) by nia. + assert ((a - b) / n = a / n - b / n + ((a mod n) - (b mod n)) / n) by nia. + nia. +Qed. +Example Zminus_mod_idemp_l: forall a b n : Z, (a mod n - b) mod n = (a - b) mod n. +Proof. + intros a b n. + destruct (Z_zerop n); [ subst; nia | ]. + assert ((a mod n - b) / n = - (b / n) + ((a mod n) - (b mod n)) / n) by nia. + assert ((a - b) / n = a / n - b / n + ((a mod n) - (b mod n)) / n) by nia. + nia. +Qed. +Example Z_mod_plus_full: forall a b c : Z, (a + b * c) mod c = a mod c. +Proof. + intros a b c. + pose proof (Z_eq_dec_or ((a+b*c)/c) (a/c + b)). + nia. +Qed. +Example Zmult_mod_distr_l: forall a b c : Z, (c * a) mod (c * b) = c * (a mod b). +Proof. + intros a b c. + destruct (Z_zerop c); try nia. + pose proof (Z_eq_dec_or ((c * a) / (c * b)) (a / b)). + nia. +Qed. +Example Z_mod_zero_opp_r: forall a b : Z, a mod b = 0 -> a mod - b = 0. +Proof. + intros a b. + pose proof (Z_eq_dec_or (a/b) (-(a/-b))). + nia. +Qed. +Example Zmod_1_l: forall a : Z, 1 < a -> 1 mod a = 1. Proof. t. Qed. +Example Z_mod_1_l: forall a : Z, 1 < a -> 1 mod a = 1. Proof. t. Qed. +Example Z_mod_mul: forall a b : Z, b <> 0 -> (a * b) mod b = 0. +Proof. + intros a b. + pose proof (Z_eq_dec_or ((a*b)/b) a). + nia. +Qed. +Example Zminus_mod: forall a b n : Z, (a - b) mod n = (a mod n - b mod n) mod n. +Proof. + intros a b n. + destruct (Z_zerop n); [ subst; nia | ]. + assert ((a - b) / n = (a / n) - (b / n) + ((a mod n) - (b mod n)) / n) by nia. + nia. +Qed. +Example Zplus_mod: forall a b n : Z, (a + b) mod n = (a mod n + b mod n) mod n. +Proof. + intros a b n. + destruct (Z_zerop n); [ subst; nia | ]. + assert ((a + b) / n = (a / n) + (b / n) + ((a mod n) + (b mod n)) / n) by nia. + nia. +Qed. +Example Zmult_mod: forall a b n : Z, (a * b) mod n = (a mod n * (b mod n)) mod n. +Proof. + intros a b n. + destruct (Z_zerop n); [ subst; nia | ]. + assert ((a * b) / n = n * (a / n) * (b / n) + (a mod n) * (b / n) + (a / n) * (b mod n) + ((a mod n) * (b mod n)) / n) + by nia. + nia. +Qed. +Example Z_mod_mod: forall a n : Z, n <> 0 -> (a mod n) mod n = a mod n. Proof. t. Qed. +Example Z_mod_div: forall a b : Z, b <> 0 -> a mod b / b = 0. Proof. intros; nia. Qed. +Example Z_div_exact_full_1: forall a b : Z, a = b * (a / b) -> a mod b = 0. Proof. intros; nia. Qed. +Example Z_mod_pos_bound: forall a b : Z, 0 < b -> 0 <= a mod b < b. Proof. intros; nia. Qed. +Example Z_mod_sign_mul: forall a b : Z, b <> 0 -> 0 <= a mod b * b. Proof. intros; nia. Qed. +Example Z_mod_neg_bound: forall a b : Z, b < 0 -> b < a mod b <= 0. Proof. intros; nia. Qed. +Example Z_mod_neg: forall a b : Z, b < 0 -> b < a mod b <= 0. Proof. intros; nia. Qed. +Example div_mod_small: forall x y : Z, 0 <= x < y -> x mod y = x. Proof. t. Qed. +Example Zmod_small: forall a n : Z, 0 <= a < n -> a mod n = a. Proof. t. Qed. +Example Z_mod_small: forall a b : Z, 0 <= a < b -> a mod b = a. Proof. t. Qed. +Example Z_div_zero_opp_full: forall a b : Z, a mod b = 0 -> - a / b = - (a / b). Proof. intros; nia. Qed. +Example Z_mod_zero_opp: forall a b : Z, b > 0 -> a mod b = 0 -> - a mod b = 0. +Proof. + intros a b. + pose proof (Z_eq_dec_or (a/b) (-(-a/b))). + nia. +Qed. +Example Z_div_zero_opp_r: forall a b : Z, a mod b = 0 -> a / - b = - (a / b). Proof. intros; nia. Qed. +Example Z_mod_lt: forall a b : Z, b > 0 -> 0 <= a mod b < b. Proof. intros; nia. Qed. +Example Z_mod_opp_opp: forall a b : Z, b <> 0 -> - a mod - b = - (a mod b). +Proof. + intros a b. + pose proof (Z_eq_dec_or ((-a)/(-b)) ((a/b))). + nia. +Qed. +Example Z_mod_bound_pos: forall a b : Z, 0 <= a -> 0 < b -> 0 <= a mod b < b. Proof. intros; nia. Qed. +Example Z_mod_opp_l_z: forall a b : Z, b <> 0 -> a mod b = 0 -> - a mod b = 0. +Proof. + intros a b. + pose proof (Z_eq_dec_or (a/b) (-(-a/b))). + nia. +Qed. +Example Z_mod_plus: forall a b c : Z, c > 0 -> (a + b * c) mod c = a mod c. +Proof. + intros a b c. + pose proof (Z_eq_dec_or ((a+b*c)/c) (a/c+b)). + nia. +Qed. +Example Z_mod_opp_r_z: forall a b : Z, b <> 0 -> a mod b = 0 -> a mod - b = 0. +Proof. + intros a b. + pose proof (Z_eq_dec_or (a/b) (-(a/-b))). + nia. +Qed. +Example Zmod_eq: forall a b : Z, b > 0 -> a mod b = a - a / b * b. Proof. intros; nia. Qed. +Example Z_div_exact_2: forall a b : Z, b > 0 -> a mod b = 0 -> a = b * (a / b). Proof. intros; nia. Qed. +Example Z_div_mod_eq: forall a b : Z, b > 0 -> a = b * (a / b) + a mod b. Proof. intros; nia. Qed. +Example Z_div_exact_1: forall a b : Z, b > 0 -> a = b * (a / b) -> a mod b = 0. Proof. intros; nia. Qed. +Example Z_mod_add: forall a b c : Z, c <> 0 -> (a + b * c) mod c = a mod c. +Proof. + intros a b c. + pose proof (Z_eq_dec_or ((a+b*c)/c) (a/c+b)). + nia. +Qed. +Example Z_mod_nz_opp_r: forall a b : Z, a mod b <> 0 -> a mod - b = a mod b - b. +Proof. + intros a b. + assert (a mod b <> 0 -> a / -b = -(a/b)-1) by t. + nia. +Qed. +Example Z_mul_mod_idemp_l: forall a b n : Z, n <> 0 -> (a mod n * b) mod n = (a * b) mod n. +Proof. + intros a b n ?. + assert (((a mod n) * b) / n = (b / n) * (a mod n) + ((b mod n) * (a mod n)) / n) + by nia. + assert ((a * b) / n = (b / n) * (a / n) * n + (b / n) * (a mod n) + (b mod n) * (a / n) + ((b mod n) * (a mod n)) / n) + by nia. + nia. +Qed. +Example Z_mod_nz_opp_full: forall a b : Z, a mod b <> 0 -> - a mod b = b - a mod b. +Proof. + intros a b. + assert (a mod b <> 0 -> -a/b = -1-a/b) by nia. + nia. +Qed. +Example Z_add_mod_idemp_r: forall a b n : Z, n <> 0 -> (a + b mod n) mod n = (a + b) mod n. +Proof. + intros a b n ?. + assert ((a + b mod n) / n = (a / n) + (a mod n + b mod n) / n) by nia. + assert ((a + b) / n = (a / n) + (b / n) + (a mod n + b mod n) / n) by nia. + nia. +Qed. +Example Z_add_mod_idemp_l: forall a b n : Z, n <> 0 -> (a mod n + b) mod n = (a + b) mod n. +Proof. + intros a b n ?. + assert ((a mod n + b) / n = (b / n) + (a mod n + b mod n) / n) by nia. + assert ((a + b) / n = (a / n) + (b / n) + (a mod n + b mod n) / n) by nia. + nia. +Qed. +Example Z_mul_mod_idemp_r: forall a b n : Z, n <> 0 -> (a * (b mod n)) mod n = (a * b) mod n. +Proof. + intros a b n ?. + assert ((a * (b mod n)) / n = (a / n) * (b mod n) + ((a mod n) * (b mod n)) / n) + by nia. + assert ((a * b) / n = (b / n) * (a / n) * n + (b / n) * (a mod n) + (b mod n) * (a / n) + ((a mod n) * (b mod n)) / n) + by nia. + nia. +Qed. +Example Zmod_eq_full: forall a b : Z, b <> 0 -> a mod b = a - a / b * b. Proof. intros; nia. Qed. +Example div_eq: forall x y : Z, y <> 0 -> x mod y = 0 -> x / y * y = x. Proof. intros; nia. Qed. +Example Z_mod_eq: forall a b : Z, b <> 0 -> a mod b = a - b * (a / b). Proof. intros; nia. Qed. +Example Z_mod_sign_nz: forall a b : Z, b <> 0 -> a mod b <> 0 -> Z.sgn (a mod b) = Z.sgn b. Proof. intros; nia. Qed. +Example Z_div_exact_full_2: forall a b : Z, b <> 0 -> a mod b = 0 -> a = b * (a / b). Proof. intros; nia. Qed. +Example Z_div_mod: forall a b : Z, b <> 0 -> a = b * (a / b) + a mod b. Proof. intros; nia. Qed. +Example Z_add_mod: forall a b n : Z, n <> 0 -> (a + b) mod n = (a mod n + b mod n) mod n. +Proof. + intros a b n ?. + assert ((a + b) / n = (a / n) + (b / n) + (a mod n + b mod n) / n) by nia. + nia. +Qed. +Example Z_mul_mod: forall a b n : Z, n <> 0 -> (a * b) mod n = (a mod n * (b mod n)) mod n. +Proof. + intros a b n ?. + assert ((a * b) / n = (b / n) * (a / n) * n + (b / n) * (a mod n) + (b mod n) * (a / n) + ((a mod n) * (b mod n)) / n) + by nia. + nia. +Qed. +Example Z_div_exact: forall a b : Z, b <> 0 -> a = b * (a / b) <-> a mod b = 0. Proof. intros; nia. Qed. +Example Z_div_opp_l_z: forall a b : Z, b <> 0 -> a mod b = 0 -> - a / b = - (a / b). Proof. intros; nia. Qed. +Example Z_div_opp_r_z: forall a b : Z, b <> 0 -> a mod b = 0 -> a / - b = - (a / b). Proof. intros; nia. Qed. +Example Z_mod_opp_r_nz: forall a b : Z, b <> 0 -> a mod b <> 0 -> a mod - b = a mod b - b. +Proof. + intros a b. + assert (a mod b <> 0 -> a/(-b) = -1-a/b) by nia. + nia. +Qed. +Example Z_mul_mod_distr_r: forall a b c : Z, b <> 0 -> c <> 0 -> (a * c) mod (b * c) = a mod b * c. +Proof. + intros a b c. + pose proof (Z_eq_dec_or ((a*c)/(b*c)) (a/b)). + nia. +Qed. +Example Z_mul_mod_distr_l: forall a b c : Z, b <> 0 -> c <> 0 -> (c * a) mod (c * b) = c * (a mod b). +Proof. + intros a b c. + pose proof (Z_eq_dec_or ((c*a)/(c*b)) (a/b)). + nia. +Qed. +Example Z_mod_opp_l_nz: forall a b : Z, b <> 0 -> a mod b <> 0 -> - a mod b = b - a mod b. +Proof. + intros a b. + assert (a mod b <> 0 -> -a/b = -1-a/b) by nia. + nia. +Qed. +Example mod_eq: forall x x' y : Z, x / y = x' / y -> x mod y = x' mod y -> y <> 0 -> x = x'. Proof. intros; nia. Qed. +Example Z_div_nz_opp_r: forall a b : Z, a mod b <> 0 -> a / - b = - (a / b) - 1. Proof. intros; nia. Qed. +Example Z_div_nz_opp_full: forall a b : Z, a mod b <> 0 -> - a / b = - (a / b) - 1. Proof. intros; nia. Qed. +Example Zmod_unique: forall a b q r : Z, 0 <= r < b -> a = b * q + r -> r = a mod b. +Proof. + intros a b q r ??. + assert (q = a / b) by nia. + nia. +Qed. +Example Z_mod_unique_neg: forall a b q r : Z, b < r <= 0 -> a = b * q + r -> r = a mod b. +Proof. + intros a b q r ??. + assert (q = a / b) by nia. + nia. +Qed. +Example Z_mod_unique_pos: forall a b q r : Z, 0 <= r < b -> a = b * q + r -> r = a mod b. +Proof. + intros a b q r ??. + assert (q = a / b) by nia. + nia. +Qed. +Example Z_rem_mul_r: forall a b c : Z, b <> 0 -> 0 < c -> a mod (b * c) = a mod b + b * ((a / b) mod c). +Proof. + intros a b c ??. + assert (a / (b * c) = ((a / b) / c)) by nia. + nia. +Qed. +Example Z_mod_bound_or: forall a b : Z, b <> 0 -> 0 <= a mod b < b \/ b < a mod b <= 0. Proof. intros; nia. Qed. +Example Z_div_opp_l_nz: forall a b : Z, b <> 0 -> a mod b <> 0 -> - a / b = - (a / b) - 1. Proof. intros; nia. Qed. +Example Z_div_opp_r_nz: forall a b : Z, b <> 0 -> a mod b <> 0 -> a / - b = - (a / b) - 1. Proof. intros; nia. Qed. +Example Z_mod_small_iff: forall a b : Z, b <> 0 -> a mod b = a <-> 0 <= a < b \/ b < a <= 0. Proof. t. Qed. +Example Z_mod_unique: forall a b q r : Z, 0 <= r < b \/ b < r <= 0 -> a = b * q + r -> r = a mod b. +Proof. + intros a b q r ??. + assert (q = a/b) by nia. + nia. +Qed. +Example Z_opp_mod_bound_or: forall a b : Z, b <> 0 -> 0 <= - (a mod b) < - b \/ - b < - (a mod b) <= 0. Proof. intros; nia. Qed. + +Example Zdiv_0_r: forall a : Z, a / 0 = 0. Proof. intros; nia. Qed. +Example Zdiv_0_l: forall a : Z, 0 / a = 0. Proof. intros; nia. Qed. +Example Z_div_1_r: forall a : Z, a / 1 = a. Proof. intros; nia. Qed. +Example Zdiv_1_r: forall a : Z, a / 1 = a. Proof. intros; nia. Qed. +Example Zdiv_opp_opp: forall a b : Z, - a / - b = a / b. Proof. intros; nia. Qed. +Example Z_div_0_l: forall a : Z, a <> 0 -> 0 / a = 0. Proof. intros; nia. Qed. +Example Z_div_pos: forall a b : Z, b > 0 -> 0 <= a -> 0 <= a / b. Proof. intros; nia. Qed. +Example Z_div_ge0: forall a b : Z, b > 0 -> a >= 0 -> a / b >= 0. Proof. intros; nia. Qed. +Example Z_div_pos': forall a b : Z, 0 <= a -> 0 < b -> 0 <= a / b. Proof. intros; nia. Qed. +Example Z_mult_div_ge: forall a b : Z, b > 0 -> b * (a / b) <= a. Proof. intros; nia. Qed. +Example Z_mult_div_ge_neg: forall a b : Z, b < 0 -> b * (a / b) >= a. Proof. intros; nia. Qed. +Example Z_mul_div_le: forall a b : Z, 0 < b -> b * (a / b) <= a. Proof. intros; nia. Qed. +Example Z_mul_div_ge: forall a b : Z, b < 0 -> a <= b * (a / b). Proof. intros; nia. Qed. +Example Z_div_same: forall a : Z, a > 0 -> a / a = 1. Proof. intros; nia. Qed. +Example Z_div_mult: forall a b : Z, b > 0 -> a * b / b = a. Proof. intros; nia. Qed. +Example Z_mul_succ_div_gt: forall a b : Z, 0 < b -> a < b * Z.succ (a / b). Proof. intros; nia. Qed. +Example Z_mul_succ_div_lt: forall a b : Z, b < 0 -> b * Z.succ (a / b) < a. Proof. intros; nia. Qed. +Example Zdiv_1_l: forall a : Z, 1 < a -> 1 / a = 0. Proof. intros; nia. Qed. +Example Z_div_1_l: forall a : Z, 1 < a -> 1 / a = 0. Proof. intros; nia. Qed. +Example Z_div_str_pos: forall a b : Z, 0 < b <= a -> 0 < a / b. Proof. intros; nia. Qed. +Example Z_div_ge: forall a b c : Z, c > 0 -> a >= b -> a / c >= b / c. Proof. intros; nia. Qed. +Example Z_div_mult_full: forall a b : Z, b <> 0 -> a * b / b = a. Proof. intros; nia. Qed. +Example Z_div_same': forall a : Z, a <> 0 -> a / a = 1. Proof. intros; nia. Qed. +Example Zdiv_lt_upper_bound: forall a b q : Z, 0 < b -> a < q * b -> a / b < q. Proof. intros; nia. Qed. +Example Z_div_mul: forall a b : Z, b <> 0 -> a * b / b = a. Proof. intros; nia. Qed. +Example Z_div_lt: forall a b : Z, 0 < a -> 1 < b -> a / b < a. Proof. intros; nia. Qed. +Example Z_div_le_mono: forall a b c : Z, 0 < c -> a <= b -> a / c <= b / c. Proof. intros; nia. Qed. +Example Zdiv_sgn: forall a b : Z, 0 <= Z.sgn (a / b) * Z.sgn a * Z.sgn b. Proof. intros; nia. Qed. +Example Z_div_same_full: forall a : Z, a <> 0 -> a / a = 1. Proof. intros; nia. Qed. +Example Z_div_lt_upper_bound: forall a b q : Z, 0 < b -> a < b * q -> a / b < q. Proof. intros; nia. Qed. +Example Z_div_le: forall a b c : Z, c > 0 -> a <= b -> a / c <= b / c. Proof. intros; nia. Qed. +Example Z_div_le_lower_bound: forall a b q : Z, 0 < b -> b * q <= a -> q <= a / b. Proof. intros; nia. Qed. +Example Zdiv_le_lower_bound: forall a b q : Z, 0 < b -> q * b <= a -> q <= a / b. Proof. intros; nia. Qed. +Example Zdiv_le_upper_bound: forall a b q : Z, 0 < b -> a <= q * b -> a / b <= q. Proof. intros; nia. Qed. +Example Z_div_le_upper_bound: forall a b q : Z, 0 < b -> a <= b * q -> a / b <= q. Proof. intros; nia. Qed. +Example Z_div_small: forall a b : Z, 0 <= a < b -> a / b = 0. Proof. intros; nia. Qed. +Example Zdiv_small: forall a b : Z, 0 <= a < b -> a / b = 0. Proof. intros; nia. Qed. +Example Z_div_opp_opp: forall a b : Z, b <> 0 -> - a / - b = a / b. Proof. intros; nia. Qed. +Example Zdiv_mult_cancel_r: forall a b c : Z, c <> 0 -> a * c / (b * c) = a / b. Proof. intros; nia. Qed. +Example Z_div_unique_exact: forall a b q : Z, b <> 0 -> a = b * q -> q = a / b. Proof. intros; nia. Qed. +Example Zdiv_mult_cancel_l: forall a b c : Z, c <> 0 -> c * a / (c * b) = a / b. Proof. intros; nia. Qed. +Example Zdiv_le_compat_l: forall p q r : Z, 0 <= p -> 0 < q < r -> p / r <= p / q. +Proof. + intros p q r ??. + assert (p mod r <= p mod q \/ p mod q <= p mod r) by nia. + assert (0 <= p / r) by nia. + assert (0 <= p / q) by nia. + nia. +Qed. +Example Z_div_le_compat_l: forall p q r : Z, 0 <= p -> 0 < q <= r -> p / r <= p / q. +Proof. + intros p q r ??. + assert (p mod r <= p mod q \/ p mod q <= p mod r) by nia. + assert (0 <= p / r) by nia. + assert (0 <= p / q) by nia. + nia. +Qed. +Example Zdiv_Zdiv: forall a b c : Z, 0 <= b -> 0 <= c -> a / b / c = a / (b * c). Proof. intros; nia. Qed. +Example Z_div_plus: forall a b c : Z, c > 0 -> (a + b * c) / c = a / c + b. Proof. intros; nia. Qed. +Example Z_div_lt': forall a b : Z, b >= 2 -> a > 0 -> a / b < a. Proof. intros; nia. Qed. +Example Zdiv_mult_le: forall a b c : Z, 0 <= a -> 0 <= b -> 0 <= c -> c * (a / b) <= c * a / b. Proof. intros; nia. Qed. +Example Z_div_add_l: forall a b c : Z, b <> 0 -> (a * b + c) / b = a + c / b. Proof. intros; nia. Qed. +Example Z_div_plus_full_l: forall a b c : Z, b <> 0 -> (a * b + c) / b = a + c / b. Proof. intros; nia. Qed. +Example Z_div_add: forall a b c : Z, c <> 0 -> (a + b * c) / c = a / c + b. Proof. intros; nia. Qed. +Example Z_div_plus_full: forall a b c : Z, c <> 0 -> (a + b * c) / c = a / c + b. Proof. intros; nia. Qed. +Example Z_div_mul_le: forall a b c : Z, 0 <= a -> 0 < b -> 0 <= c -> c * (a / b) <= c * a / b. Proof. intros; nia. Qed. +Example Z_div_mul_cancel_r: forall a b c : Z, b <> 0 -> c <> 0 -> a * c / (b * c) = a / b. Proof. intros; nia. Qed. +Example Z_div_div: forall a b c : Z, b <> 0 -> 0 < c -> a / b / c = a / (b * c). Proof. intros; nia. Qed. +Example Z_div_mul_cancel_l: forall a b c : Z, b <> 0 -> c <> 0 -> c * a / (c * b) = a / b. Proof. intros; nia. Qed. +Example Z_div_unique_neg: forall a b q r : Z, b < r <= 0 -> a = b * q + r -> q = a / b. Proof. intros; nia. Qed. +Example Zdiv_unique: forall a b q r : Z, 0 <= r < b -> a = b * q + r -> q = a / b. Proof. intros; nia. Qed. +Example Z_div_unique_pos: forall a b q r : Z, 0 <= r < b -> a = b * q + r -> q = a / b. Proof. intros; nia. Qed. +Example Z_div_small_iff: forall a b : Z, b <> 0 -> a / b = 0 <-> 0 <= a < b \/ b < a <= 0. Proof. intros; nia. Qed. +Example Z_div_unique: forall a b q r : Z, 0 <= r < b \/ b < r <= 0 -> a = b * q + r -> q = a / b. Proof. intros; nia. Qed. + +(** Now we do the same, but with [Z.quot] and [Z.rem] instead. *) +Lemma N2Z_inj_quot : forall n m : N, Z.of_N (n / m) = Z.of_N n ÷ Z.of_N m. Proof. intros; nia. Qed. +Lemma N2Z_inj_rem : forall n m : N, Z.of_N (n mod m) = Z.rem (Z.of_N n) (Z.of_N m). Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_DT_mul_quot_ge : forall a b : Z, a <= 0 -> b <> 0 -> a <= b * (a ÷ b) <= 0. +Proof. intros; destruct (Z_zerop (a ÷ b)); nia. Qed. +Lemma OrdersEx_Z_as_DT_mul_quot_le : forall a b : Z, 0 <= a -> b <> 0 -> 0 <= b * (a ÷ b) <= a. Proof. intros; destruct (Z_zerop (a ÷ b)); nia. Qed. +Lemma OrdersEx_Z_as_DT_Private_Div_NZQuot_div_0_l : forall a : Z, 0 < a -> 0 ÷ a = 0. Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_DT_Private_Div_NZQuot_div_1_l : forall a : Z, 1 < a -> 1 ÷ a = 0. Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_DT_Private_Div_NZQuot_div_1_r : forall a : Z, 0 <= a -> a ÷ 1 = a. Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_DT_Private_Div_NZQuot_div_add : forall a b c : Z, 0 <= a -> 0 <= a + b * c -> 0 < c -> (a + b * c) ÷ c = a ÷ c + b. Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_DT_Private_Div_NZQuot_div_add_l : forall a b c : Z, 0 <= c -> 0 <= a * b + c -> 0 < b -> (a * b + c) ÷ b = a + c ÷ b. Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_DT_Private_Div_NZQuot_div_div : forall a b c : Z, 0 <= a -> 0 < b -> 0 < c -> a ÷ b ÷ c = a ÷ (b * c). +Proof. intros; assert (0 < b * c) by nia; nia. Qed. +Lemma OrdersEx_Z_as_DT_Private_Div_NZQuot_div_le_compat_l : forall p q r : Z, 0 <= p -> 0 < q <= r -> p ÷ r <= p ÷ q. +Proof. + intros. + destruct (Z_zerop p), (Z_zerop (p ÷ r)), (Z_zerop (p ÷ q)); subst; [ nia.. | ]. + assert (0 < q) by nia; assert (0 < r) by nia; assert (0 < p) by nia. + nia. +Qed. +Lemma OrdersEx_Z_as_DT_Private_Div_NZQuot_div_le_lower_bound : forall a b q : Z, 0 <= a -> 0 < b -> b * q <= a -> q <= a ÷ b. Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_DT_Private_Div_NZQuot_div_le_mono : forall a b c : Z, 0 < c -> 0 <= a <= b -> a ÷ c <= b ÷ c. Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_DT_Private_Div_NZQuot_div_le_upper_bound : forall a b q : Z, 0 <= a -> 0 < b -> a <= b * q -> a ÷ b <= q. Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_DT_Private_Div_NZQuot_div_lt : forall a b : Z, 0 < a -> 1 < b -> a ÷ b < a. Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_DT_Private_Div_NZQuot_div_lt_upper_bound : forall a b q : Z, 0 <= a -> 0 < b -> a < b * q -> a ÷ b < q. Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_DT_Private_Div_NZQuot_div_mul_cancel_l : forall a b c : Z, 0 <= a -> 0 < b -> 0 < c -> c * a ÷ (c * b) = a ÷ b. Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_DT_Private_Div_NZQuot_div_mul_cancel_r : forall a b c : Z, 0 <= a -> 0 < b -> 0 < c -> a * c ÷ (b * c) = a ÷ b. Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_DT_Private_Div_NZQuot_div_mul : forall a b : Z, 0 <= a -> 0 < b -> a * b ÷ b = a. Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_DT_Private_Div_NZQuot_div_mul_le : forall a b c : Z, 0 <= a -> 0 < b -> 0 <= c -> c * (a ÷ b) <= c * a ÷ b. Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_DT_Private_Div_NZQuot_div_pos : forall a b : Z, 0 <= a -> 0 < b -> 0 <= a ÷ b. Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_DT_Private_Div_NZQuot_div_same : forall a : Z, 0 < a -> a ÷ a = 1. Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_DT_Private_Div_NZQuot_div_small : forall a b : Z, 0 <= a < b -> a ÷ b = 0. Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_DT_Private_Div_NZQuot_div_small_iff : forall a b : Z, 0 <= a -> 0 < b -> a ÷ b = 0 <-> a < b. Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_DT_Private_Div_NZQuot_div_str_pos : forall a b : Z, 0 < b <= a -> 0 < a ÷ b. Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_DT_Private_Div_NZQuot_div_str_pos_iff : forall a b : Z, 0 <= a -> 0 < b -> 0 < a ÷ b <-> b <= a. Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_DT_Private_Div_NZQuot_div_unique_exact : forall a b q : Z, 0 <= a -> 0 < b -> a = b * q -> q = a ÷ b. Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_DT_Private_Div_NZQuot_div_unique : forall a b q r : Z, 0 <= a -> 0 <= r < b -> a = b * q + r -> q = a ÷ b. Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_DT_Private_Div_NZQuot_mul_div_le : forall a b : Z, 0 <= a -> 0 < b -> b * (a ÷ b) <= a. Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_DT_quot_0_l : forall a : Z, a <> 0 -> 0 ÷ a = 0. Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_DT_quot_1_l : forall a : Z, 1 < a -> 1 ÷ a = 0. Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_DT_quot_1_r : forall a : Z, a ÷ 1 = a. Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_DT_quot_add : forall a b c : Z, c <> 0 -> 0 <= (a + b * c) * a -> (a + b * c) ÷ c = a ÷ c + b. Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_DT_quot_add_l : forall a b c : Z, b <> 0 -> 0 <= (a * b + c) * c -> (a * b + c) ÷ b = a + c ÷ b. Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_DT_quot_div_nonneg : forall a b : Z, 0 <= a -> 0 < b -> a ÷ b = a / b. Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_DT_quot_le_compat_l : forall p q r : Z, 0 <= p -> 0 < q <= r -> p ÷ r <= p ÷ q. +Proof. + intros. + destruct (Z_zerop p), (Z_zerop (p ÷ r)), (Z_zerop (p ÷ q)); [ subst; nia.. | ]. + assert (0 < p) by nia; assert (0 < r) by nia. + nia. +Qed. +Lemma OrdersEx_Z_as_DT_quot_le_lower_bound : forall a b q : Z, 0 < b -> b * q <= a -> q <= a ÷ b. Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_DT_quot_le_mono : forall a b c : Z, 0 < c -> a <= b -> a ÷ c <= b ÷ c. +Proof. + intros. + destruct (Z_zerop a), (Z_zerop b), (Z_zerop (a ÷ c)), (Z_zerop (b ÷ c)); [ subst; nia.. | ]. + nia. +Qed. +Lemma OrdersEx_Z_as_DT_quot_le_upper_bound : forall a b q : Z, 0 < b -> a <= b * q -> a ÷ b <= q. Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_DT_quot_lt : forall a b : Z, 0 < a -> 1 < b -> a ÷ b < a. Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_DT_quot_lt_upper_bound : forall a b q : Z, 0 <= a -> 0 < b -> a < b * q -> a ÷ b < q. Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_DT_quot_mul_cancel_l : forall a b c : Z, b <> 0 -> c <> 0 -> c * a ÷ (c * b) = a ÷ b. +Proof. + intros. + assert (c * b <> 0) by nia. + destruct (Z_zerop a), (Z_zerop (c * a)); subst; [ nia | exfalso; nia.. | ]. +Abort. +Lemma OrdersEx_Z_as_DT_quot_mul_cancel_r : forall a b c : Z, b <> 0 -> c <> 0 -> a * c ÷ (b * c) = a ÷ b. Proof. Abort. +Lemma OrdersEx_Z_as_DT_quot_mul : forall a b : Z, b <> 0 -> a * b ÷ b = a. Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_DT_quot_mul_le : forall a b c : Z, 0 <= a -> 0 < b -> 0 <= c -> c * (a ÷ b) <= c * a ÷ b. Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_DT_quot_opp_l : forall a b : Z, b <> 0 -> - a ÷ b = - (a ÷ b). Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_DT_quot_opp_opp : forall a b : Z, b <> 0 -> - a ÷ - b = a ÷ b. Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_DT_quot_opp_r : forall a b : Z, b <> 0 -> a ÷ - b = - (a ÷ b). Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_DT_quot_pos : forall a b : Z, 0 <= a -> 0 < b -> 0 <= a ÷ b. Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_DT_quot_quot : forall a b c : Z, b <> 0 -> c <> 0 -> a ÷ b ÷ c = a ÷ (b * c). Proof. intros; assert (b * c <> 0) by nia. Abort. +Lemma OrdersEx_Z_as_DT_quot_same : forall a : Z, a <> 0 -> a ÷ a = 1. Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_DT_quot_small : forall a b : Z, 0 <= a < b -> a ÷ b = 0. Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_DT_quot_str_pos : forall a b : Z, 0 < b <= a -> 0 < a ÷ b. Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_DT_quot_unique_exact : forall a b q : Z, b <> 0 -> a = b * q -> q = a ÷ b. Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_DT_quot_unique : forall a b q r : Z, 0 <= a -> 0 <= r < b -> a = b * q + r -> q = a ÷ b. Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_OT_mul_quot_ge : forall a b : Z, a <= 0 -> b <> 0 -> a <= b * (a ÷ b) <= 0. Proof. intros. Fail nia. Abort. +Lemma OrdersEx_Z_as_OT_mul_quot_le : forall a b : Z, 0 <= a -> b <> 0 -> 0 <= b * (a ÷ b) <= a. Proof. intros. Fail nia. Abort. +Lemma OrdersEx_Z_as_OT_Private_Div_NZQuot_div_0_l : forall a : Z, 0 < a -> 0 ÷ a = 0. Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_OT_Private_Div_NZQuot_div_1_l : forall a : Z, 1 < a -> 1 ÷ a = 0. Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_OT_Private_Div_NZQuot_div_1_r : forall a : Z, 0 <= a -> a ÷ 1 = a. Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_OT_Private_Div_NZQuot_div_add : forall a b c : Z, 0 <= a -> 0 <= a + b * c -> 0 < c -> (a + b * c) ÷ c = a ÷ c + b. Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_OT_Private_Div_NZQuot_div_add_l : forall a b c : Z, 0 <= c -> 0 <= a * b + c -> 0 < b -> (a * b + c) ÷ b = a + c ÷ b. Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_OT_Private_Div_NZQuot_div_div : forall a b c : Z, 0 <= a -> 0 < b -> 0 < c -> a ÷ b ÷ c = a ÷ (b * c). Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_OT_Private_Div_NZQuot_div_le_compat_l : forall p q r : Z, 0 <= p -> 0 < q <= r -> p ÷ r <= p ÷ q. Proof. intros. Abort. +Lemma OrdersEx_Z_as_OT_Private_Div_NZQuot_div_le_lower_bound : forall a b q : Z, 0 <= a -> 0 < b -> b * q <= a -> q <= a ÷ b. Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_OT_Private_Div_NZQuot_div_le_mono : forall a b c : Z, 0 < c -> 0 <= a <= b -> a ÷ c <= b ÷ c. Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_OT_Private_Div_NZQuot_div_le_upper_bound : forall a b q : Z, 0 <= a -> 0 < b -> a <= b * q -> a ÷ b <= q. Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_OT_Private_Div_NZQuot_div_lt : forall a b : Z, 0 < a -> 1 < b -> a ÷ b < a. Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_OT_Private_Div_NZQuot_div_lt_upper_bound : forall a b q : Z, 0 <= a -> 0 < b -> a < b * q -> a ÷ b < q. Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_OT_Private_Div_NZQuot_div_mul_cancel_l : forall a b c : Z, 0 <= a -> 0 < b -> 0 < c -> c * a ÷ (c * b) = a ÷ b. Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_OT_Private_Div_NZQuot_div_mul_cancel_r : forall a b c : Z, 0 <= a -> 0 < b -> 0 < c -> a * c ÷ (b * c) = a ÷ b. Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_OT_Private_Div_NZQuot_div_mul : forall a b : Z, 0 <= a -> 0 < b -> a * b ÷ b = a. Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_OT_Private_Div_NZQuot_div_mul_le : forall a b c : Z, 0 <= a -> 0 < b -> 0 <= c -> c * (a ÷ b) <= c * a ÷ b. Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_OT_Private_Div_NZQuot_div_pos : forall a b : Z, 0 <= a -> 0 < b -> 0 <= a ÷ b. Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_OT_Private_Div_NZQuot_div_same : forall a : Z, 0 < a -> a ÷ a = 1. Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_OT_Private_Div_NZQuot_div_small : forall a b : Z, 0 <= a < b -> a ÷ b = 0. Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_OT_Private_Div_NZQuot_div_small_iff : forall a b : Z, 0 <= a -> 0 < b -> a ÷ b = 0 <-> a < b. Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_OT_Private_Div_NZQuot_div_str_pos : forall a b : Z, 0 < b <= a -> 0 < a ÷ b. Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_OT_Private_Div_NZQuot_div_str_pos_iff : forall a b : Z, 0 <= a -> 0 < b -> 0 < a ÷ b <-> b <= a. Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_OT_Private_Div_NZQuot_div_unique_exact : forall a b q : Z, 0 <= a -> 0 < b -> a = b * q -> q = a ÷ b. Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_OT_Private_Div_NZQuot_div_unique : forall a b q r : Z, 0 <= a -> 0 <= r < b -> a = b * q + r -> q = a ÷ b. Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_OT_Private_Div_NZQuot_mul_div_le : forall a b : Z, 0 <= a -> 0 < b -> b * (a ÷ b) <= a. Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_OT_quot_0_l : forall a : Z, a <> 0 -> 0 ÷ a = 0. Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_OT_quot_1_l : forall a : Z, 1 < a -> 1 ÷ a = 0. Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_OT_quot_1_r : forall a : Z, a ÷ 1 = a. Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_OT_quot_add : forall a b c : Z, c <> 0 -> 0 <= (a + b * c) * a -> (a + b * c) ÷ c = a ÷ c + b. Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_OT_quot_add_l : forall a b c : Z, b <> 0 -> 0 <= (a * b + c) * c -> (a * b + c) ÷ b = a + c ÷ b. Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_OT_quot_div_nonneg : forall a b : Z, 0 <= a -> 0 < b -> a ÷ b = a / b. Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_OT_quot_le_compat_l : forall p q r : Z, 0 <= p -> 0 < q <= r -> p ÷ r <= p ÷ q. Proof. intros. Fail nia. Abort. +Lemma OrdersEx_Z_as_OT_quot_le_lower_bound : forall a b q : Z, 0 < b -> b * q <= a -> q <= a ÷ b. Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_OT_quot_le_mono : forall a b c : Z, 0 < c -> a <= b -> a ÷ c <= b ÷ c. Proof. intros. Fail nia. Abort. +Lemma OrdersEx_Z_as_OT_quot_le_upper_bound : forall a b q : Z, 0 < b -> a <= b * q -> a ÷ b <= q. Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_OT_quot_lt : forall a b : Z, 0 < a -> 1 < b -> a ÷ b < a. Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_OT_quot_lt_upper_bound : forall a b q : Z, 0 <= a -> 0 < b -> a < b * q -> a ÷ b < q. Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_OT_quot_mul_cancel_l : forall a b c : Z, b <> 0 -> c <> 0 -> c * a ÷ (c * b) = a ÷ b. Proof. intros. Abort. +Lemma OrdersEx_Z_as_OT_quot_mul_cancel_r : forall a b c : Z, b <> 0 -> c <> 0 -> a * c ÷ (b * c) = a ÷ b. Proof. intros. Abort. +Lemma OrdersEx_Z_as_OT_quot_mul : forall a b : Z, b <> 0 -> a * b ÷ b = a. Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_OT_quot_mul_le : forall a b c : Z, 0 <= a -> 0 < b -> 0 <= c -> c * (a ÷ b) <= c * a ÷ b. Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_OT_quot_opp_l : forall a b : Z, b <> 0 -> - a ÷ b = - (a ÷ b). Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_OT_quot_opp_opp : forall a b : Z, b <> 0 -> - a ÷ - b = a ÷ b. Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_OT_quot_opp_r : forall a b : Z, b <> 0 -> a ÷ - b = - (a ÷ b). Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_OT_quot_pos : forall a b : Z, 0 <= a -> 0 < b -> 0 <= a ÷ b. Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_OT_quot_quot : forall a b c : Z, b <> 0 -> c <> 0 -> a ÷ b ÷ c = a ÷ (b * c). Proof. intros. Abort. +Lemma OrdersEx_Z_as_OT_quot_same : forall a : Z, a <> 0 -> a ÷ a = 1. Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_OT_quot_small : forall a b : Z, 0 <= a < b -> a ÷ b = 0. Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_OT_quot_str_pos : forall a b : Z, 0 < b <= a -> 0 < a ÷ b. Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_OT_quot_unique_exact : forall a b q : Z, b <> 0 -> a = b * q -> q = a ÷ b. Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_OT_quot_unique : forall a b q r : Z, 0 <= a -> 0 <= r < b -> a = b * q + r -> q = a ÷ b. Proof. intros; nia. Qed. +Lemma Z2N_inj_quot : forall n m : Z, 0 <= n -> 0 <= m -> Z.to_N (n ÷ m) = (Z.to_N n / Z.to_N m)%N. +Proof. intros; destruct (Z_zerop n), (Z_zerop m), (Z_zerop (n ÷ m)); [ subst; try nia.. | ]. Abort. +Lemma Z2N_inj_rem : forall n m : Z, 0 <= n -> 0 <= m -> Z.to_N (Z.rem n m) = (Z.to_N n mod Z.to_N m)%N. Proof. intros. Abort. +Lemma Zabs2N_inj_quot : forall n m : Z, Z.abs_N (n ÷ m) = (Z.abs_N n / Z.abs_N m)%N. Proof. intros. Abort. +Lemma Zabs2N_inj_rem : forall n m : Z, Z.abs_N (Z.rem n m) = (Z.abs_N n mod Z.abs_N m)%N. Proof. intros. Abort. +(* Some of these don't work, and I haven't gone through and figured out which ones yet, so they're all commented out for now *) +(* +Lemma Z_add_rem : forall a b n : Z, n <> 0 -> 0 <= a * b -> Z.rem (a + b) n = Z.rem (Z.rem a n + Z.rem b n) n. Proof. intros; nia. Qed. +Lemma Z_add_rem_idemp_l : forall a b n : Z, n <> 0 -> 0 <= a * b -> Z.rem (Z.rem a n + b) n = Z.rem (a + b) n. Proof. intros; nia. Qed. +Lemma Z_add_rem_idemp_r : forall a b n : Z, n <> 0 -> 0 <= a * b -> Z.rem (a + Z.rem b n) n = Z.rem (a + b) n. Proof. intros; nia. Qed. +Lemma ZBinary_Z_add_rem : forall a b n : Z, n <> 0 -> 0 <= a * b -> ZBinary.Z.rem (a + b) n = ZBinary.Z.rem (ZBinary.Z.rem a n + ZBinary.Z.rem b n) n. Proof. intros; nia. Qed. +Lemma ZBinary_Z_add_rem_idemp_l : forall a b n : Z, n <> 0 -> 0 <= a * b -> ZBinary.Z.rem (ZBinary.Z.rem a n + b) n = ZBinary.Z.rem (a + b) n. Proof. intros; nia. Qed. +Lemma ZBinary_Z_add_rem_idemp_r : forall a b n : Z, n <> 0 -> 0 <= a * b -> ZBinary.Z.rem (a + ZBinary.Z.rem b n) n = ZBinary.Z.rem (a + b) n. Proof. intros; nia. Qed. +Lemma ZBinary_Z_gcd_quot_gcd : forall a b g : Z, g <> 0 -> g = ZBinary.Z.gcd a b -> ZBinary.Z.gcd (a ÷ g) (b ÷ g) = 1. Proof. intros; nia. Qed. +Lemma ZBinary_Z_gcd_rem : forall a b : Z, b <> 0 -> ZBinary.Z.gcd (ZBinary.Z.rem a b) b = ZBinary.Z.gcd b a. Proof. intros; nia. Qed. +Lemma ZBinary_Z_mod_mul_r : forall a b c : Z, b <> 0 -> c <> 0 -> ZBinary.Z.rem a (b * c) = ZBinary.Z.rem a b + b * ZBinary.Z.rem (a ÷ b) c. Proof. intros; nia. Qed. +Lemma ZBinary_Z_mul_pred_quot_gt : forall a b : Z, 0 <= a -> b < 0 -> a < b * ZBinary.Z.pred (a ÷ b). Proof. intros; nia. Qed. +Lemma ZBinary_Z_mul_pred_quot_lt : forall a b : Z, a <= 0 -> 0 < b -> b * ZBinary.Z.pred (a ÷ b) < a. Proof. intros; nia. Qed. +Lemma ZBinary_Z_mul_quot_ge : forall a b : Z, a <= 0 -> b <> 0 -> a <= b * (a ÷ b) <= 0. Proof. intros; nia. Qed. +Lemma ZBinary_Z_mul_quot_le : forall a b : Z, 0 <= a -> b <> 0 -> 0 <= b * (a ÷ b) <= a. Proof. intros; nia. Qed. +Lemma ZBinary_Z_mul_rem_distr_l : forall a b c : Z, b <> 0 -> c <> 0 -> ZBinary.Z.rem (c * a) (c * b) = c * ZBinary.Z.rem a b. Proof. intros; nia. Qed. +Lemma ZBinary_Z_mul_rem_distr_r : forall a b c : Z, b <> 0 -> c <> 0 -> ZBinary.Z.rem (a * c) (b * c) = ZBinary.Z.rem a b * c. Proof. intros; nia. Qed. +Lemma ZBinary_Z_mul_rem : forall a b n : Z, n <> 0 -> ZBinary.Z.rem (a * b) n = ZBinary.Z.rem (ZBinary.Z.rem a n * ZBinary.Z.rem b n) n. Proof. intros; nia. Qed. +Lemma ZBinary_Z_mul_rem_idemp_l : forall a b n : Z, n <> 0 -> ZBinary.Z.rem (ZBinary.Z.rem a n * b) n = ZBinary.Z.rem (a * b) n. Proof. intros; nia. Qed. +Lemma ZBinary_Z_mul_rem_idemp_r : forall a b n : Z, n <> 0 -> ZBinary.Z.rem (a * ZBinary.Z.rem b n) n = ZBinary.Z.rem (a * b) n. Proof. intros; nia. Qed. +Lemma ZBinary_Z_mul_succ_quot_gt : forall a b : Z, 0 <= a -> 0 < b -> a < b * ZBinary.Z.succ (a ÷ b). Proof. intros; nia. Qed. +Lemma ZBinary_Z_mul_succ_quot_lt : forall a b : Z, a <= 0 -> b < 0 -> b * ZBinary.Z.succ (a ÷ b) < a. Proof. intros; nia. Qed. +Lemma ZBinary_Z_Private_Div_NZQuot_add_mod : forall a b n : Z, 0 <= a -> 0 <= b -> 0 < n -> ZBinary.Z.rem (a + b) n = ZBinary.Z.rem (ZBinary.Z.rem a n + ZBinary.Z.rem b n) n. Proof. intros; nia. Qed. +Lemma ZBinary_Z_Private_Div_NZQuot_add_mod_idemp_l : forall a b n : Z, 0 <= a -> 0 <= b -> 0 < n -> ZBinary.Z.rem (ZBinary.Z.rem a n + b) n = ZBinary.Z.rem (a + b) n. Proof. intros; nia. Qed. +Lemma ZBinary_Z_Private_Div_NZQuot_add_mod_idemp_r : forall a b n : Z, 0 <= a -> 0 <= b -> 0 < n -> ZBinary.Z.rem (a + ZBinary.Z.rem b n) n = ZBinary.Z.rem (a + b) n. Proof. intros; nia. Qed. +Lemma ZBinary_Z_Private_Div_NZQuot_div_0_l : forall a : Z, 0 < a -> 0 ÷ a = 0. Proof. intros; nia. Qed. +Lemma ZBinary_Z_Private_Div_NZQuot_div_1_l : forall a : Z, 1 < a -> 1 ÷ a = 0. Proof. intros; nia. Qed. +Lemma ZBinary_Z_Private_Div_NZQuot_div_1_r : forall a : Z, 0 <= a -> a ÷ 1 = a. Proof. intros; nia. Qed. +Lemma ZBinary_Z_Private_Div_NZQuot_div_add : forall a b c : Z, 0 <= a -> 0 <= a + b * c -> 0 < c -> (a + b * c) ÷ c = a ÷ c + b. Proof. intros; nia. Qed. +Lemma ZBinary_Z_Private_Div_NZQuot_div_add_l : forall a b c : Z, 0 <= c -> 0 <= a * b + c -> 0 < b -> (a * b + c) ÷ b = a + c ÷ b. Proof. intros; nia. Qed. +Lemma ZBinary_Z_Private_Div_NZQuot_div_div : forall a b c : Z, 0 <= a -> 0 < b -> 0 < c -> a ÷ b ÷ c = a ÷ (b * c). Proof. intros; nia. Qed. +Lemma ZBinary_Z_Private_Div_NZQuot_div_exact : forall a b : Z, 0 <= a -> 0 < b -> a = b * (a ÷ b) <-> ZBinary.Z.rem a b = 0. Proof. intros; nia. Qed. +Lemma ZBinary_Z_Private_Div_NZQuot_div_le_compat_l : forall p q r : Z, 0 <= p -> 0 < q <= r -> p ÷ r <= p ÷ q. Proof. intros; nia. Qed. +Lemma ZBinary_Z_Private_Div_NZQuot_div_le_lower_bound : forall a b q : Z, 0 <= a -> 0 < b -> b * q <= a -> q <= a ÷ b. Proof. intros; nia. Qed. +Lemma ZBinary_Z_Private_Div_NZQuot_div_le_mono : forall a b c : Z, 0 < c -> 0 <= a <= b -> a ÷ c <= b ÷ c. Proof. intros; nia. Qed. +Lemma ZBinary_Z_Private_Div_NZQuot_div_le_upper_bound : forall a b q : Z, 0 <= a -> 0 < b -> a <= b * q -> a ÷ b <= q. Proof. intros; nia. Qed. +Lemma ZBinary_Z_Private_Div_NZQuot_div_lt : forall a b : Z, 0 < a -> 1 < b -> a ÷ b < a. Proof. intros; nia. Qed. +Lemma ZBinary_Z_Private_Div_NZQuot_div_lt_upper_bound : forall a b q : Z, 0 <= a -> 0 < b -> a < b * q -> a ÷ b < q. Proof. intros; nia. Qed. +Lemma ZBinary_Z_Private_Div_NZQuot_div_mul_cancel_l : forall a b c : Z, 0 <= a -> 0 < b -> 0 < c -> c * a ÷ (c * b) = a ÷ b. Proof. intros; nia. Qed. +Lemma ZBinary_Z_Private_Div_NZQuot_div_mul_cancel_r : forall a b c : Z, 0 <= a -> 0 < b -> 0 < c -> a * c ÷ (b * c) = a ÷ b. Proof. intros; nia. Qed. +Lemma ZBinary_Z_Private_Div_NZQuot_div_mul : forall a b : Z, 0 <= a -> 0 < b -> a * b ÷ b = a. Proof. intros; nia. Qed. +Lemma ZBinary_Z_Private_Div_NZQuot_div_mul_le : forall a b c : Z, 0 <= a -> 0 < b -> 0 <= c -> c * (a ÷ b) <= c * a ÷ b. Proof. intros; nia. Qed. +Lemma ZBinary_Z_Private_Div_NZQuot_div_pos : forall a b : Z, 0 <= a -> 0 < b -> 0 <= a ÷ b. Proof. intros; nia. Qed. +Lemma ZBinary_Z_Private_Div_NZQuot_div_same : forall a : Z, 0 < a -> a ÷ a = 1. Proof. intros; nia. Qed. +Lemma ZBinary_Z_Private_Div_NZQuot_div_small : forall a b : Z, 0 <= a < b -> a ÷ b = 0. Proof. intros; nia. Qed. +Lemma ZBinary_Z_Private_Div_NZQuot_div_small_iff : forall a b : Z, 0 <= a -> 0 < b -> a ÷ b = 0 <-> a < b. Proof. intros; nia. Qed. +Lemma ZBinary_Z_Private_Div_NZQuot_div_str_pos : forall a b : Z, 0 < b <= a -> 0 < a ÷ b. Proof. intros; nia. Qed. +Lemma ZBinary_Z_Private_Div_NZQuot_div_str_pos_iff : forall a b : Z, 0 <= a -> 0 < b -> 0 < a ÷ b <-> b <= a. Proof. intros; nia. Qed. +Lemma ZBinary_Z_Private_Div_NZQuot_div_unique_exact : forall a b q : Z, 0 <= a -> 0 < b -> a = b * q -> q = a ÷ b. Proof. intros; nia. Qed. +Lemma ZBinary_Z_Private_Div_NZQuot_div_unique : forall a b q r : Z, 0 <= a -> 0 <= r < b -> a = b * q + r -> q = a ÷ b. Proof. intros; nia. Qed. +Lemma ZBinary_Z_Private_Div_NZQuot_mod_0_l : forall a : Z, 0 < a -> ZBinary.Z.rem 0 a = 0. Proof. intros; nia. Qed. +Lemma ZBinary_Z_Private_Div_NZQuot_mod_1_l : forall a : Z, 1 < a -> ZBinary.Z.rem 1 a = 1. Proof. intros; nia. Qed. +Lemma ZBinary_Z_Private_Div_NZQuot_mod_1_r : forall a : Z, 0 <= a -> ZBinary.Z.rem a 1 = 0. Proof. intros; nia. Qed. +Lemma ZBinary_Z_Private_Div_NZQuot_mod_add : forall a b c : Z, 0 <= a -> 0 <= a + b * c -> 0 < c -> ZBinary.Z.rem (a + b * c) c = ZBinary.Z.rem a c. Proof. intros; nia. Qed. +Lemma ZBinary_Z_Private_Div_NZQuot_mod_divides : forall a b : Z, 0 <= a -> 0 < b -> ZBinary.Z.rem a b = 0 <-> (exists c : Z, a = b * c). Proof. intros; nia. Qed. +Lemma ZBinary_Z_Private_Div_NZQuot_mod_le : forall a b : Z, 0 <= a -> 0 < b -> ZBinary.Z.rem a b <= a. Proof. intros; nia. Qed. +Lemma ZBinary_Z_Private_Div_NZQuot_mod_mod : forall a n : Z, 0 <= a -> 0 < n -> ZBinary.Z.rem (ZBinary.Z.rem a n) n = ZBinary.Z.rem a n. Proof. intros; nia. Qed. +Lemma ZBinary_Z_Private_Div_NZQuot_mod_mul : forall a b : Z, 0 <= a -> 0 < b -> ZBinary.Z.rem (a * b) b = 0. Proof. intros; nia. Qed. +Lemma ZBinary_Z_Private_Div_NZQuot_mod_mul_r : forall a b c : Z, 0 <= a -> 0 < b -> 0 < c -> ZBinary.Z.rem a (b * c) = ZBinary.Z.rem a b + b * ZBinary.Z.rem (a ÷ b) c. Proof. intros; nia. Qed. +Lemma ZBinary_Z_Private_Div_NZQuot_mod_same : forall a : Z, 0 < a -> ZBinary.Z.rem a a = 0. Proof. intros; nia. Qed. +Lemma ZBinary_Z_Private_Div_NZQuot_mod_small : forall a b : Z, 0 <= a < b -> ZBinary.Z.rem a b = a. Proof. intros; nia. Qed. +Lemma ZBinary_Z_Private_Div_NZQuot_mod_small_iff : forall a b : Z, 0 <= a -> 0 < b -> ZBinary.Z.rem a b = a <-> a < b. Proof. intros; nia. Qed. +Lemma ZBinary_Z_Private_Div_NZQuot_mod_unique : forall a b q r : Z, 0 <= a -> 0 <= r < b -> a = b * q + r -> r = ZBinary.Z.rem a b. Proof. intros; nia. Qed. +Lemma ZBinary_Z_Private_Div_NZQuot_mul_div_le : forall a b : Z, 0 <= a -> 0 < b -> b * (a ÷ b) <= a. Proof. intros; nia. Qed. +Lemma ZBinary_Z_Private_Div_NZQuot_mul_mod_distr_l : forall a b c : Z, 0 <= a -> 0 < b -> 0 < c -> ZBinary.Z.rem (c * a) (c * b) = c * ZBinary.Z.rem a b. Proof. intros; nia. Qed. +Lemma ZBinary_Z_Private_Div_NZQuot_mul_mod_distr_r : forall a b c : Z, 0 <= a -> 0 < b -> 0 < c -> ZBinary.Z.rem (a * c) (b * c) = ZBinary.Z.rem a b * c. Proof. intros; nia. Qed. +Lemma ZBinary_Z_Private_Div_NZQuot_mul_mod : forall a b n : Z, 0 <= a -> 0 <= b -> 0 < n -> ZBinary.Z.rem (a * b) n = ZBinary.Z.rem (ZBinary.Z.rem a n * ZBinary.Z.rem b n) n. Proof. intros; nia. Qed. +Lemma ZBinary_Z_Private_Div_NZQuot_mul_mod_idemp_l : forall a b n : Z, 0 <= a -> 0 <= b -> 0 < n -> ZBinary.Z.rem (ZBinary.Z.rem a n * b) n = ZBinary.Z.rem (a * b) n. Proof. intros; nia. Qed. +Lemma ZBinary_Z_Private_Div_NZQuot_mul_mod_idemp_r : forall a b n : Z, 0 <= a -> 0 <= b -> 0 < n -> ZBinary.Z.rem (a * ZBinary.Z.rem b n) n = ZBinary.Z.rem (a * b) n. Proof. intros; nia. Qed. +Lemma ZBinary_Z_Private_Div_NZQuot_mul_succ_div_gt : forall a b : Z, 0 <= a -> 0 < b -> a < b * ZBinary.Z.succ (a ÷ b). Proof. intros; nia. Qed. +Lemma ZBinary_Z_Private_Div_Quot2Div_div_mod : forall a b : Z, b <> 0 -> a = b * (a ÷ b) + ZBinary.Z.rem a b. Proof. intros; nia. Qed. +ZBinary_Z_Private_Div_Quot2Div_div_wd Morphisms.Proper (Morphisms.respectful eq (Morphisms.respectful eq eq)) ZBinary.Z.quot +Lemma ZBinary_Z_Private_Div_Quot2Div_mod_bound_pos : forall a b : Z, 0 <= a -> 0 < b -> 0 <= ZBinary.Z.rem a b < b. Proof. intros; nia. Qed. +ZBinary_Z_Private_Div_Quot2Div_mod_wd Morphisms.Proper (Morphisms.respectful eq (Morphisms.respectful eq eq)) ZBinary.Z.rem +Lemma ZBinary_Z_quot_0_l : forall a : Z, a <> 0 -> 0 ÷ a = 0. Proof. intros; nia. Qed. +Lemma ZBinary_Z_quot_1_l : forall a : Z, 1 < a -> 1 ÷ a = 0. Proof. intros; nia. Qed. +Lemma ZBinary_Z_quot_1_r : forall a : Z, a ÷ 1 = a. Proof. intros; nia. Qed. +Lemma ZBinary_Z_quot_abs : forall a b : Z, b <> 0 -> ZBinary.Z.abs a ÷ ZBinary.Z.abs b = ZBinary.Z.abs (a ÷ b). Proof. intros; nia. Qed. +Lemma ZBinary_Z_quot_abs_l : forall a b : Z, b <> 0 -> ZBinary.Z.abs a ÷ b = ZBinary.Z.sgn a * (a ÷ b). Proof. intros; nia. Qed. +Lemma ZBinary_Z_quot_abs_r : forall a b : Z, b <> 0 -> a ÷ ZBinary.Z.abs b = ZBinary.Z.sgn b * (a ÷ b). Proof. intros; nia. Qed. +Lemma ZBinary_Z_quot_add : forall a b c : Z, c <> 0 -> 0 <= (a + b * c) * a -> (a + b * c) ÷ c = a ÷ c + b. Proof. intros; nia. Qed. +Lemma ZBinary_Z_quot_add_l : forall a b c : Z, b <> 0 -> 0 <= (a * b + c) * c -> (a * b + c) ÷ b = a + c ÷ b. Proof. intros; nia. Qed. +Lemma ZBinary_Z_quot_div : forall a b : Z, b <> 0 -> a ÷ b = ZBinary.Z.sgn a * ZBinary.Z.sgn b * (ZBinary.Z.abs a / ZBinary.Z.abs b). Proof. intros; nia. Qed. +Lemma ZBinary_Z_quot_div_nonneg : forall a b : Z, 0 <= a -> 0 < b -> a ÷ b = a / b. Proof. intros; nia. Qed. +Lemma ZBinary_Z_quot_exact : forall a b : Z, b <> 0 -> a = b * (a ÷ b) <-> ZBinary.Z.rem a b = 0. Proof. intros; nia. Qed. +Lemma ZBinary_Z_quot_le_compat_l : forall p q r : Z, 0 <= p -> 0 < q <= r -> p ÷ r <= p ÷ q. Proof. intros; nia. Qed. +Lemma ZBinary_Z_quot_le_lower_bound : forall a b q : Z, 0 < b -> b * q <= a -> q <= a ÷ b. Proof. intros; nia. Qed. +Lemma ZBinary_Z_quot_le_mono : forall a b c : Z, 0 < c -> a <= b -> a ÷ c <= b ÷ c. Proof. intros; nia. Qed. +Lemma ZBinary_Z_quot_le_upper_bound : forall a b q : Z, 0 < b -> a <= b * q -> a ÷ b <= q. Proof. intros; nia. Qed. +Lemma ZBinary_Z_quot_lt : forall a b : Z, 0 < a -> 1 < b -> a ÷ b < a. Proof. intros; nia. Qed. +Lemma ZBinary_Z_quot_lt_upper_bound : forall a b q : Z, 0 <= a -> 0 < b -> a < b * q -> a ÷ b < q. Proof. intros; nia. Qed. +Lemma ZBinary_Z_quot_mul_cancel_l : forall a b c : Z, b <> 0 -> c <> 0 -> c * a ÷ (c * b) = a ÷ b. Proof. intros; nia. Qed. +Lemma ZBinary_Z_quot_mul_cancel_r : forall a b c : Z, b <> 0 -> c <> 0 -> a * c ÷ (b * c) = a ÷ b. Proof. intros; nia. Qed. +Lemma ZBinary_Z_quot_mul : forall a b : Z, b <> 0 -> a * b ÷ b = a. Proof. intros; nia. Qed. +Lemma ZBinary_Z_quot_mul_le : forall a b c : Z, 0 <= a -> 0 < b -> 0 <= c -> c * (a ÷ b) <= c * a ÷ b. Proof. intros; nia. Qed. +Lemma ZBinary_Z_quot_opp_l : forall a b : Z, b <> 0 -> - a ÷ b = - (a ÷ b). Proof. intros; nia. Qed. +Lemma ZBinary_Z_quot_opp_opp : forall a b : Z, b <> 0 -> - a ÷ - b = a ÷ b. Proof. intros; nia. Qed. +Lemma ZBinary_Z_quot_opp_r : forall a b : Z, b <> 0 -> a ÷ - b = - (a ÷ b). Proof. intros; nia. Qed. +Lemma ZBinary_Z_quot_pos : forall a b : Z, 0 <= a -> 0 < b -> 0 <= a ÷ b. Proof. intros; nia. Qed. +Lemma ZBinary_Z_quot_quot : forall a b c : Z, b <> 0 -> c <> 0 -> a ÷ b ÷ c = a ÷ (b * c). Proof. intros; nia. Qed. +Lemma ZBinary_Z_quot_rem' : forall a b : Z, a = b * (a ÷ b) + ZBinary.Z.rem a b. Proof. intros; nia. Qed. +Lemma ZBinary_Z_quot_rem : forall a b : Z, b <> 0 -> a = b * (a ÷ b) + ZBinary.Z.rem a b. Proof. intros; nia. Qed. +Lemma ZBinary_Z_quot_same : forall a : Z, a <> 0 -> a ÷ a = 1. Proof. intros; nia. Qed. +Lemma ZBinary_Z_quot_small : forall a b : Z, 0 <= a < b -> a ÷ b = 0. Proof. intros; nia. Qed. +Lemma ZBinary_Z_quot_small_iff : forall a b : Z, b <> 0 -> a ÷ b = 0 <-> ZBinary.Z.abs a < ZBinary.Z.abs b. Proof. intros; nia. Qed. +Lemma ZBinary_Z_quot_str_pos : forall a b : Z, 0 < b <= a -> 0 < a ÷ b. Proof. intros; nia. Qed. +Lemma ZBinary_Z_quot_unique_exact : forall a b q : Z, b <> 0 -> a = b * q -> q = a ÷ b. Proof. intros; nia. Qed. +Lemma ZBinary_Z_quot_unique : forall a b q r : Z, 0 <= a -> 0 <= r < b -> a = b * q + r -> q = a ÷ b. Proof. intros; nia. Qed. +ZBinary_Z_quot_wd Morphisms.Proper (Morphisms.respectful ZBinary.Z.eq (Morphisms.respectful ZBinary.Z.eq ZBinary.Z.eq)) ZBinary.Z.quot +Lemma ZBinary_Z_rem_0_l : forall a : Z, a <> 0 -> ZBinary.Z.rem 0 a = 0. Proof. intros; nia. Qed. +Lemma ZBinary_Z_rem_1_l : forall a : Z, 1 < a -> ZBinary.Z.rem 1 a = 1. Proof. intros; nia. Qed. +Lemma ZBinary_Z_rem_1_r : forall a : Z, ZBinary.Z.rem a 1 = 0. Proof. intros; nia. Qed. +Lemma ZBinary_Z_rem_abs : forall a b : Z, b <> 0 -> ZBinary.Z.rem (ZBinary.Z.abs a) (ZBinary.Z.abs b) = ZBinary.Z.abs (ZBinary.Z.rem a b). Proof. intros; nia. Qed. +Lemma ZBinary_Z_rem_abs_l : forall a b : Z, b <> 0 -> ZBinary.Z.rem (ZBinary.Z.abs a) b = ZBinary.Z.abs (ZBinary.Z.rem a b). Proof. intros; nia. Qed. +Lemma ZBinary_Z_rem_abs_r : forall a b : Z, b <> 0 -> ZBinary.Z.rem a (ZBinary.Z.abs b) = ZBinary.Z.rem a b. Proof. intros; nia. Qed. +Lemma ZBinary_Z_rem_add : forall a b c : Z, c <> 0 -> 0 <= (a + b * c) * a -> ZBinary.Z.rem (a + b * c) c = ZBinary.Z.rem a c. Proof. intros; nia. Qed. +Lemma ZBinary_Z_rem_bound_abs : forall a b : Z, b <> 0 -> ZBinary.Z.abs (ZBinary.Z.rem a b) < ZBinary.Z.abs b. Proof. intros; nia. Qed. +Lemma ZBinary_Z_rem_bound_pos : forall a b : Z, 0 <= a -> 0 < b -> 0 <= ZBinary.Z.rem a b < b. Proof. intros; nia. Qed. +Lemma ZBinary_Z_rem_eq : forall a b : Z, b <> 0 -> ZBinary.Z.rem a b = a - b * (a ÷ b). Proof. intros; nia. Qed. +Lemma ZBinary_Z_rem_le : forall a b : Z, 0 <= a -> 0 < b -> ZBinary.Z.rem a b <= a. Proof. intros; nia. Qed. +Lemma ZBinary_Z_rem_mod_eq_0 : forall a b : Z, b <> 0 -> ZBinary.Z.rem a b = 0 <-> a mod b = 0. Proof. intros; nia. Qed. +Lemma ZBinary_Z_rem_mod : forall a b : Z, b <> 0 -> ZBinary.Z.rem a b = ZBinary.Z.sgn a * (ZBinary.Z.abs a mod ZBinary.Z.abs b). Proof. intros; nia. Qed. +Lemma ZBinary_Z_rem_mod_nonneg : forall a b : Z, 0 <= a -> 0 < b -> ZBinary.Z.rem a b = a mod b. Proof. intros; nia. Qed. +Lemma ZBinary_Z_rem_mul : forall a b : Z, b <> 0 -> ZBinary.Z.rem (a * b) b = 0. Proof. intros; nia. Qed. +Lemma ZBinary_Z_rem_nonneg : forall a b : Z, b <> 0 -> 0 <= a -> 0 <= ZBinary.Z.rem a b. Proof. intros; nia. Qed. +Lemma ZBinary_Z_rem_nonpos : forall a b : Z, b <> 0 -> a <= 0 -> ZBinary.Z.rem a b <= 0. Proof. intros; nia. Qed. +Lemma ZBinary_Z_rem_opp_l : forall a b : Z, b <> 0 -> ZBinary.Z.rem (- a) b = - ZBinary.Z.rem a b. Proof. intros; nia. Qed. +Lemma ZBinary_Z_rem_opp_l' : forall a b : Z, ZBinary.Z.rem (- a) b = - ZBinary.Z.rem a b. Proof. intros; nia. Qed. +Lemma ZBinary_Z_rem_opp_opp : forall a b : Z, b <> 0 -> ZBinary.Z.rem (- a) (- b) = - ZBinary.Z.rem a b. Proof. intros; nia. Qed. +Lemma ZBinary_Z_rem_opp_r : forall a b : Z, b <> 0 -> ZBinary.Z.rem a (- b) = ZBinary.Z.rem a b. Proof. intros; nia. Qed. +Lemma ZBinary_Z_rem_opp_r' : forall a b : Z, ZBinary.Z.rem a (- b) = ZBinary.Z.rem a b. Proof. intros; nia. Qed. +Lemma ZBinary_Z_rem_quot : forall a b : Z, b <> 0 -> ZBinary.Z.rem a b ÷ b = 0. Proof. intros; nia. Qed. +Lemma ZBinary_Z_rem_rem : forall a n : Z, n <> 0 -> ZBinary.Z.rem (ZBinary.Z.rem a n) n = ZBinary.Z.rem a n. Proof. intros; nia. Qed. +Lemma ZBinary_Z_rem_same : forall a : Z, a <> 0 -> ZBinary.Z.rem a a = 0. Proof. intros; nia. Qed. +Lemma ZBinary_Z_rem_sign : forall a b : Z, a <> 0 -> b <> 0 -> ZBinary.Z.sgn (ZBinary.Z.rem a b) <> - ZBinary.Z.sgn a. Proof. intros; nia. Qed. +Lemma ZBinary_Z_rem_sign_mul : forall a b : Z, b <> 0 -> 0 <= ZBinary.Z.rem a b * a. Proof. intros; nia. Qed. +Lemma ZBinary_Z_rem_sign_nz : forall a b : Z, b <> 0 -> ZBinary.Z.rem a b <> 0 -> ZBinary.Z.sgn (ZBinary.Z.rem a b) = ZBinary.Z.sgn a. Proof. intros; nia. Qed. +Lemma ZBinary_Z_rem_small : forall a b : Z, 0 <= a < b -> ZBinary.Z.rem a b = a. Proof. intros; nia. Qed. +Lemma ZBinary_Z_rem_small_iff : forall a b : Z, b <> 0 -> ZBinary.Z.rem a b = a <-> ZBinary.Z.abs a < ZBinary.Z.abs b. Proof. intros; nia. Qed. +Lemma ZBinary_Z_rem_unique : forall a b q r : Z, 0 <= a -> 0 <= r < b -> a = b * q + r -> r = ZBinary.Z.rem a b. Proof. intros; nia. Qed. +ZBinary_Z_rem_wd Morphisms.Proper (Morphisms.respectful ZBinary.Z.eq (Morphisms.respectful ZBinary.Z.eq ZBinary.Z.eq)) ZBinary.Z.rem +Lemma Z_gcd_quot_gcd : forall a b g : Z, g <> 0 -> g = Z.gcd a b -> Z.gcd (a ÷ g) (b ÷ g) = 1. Proof. intros; nia. Qed. +Lemma Z_gcd_rem : forall a b : Z, b <> 0 -> Z.gcd (Z.rem a b) b = Z.gcd b a. Proof. intros; nia. Qed. +Lemma Z_mod_mul_r : forall a b c : Z, b <> 0 -> c <> 0 -> Z.rem a (b * c) = Z.rem a b + b * Z.rem (a ÷ b) c. Proof. intros; nia. Qed. +Lemma Z_mul_pred_quot_gt : forall a b : Z, 0 <= a -> b < 0 -> a < b * Z.pred (a ÷ b). Proof. intros; nia. Qed. +Lemma Z_mul_pred_quot_lt : forall a b : Z, a <= 0 -> 0 < b -> b * Z.pred (a ÷ b) < a. Proof. intros; nia. Qed. +Lemma Z_mul_quot_ge : forall a b : Z, a <= 0 -> b <> 0 -> a <= b * (a ÷ b) <= 0. Proof. intros; nia. Qed. +Lemma Z_mul_quot_le : forall a b : Z, 0 <= a -> b <> 0 -> 0 <= b * (a ÷ b) <= a. Proof. intros; nia. Qed. +Lemma Z_mul_rem_distr_l : forall a b c : Z, b <> 0 -> c <> 0 -> Z.rem (c * a) (c * b) = c * Z.rem a b. Proof. intros; nia. Qed. +Lemma Z_mul_rem_distr_r : forall a b c : Z, b <> 0 -> c <> 0 -> Z.rem (a * c) (b * c) = Z.rem a b * c. Proof. intros; nia. Qed. +Lemma Z_mul_rem : forall a b n : Z, n <> 0 -> Z.rem (a * b) n = Z.rem (Z.rem a n * Z.rem b n) n. Proof. intros; nia. Qed. +Lemma Z_mul_rem_idemp_l : forall a b n : Z, n <> 0 -> Z.rem (Z.rem a n * b) n = Z.rem (a * b) n. Proof. intros; nia. Qed. +Lemma Z_mul_rem_idemp_r : forall a b n : Z, n <> 0 -> Z.rem (a * Z.rem b n) n = Z.rem (a * b) n. Proof. intros; nia. Qed. +Lemma Z_mul_succ_quot_gt : forall a b : Z, 0 <= a -> 0 < b -> a < b * Z.succ (a ÷ b). Proof. intros; nia. Qed. +Lemma Z_mul_succ_quot_lt : forall a b : Z, a <= 0 -> b < 0 -> b * Z.succ (a ÷ b) < a. Proof. intros; nia. Qed. +Lemma Z_Private_Div_NZQuot_add_mod : forall a b n : Z, 0 <= a -> 0 <= b -> 0 < n -> Z.rem (a + b) n = Z.rem (Z.rem a n + Z.rem b n) n. Proof. intros; nia. Qed. +Lemma Z_Private_Div_NZQuot_add_mod_idemp_l : forall a b n : Z, 0 <= a -> 0 <= b -> 0 < n -> Z.rem (Z.rem a n + b) n = Z.rem (a + b) n. Proof. intros; nia. Qed. +Lemma Z_Private_Div_NZQuot_add_mod_idemp_r : forall a b n : Z, 0 <= a -> 0 <= b -> 0 < n -> Z.rem (a + Z.rem b n) n = Z.rem (a + b) n. Proof. intros; nia. Qed. +Lemma Z_Private_Div_NZQuot_div_0_l : forall a : Z, 0 < a -> 0 ÷ a = 0. Proof. intros; nia. Qed. +Lemma Z_Private_Div_NZQuot_div_1_l : forall a : Z, 1 < a -> 1 ÷ a = 0. Proof. intros; nia. Qed. +Lemma Z_Private_Div_NZQuot_div_1_r : forall a : Z, 0 <= a -> a ÷ 1 = a. Proof. intros; nia. Qed. +Lemma Z_Private_Div_NZQuot_div_add : forall a b c : Z, 0 <= a -> 0 <= a + b * c -> 0 < c -> (a + b * c) ÷ c = a ÷ c + b. Proof. intros; nia. Qed. +Lemma Z_Private_Div_NZQuot_div_add_l : forall a b c : Z, 0 <= c -> 0 <= a * b + c -> 0 < b -> (a * b + c) ÷ b = a + c ÷ b. Proof. intros; nia. Qed. +Lemma Z_Private_Div_NZQuot_div_div : forall a b c : Z, 0 <= a -> 0 < b -> 0 < c -> a ÷ b ÷ c = a ÷ (b * c). Proof. intros; nia. Qed. +Lemma Z_Private_Div_NZQuot_div_exact : forall a b : Z, 0 <= a -> 0 < b -> a = b * (a ÷ b) <-> Z.rem a b = 0. Proof. intros; nia. Qed. +Lemma Z_Private_Div_NZQuot_div_le_compat_l : forall p q r : Z, 0 <= p -> 0 < q <= r -> p ÷ r <= p ÷ q. Proof. intros; nia. Qed. +Lemma Z_Private_Div_NZQuot_div_le_lower_bound : forall a b q : Z, 0 <= a -> 0 < b -> b * q <= a -> q <= a ÷ b. Proof. intros; nia. Qed. +Lemma Z_Private_Div_NZQuot_div_le_mono : forall a b c : Z, 0 < c -> 0 <= a <= b -> a ÷ c <= b ÷ c. Proof. intros; nia. Qed. +Lemma Z_Private_Div_NZQuot_div_le_upper_bound : forall a b q : Z, 0 <= a -> 0 < b -> a <= b * q -> a ÷ b <= q. Proof. intros; nia. Qed. +Lemma Z_Private_Div_NZQuot_div_lt : forall a b : Z, 0 < a -> 1 < b -> a ÷ b < a. Proof. intros; nia. Qed. +Lemma Z_Private_Div_NZQuot_div_lt_upper_bound : forall a b q : Z, 0 <= a -> 0 < b -> a < b * q -> a ÷ b < q. Proof. intros; nia. Qed. +Lemma Z_Private_Div_NZQuot_div_mul_cancel_l : forall a b c : Z, 0 <= a -> 0 < b -> 0 < c -> c * a ÷ (c * b) = a ÷ b. Proof. intros; nia. Qed. +Lemma Z_Private_Div_NZQuot_div_mul_cancel_r : forall a b c : Z, 0 <= a -> 0 < b -> 0 < c -> a * c ÷ (b * c) = a ÷ b. Proof. intros; nia. Qed. +Lemma Z_Private_Div_NZQuot_div_mul : forall a b : Z, 0 <= a -> 0 < b -> a * b ÷ b = a. Proof. intros; nia. Qed. +Lemma Z_Private_Div_NZQuot_div_mul_le : forall a b c : Z, 0 <= a -> 0 < b -> 0 <= c -> c * (a ÷ b) <= c * a ÷ b. Proof. intros; nia. Qed. +Lemma Z_Private_Div_NZQuot_div_pos : forall a b : Z, 0 <= a -> 0 < b -> 0 <= a ÷ b. Proof. intros; nia. Qed. +Lemma Z_Private_Div_NZQuot_div_same : forall a : Z, 0 < a -> a ÷ a = 1. Proof. intros; nia. Qed. +Lemma Z_Private_Div_NZQuot_div_small : forall a b : Z, 0 <= a < b -> a ÷ b = 0. Proof. intros; nia. Qed. +Lemma Z_Private_Div_NZQuot_div_small_iff : forall a b : Z, 0 <= a -> 0 < b -> a ÷ b = 0 <-> a < b. Proof. intros; nia. Qed. +Lemma Z_Private_Div_NZQuot_div_str_pos : forall a b : Z, 0 < b <= a -> 0 < a ÷ b. Proof. intros; nia. Qed. +Lemma Z_Private_Div_NZQuot_div_str_pos_iff : forall a b : Z, 0 <= a -> 0 < b -> 0 < a ÷ b <-> b <= a. Proof. intros; nia. Qed. +Lemma Z_Private_Div_NZQuot_div_unique_exact : forall a b q : Z, 0 <= a -> 0 < b -> a = b * q -> q = a ÷ b. Proof. intros; nia. Qed. +Lemma Z_Private_Div_NZQuot_div_unique : forall a b q r : Z, 0 <= a -> 0 <= r < b -> a = b * q + r -> q = a ÷ b. Proof. intros; nia. Qed. +Lemma Z_Private_Div_NZQuot_mod_0_l : forall a : Z, 0 < a -> Z.rem 0 a = 0. Proof. intros; nia. Qed. +Lemma Z_Private_Div_NZQuot_mod_1_l : forall a : Z, 1 < a -> Z.rem 1 a = 1. Proof. intros; nia. Qed. +Lemma Z_Private_Div_NZQuot_mod_1_r : forall a : Z, 0 <= a -> Z.rem a 1 = 0. Proof. intros; nia. Qed. +Lemma Z_Private_Div_NZQuot_mod_add : forall a b c : Z, 0 <= a -> 0 <= a + b * c -> 0 < c -> Z.rem (a + b * c) c = Z.rem a c. Proof. intros; nia. Qed. +Lemma Z_Private_Div_NZQuot_mod_divides : forall a b : Z, 0 <= a -> 0 < b -> Z.rem a b = 0 <-> (exists c : Z, a = b * c). Proof. intros; nia. Qed. +Lemma Z_Private_Div_NZQuot_mod_le : forall a b : Z, 0 <= a -> 0 < b -> Z.rem a b <= a. Proof. intros; nia. Qed. +Lemma Z_Private_Div_NZQuot_mod_mod : forall a n : Z, 0 <= a -> 0 < n -> Z.rem (Z.rem a n) n = Z.rem a n. Proof. intros; nia. Qed. +Lemma Z_Private_Div_NZQuot_mod_mul : forall a b : Z, 0 <= a -> 0 < b -> Z.rem (a * b) b = 0. Proof. intros; nia. Qed. +Lemma Z_Private_Div_NZQuot_mod_mul_r : forall a b c : Z, 0 <= a -> 0 < b -> 0 < c -> Z.rem a (b * c) = Z.rem a b + b * Z.rem (a ÷ b) c. Proof. intros; nia. Qed. +Lemma Z_Private_Div_NZQuot_mod_same : forall a : Z, 0 < a -> Z.rem a a = 0. Proof. intros; nia. Qed. +Lemma Z_Private_Div_NZQuot_mod_small : forall a b : Z, 0 <= a < b -> Z.rem a b = a. Proof. intros; nia. Qed. +Lemma Z_Private_Div_NZQuot_mod_small_iff : forall a b : Z, 0 <= a -> 0 < b -> Z.rem a b = a <-> a < b. Proof. intros; nia. Qed. +Lemma Z_Private_Div_NZQuot_mod_unique : forall a b q r : Z, 0 <= a -> 0 <= r < b -> a = b * q + r -> r = Z.rem a b. Proof. intros; nia. Qed. +Lemma Z_Private_Div_NZQuot_mul_div_le : forall a b : Z, 0 <= a -> 0 < b -> b * (a ÷ b) <= a. Proof. intros; nia. Qed. +Lemma Z_Private_Div_NZQuot_mul_mod_distr_l : forall a b c : Z, 0 <= a -> 0 < b -> 0 < c -> Z.rem (c * a) (c * b) = c * Z.rem a b. Proof. intros; nia. Qed. +Lemma Z_Private_Div_NZQuot_mul_mod_distr_r : forall a b c : Z, 0 <= a -> 0 < b -> 0 < c -> Z.rem (a * c) (b * c) = Z.rem a b * c. Proof. intros; nia. Qed. +Lemma Z_Private_Div_NZQuot_mul_mod : forall a b n : Z, 0 <= a -> 0 <= b -> 0 < n -> Z.rem (a * b) n = Z.rem (Z.rem a n * Z.rem b n) n. Proof. intros; nia. Qed. +Lemma Z_Private_Div_NZQuot_mul_mod_idemp_l : forall a b n : Z, 0 <= a -> 0 <= b -> 0 < n -> Z.rem (Z.rem a n * b) n = Z.rem (a * b) n. Proof. intros; nia. Qed. +Lemma Z_Private_Div_NZQuot_mul_mod_idemp_r : forall a b n : Z, 0 <= a -> 0 <= b -> 0 < n -> Z.rem (a * Z.rem b n) n = Z.rem (a * b) n. Proof. intros; nia. Qed. +Lemma Z_Private_Div_NZQuot_mul_succ_div_gt : forall a b : Z, 0 <= a -> 0 < b -> a < b * Z.succ (a ÷ b). Proof. intros; nia. Qed. +Lemma Z_Private_Div_Quot2Div_div_mod : forall a b : Z, b <> 0 -> a = b * (a ÷ b) + Z.rem a b. Proof. intros; nia. Qed. +Z_Private_Div_Quot2Div_div_wd Morphisms.Proper (Morphisms.respectful eq (Morphisms.respectful eq eq)) Z.quot +Lemma Z_Private_Div_Quot2Div_mod_bound_pos : forall a b : Z, 0 <= a -> 0 < b -> 0 <= Z.rem a b < b. Proof. intros; nia. Qed. +Z_Private_Div_Quot2Div_mod_wd Morphisms.Proper (Morphisms.respectful eq (Morphisms.respectful eq eq)) Z.rem +Lemma Z_quot_0_l : forall a : Z, a <> 0 -> 0 ÷ a = 0. Proof. intros; nia. Qed. +Lemma Z_quot_0_r_ext : forall x y : Z, y = 0 -> x ÷ y = 0. Proof. intros; nia. Qed. +Lemma Z_quot_1_l : forall a : Z, 1 < a -> 1 ÷ a = 0. Proof. intros; nia. Qed. +Lemma Z_quot_1_r : forall a : Z, a ÷ 1 = a. Proof. intros; nia. Qed. +Lemma Zquot2_quot : forall n : Z, Z.quot2 n = n ÷ 2. Proof. intros; nia. Qed. +Lemma Z_quot_abs : forall a b : Z, b <> 0 -> Z.abs a ÷ Z.abs b = Z.abs (a ÷ b). Proof. intros; nia. Qed. +Lemma Z_quot_abs_l : forall a b : Z, b <> 0 -> Z.abs a ÷ b = Z.sgn a * (a ÷ b). Proof. intros; nia. Qed. +Lemma Z_quot_abs_r : forall a b : Z, b <> 0 -> a ÷ Z.abs b = Z.sgn b * (a ÷ b). Proof. intros; nia. Qed. +Lemma Z_quot_add : forall a b c : Z, c <> 0 -> 0 <= (a + b * c) * a -> (a + b * c) ÷ c = a ÷ c + b. Proof. intros; nia. Qed. +Lemma Z_quot_add_l : forall a b c : Z, b <> 0 -> 0 <= (a * b + c) * c -> (a * b + c) ÷ b = a + c ÷ b. Proof. intros; nia. Qed. +Lemma Z_quot_div : forall a b : Z, b <> 0 -> a ÷ b = Z.sgn a * Z.sgn b * (Z.abs a / Z.abs b). Proof. intros; nia. Qed. +Lemma Z_quot_div_nonneg : forall a b : Z, 0 <= a -> 0 < b -> a ÷ b = a / b. Proof. intros; nia. Qed. +Lemma Z_quot_exact : forall a b : Z, b <> 0 -> a = b * (a ÷ b) <-> Z.rem a b = 0. Proof. intros; nia. Qed. +Lemma Z_quot_le_compat_l : forall p q r : Z, 0 <= p -> 0 < q <= r -> p ÷ r <= p ÷ q. Proof. intros; nia. Qed. +Lemma Z_quot_le_lower_bound : forall a b q : Z, 0 < b -> b * q <= a -> q <= a ÷ b. Proof. intros; nia. Qed. +Lemma Z_quot_le_mono : forall a b c : Z, 0 < c -> a <= b -> a ÷ c <= b ÷ c. Proof. intros; nia. Qed. +Lemma Z_quot_le_upper_bound : forall a b q : Z, 0 < b -> a <= b * q -> a ÷ b <= q. Proof. intros; nia. Qed. +Lemma Z_quot_lt : forall a b : Z, 0 < a -> 1 < b -> a ÷ b < a. Proof. intros; nia. Qed. +Lemma Z_quot_lt_upper_bound : forall a b q : Z, 0 <= a -> 0 < b -> a < b * q -> a ÷ b < q. Proof. intros; nia. Qed. +Lemma Z_quot_mul_cancel_l : forall a b c : Z, b <> 0 -> c <> 0 -> c * a ÷ (c * b) = a ÷ b. Proof. intros; nia. Qed. +Lemma Z_quot_mul_cancel_r : forall a b c : Z, b <> 0 -> c <> 0 -> a * c ÷ (b * c) = a ÷ b. Proof. intros; nia. Qed. +Lemma Z_quot_mul : forall a b : Z, b <> 0 -> a * b ÷ b = a. Proof. intros; nia. Qed. +Lemma Z_quot_mul_le : forall a b c : Z, 0 <= a -> 0 < b -> 0 <= c -> c * (a ÷ b) <= c * a ÷ b. Proof. intros; nia. Qed. +Lemma Z_quot_opp_l : forall a b : Z, b <> 0 -> - a ÷ b = - (a ÷ b). Proof. intros; nia. Qed. +Lemma Z_quot_opp_opp : forall a b : Z, b <> 0 -> - a ÷ - b = a ÷ b. Proof. intros; nia. Qed. +Lemma Z_quot_opp_r : forall a b : Z, b <> 0 -> a ÷ - b = - (a ÷ b). Proof. intros; nia. Qed. +Lemma Z_quot_pos : forall a b : Z, 0 <= a -> 0 < b -> 0 <= a ÷ b. Proof. intros; nia. Qed. +Lemma Z_quot_quot : forall a b c : Z, b <> 0 -> c <> 0 -> a ÷ b ÷ c = a ÷ (b * c). Proof. intros; nia. Qed. +Lemma Z_quot_rem' : forall a b : Z, a = b * (a ÷ b) + Z.rem a b. Proof. intros; nia. Qed. +Lemma Z_quot_rem : forall a b : Z, b <> 0 -> a = b * (a ÷ b) + Z.rem a b. Proof. intros; nia. Qed. +Lemma Z_quot_same : forall a : Z, a <> 0 -> a ÷ a = 1. Proof. intros; nia. Qed. +Lemma Z_quot_small : forall a b : Z, 0 <= a < b -> a ÷ b = 0. Proof. intros; nia. Qed. +Lemma Z_quot_small_iff : forall a b : Z, b <> 0 -> a ÷ b = 0 <-> Z.abs a < Z.abs b. Proof. intros; nia. Qed. +Lemma Z_quot_str_pos : forall a b : Z, 0 < b <= a -> 0 < a ÷ b. Proof. intros; nia. Qed. +Lemma Z_quot_unique_exact : forall a b q : Z, b <> 0 -> a = b * q -> q = a ÷ b. Proof. intros; nia. Qed. +Lemma Z_quot_unique : forall a b q r : Z, 0 <= a -> 0 <= r < b -> a = b * q + r -> q = a ÷ b. Proof. intros; nia. Qed. +Z_quot_wd Morphisms.Proper (Morphisms.respectful Z.eq (Morphisms.respectful Z.eq Z.eq)) Z.quot +Lemma Zquot_Zeven_rem : forall a : Z, Z.even a = (Z.rem a 2 =? 0). Proof. intros; nia. Qed. +Lemma Zquot_Z_mult_quot_ge : forall a b : Z, a <= 0 -> a <= b * (a ÷ b) <= 0. Proof. intros; nia. Qed. +Lemma Zquot_Z_mult_quot_le : forall a b : Z, 0 <= a -> 0 <= b * (a ÷ b) <= a. Proof. intros; nia. Qed. +Lemma Zquot_Zmult_rem_distr_l : forall a b c : Z, Z.rem (c * a) (c * b) = c * Z.rem a b. Proof. intros; nia. Qed. +Lemma Zquot_Zmult_rem_distr_r : forall a b c : Z, Z.rem (a * c) (b * c) = Z.rem a b * c. Proof. intros; nia. Qed. +Lemma Zquot_Zmult_rem : forall a b n : Z, Z.rem (a * b) n = Z.rem (Z.rem a n * Z.rem b n) n. Proof. intros; nia. Qed. +Lemma Zquot_Zmult_rem_idemp_l : forall a b n : Z, Z.rem (Z.rem a n * b) n = Z.rem (a * b) n. Proof. intros; nia. Qed. +Lemma Zquot_Zmult_rem_idemp_r : forall a b n : Z, Z.rem (b * Z.rem a n) n = Z.rem (b * a) n. Proof. intros; nia. Qed. +Lemma Zquot_Zodd_rem : forall a : Z, Z.odd a = negb (Z.rem a 2 =? 0). Proof. intros; nia. Qed. +Lemma Zquot_Zplus_rem : forall a b n : Z, 0 <= a * b -> Z.rem (a + b) n = Z.rem (Z.rem a n + Z.rem b n) n. Proof. intros; nia. Qed. +Lemma Zquot_Zplus_rem_idemp_l : forall a b n : Z, 0 <= a * b -> Z.rem (Z.rem a n + b) n = Z.rem (a + b) n. Proof. intros; nia. Qed. +Lemma Zquot_Zplus_rem_idemp_r : forall a b n : Z, 0 <= a * b -> Z.rem (b + Z.rem a n) n = Z.rem (b + a) n. Proof. intros; nia. Qed. +Lemma Zquot_Zquot_0_l : forall a : Z, 0 ÷ a = 0. Proof. intros; nia. Qed. +Lemma Zquot_Zquot_0_r : forall a : Z, a ÷ 0 = 0. Proof. intros; nia. Qed. +Lemma Zquot_Z_quot_exact_full : forall a b : Z, a = b * (a ÷ b) <-> Z.rem a b = 0. Proof. intros; nia. Qed. +Lemma Zquot_Zquot_le_lower_bound : forall a b q : Z, 0 < b -> q * b <= a -> q <= a ÷ b. Proof. intros; nia. Qed. +Lemma Zquot_Zquot_le_upper_bound : forall a b q : Z, 0 < b -> a <= q * b -> a ÷ b <= q. Proof. intros; nia. Qed. +Lemma Zquot_Z_quot_lt : forall a b : Z, 0 < a -> 2 <= b -> a ÷ b < a. Proof. intros; nia. Qed. +Lemma Zquot_Zquot_lt_upper_bound : forall a b q : Z, 0 <= a -> 0 < b -> a < q * b -> a ÷ b < q. Proof. intros; nia. Qed. +Lemma Zquot_Zquot_mod_unique_full : forall a b q r : Z, Zquot.Remainder a b r -> a = b * q + r -> q = a ÷ b /\ r = Z.rem a b. Proof. intros; nia. Qed. +Lemma Zquot_Z_quot_monotone : forall a b c : Z, 0 <= c -> a <= b -> a ÷ c <= b ÷ c. Proof. intros; nia. Qed. +Lemma Zquot_Zquot_mult_cancel_l : forall a b c : Z, c <> 0 -> c * a ÷ (c * b) = a ÷ b. Proof. intros; nia. Qed. +Lemma Zquot_Zquot_mult_cancel_r : forall a b c : Z, c <> 0 -> a * c ÷ (b * c) = a ÷ b. Proof. intros; nia. Qed. +Lemma Zquot_Zquot_mult_le : forall a b c : Z, 0 <= a -> 0 <= b -> 0 <= c -> c * (a ÷ b) <= c * a ÷ b. Proof. intros; nia. Qed. +Lemma Zquot_Zquot_opp_l : forall a b : Z, - a ÷ b = - (a ÷ b). Proof. intros; nia. Qed. +Lemma Zquot_Zquot_opp_opp : forall a b : Z, - a ÷ - b = a ÷ b. Proof. intros; nia. Qed. +Lemma Zquot_Zquot_opp_r : forall a b : Z, a ÷ - b = - (a ÷ b). Proof. intros; nia. Qed. +Lemma Zquot_Z_quot_plus : forall a b c : Z, 0 <= (a + b * c) * a -> c <> 0 -> (a + b * c) ÷ c = a ÷ c + b. Proof. intros; nia. Qed. +Lemma Zquot_Z_quot_plus_l : forall a b c : Z, 0 <= (a * b + c) * c -> b <> 0 -> b <> 0 -> (a * b + c) ÷ b = a + c ÷ b. Proof. intros; nia. Qed. +Lemma Zquot_Z_quot_pos : forall a b : Z, 0 <= a -> 0 <= b -> 0 <= a ÷ b. Proof. intros; nia. Qed. +Lemma Zquot_Zquotrem_Zdiv_eucl_pos : forall a b : Z, 0 <= a -> 0 < b -> a ÷ b = a / b /\ Z.rem a b = a mod b. Proof. intros; nia. Qed. +Lemma Zquot_Zquot_sgn : forall a b : Z, 0 <= Z.sgn (a ÷ b) * Z.sgn a * Z.sgn b. Proof. intros; nia. Qed. +Lemma Zquot_Zquot_unique_full : forall a b q r : Z, Zquot.Remainder a b r -> a = b * q + r -> q = a ÷ b. Proof. intros; nia. Qed. +Lemma Zquot_Zquot_Zdiv_pos : forall a b : Z, 0 <= a -> 0 <= b -> a ÷ b = a / b. Proof. intros; nia. Qed. +Lemma Zquot_Zquot_Zquot : forall a b c : Z, a ÷ b ÷ c = a ÷ (b * c). Proof. intros; nia. Qed. +Lemma Zquot_Zrem_0_l : forall a : Z, Z.rem 0 a = 0. Proof. intros; nia. Qed. +Lemma Zquot_Zrem_0_r : forall a : Z, Z.rem a 0 = a. Proof. intros; nia. Qed. +Lemma Zquot_Zrem_divides : forall a b : Z, Z.rem a b = 0 <-> (exists c : Z, a = b * c). Proof. intros; nia. Qed. +Lemma Zquot_Zrem_even : forall a : Z, Z.rem a 2 = (if Z.even a then 0 else Z.sgn a). Proof. intros; nia. Qed. +Lemma Zquot_Zrem_le : forall a b : Z, 0 <= a -> 0 <= b -> Z.rem a b <= a. Proof. intros; nia. Qed. +Lemma Zquot_Zrem_lt_neg : forall a b : Z, a <= 0 -> b <> 0 -> - Z.abs b < Z.rem a b <= 0. Proof. intros; nia. Qed. +Lemma Zquot_Zrem_lt_neg_neg : forall a b : Z, a <= 0 -> b < 0 -> b < Z.rem a b <= 0. Proof. intros; nia. Qed. +Lemma Zquot_Zrem_lt_neg_pos : forall a b : Z, a <= 0 -> 0 < b -> - b < Z.rem a b <= 0. Proof. intros; nia. Qed. +Lemma Zquot_Zrem_lt_pos : forall a b : Z, 0 <= a -> b <> 0 -> 0 <= Z.rem a b < Z.abs b. Proof. intros; nia. Qed. +Lemma Zquot_Zrem_lt_pos_neg : forall a b : Z, 0 <= a -> b < 0 -> 0 <= Z.rem a b < - b. Proof. intros; nia. Qed. +Lemma Zquot_Zrem_lt_pos_pos : forall a b : Z, 0 <= a -> 0 < b -> 0 <= Z.rem a b < b. Proof. intros; nia. Qed. +Lemma Zquot_Z_rem_mult : forall a b : Z, Z.rem (a * b) b = 0. Proof. intros; nia. Qed. +Lemma Zquot_Zrem_odd : forall a : Z, Z.rem a 2 = (if Z.odd a then Z.sgn a else 0). Proof. intros; nia. Qed. +Lemma Zquot_Zrem_opp_l : forall a b : Z, Z.rem (- a) b = - Z.rem a b. Proof. intros; nia. Qed. +Lemma Zquot_Zrem_opp_opp : forall a b : Z, Z.rem (- a) (- b) = - Z.rem a b. Proof. intros; nia. Qed. +Lemma Zquot_Zrem_opp_r : forall a b : Z, Z.rem a (- b) = Z.rem a b. Proof. intros; nia. Qed. +Lemma Zquot_Z_rem_plus : forall a b c : Z, 0 <= (a + b * c) * a -> Z.rem (a + b * c) c = Z.rem a c. Proof. intros; nia. Qed. +Lemma Zquot_Zrem_rem : forall a n : Z, Z.rem (Z.rem a n) n = Z.rem a n. Proof. intros; nia. Qed. +Lemma Zquot_Z_rem_same : forall a : Z, Z.rem a a = 0. Proof. intros; nia. Qed. +Lemma Zquot_Zrem_sgn2 : forall a b : Z, 0 <= Z.rem a b * a. Proof. intros; nia. Qed. +Lemma Zquot_Zrem_sgn : forall a b : Z, 0 <= Z.sgn (Z.rem a b) * Z.sgn a. Proof. intros; nia. Qed. +Lemma Zquot_Zrem_unique_full : forall a b q r : Z, Zquot.Remainder a b r -> a = b * q + r -> r = Z.rem a b. Proof. intros; nia. Qed. +Lemma Zquot_Zrem_Zmod_pos : forall a b : Z, 0 <= a -> 0 < b -> Z.rem a b = a mod b. Proof. intros; nia. Qed. +Lemma Zquot_Zrem_Zmod_zero : forall a b : Z, b <> 0 -> Z.rem a b = 0 <-> a mod b = 0. Proof. intros; nia. Qed. +Lemma Z_rem_0_l : forall a : Z, a <> 0 -> Z.rem 0 a = 0. Proof. intros; nia. Qed. +Lemma Z_rem_0_r_ext : forall x y : Z, y = 0 -> Z.rem x y = x. Proof. intros; nia. Qed. +Lemma Z_rem_1_l : forall a : Z, 1 < a -> Z.rem 1 a = 1. Proof. intros; nia. Qed. +Lemma Z_rem_1_r : forall a : Z, Z.rem a 1 = 0. Proof. intros; nia. Qed. +Lemma Z_rem_abs : forall a b : Z, b <> 0 -> Z.rem (Z.abs a) (Z.abs b) = Z.abs (Z.rem a b). Proof. intros; nia. Qed. +Lemma Z_rem_abs_l : forall a b : Z, b <> 0 -> Z.rem (Z.abs a) b = Z.abs (Z.rem a b). Proof. intros; nia. Qed. +Lemma Z_rem_abs_r : forall a b : Z, b <> 0 -> Z.rem a (Z.abs b) = Z.rem a b. Proof. intros; nia. Qed. +Lemma Z_rem_add : forall a b c : Z, c <> 0 -> 0 <= (a + b * c) * a -> Z.rem (a + b * c) c = Z.rem a c. Proof. intros; nia. Qed. +Lemma Z_rem_bound_abs : forall a b : Z, b <> 0 -> Z.abs (Z.rem a b) < Z.abs b. Proof. intros; nia. Qed. +Lemma Z_rem_bound_neg_neg : forall x y : Z, y < 0 -> x <= 0 -> y < Z.rem x y <= 0. Proof. intros; nia. Qed. +Lemma Z_rem_bound_neg_pos : forall x y : Z, y < 0 -> 0 <= x -> 0 <= Z.rem x y < - y. Proof. intros; nia. Qed. +Lemma Z_rem_bound_pos : forall a b : Z, 0 <= a -> 0 < b -> 0 <= Z.rem a b < b. Proof. intros; nia. Qed. +Lemma Z_rem_bound_pos_neg : forall x y : Z, 0 < y -> x <= 0 -> - y < Z.rem x y <= 0. Proof. intros; nia. Qed. +Lemma Z_rem_bound_pos_pos : forall x y : Z, 0 < y -> 0 <= x -> 0 <= Z.rem x y < y. Proof. intros; nia. Qed. +Lemma Z_rem_eq : forall a b : Z, b <> 0 -> Z.rem a b = a - b * (a ÷ b). Proof. intros; nia. Qed. +Lemma Z_rem_le : forall a b : Z, 0 <= a -> 0 < b -> Z.rem a b <= a. Proof. intros; nia. Qed. +Lemma Z_rem_mod_eq_0 : forall a b : Z, b <> 0 -> Z.rem a b = 0 <-> a mod b = 0. Proof. intros; nia. Qed. +Lemma Z_rem_mod : forall a b : Z, b <> 0 -> Z.rem a b = Z.sgn a * (Z.abs a mod Z.abs b). Proof. intros; nia. Qed. +Lemma Z_rem_mod_nonneg : forall a b : Z, 0 <= a -> 0 < b -> Z.rem a b = a mod b. Proof. intros; nia. Qed. +Lemma Z_rem_mul : forall a b : Z, b <> 0 -> Z.rem (a * b) b = 0. Proof. intros; nia. Qed. +Lemma Z_rem_nonneg : forall a b : Z, b <> 0 -> 0 <= a -> 0 <= Z.rem a b. Proof. intros; nia. Qed. +Lemma Z_rem_nonpos : forall a b : Z, b <> 0 -> a <= 0 -> Z.rem a b <= 0. Proof. intros; nia. Qed. +Lemma Z_rem_opp_l : forall a b : Z, b <> 0 -> Z.rem (- a) b = - Z.rem a b. Proof. intros; nia. Qed. +Lemma Z_rem_opp_l' : forall a b : Z, Z.rem (- a) b = - Z.rem a b. Proof. intros; nia. Qed. +Lemma Z_rem_opp_opp : forall a b : Z, b <> 0 -> Z.rem (- a) (- b) = - Z.rem a b. Proof. intros; nia. Qed. +Lemma Z_rem_opp_r : forall a b : Z, b <> 0 -> Z.rem a (- b) = Z.rem a b. Proof. intros; nia. Qed. +Lemma Z_rem_opp_r' : forall a b : Z, Z.rem a (- b) = Z.rem a b. Proof. intros; nia. Qed. +Lemma Z_rem_quot : forall a b : Z, b <> 0 -> Z.rem a b ÷ b = 0. Proof. intros; nia. Qed. +Lemma Z_rem_rem : forall a n : Z, n <> 0 -> Z.rem (Z.rem a n) n = Z.rem a n. Proof. intros; nia. Qed. +Lemma Z_rem_same : forall a : Z, a <> 0 -> Z.rem a a = 0. Proof. intros; nia. Qed. +Lemma Z_rem_sign : forall a b : Z, a <> 0 -> b <> 0 -> Z.sgn (Z.rem a b) <> - Z.sgn a. Proof. intros; nia. Qed. +Lemma Z_rem_sign_mul : forall a b : Z, b <> 0 -> 0 <= Z.rem a b * a. Proof. intros; nia. Qed. +Lemma Z_rem_sign_nz : forall a b : Z, b <> 0 -> Z.rem a b <> 0 -> Z.sgn (Z.rem a b) = Z.sgn a. Proof. intros; nia. Qed. +Lemma Z_rem_small : forall a b : Z, 0 <= a < b -> Z.rem a b = a. Proof. intros; nia. Qed. +Lemma Z_rem_small_iff : forall a b : Z, b <> 0 -> Z.rem a b = a <-> Z.abs a < Z.abs b. Proof. intros; nia. Qed. +Lemma Z_rem_unique : forall a b q r : Z, 0 <= a -> 0 <= r < b -> a = b * q + r -> r = Z.rem a b. Proof. intros; nia. Qed. +Lemma Z_rem_wd : Morphisms.Proper (Morphisms.respectful Z.eq (Morphisms.respectful Z.eq Z.eq)) Z.rem. Proof. intros; nia. Qed. +*) |