| Commit message (Collapse) | Author | Age |
|---|
| ... | |
| | |
|
| |
|
|
|
|
|
|
|
|
|
| |
I'm not quite sure why, but I'm pretty sure it's not. Rather, in
"allowing for foo" and "allowing to foo", "foo" modifies the sense in
which someting is allowed, rather than it being "foo" that's allowed.
"Allowing fooing" generally works, though it can sound a bit awkward.
"Allowing one to foo" (or "Allowing {him,her,it,Coq} to foo") is always
acceptable, in-as-much as it's ok to use "one".
I haven't touched the older instances of it in the CHANGES file.
|
| |
|
|
| |
"pat/term" for "apply term on current_hyp as pat".
|
| |
|
|
|
|
|
|
|
|
|
| |
integrate to "rewrite"?) with the code of "replace".
Incidentally, "inversion" relies on dependent rewrite, with an
incompatibility introduced. Left-to-right rewriting is now done with
"eq_rec_r" while before it was done using "eq_rec" of "eq_sym". The
first one reduces to the second one but simpl is not anymore able to
reduce "eq_rec_r eq_refl". Hopefully cbn is able to do it (see
Zdigits).
|
| |
|
|
| |
change of printing format of forall (need more thinking).
|
| |
|
|
|
|
|
|
|
|
| |
all the tactics using the constructor keyword in one entry. This has the
side-effect to also remove the other variant of constructor from the AST.
I also needed to hack around the "tauto" tactic to make it work, by
calling directly the ML tactic through a TacExtend node. This may be
generalized to get rid of the intermingled dependencies between this
tactic and the infamous Ltac quotation mechanism.
|
| | |
|
| |
|
|
| |
with possible further use of token "[]" + slight restructuration.
|
| | |
|
| |
|
|
|
|
|
|
|
|
| |
hypothesis when using it in apply or rewrite (prefix ">",
undocumented), and a modifier to explicitly keep it in induction or
destruct (prefix "!", reminiscent of non-linerarity).
Also added undocumented option "Set Default Clearing Used Hypotheses"
which makes apply and rewrite default to erasing the hypothesis they
use (if ever their argument is indeed an hypothesis of the context).
|
| | |
|
| |
|
|
| |
a dependent elimination principle for Prop arguments.
|
| |
|
|
|
|
|
| |
variables.
Simplifies instantiation of constants/inductives, requiring less allocation and Map.find's.
Abstraction by variables is handled mostly inside the kernel but could be moved outside.
|
| |
|
|
|
|
|
| |
This commit should be refactored by Pierre L. if he thinks this should
replace the previous version of fold_Equal, for now it is a different
lemma fold_Equal2. Same for the Section addded to SetoiList, it should
maybe replace the previous one.
|
| |
|
|
| |
Standard library now compiles fully.
|
| |
|
|
| |
Thanks to Arthur Azevedo de Amorim!
|
| |
|
|
| |
corresponding proof in ssreflect.
|
| |
|
|
| |
new files (WeakFan.v and WKL.v).
|
| |
|
|
|
| |
Renamed Fan.v into WeakFan.v since this was a proof of Weak Fan Theorem
after all.
|
| | |
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
- 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.
|
| | |
|
| |
|
|
|
| |
its universe doesn't get constrained unnecessarily (bug found in MathClasse).
Also avoid using rewrite itself in a proof in Morphisms.
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
|
|
|
| |
incompatibilities, at least until the check of compilation of contribs
succeeds more often.
Incidentally adapted some proofs in Reals which were not agnostic
relatively to whether the option is on or off.
|
| |
|
|
|
|
|
|
|
|
|
|
|
| |
for helping fixing this).
Now the issue is handled solely through refreshing of the terms assigned
to evars during unification.
If ?X = list ?Y, then Y's type is refreshed so that it doesn't mention
a template universe and in turn, ?X won't. Same goes when typechecking
(nil ?X, nil ?Y), the pair constructor levels will be set higher than fresh
universes for the lists carriers. This also handles user-defined functions
on template polymorphic inductives, which was fragile before.
Pretyping and Evd are now uncluttered from template-specific code.
|
| |
|
|
|
| |
induction/elim over a dependent elimination principle for Prop
arguments.
|
| |
|
|
|
| |
induction/elim over a dependent elimination principle for Prop
arguments.
|
| | |
|
| | |
|
| |
|
|
|
|
|
|
|
| |
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.
|
| | |
|
| |
|
|
| |
(refolding of cbn is smarter)
|
| |
|
|
|
|
|
|
|
| |
correctly when comparing stacks.
- Disallow Type i <= Prop/Set constraints, that would otherwise allow
constraints that make a universe lower than Prop.
- Fix stm/lemmas that was pushing constraints to the global context,
it is done depending on the constant/variable polymorphic status now.
- Adapt generalized rewriting in Type code to these fixes.
|
| | |
|
| |
|
|
| |
This reverts commit f3b3b6e4d01080da4f0ce37a06553769e9588d0e.
|
| |
|
|
| |
"coretactics.ml4" file.
|
| |
|
|
|
|
|
|
|
|
|
|
|
| |
corresponding Declare ML Module command. This changes essentially two
things:
1. ML plugins are forced to use the DECLARE PLUGIN statement before any
TACTIC EXTEND statement. The plugin name must be exactly the string passed to
the Declare ML Module command.
2. ML tactics are only made available after the Coq module that does the
corresponding Declare ML Module is imported. This may break a few things,
as it already broke quite some uses of omega in the stdlib.
|
| | |
|
| | |
|
| |
|
|
| |
answers #3299).
|
| | |
|
| |
|
|
|
|
|
|
|
| |
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.
|
| | |
|
| |
|
|
|
|
| |
- Enforce that no u <= Prop/Set can be added for u introduced by the user in Evd.process_constraints.
(Needs to be enforced in the kernel as well, but that's the main entry point).
- Fix a test-suite script and remove a regression comment, it's just as before now.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
- Remove Universe Polymorphism flags everywhere.
- Properly infer, discharge template arities and fix substitution inside them
(kernel code to check for correctness).
- Fix tactics that were supposing universe polymorphic constants/inductives to
be parametric on that status. Required to make interp_constr* return the whole evar
universe context now.
- Fix the univ/level/instance hashconsing to respect the fact that marshalling doesn't preserve sharing,
sadly losing most of its benefits.
Short-term solution is to add hashes to these for faster comparison, longer term requires rewriting
all serialization code.
Conflicts:
kernel/univ.ml
tactics/tactics.ml
theories/Logic/EqdepFacts.v
|
| | |
|
Jason Gross
Hugo Herbelin
Pierre-Marie Pédrot
Matthieu Sozeau
Pierre Courtieu
Maxime Dénès
Pierre Letouzey
Guillaume Melquiond
Matthieu Sozeau
Pierre Boutillier