or_iff_or

Stream: general

[Kevin Buzzard]

@Scott Morrison can you use your magic to tell me whether

example (a b c d : Prop) (h1 : a ↔ c) (h2 : b ↔ d) : a ∨ b ↔ c ∨ d :=
⟨λ hab, or.elim hab (λ ha, or.inl $ h1.1 ha) $ λ hb, or.inr $ h2.1 hb,
 λ hcd, or.elim hcd (λ hc, or.inl $ h1.2 hc) $ λ hd, or.inr $ h2.2 hd⟩

is already in mathlib? Are we yet in a position where I can find this out for myself? Note that I secretly find writing proofs of these things rather satisfying, so no hurry ;-)

[Mario Carneiro]

hint: it's a congr lemma

[Sebastien Gouezel]

lemma foo (a b c d : Prop) (h1 : a ↔ c) (h2 : b ↔ d) : a ∨ b ↔ c ∨ d :=
by library_search
-- exact or_congr h1 h2

[Sebastien Gouezel]

By the way, library_search does not work well for me when I work in advanced files (too much theorems in the environment, I guess, leading to timeouts). But I have created a file search.lean importing only basic stuff, in which I launch library_search when I need it. And it is super-efficient. Thanks @Scott Morrison !

[Kevin Buzzard]

def or_iff_or {a b c d : Prop} (h1 : a ↔ c) (h2 : b ↔ d) : a ∨ b ↔ c ∨ d :=
by rw [h1, h2]

Aww. The by hand version is far more fun :-)

[Kevin Buzzard]

hint: it's a congr lemma

I see. So I was looking in the wrong place. What does congr mean?

theorem ball_congr (H : ∀ x h, P x h ↔ Q x h) :
  (∀ x h, P x h) ↔ (∀ x h, Q x h) :=

This seems to say that bounded forall "distributes over iff" (can one even say that?) Does "congr" means "it distributes over iff"

[Patrick Massot]

By the way, library_search does not work well for me when I work in advanced files (too much theorems in the environment, I guess, leading to timeouts). But I have created a file search.lean importing only basic stuff, in which I launch library_search when I need it. And it is super-efficient. Thanks Scott Morrison !

The next step is to improve the VScode extension to get a shortcut open a small window where you can type the statement and hit "search" to launch library_search on your search.lean. Who wants to learn TypeScript?

[Kevin Buzzard]

@Sebastien Gouezel can you share search.lean as a gist? Or just post it here?

[Patrick Massot]

foo_congr means that if x = y then foo x = foo y or some variation on that.

[Kevin Buzzard]

For predicates it seems to me that if foo (P iff Q) then foo P iff foo Q which seems to be a bit different.

[Kevin Buzzard]

Do I just have to close my eyes a bit and squint?

[Sebastien Gouezel]

It's just an empty file in which I import only what should be relevant for the search (and I keep changing the imports depending on what I want). So no interest in posting it. What you really need to do is merge #839 in your local copy of mathlib (or merge it in mathlib if you are an admin, to bring it to everyone :).

[Kevin Buzzard]

Oh I see, you change the imports to suit.

[Kevin Buzzard]

Are these proofs mathlib-ready or can they be golfed more?

import data.equiv.basic algebra.order

def equiv.lt_map_of_le_map {α : Type*} {β : Type*} [preorder α] [preorder β]
  (he : α ≃ β) (hle : ∀ x y, x ≤ y ↔ he x ≤ he y) : (∀ x y, x < y ↔ he x < he y) :=
λ x y, by rw [lt_iff_le_not_le, hle x y, hle y x, lt_iff_le_not_le]

def equiv.le_map_iff_lt_map {α : Type*} {β : Type*} [partial_order α] [partial_order β]
  (he : α ≃ β) : (∀ x y, x ≤ y ↔ he x ≤ he y) ↔ (∀ x y, x < y ↔ he x < he y) :=
⟨equiv.lt_map_of_le_map he, λ hlt x y, by rw [le_iff_eq_or_lt, le_iff_eq_or_lt];
  exact or_congr (by simp) (hlt x y)⟩

[Kevin Buzzard]

I need these sorts of things to break up medium sized proofs in the perfectoid project into several smaller proofs. I am actively working on learning how to make my proofs shorter. Perhaps I'm asking the wrong question -- the question is "is this proof maintainable" and the answer is probably yes by this point.

[Kevin Buzzard]

I am dealing with preorders at the minute, and le_equiv and lt_equiv are not the same thing, but this is the relationship between them.

[Patrick Massot]

I don't think the question is whether these proofs are maintainable or not. The fact that these statement exist make other proof maintainable. And the fact that those proofs are obfuscated indicates that the statements are meant to be trivial.

[Kevin Buzzard]

It's just an empty file in which I import only what should be relevant for the search (and I keep changing the imports depending on what I want). So no interest in posting it. What you really need to do is merge #839 in your local copy of mathlib (or merge it in mathlib if you are an admin, to bring it to everyone :).

#839 seems to have some travis problem.

[Kevin Buzzard]

Here's another one:

import data.set.basic

example {α β : Type*} {f : α → β} (h : function.surjective f) {P : β → Prop} :
(∀ b, P b) ↔ ∀ a, P (f a) :=
⟨λ hb a, hb $ f a, λ ha b, begin rcases h b with ⟨a, rfl⟩, exact ha a end⟩

I am working in a project with mathlib as a dependency and merging the PR locally won't be much fun (sometimes my coauthors update mathlib so I'd lose local changes). I need this one because I have quite a complicated iff goal and the moment I split it I seem to have lost the chance to ever put the pieces together again. Rewriting this example will enable me to apply forall_congr and make progress. I want library_search! I guess I could run a second VS Code session with a patched mathlib project open -- or can one even do this within one VS Code session?

[Sebastien Gouezel]

No luck with library_search on this one. Add it to the library?

[Sebastien Gouezel]

It looks similar to forall_range_iff, if you add it to the library they should probably be close.

[Mario Carneiro]

lt_map_of_le_map looks suspiciously similar to le_iff_le_iff_lt_iff_lt

[Kevin Buzzard]

ooh thanks. I don't quite have the tools to search for this stuff.

[Kevin Buzzard]

I find myself writing x <= y iff f x <= f y a lot. Is that a bad way round to put it? Should it be f x <= f y iff x <= y?

[Mario Carneiro]

use whichever is more common in the library

[Mario Carneiro]

I would guess the second thing

[Kevin Buzzard]

lt_map_of_le_map looks suspiciously similar to le_iff_le_iff_lt_iff_lt

These are not the same though. My version is different because I am quantifying more.

[Mario Carneiro]

that's true. It is a short proof though

[Kevin Buzzard]

That's because b < a is the opposite of a <= b, whereas I don't have that luxury

[Kevin Buzzard]

oh that's not true! Maybe I do!

[Mario Carneiro]

the equiv is unnecessary I think

[Mario Carneiro]

there are variations of le_iff_le_iff_lt_iff_lt for preorders and such

[Kevin Buzzard]

aah -- not for me.

[Kevin Buzzard]

I need the equiv because I am working with preorders.

[Kevin Buzzard]

yeah, I am back to thinking they're similar but different.

[Kevin Buzzard]

For preorders, an le_equiv implies an lt_equiv, and for partial orders they're the same

[Mario Carneiro]

you can use lt_iff_lt_of_le_iff_le' to prove that first claim

[Kevin Buzzard]

and I have a real life situation where I need this result for preorders in the perfectoid project. The relation on a ring R induced by a valuation is a preorder. I only realised this a few days ago and it's made me think about things in a new way.

[Mario Carneiro]

and le_iff_le_of_strict_mono for the second

[Kevin Buzzard]

Thanks. These little things I'm writing are clogging up my for_mathlib directory and to a certain extent it's because I still don't really know where to look for some stuff.

[Johan Commelin]

There is a strict_mono file in for_mathlib/, I think