coq - 将证明从 Nat 翻译为 Rat
问题描述
我正在尝试使用 CoQ/SSReflect 证明nat
来证明rat
. 中的当前证明状态Open Scope ring_scope
是
(price bs i - price bs' i <= tnth bs i * ('ctr_ (sOi i) - 'ctr_ (sOi i')))%N
→ (price bs i)%:~R - (price bs' i)%:~R <=
(value_per_click i)%:~R * (('ctr_ (sOi i))%:~R - ('ctr_ (sOi i'))%:~R)
并且,使用Set Printing All
,它显示为
forall
_ : is_true
(leq (subn (price bs i) (price bs' i))
(muln (@nat_of_ord p (@tnth n bid bs i))
(subn (@nat_of_ord q (@tnth k ctr cs (sOi i)))
(@nat_of_ord q (@tnth k ctr cs (sOi i')))))),
is_true
(@Order.le ring_display (Num.NumDomain.porderType rat_numDomainType)
(@GRing.add rat_ZmodType
(@intmul (GRing.Ring.zmodType rat_Ring) (GRing.one rat_Ring) (Posz (price bs i)))
(@GRing.opp rat_ZmodType
(@intmul (GRing.Ring.zmodType rat_Ring) (GRing.one rat_Ring) (Posz (price bs' i)))))
(@GRing.mul rat_Ring
(@intmul (GRing.Ring.zmodType rat_Ring) (GRing.one rat_Ring)
(Posz (value_per_click i)))
(@GRing.add (GRing.Ring.zmodType rat_Ring)
(@intmul (GRing.Ring.zmodType rat_Ring) (GRing.one rat_Ring)
(Posz (@nat_of_ord q (@tnth k ctr cs (sOi i)))))
(@GRing.opp (GRing.Ring.zmodType rat_Ring)
(@intmul (GRing.Ring.zmodType rat_Ring) (GRing.one rat_Ring)
(Posz (@nat_of_ord q (@tnth k ctr cs (sOi i')))))))))
我一直在尝试使用各种rewrite
,例如ler_nat
, PoszM
, intrM
,但收效甚微。谁能给我一些关于如何进行的提示?
PS:我无法提供一个最小的工作示例,因为我并没有完全掌握我在这里所做的事情;)
解决方案
您可能已经注意到,从nat
torat
有两个嵌入:首先是 from nat
to int
,然后是 from int
to rat
。后者是环态射,因此您可以使用通用态射定理,例如rmorphM
and rmorphB
,在您的情况下,您可以从rewrite -!rmorphB -rmorphM ler_int.
然而,前一个嵌入 ( Posz : nat -> int
) 不是环态射,您仍然可以使用PoszM
确实 (Posz
是乘法的),但主要问题是Posz (m - n) != Posz m - Posz n
一般情况下(强制的静默插入使问题变得复杂)。因此,您似乎需要同时假设(price bs' i <= price bs i)%N
和'ctr_ (sOi i') <= 'ctr_ (sOi i)
。但是,多亏了您,leq_subLR
您可以避免第一个假设。
这是您的问题和解决方案的模型(如果您无法最小化,那么拥有完整的上下文会很好)。price _ _
假设我对(以下缩写为p
and p'
)、'ctr _ _
(以下缩写为c
and c'
)和value_per_click _
(缩写)的正确类型进行了逆向工程v
:
Lemma test (p p' v c c' : nat) : (c' <= c)%N -> (p - p' <= v * (c - c'))%N ->
p%:~R - p'%:~R <= v%:~R * (c%:~R - c'%:~R) :> rat.
Proof.
rewrite leq_subLR => le_c'c le_pp'_vMcc'. (* Removing the first subn. *)
rewrite -!rmorphB -rmorphM ler_int. (* Changing rat goal into int goal. *)
by rewrite ler_subl_addl subzn. (* Changing int goal into nat goal. *)
(* The rest of the proof was actually carried out using conversion. *)
Qed.
推荐阅读
- gitlab - GitLab Auto DevOps 失败 - 参考格式无效
- erlang - 使用 OpenAPI 生成器中的存根
- angular - 使用 Angular 6 中的自定义表单控件进行自定义验证
- reporting-services - SSRS 错误:无法加载文件夹内容。SQL 服务器 2016
- azure-bot-service - 使用 JS 从 azure healthbot 调用 rest api
- list - AHK 多维列表可使用箭头键和 Enter 导航
- sql - SQL Server TABLOCKX 未锁定表
- javascript - 按月和年对数组进行排序
- c# - 如何在后续瀑布步骤中检索自适应卡的表单提交
- css - Safari 的不同行为和样式