Stream: Coq users

Topic: hol2dk, exporting HOL-Light proofs to Coq


view this post on Zulip Anthony Bordg (Nov 28 2023 at 15:15):

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), withrecspace, _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?

view this post on Zulip Meven Lennon-Bertrand (Nov 28 2023 at 15:57):

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.

view this post on Zulip Meven Lennon-Bertrand (Nov 28 2023 at 15:59):

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.

view this post on Zulip Anthony Bordg (Nov 29 2023 at 17:51):

Thank you, @Meven Lennon-Bertrand .
Type' is the type of non-empty types used to interpret HOL types.

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

view this post on Zulip Anthony Bordg (Nov 29 2023 at 17:59):

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

view this post on Zulip Meven Lennon-Bertrand (Nov 30 2023 at 09:49):

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.

view this post on Zulip Meven Lennon-Bertrand (Nov 30 2023 at 10:10):

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.

view this post on Zulip Pierre Roux (Nov 30 2023 at 10:25):

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)

view this post on Zulip Michael Soegtrop (Nov 30 2023 at 10:59):

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

view this post on Zulip Anthony Bordg (Dec 01 2023 at 10:00):

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.

view this post on Zulip Karl Palmskog (Dec 01 2023 at 10:01):

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

view this post on Zulip Anthony Bordg (Dec 01 2023 at 10:29):

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

view this post on Zulip Michael Soegtrop (Dec 01 2023 at 13:03):

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

view this post on Zulip Michael Soegtrop (Dec 01 2023 at 13:04):

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

view this post on Zulip Karl Palmskog (Dec 01 2023 at 13:06):

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

view this post on Zulip Michael Soegtrop (Dec 01 2023 at 13:09):

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?

view this post on Zulip Karl Palmskog (Dec 01 2023 at 13:25):

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

view this post on Zulip Michael Soegtrop (Dec 01 2023 at 14:00):

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

view this post on Zulip Meven Lennon-Bertrand (Dec 01 2023 at 14:06):

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 !?

view this post on Zulip Meven Lennon-Bertrand (Dec 01 2023 at 14:07):

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

view this post on Zulip Meven Lennon-Bertrand (Dec 01 2023 at 14:10):

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

view this post on Zulip Anthony Bordg (Dec 01 2023 at 14:35):

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.

view this post on Zulip Anthony Bordg (Dec 01 2023 at 14:36):

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.

view this post on Zulip Frédéric Blanqui (Dec 01 2023 at 22:55):

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?

view this post on Zulip Frédéric Blanqui (Dec 01 2023 at 23:17):

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.

view this post on Zulip Frédéric Blanqui (Dec 01 2023 at 23:36):

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.

view this post on Zulip Meven Lennon-Bertrand (Dec 04 2023 at 09:37):

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

view this post on Zulip Frédéric Blanqui (Dec 04 2023 at 10:18):

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

view this post on Zulip Anthony Bordg (Dec 04 2023 at 12:11):

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.

view this post on Zulip Frédéric Blanqui (Dec 16 2023 at 07:59):

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


Last updated: Jun 18 2024 at 21:01 UTC