Edge pieces are now solved!

Rubik/Algorithm.lean

@@ -197,46 +197,135 @@ theorem edgePieceEquiv_flipEdges :
     · conv_rhs => rw [← fixEdges_move₂ e₁ e₂, edgeEquiv_mk, Edge.flipEquiv_mk, ← edge_flip]
       rfl
 
+@[simp]
+theorem edgeEquiv_flipEdges : edgeEquiv (move (flipEdges e₁ e₂)) = 1 := by
+  ext a
+  refine a.inductionOn ?_
+  intro a
+  simp [edgeEquiv_mk]
+
 end Moves
 
 namespace Rubik
 
 /-- A sequence of moves that puts the cube's edges in their correct position, in the specified
 order. -/
-private def solveEdgesAux (cube : Rubik) (l : List Edge)
-    (he : ∀ e, e ∈ l ↔ PRubik.edgeEquiv cube e ≠ e) : Moves :=
-  match l with
+private def solveEdgesAux (cube : Rubik) : List Edge → Moves
   | [] => []
   | a::l =>
-    let m := Moves.swapEdges a ((PRubik.edgeEquiv cube).symm a)
+    let m := Moves.swapEdges a ((edgeEquiv cube).symm a)
     let c := cube * move m
-    m ++ solveEdgesAux c (l.filter fun e ↦ PRubik.edgeEquiv c e ≠ e) (by
-      intro e
-      simp [c, m, Rubik.move]
-      intro ha
+    m ++ solveEdgesAux c (l.filter fun e ↦ edgeEquiv c e ≠ e)
+termination_by l => l.length
+decreasing_by exact (List.length_filter_le _ _).trans_lt (Nat.lt_succ_self _)
+
+private theorem solveEdgesAux_solve (cube : Rubik) (l : List Edge)
+    (he : ∀ e, e ∈ l ↔ edgeEquiv cube e ≠ e) :
+    edgeEquiv (PRubik.move (solveEdgesAux cube l)) = (edgeEquiv cube)⁻¹ :=
+  match l with
+  | [] => by
+    simp at he
+    have : _  = Equiv.refl _ := Equiv.ext he
+    simp [solveEdgesAux, this]
+  | a::l => by
+    rw [solveEdgesAux]
+    simp
+    rw [solveEdgesAux_solve]
+    · simp
+    · simp
+      intro e ha
       obtain rfl | he₁ := eq_or_ne e a
       · simp at ha
       · obtain rfl | he₂ := eq_or_ne e ((PRubik.edgeEquiv cube).symm a)
         · apply (List.mem_cons.1 ((he _).2 _)).resolve_left he₁
           simpa using he₁.symm
         · rw [Equiv.swap_apply_of_ne_of_ne he₁ he₂] at ha
           exact (List.mem_cons.1 ((he _).2 ha)).resolve_left he₁
-    )
 termination_by l.length
 decreasing_by exact (List.length_filter_le _ _).trans_lt (Nat.lt_succ_self _)
 
-private theorem solveEdgesAux_solve (cube : Rubik) (l : List Edge)
-    (he : ∀ e, e ∈ l ↔ PRubik.edgeEquiv cube e ≠ e) :
-    PRubik.edgeEquiv (cube * move (solveEdgesAux cube l he)) = Equiv.refl _ :=
-  sorry
-
 /-- A sequence of moves that puts the cube's edges in their correct position. -/
 def solveEdges (cube : Rubik) : Moves :=
-  solveEdgesAux cube ((Finset.univ.filter fun e ↦ PRubik.edgeEquiv cube e ≠ e).sort (· ≤ ·))
-    (by simp)
+  solveEdgesAux cube ((Finset.univ.filter fun e ↦ edgeEquiv cube e ≠ e).sort (· ≤ ·))
 
+@[simp]
 theorem solveEdges_solve (cube : Rubik) :
-    PRubik.edgeEquiv (cube * move (solveEdges cube)) = Equiv.refl _ :=
-  solveEdgesAux_solve _ _ _ 
+    edgeEquiv (PRubik.move (solveEdges cube)) = (edgeEquiv cube)⁻¹ := by
+  apply solveEdgesAux_solve
+  simp
+
+/-- A sequence of moves that puts the cube's edges in their correct orientation, in the specified
+order. -/
+private def solveEdgePiecesAux : List Edge → Moves
+  | [] | [_] => []
+  | a::b::l => Moves.flipEdges a b ++ solveEdgePiecesAux l
+
+theorem solveEdgePiecesAux_solve (cube : Rubik) (hc : edgeEquiv cube = 1)
+    (l : List Edge) (hl : l.Nodup) (he : ∀ e, ⟦e⟧ ∈ l ↔ edgePieceEquiv cube e ≠ e) :
+    edgePieceEquiv (PRubik.move (solveEdgePiecesAux l)) = (edgePieceEquiv cube)⁻¹ :=
+  have hc' (e) : cube.1.edgePieceEquiv e = e ∨ cube.1.edgePieceEquiv e = e.flip :=
+    EdgePiece.equiv_iff.1 <| Quotient.exact <| Equiv.ext_iff.1 hc ⟦e⟧
+  match l with
+  | [] => by simpa [solveEdgePiecesAux, Equiv.ext_iff] using he
+  | [a] => by
+    have : (1 : ℤˣ) ≠ -1 := by decide
+    apply (this _).elim
+    conv_lhs => rw [← (Rubik.isValid cube).edgeFlip, edgeFlip, MonoidHom.coe_comp,
+      Function.comp_apply, edgePieceEquivHom_apply]
+    suffices edgePieceEquiv cube = a.flipEquiv by
+      rw [this]
+      refine a.inductionOn ?_
+      simpa using fun a ↦ a.flip_ne.symm
+    ext e
+    simp_rw [List.mem_singleton] at he
+    obtain rfl | ha := eq_or_ne a ⟦e⟧
+    · rw [Edge.flipEquiv_mk, Equiv.swap_apply_left]
+      exact (hc' _).resolve_left ((he _).1 rfl)
+    · rwa [Edge.flipEquiv_of_ne ha, ← not_ne_iff, ← he, eq_comm]
+  | a::b::l => by
+    simp only [List.nodup_cons, List.mem_cons, not_or, ← ne_eq] at hl
+    rw [solveEdgePiecesAux, PRubik.move_append, edgePieceEquiv_mul, Moves.edgePieceEquiv_flipEdges,
+      solveEdgePiecesAux_solve (cube * move (Moves.flipEdges a b)) _ _ hl.2.2]
+    · simp [mul_assoc]
+    · simp
+      intro e
+      have H (e : EdgePiece) : edgePieceEquiv cube e ≠ e ↔ (edgePieceEquiv cube e).flip = e := by
+        constructor <;> intro h
+        · rw [← EdgePiece.flip_inj, EdgePiece.flip₂]
+          exact (hc' _).resolve_left h
+        · conv_rhs => rw [← h]
+          exact (EdgePiece.flip_ne _).symm
+      obtain rfl | ha := eq_or_ne ⟦e⟧ a
+      · rw [Edge.flipEquiv_of_ne hl.1.1.symm]
+        simp [hl.1.2]
+        rw [← H, ← he]
+        exact List.mem_cons_self _ _
+      · obtain rfl | hb := eq_or_ne ⟦e⟧ b
+        · rw [Edge.flipEquiv_mk, Equiv.swap_apply_left, Edge.flipEquiv_of_ne, ← ne_eq]
+          simp [hl.2.1]
+          · rw [← H, ← he]
+            exact List.mem_cons_of_mem _ (List.mem_cons_self _ _)
+          · rw [Edge.mk_flip]
+            exact hl.1.1
+        · rw [Edge.flipEquiv_of_ne hb.symm, Edge.flipEquiv_of_ne ha.symm, ← ne_eq, ← he]
+          simp [ha, hb]
+    · simpa
+
+/-- A sequence of moves that puts the cube's edges in their correct orientation. -/
+def solveEdgePieces (cube : Rubik) : Moves := by
+  refine solveEdgePiecesAux ((Finset.univ.filter fun e : Edge ↦ e.lift
+    (fun e ↦ PRubik.edgePieceEquiv cube e ≠ e) ?_).sort (· ≤ ·))
+  intro e₁ e₂ h
+  obtain rfl | rfl := EdgePiece.equiv_iff.1 h <;> simp
+
+@[simp]
+theorem solveEdgePieces_solve (cube : Rubik) (hc : PRubik.edgeEquiv cube = 1) :
+    edgePieceEquiv (PRubik.move (solveEdgePieces cube)) = (edgePieceEquiv cube)⁻¹ := by
+  apply solveEdgePiecesAux_solve _ hc _ (Finset.sort_nodup _ _)
+  simp [edgeEquiv_mk]
+
+def test : Rubik := move [L, R, B, F]
+
+#eval (test * move (solveEdges test)) * move (solveEdgePieces (test * move (solveEdges test)))
 
 end Rubik

Rubik/Move.lean

@@ -408,4 +408,16 @@ namespace Rubik
 def move (m : Moves) : Rubik :=
   ⟨_, PRubik.isValid_move m⟩
 
+@[simp]
+theorem val_move (m : Moves) : (move m).val = PRubik.move m :=
+  rfl
+
+@[simp]
+theorem move_nil : move [] = 1 :=
+  rfl
+
+@[simp]
+theorem move_append (l m : Moves) : move (l ++ m) = move l * move m :=
+  Subtype.ext <| PRubik.move_append l m
+
 end Rubik

Rubik/PRubik.lean

@@ -119,7 +119,6 @@ abbrev Solved : PRubik := 1
 before the second's.
 
 This matches multiplication on `Equiv.Perm`, rather than the usual convention for functions. -/
-@[simps]
 instance : Mul PRubik :=
   ⟨fun cube₁ cube₂ ↦ by
     refine ⟨cube₁.edgePieceEquiv * cube₂.edgePieceEquiv,
@@ -129,6 +128,16 @@ instance : Mul PRubik :=
     · dsimp
       rw [cube₂.corner_cyclic, cube₁.corner_cyclic]⟩
 
+@[simp]
+theorem edgePieceEquiv_mul (cube₁ cube₂ : PRubik) :
+    (cube₁ * cube₂).edgePieceEquiv = cube₁.edgePieceEquiv * cube₂.edgePieceEquiv :=
+  rfl
+
+@[simp]
+theorem cornerPieceEquiv_mul (cube₁ cube₂ : PRubik) :
+    (cube₁ * cube₂).cornerPieceEquiv = cube₁.cornerPieceEquiv * cube₂.cornerPieceEquiv :=
+  rfl
+
 @[simp]
 theorem edge_flip_inv (cube : PRubik) (e : EdgePiece) :
     cube.edgePieceEquiv⁻¹ e.flip = (cube.edgePieceEquiv⁻¹ e).flip := by
@@ -163,6 +172,14 @@ instance : Inv PRubik :=
   ⟨fun cube ↦ ⟨cube.edgePieceEquiv⁻¹, cube.cornerPieceEquiv⁻¹,
     cube.edge_flip_inv, cube.corner_cyclic_inv⟩⟩
 
+@[simp]
+theorem edgePieceEquiv_inv (cube : PRubik) : cube⁻¹.edgePieceEquiv = cube.edgePieceEquiv⁻¹ :=
+  rfl
+
+@[simp]
+theorem cornerPieceEquiv_inv (cube : PRubik) : cube⁻¹.cornerPieceEquiv = cube.cornerPieceEquiv⁻¹ :=
+  rfl
+
 /-- The "pre-Rubik's cube" group. This isn't the true Rubik's cube group as it contains positions
 that are unreachable by valid moves. -/
 instance : Group PRubik where
@@ -426,6 +443,15 @@ theorem isValid_iff :
   rw [IsValid, invariant]
   simp only [MonoidHom.mem_ker, MonoidHom.prod_apply, Prod.mk_eq_one]
 
+theorem IsValid.parity (h : IsValid cube) : parity cube = 1 :=
+  (isValid_iff.1 h).1
+
+theorem IsValid.edgeFlip (h : IsValid cube) : edgeFlip cube = 1 :=
+  (isValid_iff.1 h).2.1
+
+theorem IsValid.cornerRotation (h : IsValid cube) : cornerRotation cube = 1 :=
+  (isValid_iff.1 h).2.2
+
 end PRubik
 
 /-- The subgroup of valid Rubik's cubes, i.e. those that can be reached using only valid moves. -/

Rubik/Piece.lean

@@ -99,6 +99,11 @@ theorem flip₂ (e : EdgePiece) : e.flip.flip = e :=
 theorem flip_inj {e₁ e₂ : EdgePiece} : e₁.flip = e₂.flip ↔ e₁ = e₂ :=
   (Function.LeftInverse.injective flip₂).eq_iff
 
+theorem flip_ne (e : EdgePiece) : e.flip ≠ e := by
+  rw [ne_eq, EdgePiece.ext_iff, flip_fst, flip_snd, not_and]
+  intro h
+  cases e.isAdjacent.ne h.symm
+
 /-- Constructs the finset containing the edge's orientations. -/
 def toFinset (e : EdgePiece) : Finset Orientation :=
   ⟨{e.fst, e.snd}, by simpa using e.isAdjacent.ne⟩
@@ -239,6 +244,18 @@ def flipEquiv (e : Edge) : Equiv.Perm EdgePiece :=
 theorem flipEquiv_mk (e : EdgePiece) : flipEquiv ⟦e⟧ = Equiv.swap e e.flip :=
   rfl
 
+theorem flipEquiv_of_ne {e : Edge} {a : EdgePiece} : e ≠ ⟦a⟧ → e.flipEquiv a = a := by
+  refine e.inductionOn ?_
+  intro e he
+  rw [ne_eq, Quotient.eq, @comm _ (· ≈ ·), EdgePiece.equiv_iff, not_or] at he
+  rw [flipEquiv_mk, Equiv.swap_apply_of_ne_of_ne he.1 he.2]
+
+@[simp]
+theorem mk_flipEquiv (e : Edge) (a : EdgePiece) : ⟦e.flipEquiv a⟧ = (⟦a⟧ : Edge) := by
+  obtain rfl | ha := eq_or_ne e ⟦a⟧
+  · simp
+  · rw [flipEquiv_of_ne ha]
+
 end Edge
 
 /-- A corner piece is an ordered triple of pairwise adjacent orientations, oriented as the standard