I am thinking about "naive" set theory (again) in Coq. Here is my current experiment.

```
Definition Part (E : Type) := E -> Prop.
Definition is_in {E : Type} (x : E) (A : Part E) := (A x).
Inductive empty_part {E : Type} : Part E :=.
Inductive full_part (E : Type) : Part E := in_full (x : E) : is_in x (full_part E).
Notation "x ∈ A" := (is_in x A) (at level 50).
Notation "x ∉ A" := (~ is_in x A) (at level 50).
Notation "∅" := empty_part.
Coercion full_part : Sortclass >-> Part.
Lemma test' {E : Type} : ∅ ∈ Part E.
Proof. easy. Qed.
Lemma test'' {E : Type} (A : Part E) : A ∈ Part E.
Proof. easy. Qed.
Fail Check forall (E : Type), E ∈ Part E.
Definition included {E : Type} (A B : Part E) :=
forall (x : E), x ∈ A -> x ∈ B.
Notation "A ⊂ B" := (included A B) (at level 50).
Lemma included_full_r {E : Type} (A : Part E) : A ⊂ E.
Proof. now intros x _. Qed.
```

The perilous part is the coercion. I'm actually impressed that it already makes many things look like an introductory maths course.

However, this fails :

```
Fail Check forall (E : Type), E ∈ Part E.
```

with

```
The command has indeed failed with message:
In environment
E : Type
The term "Part E" has type "Type" while it is expected to have type
"Part Type".
```

- I don't really understand the error (to be honest, I can't say I really understand the coercion I wrote in the first place).
- Is there any way this could work, or is it hopeless and too dangerous?

According to the documentation on coercions, the source class has to be a user-defined class, so `Sortclass`

is not suitable.

You can define an alias `type_alias := Type`

and replace every occurence of `Type`

and `Sortclass`

with it. Coq will only need some help to figure out the correct implicit argument for `is_in`

, `(E : Part E) \in Part E`

works on my side.

Alternatively, you can make your version work with elpi using the `coercion`

predicate, but it requires a few things that have not yet been released, so you would need a custom build of coq and coq-elpi to try it for the time being.

Last updated: Jun 13 2024 at 19:02 UTC