Idris中congruentialMethod函数优化：免传证明与非零Nat验证

Let's walk through how to fix those annoying proof and performance issues step by step:

1. Stop Passing Proofs to congruentialMethod #

The key here is to encapsulate your fixed modulus m and its non-zero proof inside the function, so callers never have to deal with them. Here's a clean implementation:

congruentialMethod : Nat -> Nat
congruentialMethod x = modNatNZ (a * x + c) m mNonZero
  where
    -- Your LCG parameters
    a : Nat
    a = 16807
    c : Nat
    c = 0
    m : Nat
    m = 2147483647

    -- Proof that m is non-zero, hidden internally
    mNonZero : NonZero m
    mNonZero = IsSucc (rewrite plusCommutative 2147483646 1 in Refl)

Now your function signature stays clean—no proof parameters required. The proof is only used behind the scenes.

2. Simplify the Non-Zero Proof for m #

That rewrite trick works, but there are even cleaner options since m is a known positive constant:

Option A: Use believe_me (Safe for Fixed Values) #

Since we know 2147483647 is a positive natural number, we can safely use believe_me to skip tedious proof construction. This is totally acceptable here because the value is fixed and can't be negative:

mNonZero : NonZero m
mNonZero = believe_me IsSucc

Option B: Use a Hint for Auto Proof Search #

If you prefer a slightly more formal approach without the rewrite, define a global hint so Idris can automatically find the proof when needed:

%hint
mNonZero : NonZero 2147483647
mNonZero = IsSucc (rewrite plusCommutative 2147483646 1 in Refl)

-- Then reference the hint with %search in your function
congruentialMethod : Nat -> Nat
congruentialMethod x = modNatNZ (a * x + c) 2147483647 %search
  where
    a = 16807
    c = 0

3. Fix Nat's Slow Performance Without partial #

Nat's arbitrary-precision design makes it slow for numerical computations. Instead, use Integer (unbounded) or Int (fixed-size) with assert_total to keep your function total while boosting speed:

congruentialMethod : Int -> Int
congruentialMethod x = assert_total $ (a * x + c) `mod` m
  where
    a = 16807
    c = 0
    m = 2147483647

assert_total tells Idris you guarantee this function will terminate and avoid undefined behavior (which is true here because m is non-zero, and your LCG operations are well-behaved for valid inputs). This lets you ditch partial entirely while keeping performance snappy.

内容的提问来源于stack exchange，提问作者user483036