logoalt Hacker News

auggierose • yesterday at 8:41 PM • 1 reply • view on HN

Yes, I know what you mean, but there is a relationship, it is just that some of that relationship is described outside of Isabelle, but nevertheless provably. Ultimately, math is like that, provably so.

You could do what you want by making that argument explicit formally and machine-checked, but then you have to do a lot more work, by translating all of the components of the informal proof into formal ones. This will not give you any more insight than what the book already describes. But of course you could take it as an example of something that should be easy once you grasp the informal proof, but is actually quite a lot of work.

Replies

dwohnitmok • yesterday at 11:23 PM

> You could do what you want by making that argument explicit formally and machine-checked, but then you have to do a lot more work, by translating all of the components of the informal proof into formal ones.

I don't see how you can. This is why I posed my question originally. Let me make the question sharper.

Here's some Isabelle code on the very simple function `double` that just doubles a natural number.

  theory Double
    imports Main
  begin
  
  fun double :: "nat => nat" where
    "double 0 = 0"
  | "double (Suc n) = Suc (Suc (double n))"
  
  lemma double_eq_plus: "double x = x + x"
    by (induction x) auto
  
  lemma double_eq_times: "double x = 2 \* x"
    by (induction x) auto
  
  end
How do I even begin to write the formal argument that `double` has asymptotic runtime complexity that is linear in the size of its argument without resorting to `time_f`-style shenanigans?

I don't know how to even state it in Isabelle. Let alone prove it.