Making a dependent type eqType · math-comp users

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): 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").
*)

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

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

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.

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):

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).

Stream: math-comp users

Topic: Making a dependent type eqType

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