rw

Stream: new members

[Alex Zhang]

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]

nth_rewrite is a way

[Horatiu Cheval]

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]

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

[Horatiu Cheval]

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

[Sebastien Gouezel]

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]

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

[Eric Rodriguez]

a ridiculous hack that does actually work is

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

[Eric Rodriguez]

oh, also ac_change:

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

these are obviously very comm-specific though