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?

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

Wait, `deTy t`

and `t`

themselves have a similar structure. Can I copy `t`

structure to `deTy t`

?

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.

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.about deTy.
(*
HB: deTy is canonically equipped with structures:
- eqtype.Equality
(from "(stdin)", line 1)
*)
```

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?

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

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.about deTy. (* 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.

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`

).

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

Last updated: Jul 15 2024 at 20:02 UTC