Work effectively with Lean 4 quotients in ComputationalPaths (Quot.lift/Quot.ind/Quot.sound), including nested lifts and common proof obligations.
Work with Lean 4 quotients in ComputationalPaths.
def myFun : Quot r → B :=
Quot.lift
(fun x => f x) -- function on representatives
(fun a b h => ...) -- proof: r a b → f a = f b
Quot.sound : r a b → Quot.mk r a = Quot.mk r b
theorem my_thm (q : Quot r) : P q := by
induction q using Quot.ind with
| _ x => ... -- prove for representative
For Quot r → Quot s → C, use nested lifts:
def myFun₂ : Quot r → Quot s → C :=
Quot.lift
(fun a => Quot.lift
(fun b => f a b)
(fun b₁ b₂ h => ...))
(fun a₁ a₂ h => funext (Quot.ind (fun b => ...)))
Quot.liftOn₂ in Lean 4 - use nested Quot.liftfunext + Quot.indnoncomputable def circleCompPathEncode : circleCompPathPiOne → Int :=
Quot.lift
circleCompPathEncodeExpr'
(fun _ _ h => h)