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

Arguments to definitions used in Experiments.Ed25519 vary with Coq versions #75

Closed
andres-erbsen opened this issue Oct 12, 2016 · 3 comments
Closed

Arguments to definitions used in Experiments.Ed25519 vary with Coq versions #75

andres-erbsen opened this issue Oct 12, 2016 · 3 comments
Assignees
@JasonGross @jadephilipoom

Comments

@andres-erbsen
Copy link
Contributor

The definitions and lemmas used (not defined) in Ed25519 take different arguments in different coq versions. I am guessing that this is similar to the issue we had with Shrink Obligations (discussed at
#57 and https://coq.inria.fr/bugs/show_bug.cgi?id=5044).
@JasonGross
Copy link
Collaborator

Here's one instance:

Quoting the changelog:

  • Tactic "tauto" was exceptionally able to destruct other connectives
    than the binary connectives "and", "or", "prod", "sum", "iff". This
    non-uniform behavior has been fixed (bug #2680) and tauto is
    slightly weaker (possible source of incompatibilities). On the
    opposite side, new tactic "dtauto" is able to destruct any
    record-like inductive types, superseding the old version of "tauto".

You had an Equivalence in the context that tauto was destructing, but otherwise not using. This made the proof pick up an extra dependency from the context in 8.4, but not 8.5/8.6.

JasonGross added a commit that referenced this issue Oct 17, 2016
@JasonGross
Don't let [tauto] destruct [Equivalence] in PE
4eddaa1 
This makes progress towards #75 (now src/Experiments/Ed25519.v builds
with both 8.4 and 8.5).

Quoting [the
changelog](https://github.com/coq/coq/blob/trunk/CHANGES#L576):
> - Tactic "tauto" was exceptionally able to destruct other connectives
  than the binary connectives "and", "or", "prod", "sum", "iff". This
  non-uniform behavior has been fixed (bug #2680) and tauto is
  slightly weaker (possible source of incompatibilities). On the
  opposite side, new tactic "dtauto" is able to destruct any
  record-like inductive types, superseding the old version of "tauto".

There was an `Equivalence` in the context that `tauto` was destructing,
but otherwise not using.  This made the proof pick up an extra
dependency from the context in 8.4, but not 8.5/8.6.
@JasonGross
Copy link
Collaborator

Another issue is exactly that of #57 (comment). I suggested removing the pose proof from bash, but it seems to still be there...

JasonGross added a commit that referenced this issue Oct 17, 2016
@JasonGross
Be more hesitant to [pose proof E.char_gt_2]
4b3b69e 
This makes progress towards #75, #57, and compatiblity between versions of Coq
@JasonGross
Copy link
Collaborator

Closed by 4b3b69e

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

@JasonGross JasonGross

@jadephilipoom jadephilipoom

Labels
None yet
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
3 participants
@JasonGross @andres-erbsen @jadephilipoom