Stream: Coq users

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


view this post on Zulip 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?

view this post on Zulip 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