[Merged by Bors] - feat: `symm` and `trans` tactics#253

Closed

siddhartha-gadgil wants to merge 42 commits intoleanprover-community:masterfrom

siddhartha-gadgil:symm

Collaborator

siddhartha-gadgil commented Mar 28, 2022

I have implemented a symm tactic, using annotations for symm rules. This follows (including using code from) the ext implementation.

I also have a couple of test examples

siddhartha-gadgil added 6 commits

March 28, 2022 17:19


          symm tactic: implementation and first examples

2eb455a


          removed duplicate "symmAttr"

c66dc8c


          Add import

f9f0a0f


          Merge branch 'master' of https://github.com/leanprover-community/math…

8147d48

…lib4 into symm


          transitivity tactic implemented

c715ef5


          Merge branch 'master' of https://github.com/leanprover-community/math…

a4fef62

…lib4 into symm

siddhartha-gadgil changed the title ~~WIP: symm tactic: implementation and first examples~~ Symmetry and Transitivity tactics: implementations and first examples

siddhartha-gadgil added 5 commits

April 5, 2022 18:52


          allowing middle parameter, but erratic matching

b7c7b50


          Trans added to filename

d160690


          transitivity picking up a parameter

bb66c05


          typeclass used correctly

a1f0af8


          Merge branch 'master' of https://github.com/leanprover-community/math…

b70b088

…lib4 into symm

siddhartha-gadgil changed the title ~~Symmetry and Transitivity tactics: implementations and first examples~~ feat: symmetry and rransitivity tactics: implementations and first examples

siddhartha-gadgil changed the title ~~feat: symmetry and rransitivity tactics: implementations and first examples~~ feat: symm and trans tactics

siddhartha-gadgil added 4 commits

June 4, 2022 10:10


          Merge branch 'master' into symm

0e37364


          more concide examples


          Merge branch 'master' into symm

c7b0633


          Updation for symm

1b60e4f

EdAyers reviewed

View reviewed changes

Mathlib/Mathport/Syntax.lean Show resolved Hide resolved

Mathlib/Tactic/Symm.lean Outdated Show resolved Hide resolved

Mathlib/Tactic/Trans.lean Outdated Show resolved Hide resolved

kbuzzard reviewed

View reviewed changes

test/trans.lean Outdated Show resolved Hide resolved

test/trans.lean Outdated Show resolved Hide resolved

test/trans.lean Outdated Show resolved Hide resolved

test/trans.lean Outdated Show resolved Hide resolved

Kha reviewed

View reviewed changes

Mathlib/Tactic/Symm.lean Outdated Show resolved Hide resolved

gebner reviewed

View reviewed changes

Mathlib/Tactic/Trans.lean Outdated Show resolved Hide resolved

gebner reviewed

View reviewed changes

Mathlib/Tactic/Trans.lean Outdated Show resolved Hide resolved

Member

urkud commented Jul 18, 2022

There is a stub transitivity in Tactic.Basic. Probably, it should be removed. Also, could you please mark some lemmas as @[symm]/@[trans]?

siddhartha-gadgil and others added 6 commits

July 18, 2022 20:17


          removed symm, trans

f178cbd


          Update test/trans.lean

b805c7d

Co-authored-by: Kevin Buzzard <k.buzzard@imperial.ac.uk>


          Update test/trans.lean

Co-authored-by: Kevin Buzzard <k.buzzard@imperial.ac.uk>


          Update test/trans.lean

f73f213

Co-authored-by: Kevin Buzzard <k.buzzard@imperial.ac.uk>


          added docstring removed redundant stuff


          using elab syntax

3b2cc25

siddhartha-gadgil and others added 3 commits

October 15, 2022 13:06


          Merge branch 'master' of https://github.com/leanprover-community/math…

031820b

…lib4 into symm


          Merge remote-tracking branch 'origin/master' into symm

03a21ef


          feat: add symm at h, cleanup symm/trans

f69adf6

Member

digama0 commented Oct 22, 2022

bors merge

bors bot pushed a commit that referenced this pull request


          feat: symm and trans tactics (#253)

ee3ccc4

I have implemented a symm tactic, using annotations for symm rules. This follows (including using code from) the ext implementation.

I also have a couple of test examples

bors bot commented Oct 22, 2022

Build failed:

Lint style

Member

digama0 commented Oct 22, 2022

bors merge

bors bot pushed a commit that referenced this pull request


          feat: symm and trans tactics (#253)

8fa1a63

I have implemented a symm tactic, using annotations for symm rules. This follows (including using code from) the ext implementation.

I also have a couple of test examples

bors bot commented Oct 22, 2022

Build failed:

Build

Member

digama0 commented Oct 22, 2022

bors merge

bors bot pushed a commit that referenced this pull request


          feat: symm and trans tactics (#253)

929d20b

I have implemented a symm tactic, using annotations for symm rules. This follows (including using code from) the ext implementation.

I also have a couple of test examples

bors bot commented Oct 22, 2022

Build failed:

Build

digama0 force-pushed the symm branch from 1318c7d to a215b0c Compare

October 22, 2022 16:16

Member

digama0 commented Oct 22, 2022

bors merge

bors bot pushed a commit that referenced this pull request


          feat: symm and trans tactics (#253)

87d6290

I have implemented a symm tactic, using annotations for symm rules. This follows (including using code from) the ext implementation.

I also have a couple of test examples


          move symm/trans to Mathlib.Tactic.Relation

2b09d73

digama0 force-pushed the symm branch from a215b0c to 2b09d73 Compare

October 22, 2022 16:21

bors bot commented Oct 22, 2022

Canceled.

Member

digama0 commented Oct 22, 2022

bors merge

bors bot pushed a commit that referenced this pull request


          feat: symm and trans tactics (#253)

480a321

I have implemented a symm tactic, using annotations for symm rules. This follows (including using code from) the ext implementation.

I also have a couple of test examples

bors bot commented Oct 22, 2022

Build failed (retrying...):

Build

bors bot pushed a commit that referenced this pull request


          feat: symm and trans tactics (#253)

5ad3946

I have implemented a symm tactic, using annotations for symm rules. This follows (including using code from) the ext implementation.

I also have a couple of test examples

bors bot commented Oct 22, 2022

Pull request successfully merged into master.

Build succeeded:

bors bot changed the title ~~feat: symm and trans tactics~~ [Merged by Bors] - feat: symm and trans tactics

bors bot closed this

kim-em mentioned this pull request

[Merged by Bors] - feat: align init.{core, logic} #490

Closed

kim-em added a commit that referenced this pull request


          chore: bump Std to #253

372eb12

bors bot pushed a commit that referenced this pull request


          chore: bump Std to #253 (#7113)

e0540ea

Bump PR for leanprover-community/batteries#253



Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

bors bot pushed a commit that referenced this pull request


          chore: bump Std to #253 (#7113)

d0e5669

Bump PR for leanprover-community/batteries#253



Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

kodyvajjha pushed a commit that referenced this pull request


          chore: bump Std to #253 (#7113)

e745087

Bump PR for leanprover-community/batteries#253



Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

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

Reviewers

gebner gebner left review comments

digama0 digama0 left review comments

kbuzzard kbuzzard left review comments

+2 more reviewers

Kha Kha left review comments

EdAyers EdAyers left review comments

Labels

None yet