associativity tactic

Stream: maths

[Dean Young]

Here I have a definition of a category:

-- Definition of a category
structure CatObj where
  Obj : Type u
  Hom : ∀(_:Obj),∀(_:Obj), Type v
  identity : ∀(X:Obj),Hom X X
  composition : ∀(X:Obj),∀(Y:Obj),∀(Z:Obj),∀(_:Hom X Y),∀(_:Hom Y Z),Hom X Z
  identity₁: ∀(X:Obj),∀(Y:Obj),∀(f:Hom X Y),(composition X Y Y) f (identity Y) = f
  identity₂: ∀(X:Obj),∀(Y:Obj),∀(f:Hom X Y),(composition X X Y) (identity X) f = f
  Ass : ∀(W:Obj),∀(X:Obj),∀(Y:Obj),∀(Z:Obj),∀(f:Hom W X),∀(g:Hom X Y),∀(h:Hom Y Z),
  (composition W X Z) f (composition X Y Z g h) = composition W Y Z (composition W X Y f g) h

I'm trying to design a tactic that applies associativity to show that "the brackets don't matter" in any two expressions involving composition, like this:

def p : Expression₁ = Expression₂ := by associativity

I figured the way it would work is to show that both are equal to the right-associated expression Expression₃.

I'm still pretty new to Lean, especially tactics. I was wondering how something like this should be done.

--Dean

[Dean Young]

Ok, so I want to always rewrite

(composition W X Z) f (composition X Y Z g h)

to

composition W Y Z (composition W X Y f g) h

on both sides of the expression, until I can't anymore (so using repeat {}).

Then I want to apply reflexivity.

[Dean Young]

I don't really understand how to use rewrite though. Is it based in regex?

[Dean Young]

I guess I'm wondering about rewrite then. Exactly how powerful is rewrite? For instance, will rewrite be able to find that

a ∘ (b ∘ X)

is a subexpression of

a ∘ (b ∘ (c ∘ d))

so as to apply associativity?

[Dean Young]

Ok so something like this:

begin
repeat {rewrite C.Ass},
reflexivity
end

[Dean Young]

that felt way too easy... and I'm very curious about exactly which subexpressions rewrite can find. Seems like it brute force searches them all? Or just the "atomic" ones?

[Henrik Böving]

it will look for a match of the expression on the left hand side inside of your rewrite term in the goal by simply traversing the expression tree that underlies the goal (it can also do this with quantified variables like in your case) and replace that expression with the right hand side of your rewrite term.

[Dean Young]

ok that's great then. seems like my associativity tactic will work perfectly!

[Dean Young]

(deleted)