Zulip Chat Archive

Stream: general

Topic: subst at hyp


view this post on Zulip Johan Commelin (Sep 07 2018 at 08:31):

Could we have subst foobar at hyp for substituting in the hypotheses of the local context? Currently I am using repeat {rw foobar at hyp} which feels a bit verbose...

view this post on Zulip Kenny Lau (Sep 07 2018 at 08:32):

subst foobar

view this post on Zulip Chris Hughes (Sep 07 2018 at 08:34):

What about simp only [foobar] at hyp

view this post on Zulip Johan Commelin (Sep 07 2018 at 08:35):

aah never mind. subst is only for local constants. I wanted to substitute x = y where x = y was the result of some proposition.

view this post on Zulip Johan Commelin (Sep 07 2018 at 08:36):

simp only works!

view this post on Zulip Kenny Lau (Sep 07 2018 at 08:38):

MWE?

view this post on Zulip Johan Commelin (Sep 07 2018 at 08:38):

https://gist.github.com/jcommelin/2e031b5446ca54089576ea9f66f12abf

view this post on Zulip Kenny Lau (Sep 07 2018 at 08:39):

?

view this post on Zulip Johan Commelin (Sep 07 2018 at 08:40):

Right, so now you only see the simps. For the repeat {rw ...} you have to look in the history.

view this post on Zulip Johan Commelin (Sep 07 2018 at 08:40):

Basically I'm challenging you to golf it :lol:

view this post on Zulip Kenny Lau (Sep 07 2018 at 08:44):

what import is allowed?

view this post on Zulip Johan Commelin (Sep 07 2018 at 08:45):

I don't really care

view this post on Zulip Johan Commelin (Sep 07 2018 at 08:45):

What would you want to use? tidy?

view this post on Zulip Kenny Lau (Sep 07 2018 at 08:46):

you didn't import any file from mathlib, so I can't use any mathlib tactic

view this post on Zulip Johan Commelin (Sep 07 2018 at 08:47):

Wasnt have ... simp at this ... exact this some sort of idiom that can be golfed into a simpa-oneliner? I tried but failed.

view this post on Zulip Reid Barton (Sep 07 2018 at 08:50):

simpa using this

view this post on Zulip Reid Barton (Sep 07 2018 at 08:51):

Or rather simpa using ...

view this post on Zulip Johan Commelin (Sep 07 2018 at 08:54):

And what do I need to import to get simpa?

view this post on Zulip Reid Barton (Sep 07 2018 at 08:54):

My attempt: https://gist.github.com/rwbarton/b79b804e4bff300a5aa2a4ec2951c55e

view this post on Zulip Reid Barton (Sep 07 2018 at 08:54):

Anything in mathlib, but say tactic.interactive

view this post on Zulip Kenny Lau (Sep 07 2018 at 08:55):

import tactic.interactive

universe u

namespace eckmann_hilton
variables (X : Type u)

local notation a `<`m`>` b := @has_mul.mul X m a b

class is_unital [m : has_mul X] [e : has_one X] : Prop :=
(one_mul :  x : X, (e.one <m> x) = x)
(mul_one :  x : X, (x <m> e.one) = x)

attribute [simp] is_unital.one_mul is_unital.mul_one

variables {X} {m₁ : has_mul X} {e₁ : has_one X} {m₂ : has_mul X} {e₂ : has_one X}
variables (h₁ : @is_unital X m₁ e₁) (h₂ : @is_unital X m₂ e₂)
variables (distrib :  a b c d, ((a <m₂> b) <m₁> (c <m₂> d)) = ((a <m₁> c) <m₂> (b <m₁> d)))
include h₁ h₂ distrib

lemma one : (e₁.one = e₂.one) :=
by simpa using distrib e₂.one e₁.one e₁.one e₂.one

lemma mul : (m₁.mul = m₂.mul) :=
by funext a b; have := distrib a e₁.one e₁.one b;
simp at this; simpa [one h₁ h₂ distrib] using this

lemma mul_comm : is_commutative _ m₂.mul :=
⟨λ a b, by simpa [mul h₁ h₂ distrib] using distrib e₂.one a b e₂.one

lemma mul_assoc : is_associative _ m₂.mul :=
⟨λ a b c, by simpa [mul h₁ h₂ distrib] using distrib a b e₂.one c

instance : comm_monoid X :=
{ mul_comm := (mul_comm h₁ h₂ distrib).comm,
  mul_assoc := (mul_assoc h₁ h₂ distrib).assoc,
  ..m₂, ..e₂, ..h₂ }

end eckmann_hilton

view this post on Zulip Johan Commelin (Sep 07 2018 at 09:00):

Well done!

view this post on Zulip Johan Commelin (Sep 07 2018 at 09:02):

@Kenny Lau https://gist.github.com/jcommelin/2e031b5446ca54089576ea9f66f12abf
I added your name.

view this post on Zulip Kenny Lau (Sep 07 2018 at 09:02):

lol


Last updated: May 14 2021 at 22:15 UTC