| Age | Commit message (Collapse) | Author |
|---|
|
Reviewed-by: gares
Ack-by: herbelin
|
|
Reviewed-by: CohenCyril
Ack-by: Zimmi48
Ack-by: erikmd
Ack-by: gares
Ack-by: jfehrle
|
|
See also PR math-comp/math-comp#73
|
|
|
|
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.
|
|
|
|
In particular, this enhances support for lemma eq_big (with 2 side-conditions).
|
|
|
|
* Use ssr `by […|…]` and `apply:`
|
|
|
|
|
|
It was only required in the (not realistic) test case "test_over_2_2",
which happened to introduce evars after the context variables.
|
|
* "under"-specific behavior:
the order of goals is kept even if one issues
Global Set SsrOldRewriteGoalsOrder.
* href: https://github.com/math-comp/math-comp/blob/mathcomp-1.7.0/mathcomp/ssreflect/ssreflect.v
|
|
|
|
|
|
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
|
|
|
|
in the particular case where the side-condition is phrased
(_ : @eqfun bool I P1 P2)
instead of
(_ : forall x : I, P1 x = P2 x)
|
|
Supported syntax:
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 *)
Equivalent, expanded form:
under i: eq_bigr; [rewrite adnnC; over | idtac].
under i: eq_big; [rewrite adnnC; over | rewrite adnnC; over | idtac].
|
|
|
|
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>
|
|
Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Reviewed-by: ejgallego
Reviewed-by: gares
|
|
We make clearer which arguments are optional and which are mandatory.
Some of these representations are tricky because of small differences
between Program and Function, which share the same infrastructure.
As a side-effect of this cleanup, Program Fixpoint can now be used with
e.g. {measure (m + n) R}. Previously, parentheses were required around
R.
|
|
Not sure if the idetop.set_options was correctly changed, ocaml types
pass at least.
|
|
|
|
One other call still remains, but will require to refactor some
section-handling code.
|
|
|
|
|
|
Still to do: renaming the bound variables afterwards
|
|
(Note: coq notations cannot contain \n)
Co-authored-by: Enrico Tassi <Enrico.Tassi@inria.fr>
|
|
|
|
|
|
|
|
* If this flag under=true: enable flag with_evars of refine_with
to create evar(s) if the "under lemma" has non-inferable args.
* Backward compatibility of ssr rewrite is kept.
* Fix test-suite/ssr/dependent_type_err.v
|
|
Rather than integers '[0-9]+', numeral constant can now be parsed
according to the regexp '[0-9]+ ([.][0-9]+)? ([eE][+-]?[0-9]+)?'.
This can be used in one of the two following ways:
- using the function `Notation.register_rawnumeral_interpreter` in an OCaml plugin
- using `Numeral Notation` with the type `decimal` added to `Decimal.v`
See examples of each use case in the next two commits.
|
|
In anticipation of future uses of this token for non integer numerals.
|
|
|
|
|
|
|
|
Ack-by: gares
Ack-by: maximedenes
|
|
|
|
|
|
Eliminators can be:
- dependent: ... -> forall x (y : I x), P x y
- truncated: ... -> forall x (y : I x), P x
- funind like: ..-> forall x, P t
The user may provide a term t in `elim: t`
- t may be the last argument
- t may be the last "pattern" (standing for the last
argument of P)
We use unification to see if t (and its type) fits
in one of these cases (and/or to infer t).
This patch refuses to use unification in the HO case
eg `?T a = t` since the result is too often a false
positive.
|
