Zulip Chat Archive

I'm trying to define a board which has either of two states and I am not sure how to do it
This is what I have written so far:
Is there a nicer way to do so? Because the Board structure asks me to pass in a state

inductive State
| Alive
| Dead

structure Point (α : State) :=
mk :: (x : State) (y : State)

structure Board (β : Point) where
  x : [β]

and this is what I get

type expected at
  Point
term has type
  State → Type

Something I would do in haskell would be type Point = (int, int) and type Board = [Point].

Johan Commelin (Feb 01 2021 at 15:02):

This should be asked in #general in a new thread with a name. This stream is for asking whether stuff already exists in mathlib...

Mehul (Feb 01 2021 at 15:03):

Johan Commelin said:

This should be asked in #general in a new thread with a name. This stream is for asking whether stuff already exists in mathlib...

Oh I am sorry, I just got confused where to ask. Thanks!

Johan Commelin (Feb 01 2021 at 15:05):

No worries!

Scott Morrison (Mar 31 2021 at 11:37):

I want to make use of the following lemma. Should I just prove it locally at the point of use, or is it worthy of algebra.ordered_ring?

lemma mul_unit_interval_le {α : Type*} [ordered_semiring α] {a b c : α}
  (h₁ : 0 ≤ c) (h₂ : a ≤ c) (h₃ : 0 ≤ b) (h₄ : b ≤ 1) : a * b ≤ c :=
begin
  conv_rhs { rw ←mul_one c, },
  exact mul_le_mul h₂ h₄ h₃ h₁,
end

Eric Wieser (Mar 31 2021 at 11:45):

I think I remember seeing a collection of that style of lemma somewhere

Eric Wieser (Mar 31 2021 at 11:46):

Searching ordered_ring.lean for one_mul suggests we only covered the cases with two variables, not three

Johan Commelin (Mar 31 2021 at 11:48):

I think it's ok to have all these variations. Btw, with simpa it's a oneliner:

lemma mul_unit_interval_le {α : Type*} [ordered_semiring α] {a b c : α}
  (h₁ : 0 ≤ c) (h₂ : a ≤ c) (h₃ : 0 ≤ b) (h₄ : b ≤ 1) : a * b ≤ c :=
by simpa only [mul_one] using mul_le_mul h₂ h₄ h₃ h₁