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: Oct 13 2024 at 01:02 UTC