1
$\begingroup$

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)

$\endgroup$
1
  • 1
    $\begingroup$ One option is to write a calc proof. Then you can explicitly state each step of the equality and then fill in a proof (maybe using simp with the appropriate instance of your axiom for each step). $\endgroup$
    – Jason Rute
    Dec 1, 2023 at 4:39

1 Answer 1

1
$\begingroup$

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.

$\endgroup$
1
  • $\begingroup$ Thanks! Works like a charm. This occs setting was not showing up in my documentation because I had an old version, I guess one needs to update lean more frequently :). $\endgroup$
    – swish
    Dec 2, 2023 at 16:49

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.