Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Coq 8.4, 8.5, 8.6 : issues with ssrpattern and ssrpatternarg(pat) #62

Closed
3 tasks
erikmd opened this issue Sep 1, 2016 · 5 comments
Closed
3 tasks

Coq 8.4, 8.5, 8.6 : issues with ssrpattern and ssrpatternarg(pat) #62

erikmd opened this issue Sep 1, 2016 · 5 comments
Assignees
@gares
Labels
kind: bug Issue which describe bugs

Comments

@erikmd
Copy link
Member

erikmd commented Sep 1, 2016 •
edited

Hello,
I've experimented the ssrpattern tactic with MathComp for Coq 8.4, 8.5, and 8.6, and I believe that the behavior/syntax of this tactic is not uniform across the versions of SSReflect.

EDIT: Below is an update of my report that relies on MathComp 1.6.1 for Coq 8.5 and 8.6.
Here is my setup:

  • OCaml 4.02.3, Coq 8.5pl2, MathComp 1.6.1
  • OCaml 4.02.3, Coq 8.6, MathComp 1.6.1

My report relies on the following test file:

Require Import mathcomp.ssreflect.ssreflect mathcomp.ssreflect.seq.
(* 1 *) From mathcomp (* ONLY FOR Coq 8.5 *)
Require Import ssrmatching.
(* 2 *) Declare ML Module "ssreflect". (* ONLY FOR Coq 8.5, cf. issue #61 *)
Tactic Notation "ssrpat" ssrpatternarg(pat) := ssrpattern pat.
Tactic Notation "ssrrew" ssrpatternarg(pat) :=
  rewrite [pat](eq_from_nth (x0 := 0) (s2 := [:: 99])).

Goal [::] = [::] :> list nat.
(* 3 *) ssrpattern RHS.

Goal [::] = [::] :> list nat.
(* 4 *) ssrpat RHS.

Goal [::] = [::] :> list nat.
(* 5 *) ssrrew RHS.

Goal [::] = [::] :> list nat.
(* 6 *) ssrpattern (X in _ = X).

Goal [::] = [::] :> list nat.
(* 7 *) ssrpat (X in _ = X).

Goal [::] = [::] :> list nat.
(* 8 *) ssrrew (X in _ = X).

Here is the summary of what I obtained:

  • Coq 8.6: everything compiles, if one removes Line 1 and Line 2 (which is a workaround for Coq 8.5).
  • Coq 8.5:
    • Line 3 raises "Error: RHS is bound to a notation that does not denote a reference."
    • Line 5 raises "Error: variable pat should be bound to a term."
    • Lines 6, 7, 8 raise "Error: Unknown interpretation for notation "( _ in _ )"."

Best,
Erik
@erikmd erikmd mentioned this issue Nov 29, 2016
Closed
@gares gares self-assigned this Jan 19, 2017
@gares gares added the kind: bug Issue which describe bugs label Jan 19, 2017
@gares gares added this to the 1.7 milestone Jan 19, 2017
@gares
Copy link
Member

gares commented Jan 19, 2017

Needs to be reviewed since 1.6.1 should have aligned 8.5 and 8.6 on the syntax of ssrpattern

@gares gares mentioned this issue Jan 19, 2017
Closed
@erikmd
Copy link
Member Author

erikmd commented Jan 19, 2017

Hi @gares, indeed I have to retest this with MathComp 1.6.1... I'm going to do this ASAP. Kind regards.

@erikmd
Copy link
Member Author

erikmd commented Feb 4, 2017

Hi @gares, sorry for the delay of my reply.
I have installed MathComp 1.6.1 with both Coq 8.5pl2 and Coq 8.6 and I confirm that there is still some issue regarding ssrpattern and/or ssrpatternarg for Coq 8.5.
I have just edited the description of this issue for updating my test cases.
Best regards.

@erikmd erikmd mentioned this issue Oct 18, 2017
Closed
@erikmd
Copy link
Member Author

erikmd commented Nov 13, 2017

Hi @gares
FYI this issue is still reproducible with Coq 8.5.3 and MathComp 1.6.4

@erikmd erikmd mentioned this issue Nov 14, 2017
Merged
erikmd added a commit to validsdp/validsdp that referenced this issue Apr 1, 2018
@erikmd
New version of bigop_tactics.v.
7f6919c 
Summary:
- Add tactic support for eq_bigl (for rewriting bigop predicates).
- Add a shortcut: big := bigop _ _ _.
- Rephrase the tactic notations.
  Before:
    underbig (bigop _ _ _) i Hi rewrite lem.
  Now:
    under big i Hi rewrite lem.
- Improve the Ltac tactics so the bigop variable ("i" or so) is kept,
  if specified.

Note: this file correspond to the first commit of repo
erikmd/ssr-under-tac@e2aeee0

Since then it has been significantly improved thanks to Cyril Cohen's
advice, but the latest version of my tactic only work with the
development version of MathComp, which contains a few bugs related to
the ssrpattern tactic. As soon as both issues
math-comp/math-comp#61 and
math-comp/math-comp#62 are resolved, I will
submit a PR for integrating https://github.com/erikmd/ssr-under-tac in
MathComp (and upgrade validsdp accordingly).
@gares gares removed this from the 1.7 milestone Apr 17, 2018
@CohenCyril
Copy link
Member

None of the versions of Coq mentioned in the title are supported by math-comp anymore. Feel free to reopen the issue if needed.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@gares gares

Labels
kind: bug Issue which describe bugs
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
3 participants
@CohenCyril @gares @erikmd