abab9579 (Aug 20 2022 at 07:59): abab9579 (Aug 20 2022 at 07:59):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!
Pierre Roux (Aug 20 2022 at 10:43):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
Pierre Roux (Aug 20 2022 at 10:46):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).
Pierre Roux (Aug 20 2022 at 10:48):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")
Pierre Roux (Aug 20 2022 at 10:57):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
Pierre Roux (Aug 20 2022 at 11:00):I agree this involves a few rather tricky steps. All this should become less tricky with MathCop 2.0.
abab9579 (Aug 21 2022 at 02:54):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?
Pierre Roux (Aug 22 2022 at 06:40):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.
abab9579 (Aug 22 2022 at 07:09):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.
abab9579 (Aug 22 2022 at 10:55):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.
Pierre Roux (Aug 22 2022 at 11:12):Looks like a missing coercion, have you done the same imports than in vector.v (in particular maybe Import GRing.Theory).
abab9579 (Aug 22 2022 at 11:15):Ouch, I missed that one. Thank you!!!!!
abab9579 (Aug 22 2022 at 13:00):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.
Pierre Roux (Aug 22 2022 at 14:28):Could you provide the "complete" code (leading to the error), I'm a bit out of ideas without being able to reproduce it.
abab9579 (Aug 23 2022 at 00:51):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.
Reynald Affeldt (Aug 23 2022 at 02:20):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.
abab9579 (Aug 23 2022 at 10:06):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?
Reynald Affeldt (Aug 23 2022 at 10:28):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.
Reynald Affeldt (Aug 23 2022 at 10:36):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.
Reynald Affeldt (Aug 23 2022 at 10:39):(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)
Last updated: Jan 29 2023 at 19:02 UTC