如何在 Coq 中使用 Rmult 在一个术语中重写 Rle?

Posted

技术标签:

【中文标题】如何在 Coq 中使用 Rmult 在一个术语中重写 Rle?【英文标题】:How to rewrite over Rle inside a term with Rmult in Coq? 【发布时间】:2015-03-11 19:52:22 【问题描述】:

关于关系 Rle (Rplus (+) 和 Rminus (-) 内重写,因为两个二元运算符的两个位置都有固定的方差:

Require Import Setoid Relation_Definitions Reals.
Open Scope R.

Add Parametric Relation : R Rle
reflexivity proved by Rle_refl
transitivity proved by Rle_trans
as Rle_setoid_relation.

Add Parametric Morphism : Rplus with
signature Rle ++> Rle ++> Rle as Rplus_Rle_mor.
intros ; apply Rplus_le_compat ; assumption.
Qed.

Add Parametric Morphism : Rminus with
signature Rle ++> Rle --> Rle as Rminus_Rle_mor.
intros ; unfold Rminus ;
apply Rplus_le_compat;
[assumption | apply Ropp_le_contravar ; assumption].
Qed.

Goal forall (x1 x2 y1 y2 : R),
   x1 <= x2 -> y1 <= y2 ->
   x1 - y2 <= x2 - y1.
Proof.
  intros x1 x2 y1 y2 x1_le_x2 y1_le_y2;
  rewrite x1_le_x2; rewrite y1_le_y2;
  reflexivity.
Qed.

不幸的是,Rmult (*) 没有这个性质:方差取决于另一个被乘数是正数还是负数。是否可以定义条件态射,以便 Coq 执行重写步骤并简单地添加被乘数的非负性作为证明义务?谢谢。

【问题讨论】:

你总是可以试试coq-club邮件列表,你可能会走运:) 【参考方案1】:

我认为定义你想要的东西应该是可能的,但可能不是微不足道的。

但是,您可能对使用 math-comp 的代数层次结构的不同方法感兴趣,请参阅:

Lemma ler_pmul2l x : 0 < x → mono *%R x : x y / x ≤ y.

和相关的引理(http://math-comp.github.io/math-comp/htmldoc/mathcomp.algebra.s-s-rnum.html)。在 s-s-reflect 中,&lt;= 是一个布尔关系,因此可以进行原版重写,因为 a &lt;= b 真的意味着 a &lt;= b = true

【讨论】:

以上是关于如何在 Coq 中使用 Rmult 在一个术语中重写 Rle?的主要内容,如果未能解决你的问题,请参考以下文章

如何在 Coq 中从见证人那里引入新的存在条件?

coq 中存在变量的实例化规则

如何在 Coq 中使用归纳类型处理案例

如何在 Coq 中使用包含全称量词的假设?

如何在 Coq 中将直线公理定义为两点

Coq 中同一个库的不同版本