Comment by dwohnitmok

> That's why you need to modify the type system, obviously. That is not a problem.

What typing judgment rules would you have for RUNTIME?

> On the other hand, if you can prove f x = g x for all x, then you should be able to prove RUNTIME f x = RUNTIME g x as well, simply by noting that f = g, and x = x, and therefore RUNTIME f x = RUNTIME g x as well by the usual extensionality rule that would also apply to RUNTIME.

Yes that's the problem.

Take factorial.

  fun factorial :: "nat => nat" where
    "factorial 0 = 1"
  | "factorial (Suc n) = (Suc n) * factorial n

I can then define

  fun factorial_10_hardcoded :: "nat => nat" where 
    "factorial 10 = 3628800"
  | "factorial 0 = 1"
  | "factorial (Suc n) = (Suc n) * factorial n"

Clearly `factorial_10_hardcoded = factorial` for all `x`. Hence `RUNTIME f x = RUNTIME g x`. `RUNTIME factorial_10_hardcoded 10 <= 1` and therefore `RUNTIME factorial 10 <= 1`. So that gives you constant time for any particular constant input. But it gets even worse!

  factorial_hardcoded_a_b "nat => nat => nat => nat" where
    "factorial_hard_coded_a_b a b x = if x=a then b else factorial x

And of course `RUNTIME factorial_hardcoded_a_b x b x <= 1`.

Then I can prove

  FORALL n. EX b. factorial n = factorial_hardcoded_a_b n b n

which then means I can conclude `RUNTIME factorial n <= 1`.