andrejbauer / dedekind-reals Goto Github PK

Hello,

Admitted theorem Req_neq in file Order.v is probably false in constructive mathematics, because equality is not decidable on the real numbers. Do you rely on some non-constructive axioms, or do you have a proof of it?

Also I think that this implementation of Dedekind reals would also be Cauchy-complete, if the located hypothesis was a sumbool instead of a disjunction in sort Prop. Is there a reason for using Prop here?

Hi Andrej,

I think that upper_bound : {r : Q | upper r} won't let you define the inverse of a real number, because of the sort Type.

Take a positive real number x, but very very small. Then a rational number q > 1/x will be gigantic, and the only way to compute it is to find a rational number 0 < r < x. That suggests to use lower_open x 0, but you cannot because it is in sort Prop.

Anyway why did you use the sort Type for the bounds and the sort Prop everywhere else ? As we already discussed you want the Dedekind reals, not the Cauchy reals, so you probably want Prop everywhere.

V svojem dokazu želim uporabiti archimedean lemmo, imam pa nek q:Q (za katerega lahko dokažem da je pozitiven). Kako coq-u dopovedati da je q tudi tipa QPositive in ga zato lahko uporabim kot vhod za lemmo?

Pri npr. Metric.v "uvozimo" knjižnice z ukazi
Require Import Setoid SetoidClass.
Require Import QArith Qabs.
Require Import MiscLemmas.
meni se pritoži, češ
Error: Cannot find library MiscLemmas in loadpath
Potem sem Require Import nadomestil z Load. To sem delal pred spremembami, ki so se pojavile v torek, 26. Problem je bil, saj pomojem, tale:

• Require import deluje samo za knjižnice, ki so že vgrajene v Coq-u.
• Load pa se uporablja za uvoz "knjižnic", ki jim mi napišemo, to so npr. MiscLemmas.v, Cut.v, itd.

Ko sem to naredil, je bilo treba popraviti še nekaj.
V Arithmetic.v je bilo po moji spremembi Require import <-> Load na začetku
Load Cut.
Load Lipschitz.
Motilo ga je (saj pomojem): Arithmetic.v kliče Lipschitz.v in Cut.v. Ampak tudi Lipschitz.v kliče Cut.v. Tako se Cut.v pokliče dvakrat. Ko sem iz Arithmetic.v pobrisal vrstico Load Cut. je pa bil (končno) zadovoljen. Zgleda kot, da noče "povoziti" že klicane knjižnice z isto?

Kakorkoli že, to je delovalo pri starih (tj. pred 26.11.) Arithmetic.v, Lipschitz.v, Cut.v, Misclemmas.v. Danes sem pri prenovljenih poskusil isti trik, vendar ne dela, navaja nekaj v zvezi s Setoid Q in compose.

Zdi se mi, da nam gre precej dobro, edino ne vem, kam je izginila Petra. Petra, a ti misliš narediti ta predmet? Jaz se bom spravil malo nad Multiplication.v, ker ima največ admit-ov, razen če se kdo od vas grebe. Bom delal najprej najtežje dele.

I am giving up on the fancy setup with Lipschitz maps. Even if it worked, the students would not understand what is going on. So we are going to do things with bare hands. I started to define addition and basic properties of the additive structure. There are a bunch of admit's there, most of them are easy. So the students can now start working on things.

Vem, da je tole na zadnji moment, ampak če bi se jutri dobili od 12h do 14h na seminarju, kdo bi prišel?

It seems that Rlt should be defined as {q : Q | ....} instead of exists q, ...., otherwise we cannot get Rlt_linear with +, but we need that to get locatedness in RCut_of_R.