Zulip Chat Archive

Stream: new members

Topic: rw


Alex Zhang (May 29 2021 at 14:29):

import order.lattice
import tactic

variables {α : Type*} [lattice α]
variables a b c : α

example (h :  x y z : α, x  (y  z) = (x  y)  (x  z)) :
  (a  b)  c = (a  c)  (b  c) :=
by {rewrite inf_comm, }

Here rw only allows me to apply inf_comm to the LHS. Is there any convenient way to apply inf_comm to all the three instances of c (i.e. changing the goal to c ⊓ (a ⊔ b) = (c ⊓ a) ⊔ (c ⊓ b)?

Horatiu Cheval (May 29 2021 at 14:45):

nth_rewrite is a way

Horatiu Cheval (May 29 2021 at 14:45):

import order.lattice
import tactic

variables {α : Type*} [lattice α]
variables a b c : α

example (h :  x y z : α, x  (y  z) = (x  y)  (x  z)) :
  (a  b)  c = (a  c)  (b  c) :=
by {
  nth_rewrite 0 inf_comm,
  nth_rewrite 1 inf_comm,
  nth_rewrite 2 inf_comm,
}

Horatiu Cheval (May 29 2021 at 14:46):

It allows you to rewrite the nth matching term in the goal

Horatiu Cheval (May 29 2021 at 14:47):

I'm not sure how to make it more concise here

Sebastien Gouezel (May 29 2021 at 14:49):

import order.lattice
import tactic

variables {α : Type*} [lattice α]
variables a b c : α

example (h :  x y z : α, x  (y  z) = (x  y)  (x  z)) :
  (a  b)  c = (a  c)  (b  c) :=
by { simp [@inf_comm _ _ _ c], }

The @ syntax makes it possible to prescribe all the parameters to a lemma, even the implicit ones. Here, I am telling simp to rewrite using inf_comm, but only each time the second parameter to this inf_comm is c.

Eric Rodriguez (May 29 2021 at 14:51):

i wonder if there could be something like ac_refl that's ac_exact or something

Eric Rodriguez (May 29 2021 at 14:53):

a ridiculous hack that does actually work is

  suffices : (a  b)  c = c  a  c  b,
  convert this using 0, ac_refl,

Eric Rodriguez (May 29 2021 at 14:56):

oh, also ac_change:

  ac_change (a  b)  c = c  a  c  b,

these are obviously very comm-specific though


Last updated: Dec 20 2023 at 11:08 UTC