- port to HB #733
- status: works on 8.15 and 8.16, waiting for HB update of coq-master branch for master
- need to update the branch
-master of HB
- reverse dependencies (nix)
- deriving and extructures requiring universe poly
- some CI failures I don't understand with analysis and odd-order
(likely Nix issues)
- now that #910 is merged, rebased and
added SemiGroup to the Monoid hierarchy (in bigop.v)
- I (Pierre) also have a branch with semirings (https://github.com/proux01/math-comp/tree/hierarchy-builder-semiring),
seems to work rather well
- does it augment the compiling time of odd-order? that would be the quality criterion (Pierre: will try)
- remaining TODO/FIXME (part 1):
+++ algebra/intdiv.v
-Proof. by rewrite {2}(divz_eq m d) mulrDl mulrAC modzMDl. Qed.
+Proof. by rewrite {2}(divz_eq m d) [in RHS]mulrDl mulrAC modzMDl. Qed. (* FIXME: rewrite pattern *)
Pierre Roux 2021-04-16 14:08 Codification of FIXMEs
~~> remove the FIXME?
+++ algebra/ssrint.v
+Proof. by rewrite -[LHS]subr_ge0 opprB add0r subr_ge0. Qed. (* FIXME: rewrite pattern *)
Pierre Roux 2021-04-16 14:08 Codification of FIXMEs
~~> remove the FIXME?
+Proof. by rewrite -[LHS]subr_gt0 opprB add0r subr_gt0. Qed. (* FIXME: rewrite pattern *)
Pierre Roux 2021-04-16 14:08 Codification of FIXMEs
~~> remove the FIXME?
+++ fingroup/action.v
-apply/setP=> a; rewrite 2!in_setI; apply: andb_id2r => AutGa.
+(* TODO: investigate why rewrite does not match in the same order *)
+apply/setP=> a; rewrite in_setI [in RHS]in_setI; apply: andb_id2r => AutGa.
+(* the middle rewrite was rewrite 2!in_setI *)
Cyril Cohen 2021-04-08 11:37 all_fingroup compiles
~~> actual TODO
-Proof. by move=> sGD charM; split; rewrite (acts_char, char_sub). Qed.
+(* TODO: investigate why rewrite does not match in the same order *)
+Proof. by move=> sGD charM; split; rewrite ?acts_char// char_sub. Qed.
+(* was ending with rewrite (acts_char, char_sub)// *)
Cyril Cohen 2021-04-08 11:37 all_fingroup compiles
~~> actual TODO
+++ fingroup/gproduct.v
-rewrite -setX_prod -morphim_pair1g -morphim_pairg1 !morphim_gen ?subsetT //.
+(* TODO: investigate why the occurence selection changed *)
+rewrite -[in X in X \subset _]setX_prod.
+rewrite -morphim_pair1g -morphim_pairg1 !morphim_gen ?subsetT //.
Cyril Cohen 2021-04-08 11:37 all_fingroup compiles
~~> actual TODO
- about the
rewrite pattern comments
rewrite does not rewrite the first occurrence anymore- problem also occurs with the new semirings, associativity rewrites?
rewrite now seems to sometimes select a (visible) occurrence which is not the first visible occurrence- problem maybe related to coercions that appear in implicit arguments
- Cyril opened an issue for the
rewrite of SSReflect: https://github.com/coq/coq/issues/16763
+++ algebra/ssralg.v
+(* TODO : revise name "decidable_of_QE", check explicit arguments. *)
Yves Bertot 2021-04-08 15:57 Fix typos in the documentation of IsField.Build and ComRing_IsField.Build
~~> doc is definitely TODO
+(* FIXME: wrong name *)
+HB.factory Record decidable_of_QE F of Field F := {
+ proj : nat -> seq (term F) * seq (term F) -> formula F;
+ wf_proj : wf_QE_proj proj;
+ ok_proj : valid_QE_proj proj;
+}.
Cyril Cohen 2021-05-10 15:26 Partial port to HB
~~> fix name?
- rename
decidable_of_QE to QE_isDecidable?
+++ algebra/ssralg.v
+HB.structure Definition RMorphism (R S : ringType) :=
+ {f of @Additive R S f & isMultiplicative R S f}.
+(* FIXME: Additive has very strange implicit arguments
+ (without @, one would have to write Additive R f) *)
Pierre Roux 2022-09-08 11:30 Port morphism hierarchy to HB
~~> should we do anything?
+HB.structure Definition LRMorphism (R : ringType) (A : lalgType R) (B : ringType)
+ (s : R -> B -> B) :=
+ {f of @RMorphism A B f & isLinear R A B s f}.
+(* FIXME: strange implicit arguments for RMorphism (just like Additive) *)
Pierre Roux 2022-09-08 11:30 Port morphism hierarchy to HB
~~> should we do anything?
+(* FIXME: bad naming *)
+HB.factory Record is_ComAlgebra R V of ComRing V & Lalgebra R V := {}.
Cyril Cohen 2021-05-10 15:26 Partial port to HB
~~> maybe ComRing_Lalgebra_isComAlgebra?
- rename
is_ComAlgebra
- TODO: why is this factory empty? what happens if we remove this factory?
(it seems to be used a priori, in relation with
R^o)
+(* TODO: put a factory in field/closed_field *)
+#[mathcomp(axiom="closed_field_axiom"), short(type="closedFieldType")]
+HB.structure Definition ClosedField :=
+ { F of DecidableField F & DecField_isAlgClosed F }.
Enrico Tassi 2021-04-01 Partial Port to HB
~~> true TODO?
- put a factory in
field/closed_field.v
- needed factory
isAlgClosed that generates the proof of decidability
(lemma: the first order theory of an alg. closed field is decidable)
+++ algebra/vector.v
-Notation axiom n V := (axiom_def n (Phant V)).
+(* FIXME: Vector.axiom requires a phantom type *
+ * -> a shortand notation is used instead *)
+Notation vector_axiom n V := (Vector.axiom n (Phant V)).
Xavier Allamigeon 2021-04-09 18:15 First proof of vector.v
~~> remove the FIXME?
Vector.axiom requires a phantom type
- just add
infer
- same for in
Lmodule.type
+(* FIXME: S/space and H/hom were defined behind the module Vector *
+ * Perhaps we should change their names to avoid conflits. *)
Xavier Allamigeon 2021-04-09 18:15 First proof of vector.v
~~> ?
+(* FIXME: as explained above, the following structures should not be declared *
+ * as canonical, so mixins and structures are built separately, and we *
+ * don't use HB.instance Definition _ := ... *
+ * This is ok, but maybe we could introduce an alias *)
Xavier Allamigeon 2021-04-09 18:15 First proof of vector.v
~~> ?
- TODO:
- explicit calls to
HB.pack -> instead we should either
- create an alias for
'End(vT) with in phantom the proof of vT_proper : dim vT > 0
- or add the structure
vec_Type of non-zero dimension
- related note: backport pointed from MathComp-Analysis
(and introduce a new definition for
nth with a default argument)
+++ character/mxrepresentation.v
+(* FIXME : why this MathCompCompatDecidableField *)
+Lemma gen_satP :
+ GRing.MathCompCompatDecidableField.DecidableField.axiom gen_sat.
thery 2021-04-11 02:55 Starting character : mxrepresentation
~~> ?
- TODO:
- add
#[mathcomp(axiom = ...)] in DecidableField? no, already there
- maybe this is not needed...
-set F' := gen_fieldType _ _; set rG' := @map_repr _ F' _ _ _ _ rG.
-move: F' (gen_rmorphism _ _ : {rmorphism F -> F'}) => F' f' in rG' * => irrG'.
+(* FIXME: _ matches a generated constant *)
+set F' := _ irrG cGA; set rG' := @map_repr _ F' _ _ _ _ rG.
+move: F' ([rmorphism of gen _ _] : {rmorphism F -> F'}) => F' f' in rG' * => irrG'.
Cyril Cohen 2021-04-22 23:04 Fix mxrepresentation Canonical subType + rVval
~~> ?
- we should not use
gen_fieldType because it is produced by HB, that's why there is an underscore
+++ field/falgebra.v
-Canonical regular_FalgType (R : comUnitRingType) := [FalgType R of R^o].
+HB.instance Definition _ (R : comUnitRingType) := GRing.UnitAlgebra.on R^o.
+(* FIXME: builds a FalgType R R^o, works but couldn't it look nicer? *)
Pierre Roux 2021-04-10 16:27 Port falgebra.v
~~> ?
- HB does not do the automatic completion of the graph, this should be an issue for HB
+++ field/galois.v
+(* FIXME: add factory *)
Cyril Cohen 2021-04-14 12:18 Galois compiles
~~> actual TODO
Lemma normal_field_splitting (F : fieldType) (L : fieldExtType F) :
(forall (K : {subfield L}) x,
exists r, minPoly K x == \prod_(y <- r) ('X - y%:P)) ->
+(* FIXME: add factory *)
+Fact regular_splittingAxiom (F : fieldType) :
+ SplittingField.axiom [the fieldExtType F of F^o].
Cyril Cohen 2021-04-14 12:18 Galois compiles
~~> actual TODO
+++ solvable/center.v
-Local Notation C := [set: FinGroup.arg_sort (FinGroup.base cprod_by)].
+Local Notation C := [set: FinGroup.sort cprod_by].
+(*FIXME : Check if we need arg_sort instead of sort*)
Quentin Canu 2021-04-09 11:12 center.v ported
~~> ?
- there was a telescope before,
arg_sort is an alias of sort to do inference of predicates
- that should be
arg_sort
- TODO: investigate
+++ solvable/extraspecial.v
- have def_xi i: x ^+ i = sdpair1 _ (0, i%:R)%R.
+ have def_xi i: x ^+ i = sdpair1 actp (0, i%:R)%R. (* FIXME: had to explicitly give actp (instead of _) *)
Pierre Roux 2021-04-12 14:39 Port extraspecial.v
~~> remove FIXME? (x3 in that file)
+++ b/mathcomp/solvable/finmodule.v
+(* TODO: understand why FinGroup has to be changed to BaseFinGroup here. *)
Let f2sub (gT : finGroupType) (A : {group gT}) (abA : abelian A) :=
- fun u : fmod_of abA => let : Fmod x Ax := u in Subg Ax : FinGroup.arg_sort _.
-Local Coercion f2sub : fmod_of >-> FinGroup.arg_sort.
+ fun u : fmod_of abA => let : Fmod x Ax := u in Subg Ax : BaseFinGroup.arg_sort _.
+Local Coercion f2sub : fmod_of >-> BaseFinGroup.arg_sort.
Yves Bertot 2021-04-09 12:11 all HB.instances done in finmodule, but notations and scopes
~~> maybe we can just remove that TODO?
+#[export]
+HB.instance Definition _ :=
+ GRing.isZmodule.Build fmodA fmod_addrA fmod_addrC fmod_add0r fmod_addNr.
+(* TODO: Should isZmodule and the like be exported from ssralg *)
+#[export]
+HB.instance Definition _ := [finGroupMixin of fmodA for +%R].
Yves Bertot 2021-04-09 12:11 all HB.instances done in finmodule, but notations and scopes
~~> actual question
- should we export all the mixins and factories?
+++ solvable/nilpotent.v
-apply/setP=> x; rewrite inE -(setIidPr (ucn_sub n.+1 G)) inE ucnSn.
+(* apply/setP=> x; rewrite inE -(setIidPr (ucn_sub n.+1 G)) inE ucnSn. *)
+(* FIXME: before, we got a `rewrite inE` right after the apply/setP=> x. *
+ * However, this rewrite unfolds termes to strange internal HB names. *
+ * We fixed the issue by applying the inE more carefully, but the problem *
+ * needs to be investigated. *)
+apply/setP=> x; rewrite -(setIidPr (ucn_sub n.+1 G)) [LHS]inE [RHS]inE ucnSn.
Xavier Allamigeon 2021-04-09 11:47 Port nilpotent.v
~~> ?
- TODO: need to execute to understand,
- maybe also a problem of names generated by HB
+++ ssreflect/choice.v
-Notation "[ 'subCountType' 'of' T ]" :=
- (@pack_subCountType _ _ T _ _ id _ _ id)
+(* TODO: replace with trivial pack *)
+Notation "[ 'subCountType' 'of' T ]" := (SubCountable.clone _ _ T _)
Enrico Tassi 2021-04-01 16:21 Portail port to HB
~~> ?
- replace with a trivial pack,
.clone should be .pack
+++ ssreflect/order.v
+HB.builders Context (d : unit) T of isLePOrdered d T.
+(* TODO: print nice error message when keyed type is not provided *)
Enrico Tassi 2021-04-01 16:21 Partial port to HB
~~> check and if not fixed issue to HB and remove TODO
+(* TODO: Restore when we remove the mathcomp attribute *)
Enrico Tassi 2021-04-01 16:21 Partial port to HB
~~> ? (x2 in that file)
-Definition top disp {T : tbLatticeType disp} : T :=
- TBLattice.top (TBLattice.class T).
+Module TBLatticeExports.
+(* FIXME: clone? *)
+End TBLatticeExports.
+HB.export TBLatticeExports.
Cyril Cohen 2021-05-10 15:26 Several fixes
~~> ?
+(* TODO: rename to lattice_ismeet_distributive ? *)
+#[key="T"]
+HB.mixin Record Lattice_MeetIsDistributive d (T : Type) of Lattice d T := {
+ meetUl : @left_distributive T T meet join;
Cyril Cohen 2021-04-07 01:03 renamings
~~> rename?
+Module DistrLatticeExports.
+(* FIXME: clone? *)
Cyril Cohen 2021-05-10 15:26 Several fixes
~~> ?
- TODO: remove the TODO and add the structures
- _ : forall x, compl x = sub top x
+ complE : forall x : T, compl x = (top : T) `\` x (* FIXME? *)
Cyril Cohen 2021-04-07 01:03 CanOrders, SubOrders and uniformization of conventions in order.v
~~> ?
- TODO: why did we lose the type?