Have to keep passing same variable as inputs

Stream: lean4

[Nir Paz]

I think I asked for help with this in the past. I'm formalizing a proof that involves a somewhat complicated construction with many hypotheses fixed throughout. Basically the theorem has the form ∀ x : Foo, ∃ y, P y, and the proof fixes an x and reaches a contradiction using a lengthy construction that uses the hypothesis ∀ y, ¬ P y.

There are many assumptions about Foo in the background, and theoretically the way I want to structure the proof is to add them all as variables in a section and in it define the steps of the construction and the lemmas about it. The problem is that I always have to pass the variables as inputs at every step. For example:

import Mathlib

noncomputable section
open Classical

variable {Foo : Type*} {assumptions : Prop} {we : Prop} {make : Prop}

-- function uses many variables
def foo : Foo → ℕ := fun _ ↦ if assumptions ∧ we ∧ make then 0 else 1

-- failed to synth implicit arguments to `foo`
def foo' : Foo → ℕ := fun x ↦ (foo x) + 1

end

So whenevery I use foo I have to pass many assumptions to it, which I would like to think of as "assumptions we fixed before we started the construction". These extra inputs are passed down into every theorem about foo.

Does anyone have a better way to organize such proofs?

[Patrick Massot]

You can put assumptions in a structure.

[Nir Paz]

Patrick Massot said:

You can put assumptions in a structure.

This works nicely! Also makes it easier for lean to fill it in. Is there a way to "open" a structure so that I can write h instead of foo.h?

[Mario Carneiro]

open foo

[Mario Carneiro]

One technique I have used occasionally when the list of assumptions is sufficiently large and stable across theorems is to use nullary typeclasses. Here is an example. Note the use of a in the dom_a theorem is referring to the field of the Extension1 structure

[Nir Paz]

Mario Carneiro said:

open foo

foo : Foo in this context, so I can't open foo. And open Foo doesn't work either. But the example you gave using classes is great! The exact same structure seems to work smoothly in my case, thanks!