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?
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 ofType'
, using aType'
as aType
projects out the first component, so that using this newrecspace
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 withrecspace
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 withrecspace
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
andINJP
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: Oct 13 2024 at 01:02 UTC