| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
|
|
|
|
|
|
|
| |
It's possible that I should have removed more "allows", as many
instances of "foo allows to bar" could have been replaced by "foo bars"
(e.g., "[Qed] allows to check and save a complete proof term" could be
"[Qed] checks and saves a complete proof term"), but not always (e.g.,
"the optional argument allows to ignore universe polymorphism" should
not be "the optional argument ignores universe polymorphism" but "the
optional argument allows the caller to instruct Coq to ignore universe
polymorphism" or something similar).
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
- The earlier proof-of-concept file NPeano (which instantiates
the "Numbers" framework for nat) becomes now the entry point
in the Arith lib, and gets renamed PeanoNat. It still provides
an inner module "Nat" which sums up everything about type nat
(functions, predicates and properties of them).
This inner module Nat is usable as soon as you Require Import Arith,
or just Arith_base, or simply PeanoNat.
- Definitions of operations over type nat are now grouped in a new
file Init/Nat.v. This file is meant to be used without "Import",
hence providing for instance Nat.add or Nat.sqrt as soon as coqtop
starts (but no proofs about them).
- The definitions that used to be in Init/Peano.v (pred, plus, minus, mult)
are now compatibility notations (for Nat.pred, Nat.add, Nat.sub, Nat.mul
where here Nat is Init/Nat.v).
- This Coq.Init.Nat module (with only pure definitions) is Include'd
in the aforementioned Coq.Arith.PeanoNat.Nat. You might see Init.Nat
sometimes instead of just Nat (for instance when doing "Print plus").
Normally it should be ok to just ignore these "Init" since
Init.Nat is included in the full PeanoNat.Nat. I'm investigating if
it's possible to get rid of these "Init" prefixes.
- Concerning predicates, orders le and lt are still defined in Init/Peano.v,
with their notations "<=" and "<". Properties in PeanoNat.Nat directly
refer to these predicates in Peano. For instantation reasons, PeanoNat.Nat
also contains a Nat.le and Nat.lt (defined via "Definition le := Peano.le",
we cannot yet include an Inductive to implement a Parameter), but these
aliased predicates won't probably be very convenient to use.
- Technical remark: I've split the previous property functor NProp in
two parts (NBasicProp and NExtraProp), it helps a lot for building
PeanoNat.Nat incrementally. Roughly speaking, we have the following schema:
Module Nat.
Include Coq.Init.Nat. (* definition of operations : add ... sqrt ... *)
... (** proofs of specifications for basic ops such as + * - *)
Include NBasicProp. (** generic properties of these basic ops *)
... (** proofs of specifications for advanced ops (pow sqrt log2...)
that may rely on proofs for + * - *)
Include NExtraProp. (** all remaining properties *)
End Nat.
- All other files in directory Arith are now taking advantage of PeanoNat :
they are now filled with compatibility notations (when earlier lemmas
have exact counterpart in the Nat module) or lemmas with one-line proofs
based on the Nat module. All hints for database "arith" remain declared
in these old-style file (such as Plus.v, Lt.v, etc). All the old-style
files are still Require'd (or not) by Arith.v, just as before.
- Compatibility should be almost complete. For instance in the stdlib,
the only adaptations were due to .ml code referring to some Coq constant
name such as Coq.Init.Peano.pred, which doesn't live well with the
new compatibility notations.
|
| |
|
|
|
|
|
|
|
| |
in Prop of constructors of inductive types independent of these names.
Incidentally upgraded/simplified a couple of proofs, mainly in Reals.
This prepares to the next commit about using names based on H for such
hypotheses in Prop.
|
| | |
|
| |
|
|
|
|
|
|
|
| |
in the Evd of proofs (Evd.from_env).
- Allow to set the Store.t value of new evars, e.g. to set constraint evars as
unresolvable in rewrite.ml.
- Fix a HUGE performance problem in the processing of constraints, which was remerging
all the previous constraints with the ambient global universes at each new constraint addition.
Performance is now back to (or better than) normal.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Add [Polymorphic] and [Monomorphic] local flag for definitions as well as
[Set Universe Polymorphism] global flag to make all following definitions
polymorphic. Mainly syntax for now.
First part of the big changes to the kernel:
- Const, Ind, Construct now come with a universe level instance
- It is used for type inference in the kernel, which now also takes
a graph as input: actually a set of local universe variables and their
constraints. Type inference just checks that the constraints are enough
to satisfy its own rules.
- Remove polymorphic_arity and _knowing_parameters everywhere: we
don't need full applications for polymorphism to apply anymore, as
we generate fresh variables at each constant/inductive/constructor
application. However knowing_parameters variants might be reinstated
later for optimization.
- New structures exported in univ.mli:
- universe_list for universe level instances
- universe_context(_set) for the local universe constraints, also
recording which variables will be local and hence generalized after
inference if defining a polymorphic ind/constant.
- this patch makes coq stop compiling at indtypes.ml
Adapt kernel, library, pretyping, tactics and toplevel to universe polymorphism.
Various degrees of integration, places where I was not sure what to do or
just postponed bigger reorganizations of the code are marked with FIXMEs.
Main changes:
- Kernel now checks constraints and does not infer them anymore.
- The inference functions produce a context of constraints that were checked
during inference, useful to do double-checking of the univ. poly. code
but might be removed later.
- Constant, Inductive entries now have a universe context (local variables
and constraints) associated to them.
- Printing, debugging functions for the new structures are also implemented.
- Now stopping at Logic.v
- Lots of new code in kernel/univ.ml that should be reviewed.
- kernel/indtypes probably does not do what's right when inferring inductive
type constraints.
- Adapted evd to use the new universe context structure.
- Did not deal with unification/evar_conv.
- Add externalisation code for universe level instances.
- Support for polymorphism in pretyping/command and proofs/proofview etc.
Needed wrapping of [fresh_.._instance] through the evar_map, which
contains the local state of universes during type-checking.
- Correct the inductive scheme generation to support polymorphism as well.
- Have to review kernel code for correctness, and especially rework the
computation of universe constraints for inductives.
Stops somewhat later in Logic.v
- Fix naming of local/toplevel universes to be correctly done at typechecking time:
local variables have no dirpath.
- Add code to do substitution of universes in modules, not finished yet.
- Move fresh_* functions out of kernel, it won't ever build a universe level again!
- Adapt a lot of new_Type to use the correct dirpath and declare the new types in the evar_map
so we keep track of them.
- A bit of code factorization (evd_comb moved, pretype_global).
- Refactor more code
- Adapt plugins code (sometimes wrong, marked with FIXME)
- Fix cases generating unneeded universe (not sure it's ok though)
- Fix scheme generation for good, might have opportunity to cleanup
the terms later.
Init compiles now (which means rewrite, inversion, elim etc.. work as well).
- Unsolved issue of pretyping to lower sorts properly (to Prop for example).
This has to do with the (Retyping.get_type_of) giving algebraic universes that
would appear on the right of constraints.
This makes checking for dangling universes at the end of pretyping fail,
hence the check in kernel/univ was removed. It should come back when we have
a fix for this.
- Correctly (?) compute the levels of inductive types.
Removed old code pertaining to universe polymorphism. Note that we generate
constraint variables for the conclusion of inductive types invariably.
- Shrink constraints before going to the kernel, combine substitution of the
smaller universe set with normalization of evars (maybe not done everywhere,
only ordinary inductives, definitions and proofs)
- More API reworks overall. tclPUSHCONTEXT can be used to add fresh universes
to the proof goal (used in a few places to get the right instance.
- Quick fix for auto that won't work in the long run. It should always have been
restricted to take constant references as input, without any loss of generality
over constrs.
Fix some plugins and insertion of non-polymorphic constants in a module.
Now stops in relation classes.
Cleanup and move code from kernel to library and from pretyping to library too.
Now there is a unique universe counter declared in library/universes.ml along
with all the functions to generate new universes and get fresh constant/inductive
terms.
- Various function renamings
- One important change in kernel/univ.ml: now [sup] can be applied to Prop.
- Adapt records/classes to universe polymorphism
- Now stops in EqDepFacts due to imprecise universe polymorphism.
Forgot to git add those files.
interp_constr returns the universe context
The context is then pushed through the environment (or proof goal
sigma).
- Fix insertion of constants/inductives in env, pushing constraints to
the global env for non-polymorphic ones.
- Add Prop as a universe level to do proper type inference with sorts.
It is allowed to take [sup] of [Prop] now.
- New nf_evar based on new Evd.map(_undefined)
- In proofs/logic.ml: conv_leq_goal might create some constraints that
are now recorded.
- Adapt Program code to universes.
Merge with latest trunk + fixes
-Use new constr_of_global from universes
- fix eqschemes to use polymorphic universes
- begin fixing cctac but f_equal still fails
- fix [simpl] and rest of tacred
- all the eq_constr with mkConst foo should be fixed as well, only
partially done
- Fix term hashing function to recognize equal terms up to universe instances.
- Fix congruence closure to equate terms that differ only in universe instances,
these will be resolved by constraints.
Add a set of undefined universe variables to unification.
Universe variables can now be declared rigid or flexible (unifiable).
Flexible variables are resolved at the end of typechecking by instantiating
them to their glb, adding upper bound constraints associated to them.
Also:
- Add polymorphic flag for inductives.
- Fix cooking partially
- Fix kernel/univ.ml to do normalization of universe expressions at
the end of substitution.
Correct classes/structures universe inference
- Required a bit of extension in Univ to handle Max properly (sup u
(u+1)) was returning (max(u,u+1)) for example.
- Try a version where substitution of universe expressions for universe
levels is allowed at the end of unification. By an invariant this
should only instantiate with max() types that are morally "on the
right" only.
This is controlled using a rigidity attribute of universe variables,
also allowing to properly do unification w.r.t. universes during
typechecking/inference.
- Currently fails in Vectors/Fin.v because case compilation generates
"flexible" universes that actually appear in the term...
Fix unification of universe variables.
- Fix choice of canonical universe in presence of universe constraints,
and do so by relying on a trichotomy for universe variables: rigid
(won't be substituted), flexible (might be if not substituted by an
algebraic) and flexible_alg (always substituted).
- Fix romega code and a few more plugins, most of the standard library
goes through now.
- Had to define some inductives as Polymorphic explicitly to make
proofs go through, more to come, and definitions should be polymorphic
too, otherwise inconsistencies appear quickly (two uses of the same
polymorphic ind through monomorphic functions (like nth on lists of
Props and nats) will fix the monomorphic function's universe with eq
constraints that are incompatible).
- Correct universe polymorphism handling for fixpoint/cofixpoint
definitions.
- Fix romega to use the right universes for list constructors.
- Fix internalization/externalization to deal properly with the
implicit parsing of params.
- Fix fourier tactic w.r.t. GRefs
- Fix substitution saturation of universes.
- Fix number syntax plugin.
- Fix setoid_ring to take its coefficients in a Set rather
than a Type, avoiding a large number of useless universe constraints.
- Fix minor checker decl
- Fix btauto w.r.t. GRef
- Fix proofview to normalize universes in the original types as well.
- Fix definitions of projections to not take two universes at the same level,
but at different levels instead, avoiding unnecessary constraints that could
lower the level of one component depending on the use of the other component.
Fix simpl fst, snd to use @fst @snd as they have maximal implicits now.
- More simpl snd, fst fixes.
- Try to make the nth theory of lists polymorphic.
Check with Enrico if this change is ok. Case appearing in RingMicromega's call
to congruence l417, through a call to refine -> the_conv_x_leq.
Compile everything.
- "Fix" checker by deactivating code related to polymorphism, should
be updated.
- Make most of List.v polymorphic to help with following definitions.
- When starting a lemma, normalize w.r.t. universes, so that the types
get a fixed universe, not refinable later.
- In record, don't assign a fully flexible universe variable to the record
type if it is a definitional typeclass, as translate_constant doesn't expect
an algebraic universe in the type of a constant. It certainly should though.
- Fix micromega code.
Fix after rebase.
Update printing functions to print the polymorphic status of definitions
and their universe context.
Refine printing of universe contexts
- Fix printer for universe constraints
- Rework normalization of constraints to separate the Union-Find result
from computation of lubs/glbs.
Keep universe contexts of inductives/constants in entries for correct
substitution inside modules. Abstract interface to get an instantiation
of an inductive with its universe substitution in the kernel (no
substitution if the inductive is not polymorphic, even if mind_universes
is non-empty).
Make fst and snd polymorphic, fix instances in RelationPairs to use
different universes for the two elements of a pair.
- Fix bug in nf_constraints: was removing Set <= constraints, but should
remove Prop <= constraints only.
- Make proj1_sig, projT1... polymorphic to avoid weird universe unifications,
giving rise to universe inconsistenties.
Adapt auto hints to polymorphic references.
Really produce polymorphic hints... second try
- Remove algebraic universes that can't appear in the goal when taking the
type of a lemma to start.
Proper handling of universe contexts in clenv and auto so that
polymorphic hints are really refreshed at each application.
Fix erroneous shadowing of sigma variable.
- Make apparent the universe context used in pretyping, including information
about flexibility of universe variables.
- Fix induction to generate a fresh constant instance with flexible universe variables.
Add function to do conversion w.r.t. an evar map and its local universes.
- Fix define_evar_as_sort to not forget constraints coming from the refinement.
- Do not nf_constraints while we don't have the whole term at hand to substitute in.
- Move substitution of full universes to Universes
- Normalize universes inside an evar_map when doing nf_evar_map_universes.
- Normalize universes at each call to interp_ltac (potentially expensive)
Do not normalize all evars at each call to interp_gen in tactics: rather
incrementally normalize the terms at hand, supposing the normalization of universes
will concern only those appearing in it (dangerous but much more efficient).
Do not needlessly generate new universes constraints for projections of records.
Correct polymorphic discharge of section variables.
Fix autorewrite w.r.t. universes: polymorphic rewrite hints get fresh universe
instances at each application.
Fix r2l rewrite scheme to support universe polymorphism
Fix a bug in l2r_forward scheme and fix congruence scheme to handle polymorphism correctly.
Second try at fixing autorewrite, cannot do without pushing the constraints and the set of fresh
universe variables into the proof context.
- tclPUSHCONTEXT allow to set the ctx universe variables as flexible or rigid
- Fix bug in elimschemes, not taking the right sigma
Wrong sigma used in leibniz_rewrite
Avoid recomputation of bounds for equal universes in normalization of constraints,
only the canonical one need to be computed.
Make coercions work with universe polymorphic projections.
Fix eronneous bound in universes constraint solving.
Make kernel reduction and term comparison strictly aware of universe instances,
with variants for relaxed comparison that output constraints.
Otherwise some constraints that should appear during pretyping don't and we generate
unnecessary constraints/universe variables.
Have to adapt a few tactics to this new behavior by making them universe aware.
- Fix elimschemes to minimize universe variables
- Fix coercions to not forget the universe constraints generated by an application
- Change universe substitutions to maps instead of assoc lists.
- Fix absurd tactic to handle univs properly
- Make length and app polymorphic in List, unification sets their levels otherwise.
Move to modules for namespace management instead of long names in universe code.
More putting things into modules.
Change evar_map structure to support an incremental substitution of universes
(populated from Eq constraints), allowing safe and fast inference of precise levels,
without computing lubs.
- Add many printers and reorganize code
- Extend nf_evar to normalize universe variables according to the substitution.
- Fix ChoiceFacts.v in Logic, no universe inconsistencies anymore. But Diaconescu
still has one (something fixes a universe to Set).
- Adapt omega, functional induction to the changes.
Fix congruence, eq_constr implem, discharge of polymorphic inductives.
Fix merge in auto.
The [-parameters-matter] option (formerly relevant_equality).
Add -parameters-matter to coqc
Do compute the param levels at elaboration time if parameters_matter.
- Fix generalize tactic
- add ppuniverse_subst
- Start fixing normalize_universe_context w.r.t. normalize_univ_variables.
- Fix HUGE bug in Ltac interpretation not folding the sigma correctly if interpreting a tactic application
to multiple arguments.
- Fix bug in union of universe substitution.
- rename parameters-matter to indices-matter
- Fix computation of levels from indices not parameters.
- Fixing parsing so that [Polymorphic] can be applied to gallina extensions.
- When elaborating definitions, make the universes from the type rigid when
checking the term: they should stay abstracted.
- Fix typeclasses eauto's handling of universes for exact hints.
Rework all the code for infering the levels of inductives and checking their
allowed eliminations sorts.
This is based on the computation of a natural level for an inductive type I.
The natural level [nat] of [I : args -> sort := c1 : A1 -> I t1 .. cn : An -> I tn] is
computed by taking the max of the levels of the args (if indices matter) and the
levels of the constructor arguments.
The declared level [decl] of I is [sort], which might be Prop, Set or some Type u (u fresh
or not).
If [decl >= nat && not (decl = Prop && n >= 2)], the level of the inductive is [decl],
otherwise, _smashing_ occured.
If [decl] is impredicative (Prop or Set when Set is impredicative), we accept the
declared level, otherwise it's an error.
To compute the allowed elimination sorts, we have the following situations:
- No smashing occured: all sorts are allowed. (Recall props that are not
smashed are Empty/Unitary props)
- Some smashing occured:
- if [decl] is Type, we allow all eliminations (above or below [decl],
not sure why this is justified in general).
- if [decl] is Set, we used smashing for impredicativity, so only
small sorts are allowed (Prop, Set).
- if [decl] is Prop, only logical sorts are allowed: I has either
large universes inside it or more than 1 constructor.
This does not treat the case where only a Set appeared in I which
was previously accepted it seems.
All the standard library works with these changes. Still have to cleanup
kernel/indtypes.ml. It is a good time to have a whiskey with OJ.
Thanks to Peter Lumsdaine for bug reporting:
- fix externalisation of universe instances (still appearing when no Printing Universes)
- add [convert] and [convert_leq] tactics that keep track of evars and universe constraints.
- use them in [exact_check].
Fix odd behavior in inductive type declarations allowing to silently lower a Type i parameter
to Set for squashing a naturally Type i inductive to Set. Reinstate the LargeNonPropInductiveNotInType
exception.
Fix the is_small function not dealing properly with aliases of Prop/Set in Type.
Add check_leq in Evd and use it to decide if we're trying to squash an
inductive naturally in some Type to Set.
- Fix handling of universe polymorphism in typeclasses Class/Instance declarations.
- Don't allow lowering a rigid Type universe to Set silently.
- Move Ring/Field back to Type. It was silently putting R in Set due to the definition of ring_morph.
- Rework inference of universe levels for inductive definitions.
- Make fold_left/right polymorphic on both levels A and B (the list's type). They don't have to be
at the same level.
Handle selective Polymorphic/Monomorphic flag right for records.
Remove leftover command
Fix after update with latest trunk.
Backport patches on HoTT/coq to rebased version of universe polymorphism.
- Fix autorewrite wrong handling of universe-polymorphic rewrite rules. Fixes part of issue #7.
- Fix the [eq_constr_univs] and add an [leq_constr_univs] to avoid eager equation of universe
levels that could just be inequal. Use it during kernel conversion. Fixes issue #6.
- Fix a bug in unification that was failing too early if a choice in unification of universes
raised an inconsistency.
- While normalizing universes, remove Prop in the le part of Max expressions.
- Stop rigidifying the universes on the right hand side of a : in definitions.
- Now Hints can be declared polymorphic or not. In the first case they
must be "refreshed" (undefined universes are renamed) at each application.
- Have to refresh the set of universe variables associated to a hint
when it can be used multiple times in a single proof to avoid fixing
a level... A better & less expensive solution should exist.
- Do not include the levels of let-ins as part of records levels.
- Fix a NotConvertible uncaught exception to raise a more informative
error message.
- Better substitution of algebraics in algebraics (for universe variables that
can be algebraics).
- Fix issue #2, Context was not properly normalizing the universe context.
- Fix issue with typeclasses that were not catching UniverseInconsistencies
raised by unification, resulting in early failure of proof-search.
- Let the result type of definitional classes be an algebraic.
- Adapt coercions to universe polymorphic flag (Identity Coercion etc..)
- Move away a dangerous call in autoinstance that added constraints for every
polymorphic definitions once in the environment for no use.
Forgot one part of the last patch on coercions.
- Adapt auto/eauto to polymorphic hints as well.
- Factor out the function to refresh a clenv w.r.t. undefined universes.
Use leq_univ_poly in evarconv to avoid fixing universes.
Disallow polymorphic hints based on a constr as it is not possible to infer their universe
context. Only global references can be made polymorphic. Fixes issue #8.
Fix SearchAbout bug (issue #10).
Fix program w.r.t. universes: the universe context of a definition changes
according to the successive refinements due to typechecking obligations.
This requires the Proof modules to return the generated universe substitution
when finishing a proof, and this information is passed in the closing hook.
The interface is not very clean, will certainly change in the future.
- Better treatment of polymorphic hints in auto: terms can be polymorphic now, we refresh their
context as well.
- Needs a little change in test-pattern that seems breaks multiary uses of destruct in NZDiv.v, l495.
FIX to do.
Fix [make_pattern_test] to keep the universe information around and still
allow tactics to take multiple patterns at once.
- Fix printing of universe instances that should not be factorized blindly
- Fix handling of the universe context in program definitions by allowing the
hook at the end of an interactive proof to give back the refined universe context,
before it is transformed in the kernel.
- Fix a bug in evarconv where solve_evar_evar was not checking types of instances,
resulting in a loss of constraints in unification of universes and a growing number
of useless parametric universes.
- Move from universe_level_subst to universe_subst everywhere.
- Changed representation of universes for a canonical one
- Adapt the code so that universe variables might be substituted by
arbitrary universes (including algebraics). Not used yet except for
polymorphic universe variables instances.
- Adapt code to new constraint structure.
- Fix setoid rewrite handling of evars that was forgetting the initial
universe substitution !
- Fix code that was just testing conversion instead of keeping the
resulting universe constraints around in the proof engine.
- Make a version of reduction/fconv that deals with the more general
set of universe constraints.
- [auto using] should use polymorphic versions of the constants.
- When starting a proof, don't forget about the algebraic universes in
the universe context.
Rationalize substitution and normalization functions for universes.
Also change back the structure of universes to avoid considering levels
n+k as pure levels: they are universe expressions like max.
Everything is factored out in the Universes and Univ modules now and
the normalization functions can be efficient in the sense that they
can cache the normalized universes incrementally.
- Adapt normalize_context code to new normalization/substitution functions.
- Set more things to be polymorphic, e.g. in Ring or SetoidList for the rest
of the code to work properly while the constraint generation code is not adapted.
And temporarily extend the universe constraint code in univ to solve max(is) = max(js)
by first-order unification (these constraints should actually be implied not enforced).
- Fix romega plugin to use the right universes for polymorphic lists.
- Fix auto not refreshing the poly hints correctly.
- Proper postponing of universe constraints during unification, avoid making
arbitrary choices.
- Fix nf_evars_and* to keep the substitution around for later normalizations.
- Do add simplified universe constraints coming from unification during typechecking.
- Fix solve_by_tac in obligations to handle universes right, and the corresponding
substitution function.
Test global universe equality early during simplication of constraints.
Better hashconsing, but still not good on universe lists.
- Add postponing of "lub" constraints that should not be checked early,
they are implied by the others.
- Fix constructor tactic to use a fresh constructor instance avoiding
fixing universes.
- Use [eq_constr_universes] instead of [eq_constr_univs] everywhere,
this is the comparison function that doesn't care about the universe
instances.
- Almost all the library compiles in this new setting, but some more tactics
need to be adapted.
- Reinstate hconsing.
- Keep Prop <= u constraints that can be used to set the level of a universe
metavariable.
Add better hashconsing and unionfind in normalisation of constraints.
Fix a few problems in choose_canonical, normalization and substitution functions.
Fix after merge
Fixes after rebase with latest Coq trunk, everything compiles again,
albeit slowly in some cases.
- Fix module substitution and comparison of table keys in conversion
using the wrong order (should always be UserOrd now)
- Cleanup in universes, removing commented code.
- Fix normalization of universe context which was assigning global
levels to local ones. Should always be the other way!
- Fix universe implementation to implement sorted cons of universes
preserving order. Makes Univ.sup correct again, keeping universe in
normalized form.
- In evarconv.ml, allow again a Fix to appear as head of a weak-head normal
form (due to partially applied fixpoints).
- Catch anomalies of conversion as errors in reductionops.ml, sad but
necessary as eta-expansion might build ill-typed stacks like FProd,
[shift;app Rel 1], as it expands not only if the other side is rigid.
- Fix module substitution bug in auto.ml
- Fix case compilation: impossible cases compilation was generating useless universe
levels. Use an IDProp constant instead of the polymorphic identity to not influence
the level of the original type when building the case construct for the return type.
- Simplify normalization of universe constraints.
- Compute constructor levels of records correctly.
Fall back to levels for universe instances, avoiding issues of unification.
Add more to the test-suite for universe polymorphism.
Fix after rebase with trunk
Fix substitution of universes inside fields/params of records to be made
after all normalization is done and the level of the record has been
computed.
Proper sharing of lower bounds with fixed universes.
Conflicts:
library/universes.ml
library/universes.mli
Constraints were not enforced in compilation of cases
Fix after rebase with trunk
- Canonical projections up to universes
- Fix computation of class/record universe levels to allow
squashing to Prop/Set in impredicative set mode.
- Fix descend_in_conjunctions to properly instantiate projections with universes
- Avoid Context-bound variables taking extra universes in their associated universe context.
- Fix evar_define using the wrong direction when refreshing a universe under cumulativity
- Do not instantiate a local universe with some lower bound to a global one just because
they have the same local glb (they might not have the same one globally).
- Was loosing some global constraints during normalization (brought again by the kernel), fixed now.
- Proper [abstract] with polymorphic lemmas (polymorphic if the current proof is).
- Fix silly bug in autorewrite: any hint after the first one was always monomorphic.
- Fix fourier after rebase
- Refresh universes when checking types of metas in unification (avoid (sup (sup univ))).
- Speedup a script in FSetPositive.v
Rework definitions in RelationClasses and Morphisms to share universe
levels as much as possible. This factorizes many useless x <=
RelationClasses.foo constraints in code that uses setoid rewriting.
Slight incompatible change in the implicits for Reflexivity and
Irreflexivity as well.
- Share even more universes in Morphisms using a let.
- Use splay_prod instead of splay_prod_assum which doesn't reduce let's
to find a relation in setoid_rewrite
- Fix [Declare Instance] not properly dealing with let's in typeclass contexts.
Fixes in inductiveops, evarutil.
Patch by Yves Bertot to allow naming universes in inductive definitions.
Fixes in tacinterp not propagating evars correctly.
Fix for issue #27: lowering a Type to Prop is allowed during
inference (resulting in a Type (* Set *)) but kernel reduction
was wrongly refusing the equation [Type (*Set*) = Set].
Fix in interface of canonical structures: an instantiated polymorphic
projection is not needed to lookup a structure, just the projection name
is enough (reported by C. Cohen).
Move from universe inference to universe checking in the kernel.
All tactics have to be adapted so that they carry around their generated
constraints (living in their sigma), which is mostly straightforward.
The more important changes are when refering to Coq constants, the
tactics code is adapted so that primitive eq, pairing and sigma types might
be polymorphic.
Fix another few places in tacinterp and evarconv/evarsolve where the sigma
was not folded correctly.
- Fix discharge adding spurious global constraints on polymorphic universe variables
appearing in assumptions.
- Fixes in inductiveops not taking into account universe polymorphic inductives.
WIP on checked universe polymorphism, it is clearly incompatible
with the previous usage of polymorphic inductives + non-polymorphic
definitions on them as universe levels now appear in the inductive type,
and add equality constraints between universes that were otherwise just
in a cumulativity relation (not sure that was actually correct).
Refined version of unification of universe instances for first-order unification,
prefering unfolding to arbitrary identification of universes.
Moved kernel to universe checking only.
Adapt the code to properly infer constraints during typechecking and
refinement (tactics) and only check constraints when adding
constants/inductives to the environment. Exception made of module
subtyping that needs inference of constraints... The kernel conversion
(fconv) has two modes: checking only and inference, the later being used
by modules only. Evarconv/unification make use of a different strategy for
conversion of constants that prefer unfolding to blind unification of
rigid universes. Likewise, conversion checking backtracks on different universe
instances (modulo the constraints).
- adapt congruence/funind/ring plugins to this new mode, forcing them to
declare their constraints.
- To avoid big performance penalty with reification, make ring/field non-polymorphic
(non-linear explosion in run time to be investigated further).
- pattern and change tactics need special treatment: as they are not _reduction_
but conversion functions, their operation requires to update an evar_map with
new universe constraints.
- Fix vm_compute to work better with universes. If the normal
form is made only of constructors then the readback is correct. However a deeper change will
be needed to treat substitution of universe instances when unfolding constants.
Remove libtypes.ml
Fix after merge.
Fix after rebase with trunk.
**** Add projections to the kernel, as optimized implementations of constants.
- New constructor Proj expects a projection constant applied to its principal
inductive argument.
- Reduction machines shortcut the expansion to a case and directly project the
right argument.
- No need to keep parameters as part of the projection's arguments as they
are inferable from the type of the principal argument.
- ML code now compiles, debugging needed.
Start debugging the implementation of projections. Externalisation should
keep the information about projections.
Internalization, pattern-matching, unification and reduction
of projections.
Fix some code that used to have _ for parameters that are no longer
present in projections.
Fixes in unification, reduction, term indexing, auto hints based on projections,
add debug printers.
Fix byte-compilation of projections, unification, congruence with projections.
Adapt .v files using "@proj _ _ record" syntax, should come back on this later.
Fix coercion insertion code to properly deal with projection coercions.
Fix [simpl proj]... TODO [unfold proj], proj is not considered evaluable.
- Fix whnf of projections, now respecting opacity information.
- Fix conversion of projections to try first-order first and then
incrementally unfold them.
- Fix computation of implicit args for projections, simply dropping
the information for parameters.
- Fix a few scripts that relied on projections carrying their parameters (few at's,
rewrites).
- Fix unify_with_subterm to properly match under projections.
- Fix bug in cooking of projections.
- Add pattern PProj for projections.
- A very strange bug appeared in BigZ.v, making coqtop segfault on the export
of BigN... tofix
Fixes after rebase with trunk. Everything compiles now, with efficient
projections.
Fixes after rebase with trunk (esp. reductionops).
Remove warnings, backport patch from old univs+projs branch.
Proper expansion of projections during unification.
They are considered as maybe flexible keys in evarconv/unification. We
try firstorder unification and otherwise expand them as necessary,
completely mimicking the original behavior, when they were
constants. Fix head_constr_bound interface, the arguments are never
needed (they're outside their environment actually). [simpl] and
[red]/[intro] should behave just like before now.
Fix evarconv that was giving up on proj x = ?e problems too early.
- Port patch by Maxime Denes implementing fast projections in the native conversion.
- Backport patch to add eta-expansion for records.
Do not raise an exception but simply fails if trying to do eta on an inductive that is not a record.
Fix projections detyping/matching and unification.ml not always
recovering on first-order universe inequalities.
Correct eta-expansion for records, and change strategy for conversion
with projections to favor reduction over first-order unification a
little more. Fix a bug in Ltac pattern matching on projections.
Fix evars_reset_evd to not recheck existing constraints in case it is just an update
(performance improvement for typeclass resolution).
- Respect Global/Transparent oracle during unification. Opaque means
_never_ unfolded there.
- Add empty universes as well as the initial universes (having Prop < Set).
- Better display of universe inconsistencies.
- Add Beta Ziliani's patch to go fast avoiding imitation when possible.
- Allow instantiation by lower bound even if there are universes above
- (tentative) In refinement, avoid incremental refinement of terms
containing no holes and do it in one step (much faster on big terms).
Turned on only if not a checked command.
Remove dead code in univ/universes.ml and cleanup setup of hashconsing,
for a small speed and memory footprint improvement.
- Fix bug in unification using cumulativity when conversion should have been used.
- Fix unification of evars having type Type, no longer forcing them to be equal
(potentially more constraints): algorithm is now complete w.r.t. cumulativity.
- In clenvtac, use refine_nocheck as we are guaranteed to get well-typed terms
from unification now, including sufficient universe constraints. Small general
speedup.
- Fix inference of universe levels of inductive types to avoid smashing
inadvertently from Set to Prop.
- Fix computation of discharged hypotheses forgetting the arity in inductives.
- Fix wrong order in printing of universe inconsistency explanation
- Allow coercions between two polymorphic instances of the same inductive/constant.
- Do evar normalization and saturation by classes before trying to use program coercion
during pretyping.
- In unification, force equalities of universes when unifying the same rigid head constants.
- Fix omission of projections in constr_leq
- Fix [admit] tactic's handling of normalized universes.
Fix typing of projections not properly normalizing w.r.t. evars, resulting in anomaly sometimes.
Adapt rewrite to work with computational relations (in Type), while
maintaining backward compatibility with Propositional rewriting.
Introduce a [diff] function on evar maps and universe contexts to
properly deal with clause environments. Local hints in auto now store
just the extension of the evar map they rely on, so merging them becomes
efficient. This fixes an important performance issue in auto and typeclass
resolution in presence of a large number of universe constraints.
Change FSetPositive and MSetPositive to put their [elt] and [t] universes in
Type to avoid restricting global universes to [Set]. This is due to [flip]s
polymorphic type being fixed in monomorphic instances of Morphisms.v,
and rewriting hence forcing unification of levels that could be left unrelated.
- Try a fast_typeops implementation of kernel type inference that
allocates less by not rebuilding the term, shows a little performance
improvement, and less allocation.
- Build universe inconsistency explanations lazily, avoiding huge blowup
(x5) in check_constraints/merge_constraints in time and space (these
are stressed in universe polymorphic mode).
- Hashcons universe instances.
Add interface file for fast_typeops
Use monomorphic comparisons, little optimizations of hashconsing and
comparison in univ.ml.
Fix huge slowdown due to building huge error messages. Lazy is not
enough to tame this completely.
Fix last performance issue, due to abstracts building huge terms abstracting on parts of the section
context. Was due to wrong handling of Let... Qed.s in abstract. Performance is a tiny bit better than the
trunk now.
First step at compatibility layer for projections.
Compatibility mode for projections. c.(p), p c use primitive projs,
while @p refers to an expansion [λ params c, c.(p)]. Recovers almost
entire source compatibility with trunk scripts, except when mixing
@p and p and doing syntactic matching (they're unifiable though).
Add a [Set Primitive Projections] flag to set/unset the use of primitive
projections, selectively for each record. Adapt code to handle both the
legacy encoding and the primitive projections. Library is almost
source-to-source compatible, except for syntactic operations relying
on the presence of parameters. In primitive projections mode, @p refers
to an expansion [λ params r. p.(r)]. More information in CHANGES (to be
reformated/moved to reference manual).
Backport changes from HoTT/coq:
- Fix anomaly on uncatched NotASort in retyping.
- Better recognition of evars that are subject to typeclass resolution.
Fixes bug reported by J. Gross on coq-club.
- Print universe polymorphism information for parameters as well.
Fix interface for unsatisfiable constraints error, now a type error.
Try making ring polymorphic again, with a big slowdown, to be investigated.
Fix evar/universe leak in setoid rewrite.
- Add profiling flag
- Move setoid_ring back to non-polymorphic mode to compare perfs with trunk
- Change unification to allow using infer_conv more often (big perf culprit),
but semantics of backtracking on unification of constants is not properly
implemented there.
- Fix is_empty/union_evar_universe_context forgetting about some assignments.
- Performance is now very close to the trunk from june,
with projections deactivated.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Inner sub-modules with "Definition t := t" is hard to handle by
extraction: "type t = t" is recursive by default in OCaml, and
the aliased t cannot easily be fully qualified if it comes from
a higher unterminated module. There already exists some workarounds
(generating Coq__XXX modules), but this isn't playing nicely with
module types, where it's hard to insert code without breaking
subtyping.
To avoid falling too often in this situation, I've reorganized:
- GenericMinMax : we do not try anymore to deduce facts about
min by saying "min is a max on the reversed order". This hack
was anyway not so nice, some code was duplicated nonetheless
(at least statements), and the module structure was complex.
- OrdersTac : by splitting the functor argument in two
(EqLtLe <+ IsTotalOrder instead of TotalOrder), we avoid
the need for aliasing the type t, cf NZOrder.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16100 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
The ugly syntax "destruct x as [ ]_eqn:H" is replaced by:
destruct x eqn:H
destruct x as [ ] eqn:H
Some with induction. Of course, the pattern behind "as" is arbitrary.
For an anonymous version, H could be replaced by ?. The old syntax
with "_eqn" still works for the moment, by triggers a warning.
For making this new syntax work, we had to change the seldom-used
"induction x y z using foo" into "induction x, y, z using foo".
Now, only one "using" can be used per command instead of one per
comma-separated group earlier, but I doubt this will bother anyone.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15566 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
- For instance, refl_equal --> eq_refl
- Npos, Zpos, Zneg now admit more uniform qualified aliases
N.pos, Z.pos, Z.neg.
- A new module BinInt.Pos2Z with results about injections from
positive to Z
- A result about Z.pow pushed in the generic layer
- Zmult_le_compat_{r,l} --> Z.mul_le_mono_nonneg_{r,l}
- Using tactic Z.le_elim instead of Zle_lt_or_eq
- Some cleanup in ring, field, micromega
(use of "Equivalence", "Proper" ...)
- Some adaptions in QArith (for instance changed Qpower.Qpower_decomp)
- In ZMake and ZMake, functor parameters are now named NN and ZZ
instead of N and Z for avoiding confusions
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15515 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
- tauto/intuition now works uniformly on and, prod, or, sum, False,
Empty_set, unit, True (and isomorphic copies of them), iff, ->, and
on all inhabited singleton types with a no-arguments constructor
such as "eq t t" (even though the last case goes out of
propositional logic: this features is so often used that it is
difficult to come back on it).
- New dtauto and dintuition works on all inductive types with one
constructors and no real arguments (for instance, they work on
records such as "Equivalence"), in addition to -> and eq-like types.
- Moreover, both of them no longer unfold inner negations (this is a
souce of incompatibility for intuition and evaluation of the level
of incompatibility on contribs still needs to be done).
Incidentally, and amazingly, fixing bug #2680 made that constants
InfA_compat and InfA_eqA in SetoidList.v lost one argument: old tauto
had indeed destructed a section hypothesis "@StrictOrder A ltA@
thinking it was a conjunction, making this section hypothesis
artificially necessary while it was not.
Renouncing to the unfolding of inner negations made auto/eauto
sometimes succeeding more, sometimes succeeding less. There is by the
way a (standard) problem with not in auto/eauto: even when given as an
"unfold hint", it works only in goals, not in hypotheses, so that auto
is not able to solve something like "forall P, (forall x, ~ P x) -> P
0 -> False". Should we automatically add a lemma of type "HYPS -> A ->
False" in the hint database everytime a lemma ""HYPS -> ~A" is
declared (and "unfold not" is a hint), and similarly for all unfold
hints?
At this occasion, also re-did some proofs of Znumtheory.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15180 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
| |
Might be too much of a backwards-incompatible change"
Indeed it is breaking too many scripts.
This reverts commit 47e9afaaa4c08aca97d4f4b5a89cb40da76bd850.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14956 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
| |
too much of a backwards-incompatible change
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14949 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14718 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Instead of hard-coding in search.ml some substrings such
as "_admitted" or "_subproof" we don't want to see in results
of SearchAbout and co, we now have a user command:
Add Search Blacklist "foo".
Remove Search Blacklist "foo". (* the opposite *)
Print Table Search Blacklist. (* the current state *)
In Prelude.v, three substrings are blacklisted originally:
- "_admitted" for internal lemmas due to admit.
- "_subproof" for internal lemmas due to abstract.
- "Private_" for hiding auxiliary modules not meant for
global usage.
Note that substrings are searched in the fully qualified names
of the available lemmas (e.g. "Coq.Init.Peano.plus").
This commit also adds the prefix "Private_" to some internal modules
in Numbers, Z, N, etc.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14408 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14297 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
|
| |
- All statement using reflect are made transparent.
(Otherwise, since reflect isn't in Prop, extraction
complains now about opaque Type definition).
- remove two local Peqb_spec and Neqb_spec, now provided
globally as Pos.eqb_spec and N.eqb_spec.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14232 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Start of a uniform treatment of compare, eqb, leb, ltb:
- We now ensure that they are provided by N,Z,BigZ,BigN,Nat and Pos
- Some generic properties are derived in OrdersFacts.BoolOrderFacts
In BinPos, more work about sub_mask with nice implications
on compare (e.g. simplier proof of lt_trans).
In BinNat/BinPos, for uniformity, compare_antisym is now
(y ?= x) = CompOpp (x ?=y) instead of the symmetrical result.
In BigN / BigZ, eq_bool is now eqb
In BinIntDef, gtb and geb are kept for the moment, but
a comment advise to rather use ltb and leb. Z.div now uses
Z.ltb and Z.leb.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14227 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
|
| |
All the functions about Z is now in a separated file BinIntDef,
which is Included in BinInt.Z. This BinInt.Z directly
implements ZAxiomsSig, and instantiates derived properties ZProp.
Note that we refer to Z instead of t inside BinInt.Z,
otherwise ring breaks later on @eq Z.t
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14106 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
|
|
| |
A sub-module N in BinNat now contains functions add (ex-Nplus),
mul (ex-Nmult), ... and properties.
In particular, this sub-module N directly instantiates NAxiomsSig
and includes all derived properties NProp.
Files Ndiv_def and co are now obsolete and kept only for compat
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14100 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
BinPos now contain a sub-module Pos, in which are placed functions
like add (ex-Pplus), mul (ex-Pmult), ... and properties like
add_comm, add_assoc, ...
In addition to the name changes, the organisation is changed quite
a lot, to try to take advantage more of the orders < and <= instead
of speaking only of the comparison function.
The main source of incompatibilities in scripts concerns this compare:
Pos.compare is now a binary operation, expressed in terms of the
ex-Pcompare which is ternary (expecting an initial comparision as 3rd arg),
this ternary version being called now Pos.compare_cont. As for everything
else, compatibility notations (only parsing) are provided. But notations
"_ ?= _" on positive will have to be edited, since they now point to
Pos.compare.
We also make the sub-module Pos to be directly an OrderedType,
and include results about min and max.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14098 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
CompareSpec expects 3 propositions Peq Plt Pgt instead of 2 relations
eq lt and 2 points x y. For the moment, we still always use (Peq=eq x y),
(Plt=lt x y) (Pgt=lt y x), but this may not be always the case,
especially for Pgt. The former CompSpec is now defined in term of
CompareSpec. Compatibility is preserved (except maybe a rare unfold
or red to break the CompSpec definition).
Typically, CompareSpec looks nicer when we have infix notations, e.g.
forall x y, CompareSpec (x=y) (x<y) (y<x) (x?=x)
while CompSpec is shorter when we directly refer to predicates:
forall x y, CompSpec eq lt x y (compare x y)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13914 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
conversion when checking types of instanciations while having
restricted delta reduction for unification itself. This
makes auto/eauto... backward compatible.
- Change semantics of [Instance foo : C a.] to _not_ search
for an instance of [C a] automatically and potentially slow
down interaction, except for trivial classes with no fields.
Use [C a := _.] or [C a := {}] to search for an instance of
the class or for every field.
- Correct treatment of transparency information for classes
declared in sections.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13908 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13843 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
| |
were all declared as global).
- Add possibility to remove hints (Resolve or Immediate only) based on
the name of the lemma.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13842 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
As said in CHANGES:
<<
The inlining done during application of functors can now be controlled
more precisely. In addition to the "!F G" syntax preventing any inlining,
we can now use a priority level to select parameters to inline :
"<30>F G" means "only inline in F the parameters whose levels are <= 30".
The level of a parameter can be fixed by "Parameter Inline(30) foo".
When levels aren't given, the default value is 100. One can also use
the flag "Set Inline Level ..." to set a level.
>>
Nota : the syntax "Parameter Inline(30) foo" is equivalent to
"Set Inline Level 30. Parameter Inline foo.",
and "Include <30>F G" is equivalent to "Set Inline Level 30. Include F G."
For instance, in ZBinary, eq is @Logic.eq and should rather be inlined,
while in BigZ, eq is (fun x y => [x]=[y]) and should rather not be inlined.
We could achieve this behavior by setting a level such as 30 to the
parameter eq, and then tweaking the current level when applying functors.
This idea of levels might be too restrictive, we'll see, but at least
the implementation of this change was quite simple. There might be
situation where parameters cannot be linearly ordered according to their
"inlinablility". For these cases, we would need to mention names to inline
or not at a functor application, and this is a bit more tricky
(and might be a pain to use if there are many names).
No documentation for the moment, since this feature is experimental
and might still evolve.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13807 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
See NatInt/NZBits.v for the common axiomatization of bitwise functions
over naturals / integers. Some specs aren't pretty, but easier to
prove, see alternate statements in property functors {N,Z}Bits.
Negative numbers are considered via the two's complement convention.
We provide implementations for N (in Ndigits.v), for nat (quite dummy,
just for completeness), for Z (new file Zdigits_def), for BigN
(for the moment partly by converting to N, to be improved soon)
and for BigZ.
NOTA: For BigN.shiftl and BigN.shiftr, the two arguments are now in
the reversed order (for consistency with the rest of the world):
for instance BigN.shiftl 1 10 is 2^10.
NOTA2: Zeven.Zdiv2 is _not_ doing (Zdiv _ 2), but rather (Zquot _ 2)
on negative numbers. For the moment I've kept it intact, and have
just added a Zdiv2' which is truly equivalent to (Zdiv _ 2).
To reorganize someday ?
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13689 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
(floor convention).
We follow Haskell naming convention: quot and rem are for
Round-Toward-Zero (a.k.a Trunc, what Ocaml, C, Asm do by default, cf.
the ex-ZOdiv file), while div and mod are for Round-Toward-Bottom
(a.k.a Floor, what Coq does historically in Zdiv). We use unicode ÷
for quot, and infix rem for rem (which is actually remainder in
full). This way, both conventions can be used at the same time.
Definitions (and proofs of specifications) for div mod quot rem are
migrated in a new file Zdiv_def. Ex-ZOdiv file is now Zquot. With
this new organisation, no need for functor application in Zdiv and
Zquot.
On the abstract side, ZAxiomsSig now provides div mod quot rem.
Zproperties now contains properties of them. In NZDiv, we stop
splitting specifications in Common vs. Specific parts. Instead,
the NZ specification is be extended later, even if this leads to
a useless mod_bound_pos, subsumed by more precise axioms.
A few results in ZDivTrunc and ZDivFloor are improved (sgn stuff).
A few proofs in Nnat, Znat, Zabs are reworked (no more dependency
to Zmin, Zmax).
A lcm (least common multiple) is derived abstractly from gcd and
division (and hence available for nat N BigN Z BigZ :-).
In these new files NLcm and ZLcm, we also provide some combined
properties of div mod quot rem gcd.
We also provide a new file Zeuclid implementing a third division
convention, where the remainder is always positive. This file
instanciate the abstract one ZDivEucl. Operation names are
ZEuclid.div and ZEuclid.modulo.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13633 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
| |
We temporary use a hack to convert a module type into a module
Module M := T is refused, so we force an include via
Module M := Nop <+ T where Nop is an empty module.
To be fixed later more beautifully...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13602 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13294 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13293 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
| |
Contributed by Alexandre Ren, Damien Pous, and Thomas Braibant.
I've also included a MSets version, hence FSetPositive might become
soon a mere wrapper for MSetPositive, as for other FSets
implementations.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13287 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
|
| |
For the moment, almost no lemmas about (reflect P b), just the proofs
that it is equivalent with an P<->b=true.
is_true b is (b=true), and is meant to be added as a coercion
if one wants it. In the StdLib, this coercion is not globally
activated, but particular files are free to use Local Coercion...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13275 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
|
| |
- Many of them were broken, some of them after Pierre B's rework
of mli for ocamldoc, but not only (many bad annotation, many files
with no svn property about Id, etc)
- Useless for those of us that work with git-svn (and a fortiori
in a forthcoming git-only setting)
- Even in svn, they seem to be of little interest
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12972 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12772 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
|
| |
In interfaces fields like compare_spec, a CompSpec is prefered to get
nice extraction, but then no "destruct (compare_spec .. ..)" is
possible in a Type context. Now you can say there
"destruct (CompSpec2Type (compare_spec ... ...))"
This translate to the Type variant, and make the analysis on it
(which is equivalent to analysing the comparison directly).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12753 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12717 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12715 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12714 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
We use the <+ operation to regroup all known facts about BigN
(resp BigZ, ...) in a unique module. This uses also the new ! feature
for controling inlining. By the way, we also make sure that these
new BigN and BigZ modules implements OrderedTypeFull and TotalOrder,
and also contains facts about min and max (cf. GenericMinMax).
Side effects:
- In NSig and ZSig, specification of compare and eq_bool is now
done with respect to Zcompare and Zeq_bool, as for other ops.
The order <= and < are also defined via Zle and Zlt, instead
of using compare. Min and max are axiomatized instead of being
macros.
- Some proofs rework in QMake
- QOrderedType and Qminmax were in fact not compiled by make world
Still todo: OrderedType + MinMax for BigQ, etc etc
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12680 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12679 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12662 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12661 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
| |
Old stuff DecidableType.v and OrderedType.v stay there and keep their
names for the moment, for compatibility.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12641 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
| |
Syntax Include Type is still active, but deprecated, and triggers a warning.
The syntax M <+ M' <+ M'', which performs internally an Include, also
benefits from this: M, M', M'' can be independantly modules or module type.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12640 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
| |
without scope.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12639 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
| |
Leibniz part
Moreover, instantiation like MinMax are now made without redefining
generic properties (easier maintenance). We start using inner modules
for qualifying (e.g. Z.max_comm).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12638 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
| |
with Inline)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12636 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
OrderedType2
OrderedType2 is reorganized in atomic module type following the same approach used
for DecidableType2.
We use the following convention: module type Foo' is exactly module type Foo,
except that some notations may have been added. In functor arg, we can use
Foo or Foo' depending on whether we want nice notation or not. Note that any
implementation of Foo is accepted as implementation of Foo' :-). For the moment,
these notations are not placed in specific scopes, I think it isn't useful, but
I may be wrong, we'll see later when using them.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12635 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12634 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
| |
This used to be convenient in FSets, but since we now try to integrate
DecidableType and OrderedType as foundation for other part of the stdlib,
this should be avoided, otherwise some eauto take a _long_ time.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12626 85f007b7-540e-0410-9357-904b9bb8a0f7
|
Jason Gross
Pierre Letouzey
Hugo Herbelin
Matthieu Sozeau
letouzey
herbelin
msozeau
gareuselesinge
pboutill