mirror of
https://github.com/allaunthefox/Research-Stack.git
synced 2026-07-31 03:05:21 +00:00
55 lines
2 KiB
Python
55 lines
2 KiB
Python
import os
|
|
import sys
|
|
from infra.deepseek_adapter import DeepSeekV4, DeepSeekProver
|
|
|
|
def resolve_triangle_closure():
|
|
client = DeepSeekV4(use_local=True)
|
|
prover = DeepSeekProver(client)
|
|
|
|
# Provide the actual code from the library for context
|
|
context = """
|
|
import Semantics.RealityContractMassNumber
|
|
namespace HolyDiver.ENE
|
|
|
|
structure AdmissibilityEdge where
|
|
u : CandidateRecord
|
|
v : CandidateRecord
|
|
cost : Score
|
|
symm : cost = cost
|
|
|
|
def Path := List AdmissibilityEdge
|
|
|
|
def pathCost (p : Path) : Score :=
|
|
p.foldl (fun acc e => acc.add e.cost) { num := 0, den := 1, den_ne := by simp }
|
|
|
|
def is_path (g : AdmissibilityGraph) (x y : CandidateRecord) (p : Path) : Prop :=
|
|
match p with
|
|
| [] => x = y
|
|
| [e] => e.u = x ∧ e.v = y ∧ e ∈ g.edges ∧ edgeAdmissible g e
|
|
| e :: es => e.u = x ∧ e ∈ g.edges ∧ edgeAdmissible g e ∧ is_path g e.v y es
|
|
|
|
def allPaths (g : AdmissibilityGraph) (x y : CandidateRecord) : Set Path :=
|
|
{p | is_path g x y p}
|
|
|
|
def shortestPathDist (g : AdmissibilityGraph) (x y : CandidateRecord) : Score :=
|
|
-- We assume a well-defined infimum of pathCosts for all p in allPaths g x y
|
|
-- For this proof, just use the property:
|
|
-- for any p such that is_path g x y p, shortestPathDist g x y ≤ pathCost p
|
|
|
|
Theorem to prove:
|
|
theorem shortestPathDist_triangle (g : AdmissibilityGraph) (x y z : CandidateRecord) :
|
|
Score.le (shortestPathDist g x z) ((shortestPathDist g x y).add (shortestPathDist g y z))
|
|
|
|
Hint: If p1 is a path from x to y and p2 is a path from y to z,
|
|
then p1 ++ p2 is a path from x to z.
|
|
And pathCost (p1 ++ p2) = (pathCost p1).add (pathCost p2).
|
|
Since shortestPathDist x z is the infimum, it must be ≤ pathCost (p1 ++ p2).
|
|
"""
|
|
|
|
print("Generating proof for shortestPathDist_triangle...")
|
|
proof = prover.formalize(context)
|
|
print("\nProposed Proof:\n", proof)
|
|
return proof
|
|
|
|
if __name__ == "__main__":
|
|
resolve_triangle_closure()
|