将证明从 Nat 翻译成 Rat

Question

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

Answer 1

您可能已经注意到，从 nat 到 rat 有两个嵌入：第一个是从 nat 到 int，然后是从 int至 rat。后者是环态射，因此您可以使用通用态射定理，例如 rmorphM 和 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 和 p'）、'ctr _ _（此后缩写为 c 和 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.

将证明从 Nat 翻译成 Rat

Translating proof from Nat to Rat

coq

ssreflect