search

AlexDuchnowski / rubiks-cube

A Lean 4 representation of the Rubik's Cube, some proofs about the representation, and a simple solution algorithm.
6 stars 0 forks source link

I proved the ps_mul_assoc, its order should be like this: lemma ps_mul_assoc {p o : ℕ+} : ∀ (a b c : PieceState p o), ps_mul c (ps_mul b a) = ps_mul (ps_mul c b) a #1

Closed chenjulang closed 5 months ago

chenjulang commented 5 months ago

Check this out:https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/.E2.9C.94.20Rubik's.20cube.20associative.20law.3F

In this file: "https://github.com/AlexDuchnowski/rubiks-cube/blob/main/RubiksCube/RubiksCubeFunc.lean"

lemma ps_mul_assoc {p o : ℕ+} : ∀ (a b c : PieceState p o), ps_mul c (ps_mul b a) = ps_mul (ps_mul c b) a := by intro a b c simp [ps_mul] apply And.intro · simp [Perm.mul_def] simp [Equiv.trans_assoc] · rw [← add_assoc] simp only [add_left_inj] exact rfl done

chenjulang commented 5 months ago

The second parameter of "ps_mul" is actually the first Rubik's Cube operation performed.

AlexDuchnowski commented 5 months ago

Thanks for completing the proof of the second conjunct! I've updated the file to have the full proof.

When it comes to the order of the variables in the statement of the lemma, I'm pretty sure the statements are equivalent, since there are no particular assumptions made about any of the PieceStates. To transform one statement into the other, simply flip the sides of the equality and swap a and c. (Either way, the original lemma statement is proven with the proof you provided, so I kept it the same).

chenjulang commented 4 months ago

Doubts about "plus_mul":

How is the "orient" defined in a practical sense in "plus_mul"? Clockwise or counterclockwise? Which direction of edge block and corner block is 0,1,2?

julang @.***

 

------------------ 原始邮件 ------------------ 发件人: "AlexDuchnowski/rubiks-cube" @.>; 发送时间: 2024年2月20日(星期二) 凌晨4:01 @.>; @.**@.>; 主题: Re: [AlexDuchnowski/rubiks-cube] I proved the ps_mul_assoc, its order should be like this: lemma ps_mul_assoc {p o : ℕ+} : ∀ (a b c : PieceState p o), ps_mul c (ps_mul b a) = ps_mul (ps_mul c b) a (Issue #1)

Thanks for completing the proof of the second conjunct! I've updated the file to have the full proof.

When it comes to the order of the variables in the statement of the lemma, I'm pretty sure the statements are equivalent, since there are no particular assumptions made about any of the PieceStates. To transform one statement into the other, simply flip the sides of the equality and swap a and c. (Either way, the original lemma statement is proven with the proof you provided, so I kept it the same).

— Reply to this email directly, view it on GitHub, or unsubscribe. You are receiving this because you authored the thread.Message ID: @.***>