[Merged by Bors] - feat(logic/basic): Add forall_apply_eq_imp_iff #4109

eric-wieser · 2020-09-11T09:41:15Z

Also adds forall_apply_eq_imp_iff' for swapped forall arguments

This means that forall_range_iff can now be solved by simp.

This requires changes in data/pfun and measure_theory/borel_space, where non-terminal simps broke.

Discussed at https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Should.20.60set.2Eforall_range_iff.60.20be.20taged.20.60simp.60.3F

jcommelin · 2020-09-11T11:14:01Z

LGTM, let's see if the simp linter is happy with this.

jcommelin · 2020-09-11T11:44:56Z

@eric-wieser CI doesn't like this 😢
It's up to you whether you want to fix mathlib or abandon this PR.

eric-wieser · 2020-09-11T12:10:09Z

src/data/set/basic.lean

+@[simp] theorem forall_range_iff {p : α → Prop} : (∀ a ∈ range f, p a) ↔ (∀ i, p (f i)) :=
 ⟨assume h i, h (f i) (mem_range_self _), assume h a ⟨i, (hi : f i = a)⟩, hi ▸ h i⟩


I think I can fix this with

Suggested change

@[simp] theorem forall_range_iff {p : α → Prop} : (∀ a ∈ range f, p a) ↔ (∀ i, p (f i)) :=

⟨assume h i, h (f i) (mem_range_self _), assume h a ⟨i, (hi : f i = a)⟩, hi ▸ h i⟩

@[simp] theorem forall_range_iff_aux {p : α → Prop} : (∀ a i, f i = a → p a) ↔ (∀ i, p (f i)) :=

⟨assume h i, h (f i) i rfl, assume h a i hi, hi ▸ h i⟩

theorem forall_range_iff {p : α → Prop} : (∀ a ∈ range f, p a) ↔ (∀ i, p (f i)) :=

by simp

What would be a better name for forall_range_iff_aux?

The best I can come up with is forall_apply_eq_imp_iff. And it certainly is a good simp lemma 😀

If if helps, parts of it look like forall_eq', and the lemma used to prove exists_range_iff is exists_exists_eq_and.

I'm also happy with forall_range_iff'. Whatever you want.

Alright, added using your suggested name.

Also adds forall_apply_eq_imp_iff' for swapped forall arguments

jcommelin · 2020-09-11T13:34:23Z

src/logic/basic.lean

+  (∀ a, ∀ b, f a = b → p b) ↔ (∀ a, p (f a)) :=
+⟨λ h i, h i (f i) rfl, λ h i a hi, hi ▸ h i⟩
+
+@[simp] theorem forall_apply_eq_imp_iff' {f : α → β} {p : β → Prop} :


I guess it's less likely to show up, but b = f a could also be a pattern: forall_eq_apply_iff?
Do you want to add those?

Feel free to merge if the linter is happy

bors d+

Tempting, yeah. Is there a way for me to run the simp linter without waiting for a full mathlib build? The CI is taking a very long time on this PR, thanks to touching such low-level files I guess.

You can (temporarily) add #lint at the bottom of the file, but it's not completely foolproof since simp lemmas in later files may change what the simp normal form is. I guess that's not likely for stuff in logic.basic though.

Given how slow the build was for this one, I think I'll come back and add the reversed-equality lemmas in a follow-up PR.

bors · 2020-09-11T13:34:33Z

✌️ eric-wieser can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

eric-wieser · 2020-09-11T13:52:38Z

src/logic/basic.lean

-by simp [@eq_comm _ a']
+@[simp] theorem forall_apply_eq_imp_iff {f : α → β} {p : β → Prop} :
+  (∀ a, ∀ b, f a = b → p b) ↔ (∀ a, p (f a)) :=
+⟨λ h a, h a (f a) rfl, λ h a b hab, hab ▸ h a⟩


Would by tidy be better or worse here?

Worse, but I'm almost certain that tactic.tidy depends on this file anyways.

eric-wieser · 2020-09-11T13:58:36Z

src/data/pfun.lean

@@ -612,11 +612,7 @@ rel.core_inter _ s t

 lemma mem_core_res (f : α → β) (s : set α) (t : set β) (x : α) :
  x ∈ core (res f s) t ↔ (x ∈ s → f x ∈ t) :=
-begin
-  simp [mem_core, mem_res], split,


Non-terminal simp is to blame here, but I suppose writing it this way lead to the proof being removable which is a good thing

eric-wieser · 2020-09-11T15:03:13Z

More non-terminal simp breaking CI

bryangingechen · 2020-09-11T15:07:55Z

More non-terminal simp breaking CI

Yep, seems worth fixing.

eric-wieser · 2020-09-11T15:16:19Z

src/measure_theory/borel_space.lean

+  { simp only [mem_range, exists_imp_distrib, forall_apply_eq_imp_iff'],
+    intro a,
    exact generate_measurable.basic _ is_open_Iio }


I assume this is a reasonable fix, since I don't think I can rewrite this to put the simp last.

Nevermind, I can eliminate this simp entirely

…nal simp

eric-wieser · 2020-09-11T16:43:33Z

bors r+

bors · 2020-09-11T16:43:35Z

👎 Rejected by label

eric-wieser · 2020-09-11T16:44:47Z

@jcommelin: Can I remove your changes requested label?

bryangingechen · 2020-09-11T16:45:35Z

@jcommelin: Can I remove your changes requested label?

Yes, and in the future feel free to do so without asking.

bors r+

Also adds forall_apply_eq_imp_iff' for swapped forall arguments This means that `forall_range_iff` can now be solved by `simp`. This requires changes in data/pfun and measure_theory/borel_space, where non-terminal `simp`s broke.

bors · 2020-09-11T19:46:26Z

Pull request successfully merged into master.

Build succeeded:

eric-wieser marked this pull request as ready for review September 11, 2020 11:00

eric-wieser added the awaiting-review The author would like community review of the PR label Sep 11, 2020

jcommelin changed the title ~~chore(data/set/basic): Mark forall_range_iff and exist_range_iff with simp~~ chore(data/set/basic): tag forall_range_iff and exist_range_iff with simp Sep 11, 2020

eric-wieser requested a review from jcommelin September 11, 2020 11:04

jcommelin added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review The author would like community review of the PR labels Sep 11, 2020

eric-wieser commented Sep 11, 2020

View reviewed changes

eric-wieser added 2 commits September 11, 2020 14:31

chore(logic/basic): Move the forall_eq lemmas to be adjacent

408a59f

feat(logic/basic): Add forall_apply_eq_imp_iff

527e736

Also adds forall_apply_eq_imp_iff' for swapped forall arguments

jcommelin approved these changes Sep 11, 2020

View reviewed changes

chore(data/set/basic): Use the new simp lemma

5316a2d

eric-wieser force-pushed the eric-wieser/simp-range branch from 19dea2f to 5316a2d Compare September 11, 2020 13:37

eric-wieser commented Sep 11, 2020

View reviewed changes

chore(data/pfun): Removes proofs handled by non-terminal simp

85aae1d

eric-wieser commented Sep 11, 2020

View reviewed changes

eric-wieser changed the title ~~chore(data/set/basic): tag forall_range_iff and exist_range_iff with simp~~ feat(logic/basic): Add forall_apply_eq_imp_iff Sep 11, 2020

eric-wieser commented Sep 11, 2020

View reviewed changes

chore(measure_theory/borel_space): Correct proofs broken by non-termi…

dcdd822

…nal simp

eric-wieser force-pushed the eric-wieser/simp-range branch from d2c12d8 to dcdd822 Compare September 11, 2020 15:29

bryangingechen removed the awaiting-author A reviewer has asked the author a question or requested changes label Sep 11, 2020

github-actions bot added the ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) label Sep 11, 2020

bors bot changed the title ~~feat(logic/basic): Add forall_apply_eq_imp_iff~~ [Merged by Bors] - feat(logic/basic): Add forall_apply_eq_imp_iff Sep 11, 2020

bors bot closed this Sep 11, 2020

bors bot deleted the eric-wieser/simp-range branch September 11, 2020 19:46

eric-wieser mentioned this pull request Sep 14, 2020

[Merged by Bors] - feat(logic/basic): Add more simp lemmas for forall #4117

Closed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - feat(logic/basic): Add forall_apply_eq_imp_iff #4109

[Merged by Bors] - feat(logic/basic): Add forall_apply_eq_imp_iff #4109

eric-wieser commented Sep 11, 2020 •

edited

jcommelin commented Sep 11, 2020

jcommelin commented Sep 11, 2020

eric-wieser Sep 11, 2020

jcommelin Sep 11, 2020

eric-wieser Sep 11, 2020

jcommelin Sep 11, 2020

eric-wieser Sep 11, 2020

jcommelin Sep 11, 2020

eric-wieser Sep 11, 2020

bryangingechen Sep 11, 2020 •

edited

eric-wieser Sep 11, 2020

bors bot commented Sep 11, 2020

eric-wieser Sep 11, 2020

bryangingechen Sep 11, 2020 •

edited

eric-wieser Sep 11, 2020

eric-wieser commented Sep 11, 2020

bryangingechen commented Sep 11, 2020

eric-wieser Sep 11, 2020

eric-wieser Sep 11, 2020 •

edited

eric-wieser commented Sep 11, 2020

bors bot commented Sep 11, 2020

eric-wieser commented Sep 11, 2020

bryangingechen commented Sep 11, 2020

bors bot commented Sep 11, 2020

		@[simp] theorem forall_range_iff {p : α → Prop} : (∀ a ∈ range f, p a) ↔ (∀ i, p (f i)) :=
		⟨assume h i, h (f i) (mem_range_self _), assume h a ⟨i, (hi : f i = a)⟩, hi ▸ h i⟩

[Merged by Bors] - feat(logic/basic): Add forall_apply_eq_imp_iff #4109

[Merged by Bors] - feat(logic/basic): Add forall_apply_eq_imp_iff #4109

Conversation

eric-wieser commented Sep 11, 2020 • edited

jcommelin commented Sep 11, 2020

jcommelin commented Sep 11, 2020

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

bryangingechen Sep 11, 2020 • edited

Choose a reason for hiding this comment

Choose a reason for hiding this comment

bors bot commented Sep 11, 2020

Choose a reason for hiding this comment

bryangingechen Sep 11, 2020 • edited

Choose a reason for hiding this comment

Choose a reason for hiding this comment

eric-wieser commented Sep 11, 2020

bryangingechen commented Sep 11, 2020

Choose a reason for hiding this comment

eric-wieser Sep 11, 2020 • edited

Choose a reason for hiding this comment

eric-wieser commented Sep 11, 2020

bors bot commented Sep 11, 2020

eric-wieser commented Sep 11, 2020

bryangingechen commented Sep 11, 2020

bors bot commented Sep 11, 2020

eric-wieser commented Sep 11, 2020 •

edited

bryangingechen Sep 11, 2020 •

edited

bryangingechen Sep 11, 2020 •

edited

eric-wieser Sep 11, 2020 •

edited