search

leanprover / lean4

Lean 4 programming language and theorem prover
https://lean-lang.org
Apache License 2.0
3.82k stars 325 forks source link

feat: lemmas to simplify equalities with `Option`-typed dependent if-then-else #4037

Closed wupr closed 1 week ago

wupr commented 2 weeks ago

Closes #4013.

Add dite_some_none_eq_none and dite_some_none_eq_some, analogous to the existing ite_some_none_eq_none and ite_some_none_eq_some.

leanprover-community-mathlib4-bot commented 2 weeks ago

Mathlib CI status (docs):

nomeata commented 2 weeks ago

Hmm, looks like this breaks mathlib, this might need diagnosing

wupr commented 2 weeks ago

It looks like the problem could be with the use of a non-final simp in Mathlib. But I think I need to merge the new commits in nightly-with-mathlib first.

wupr commented 2 weeks ago

The errors was thrown in Mathlib/Data/FinEnum.lean at the third line below:

instance Subtype.finEnum [FinEnum α] (p : α → Prop) [DecidablePred p] : FinEnum { x // p x } :=
  ofList ((toList α).filterMap fun x => if h : p x then some ⟨_, h⟩ else none)
    (by rintro ⟨x, h⟩; simp; exists x; simp [*])

But the proof can be simplified as follows now:

instance Subtype.finEnum [FinEnum α] (p : α → Prop) [DecidablePred p] : FinEnum { x // p x } :=
  ofList ((toList α).filterMap fun x => if h : p x then some ⟨_, h⟩ else none)
    (by simp)

There may be other problems like this and I'm trying to compile Mathlib locally to identify them.

Where should I push the fix? To the lean-pr-testing-4037 branch on Mathlib?

nomeata commented 2 weeks ago

Where should I push the fix? To the lean-pr-testing-4037 branch on Mathlib?

Exactly! Just keep pushing fixed until mathlib is happy, then we can see if the changes needed are benign

semorrison commented 1 week ago

Changes to Mathlib look fine, so lets proceed!