module parameters

Stream: new members

[Thorsten Altenkirch]

Is there anything like module parameters (or section parameters) in Lean? I want to assume that a relation is a decidable partial order without prefixing even construction with this assumption. While I can use variables to abstract over the relation this obviously doesn't work for the properties. because they show only up in the proofs.

[Mario Carneiro]

this obviously doesn't work for the properties

But it does work for properties

[Mario Carneiro]

in particular, for typeclass assumptions you can have variables (R : A -> A -> Prop) [decidable_rel R] and it will work as you expect

[Mario Carneiro]

For other kinds of hypotheses, that are not typeclasses like variables (R : A -> A -> Prop) (hr : \all x, R x x), you may have to use include hr to include the assumption even in definitions that don't require it (although this may cause a linting warning since it's an unused argument)

[Thorsten Altenkirch]

Thank you. So where do I say "include hr" when I want to use it in a proof?

[Mario Carneiro]

section
variables (R : A -> A -> Prop) (hr : \all x, R x x)
theorem uses_hr : \all x, R x x := hr
theorem doesnt_use_hr : true := by have := hr -- fail
include hr
theorem uses_hr : true := by have := hr; trivial
end

[Mario Carneiro]

include is scoped like variable

[Mario Carneiro]

you can also undo include using omit