Equations 1.3beta1 for Coq 8.13

Equations 1.3

This is a new major release of Equations, working with Coq 8.13. This version adds an improved syntax (less ;-separation), integration with the Coq-HoTT library and numerous bug fixes. See the reference manual for details.

This version introduces minor breaking changes along with the following features:

• Improved syntax for "concise" clauses separated by |, at top-level or inside with subprograms.
  We no longer require to separate them by ;. For example, the following definition is now accepted:

  Equations foo : nat -> nat := 
    | 0 => 1
    | S n => S (foo n).

  The old syntax is however still supported for backwards compatibility.
• Multiple patterns can be separated by , in addition to |, as in:

  Equations trans {A} {x y z : A} (e : x = y) (e' : y = z) : x = z := | 1, 1 => 1.

• Require Import Equations.Equations. does not work anymore.
  One has to use Require Import Equations.Prop.Equations to load the plugin's default instance where equality is in Prop. From Equations Require Import Equations is unaffected.
• Use Require Import Equations.HoTT.All to use the HoTT variant of the library compatible with the Coq HoTT library
  The plugin then reuses the definition of paths from the HoTT library and all its constructions are universe polymorphic. As for the HoTT library alone, coq must be passed the arguments -noinit -indices-matter to use the library and plugin. The coq-equations opam package depends optionally on coq-hott, so if coq-hott is installed before it, coq-equations will automatically install the HoTT library variant in addition to the standard one. This variant of Equations allows to write very concise dependent pattern-matchings on equality:

  Require Import Equations.HoTT.All.
  Equations sym {A} {x y : A} (e : x = y) : y = x := | 1 => 1.

• New attribute #[tactic=tac] to set locally the default tactic to solve remaining holes.
  The goals on which the tactic applies are now always of the form Γ |- τ where Γ is the context where the hole was introduced and τ the expected type, even when using the Obligation machinery to solve them, resulting in a possible incompatibility if the obligation tactic treated the context differently than the conclusion. By default, the program_simpl tactic performs a simpl call before introducing the hypotheses, so you might need to add a simpl in * to your tactics.
• New attributes #[derive(equations=yes,no, eliminator=yes|no)] can be used in place of the (noeqns, noind) flags which are deprecated.

Fixed in this version:

∗ #329: improved strengthening avoiding to abstract over recursive definitions which would not pass the guardness checker. This can simplify the produced terms, avoiding unnecessary "commutative cuts".
∗ #321: warn rather than error when using Equations? and no subgoals are left. This will leave a proof state with no subgoals, that must be closed using a Qed or Defined (similarly to Coq’s #[refine] Instance command).
∗ #372, #194: funelim applied to a partial application failing
∗ #354: support for building values in SProp
∗ #353: name capture problem in presence of modules
∗ #335: provide an alias Equations Derive to not conflict with QuickChick’s Derive
∗ #325: properly inline all Equations helper constants during Extraction

Equations 1.2.4 for Coq 8.13

This is a bugfix release of version 1.2 working with Coq 8.13, 8.12 and 8.11
See https://mattam82.github.io/Coq-Equations/equations/2019/05/17/1.2.html for the 1.2 release notes.
Fixed in this version:

• Fixed issues #228, #306 and #349 where functional elimination proofs were failing for no good reason. The tactic is now more robust and proves more unfolding lemmas without relying on functional extensionality (e.g. when no higher-order recursion is involved). It also generates smaller proof terms.
• Fix conflicting grammar extension that declared "-!" as a token, conflicting with with ssr's rewrite syntax in particular. Now Equations also defines its potentially conflicting notations (for patterns, sigma-times etc) in an EquationsNotations module that does not have to be imported to make the plugin work (however the default is still to export them when Require Import Equations for compatibility and ease of use).
• Fix issue #346: Derive not working when the inductive type's sort is hidden under a constant.

Equations 1.2.4 for Coq 8.12

This is a bugfix release of version 1.2 working with Coq 8.13, 8.12 and 8.11
See https://mattam82.github.io/Coq-Equations/equations/2019/05/17/1.2.html for the 1.2 release notes.
Fixed in this version:

• Fixed issues #228, #306 and #349 where functional elimination proofs were failing for no good reason. The tactic is now more robust and proves more unfolding lemmas without relying on functional extensionality (e.g. when no higher-order recursion is involved). It also generates smaller proof terms.
• Fix conflicting grammar extension that declared "-!" as a token, conflicting with with ssr's rewrite syntax in particular. Now Equations also defines its potentially conflicting notations (for patterns, sigma-times etc) in an EquationsNotations module that does not have to be imported to make the plugin work (however the default is still to export them when Require Import Equations for compatibility and ease of use).
• Fix issue #346: Derive not working when the inductive type's sort is hidden under a constant.

Equations 1.2.4 for Coq 8.11

This is a bugfix release of version 1.2 working with Coq 8.13, 8.12 and 8.11
See https://mattam82.github.io/Coq-Equations/equations/2019/05/17/1.2.html for the 1.2 release notes.
Fixed in this version:

• Fixed issues #228, #306 and #349 where functional elimination proofs were failing for no good reason. The tactic is now more robust and proves more unfolding lemmas without relying on functional extensionality (e.g. when no higher-order recursion is involved). It also generates smaller proof terms.
• Fix conflicting grammar extension that declared "-!" as a token, conflicting with with ssr's rewrite syntax in particular. Now Equations also defines its potentially conflicting notations (for patterns, sigma-times etc) in an EquationsNotations module that does not have to be imported to make the plugin work (however the default is still to export them when Require Import Equations for compatibility and ease of use).
• Fix issue #346: Derive not working when the inductive type's sort is hidden under a constant.

Equations 1.2.3 for Coq 8.13

This is a bugfix release of version 1.2 working with Coq 8.13+beta1
See https://mattam82.github.io/Coq-Equations/equations/2019/05/17/1.2.html for the 1.2 release notes.
New in this version:

• Fixed issue #297: dependent elimination simplification mistreated let-bindings
• Fixed issue #295: discrepancy between the syntax in the manual and the implementation
• Ensure that NoConfusion is derived before EqDec as it is necessary to solve the corresponding obligation.

Equations 1.2.3 for Coq 8.12

This is a bugfix release of version 1.2 working with Coq 8.12.0
See https://mattam82.github.io/Coq-Equations/equations/2019/05/17/1.2.html for the 1.2 release notes.
New in this version:

• Fixed issue #297: dependent elimination simplification mistreated let-bindings
• Fixed issue #295: discrepancy between the syntax in the manual and the implementation
• Ensure that NoConfusion is derived before EqDec as it is necessary to solve the corresponding obligation.

Equations 1.2.3 for Coq 8.11

This is a bugfix release of version 1.2 working with Coq 8.11
See https://mattam82.github.io/Coq-Equations/equations/2019/05/17/1.2.html for the 1.2 release notes.
New in this version:

• Fixed issue #297: dependent elimination simplification mistreated let-bindings
• Fixed issue #295: discrepancy between the syntax in the manual and the implementation
• Ensure that NoConfusion is derived before EqDec as it is necessary to solve the corresponding obligation.

Equations 1.2.2 for Coq 8.12

This is a bugfix release of version 1.2 working with Coq 8.12 (beta1 for now).
The bug fixes in the depind and depelim are potential sources of incompatibility.
See https://mattam82.github.io/Coq-Equations/equations/2019/05/17/1.2.html for the 1.2 release notes.
New in this version:

• Fixed issue #286 : allow let-ins in constructors
• Fixed issue #246: derive subterm for inductives with non-uniform parameters. Also force the user to derive NoConfusion before Subterm, as required for the well-foundedness proof of the Subterm relation. Report an error when the user tries to derive the subterm relation on propositional inductive types (this is impossible).
• PR #285: depelim and noconf were not working up-to simplification of equations. Potential source of incompatibility
• PR #283: depelim and depind no longer simplify unrelated equations in the goal (this was making some subgoals unprovable in some cases). Potential source of incompatibility
• PR #281: add an example of the inspect pattern in the documentation (by Yves Bertot).
• Fixed issue #256: derive eliminators of well-founded definitions in presence of lets in the body.
• Fixed issue #273: derivation of the eliminator was launched too eagerly depending on the order the obligations of a definition were solved.
• Fixed deprecations in OCaml and .v files w.r.t. Coq 8.12

Equations 1.2.2 for Coq 8.11

This is a bugfix release of version 1.2 working with Coq 8.11.
The bug fixes in the depind and depelim tactics are potential sources of incompatibility.
See https://mattam82.github.io/Coq-Equations/equations/2019/05/17/1.2.html for the 1.2 release notes.
New in this version:

• Fixed issue #286 : allow let-ins in constructors
• Fixed issue #246: derive subterm for inductives with non-uniform parameters. Also force the user to derive NoConfusion before Subterm, as required for the well-foundedness proof of the Subterm relation. Report an error when the user tries to derive the subterm relation on propositional inductive types (this is impossible).
• PR #285: depelim and noconf were not working up-to simplification of equations. Potential source of incompatibility
• PR #283: depelim and depind no longer simplify unrelated equations in the goal (this was making some subgoals unprovable in some cases). Potential source of incompatibility
• PR #281: add an example of the inspect pattern in the documentation (by Yves Bertot).
• Fixed issue #256: derive eliminators of well-founded definitions in presence of lets in the body.
• Fixed issue #273: derivation of the eliminator was launched too eagerly depending on the order the obligations of a definition were solved.
• Fixed deprecations in OCaml and .v files w.r.t. Coq 8.11

Equations 1.2.1 for Coq 8.11

This release has all the features of 1.2.1 working for Coq 8.11.
See https://mattam82.github.io/Coq-Equations/equations/2019/05/17/1.2.html for the 1.2 release notes.