Zulip Chat Archive

Stream: general

Topic: or_iff_or


Kevin Buzzard (Mar 22 2019 at 12:14):

@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 (Mar 22 2019 at 12:17):

hint: it's a congr lemma

Sebastien Gouezel (Mar 22 2019 at 12:30):

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 (Mar 22 2019 at 12:32):

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 (Mar 22 2019 at 12:36):

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 (Mar 22 2019 at 12:42):

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 (Mar 22 2019 at 12:43):

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 (Mar 22 2019 at 12:43):

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

Patrick Massot (Mar 22 2019 at 12:44):

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

Kevin Buzzard (Mar 22 2019 at 12:46):

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 (Mar 22 2019 at 12:46):

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

Sebastien Gouezel (Mar 22 2019 at 12:47):

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 (Mar 22 2019 at 12:50):

Oh I see, you change the imports to suit.

Kevin Buzzard (Mar 22 2019 at 12:51):

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 (Mar 22 2019 at 12:51):

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 (Mar 22 2019 at 12:56):

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 (Mar 22 2019 at 13:20):

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 (Mar 22 2019 at 17:59):

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 (Mar 22 2019 at 18:04):

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 (Mar 22 2019 at 18:23):

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

Sebastien Gouezel (Mar 22 2019 at 18:25):

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

Mario Carneiro (Mar 22 2019 at 20:55):

lt_map_of_le_map looks suspiciously similar to le_iff_le_iff_lt_iff_lt

Kevin Buzzard (Mar 22 2019 at 21:05):

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

Kevin Buzzard (Mar 22 2019 at 21:06):

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 (Mar 22 2019 at 21:07):

use whichever is more common in the library

Mario Carneiro (Mar 22 2019 at 21:08):

I would guess the second thing

Kevin Buzzard (Mar 22 2019 at 21:08):

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 (Mar 22 2019 at 21:08):

that's true. It is a short proof though

Kevin Buzzard (Mar 22 2019 at 21:09):

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

Kevin Buzzard (Mar 22 2019 at 21:09):

oh that's not true! Maybe I do!

Mario Carneiro (Mar 22 2019 at 21:09):

the equiv is unnecessary I think

Mario Carneiro (Mar 22 2019 at 21:10):

there are variations of le_iff_le_iff_lt_iff_lt for preorders and such

Kevin Buzzard (Mar 22 2019 at 21:10):

aah -- not for me.

Kevin Buzzard (Mar 22 2019 at 21:10):

I need the equiv because I am working with preorders.

Kevin Buzzard (Mar 22 2019 at 21:11):

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

Kevin Buzzard (Mar 22 2019 at 21:11):

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

Mario Carneiro (Mar 22 2019 at 21:12):

you can use lt_iff_lt_of_le_iff_le' to prove that first claim

Kevin Buzzard (Mar 22 2019 at 21:12):

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 (Mar 22 2019 at 21:13):

and le_iff_le_of_strict_mono for the second

Kevin Buzzard (Mar 22 2019 at 21:14):

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 (Mar 22 2019 at 21:19):

There is a strict_mono file in for_mathlib/, I think


Last updated: Dec 20 2023 at 11:08 UTC