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

trans tactic does not use HEq.trans #1119

Closed
semorrison opened this issue Dec 20, 2022 · 2 comments
Closed

trans tactic does not use HEq.trans #1119

semorrison opened this issue Dec 20, 2022 · 2 comments
Assignees
@siddhartha-gadgil

Comments

@semorrison
Copy link
Contributor

See example in Mathlib.CategoryTheory.Functor.FullyFaithful.
@semorrison semorrison mentioned this issue Dec 20, 2022
Closed
bors bot pushed a commit that referenced this issue Dec 20, 2022
@rosborn @semorrison @mpenciak
feat: port CategoryTheory.Functor.FullyFaithful (#846)
bf9d289 
mathlib SHA: 70d50ecfd4900dd6d328da39ab7ebd516abe4025

Porting notes:
1. ~~`aesop_cat` was unable to close goals that `tidy` was able to. I left an example proof of what `tidy` emits (with some cleanup).~~
2. `unfold_projs` is not ported. Is it an easy tactic to port over or is there a better "lean4" way? (ed: not needed)
3. `trans` doesn't seem to work with `HEq` (see #1119)
4. Some documentation is needed for `Full` and `Faithful`. Please feel free to fill it in if you wish.

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Co-authored-by: mpenciak <matej.penciak@gmail.com>
@siddhartha-gadgil
Copy link
Collaborator

This was my mistake in assuming types equal in transitivity and using a single relation r. Should model on the Trans class and assume separate relations. Will try to fix.

@siddhartha-gadgil
Copy link
Collaborator

It looks like trans needs serious repairs. Will work on it.

@siddhartha-gadgil siddhartha-gadgil self-assigned this Dec 20, 2022
siddhartha-gadgil added a commit that referenced this issue Dec 20, 2022
@siddhartha-gadgil
improved transitivity, handles HEq ref trans tactic does not use `HEq…
58ce984 
….trans` #1119
@siddhartha-gadgil siddhartha-gadgil mentioned this issue Dec 20, 2022
Closed
@bors bors bot closed this as completed in 047ae09 Dec 21, 2022
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@siddhartha-gadgil siddhartha-gadgil

Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

[Merged by Bors] - fix: improved transitivity, handles HEq.trans leanprover-community/mathlib4
2 participants
@semorrison @siddhartha-gadgil