two parallel hypotheses in a lemma

Stream: Is there code for X?

[Filippo A. E. Nuccio]

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...

[Patrick Massot]

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.

[Johan Commelin]

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

[Filippo A. E. Nuccio]

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.

[Johan Commelin]

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.

[Filippo A. E. Nuccio]

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".

[Filippo A. E. Nuccio]

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?

[Anne Baanen]

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 :(

[Eric Wieser]

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

[Filippo A. E. Nuccio]

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?

[Patrick Massot]

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

[Filippo A. E. Nuccio]

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

[Filippo A. E. Nuccio]

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...

[Anne Baanen]

(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.

[Anne Baanen]

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?

[Filippo A. E. Nuccio]

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

[Filippo A. E. Nuccio]

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.

[Anne Baanen]

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

[Filippo A. E. Nuccio]

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

[Patrick Massot]

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...)

[Filippo A. E. Nuccio]

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

[Patrick Massot]

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.

[Filippo A. E. Nuccio]

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.

[Mario Carneiro]

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

[Mario Carneiro]

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

[Anne Baanen]

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

[Filippo A. E. Nuccio]

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