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

[Merged by Bors] - chore(data/fin): succ_above defn compares fin terms instead of values #3999

Closed
wants to merge 54 commits into from
Closed

[Merged by Bors] - chore(data/fin): succ_above defn compares fin terms instead of values #3999

wants to merge 54 commits into from

Commits on Aug 13, 2020

  1. feat(data/fin, data/nat/basic): flesh out API for fin

    @pechersky
    pechersky committed Aug 13, 2020
    Configuration menu
    Copy the full SHA
    5e61dad View commit details
    Browse the repository at this point in the history

Commits on Aug 14, 2020

  1. Use lemma name as if not using proj notation 

    Co-authored-by: Shing Tak Lam <shingtaklam1324@gmail.com>
    @pechersky @shingtaklam1324
    pechersky and shingtaklam1324 committed Aug 14, 2020
    Configuration menu
    Copy the full SHA
    0cf4d64 View commit details
    Browse the repository at this point in the history

  2. Remove extra implicit arguments

    @pechersky
    pechersky committed Aug 14, 2020
    Configuration menu
    Copy the full SHA
    408e4c0 View commit details
    Browse the repository at this point in the history

Commits on Aug 16, 2020

  1. Remove simp, norm_cast attrs for coe_nat_eq_last 

    This change makes quadratic_reciprocity compile again, likely.
The lemma could probably have  norm_cast attr.
    @pechersky
    pechersky committed Aug 16, 2020
    Configuration menu
    Copy the full SHA
    28ded92 View commit details
    Browse the repository at this point in the history

  2. Remove added docstrings

    @pechersky
    pechersky committed Aug 16, 2020
    Configuration menu
    Copy the full SHA
    241da2d View commit details
    Browse the repository at this point in the history

  3. Remove simp attr from cons_val_zero' (linter)

    @pechersky
    pechersky committed Aug 16, 2020
    Configuration menu
    Copy the full SHA
    be70562 View commit details
    Browse the repository at this point in the history

  4. Additional lemmas on pred and succ_above

    @pechersky
    pechersky committed Aug 16, 2020
    Configuration menu
    Copy the full SHA
    1a422fe View commit details
    Browse the repository at this point in the history

  5. remove simp attr from succ_above_zero

    @pechersky
    pechersky committed Aug 16, 2020
    Configuration menu
    Copy the full SHA
    9f1dd9a View commit details
    Browse the repository at this point in the history

Commits on Aug 17, 2020

  1. Incorporate edits from rwbarton

    @pechersky
    pechersky committed Aug 17, 2020
    Configuration menu
    Copy the full SHA
    b11ffe5 View commit details
    Browse the repository at this point in the history

  2. Additional simp attr removal

    @pechersky
    pechersky committed Aug 17, 2020
    Configuration menu
    Copy the full SHA
    77f45fc View commit details
    Browse the repository at this point in the history

  3. Specify which zero_lt_one to use

    @pechersky
    pechersky committed Aug 17, 2020
    Configuration menu
    Copy the full SHA
    ec6378e View commit details
    Browse the repository at this point in the history

  4. Specifty nat.zero_lt_one

    @pechersky
    pechersky committed Aug 17, 2020
    Configuration menu
    Copy the full SHA
    6091c91 View commit details
    Browse the repository at this point in the history

  5. Simplify succ_pred proof

    @pechersky
    pechersky committed Aug 17, 2020
    Configuration menu
    Copy the full SHA
    014667b View commit details
    Browse the repository at this point in the history

  6. Remove nat succ_pred lemma

    @pechersky
    pechersky committed Aug 17, 2020
    Configuration menu
    Copy the full SHA
    9785138 View commit details
    Browse the repository at this point in the history

  7. ne to lt for cast_succ_lt_last

    @pechersky
    pechersky committed Aug 17, 2020
    Configuration menu
    Copy the full SHA
    eca7cea View commit details
    Browse the repository at this point in the history

  8. pred_one_add lemma

    @pechersky
    pechersky committed Aug 17, 2020
    Configuration menu
    Copy the full SHA
    fc90942 View commit details
    Browse the repository at this point in the history

Commits on Aug 18, 2020

  1. fix broken cast_succ_lt_lemmas

    @pechersky
    pechersky committed Aug 18, 2020
    Configuration menu
    Copy the full SHA
    a6584c7 View commit details
    Browse the repository at this point in the history

  2. lemmas on mk for zero and pred

    @pechersky
    pechersky committed Aug 18, 2020
    Configuration menu
    Copy the full SHA
    3530dcc View commit details
    Browse the repository at this point in the history

  3. fix squeeze_simp into simp only

    @pechersky
    pechersky committed Aug 18, 2020
    Configuration menu
    Copy the full SHA
    286629d View commit details
    Browse the repository at this point in the history

  4. fix use of cast_succ_ne_last to lt

    @pechersky
    pechersky committed Aug 18, 2020
    Configuration menu
    Copy the full SHA
    cc7df5a View commit details
    Browse the repository at this point in the history

  5. make pred_mk_succ have all explicit args

    @pechersky
    pechersky committed Aug 18, 2020
    Configuration menu
    Copy the full SHA
    ea7f18d View commit details
    Browse the repository at this point in the history

  6. add succ_above_pos

    @pechersky
    pechersky committed Aug 18, 2020
    Configuration menu
    Copy the full SHA
    87cd05a View commit details
    Browse the repository at this point in the history

  7. rename to prod_add_one

    @pechersky
    pechersky committed Aug 18, 2020
    Configuration menu
    Copy the full SHA
    6d13c3a View commit details
    Browse the repository at this point in the history

  8. rename zero_lt lemmas to _pos

    @pechersky
    pechersky committed Aug 18, 2020
    Configuration menu
    Copy the full SHA
    661f99a View commit details
    Browse the repository at this point in the history

  9. use fin_zero_elim over elim0

    @pechersky
    pechersky committed Aug 18, 2020
    Configuration menu
    Copy the full SHA
    b1e9978 View commit details
    Browse the repository at this point in the history

  10. undo zeoo typo

    @pechersky
    pechersky committed Aug 18, 2020
    Configuration menu
    Copy the full SHA
    d33e934 View commit details
    Browse the repository at this point in the history

Commits on Aug 19, 2020

  1. add succ_above_last

    @pechersky
    pechersky committed Aug 19, 2020
    Configuration menu
    Copy the full SHA
    26674ee View commit details
    Browse the repository at this point in the history

Commits on Aug 20, 2020

  1. simplify succ_above reduction lemmas

    @pechersky
    pechersky committed Aug 20, 2020
    Configuration menu
    Copy the full SHA
    0c1da94 View commit details
    Browse the repository at this point in the history

Commits on Aug 21, 2020

  1. incorporate sugg changes

    @pechersky
    pechersky committed Aug 21, 2020
    Configuration menu
    Copy the full SHA
    69854e7 View commit details
    Browse the repository at this point in the history

  2. fix broken succ_above_pos cases

    @pechersky
    pechersky committed Aug 21, 2020
    Configuration menu
    Copy the full SHA
    729463b View commit details
    Browse the repository at this point in the history

Commits on Aug 23, 2020

  1. simplify mk lemma names

    @pechersky
    pechersky committed Aug 23, 2020
    Configuration menu
    Copy the full SHA
    d65d786 View commit details
    Browse the repository at this point in the history

  2. mk bit0, bit1 lemmas 

    Co-authored by: Yury Kudryashov urkud@ya.ru
    @pechersky
    pechersky committed Aug 23, 2020
    Configuration menu
    Copy the full SHA
    005f2c8 View commit details
    Browse the repository at this point in the history

Commits on Aug 24, 2020

  1. cast_succ_lt_succ is valid on all fin n

    @pechersky
    pechersky committed Aug 24, 2020
    Configuration menu
    Copy the full SHA
    036e31e View commit details
    Browse the repository at this point in the history

  2. add helper zero_ne_one

    @pechersky
    pechersky committed Aug 24, 2020
    Configuration menu
    Copy the full SHA
    72c5c91 View commit details
    Browse the repository at this point in the history

  3. chore(data/fin): succ_above defn compares fin terms instead of values

    @pechersky
    pechersky committed Aug 24, 2020
    Configuration menu
    Copy the full SHA
    176fded View commit details
    Browse the repository at this point in the history

Commits on Aug 25, 2020

  1. add docstrings

    @pechersky
    pechersky committed Aug 25, 2020
    Configuration menu
    Copy the full SHA
    bc4245f View commit details
    Browse the repository at this point in the history

  2. succ_above about fixed pivot is injective

    @pechersky
    pechersky committed Aug 25, 2020
    Configuration menu
    Copy the full SHA
    297d27c View commit details
    Browse the repository at this point in the history

  3. docstrings on succ_above at pivot injectivity

    @pechersky
    pechersky committed Aug 25, 2020
    Configuration menu
    Copy the full SHA
    4cffe2f View commit details
    Browse the repository at this point in the history

  4. rearrange succ_above lt lemmas

    @pechersky
    pechersky committed Aug 25, 2020
    Configuration menu
    Copy the full SHA
    6c79aae View commit details
    Browse the repository at this point in the history

  5. injectivity lemmas about succ_above

    @pechersky
    pechersky committed Aug 25, 2020
    Configuration menu
    Copy the full SHA
    69b077d View commit details
    Browse the repository at this point in the history

  6. univ_succ_above

    @pechersky
    pechersky committed Aug 25, 2020
    Configuration menu
    Copy the full SHA
    06fa7a6 View commit details
    Browse the repository at this point in the history

  7. univ_succ_above prod and sum

    @pechersky
    pechersky committed Aug 25, 2020
    Configuration menu
    Copy the full SHA
    77ced3e View commit details
    Browse the repository at this point in the history

  8. simplify proof with or_iff_not

    @pechersky
    pechersky committed Aug 25, 2020
    Configuration menu
    Copy the full SHA
    e5dcfc2 View commit details
    Browse the repository at this point in the history

  9. univ_succ_above prod and sum docstrings

    @pechersky
    pechersky committed Aug 25, 2020
    Configuration menu
    Copy the full SHA
    1e33a3a View commit details
    Browse the repository at this point in the history

  10. simplify fin.prod and sum proofs using succ_above proofs

    @pechersky
    pechersky committed Aug 25, 2020
    Configuration menu
    Copy the full SHA
    ee0d3af View commit details
    Browse the repository at this point in the history

  11. prod_univ_zero and sum_univ_zero docstrings

    @pechersky
    pechersky committed Aug 25, 2020
    Configuration menu
    Copy the full SHA
    b4eab6c View commit details
    Browse the repository at this point in the history

  12. remove extra "the" in docstrings

    @pechersky
    pechersky committed Aug 25, 2020
    Configuration menu
    Copy the full SHA
    7c4feee View commit details
    Browse the repository at this point in the history

  13. fin.prod_univ and fin.sum_univ docstrings

    @pechersky
    pechersky committed Aug 25, 2020
    Configuration menu
    Copy the full SHA
    0a2f98f View commit details
    Browse the repository at this point in the history

  14. spacing and prefer n + 1 over n.succ

    @pechersky
    pechersky committed Aug 25, 2020
    Configuration menu
    Copy the full SHA
    d68f6e7 View commit details
    Browse the repository at this point in the history

  15. typo fix

    @pechersky
    pechersky committed Aug 25, 2020
    Configuration menu
    Copy the full SHA
    e1f4fa0 View commit details
    Browse the repository at this point in the history

Commits on Aug 31, 2020

  1. Merge branch 'master' into succ-above-redef

    @pechersky
    pechersky committed Aug 31, 2020
    Configuration menu
    Copy the full SHA
    3338708 View commit details
    Browse the repository at this point in the history

Commits on Sep 1, 2020

  1. change injectivity lemma names 

    Co-authored by: Bryan Gin-ge Chen bryangingechen@gmail.com
    @pechersky
    pechersky committed Sep 1, 2020
    Configuration menu
    Copy the full SHA
    f7ef1b0 View commit details
    Browse the repository at this point in the history

  2. replace inj lemma name

    @pechersky
    pechersky committed Sep 1, 2020
    Configuration menu
    Copy the full SHA
    e36283b View commit details
    Browse the repository at this point in the history

  3. rename injectivity lemmas

    @pechersky
    pechersky committed Sep 1, 2020
    Configuration menu
    Copy the full SHA
    7c9067c View commit details
    Browse the repository at this point in the history