## Stream: Is there code for X?

### Topic: (no topic)

(deleted)

#### Mehul (Feb 01 2021 at 15:01):

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

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!

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₁


#### Eric Wieser (Mar 31 2021 at 11:50):

If you want a one-liner, mul_one c ▸ mul_le_mul h₂ h₄ h₃ h₁

#### Eric Wieser (Mar 31 2021 at 11:51):

If you're going to add that lemma though, you should probably add variations for each argument of mul_le_mul being 1

#### Scott Morrison (Mar 31 2021 at 12:12):

Ugh, that requires making some of the other variations of mul_le_mul as well.

#### Damiano Testa (Mar 31 2021 at 14:17):

I wonder whether ordered_monoid_with_zero is the right level of generality... :lol: :upside_down:

Last updated: May 07 2021 at 22:14 UTC