Stream: math-comp users

Topic: Making a dependent type eqType


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

view this post on Zulip Julin Shaji (Apr 06 2024 at 08:09):

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

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

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

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

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

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

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

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

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