Dear HBers,

I'm reading this page from the HB wiki.

It states that copying instances are possible when types are convertible.

What are convertible types?

What type class would I need to implement?

Thanks a lot for any pointers.

Two terms (e.g. types) are convertible if they are equal modulo some conversion rules (like alpha-conversion and beta-reduction), see https://coq.inria.fr/doc/V8.19.0/refman/language/core/conversion.html#term-convertible.

Regarding the type class question, I am not sure to understand what you mean. Do you have a specific example in mind?

I ultimately would like to specify `{set prime'}`

, a type for the set of prime numbers.

```
Inductive prime' : Type := Prime' (x: 'I_n.+1) (_ : prime x).
```

But this errors:

```
Fail Definition xxx : {set (prime' n)}.
```

with

```
The term "Phant prime'" has type "phant prime'" while it is expected to have type "phant (Finite.sort ?T)".
```

Here is what I have so far:

```
Definition eqprime (p1 p2 : prime') :=
match p1,p2 with
| Prime' x1 _, Prime' x2 _ => x1 == x2
end.
Lemma eqprimeP : Equality.axiom eqprime.
Proof.
case => [p₁ h₁] [p₂ h₂] /=. rewrite /eqprime.
case H : (p₁ == p₂).
- apply ReflectT.
move/eqP:H => H.
move: h₁ h₂. rewrite H => h₁ h₂.
f_equal.
apply bool_irrelevance.
- apply ReflectF.
move/eqP:H => H.
injection => H₀.
contradiction.
Qed.
HB.instance Definition _ := hasDecEq.Build prime' eqprimeP.
```

All of this works.

Now I wanted to do this:

```
HB.instance Definition _ := Finite.on prime'.
```

and get

```
Error: Definition illtyped: The term "Finite.phant_on_ (Phant ?t)" has type
"Finite.axioms_ (Finite.sort ?t)" while it is expected to have type
"Finite.axioms_ prime'".
```

Here, `prime'`

is not convertible to anything that already is an instance of `Finite`

, so HB does not find the instance you are trying to declare. You probably want to start with the fact that `prime'`

is a subType of `'I_n.+1`

and then derive all the instances you want (`eqType`

, `choiceType`

, etc.). Alternatively, you can define `prime'`

as a sigma type, on which the instance would be automatically inferred.

Last updated: Oct 13 2024 at 01:02 UTC