Stream: Beginner Questions

Topic: Datatype issuue -Greedy Algorithm of Greedoids

Shriya M (Jun 22 2024 at 12:11):

Hi everyone,
I'm trying to formalize the greedy algorithm of greedoids and have a couple of quick questions regarding the same.

locale greedoid =
  fixes E :: "'a set"
  fixes F :: "'a set"
  assumes contains_empty_set: "{} ∈ F"
  assumes third_condition: "(X Y ∈ F) ∧ (card X > card Y) ⟹ ∃x ∈ X - Y.  Y ∪ {x} ∈ F"

Here is the error message I get for the same:

Type unification failed

Type error in application: incompatible operand type

Operator:  (∈) {} :: ??'a set set ⇒ bool
Operand:   F :: 'a set

In this case, E,F is a set system (E is any aribitrary set, and F is any set of subsets of E). I understand that I have to define the type of F differently (maybe sets of sets), but how do I do that?

2. Here's the definition of what it means for a set of subsets to be closed under union:

definition closed_under_union where "closed_under_union F ⟷ X Y ∈ F ⟹ X ∪ Y ∈ F"

The error message is:

Type unification failed: Clash of types "_ ⇒ _" and "_ set"

Type error in application: incompatible operand type

Operator:  (∪) :: ??'a set ⇒ ??'a set ⇒ ??'a set
Operand:   X :: ??'b ⇒ ??'c

How do I fix the type of X?

Thank you!

Mathias Fleury (Jun 22 2024 at 12:50):

1. fixes F :: "'a set" is defining the type. Change that line…

Mathias Fleury (Jun 22 2024 at 12:51):

assuming that each element of F is a subset of E is obvious

Mathias Fleury (Jun 22 2024 at 12:53):

2. I assume that you want `X∈ F ⟹Y ∈ F⟹...

Mathias Fleury (Jun 22 2024 at 12:53):

The question has no relation to datatypes unlike the title (there is not even a datatype !)

Mathias Fleury (Jun 22 2024 at 12:54):

And I recommend starting with an Isabelle tutorial like the prog prove

Shriya M (Jun 22 2024 at 13:08):

Thanks!

Last updated: Dec 21 2024 at 16:20 UTC