Reals: Make "Rsqr x" and an alias for "x^2"
Nessuno ha ancora preso questa issue.
Valutazione
- Difficoltà
- 5/5
- Tempo stimato
- Più di una settimana
- Idoneità per principianti
- 25/100
- Tipo di issue
- Refactoring
- Chiarezza
- Da chiarire
- Stato di attività
- Ferma
- Ambito
- devtools
Direzione di ricerca
Inizia esaminando le definizioni della libreria Reals che coinvolgono Rsqr, x^2 e sqrt, quindi esamina la field tactic e i lemmi trigonometrici menzionati nell’issue. Verifica le implicazioni sulle prestazioni per CoqInterval prima di proporre la pulizia; per completare il lavoro è necessario concordare la rappresentazione e garantire un comportamento coerente della libreria.
Scritto dal modello di indicizzazione a partire dal testo della issue.
Descrizione
Some developments of the Reals library use a wild mix between Rsqr x (aka x²) and x^2. the field tactic supports (afaikt) only x^2 while most of the lemmas connecting x^2 and sqrt use Rsqr. Trigonometric lemmas use a mix of both. As a result many proofs have to convert between the two forms from time to time. Also proof search is made substantially harder by this.
I would suggest to clean this up by making Rsqr an alias for x^2. The small performance advantage given by Rsqr should not be significant and less important that cleanliness and usability of the library.
@silene, @thery : can you please comment on this, especially also on the performance implications e.g. in CoqInterval (I always used x^2 there btw.)
- Lingua principale
- Rocq Prover
- Stelle
- 42
- Fork
- 40
- Merge medio
- 20h 23m
- PR unite (30g)
- 2
Preparare l'ambiente
- Nessun Dockerfile né file Docker Compose
- Ha un modello di pull request
- Leggi la guida per i contributori
Come iniziare
- Leggi tutta la issue e poi la guida ai contributi del progetto.
- Commenta sulla issue per dire che te ne occupi tu — evita che due persone facciano lo stesso lavoro.
- Fai un fork del repository e lavora su un branch.
- Apri una pull request che faccia riferimento al numero della issue.
Altre issue di rocq-prover/stdlib
-
incl_dec and NoDup_dec should be Defined and not QedForse di nuovo libera Una pull request per questa issue è stata chiusa senza essere unita. Aperta
Difficoltà 1/5 1-3 ore Idoneità per principianti 65/100
rocq-prover/stdlib#25 ·
-
Reals: escape-window separation engine for the constructive Cauchy reals (abstract irrationality criterion)Forse già presa Una pull request collegata a questa issue è aperta o già unita. Aperta
Difficoltà 5/5 Più di una settimana Idoneità per principianti 35/100
rocq-prover/stdlib#312 ·
-
Maintaining NaryFunctionsAperta
Difficoltà 5/5 Più di una settimana Idoneità per principianti 25/100
rocq-prover/stdlib#293 ·
-
`QArith`: Add more rounding modes to complement `Qfloor` and `Qceiling`Forse già presa @RyanGlScott l’ha presa 87 giorni fa. Aperta
Difficoltà 3/5 1-2 giorni Idoneità per principianti 52/100
rocq-prover/stdlib#283 · 2 commenti ·
-
Inconsistent OPAM packaging of rocq-stdlibForse già presa Una pull request collegata a questa issue è aperta o già unita. Aperta
Difficoltà 4/5 3-5 giorni Idoneità per principianti 42/100
rocq-prover/stdlib#256 · 4 commenti · 3 reazioni ·
Tutte le issue di rocq-prover/stdlib
Issue simili
-
Service process inherits the caller's cwd at first use, holding that folder open on Windows (EBUSY)Aperta
Difficoltà 2/5 1-3 ore Idoneità per principianti 76/100
-
enhancement
Difficoltà 2/5 1-3 ore Idoneità per principianti 65/100
liquid-java/liquidjava#373 ·
I maintainer di solito rispondono entro 1 giorno
-
[bug] diagnostics.dumpBody：Buffer 形态请求（透传 lane）跳过 dumps/ 落盘，仅留 raw/-unknown-Forse già presa @ranxianglei l’ha presa oggi. Aperta
Difficoltà 2/5 1-3 ore Idoneità per principianti 62/100
ranxianglei/billion-context#2421 · 2 commenti ·
I maintainer di solito rispondono entro 1 giorno
-
Ploidy optionApertaenhancement
Difficoltà 2/5 1-3 ore Idoneità per principianti 65/100
I maintainer di solito rispondono entro 2 giorni
-
Difficoltà 2/5 1-3 ore Idoneità per principianti 65/100