1

我正在尝试使用 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：我无法提供一个最小的工作示例，因为我并没有完全掌握我在这里所做的事情；）

4

1 回答 1

3

您可能已经注意到，从nattorat有两个嵌入：首先是 from natto int，然后是 from intto rat。后者是环态射，因此您可以使用通用态射定理，例如rmorphMand 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 _ _假设我对（以下缩写为pand p'）、'ctr _ _（以下缩写为cand 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.
于 2021-02-21T00:20:04.577 回答