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

chore(*): redefine {nat,int} mul based on a left-smul #6773

Closed
wants to merge 43 commits into from
Closed

chore(*): redefine {nat,int} mul based on a left-smul #6773

wants to merge 43 commits into from

Commits on Mar 8, 2021

  1. chore(*): nat.mul recurse on left

    @pechersky
    pechersky committed Mar 8, 2021
    Configuration menu
    Copy the full SHA
    a2722f4 View commit details
    Browse the repository at this point in the history

  2. cast_mul zero case

    @pechersky
    pechersky committed Mar 8, 2021
    Configuration menu
    Copy the full SHA
    da174c1 View commit details
    Browse the repository at this point in the history

  3. cast_mul succ case

    @pechersky
    pechersky committed Mar 8, 2021
    Configuration menu
    Copy the full SHA
    1c698c0 View commit details
    Browse the repository at this point in the history

Commits on Mar 9, 2021

  1. int proofs using try

    @pechersky
    pechersky committed Mar 9, 2021
    Configuration menu
    Copy the full SHA
    d8fa2fd View commit details
    Browse the repository at this point in the history

  2. avoid convert

    @pechersky
    pechersky committed Mar 9, 2021
    Configuration menu
    Copy the full SHA
    7f16140 View commit details
    Browse the repository at this point in the history

  3. no defeq for list.repeat

    @pechersky
    pechersky committed Mar 9, 2021
    Configuration menu
    Copy the full SHA
    6127472 View commit details
    Browse the repository at this point in the history

  4. make proofs agnostic to mul defn

    @pechersky
    pechersky committed Mar 9, 2021
    Configuration menu
    Copy the full SHA
    fc0c458 View commit details
    Browse the repository at this point in the history

Commits on Mar 12, 2021

  1. rework proofs to deal with new mul defns

    @pechersky
    pechersky committed Mar 12, 2021
    Configuration menu
    Copy the full SHA
    d20fc8e View commit details
    Browse the repository at this point in the history

  2. rephrase to make work with 3.27

    @pechersky
    pechersky committed Mar 12, 2021
    Configuration menu
    Copy the full SHA
    340fba2 View commit details
    Browse the repository at this point in the history

  3. satisfy linter

    @pechersky
    pechersky committed Mar 12, 2021
    Configuration menu
    Copy the full SHA
    ccbea4e View commit details
    Browse the repository at this point in the history

  4. redefine nsmul and gsmul

    @pechersky
    pechersky committed Mar 12, 2021
    Configuration menu
    Copy the full SHA
    cf77813 View commit details
    Browse the repository at this point in the history

  5. avoid referencing core smul directly

    @pechersky
    pechersky committed Mar 12, 2021
    Configuration menu
    Copy the full SHA
    3ffbf46 View commit details
    Browse the repository at this point in the history

  6. avoid rfl proof of nsmul_eq_mul to work with 3.27

    @pechersky
    pechersky committed Mar 12, 2021
    Configuration menu
    Copy the full SHA
    be8f6b1 View commit details
    Browse the repository at this point in the history

  7. avoid defeq in neg mod two

    @pechersky
    pechersky committed Mar 12, 2021
    Configuration menu
    Copy the full SHA
    8c1f897 View commit details
    Browse the repository at this point in the history

  8. avoid multiplicative proof

    @pechersky
    pechersky committed Mar 12, 2021
    Configuration menu
    Copy the full SHA
    d52631e View commit details
    Browse the repository at this point in the history

  9. remove some other multiplicative proofs

    @pechersky
    pechersky committed Mar 12, 2021
    Configuration menu
    Copy the full SHA
    d15198e View commit details
    Browse the repository at this point in the history

Commits on Mar 14, 2021

  1. fix subgroup multiplicative proof

    @pechersky
    pechersky committed Mar 14, 2021
    Configuration menu
    Copy the full SHA
    6a356b5 View commit details
    Browse the repository at this point in the history

  2. ditto deprecated

    @pechersky
    pechersky committed Mar 14, 2021
    Configuration menu
    Copy the full SHA
    5b5e841 View commit details
    Browse the repository at this point in the history

  3. finite ring proof

    @pechersky
    pechersky committed Mar 14, 2021
    Configuration menu
    Copy the full SHA
    80ad932 View commit details
    Browse the repository at this point in the history

Commits on Mar 15, 2021

  1. port gabriel's lemmas

    @pechersky
    pechersky committed Mar 15, 2021
    Configuration menu
    Copy the full SHA
    d5a1d03 View commit details
    Browse the repository at this point in the history

  2. remove defeq proof

    @pechersky
    pechersky committed Mar 15, 2021
    Configuration menu
    Copy the full SHA
    4f8db60 View commit details
    Browse the repository at this point in the history

Commits on Mar 16, 2021

  1. try toml change

    @pechersky
    pechersky committed Mar 16, 2021
    Configuration menu
    Copy the full SHA
    a17d6d7 View commit details
    Browse the repository at this point in the history

Commits on Mar 18, 2021

  1. Merge branch 'pechersky/mul-on-left' of https://github.com/leanprover… 

    …-community/mathlib into pechersky/mul-on-left
    @pechersky
    pechersky committed Mar 18, 2021
    Configuration menu
    Copy the full SHA
    79fa00b View commit details
    Browse the repository at this point in the history

  2. fix fpow

    @pechersky
    pechersky committed Mar 18, 2021
    Configuration menu
    Copy the full SHA
    3941ca0 View commit details
    Browse the repository at this point in the history

  3. fix zsqrtd

    @pechersky
    pechersky committed Mar 18, 2021
    Configuration menu
    Copy the full SHA
    2a04190 View commit details
    Browse the repository at this point in the history

Commits on Mar 19, 2021

  1. fix modeq

    @pechersky
    pechersky committed Mar 19, 2021
    Configuration menu
    Copy the full SHA
    07b812a View commit details
    Browse the repository at this point in the history

  2. fix sampleable dec_trivial proof 

    This is a little worrisome, in that dec_trivial no longer can tell that
the coercion of nat to int + 1 is still nonnegative.
    @pechersky
    pechersky committed Mar 19, 2021
    Configuration menu
    Copy the full SHA
    93e955d View commit details
    Browse the repository at this point in the history

  3. fix pell

    @pechersky
    pechersky committed Mar 19, 2021
    Configuration menu
    Copy the full SHA
    0775dac View commit details
    Browse the repository at this point in the history

  4. fix digits

    @pechersky
    pechersky committed Mar 19, 2021
    Configuration menu
    Copy the full SHA
    77d9391 View commit details
    Browse the repository at this point in the history

  5. fix dioph

    @pechersky
    pechersky committed Mar 19, 2021
    Configuration menu
    Copy the full SHA
    d60754f View commit details
    Browse the repository at this point in the history

  6. fix arithmetic function

    @pechersky
    pechersky committed Mar 19, 2021
    Configuration menu
    Copy the full SHA
    7b1e3ce View commit details
    Browse the repository at this point in the history

  7. fix gaussian_int

    @pechersky
    pechersky committed Mar 19, 2021
    Configuration menu
    Copy the full SHA
    105ae1b View commit details
    Browse the repository at this point in the history

  8. fix frobenius

    @pechersky
    pechersky committed Mar 19, 2021
    Configuration menu
    Copy the full SHA
    7f77577 View commit details
    Browse the repository at this point in the history

  9. remove try_for in norm_num test 

    Previously, there was a try_for to make sure the types check. But now
the type checking of the result times out, so to make the tests work,
the try_for is removed entirely. This should be investigated further.
But in any case, norm_num is able to discharge the goal, and the
kernel does not complain, so that must mean that the proof does
typecheck properly.
    @pechersky
    pechersky committed Mar 19, 2021
    Configuration menu
    Copy the full SHA
    8b9b65a View commit details
    Browse the repository at this point in the history

  10. fix decision_suf

    @pechersky
    pechersky committed Mar 19, 2021
    Configuration menu
    Copy the full SHA
    8ba9886 View commit details
    Browse the repository at this point in the history

  11. revert to rw; norm_cast

    @pechersky
    pechersky committed Mar 19, 2021
    Configuration menu
    Copy the full SHA
    99ef3a8 View commit details
    Browse the repository at this point in the history

  12. add explicit diamond test

    @pechersky
    pechersky committed Mar 19, 2021
    Configuration menu
    Copy the full SHA
    9950da1 View commit details
    Browse the repository at this point in the history

Commits on Mar 21, 2021

  1. update to pr511-3.28.0

    @pechersky
    pechersky committed Mar 21, 2021
    Configuration menu
    Copy the full SHA
    0e6b523 View commit details
    Browse the repository at this point in the history

  2. Merge branch 'master' into pechersky/mul-on-left

    @pechersky
    pechersky committed Mar 21, 2021
    Configuration menu
    Copy the full SHA
    94c8bac View commit details
    Browse the repository at this point in the history

  3. rephrase defeq proof

    @pechersky
    pechersky committed Mar 21, 2021
    Configuration menu
    Copy the full SHA
    7012488 View commit details
    Browse the repository at this point in the history

  4. rephrase additive proof

    @pechersky
    pechersky committed Mar 21, 2021
    Configuration menu
    Copy the full SHA
    ec33744 View commit details
    Browse the repository at this point in the history

  5. make ring happier by expanding succ to +1

    @pechersky
    pechersky committed Mar 21, 2021
    Configuration menu
    Copy the full SHA
    5d0c4a5 View commit details
    Browse the repository at this point in the history

Commits on Mar 22, 2021

  1. rephrase sim integral proof

    @pechersky
    pechersky committed Mar 22, 2021
    Configuration menu
    Copy the full SHA
    be87cbc View commit details
    Browse the repository at this point in the history