Zulip Chat Archive

Stream: new members

Topic: How does polymorphism work in Lean?


view this post on Zulip YH (Dec 11 2019 at 06:23):

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

view this post on Zulip Johan Commelin (Dec 11 2019 at 06:39):

@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

view this post on Zulip Johan Commelin (Dec 11 2019 at 06:39):

The problem was with the positivity assumption

view this post on Zulip YH (Dec 11 2019 at 06:40):

Oh, OK. Let me check it out.

view this post on Zulip Johan Commelin (Dec 11 2019 at 06:40):

Try eg:

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

view this post on Zulip Johan Commelin (Dec 11 2019 at 06:41):

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

view this post on Zulip Johan Commelin (Dec 11 2019 at 06:41):

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

view this post on Zulip YH (Dec 11 2019 at 06:42):

Yes it works, thanks.

view this post on Zulip Kevin Buzzard (Dec 11 2019 at 15:04):

Hypotheses before the colon need to be named, right?

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

view this post on Zulip Rob Lewis (Dec 11 2019 at 15:07):

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

view this post on Zulip Marc Huisinga (Dec 11 2019 at 15:12):

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


Last updated: May 15 2021 at 22:14 UTC