From 9f1f62606c639618779f951c8f9888d4e042b846 Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Wed, 13 Jul 2022 15:50:55 +0200 Subject: [PATCH] Starting port to HB --- .nix/config.nix | 19 ++++++++++++------ theories/boolp.v | 42 +++++++++++++++++++-------------------- theories/mathcomp_extra.v | 1 - 3 files changed, 33 insertions(+), 29 deletions(-) diff --git a/.nix/config.nix b/.nix/config.nix index 7c950ade64..79d7041189 100644 --- a/.nix/config.nix +++ b/.nix/config.nix @@ -31,14 +31,21 @@ ## select an entry to build in the following `bundles` set ## defaults to "default" - default-bundle = "8.16"; + default-bundle = "8.15"; ## write one `bundles.name` attribute set per ## alternative configuration ## When generating GitHub Action CI, one workflow file ## will be created per bundle bundles."8.14".coqPackages.coq.override.version = "8.14"; - bundles."8.15".coqPackages.coq.override.version = "8.15"; + bundles."8.15".coqPackages = { + coq.override.version = "8.15"; + hierarchy-builder.override.version = "fun_instances"; + mathcomp.override.version = "CohenCyril:hb-ssrnum"; + mathcomp-bigenough.override.version = "1.0.1"; + mathcomp-finmap.override.version = "proux01:hierarchy-builder"; + mathcomp-real-closed.override.version = "CohenCyril:hierarchy-builder"; + }; bundles."8.16".coqPackages = { coq.override.version = "8.16"; @@ -47,7 +54,7 @@ mathcomp-bigenough.override.version = "1.0.1"; mathcomp-finmap.override.version = "1.5.2"; mathcomp-real-closed.override.version = "1.1.3"; - mathcomp.override.version = "mathcomp-1.15.0"; + mathcomp.override.version = "CohenCyril:hb-ssrnum"; }; bundles."master".coqPackages = { @@ -65,17 +72,17 @@ cachix.coq = {}; cachix.math-comp.authToken = "CACHIX_AUTH_TOKEN"; cachix.coq-community = {}; - + ## If you have write access to one of these caches you can ## provide the auth token or signing key through a secret ## variable on GitHub. Then, you should give the variable ## name here. For instance, coq-community projects can use ## the following line instead of the one above: # cachix.coq-community.authToken = "CACHIX_AUTH_TOKEN"; - + ## Or if you have a signing key for a given Cachix cache: # cachix.my-cache.signingKey = "CACHIX_SIGNING_KEY" - + ## Note that here, CACHIX_AUTH_TOKEN and CACHIX_SIGNING_KEY ## are the names of secret variables. They are set in ## GitHub's web interface. diff --git a/theories/boolp.v b/theories/boolp.v index f33fdb2028..33f30fc19f 100644 --- a/theories/boolp.v +++ b/theories/boolp.v @@ -4,7 +4,7 @@ (* Copyright (c) - 2015--2018 - Inria *) (* Copyright (c) - 2016--2018 - Polytechnique *) (* -------------------------------------------------------------------- *) - +From HB Require Import structures. From mathcomp Require Import all_ssreflect. (******************************************************************************) @@ -164,7 +164,7 @@ Proof. by move: x (x) y => /propT-> [] []. Qed. (* -------------------------------------------------------------------- *) Record mclassic := { _ : forall (P : Prop), {P} + {~P}; - _ : forall T, Choice.mixin_of T + _ : forall T, HasChoice T }. Lemma choice X Y (P : X -> Y -> Prop) : @@ -211,7 +211,7 @@ exists (fun (P : pred T) (n : nat) => by exists 0; case: pselect => // -[]; exists x. Qed. -Lemma gen_choiceMixin {T : Type} : Choice.mixin_of T. +Lemma gen_choiceMixin (T : Type) : HasChoice T. Proof. by case: classic. Qed. Lemma pdegen (P : Prop): P = True \/ P = False. @@ -322,28 +322,22 @@ Proof. by move=> [] []; rewrite ?(trueE, falseE) ?propeqE; tauto. Qed. Definition gen_eq (T : Type) (u v : T) := `[]. Lemma gen_eqP (T : Type) : Equality.axiom (@gen_eq T). Proof. by move=> x y; apply: (iffP (asboolP _)). Qed. -Definition gen_eqMixin {T : Type} := EqMixin (@gen_eqP T). - -Canonical arrow_eqType (T : Type) (T' : eqType) := - EqType (T -> T') gen_eqMixin. -Canonical arrow_choiceType (T : Type) (T' : choiceType) := - ChoiceType (T -> T') gen_choiceMixin. +Definition gen_eqMixin (T : Type) : HasDecEq T := + HasDecEq.Build T (@gen_eqP T). -Definition dep_arrow_eqType (T : Type) (T' : T -> eqType) := - EqType (forall x : T, T' x) gen_eqMixin. -Definition dep_arrow_choiceClass (T : Type) (T' : T -> choiceType) := - Choice.Class (Equality.class (dep_arrow_eqType T')) gen_choiceMixin. -Definition dep_arrow_choiceType (T : Type) (T' : T -> choiceType) := - Choice.Pack (dep_arrow_choiceClass T'). +HB.instance Definition _ (T : Type) (T' : T -> eqType) := + gen_eqMixin (forall x : T, T' x). +HB.instance Definition _ (T : Type) (T' : T -> choiceType) := + gen_choiceMixin (forall x : T, T' x). -Canonical Prop_eqType := EqType Prop gen_eqMixin. -Canonical Prop_choiceType := ChoiceType Prop gen_choiceMixin. +HB.instance Definition _ := gen_eqMixin Prop. +HB.instance Definition _ := gen_choiceMixin Prop. Section classicType. Variable T : Type. Definition classicType := T. -Canonical classicType_eqType := EqType classicType gen_eqMixin. -Canonical classicType_choiceType := ChoiceType classicType gen_choiceMixin. +HB.instance Definition _ := gen_eqMixin classicType. +HB.instance Definition _ := gen_choiceMixin classicType. End classicType. Notation "'{classic' T }" := (classicType T) (format "'{classic' T }") : type_scope. @@ -351,8 +345,8 @@ Notation "'{classic' T }" := (classicType T) Section eclassicType. Variable T : eqType. Definition eclassicType : Type := T. -Canonical eclassicType_eqType := EqType eclassicType (Equality.class T). -Canonical eclassicType_choiceType := ChoiceType eclassicType gen_choiceMixin. +HB.instance Definition _ := Equality.copy eclassicType T. +HB.instance Definition _ := gen_choiceMixin eclassicType. End eclassicType. Notation "'{eclassic' T }" := (eclassicType T) (format "'{eclassic' T }") : type_scope. @@ -371,7 +365,10 @@ Proof. by apply: canon => T; exists [eqType of {classic T}]. Qed. Lemma Pchoice : canonical Type choiceType. Proof. by apply: canon => T; exists [choiceType of {classic T}]. Qed. Lemma eqPchoice : canonical eqType choiceType. -Proof. by apply: canon=> T; exists [choiceType of {eclassic T}]; case: T. Qed. +Proof. +apply: canon => T; exists [choiceType of {eclassic T}]. +by case: T => //= T [?]//. +Qed. Lemma not_True : (~ True) = False. Proof. exact/propext. Qed. Lemma not_False : (~ False) = True. Proof. by apply/propext; split=> _. Qed. @@ -715,6 +712,7 @@ move=> g f h /asboolP fg /asboolP gh; apply/asboolP => x. by rewrite (le_trans (fg x)). Qed. +HB.instance Definition := Definition porderMixin := @LePOrderMixin _ lef ltf ltf_def lef_refl lef_anti lef_trans. diff --git a/theories/mathcomp_extra.v b/theories/mathcomp_extra.v index 333f1afc69..a85ab43a66 100644 --- a/theories/mathcomp_extra.v +++ b/theories/mathcomp_extra.v @@ -3,7 +3,6 @@ From mathcomp Require choice. (* Missing coercion (done before Import to avoid redeclaration error, thanks to KS for the trick) *) (* MathComp 1.15 addition *) -Coercion choice.Choice.mixin : choice.Choice.class_of >-> choice.Choice.mixin_of. From mathcomp Require Import all_ssreflect finmap ssralg ssrnum ssrint rat. From mathcomp Require Import finset interval.