Zulip Chat Archive

Stream: Is there code for X?

Topic: two parallel hypotheses in a lemma


view this post on Zulip Filippo A. E. Nuccio (Nov 10 2020 at 08:42):

Is there a way to state one lemma but with two different layers of hypothesis? What I am proving is that
1) in a noetherian ring every ideal contains a product of primes; and
2) in every domain any nonzero ideal contains a nonzero product of primes.
The proof of the two lemmas is "the same", upon adding the hypothesis nonzero here and there. Unfortunately, though, I am not aware of a proof deducing 2) from 1). So I am wondering if a statement along the lines of lemma (h1 : p) (h2 : q) [optional h3] : foo [plus benefits] (meaning that the benefits hold only when assuming h3) exists in Lean. Recalling @Patrick Massot 's talk in LFTCM when he spoke about 2197 lemmas to be stated and proven to express the composition of limits when not using filters makes me believe the answer is no, but I lean towards optimism...

view this post on Zulip Patrick Massot (Nov 10 2020 at 08:44):

There is no such syntax. Indeed I explained in my talk that the 2197 lemmas issues is not solved by a software gadget but by mathematical insight.

view this post on Zulip Johan Commelin (Nov 10 2020 at 08:45):

In this case, I would just copy-paste the proof and modify it.

view this post on Zulip Filippo A. E. Nuccio (Nov 10 2020 at 08:45):

I believed so, and this is what I was going to do. But it does not look nice and I wanted to avoid stupid things.

view this post on Zulip Johan Commelin (Nov 10 2020 at 08:46):

You will then either find sublemmas that can be extracted, or you can define a "tactic macro" (this sounds scary, but is easy) that gives you a custom tactic that you can use in both proofs.

view this post on Zulip Filippo A. E. Nuccio (Nov 10 2020 at 08:46):

Patrick Massot said:

There is no such syntax. Indeed I explained in my talk that the 2197 lemmas issues is not solved by a software gadget but by mathematical insight.

I was pretty sure, my only hope was that "adding" a layer was slightly different from "having two parallels proofs going along parallel lines".

view this post on Zulip Filippo A. E. Nuccio (Nov 10 2020 at 08:48):

Johan Commelin said:

You will then either find sublemmas that can be extracted, or you can define a "tactic macro" (this sounds scary, but is easy) that gives you a custom tactic that you can use in both proofs.

I see what you mean when you speak about sublemmas and I will try to do so. Can you point to some reference describing the scarying-but-easy macro?

view this post on Zulip Anne Baanen (Nov 10 2020 at 08:48):

It could be possible with the power of dependent type theory: lemma foo (h3 : option (type_of_hypothesis) : h3.elim easy (λ _, easy ∧ bonus). But nothing in the Lean library is set up to deal with it, so you will have a bad time :(

view this post on Zulip Eric Wieser (Nov 10 2020 at 08:51):

Presumably though you could do what @Anne Baanen suggests and then create two wrapper lemmas to untangle the weirdness for normal use?

view this post on Zulip Filippo A. E. Nuccio (Nov 10 2020 at 08:51):

Looks very nice; yet I am not sure to understand the syntax. Are you saying that I should let h3 be a term of the dependent type option which has only two terms, one being "empty" and the other being my "true" h3?

view this post on Zulip Patrick Massot (Nov 10 2020 at 08:52):

That sounds like a fun exercise, although it's unclear you'll gain anything.

view this post on Zulip Filippo A. E. Nuccio (Nov 10 2020 at 08:52):

In particular, I first need to define this option : Type

view this post on Zulip Filippo A. E. Nuccio (Nov 10 2020 at 08:53):

Patrick Massot said:

That sounds like a fun exercise, although it's unclear you'll gain anything.

Well, I will learn something and kill some lockdown-time...

view this post on Zulip Anne Baanen (Nov 10 2020 at 08:53):

(Option is not really a dependent type, but yes indeed.) My advice would be to try it and if it doesn't work, use Johan's suggestion.

view this post on Zulip Anne Baanen (Nov 10 2020 at 08:53):

Filippo A. E. Nuccio said:

In particular, I first need to define this option : Type

option is defined in core Lean, so you have it available, right?

view this post on Zulip Filippo A. E. Nuccio (Nov 10 2020 at 08:54):

OK, I'll see what I can come up with... :cold_sweat: . Thanks!

view this post on Zulip Filippo A. E. Nuccio (Nov 10 2020 at 08:54):

Anne Baanen said:

Filippo A. E. Nuccio said:

In particular, I first need to define this option : Type

option is defined in core Lean, so you have it available, right?

AH, I did not know, I thought it was part of your example. This seems a good news.

view this post on Zulip Anne Baanen (Nov 10 2020 at 08:54):

Ah, one problem is that the argument to option needs to be a Type u and you probably have a Prop.

view this post on Zulip Filippo A. E. Nuccio (Nov 10 2020 at 08:55):

Can't I make a new Type from option "bundling" it over Type?

view this post on Zulip Patrick Massot (Nov 10 2020 at 08:56):

Filippo A. E. Nuccio said:

Well, I will learn something and kill some lockdown-time...

I have 50 exams to grade if you need some lockdown-time killing (that's my I'm answering questions here instead of working...)

view this post on Zulip Filippo A. E. Nuccio (Nov 10 2020 at 08:57):

Something like that will land on my desk next week, I try to be super-busy by then :wink:

view this post on Zulip Patrick Massot (Nov 10 2020 at 09:00):

This is a lock-down exam so students actually had all the time they wanted to do it. I told them they could send me formalized solutions but it didn't work.

view this post on Zulip Filippo A. E. Nuccio (Nov 10 2020 at 09:01):

But was it a Lean course or a math-course where you were using Lean? I am asking since I am thinking about teaching a bit using Lean in the Second term and hoped to borrow some of your material in French.

view this post on Zulip Mario Carneiro (Nov 10 2020 at 09:12):

You don't need fancy dependent types for this, you can just prove lemma (h1 : p) (h2 : q) : foo /\ (h3 -> benefits)

view this post on Zulip Mario Carneiro (Nov 10 2020 at 09:13):

Usually that would be two separate proofs, but if they share a lot of common structure it might make sense to prove both in one go and unpack them afterwards

view this post on Zulip Anne Baanen (Nov 10 2020 at 09:15):

Ah yes of course. I had a dependently-typed hammer and this problem looked like a pi-shaped nail. :face_palm:

view this post on Zulip Filippo A. E. Nuccio (Nov 10 2020 at 09:15):

I see, I guess this goes very much along the lines suggested by @Johan Commelin , of "extracting as many sublemmas as possible", just shifting the presentation a bit from "some sublemmas allow to quickly deduce two statements" to "many parts of this proof can be used to show the /\ part


Last updated: May 17 2021 at 16:26 UTC