| Age | Commit message (Collapse) | Author |
|---|
|
specification
Ack-by: Zimmi48
Ack-by: herbelin
Ack-by: maximedenes
Ack-by: proux01
Reviewed-by: vbgl
|
|
|
|
frequently on CI.
Reviewed-by: vbgl
|
|
Ack-by: JasonGross
Reviewed-by: gares
Reviewed-by: ppedrot
Reviewed-by: jfehrle
Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Reviewed-by: ejgallego
|
|
Since Ltac2 cannot be put under the stdlib logical root (some file names
would clash), we move it to the `user-contrib` directory, to avoid adding
another hardcoded path in `coqinit.ml`, following a suggestion by @ejgallego.
Thanks to @Zimmi48 for the thorough documentation review and the
numerous suggestions.
|
|
Reviewed-by: ppedrot
|
|
as assumptions
Ack-by: RalfJung
Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Ack-by: maximedenes
Reviewed-by: ppedrot
Ack-by: robbertkrebbers
|
|
(Merge of the initial version with #9983 was broken)
|
|
There are three implementations of this primitive:
* one in OCaml on 63 bits integer in kernel/uint63_amd64.ml
* one in OCaml on Int64 in kernel/uint63_x86.ml
* one in C on unsigned 64 bit integers in kernel/byterun/coq_uint63_native.h
Its specification is the axiom `diveucl_21_spec` in
theories/Numbers/Cyclic/Int63/Int63.v
* comment the implementations with loop invariants to enable an easy
pen&paper proof of correctness (note to reviewers: the one in
uint63_amd64.ml might be the easiest to read)
* make sure the three implementations are equivalent
* fix the specification in Int63.v
(only the lowest part of the result is actually returned)
* make a little optimisation in div21 enabled by the proof of correctness
(cmp is computed at the end of the first loop rather than at the beginning,
potentially saving one loop iteration while remaining correct)
* update the proofs in Int63.v and Cyclic63.v to take into account the
new specifiation of div21
* add a test
|
|
We add a fast path when generalizing over variables.
|
|
Ack-by: Zimmi48
Ack-by: herbelin
Reviewed-by: ppedrot
|
|
|
|
Reviewed-by: ejgallego
|
|
|
|
`nonPropType` interface
Ack-by: SkySkimmer
Reviewed-by: gares
Ack-by: ggonthier
|
|
|
|
Ack-by: SkySkimmer
Reviewed-by: maximedenes
Ack-by: ppedrot
|
|
** Changed definition of `simpl_rel` to `T -> `simpl_pred T`, so that
`inE` will now expand `a \in r b`, when `r := [rel x y | R]` to `R{b/x,
a/y}`, as the expanding coercion is now only inserted in the _last_
application.
The old definition made it possible to have a `simpl_rel >-> rel`
coercion that does not block expansion, but this can now be achieved
more economically with the `Arguments … /.` annotation.
** Deleted the `[rel of P]` notation which is no longer needed with
the new `simpl_rel` definition, and was broken anyway.
** Added `relpre f R` definition of functional preimage of a notation.
** `comp` and `idfun` are now proper definitions, using the `Arguments
… /.` annotation to specify simplification on application.
** Added `{pred T}` syntax for the alias of `pred T` in the `pred_sort`
coercion class; deleted the `pred_class` alias: one should either
use `pred_sort` in `Coercion` declarations, or `{pred T}` in type casts.
Used `{pred T}` as appropriate in localised predicate (`{in …, …}`) theory.
Extended and corrected `pred` coercion internal documentation.
** Simplified the `predType` structure by removing the redundant
explicit `mem_pred` subfield, and replacing it with an interlocked
projection; deleted `mkPredType`, now replaced by `PredType`.
** Added (and extensively documented) a `nonPropType` interface
matching types that do _not_ have sort `Prop`, and used it to remove
the non-standard maximal implicits annotation on `Some_inj` introduced
in #6911 by @anton-trumov; included `test-suite` entry for `nonPropType`.
** Documented the design of the four structures used to control the
matching of `inE` and related predicate rewriting lemmas; added `test-suite`
entry covering the `pred` rewriting control idioms.
** Used `only printing` annotations to get rid of token concatenation
hacks.
** Fixed boolean and general `if b return t then …` notation so that
`b` is bound in `t`. This is a minor source of incompatibility for
misuses of this syntax when `b` is _not_ bound in `t`, and `(if b then
…) : t` should have been used instead.
** Reserved all `ssreflect`, `ssrfun` and `ssrbool` notation at the top
of the file, adding some printing boxes, and removing some spurious
`[pred .. => ..]` reserved notation.
** Fixed parsing precedence and format of `<hidden n>` notation, and
declared and put it in an explicit `ssr_scope`.
** Used module-and-functor idiom to ensure that the `simpl_pred T >-
pred T` _and_ `simpl_pred T >-> {pred T}` coercions are realised by the
_same_ Gallina constant.
** Updated `CREDITS`.
The policy implied by this PR: that `{pred T}` should systematically
be used as the generic collective predicate type, was implemented in MathComp
math-comp/math-comp#237. As a result `simpl_pred >-> pred_sort` coercions
became more frequent, as it turned out they were not, as incorrectly stated
in `ssrbool` internal comments, impossible: while the `simplPredType`
canonical instance does solve all `simpl_pred T =~= pred_sort ?pT`
instances, it does _not_ solve `simpl_pred T =~= {pred T}`, and so the
coercion will be used in that case. However it appeared that having two
different coercion constants confused the SSReflect keyed matching
heuristic, hence the fix introduced here. This has entailed some
rearrangement of `ssrbool`: the large `Predicates` section had to be
broken up as the module-functor idiom for aliasing coercions cannot be
used inside a section.
|
|
Reviewed-by: maximedenes
|
|
|
|
|
|
Reviewed-by: CohenCyril
Ack-by: Zimmi48
Ack-by: erikmd
Ack-by: gares
Ack-by: jfehrle
|
|
|
|
|
|
|
|
|
|
|
|
So if the underlying tactic "contains a ;" one should actually write:
under eq_bigl => i do [rewrite andb_idl; first by move/eqP->].
|
|
so it acts "more naturally" like (under eq_bigl; [hnf|]); move=> [*|].
Also: replace "by over." in the doc example with "over."
|
|
as suggested by @gares, and:
* Rename some Under_* terms for better uniformity;
* Update & Improve minor details in the documentation.
|
|
* Add tests accordingly.
|
|
|
|
|
|
Ack-by: JasonGross
Ack-by: erikmd
Reviewed-by: maximedenes
Ack-by: proux01
|
|
|
|
It was only required in the (not realistic) test case "test_over_2_2",
which happened to introduce evars after the context variables.
|
|
As a result, the following:
under i: eq_bigr by rewrite adnnC. (* ensure 1 Under subogal is created *)
under i: eq_big by [rewrite adnnC | rewrite addnC]. (* 2 Under subgoals *)
amounts to:
under i: eq_bigr; [rewrite adnnC; over | cbv beta iota].
under i: eq_big; [rewrite adnnC; over | rewrite adnnC; over | cbv beta iota].
|
|
|
|
|
|
* Rely on a new tactic unify_helper that workarounds the fact
[apply Under.under_done] cannot unify (?G i...) with (expr i...) in
[|- @Under T (expr i...) (?G i...)]
when expr is a constant expression, or has more than one var (i...).
Idea: massage the expression with Ltac to obtain a beta redex.
* Simplify test-suite/ssr/under.v by using TestSuite.ssr_mini_mathcomp
and add a test-case [test_big_andb].
* Summary of commands to quickly test [under]:
$ cd .../coq
$ make plugins/ssr/ssreflect.vo plugins/ssr/ssrfun.vo plugins/ssr/ssrbool.vo
$ cd test-suite
$ touch prerequisite/ssr_mini_mathcomp.v
$ make
$ emacs under.v
|
|
|
|
Both can be use to close the "under goals", in rewrite style or in
closing-tactic style.
Contrarily to the previous implementation that assumed
"over : forall (T : Type) (x : T), @Under T x x <-> True"
this new design won't require the Setoid library.
Extend the test-suite (in test-suite/ssr/under.v)
|
|
Rename the bound variables of the last (lambda) argument of the redex
w.r.t. the varnames specified by the user.
Co-authored-by: Erik Martin-Dorel <erik.martin-dorel@irit.fr>
|
|
Reviewed-by: gares
|
|
Previsouly, it was silently ignored.
|
|
|
|
|
|
projections
Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Ack-by: maximedenes
Reviewed-by: ppedrot
|
|
Async causes output reordering in one test. Since we don't care about
the output of that test (it's just a [Fail]) we move it to success/.
|
|
A scope delimiter was missing for primitive integers constants.
Add related regression tests.
|
