mathlib4

mathlib4 copied to clipboard

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

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

@urkud I don't know if transitivity is meant to be a stub for something different. Can someone who knows clarify?

I have cases of @[symm] and @[trans] in the test files. Do you mean also in the mathlib4 code?

The transitivity tactic in Mathlib.Tactic.Basic is indeed meant to be subsumed by your trans tactic, but make sure to add some tests of the transitivity tactic and ensure that they still work with trans.

The transitivity tactic in Mathlib.Tactic.Basic is indeed meant to be subsumed by your trans tactic, but make sure to add some tests of the transitivity tactic and ensure that they still work with trans.

~I have used a macro to map this and added a few tests. Sorry, I created a mistake as transitivity was used in Init~

The transitivity tactic in Mathlib.Tactic.Basic is indeed meant to be subsumed by your trans tactic, but make sure to add some tests of the transitivity tactic and ensure that they still work with trans.

I made a mess earlier, but have addressed this correctly I hope now. There is a single use of transitivity in the codebase and I copied the example and checked that trans works instead.

@gebner just want to clarify that so far as I see I have addressed the comments. Should the "awaiting-author" tag be removed.

Yes, in the code. BTW, what lemmas does lean4 calc mode use? In lean 3 we had one attribute that was used both for calc and trans. In lean 3, the tactic transitivity uses trans lemmas.

When you want another round of review, you remove awaiting author and add awaiting review.

When you want another round of review, you remove awaiting author and add awaiting review.

I don't seem to be able to do this. Maybe only maintainers can.

Yes, in the code. BTW, what lemmas does lean4 calc mode use? In lean 3 we had one attribute that was used both for calc and trans. In lean 3, the tactic transitivity uses trans lemmas.

There is a typeclass Trans. This is picked up by the trans tactic I implemented in addition to attributes.

To fix the main import linting error you can run

/usr/bin/find Mathlib -name "*.lean" | LC_ALL=C sort | sed 's/\.lean//;s,/,.,g;s/^/import /' > Mathlib.lean

in the mathlib root dir

To fix the main import linting error you can run

/usr/bin/find Mathlib -name "*.lean" | LC_ALL=C sort | sed 's/\.lean//;s,/,.,g;s/^/import /' > Mathlib.lean

in the mathlib root dir

Thanks. Done this.

Can this tactic rewrite hypotheses? symm at h ? I tried it but doesn't seem to like it. I believe the symmetry tactic could do that.

bors merge

Build failed:

• Lint style

bors merge

Build failed:

• Build

bors merge

Build failed:

• Build

bors merge

Canceled.

bors merge

Build failed (retrying...):

• Build

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style