Reals: Make "Rsqr x" and an alias for "x^2"
メンテナーはふだん 2 日以内に返信
まだ誰も着手していません。
評価
- 難易度
- 5/5
- 見積もり時間
- 1週間以上
- 初心者へのやさしさ
- 25/100
- issue の種類
- リファクタリング
- 明瞭さ
- 説明が足りない
- 活発さ
- 停滞
- 領域
- devtools
調査の方向性
まず Rsqr、x^2、sqrt に関係する Reals ライブラリの定義を確認し、次に issue で言及されている field tactic と三角法の補題を調べます。cleanup を提案する前に CoqInterval へのパフォーマンス上の影響を確認してください。完了には、表現について合意し、ライブラリの動作が一貫していることが必要です。
索引モデルが issue の本文から書いたものです。
説明
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.)
- 主要言語
- Rocq Prover
- スター
- 43
- フォーク
- 39
- 平均マージ
- 4日 13時間
- マージ済み PR（30日）
- 6
環境構築
- Dockerfile・Docker Compose ファイルなし
- プルリクエストのテンプレートあり
- コントリビューションガイドを読む
はじめの一歩
- issue を最後まで読み、次にプロジェクトのコントリビューションガイドを読みます。
- 着手することを issue にコメントします — 二人が同じ作業をするのを防げます。
- リポジトリをフォークし、ブランチを切って変更します。
- issue 番号を参照したプルリクエストを送ります。
rocq-prover/stdlib のほかの issue
-
incl_dec and NoDup_dec should be Defined and not Qed再び着手できるかも このイシューのプルリクエストはマージされずにクローズされました。 オープン
難易度 1/5 1〜3時間 初心者へのやさしさ 65/100
rocq-prover/stdlib#25 ·
メンテナーはふだん 2 日以内に返信
-
Reals: a constructive pi for the constructive Cauchy reals with a strong irrationality separation theorem (Leibniz series)対応中かも @hy7pc8gfmf-dotcom が 16 日前に担当しました。 オープン
難易度 5/5 1週間以上 初心者へのやさしさ 6/100
rocq-prover/stdlib#315 ·
メンテナーはふだん 2 日以内に返信
-
Reals: escape-window separation engine for the constructive Cauchy reals (abstract irrationality criterion)対応中かも このイシューにリンクされたプルリクエストがオープン中、またはマージ済みです。 オープン
難易度 5/5 1週間以上 初心者へのやさしさ 35/100
rocq-prover/stdlib#312 ·
メンテナーはふだん 2 日以内に返信
-
難易度 5/5 1週間以上 初心者へのやさしさ 25/100
rocq-prover/stdlib#293 ·
メンテナーはふだん 2 日以内に返信
-
Inconsistent OPAM packaging of rocq-stdlib対応中かも このイシューにリンクされたプルリクエストがオープン中、またはマージ済みです。 オープン
難易度 4/5 3〜5日 初心者へのやさしさ 42/100
rocq-prover/stdlib#256 · コメント 4 件 · リアクション 3 件 ·
メンテナーはふだん 2 日以内に返信
rocq-prover/stdlib の issue をすべて見る
似ている issue
-
難易度 2/5 1〜3時間 初心者へのやさしさ 84/100
home-assistant/core#188424 ·
メンテナーはふだん 1 日以内に返信
-
docs good first issue
難易度 2/5 1〜3時間 初心者へのやさしさ 82/100
-
area: lockfile
難易度 2/5 1〜3時間 初心者へのやさしさ 76/100
メンテナーはふだん 1 日以内に返信
-
難易度 2/5 1〜3時間 初心者へのやさしさ 73/100
メンテナーはふだん 1 日以内に返信
-
難易度 2/5 1〜3時間 初心者へのやさしさ 82/100
limitlessprojects/Go-Hybrid#1595 ·
メンテナーはふだん 1 日以内に返信