问题标签 [ssreflect]

在ℝn-n维欧几里得空间R^n与标准内积，即点积，Cauchy-Schwarz不等式变为：[1]：https ://i.stack.imgur.com/ZNBfx.png

有没有人知道 Coq 中 Cauchy-Schwartz 不等式总和的实现，例如 infotheo？

我一直在寻找一个ssreflect表示总和线性的引理，以便我可以转换

进入

然后导出为

在这种情况下哪个可能合适？

目标：

我的目的是说，如果我们有

然后

如果目标如下所示，那么合适的策略是什么：

已编辑。上下文包含：

之后的目标rewrite /=.是这样的：

我是一名初学者，希望您能帮助我将事件 F 的概率和事件非 F 的概率相加为一。有没有快速前进的方法？

===

这是我的问题的一个最小示例

Lemma arith: forall T (G: seq T), (size G + 1 + 1).+1 = (size G + 3).

我希望能够将其减少到 forall T (G: seq T), (size G + 2).+1 = (size G + 3).

用最简单的方法。立即尝试 simpl 或 auto 无济于事。

如果我先用关联性重写，也就是说，

intros. rewrite - addnA. simpl. auto.,

simpl 和 auto 仍然什么都不做。我的目标是

(size G + (1 + 1)).+1 = size G + 3

我猜 .+1 以某种方式在 (1+1) 上进行简单和自动工作的“方式”。看来我必须先删除 .+1 才能简化 1+1。

然而，在我的实际证明中，除了 .+1 之外，还有很多东西“挡道”，我真的很想先简化我大量的 +1。作为一个黑客，我在个别事件上使用“替换”，但这感觉非常笨拙（并且有很多不同的算术表达式要替换）。有没有更好的方法来做到这一点？

我正在使用 ssrnat 库。

谢谢。

嗯，代码

错误是 is之前Error: Case analysis on sort Set is not allowed for inductive definition or. 的最后一个目标case

我已经rewrite leq_eqVlt => /orP; case在非常相似的情况下使用了这种构造 ( ) 并且它确实有效：

1. 两种情况有什么区别？
2. 以及为什么“归纳定义或不允许对排序集进行案例分析”？

我喜欢在目标是暗示的情况下（例如 A -> B）使用库中的move=>策略ssreflect，以使前提成为假设，并使结论成为新目标。但是，我并不总是想使用ssreflect.

是否有另一种 Coq 策略可以在不使用 的情况下做同样的事情ssreflect？

使用 ssreflect，我爱上了它积极管理进出目标的活页夹的风格。但是，我在从其文档中搜索我想要的内容时遇到了问题。

特别是，我找不到该策略的 ssreflectinversion策略。

我知道我可以很好地使用inversion战术。然而，它在使用活页夹时遵循了传统的 coq 风格，我很难为每个分支指定正确的名称，因为它从多目标视图中“隐藏”了。同时，ssreflect 策略总是将绑定器释放到目标中，因此我可以将名称绑定到类似的move。

例如，通过在 上应用反转Forall2 R l m，我得到

这是我不喜欢的名称，并且跟踪和指定这些名称会很痛苦，因为绑定隐藏在第二个分支后面（第一个分支只是l = m = []）。

如果我想以 ssreflect 风格反转归纳类型，我可以使用什么？可以elim用于某种反转吗？

在试图证明 ssreflect 中的一些相等性时，我得到了以下结果：

WTS: forall (a b: ~ false), a = b

这基本上是

WTS: forall (a b: false <> true), a = b.

知道以下内容具有建设性，

bool_irrelevance (b: bool): (x y: b), x = y

我想知道是否有可能WTS建设性地证明。由于 所需的可判定相等性为{x = y} + {x <> y}，我认为它可能无需公理即可证明。这是可以证明的吗？

此外，是否有可能证明与道具无关的证据False -> False？

请注意，我确实可以使用证明无关公理。简单地询问是否有办法避免使用公理。

我有下一个定义（可以编译代码）：

我想证明以下引理：

• case E: _ _ / H => // [v1' t1' v2' t2' jv1 jv2].离开E : VPair v1 v2 = VPair v1' v2'我。
• case E: _ / H => // [v1' t1' v2' t2TPair t1 t2 = TPair t1' t2'' jv1 jv2].离开E : TPair t1 t2 = TPair t1' t2'我。

但在我看来，我需要他们两个在一起。如何？