Rewriting certain terms in Lean4

Question

I want to prove the following theorem using a single axiom (https://mathworld.wolfram.com/WolframAxiom.html):

variable {A : Type}

axiom dot : A -> A -> A
infix : 50 " * " => dot

axiom wolfram_axiom (a b c : A) : (((a * b) * c) * (a * ((a * c) * a))) = c

theorem double_negation (a : A) : ((a * a) * (a * a)) = a := sorry

I already have a long proof from Automatic Theorem Prover in terms of many-many rewrites at certain term positions. I just want to see how it would look like in Lean. For example as my first rewrite I want to apply this term:

let term1 := wolfram_axiom a ((a * a) * a) a -- ((a * ((a * a) * a)) * a) * (a * ((a * a) * a))) = a

at a certain a, the 4th one for example, so that the new goal becomes this:

(a * a) * (a  * (((a * (a  * ((a * a) * a))) * a) * (a * ((a * a) * a)))) = a

How can I do it?

(Also is it possible to use . instead of * here? Lean thinks it's a function composition)

Answer 1

Use the following:

variable {A : Type}

axiom dot : A -> A -> A
infix : 50 " * " => dot

axiom wolfram_axiom (a b c : A) : (((a * b) * c) * (a * ((a * c) * a))) = c

example (a : A) (b : A): ((a * a) * (a * a)) = a := by
  have term1 := wolfram_axiom a ((a * a) * a) a
  rw (config := {occs := .pos [4]}) [<-term1]
  -- goal: ((a * a) * (a * (((a * ((a * a) * a)) * a) * (a * ((a * a) * a))))) = a
  sorry

Let's look at:

rw (config := {occs := .pos [4]}) [<-term1]

• the <-term1 means to rewrite with term1 but in reverse, namely

  a = (((a * ((a * a) * a)) * a) * (a * ((a * a) * a)))
  

• the (config := {occs := .pos [4]}) means to rewrite at the forth possibly rewrite occurrence. It is a list so you can put more than one number in there, or use .neg for specifying which occurrences not to rewrite.

All this can be found in the documentation for rewrite which you can get hovering over the tactic. (The rw tactic annoyingly tells you to look at the documentation for rewrite.)

Another approach is to use calc mode to outline long equality proofs. Then you only need to give a separate proof of each equality step which is often easier. For example:

example (a : A) (b : A): ((a * a) * (a * a)) = a :=
  calc
    ((a * a) * (a * a)) 
      = ((a * a) * (a * (((a * ((a * a) * a)) * a) * (a * ((a * a) * a))))) := by
        rw [wolfram_axiom a ((a * a) * a) a]
    _ = a := by sorry

Note how the rw tactic is now much simpler since I can rewrite the complicated term which there is only one of.