## Stream: Coq users

### Topic: Coercion from a type E to E -> Prop

#### Pierre Rousselin (Nov 24 2023 at 17:32):

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".

1. 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).
2. Is there any way this could work, or is it hopeless and too dangerous?

#### Quentin VERMANDE (Nov 24 2023 at 21:02):

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