Hi,

Following the recent release of hol2dk by @Frédéric Blanqui , a small part of the HOL-Light library was translated into Coq: 448 lemmas, including some material on natural numbers -- to achieve this, a mapping of the HOL type `num`

to the Coq type `nat`

was defined (file coq.v). I would like to see if this translation can be extended, for instance to lists.

Translating the HOL-Light files up to lists into Coq generates a number of axioms such as

```
Axiom axiom_9 : forall {A : Type'} (a : recspace A), (@_mk_rec A (@_dest_rec A a)) = a.
```

(where `recspace`

comes from the file `ind_types.ml`

of the hol-light library), with`recspace`

, `_mk_rec`

, and `_dest_rec`

taken as axioms such as

```
Axiom recspace : Type' -> Type'.
Axiom _mk_rec : forall {A : Type'}, (nat -> A -> Prop) -> recspace A.
Axiom _dest_rec : forall {A : Type'}, (recspace A) -> nat -> A -> Prop.
```

In the hol-light library , the type `recspace`

is defined as follows (`ind_types.ml`

).

```
(* ------------------------------------------------------------------------- *)
(* Carve out an inductively defined set. *)
(* ------------------------------------------------------------------------- *)
let ZRECSPACE_RULES,ZRECSPACE_INDUCT,ZRECSPACE_CASES =
new_inductive_definition
`ZRECSPACE (ZBOT:num->A->bool) /\
(!c i r. (!n. ZRECSPACE (r n)) ==> ZRECSPACE (ZCONSTR c i r))`;;
let recspace_tydef =
new_basic_type_definition "recspace" ("_mk_rec","_dest_rec")
(CONJUNCT1 ZRECSPACE_RULES);;
```

How would you proceed to define `recspace`

, `_mk_rec`

, and `_dest_rec`

in Coq?

Here is one possibility (although I am not sure what `Type'`

is, this gives you `Type`

instead), using a record:

```
Record recspace (A : Type) : Type :=
_mk_rec { _dest_rec : nat -> A -> Prop }.
Lemma axiom_9 : forall {A : Type} (a : recspace A), (@_mk_rec A (@_dest_rec A a)) = a.
Proof.
intros.
destruct a.
reflexivity.
Qed.
```

I guess you do not care too much about the equality being definitional vs propositional, but if you do you can use primitive projections:

```
#[projections(primitive)]Record recspace' (A : Type) : Type :=
_mk_rec' { _dest_rec' : nat -> A -> Prop }.
Lemma axiom_9' : forall {A : Type} (a : recspace' A), (@_mk_rec' A (@_dest_rec' A a)) = a.
Proof.
reflexivity.
Qed.
```

Here records can be used because the type is not recursive. If it were, you'd need an `Inductive`

type instead. In that case, you cannot get η laws, ie the equality can only be propositional.

Thank you, @Meven Lennon-Bertrand .

`Type'`

is the type of non-empty types used to interpret HOL types.

```
Record Type' := { type :> Type; el : type }.
```

I don't understand hol-light code, but the definition of `recspace`

seems to use `zrecspace`

, possibly through the line `(CONJUNCT1 ZRECSPACE_RULES);;`

and this relationship is probably needed to prove the next axiom:

```
Axiom axiom_10 : forall {A : Type'} (r : nat -> A -> Prop),
(@ZRECSPACE A r) = ((@_dest_rec A (@_mk_rec A r)) = r).
```

Mmmmm, this is a bit weirder: it looks like an equality between propositions. Afaik, in HOL this is how you express logical equivalence. But in Coq without axioms there is in general no hope to prove such equalities. You probably want to either express `axiom_10`

as logical equivalence, or add a form of propositional extensionality to obtain equality of propositions from their equivalences.

Anthony Bordg said:

`Type'`

is the type of non-empty types used to interpret HOL types.

So you need an extra layer (I guess you already have the equivalent of `Prop'`

lying around?).

```
Record Type' := { type :> Type; el : type }.
Definition Prop' : Type' := {| type := Prop ; el := True |}.
Record _recspace (A : Type') : Type :=
_mk_rec { _dest_rec : nat -> A -> Prop }.
Definition recspace (A : Type') : Type' :=
{| type := _recspace A ; el := _mk_rec A (fun _ _ => Prop'.(el)) |}.
```

Note that thank to the coercion `type :> Type`

in the definition of `Type'`

, using a `Type'`

as a `Type`

projects out the first component, so that using this new `recspace`

as a type amounts to `_recspace`

, ie nothing changes for `_dest_rec`

and `_mk_rec`

.

BTW, https://inria.hal.science/file/index/docid/520604/filename/itp10.pdf might also be of interest here (although I don't know how similar it is to the encoding used by dedukti)

If there is interest, I am quite sure I could make an opam package of the whole thing (including the patched HOL-Light)

Meven Lennon-Bertrand said:

Anthony Bordg said:

`Type'`

is the type of non-empty types used to interpret HOL types.So you need an extra layer (I guess you already have the equivalent of

`Prop'`

lying around?).

@Meven Lennon-Bertrand , exactly. In the Coq theory for handling hol-light proofs Frédéric defines `Prop'`

and `prop_ext`

.

```
Definition Prop' : Type' := {| type := Prop; el := True |}.
Canonical Prop'.
Axiom prop_ext : forall {P Q : Prop}, (P -> Q) -> (Q -> P) -> P = Q.
```

@Michael Soegtrop https://github.com/coq/opam/blob/master/released/packages/coq-hol-light/coq-hol-light.0.0.0/opam

Meven Lennon-Bertrand said:

Note that thank to the coercion

`type :> Type`

in the definition of`Type'`

, using a`Type'`

as a`Type`

projects out the first component, so that using this new`recspace`

as a type amounts to`_recspace`

, ie nothing changes for`_dest_rec`

and`_mk_rec`

.

@Meven Lennon-Bertrand, indeed. However, I'm still confused as to the meaning of `ZRECSPACE`

in the hol-light code and its relationship with `recspace`

, though I guess `ZRECSPACE`

could be defined in Coq as follows.

```
Inductive ZRECSPACE {A : Type'} : (nat -> A -> Prop) -> Prop :=
| ZRECSPACE0 : ZRECSPACE ZBOT
| ZRECSPACE1 c i r : ZRECSPACE (ZCONSTR c i r).
```

where `ZBOT`

and `ZCONSTR`

have been automatically translated into Coq by hol2dk as follows.

```
Definition ZBOT {A : Type'} := @INJP A (@INJN A (NUMERAL 0)) (@ε (nat -> A -> Prop) (fun z : nat -> A -> Prop => True)).
Definition ZCONSTR {A : Type'} := fun _17403 : nat => fun _17404 : A => fun _17405 : nat -> nat -> A -> Prop => @INJP A (@INJN A (S _17403)) (@INJP A (@INJA A _17404) (@INJF A _17405)).
```

But those two definitions are quite unlegible.

Note that `ZRECSPACE`

was also automatically translated as follows

```
Definition ZRECSPACE {A : Type'} := fun a : nat -> A -> Prop => forall ZRECSPACE' : (nat -> A -> Prop) -> Prop, (forall a' : nat -> A -> Prop, ((a' = (@ZBOT A)) \/ (exists c : nat, exists i : A, exists r : nat -> nat -> A -> Prop, (a' = (@ZCONSTR A c i r)) /\ (forall n : nat, ZRECSPACE' (r n)))) -> ZRECSPACE' a') -> ZRECSPACE' a.
Lemma ZRECSPACE_def {A : Type'} : (@ZRECSPACE A) = (fun a : nat -> A -> Prop => forall ZRECSPACE' : (nat -> A -> Prop) -> Prop, (forall a' : nat -> A -> Prop, ((a' = (@ZBOT A)) \/ (exists c : nat, exists i : A, exists r : nat -> nat -> A -> Prop, (a' = (@ZCONSTR A c i r)) /\ (forall n : nat, ZRECSPACE' (r n)))) -> ZRECSPACE' a') -> ZRECSPACE' a).
Proof. exact (eq_refl (@ZRECSPACE A)). Qed.
```

but the above `inductive ZRECSPACE`

is an attempt at making the def. of `zrecspace`

more idiomatic in Coq.

@Karl Palmskog : does this include the patches required by hol2dk?

See https://github.com/Deducteam/hol2dk#patching-hol-light-sources

no idea about package contents, I guess only Frédéric Blanqui can answer that

Looking at the opam package I would say it doesn't have the patches.

So again the question: is there interest in an opam package for hol2dk including the patched hol-light?

fine by me to have such a package in the Coq opam archive, but maybe open an issue about it first: https://github.com/Deducteam/hol2dk/issues

Done: https://github.com/Deducteam/hol2dk/issues/68

Anthony Bordg said:

Meven Lennon-Bertrand, indeed. However, I'm still confused as to the meaning of

`ZRECSPACE`

in the hol-light code and its relationship with`recspace`

I'm puzzled too: in the presence of prop-ext, we have

```
Lemma trivial : forall {A : Type'} (r : nat -> A -> Prop),
True = ((@_dest_rec A (@_mk_rec A r)) = r).
Proof.
intros.
apply prop_ext.
2: easy.
intros _.
reflexivity.
Qed.
```

And so it seems `ZRECSPACE`

is a very complicated definition for the constant-true predicate !?

Although I am not sure what roles ZBOT and ZCONSTR play, since they rely of `INJN`

and `INJP`

which are rather mysterious (I guess `ε`

is some choice operator?)

My guess would be that in impredicative encodings give you types which are only weakly initial (see eg Geuvers). So you need a predicate like `ZRECSPACE`

to carve out the "standard" elements on which your constructors/destructors play nicely. But with inductive types all of this disappears

Meven Lennon-Bertrand said:

Anthony Bordg said:

Meven Lennon-Bertrand, indeed. However, I'm still confused as to the meaning of

`ZRECSPACE`

in the hol-light code and its relationship with`recspace`

I'm puzzled too: in the presence of prop-ext, we have

`Lemma trivial : forall {A : Type'} (r : nat -> A -> Prop), True = ((@_dest_rec A (@_mk_rec A r)) = r). Proof. intros. apply prop_ext. 2: easy. intros _. reflexivity. Qed.`

And so it seems

`ZRECSPACE`

is a very complicated definition for the constant-true predicate !?

Weird! Thanks for noticing that.

Meven Lennon-Bertrand said:

Although I am not sure what roles ZBOT and ZCONSTR play, since they rely of

`INJN`

and`INJP`

which are rather mysterious (I guess`ε`

is some choice operator?)

Yes.

```
Definition ε : forall {A : Type'}, (type A -> Prop) -> type A := fun A P => epsilon (inhabits (el A)) P.
```

Hi. Thanks all with your interest in hol2dk and coq-hol-light.

This library uses the following axioms: classical logic, functional and propositional extensionnality, and constructive indefinite description (Hilbert epsilon). This is explained on https://github.com/Deducteam/coq-hol-light.

I see no need to include the HOL-Light sources in the coq-hol-light opam package for the moment. Do you think that it would be useful?

@Meven Lennon-Bertrand : what are the definitions of _dest_rec and _mk_rec did you use to prove trivial?

My understanding at the moment is that ZRECSPACE is the smallest predicate on nat -> A -> Prop satisfied by ZBOT and stable by ZCONSTR. I think that it should be defined by an Inductive in Coq. recspace is the subset of nat->A->Prop satisfying zrecspace. _mk_rec should be defined so as to map a function of nat->A->Prop to an element of recspace satisfying ZRECSPACE, i.e. epsilon ZRECSPACE. _dest_rec is the reverse.

This is like the Coq Inductive type nat proved to be equal to the subset of ind containing IND_0 and stable by IND_SUC for building natural numbers in https://github.com/Deducteam/coq-hol-light/blob/main/coq.v.

@Frédéric Blanqui it was in the context of my previous code snippets, the full code should be:

```
Record Type' := { type :> Type; el : type }.
Definition Prop' : Type' := {| type := Prop; el := True |}.
Canonical Prop'.
Axiom prop_ext : forall {P Q : Prop}, (P -> Q) -> (Q -> P) -> P = Q.
Record _recspace (A : Type') : Type :=
_mk_rec { _dest_rec : nat -> A -> Prop }.
Definition recspace (A : Type') : Type' :=
{| type := _recspace A ; el := _mk_rec A (fun _ _ => Prop'.(el)) |}.
Lemma trivial : forall {A : Type'} (r : nat -> A -> Prop),
True = ((@_dest_rec A (@_mk_rec A r)) = r).
Proof.
intros.
apply prop_ext.
2: easy.
intros _.
reflexivity.
Qed.
```

I see. In this case, this is not very surprising since the RHS is true by definition.

Frédéric Blanqui said:

My understanding at the moment is that ZRECSPACE is the smallest predicate on nat -> A -> Prop satisfied by ZBOT and stable by ZCONSTR.

@Frédéric Blanqui , note that the type of `zconstr`

is not `(nat -> A -> Prop) -> (nat -> A -> Prop)`

, but `nat -> A -> (nat -> nat -> A -> Prop) -> (nat -> A -> Prop)`

. Moreover, axiom 10 suggests that `zrecspace A r`

is true for every A and `r : nat -> A -> Prop`

. Thus, I'm not sure how all this is compatible with `zrecspace`

being the smallest predicate on nat -> A -> Prop satisfied by ZBOT and stable by ZCONSTR.

Hi. This is solved in https://github.com/Deducteam/hol2dk/pull/77 .

Last updated: Jun 18 2024 at 21:01 UTC