computable out

Rubik/Card.lean

@@ -58,43 +58,48 @@ theorem cornerEquiv_of_mem_ker_edgeCornerEquiv (h : cube ∈ edgeCornerEquiv.ker
     cornerEquiv cube = 1 :=
   (mem_ker_edgeCornerEquiv.1 h).2
 
-/- It's perfectly possible to provide a constructive proof, but it's a bit easier to do this via
-choice. -/
-theorem edgeCornerEquiv_surjective : Function.Surjective edgeCornerEquiv := by
-  rintro ⟨f, g⟩
-  let f' : EdgePiece → EdgePiece := fun e ↦ let x := (f ⟦e⟧).out
-    if e = ⟦e⟧.out then x else x.flip
-  let g' : CornerPiece → CornerPiece := fun c ↦ let x := (g ⟦c⟧).out
-    if c = ⟦c⟧.out then x else if c = ⟦c⟧.out.cyclic then x.cyclic else x.cyclic.cyclic
-  refine ⟨⟨Equiv.Perm.ofSurjective f' ?_, Equiv.Perm.ofSurjective g' ?_, ?_, ?_⟩, ?_⟩
+/-- A computable inverse for `edgeCornerEquiv`. -/
+def edgeCornerEquiv_inv (p : Perm Edge × Perm Corner) : PRubik := by
+  let f' : EdgePiece → EdgePiece := fun e ↦ let x := (p.1 ⟦e⟧).out
+    if e = Edge.out ⟦e⟧ then x else x.flip
+  let g' : CornerPiece → CornerPiece := fun c ↦ let x := (p.2 ⟦c⟧).out
+    if c = Corner.out ⟦c⟧ then x else
+      if c = (Corner.out ⟦c⟧).cyclic then x.cyclic else x.cyclic.cyclic
+  refine ⟨Equiv.Perm.ofSurjective f' ?_, Equiv.Perm.ofSurjective g' ?_, ?_, ?_⟩
   · intro e
-    obtain he | he := EdgePiece.equiv_iff.1 (Quotient.mk_out e).symm
-    · use (f.symm ⟦e⟧).out
+    obtain he | he := EdgePiece.equiv_iff.1 (Edge.mk_out e).symm
+    · use (p.1.symm ⟦e⟧).out
       simpa [f'] using he.symm
-    · use (f.symm ⟦e⟧).out.flip
+    · use (p.1.symm ⟦e⟧).out.flip
       simpa [f'] using he.symm
   · intro c
-    obtain hc | hc | hc := CornerPiece.equiv_iff'.1 (Quotient.mk_out c).symm
-    · use (g.symm ⟦c⟧).out
+    obtain hc | hc | hc := CornerPiece.equiv_iff'.1 (Corner.mk_out c).symm
+    · use (p.2.symm ⟦c⟧).out
       simpa [g'] using hc.symm
-    · use (g.symm ⟦c⟧).out.cyclic
+    · use (p.2.symm ⟦c⟧).out.cyclic
       simpa [g'] using hc.symm
-    · use (g.symm ⟦c⟧).out.cyclic.cyclic
+    · use (p.2.symm ⟦c⟧).out.cyclic.cyclic
       simpa [g'] using hc.symm
   · intro e
     simp_rw [Perm.ofSurjective_apply, f']
-    obtain he | he := EdgePiece.equiv_iff.1 (Quotient.mk_out e) <;>
+    obtain he | he := EdgePiece.equiv_iff.1 (Edge.mk_out e) <;>
     simp [he, e.flip_ne.symm]
   · intro c
     simp_rw [Perm.ofSurjective_apply, g', Corner.mk_cyclic, CornerPiece.cyclic_inj]
-    obtain hc | hc | hc := CornerPiece.equiv_iff'.1 (Quotient.mk_out c) <;>
+    obtain hc | hc | hc := CornerPiece.equiv_iff'.1 (Corner.mk_out c) <;>
     simp [hc, c.cyclic_ne.symm, c.cyclic_cyclic_ne.symm]
-  · rw [edgeCornerEquiv_apply, Prod.mk.injEq]
-    constructor <;> ext x <;> refine x.inductionOn ?_ <;> intro x
-    · simp_rw [edgeEquiv_mk, f', Perm.ofSurjective_apply]
-      split_ifs <;> simp
-    · simp_rw [cornerEquiv_mk, g', Perm.ofSurjective_apply]
-      split_ifs <;> simp
+
+theorem edgeCornerEquiv_leftInverse : Function.LeftInverse edgeCornerEquiv edgeCornerEquiv_inv := by
+  intro x
+  rw [edgeCornerEquiv_apply, Prod.mk.injEq]
+  constructor <;> ext x <;> refine x.inductionOn ?_ <;> intro x
+  · simp_rw [edgeEquiv_mk, edgeCornerEquiv_inv, Perm.ofSurjective_apply]
+    split_ifs <;> simp
+  · simp_rw [cornerEquiv_mk, edgeCornerEquiv_inv, Perm.ofSurjective_apply]
+    split_ifs <;> simp
+
+theorem edgeCornerEquiv_surjective : Function.Surjective edgeCornerEquiv :=
+  edgeCornerEquiv_leftInverse.surjective
 
 /-- The kernel of `edgeCornerEquiv` consists of cubes with only their edges flipped and corners
 rotated. -/

Rubik/PRubik.lean

@@ -498,11 +498,11 @@ def invariant_inv : ℤˣ × ℤˣ × Multiplicative (ZMod 3) → PRubik :=
   fun ⟨a, b, c⟩ ↦ (swapEdges (default : EdgePiece).isAdjacent) ^ ((1 - a.1) / 2) *
     (flipEdge default) ^ b.toZMod.1 * (rotateCorner default) ^ c.1
 
-theorem invariant_rightInverse : Function.RightInverse invariant_inv invariant := by
+theorem invariant_leftInverse : Function.LeftInverse invariant invariant_inv := by
   decide
 
 theorem invariant_surjective : Function.Surjective invariant :=
-  invariant_rightInverse.surjective
+  invariant_leftInverse.surjective
 
 /-- A Rubik's cube is valid when it has invariant 1. We show that this condition is equivalent to
 being solvable. -/

Rubik/Piece.lean

@@ -221,6 +221,17 @@ unsafe instance : Repr Edge :=
 instance : LinearOrder Edge :=
   LinearOrder.lift' (fun e ↦ Finset.Colex.toColex e.toFinset) (fun _ _ ↦ by simp)
 
+/-- Computably chooses an edge piece equivalent to this edge. -/
+def out (e : Edge) : EdgePiece :=
+  (Finset.univ.sort (· ≤ ·)).choose (fun x ↦ ⟦x⟧ = e) ⟨Quotient.out e, by simp⟩
+
+@[simp]
+theorem out_eq (e : Edge) : ⟦e.out⟧ = e :=
+  (List.choose_spec (fun x ↦ ⟦x⟧ = e) _ _).2
+
+theorem mk_out (e : EdgePiece) : Edge.out ⟦e⟧ ≈ e :=
+  Quotient.exact (out_eq _)
+
 /-- Given an edge and an orientation it contains, you can recover a unique edge piece within that
 edge with that orientation.
 
@@ -572,6 +583,17 @@ unsafe instance : Repr Corner :=
 instance : LinearOrder Corner :=
   LinearOrder.lift' (fun c ↦ Finset.Colex.toColex c.toFinset) (fun _ _ ↦ by simp)
 
+/-- Computably chooses a corner piece equivalent to this corner. -/
+def out (c : Corner) : CornerPiece :=
+  (Finset.univ.sort (· ≤ ·)).choose (fun x ↦ ⟦x⟧ = c) ⟨Quotient.out c, by simp⟩
+
+@[simp]
+theorem out_eq (c : Corner) : ⟦c.out⟧ = c :=
+  (List.choose_spec (fun x ↦ ⟦x⟧ = c) _ _).2
+
+theorem mk_out (c : CornerPiece) : Corner.out ⟦c⟧ ≈ c :=
+  Quotient.exact (out_eq _)
+
 /-- Given a corner and an axis, you can recover a unique corner piece within that corner with that
 axis. -/
 def toCornerPiece (c : Corner) (a : Axis) : CornerPiece :=