I want to use subtype mixins, e.g. `[zmodMixin of M by <: ]`

.

It seems to encapsulate the logic for providing structures on subtypes (given operations are closed).

Obviously, the closure property needs to be specified. I am stuck at how to do this.

Looking at the documentation, it looks like I have to attach zmodPred keys onto it. I do not know how the key works, though.

Could anyone help with this? Help would be greatly appreciated!

Indeed, that's rather hard to discover. The best solution is probably to look at an example, you can find one here for instance (vector subspaces) : https://github.com/math-comp/math-comp/blob/c66a532bc7878c366acfe5203083fb3dcbb31d3e/mathcomp/algebra/vector.v#L1893-L1907

Basically, the subtype is declared with `[subType for injection_from_subtype_to_base_type]`

then structures have to be built and declared canonical in order (`eqType`

, then `choiceType`

then `zmodType`

since `zmodType`

inherits from `choiceType`

which itself inherits from `eqType`

).

The doc for subtypes is in the header of the `eqType.v`

file: https://github.com/math-comp/math-comp/blob/c66a532bc7878c366acfe5203083fb3dcbb31d3e/mathcomp/ssreflect/eqtype.v (found for instance with the command `Locate "subType"`

)

You indeed also need to key the predicate and associate it a ZmodPred, see example here : https://github.com/math-comp/math-comp/blob/c66a532bc7878c366acfe5203083fb3dcbb31d3e/mathcomp/algebra/vector.v#L423-L441

I agree this involves a few rather tricky steps. All this should become less tricky with MathCop 2.0.

Thank you for great guidance!

Do you also happen to know how to coerce `set A`

with boolean predicate in context of `math-comp/analysis`

?

EDIT: Also, with predicate `pred_key [pred f in CPow m]`

, Canonical on `KeyedPred`

does not work. How do I go around this?

To get from Prop to bool, you can use the ``[< P >]`

notation from boolp.v https://github.com/math-comp/analysis/blob/master/theories/boolp.v The main lemma is `asboolP`

but other lemmas about `asbool`

can be useful.

Hmm, can I give a key to such predicate? What kind of predicate can I make a `KeyedPred`

?

EDIT: This code gives a warning:

```
Definition CPowS m := [pred f | `[< CPow m f >]].
Fact cpow_key m : pred_key (CPowS m). Proof. by []. Qed.
Canonical cpow_keyed m := KeyedPred (cpow_key m).
```

Warning is:

```
Ignoring canonical projection to PredOfSimpl.coerce by unkey_pred in
cpow_keyed: redundant with keyed_mem_simpl
```

The warning means that the predicate is already keyed. Maybe you just don't need to key it again.

I see. Then, I do not get this error:

When I have

```
Fact cpow_submod_closed m : submod_closed (CPowS m).
Canonical opprPred m := OpprPred (cpow_submod_closed m).
```

where `CPowS m`

is the keyed predicate above, the following error occurs:

```
The term "cpow_submod_closed m" has type
"submod_closed (V:=fct_lmodType V R) (CPowS m)"
while it is expected to have type "oppr_closed ?kS".
```

However, in the `vector.v`

there is

```
Fact memv_submod_closed U : submod_closed U.
(...)
Canonical memv_opprPred U := OpprPred (memv_submod_closed U).
```

which indeed works. Do you know what difference in my code is the culprit? It looks quite identical in my eye.

Looks like a missing coercion, have you done the same imports than in `vector.v`

(in particular maybe `Import GRing.Theory`

).

Ouch, I missed that one. Thank you!!!!!

Hm, it seems like that was not the culprit. I have

```
From mathcomp Require Import all_ssreflect.
From mathcomp Require Import ssralg ssrnum matrix mxalgebra zmodp.
From mathcomp Require Import boolp classical_sets topology functions.
From mathcomp Require Import normedtype derive reals.
Set Implicit Arguments.
Import GRing.Theory.
Import numFieldNormedType.Exports.
```

at header, yet the error persists.

Could you provide the "complete" code (leading to the error), I'm a bit out of ideas without being able to reproduce it.

Sorry.. Here's the whole code.

```
From mathcomp Require Import all_ssreflect.
From mathcomp Require Import ssralg ssrnum matrix mxalgebra zmodp.
From mathcomp Require Import boolp classical_sets topology functions.
From mathcomp Require Import normedtype derive reals.
Set Implicit Arguments.
Import GRing.Theory.
Import numFieldNormedType.Exports.
Local Open Scope classical_set_scope.
Local Open Scope ring_scope.
Reserved Notation "''C^' n ( V )" (at level 0, n, V at next level).
Reserved Notation "''C^infty' ( V )" (at level 0, V at next level).
Module CNSpace.
Section CNSpace.
Context {R: realType} (V: normedModType R).
(* C^N (V) set *)
Fixpoint CPow (m: nat): set (V -> R) :=
match m with
| 0 => fun f => continuous f
| S m' => fun f =>
(forall (v x: V), derivable f x v) /\ (forall v: V, CPow m' ('D_v f))
end.
(* Cannot find where contiAdd/contiNeg etc are defined.. *)
Lemma contiPowAdd m (f g: V -> R):
CPow m f -> CPow m g -> CPow m (f + g).
Proof. move: f g. elim: m=> [|m IH] f g /=.
- move=> Hf Hg x. apply/continuousD. apply/Hf. apply/Hg.
- move=> [Df Cf] [Dg Cg]. split=> [v x | v].
+ by apply/derivableD.
+ have ->: 'D_v (f + g) = 'D_v f + 'D_v g.
* apply/funext=> x. by apply/deriveD.
by apply/IH.
Qed.
Lemma contiPowNeg m (f: V -> R):
CPow m f -> CPow m (-f).
Proof. move: f. elim: m=> [|m IH] f /=.
- move=> Hf x. apply/continuousN. apply/Hf.
- move=> [Df Cf]. split=> [v x | v].
+ by apply/derivableN.
+ have ->: 'D_v (-f) = - 'D_v f.
* apply/funext=> x. by apply/deriveN.
by apply/IH.
Qed.
Definition CPowS m := [pred f | `[< CPow m f >]].
(*
Fact cpow_key m : pred_key (CPowS m). Proof. by []. Qed.
Canonical cpow_keyed m := KeyedPred (cpow_key m).
*)
(* TODO Simplify derivable stuffs *)
Fact cpow_submod_closed m : submod_closed (CPowS m).
Proof. split.
- rewrite in_setE. elim: m=> [| m IH] /=.
+ apply/cst_continuous.
+ split=> [v x | v]. apply/ex_derive.
have -> //: 'D_v 0 = (0 : V -> R).
* apply/funext=> x. by rewrite derive_val.
- move=> c f g. rewrite !in_setE. move: f g.
elim: m=> [| m IH] f g /=.
+ move=> Hf Hg x. apply/continuousD. apply/continuousZr.
apply/Hf. apply/Hg.
+ move=> [Df Cf] [Dg Cg]. split=> [v x | v].
* apply/derivableD=> [| //]. by apply/derivableZ.
* have ->: 'D_v (c *: f + g) = c *: 'D_v f + 'D_v g.
- apply/funext=> x. rewrite deriveD //= ?deriveZ //.
by apply/derivableZ.
by apply/IH.
Qed.
(* This part is not working, is it due to warning above? *)
Canonical opprPred m := OpprPred (cpow_submod_closed m).
Canonical addrPred m := AddrPred (cpow_submod_closed m).
Canonical zmodPred m := ZmodPred (cpow_submod_closed m).
Canonical submodPred m := SubmodPred (cpow_submod_closed m).
```

It errors out at `Canonical opprPred m := ...`

part.

This goes through:

```
From mathcomp Require Import all_ssreflect all_algebra.
From mathcomp Require Import boolp classical_sets topology functions.
From mathcomp Require Import reals normedtype derive.
Set Implicit Arguments.
Import GRing.Theory.
Import numFieldNormedType.Exports.
Local Open Scope classical_set_scope.
Local Open Scope ring_scope.
Reserved Notation "''C^' n ( V )" (at level 0, n, V at next level).
Reserved Notation "''C^infty' ( V )" (at level 0, V at next level).
Section Cpow_def.
Context {R : realType} {V : normedModType R}.
(* C^N (V) set *)
Fixpoint CPow m : set (V -> R) :=
if m is m'.+1 then
[set f | (forall v (x : V), derivable f x v) /\ (forall v, CPow m' ('D_v f))]
else
[set f : V -> R | continuous f].
Definition Cpow m := [qualify a f : V -> R | f \in CPow m].
Fact Cpow_key m : pred_key (Cpow m). Proof. by []. Qed.
Canonical Cpow_keyed m := KeyedQualifier (Cpow_key m).
End Cpow_def.
Section CNSpace.
Context {R : realType} {V : normedModType R}.
Implicit Types f g : V -> R.
Lemma CpowD m f g : f \is a Cpow m -> g \is a Cpow m -> f + g \is a Cpow m.
Proof.
rewrite 3!inE; elim: m => [|m ih] /= in f g *.
- by move=> cf cg x; apply/continuousD; [exact/cf|exact/cg].
- move=> [Df cf] [Dg cg]; split=> [v x|v]; first exact/derivableD.
suff -> : 'D_v (f + g) = 'D_v f + 'D_v g by exact/ih.
by apply/funext=> x; exact/deriveD.
Qed.
Lemma CpowN m f : f \is a Cpow m -> - f \is a Cpow m.
Proof.
rewrite 2!inE; elim: m => [|m ih] /= in f *.
- by move=> cf x; exact/continuousN/cf.
- move=> [Df Cf]; split=> [v x|v]; first exact/derivableN.
suff -> : 'D_v (-f) = - 'D_v f by exact/ih.
by apply/funext=> x; exact/deriveN.
Qed.
(* TODO Simplify derivable stuffs *)
Fact Cpow_submod_closed m : submod_closed (@Cpow R V m).
Proof.
split.
- rewrite inE; elim: m => [|m ih] /=; first exact/cst_continuous.
split => [v x|v]; first exact/derivable_cst.
suff -> : 'D_v 0 = (0 : V -> R) by [].
by apply/funext=> x; rewrite derive_val.
- move=> c f g; rewrite 3!inE; elim: m => [|m ih] /= in f g *.
+ by move=> cf cg x; apply/continuousD; [exact/continuousZr/cf|exact/cg].
+ move=> [Df Cf] [Dg Cg]; split=> [v x|v].
by apply/derivableD => [| //]; exact/derivableZ.
suff -> : 'D_v (c *: f + g) = c *: 'D_v f + 'D_v g by exact/ih.
by apply/funext=> x; rewrite deriveD //= ?deriveZ //; exact/derivableZ.
Qed.
Canonical opprPred m := OpprPred (Cpow_submod_closed m).
Canonical addrPred m := AddrPred (Cpow_submod_closed m).
Canonical zmodPred m := ZmodPred (Cpow_submod_closed m).
Canonical submodPred m := SubmodPred (Cpow_submod_closed m).
End CNSpace.
```

The minimal change would have been to use `qualify a`

instead of `pred`

and (consequently) `KeyedQualifier`

instead of `KeyedPred`

.

Thank you so much, this works!

I am sorry that I did not provide full code early on. Guess I forgot how to ask questions properly..

If it does not bother you, may I ask what the `qualify`

or `Qualifier`

is? Is it a special predicate which does not auto-simplify?

It looks like this is mostly for cosmetics. For example, if you use `Definition Cpow m := [qualify f : V -> R | f \in CPow m].`

instead of `Definition Cpow m := [qualify a f : V -> R | f \in CPow m].`

(the difference is the `a`

), then the notation will be `f \is Cpow m`

(which maybe would be a better fit here). I do not think it has a special behavior w.r.t. simplication.

Your example could also have gone through with:

```
Definition CPowS m := fun f => f \in CPow m.
Fact cpow_key m : pred_key (CPowS m). Proof. by []. Qed.
Canonical cpow_keyed m := KeyedPred (cpow_key m).
```

and the `\in`

would have been available instead of `\is`

.

(so just change `pred`

to `fun`

was the answer to your original question, sorry for the digression but my first reaction was to try `qualify`

)

Wow, very interesting mechanics happening here.

Anyway, thank you again for all the helpful answers!!

abab9579 has marked this topic as resolved.

The precise doc is there : https://github.com/coq/coq/blob/de96bfd67df02068c853155bd53264ad61ddab81/theories/ssr/ssrbool.v#L200-L220

Last updated: Jul 23 2024 at 19:02 UTC