Skip to content

WIP / Experiment : Remove the dependency on R #112

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
drouhling wants to merge 11 commits into from
Closed

WIP / Experiment : Remove the dependency on R #112

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
11 commits
Select commit Hold shift + click to select a range
3f96140
Remove ball and absRingType
Sep 28, 2018
334a32b
Shorten proofs
Oct 2, 2018
22d8bac
Use {ereal R} in hierarchy
Oct 3, 2018
dc99671
Reintroduce lemmas about R that were commented out
Oct 4, 2018
b644833
Add and use a theory of max using bigop
Oct 8, 2018
893bf88
Add min using bigop and simplify proofs
Oct 9, 2018
a1834b2
Move and extend Rstruct.v
Oct 9, 2018
cb4ca5f
Clean up
Oct 10, 2018
091772f
More clean up
Oct 12, 2018
3aaf321
Rework documentation and mark missing lemmas
Oct 12, 2018
909029d
Reintroduce missing lemmas + more clean up
Oct 12, 2018
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 2 additions & 2 deletions _CoqProject
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,8 +6,7 @@ reals.v
posnum.v
landau.v
classical_sets.v
Rstruct.v
Rbar.v
# Rbar.v
topology.v
hierarchy.v
forms.v
Expand All @@ -18,5 +17,6 @@ altreals/discrete.v
altreals/realseq.v
altreals/realsum.v
altreals/distr.v
misc/Rstruct.v

-R . mathcomp.analysis
10 changes: 5 additions & 5 deletions altreals/distr.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -544,15 +544,15 @@ End DLetAlg.

(* -------------------------------------------------------------------- *)
Definition mlim T (f : nat -> distr T) : T -> R :=
fun x => nlim (fun n => f n x).
fun x => (nlim (fun n => f n x) : [numDomainType of R]).

Lemma isd_mlim T (f : nat -> distr T) : isdistr (mlim f).
Proof. split=> [x|J]; rewrite /mlim.
+ case: nlimP=> // l cvSl; apply/le0R/(ncvg_geC _ cvSl).
by move=> n; apply/ge0_mu.
move=> uqJ; pose F j :=
if `[< iscvg (fun n => f n j) >] then fun n => f n j else 0%:S.
apply/(@ler_trans _ (\sum_(j <- J) (nlim (F j) : R))).
apply/(@ler_trans _ (\sum_(j <- J) (nlim (F j) : [numDomainType of R]))).
apply/ler_sum=> j _; rewrite /F; case/boolP: `[< _ >] => //.
move/asboolPn=> h; rewrite nlimC; case: nlimP=> //.
by case=> // l cf; case: h; exists l.
Expand All @@ -579,7 +579,7 @@ Definition dlim T (f : nat -> distr T) :=
Notation "\dlim_ ( n ) E" := (dlim (fun n => E)).

Lemma dlimE T (f : nat -> distr T) x :
(\dlim_(n) f n) x = nlim (fun n => f n x).
(\dlim_(n) f n) x = (nlim (fun n => f n x) : [numDomainType of R]).
Proof. by unlock dlim. Qed.

(* -------------------------------------------------------------------- *)
Expand Down Expand Up @@ -1192,7 +1192,7 @@ Definition convexon (a b : {ereal R}) (f : R -> R) :=
forall t, 0 <= t <= 1 ->
f (t * x + (1 - t) * y) <= t * (f x) + (1 - t) * (f y).

Notation convex f := (convexon \-inf \+inf f).
Notation convex f := (convexon -oo +oo f).

Section Jensen.
Context (f : R -> R) (x l : I -> R).
Expand Down Expand Up @@ -1228,6 +1228,6 @@ Qed.
End Jensen.
End Jensen.

Notation convex f := (convexon \-inf \+inf f).
Notation convex f := (convexon -oo +oo f).

(* -------------------------------------------------------------------- *)
22 changes: 11 additions & 11 deletions altreals/realseq.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -49,8 +49,8 @@ Context {R : realType}.

Inductive nbh : {ereal R} -> predArgType :=
| NFin (c e : R) of (0 < e) : nbh c%:E
| NPInf (M : R) : nbh \+inf
| NNInf (M : R) : nbh \-inf.
| NPInf (M : R) : nbh +oo
| NNInf (M : R) : nbh -oo.

Coercion pred_of_nbh l (v : nbh l) :=
match v with
Expand All @@ -73,16 +73,16 @@ by move=> e eE v; case: v eE => // c' e' h [->].
Qed.

Lemma nbh_pinfW (P : forall x, nbh x -> Prop) :
(forall M, P _ (@NPInf R M)) -> forall (v : nbh \+inf), P _ v.
(forall M, P _ (@NPInf R M)) -> forall (v : nbh +oo), P _ v.
Proof.
move=> ih ; move: {-2}\+inf (erefl (@ERPInf R)).
move=> ih ; move: {-2}+oo (erefl (@ERPInf R)).
by move=> e eE v; case: v eE => // c' e' h [->].
Qed.

Lemma nbh_ninfW (P : forall x, nbh x -> Prop) :
(forall M, P _ (@NNInf R M)) -> forall (v : nbh \-inf), P _ v.
(forall M, P _ (@NNInf R M)) -> forall (v : nbh -oo), P _ v.
Proof.
move=> ih ; move: {-2}\-inf (erefl (@ERNInf R)).
move=> ih ; move: {-2}-oo (erefl (@ERNInf R)).
by move=> e eE v; case: v eE => // c' e' h [->].
Qed.
End NbhElim.
Expand Down Expand Up @@ -309,7 +309,7 @@ move=> cu cv; pose a := u \- lu%:S; pose b := v \- lv%:S.
have eq: (u \* v) =1 (lu * lv)%:S \+ ((lu%:S \* b) \+ (a \* v)).
move=> n; rewrite {}/a {}/b /= [u n+_]addrC [(_+_)*(v n)]mulrDl.
rewrite !addrA -[LHS]add0r; congr (_ + _); rewrite mulrDr.
by rewrite !(mulrN, mulNr) [X in X-_]addrCA subrr addr0 subrr.
by rewrite !(mulrN, mulNr) addrCA subrr addr0 subrr.
apply/(ncvg_eq eq); rewrite -[X in X%:E]addr0; apply/ncvgD.
by apply/ncvgC. rewrite -[X in X%:E]addr0; apply/ncvgD.
+ apply/ncvgMr; first rewrite -[X in X%:E](subrr lv).
Expand Down Expand Up @@ -429,7 +429,7 @@ Implicit Types (u v : nat -> R).

Definition nlim u : {ereal R} :=
if @idP `[exists l, `[< ncvg u l >]] is ReflectT Px then
xchooseb Px else \-inf.
xchooseb Px else -oo.

Lemma nlim_ncvg u : (exists l, ncvg u l) -> ncvg u (nlim u).
Proof.
Expand All @@ -439,15 +439,15 @@ move=> p; rewrite -[xchooseb _](ncvg_uniq cv_u_l) //.
by apply/asboolP/(xchoosebP p).
Qed.

Lemma nlim_out u : ~ (exists l, ncvg u l) -> nlim u = \-inf.
Lemma nlim_out u : ~ (exists l, ncvg u l) -> nlim u = -oo.
Proof.
move=> h; rewrite /nlim; case: {-}_ / idP => // p.
by case: h; case/existsbP: p => l /asboolP; exists l.
Qed.

CoInductive nlim_spec (u : nat -> R) : er R -> Type :=
| NLimCvg l : ncvg u l -> nlim_spec u l
| NLimOut : ~ (exists l, ncvg u l) -> nlim_spec u \-inf.
| NLimOut : ~ (exists l, ncvg u l) -> nlim_spec u -oo.

Lemma nlimP u : nlim_spec u (nlim u).
Proof.
Expand Down Expand Up @@ -521,7 +521,7 @@ Qed.
Lemma nlim_sumR {I : eqType} (u : I -> nat -> R) (r : seq I) :
(forall i, i \in r -> iscvg (u i)) ->
nlim (fun n => \sum_(i <- r) (u i) n)
= (\sum_(i <- r) (nlim (u i) : R))%:E.
= (\sum_(i <- r) (nlim (u i) : [numDomainType of R]))%:E.
Proof.
move=> h; rewrite nlim_sum //; elim: r h => [|i r ih] h.
by rewrite !big_nil.
Expand Down
7 changes: 4 additions & 3 deletions altreals/realsum.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -169,12 +169,12 @@ Context {R : realType}.
Lemma ncvg_mono (u : nat -> R) :
(* {mono u : x y / (x <= y)%N >-> u x <= u y *)
(forall x y, (x <= y)%N -> u x <= u y)
-> exists2 l, (\-inf < l)%E & ncvg u l.
-> exists2 l, (-oo < l)%E & ncvg u l.
Proof.
move=> mono_u; pose E := [pred x | `[exists n, x == u n]].
have nzE: nonempty E by exists (u 0%N); apply/imsetbP; exists 0%N.
case/boolP: `[< has_sup E >] => /asboolP; last first.
move/has_supPn=> -/(_ nzE) h; exists \+inf => //; elim/nbh_pinfW => M /=.
move/has_supPn=> -/(_ nzE) h; exists +oo => //; elim/nbh_pinfW => M /=.
case/(_ M): h=> x /imsetbP[K -> lt_MuK]; exists K=> n le_Kn; rewrite inE.
by apply/(ltr_le_trans lt_MuK)/mono_u.
move=> supE; exists (sup E)%:E => //; elim/nbh_finW=>e /= gt0_e.
Expand Down Expand Up @@ -490,7 +490,8 @@ Hypothesis smS : summable S.
Hypothesis homo_P : forall n m, (n <= m)%N -> (P n `<=` P m).
Hypothesis cover_P : forall x, S x != 0 -> exists n, x \in P n.

Lemma psum_as_lim : psum S = nlim (fun n => \sum_(j : P n) (S (val j))).
Lemma psum_as_lim :
psum S = (nlim (fun n => \sum_(j : P n) (S (val j))) : [numDomainType of R]).
Proof.
set v := fun n => _; have hm_v m n: (m <= n)%N -> v m <= v n.
by move=> le_mn; apply/big_fset_subset/fsubsetP/homo_P.
Expand Down
48 changes: 46 additions & 2 deletions classical_sets.v
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
From mathcomp Require Import ssreflect ssrfun ssrbool ssrnat eqtype choice.
From mathcomp Require Import ssralg matrix.
Require Import boolp.
From mathcomp Require Import ssralg matrix ssrnum.
Require Import boolp reals.

(******************************************************************************)
(* This file develops a basic theory of sets and types equipped with a *)
Expand Down Expand Up @@ -334,6 +334,9 @@ move=> [i Di]; rewrite predeqE => a; split=> [[Ifa Xa] j Dj|IfIXa].
by split=> [j /IfIXa [] | ] //; have /IfIXa [] := Di.
Qed.

Lemma setMT A B : (@setT A) `*` (@setT B) = setT.
Proof. by rewrite predeqE. Qed.

Definition is_prop {A} (X : set A) := forall x y, X x -> X y -> x = y.
Definition is_fun {A B} (f : A -> B -> Prop) := all (is_prop \o f).
Definition is_total {A B} (f : A -> B -> Prop) := all (nonempty \o f).
Expand Down Expand Up @@ -447,6 +450,47 @@ Canonical prod_pointedType (T T' : pointedType) :=
PointedType (T * T') (point, point).
Canonical matrix_pointedType m n (T : pointedType) :=
PointedType 'M[T]_(m, n) (\matrix_(_, _) point)%R.
Canonical zmod_pointedType (V : zmodType) := PointedType V 0%R.
Copy link
Member

@CohenCyril CohenCyril Oct 30, 2018

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Having a pointed type structure over something that is stable by product (and matrix) introduces a risk of inconsistency of the point operator. Indeed there would be two ways of getting it: as a pointed type of a product of as the product of two pointed type.
It would be ok to start with a realField (or realDomain? even though unnecessary), because the product of two realDomains cannot be a realDomain again.

Canonical ring_pointedType (R : ringType) :=
[pointedType of R for zmod_pointedType R].
Canonical lmod_pointedType (R : ringType) (V : lmodType R) :=
[pointedType of V for zmod_pointedType V].
Canonical lalg_pointedType (R : ringType) (A : lalgType R) :=
[pointedType of A for zmod_pointedType A].
Canonical comRing_pointedType (R : comRingType) :=
[pointedType of R for zmod_pointedType R].
Canonical alg_pointedType (R : comRingType) (A : algType R) :=
[pointedType of A for zmod_pointedType A].
Canonical unitRing_pointedType (R : unitRingType) :=
[pointedType of R for zmod_pointedType R].
Canonical comUnitRing_pointedType (R : comUnitRingType) :=
[pointedType of R for zmod_pointedType R].
Canonical unitAlg_pointedType (R : comUnitRingType) (A : unitAlgType R) :=
[pointedType of A for zmod_pointedType A].
Canonical idomain_pointedType (R : idomainType) :=
[pointedType of R for zmod_pointedType R].
Canonical field_pointedType (F : fieldType) :=
[pointedType of F for zmod_pointedType F].
Canonical decField_pointedType (F : decFieldType) :=
[pointedType of F for zmod_pointedType F].
Canonical closedField_pointedType (F : closedFieldType) :=
[pointedType of F for zmod_pointedType F].
Canonical numDomain_pointedType (R : numDomainType) :=
[pointedType of R for zmod_pointedType R].
Canonical numField_pointedType (R : numFieldType) :=
[pointedType of R for zmod_pointedType R].
Canonical numClosedField_pointedType (R : numClosedFieldType) :=
[pointedType of R for zmod_pointedType R].
Canonical realDomain_pointedType (R : realDomainType) :=
[pointedType of R for zmod_pointedType R].
Canonical realField_pointedType (R : realFieldType) :=
[pointedType of R for zmod_pointedType R].
Canonical archiField_pointedType (R : archiFieldType) :=
[pointedType of R for zmod_pointedType R].
Canonical rcf_pointedType (R : rcfType) :=
[pointedType of R for zmod_pointedType R].
Canonical real_pointedType (R : realType) :=
[pointedType of R for zmod_pointedType R].

Notation get := (xget point).

Expand Down
Loading