reflexive - variable vs. argument to a function

Stream: new members

[Andrew Lubrino]

the following code works:

variable {U : Type}
variable R : U → U → Prop

lemma reflexive_a (a : U) (h1 : reflexive R) : R a a :=
begin
  exact h1 a
end

but the below code doesn't work:

variable {U : Type}
variable R : U → U → Prop
variable h1 : reflexive R

lemma reflexive_a (a : U) : R a a :=
begin
  exact h1 a
end

the only difference between the two sets of code is that in working example h1 : reflexive R is an argument to the lemma and in the non-working example, h1 : reflexive R is a variable. The error I get on the non-working example is, unknown identifier 'h1'.

could anyone tell me what's going wrong?

[Julian Berman]

Lean has different rules about prop variables -- if you do include h1 it will work, i.e.:

variable {U : Type}
variable R : U → U → Prop
variable (h1 : reflexive R)
include h1

lemma reflexive_a (a : U) : R a a :=
begin
  exact h1 a
end

[Julian Berman]

I think the rules are something like that they only get included if some other argument uses them -- #TPIL should say for sure

[Andrew Lubrino]

oh okay, so it's only a problem with Prop. Thanks!

[Julian Berman]

Sorry maybe I've misspoke about that bit as well:

Variables are only included in declarations where they are actually mentioned. More precisely, they must be mentioned outside of a tactic block; because variables can appear and can be renamed dynamically in a tactic proof, there is no reliable way of determining when a name used in a tactic proof refers to an element of the context in which the theorem is parsed, and Lean does not try to guess. You can manually ask Lean to include a variable in every definition in a section with the include command.

From https://leanprover.github.io/theorem_proving_in_lean/interacting_with_lean.html?highlight=included%20in#more-on-sections