Zulip Chat Archive

Stream: Is there code for X?

Topic: (no topic)


view this post on Zulip Gabriel Ebner (Oct 27 2020 at 08:35):

(deleted)

view this post on Zulip 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
| 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].

view this post on Zulip 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...

view this post on Zulip 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!

view this post on Zulip Johan Commelin (Feb 01 2021 at 15:05):

No worries!

view this post on Zulip 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

view this post on Zulip Eric Wieser (Mar 31 2021 at 11:45):

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

view this post on Zulip 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

view this post on Zulip 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₁

view this post on Zulip Eric Wieser (Mar 31 2021 at 11:50):

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

view this post on Zulip 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

view this post on Zulip Scott Morrison (Mar 31 2021 at 12:12):

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

view this post on Zulip 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