Mapping for int_div, int_rem and bunch of other int notions #6
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
TheoWinterhalter
changed the title
TheoWinterhalter
changed the title
TheoWinterhalter
force-pushed
the
div
branch
2 times, most recently
from
732b937 to
bf3658e
Compare
Co-authored-by: Alessio Coltellacci <[email protected]>
Co-authored-by: Alessio Coltellacci <[email protected]>
Co-authored-by: Alessio Coltellacci <[email protected]>
TheoWinterhalter
force-pushed
the
div
branch
from
bf3658e to
5640847
Compare
|
Thank you @TheoWinterhalter ! |
fblanqui
reviewed
Feb 18, 2025
|
|
||
| Lemma int_lcm_def : | ||
| int_lcm = | ||
| (fun _30961 : prod Z Z => @COND Z ((Z.mul (@fst Z Z _30961) (@snd Z Z _30961)) = (Z_of_N (NUMERAL 0%N))) (Z_of_N (NUMERAL 0%N)) (Z.div (Z.abs (Z.mul (@fst Z Z _30961) (@snd Z Z _30961))) (int_gcd (@pair Z Z (@fst Z Z _30961) (@snd Z Z _30961))))). |
There was a problem hiding this comment.
Hi. In fact, there is a problem with this lemma as div is mapped above to Zdiv and not Z.div. What is the difference between these two functions? How to fix this lemma if one replaces Z.div by Zdiv?
There was a problem hiding this comment.
Solved in #9.
Closed
fblanqui
added a commit
to Deducteam/coq-hol-light-real-with-N
that referenced
this pull request
Feb 19, 2025
* add tactics developed by Théo (Deducteam/coq-hol-light#6) * structure proof scripts * add alignments of even, odd and WF * add alignment of factorial Co-authored-by: Théo Winterhalter <[email protected]> Co-authored-by: Frédéric Blanqui <[email protected]>
fblanqui
added a commit
that referenced
this pull request
Feb 20, 2025
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This PR proposes multiple alignments, mostly for integers, and sometimes for some real notions that are required as dependencies.
I also proved some util lemmas for
CONDand I don't know where to put them. Maybe the code should be refactored to use otherCONDlemmas instead.This PR also introduces some handy tactics such as
extto performapply fun_extfollowed byintroand a tacticalign_εto prove equalities where the RHS isεapplied to an arbitrary number of arguments, and getting rid of those that are useless like tags (then the proof doesn't have to even mention it).The work on
Z.lcmwas a collaboration with @NotBad4U.