How does polymorphism work in Lean?

Stream: new members

[YH]

For example, if I want to write

lemma tN (a b : ℕ) (a > 0) : (a + b > b) := sorry
lemma tQ (a b : ℚ) (a > 0) : (a + b > b) := sorry
lemma tR (a b : ℝ) (a > 0) : (a + b > b) := sorry

how do I convince Lean that the 2nd + is for ℚ and the 3rd + is for ℝ? Lean doesn't seem happy if I just write it like that. (Same question for >.)

[Johan Commelin]

@YH This solves your error message:

lemma tN (a b : ℕ) (h : a > 0) : (a + b > b) := sorry
lemma tQ (a b : ℚ) (h : a > 0) : (a + b > b) := sorry
lemma tR (a b : ℝ) (h : a > 0) : (a + b > b) := sorry

[Johan Commelin]

The problem was with the positivity assumption

[YH]

Oh, OK. Let me check it out.

[Johan Commelin]

Try eg:

lemma tQ (a b : ℚ) (a > 0) : true :=
begin
  -- cursor here
end

[Johan Commelin]

You'll see that the 2nd a in the statement is introduced as a new variable of type nat

[Johan Commelin]

I don't know why... it looks a bit buggy to me. But explicitly naming the hypothesis solves the issue

[YH]

Yes it works, thanks.

[Kevin Buzzard]

Hypotheses before the colon need to be named, right?

I would avoid y > x if you can. Replace it with x < y.

[Rob Lewis]

I think the acceptance of (a > 0) is a "feature" related to the parsing of ∀ x > 0. Not sure how intentional it is.

[Marc Huisinga]

lemma a (α : Type*) (xs : list α) (x : α) (h : x ∈ xs) : true := sorry
lemma b (α : Type*) (xs : list α) (x ∈ xs) : true := sorry
lemma c (α : Type*) (xs : list α) : Π x ∈ xs, true := sorry

all yield the same type when using check