## Stream: math-comp users

### Topic: Making a dependent type eqType

#### Julin Shaji (Apr 06 2024 at 08:07):

How can we make a dependent type an eqType using hierarchy-builder?

For non-dependent type, we could do like this:

``````From mathcomp Require Import all_ssreflect.
From HB Require Import structures.

Inductive t: Type :=
| One: t
| Add: t -> t -> t.

Axiom teqb: t -> t -> bool.
Axiom teqP: forall (a b: t), reflect (a=b) (teqb a b).
HB.instance Definition _ := hasDecEq.Build t teqP.
``````

But how would we do for a dependent type?

``````Fixpoint deTy (ty: t): Type :=
match ty with
| One => unit
| Add a b => (deTy a) + (deTy b)
end.

Axiom deqb: forall {ty: t}, deTy ty -> deTy ty -> bool.
Axiom deqP: forall (ty: t) (a b: deTy ty), reflect (a=b) (deqb a b).

HB.instance Definition _  {ty: t} := hasDecEq.Build (deTy ty) deqP.
(*
Definition illtyped: In environment
ty : t
The term "deqP" has type
"forall (ty : t) (a b : deTy ty), reflect (a = b) (deqb a b)"
while it is expected to have type "Equality.axiom (T:=deTy ty) ?r"
(cannot unify "deTy ty" and "t").
*)
``````

How can this be fixed?

#### Julin Shaji (Apr 06 2024 at 08:09):

Assuming that we couldn't find a predefined type from which can 'copy' the eqType structure.

#### Julin Shaji (Apr 06 2024 at 08:10):

Wait, `deTy t` and `t` themselves have a similar structure. Can I copy `t` structure to `deTy t`?

#### Quentin VERMANDE (Apr 06 2024 at 09:01):

The error message is correct. It is not clear yet what the solution is because we do not see what hides behind `Equality.axiom`, so do `Print Equality.axiom` and you will see what happens.
Regarding `copy`, you can always try.

#### Julin Shaji (Apr 06 2024 at 10:23):

Okay, I guess it couldn't infer `Equality.axiom` implicit argument.
As I was going on trying to construct one manually, I ended up making
a section.
That somehow allowed Coq to figure it out by itself.

``````Fixpoint deTy (ty: t): Type :=
match ty with
| One => unit
| Add a b => (deTy a) + (deTy b)
end.
Section Foo.
Context {ty: t}.
Axiom deqb: deTy ty -> deTy ty -> bool.
Axiom deqP: forall (a b: deTy ty), reflect (a=b) (deqb a b).
HB.instance Definition _  := hasDecEq.Build (deTy ty) deqP.
End Foo.

(*
HB: deTy is canonically equipped with structures:
- eqtype.Equality
(from "(stdin)", line 1)
*)
``````

#### Julin Shaji (Apr 06 2024 at 10:31):

Hmm..

When I tried to make the type `finType`, I got non-forgetful
inheritance warning.

``````From mathcomp Require Import all_ssreflect.
From HB Require Import structures.

Inductive t: Type :=
| One: t
| Add: t -> t -> t.

Axiom teqb: t -> t -> bool.
Axiom teqP: forall (a b: t), reflect (a=b) (teqb a b).
HB.instance Definition _ := hasDecEq.Build t teqP.

Fixpoint deTy (ty: t): finType :=
match ty with
| One => unit
| Add a b => (deTy a) + (deTy b)
end%type.
Section Foo.
Context {ty: t}.
Axiom deqb: deTy ty -> deTy ty -> bool.
Axiom deqP: forall (a b: deTy ty), reflect (a=b) (deqb a b).
HB.instance Definition _  := hasDecEq.Build (deTy ty) deqP.
(*
HB_unnamed_factory_19 is defined

non forgetful inheritance detected.
You have two solutions:
1. (Best practice) Reorganize your hierarchy to make eqtype_hasDecEq
depend on fintype_Finite. See the paper "Competing inheritance paths in
dependent type theory" (https://hal.inria.fr/hal-02463336) for more
explanations
2. Use the attribute #[non_forgetful_inheritance] to disable this check.
We strongly advise you encapsulate this instance inside a module,
in order to isolate it from the rest of the code, and to be able
to import it on demand. See the above paper and the file
https://github.com/math-comp/hierarchy-builder/blob/master/tests/non_forgetful_inheritance.v
to witness devastating effects.
[HB.non-forgetful-inheritance,HB,elpi,default]

eqtype_hasDecEq__to__eqtype_hasDecEq is defined
*)
End Foo.
``````

What does making hasDecEq dependent on fintype mean?

#### Julin Shaji (Apr 06 2024 at 10:32):

The paper seems to deal with the innards of HB. Looks like it will take some time to digest that..

#### Quentin VERMANDE (Apr 06 2024 at 11:26):

Julin Shaji said:

Okay, I guess it couldn't infer `Equality.axiom` implicit argument.
As I was going on trying to construct one manually, I ended up making
a section.
That somehow allowed Coq to figure it out by itself.

``````Fixpoint deTy (ty: t): Type :=
match ty with
| One => unit
| Add a b => (deTy a) + (deTy b)
end.
Section Foo.
Context {ty: t}.
Axiom deqb: deTy ty -> deTy ty -> bool.
Axiom deqP: forall (a b: deTy ty), reflect (a=b) (deqb a b).
HB.instance Definition _  := hasDecEq.Build (deTy ty) deqP.
End Foo.

(*
HB: deTy is canonically equipped with structures:
- eqtype.Equality
(from "(stdin)", line 1)
*)
``````

There is no implicit `Equality.axiom` argument, `deqP` had type `forall ty : t, Equality.axiom (dety ty) (deqb ty)`, so you simply needed to write `(deqP ty)` instead of `deqP`. Putting everything inside a section also works because it allows you to define `deqP` so that it does not have this argument as long as you stay inside the section.

#### Quentin VERMANDE (Apr 06 2024 at 11:40):

I think the issue is that since `deTy t` is a `finType`, it is in particular already an `eqType` and so HB does not like the fact that you declare another instance of `eqType`.
I think making `hasDecEq` depend on `Finite` means something like `hasDecEq` should have a parameter that is an instance of `Finite` (which does not makes sense since `Finite` already depends on `hasDecEq`).

#### Julin Shaji (Apr 08 2024 at 05:05):

Oh.. I missed the finType being eqType part. Thanks.

Last updated: Jul 15 2024 at 20:02 UTC