andrejbauer / dedekind-reals Goto Github PK
View Code? Open in Web Editor NEWA formalization of the Dedekind real numbers in Coq [maintainer=@andrejbauer]
License: MIT License
A formalization of the Dedekind real numbers in Coq [maintainer=@andrejbauer]
License: MIT License
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?
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.
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?
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.
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:
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.
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?
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
.
A declarative, efficient, and flexible JavaScript library for building user interfaces.
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
An Open Source Machine Learning Framework for Everyone
The Web framework for perfectionists with deadlines.
A PHP framework for web artisans
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
Some thing interesting about web. New door for the world.
A server is a program made to process requests and deliver data to clients.
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Some thing interesting about visualization, use data art
Some thing interesting about game, make everyone happy.
We are working to build community through open source technology. NB: members must have two-factor auth.
Open source projects and samples from Microsoft.
Google ❤️ Open Source for everyone.
Alibaba Open Source for everyone
Data-Driven Documents codes.
China tencent open source team.