将证明从Nat转换为Rat

Question

我正在尝试使用一个使用nat的CoQ/SSReflect证明来证明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.