Stream: Beginner Questions

Topic: Big Oh Basic Proof Failing: Type unification failed: No type

zigzagdoom (Jan 29 2024 at 19:54):

Hi,

I am a beginner learning to use Isabelle. I am trying to define big Oh, and prove a basic property. However, I am getting failures:

theory Scratch
  imports Main "HOL.Real"

begin

definition big_O :: "(nat ⇒ real) ⇒ (nat ⇒ real) ⇒ bool" (infix "∈ O" 50)
  where "f ∈ O g ⟷ (∃c>0. ∃n0. ∀n≥n0. abs (f n) ≤ c * abs (g n))"

lemma square_in_O_square_plus_linear: "λn. of_nat (n * n) ∈ O (λn. of_nat (n * n) + of_nat n)"

end

The issue I get is:

Type unification failed: No type arity fun :: semiring_1

Type error in application: incompatible operand type

Operator:  (∈ O) :: (nat ⇒ real) ⇒ (nat ⇒ real) ⇒ bool
Operand:   of_nat (n * n) :: ??'a

Coercion Inference:

Local coercion insertion on the operand failed:
No type arity fun :: semiring_1

Now trying to infer coercions globally.

Coercion inference failed:
weak unification of subtype constraints fails
Clash of types "_ ⇒ _" and "bool"

Why is the type inference failing? I have converted to reals using of_nat?

Any help is greatly appreciated.

Mathias Fleury (Jan 29 2024 at 20:02):

I am doing Isabelle for too long apparently, because I find the error message very clear actually

Mathias Fleury (Jan 29 2024 at 20:03):

The typing error indicates that Isabelle parses your expression as (∈ O) (of_nat (n * n))

Mathias Fleury (Jan 29 2024 at 20:03):

which is not what you want

Mathias Fleury (Jan 29 2024 at 20:06):

If can live with ambiguous parse trees:

definition big_O :: "(nat ⇒ real) ⇒ (nat ⇒ real) ⇒ bool" ("_ ∈ O _" 99)
  where "(f ∈ O g) ⟷ (∃c>0. ∃n0. ∀n≥n0. abs (f n) ≤ c * abs (g n))"

lemma square_in_O_square_plus_linear: "λn. of_nat (n * n) ∈ O (λn. of_nat (n * n) + of_nat n)"

zigzagdoom (Jan 29 2024 at 22:29):

Mathias Fleury said:

I am doing Isabelle for too long apparently, because I find the error message very clear actually

Thank you @Mathias Fleury ,

Is there any way I can avoid the ambiguity caused by ∈ O?

Yong Kiam (Jan 30 2024 at 04:21):

you may want to check out how it was set up by Manuel Eberl: https://isabelle.in.tum.de/library/HOL/HOL-Library/Landau_Symbols.html (short answer: O actually gives you a set, and \in is actually set inclusion)

Last updated: Apr 27 2024 at 12:25 UTC