CODEWITHSUNDEEP
sethigher-order-functionsisabelletheorem-provingisar
Hai Nguyen Van
Hai Nguyen Van

Reputation: 35

Create a quotient-lifted type with polymorphism over working set and equivalence relation in Isabelle/HOL

I would like to create a quotient type with quotient_type in Isabelle/HOL in which I would left "non-constructed" the non-empty set S and the equivalence relation ≡. The goal is for me to derive generic properties w.r.t. S and ≡ over the quotient-lifted set S/≡. In this way, it would be interesting that Isabelle/HOL accepts dependent types... But I was told that was not possible.

Hence, I tried this

(* 1. Defining an arbitrary set and its associated type *)
consts S :: "'a set"
typedef ('a) inst = "{ x :: 'a. ¬ S = ({} :: 'a set) ⟶ x ∈ S}" by(auto)

(* 2. Defining the equivalence relation *)
definition equiv :: "'a ⇒ 'a ⇒ bool" where
  "equiv x y = undefined"
  (* here needs a property of equivalence relationship... *)

(* 3. Defining the quotiented set *)
quotient_type ('a) quotiented_set = "('a inst × 'a inst)" / "equiv"
(* Hence, impossible end proof here... *)

Is this formalization, there appears to be two problems

  1. I don't think this is the cleanest way to define an arbitrary set S as I can't specify it to be non-empty...
  2. I can't define an arbitrary equivalence relation equiv with the definition nor the fun commands as they only allow me define "constructive-strongly normalizing-inductive" definitions only... And yet, I want to say that I just have some function equiv that satisfies properties of equivalence (reflexivity, symmetry, transitivity).

Do you have any idea ? Thanks.

Upvotes: 0

Views: 90

Answers (1)

Andreas Lochbihler
Andreas Lochbihler

Reputation: 5078

HOL types cannot depend on values. So if you want to define a quotient type for an arbitrary non-empty set S and equivalence relation equiv using quotient_type, the arbitrary part must stay at the meta-level. Thus, S and equiv can either be axiomatized or defined such that you can convince yourself that you really have captured the desired notion of arbitrary.

If you axiomatize S and equiv, then you yourself are responsible that the axioms are consistent with the other axioms of HOL. You can do that with the command axiomatization as in

axiomatization S :: "'a set" where S_not_empty: "S ≠ {}"

For Isabelle/HOL, S is then a fixed constant of which you only know that it is not empty. You will never be able to instantiate S, because the arbitrariness only exists in the set-theoretic interpretation of Isabelle/HOL.

If you do not want to add new axioms, you can use specification instead:

consts S :: "'a set"
specification (S) S_not_empty: "S ≠ {}" by auto

With specification, you have to prove that your axioms are consistent, so there is no danger here. However, S no longer is absolutely arbitrary, because it is defined in terms of the choice operator Eps, as can be seen from the generated theorem S_def.

If you really want to study the theory of quotients within Isabelle/HOL, I recommend that you do not use types, but ordinary sets. There is the quotient operator op // and some theorems in the theory Equiv_Relations which is part of the library.

Upvotes: 1

Related Questions