Skip to content

Commit 313545c

Browse files
jessealamajessealama
authored
Merge branch 'main' into sqrt-computable
2 parents 0a9b93c + 730f3c1 commit 313545c

1 file changed

Lines changed: 184 additions & 1 deletion

File tree

‎Urm/Partrec.lean‎

Lines changed: 184 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -626,14 +626,197 @@ theorem sqrt_computable : URMComputable 1 (fun x => Part.some (Nat.sqrt (x 0)))
626626

627627
end Sqrt
628628

629+
/-! ## Square Function -/
630+
631+
section Square
632+
633+
/-- The inner functions for squaring: (x, x) for multiplication. -/
634+
private def sqGs : Fin 2 → (Fin 1 → ℕ) → Part ℕ :=
635+
fun _ => fun x => Part.some (x 0)
636+
637+
@[simp] private theorem sqGs_eval (i : Fin 2) (x : Fin 1 → ℕ) : sqGs i x = Part.some (x 0) := rfl
638+
639+
/-- Helper: Composing mul with (x, x) computes x². -/
640+
private theorem sq_comp_eq (x : Fin 1 → ℕ) :
641+
compFunction 2 1 (fun ab => Part.some (ab 0 * ab 1)) sqGs x =
642+
Part.some (x 0 * x 0) := by
643+
simp only [compFunction, Part.sequence, sqGs_eval, Part.bind_some, Part.map_some]
644+
rfl
645+
646+
/-- Square function is URM-computable. sq(x) = x * x -/
647+
theorem sq_computable : URMComputable 1 (fun x => Part.some ((x 0) * (x 0))) := by
648+
have hgs : ∀ i, URMComputable 1 (sqGs i) := fun _ => URMComputable.proj_computable 1 0
649+
have h := URMComputable.comp_general (m := 2) (n := 1) mul_computable hgs
650+
convert h.toComputable using 1
651+
funext x
652+
exact (sq_comp_eq x).symm
653+
654+
end Square
655+
629656
/-! ## Pairing Functions -/
630657

631658
section Pairing
632659

660+
/-- The branchless formula for Cantor pairing equals Nat.pair.
661+
pair(a, b) = lt(a,b) * (b² + a) + (1 - lt(a,b)) * (a² + a + b) -/
662+
private theorem pair_branchless_eq (a b : ℕ) :
663+
(if a < b then 1 else 0) * (b * b + a) +
664+
(1 - if a < b then 1 else 0) * (a * a + a + b) =
665+
pair a b := by
666+
unfold pair
667+
by_cases h : a < b
668+
· simp [h]
669+
· simp [h]
670+
671+
-- Helper: b² is computable (as a 2-arg function extracting b)
672+
private def sqBGs : Fin 1 → (Fin 2 → ℕ) → Part ℕ :=
673+
fun _ => fun xy => Part.some (xy 1)
674+
675+
private theorem sqB_computable : URMComputableSF 2 (fun xy => Part.some ((xy 1) * (xy 1))) := by
676+
have hgs : ∀ i, URMComputable 2 (sqBGs i) := fun _ => URMComputable.proj_computable 2 1
677+
have h := URMComputable.comp_general (m := 1) (n := 2) sq_computable hgs
678+
convert h using 1
679+
funext xy
680+
simp only [compFunction, Part.sequence, sqBGs, Part.bind_some, Part.map_some, Fin.cons_zero]
681+
682+
-- Helper: a² is computable (as a 2-arg function extracting a)
683+
private def sqAGs : Fin 1 → (Fin 2 → ℕ) → Part ℕ :=
684+
fun _ => fun xy => Part.some (xy 0)
685+
686+
private theorem sqA_computable : URMComputableSF 2 (fun xy => Part.some ((xy 0) * (xy 0))) := by
687+
have hgs : ∀ i, URMComputable 2 (sqAGs i) := fun _ => URMComputable.proj_computable 2 0
688+
have h := URMComputable.comp_general (m := 1) (n := 2) sq_computable hgs
689+
convert h using 1
690+
funext xy
691+
simp only [compFunction, Part.sequence, sqAGs, Part.bind_some, Part.map_some, Fin.cons_zero]
692+
693+
-- Helper: b² + a is computable
694+
private def termLtGs : Fin 2 → (Fin 2 → ℕ) → Part ℕ :=
695+
fun i => if i.val = 0 then (fun xy => Part.some (xy 1 * xy 1)) else (fun xy => Part.some (xy 0))
696+
697+
private theorem termLt_computable : URMComputableSF 2 (fun xy => Part.some (xy 1 * xy 1 + xy 0)) := by
698+
have hgs : ∀ i, URMComputable 2 (termLtGs i) := by
699+
intro i; fin_cases i
700+
· simp only [termLtGs]; exact sqB_computable.toComputable
701+
· simp only [termLtGs]; exact URMComputable.proj_computable 2 0
702+
have h := URMComputable.comp_general (m := 2) (n := 2) add_computable hgs
703+
convert h using 1
704+
funext xy
705+
simp only [compFunction, Part.sequence, termLtGs, Part.bind_some, Part.map_some,
706+
Fin.val_zero, ↓reduceIte, Fin.cons_zero, Fin.cons_one,
707+
Fin.val_succ, Nat.add_one_ne_zero]
708+
709+
-- Helper: a² + a is computable
710+
private def sqAPlusAGs : Fin 2 → (Fin 2 → ℕ) → Part ℕ :=
711+
fun i => if i.val = 0 then (fun xy => Part.some (xy 0 * xy 0)) else (fun xy => Part.some (xy 0))
712+
713+
private theorem sqAPlusA_computable : URMComputableSF 2 (fun xy => Part.some (xy 0 * xy 0 + xy 0)) := by
714+
have hgs : ∀ i, URMComputable 2 (sqAPlusAGs i) := by
715+
intro i; fin_cases i
716+
· simp only [sqAPlusAGs]; exact sqA_computable.toComputable
717+
· simp only [sqAPlusAGs]; exact URMComputable.proj_computable 2 0
718+
have h := URMComputable.comp_general (m := 2) (n := 2) add_computable hgs
719+
convert h using 1
720+
funext xy
721+
simp only [compFunction, Part.sequence, sqAPlusAGs, Part.bind_some, Part.map_some,
722+
Fin.val_zero, ↓reduceIte, Fin.cons_zero, Fin.cons_one,
723+
Fin.val_succ, Nat.add_one_ne_zero]
724+
725+
-- Helper: a² + a + b is computable
726+
private def termGeGs : Fin 2 → (Fin 2 → ℕ) → Part ℕ :=
727+
fun i => if i.val = 0 then (fun xy => Part.some (xy 0 * xy 0 + xy 0)) else (fun xy => Part.some (xy 1))
728+
729+
private theorem termGe_computable : URMComputableSF 2 (fun xy => Part.some (xy 0 * xy 0 + xy 0 + xy 1)) := by
730+
have hgs : ∀ i, URMComputable 2 (termGeGs i) := by
731+
intro i; fin_cases i
732+
· simp only [termGeGs]; exact sqAPlusA_computable.toComputable
733+
· simp only [termGeGs]; exact URMComputable.proj_computable 2 1
734+
have h := URMComputable.comp_general (m := 2) (n := 2) add_computable hgs
735+
convert h using 1
736+
funext xy
737+
simp only [compFunction, Part.sequence, termGeGs, Part.bind_some, Part.map_some,
738+
Fin.val_zero, ↓reduceIte, Fin.cons_zero, Fin.cons_one,
739+
Fin.val_succ, Nat.add_one_ne_zero]
740+
741+
-- Helper: lt(a,b) * (b² + a) is computable
742+
private def mulLtGs : Fin 2 → (Fin 2 → ℕ) → Part ℕ :=
743+
fun i => if i.val = 0 then (fun xy => Part.some (if xy 0 < xy 1 then 1 else 0))
744+
else (fun xy => Part.some (xy 1 * xy 1 + xy 0))
745+
746+
private theorem mulLt_computable : URMComputableSF 2
747+
(fun xy => Part.some ((if xy 0 < xy 1 then 1 else 0) * (xy 1 * xy 1 + xy 0))) := by
748+
have hgs : ∀ i, URMComputable 2 (mulLtGs i) := by
749+
intro i; fin_cases i
750+
· simp only [mulLtGs]; exact lt_computable
751+
· simp only [mulLtGs]; exact termLt_computable.toComputable
752+
have h := URMComputable.comp_general (m := 2) (n := 2) mul_computable hgs
753+
convert h using 1
754+
funext xy
755+
simp only [compFunction, Part.sequence, mulLtGs, Part.bind_some, Part.map_some,
756+
Fin.val_zero, ↓reduceIte, Fin.cons_zero, Fin.cons_one,
757+
Fin.val_succ, Nat.add_one_ne_zero]
758+
759+
-- Helper: 1 - lt(a,b) is computable (ge indicator)
760+
private def geGs : Fin 2 → (Fin 2 → ℕ) → Part ℕ :=
761+
fun i => if i.val = 0 then (fun _ => Part.some 1)
762+
else (fun xy => Part.some (if xy 0 < xy 1 then 1 else 0))
763+
764+
private theorem ge_computable : URMComputableSF 2
765+
(fun xy => Part.some (1 - if xy 0 < xy 1 then 1 else 0)) := by
766+
have hgs : ∀ i, URMComputable 2 (geGs i) := by
767+
intro i; fin_cases i
768+
· simp only [geGs]; exact const_one_computable
769+
· simp only [geGs]; exact lt_computable
770+
have h := URMComputable.comp_general (m := 2) (n := 2) monus_computable hgs
771+
convert h using 1
772+
funext xy
773+
simp only [compFunction, Part.sequence, geGs, Part.bind_some, Part.map_some,
774+
Fin.val_zero, ↓reduceIte, Fin.cons_zero, Fin.cons_one,
775+
Fin.val_succ, Nat.add_one_ne_zero]
776+
777+
-- Helper: (1 - lt(a,b)) * (a² + a + b) is computable
778+
private def mulGeGs : Fin 2 → (Fin 2 → ℕ) → Part ℕ :=
779+
fun i => if i.val = 0 then (fun xy => Part.some (1 - if xy 0 < xy 1 then 1 else 0))
780+
else (fun xy => Part.some (xy 0 * xy 0 + xy 0 + xy 1))
781+
782+
private theorem mulGe_computable : URMComputableSF 2
783+
(fun xy => Part.some ((1 - if xy 0 < xy 1 then 1 else 0) * (xy 0 * xy 0 + xy 0 + xy 1))) := by
784+
have hgs : ∀ i, URMComputable 2 (mulGeGs i) := by
785+
intro i; fin_cases i
786+
· simp only [mulGeGs]; exact ge_computable.toComputable
787+
· simp only [mulGeGs]; exact termGe_computable.toComputable
788+
have h := URMComputable.comp_general (m := 2) (n := 2) mul_computable hgs
789+
convert h using 1
790+
funext xy
791+
simp only [compFunction, Part.sequence, mulGeGs, Part.bind_some, Part.map_some,
792+
Fin.val_zero, ↓reduceIte, Fin.cons_zero, Fin.cons_one,
793+
Fin.val_succ, Nat.add_one_ne_zero]
794+
795+
-- Final composition: pair(a,b) = mulLt + mulGe
796+
private def pairGs : Fin 2 → (Fin 2 → ℕ) → Part ℕ :=
797+
fun i => if i.val = 0 then (fun xy => Part.some ((if xy 0 < xy 1 then 1 else 0) * (xy 1 * xy 1 + xy 0)))
798+
else (fun xy => Part.some ((1 - if xy 0 < xy 1 then 1 else 0) * (xy 0 * xy 0 + xy 0 + xy 1)))
799+
800+
private theorem pair_comp_eq (xy : Fin 2 → ℕ) :
801+
compFunction 2 2 (fun ab => Part.some (ab 0 + ab 1)) pairGs xy =
802+
Part.some ((if xy 0 < xy 1 then 1 else 0) * (xy 1 * xy 1 + xy 0) +
803+
(1 - if xy 0 < xy 1 then 1 else 0) * (xy 0 * xy 0 + xy 0 + xy 1)) := by
804+
simp only [compFunction, Part.sequence, pairGs, Part.bind_some, Part.map_some,
805+
Fin.val_zero, ↓reduceIte, Fin.cons_zero, Fin.cons_one,
806+
Fin.val_succ, Nat.add_one_ne_zero]
807+
633808
/-- Pairing function is URM-computable.
634809
pair(a, b) = if a < b then b² + a else a² + a + b -/
635810
theorem pair_computable : URMComputable 2 (fun xy => Part.some (pair (xy 0) (xy 1))) := by
636-
sorry
811+
have hgs : ∀ i, URMComputable 2 (pairGs i) := by
812+
intro i; fin_cases i
813+
· simp only [pairGs]; exact mulLt_computable.toComputable
814+
· simp only [pairGs]; exact mulGe_computable.toComputable
815+
have h := URMComputable.comp_general (m := 2) (n := 2) add_computable hgs
816+
convert h.toComputable using 1
817+
funext xy
818+
rw [pair_comp_eq]
819+
exact congrArg Part.some (pair_branchless_eq (xy 0) (xy 1)).symm
637820

638821
/-- Left unpair component is URM-computable. -/
639822
theorem unpairLeft_computable : URMComputable 1 (fun x => Part.some (x 0).unpair.1) := by

0 commit comments

Comments
 (0)