Stream: General

Topic: Proving set membership in a type

Gergely Buday (Jun 14 2023 at 14:38):

locale monoid =
  fixes Monoid and composition (infixl "oMonoid" 70) and unitMonoid
  assumes composition_closed [intro, simp]: "⟦ a ∈ Monoid; b ∈ Monoid ⟧ ⟹ a oMonoid b ∈ Monoid"
    and unit_closed [intro, simp]: "unitMonoid ∈ M"
    and associative [intro]: "⟦ a ∈ Monoid; b ∈ Monoid; c ∈ Monoid ⟧ ⟹ (a oMonoid b) oMonoid c = a oMonoid (b oMonoid c)"
    and left_unit [intro, simp]: "a ∈ Monoid ⟹ unitMonoid oMonoid a = a"
    and right_unit [intro, simp]: "a ∈ Monoid ⟹ a oMonoid unitMonoid = a"

interpretation list: monoid where
  Monoid = "char list" and
  composition = List.append and
  unitMonoid = "[]"
  apply (unfold_locales)
  apply auto

gives

proof (prove)
goal (2 subgoals):
 1. ⋀a b. a ∈ char list ⟹ b ∈ char list ⟹ a @ b ∈ char list
 2. ⋀M. [] ∈ M

which seem to be trivial, these set memberships follow from the properties of char list, the type.

But how can I convince Isabelle about them?

Fabian Huch (Jun 14 2023 at 14:46):

I think you're mixing up types and terms here. You can't quantify over types in Isabelle, you have to prove set membership of the sets "char list" and "M" here. Of course that doesn't hold, [] is certainly not in any set.

Fabian Huch (Jun 14 2023 at 14:47):

Monoid is a variable (not a type), no matter if you spell it upper- or lowercase.

Gergely Buday (Jun 14 2023 at 15:13):

@Fabian Huch I did Monoid = "UNIV :: char list set"but that did not eliminate the spurious ⋀M. [] ∈ M subgoal.

Fabian Huch (Jun 14 2023 at 15:18):

Then your definition does make sense, the problem with M is just that it's not mentioned anywhere else. I think you meant Monoid? (in the locale specification)

Gergely Buday (Jun 14 2023 at 18:45):

Oh yes, I have failed to rename M to Monoid at one instance, thanks.

Last updated: May 02 2024 at 08:19 UTC