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

feat(Mathlib/Tactic/finCases): Port fin_cases #346

Closed
wants to merge 6 commits into from
Closed

feat(Mathlib/Tactic/finCases): Port fin_cases #346

wants to merge 6 commits into from

Conversation

winston-h-zhang
Copy link
Collaborator

@winston-h-zhang winston-h-zhang commented Jul 25, 2022 •
edited

This PR implements fin_cases from mathlib3. It largely follows the original idea behind Scott's code. There are a few notable details for this PR

  • To have fin_casess full functionality, we must port Fintype/Finset/Multiset. I've tried my best to only use the minimal number of dependencies, but right now it feels very messy. Is there a standard way of organizing this?
  • cases_core doesn't exist and I don't know how to recreate the API. There's an extremely hacky section that needs to be fixed.

winston-h-zhang
winston-h-zhang commented Jul 25, 2022
View reviewed changes
Mathlib/Tactic/finCases.lean Outdated
Comment on lines 35 to 43
liftMetaTacticAux fun mvarId => do
let rec loop (goal : MVarId) (hyp : FVarId) (cont : Array MVarId) := do
try
let #[g₁, g₂] ← cases goal hyp |
throwError "'cases' tactic failed, unexpected number of subgoals"
loop g₂.mvarId g₂.fields[3]!.fvarId! (cont.push g₁.mvarId)
catch _ =>
return cont
return ((), Array.toList <|← loop mvarId hyp #[])
Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This feels like a gigantic hack. Is there a way recursively apply cases and capture the subgoals in a list nicely?

winston-h-zhang
winston-h-zhang commented Jul 25, 2022
View reviewed changes
Mathlib/Tactic/finCases.lean Outdated
Comment on lines 45 to 56
-- Deal with `x : A`, where `[Fintype A]` is available:
let inst ← synthInstance (← mkAppM ``Fintype #[lDecl.type])
let elems ← mkAppOptM ``Fintype.elems #[lDecl.type, inst]
let t ← mkAppM ``Membership.mem #[lDecl.toExpr, elems]
let v ← mkAppOptM ``Fintype.complete #[lDecl.type, inst, lDecl.toExpr]

let hyp ← liftMetaTacticAux fun mvarId => do
let (fvar, mvarId) ← intro1P (← assert mvarId `this t v)
pure (fvar, [mvarId])

withMainContext do
finCasesAt hyp
Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This seems like it works, but are there any footguns I should be careful about?

@winston-h-zhang winston-h-zhang self-assigned this Jul 25, 2022
@winston-h-zhang winston-h-zhang added the help-wanted The author needs attention to resolve issues label Jul 25, 2022
@digama0
Copy link
Member

digama0 commented Jul 25, 2022

Please separate out the porting parts of this PR into its own PR.

digama0
digama0 reviewed Jul 25, 2022
View reviewed changes
Mathlib/Data/List/Basic.lean
@@ -882,7 +883,7 @@ theorem erasep_append_right :
| (x::xs), l₂, h => by
simp [(forall_mem_cons.1 h).1, erasep_append_right _ (forall_mem_cons.1 h).2]

-- theorem erasep_sublist (l : List α) : l.erasep p <+ l :=
-- theorem erasep_subList (l : List α) : l.erasep p <+ l :=
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

s/subList/sublist/, this is an actual word

digama0
digama0 reviewed Jul 25, 2022
View reviewed changes
Mathlib/Data/List/Basic.lean
@@ -1168,7 +1169,7 @@ end union
cases l₁ <;> simp [List.inter, mem_filter]

/--
List.prod satisfies a specification of cartesian product on lists.
List.prod satisfies a specification of cartesian product on Lists.
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
List.prod satisfies a specification of cartesian product on Lists.
List.prod satisfies a specification of cartesian product on lists.

@digama0
Copy link
Member

digama0 commented Jul 25, 2022

For porting, you should be using https://github.com/leanprover-community/mathlib3port, not https://github.com/leanprover-community/mathlib directly. This will save you a lot of trouble fixing lean 3 syntax stuff, and will save us trouble when we later have to diff these files against the automatically ported files when new theorems are added to mathlib and/or we get around to porting these files for real.

@dwrensha dwrensha mentioned this pull request Jul 26, 2022
Closed
dwrensha
dwrensha reviewed Jul 26, 2022
View reviewed changes
Mathlib/Data/List/Chain.lean
· sorry
· sorry
-- hb.Pairwise.cons begin
-- simp only [mem_cons_iff, forall_eq_or_imp, h, true_and]
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I opened #350 to add these missing lemmas.

bors bot pushed a commit that referenced this pull request Aug 9, 2022
@dwrensha
port some lemmas for use in fin_cases (#350)
148380a 
Ports [`mem_cons_iff`](https://github.com/leanprover-community/lean/blob/3526539070ea6268df5dd373deeb3ac8b9621952/library/init/data/list/lemmas.lean#L100-L101) and [`forall_eq_or_imp`](https://github.com/leanprover-community/mathlib/blob/8edffc250c25db5a7bada5472dd02a166f7f8bfc/src/logic/basic.lean#L1135-L1137), to be used in the proof of `Chain.Pairwise` in #346.
EdAyers pushed a commit that referenced this pull request Aug 18, 2022
@dwrensha @EdAyers
port some lemmas for use in fin_cases (#350)
7cb5b36 
Ports [`mem_cons_iff`](https://github.com/leanprover-community/lean/blob/3526539070ea6268df5dd373deeb3ac8b9621952/library/init/data/list/lemmas.lean#L100-L101) and [`forall_eq_or_imp`](https://github.com/leanprover-community/mathlib/blob/8edffc250c25db5a7bada5472dd02a166f7f8bfc/src/logic/basic.lean#L1135-L1137), to be used in the proof of `Chain.Pairwise` in #346.
@semorrison
Copy link
Contributor

@winston-h-zhang, would it be okay if I started some work on this port? My plan would be

  1. Port a minimal version of fin_cases that only deals with List A hypotheses. This will get most of the logic of the tactic sorted out, but not need any material on Finset and Multiset ported.
  2. In parallel, port as little as possible of Finset and Multiset from mathlib3port.
  3. Once those are both done, make fin_cases do everything.

I would probably just start a new branch, but make use of some of your code from here (appropriately credited, of course :-).

This was referenced Sep 19, 2022
Closed
Open
bors bot pushed a commit that referenced this pull request Sep 23, 2022
@semorrison @digama0
feat: minimal port of Fintype (#429)
492d30e 
This is a bare minimum port of the definitions of `Finset` / `Multiset` / `Fintype`. I am hoping that these are enough to port the `fin_cases` tactic. (i.e. replacing the unfinished work in #346, which still had sorries in the corresponding material)

Where possible I have started by copying and pasting the output from `mathlib3port`.



Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Co-authored-by: Mario Carneiro <di.gama@gmail.com>
@semorrison
Copy link
Contributor

Made redundant by #437.

@semorrison semorrison closed this Sep 23, 2022
@int-y1 int-y1 deleted the hz/fin_cases branch April 16, 2023 18:21
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@semorrison semorrison semorrison left review comments

@dwrensha dwrensha dwrensha left review comments

@digama0 digama0 digama0 left review comments

Assignees

@winston-h-zhang winston-h-zhang

Labels
help-wanted The author needs attention to resolve issues
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
4 participants
@winston-h-zhang @digama0 @semorrison @dwrensha