关于的案例分析
关于的案例分析
提问于 2022-06-21 02:52:06
我的目标如下：
maxr x0 x我想做一个案例分析，考虑在x0是最大的情况下发生的情况，以及x是最大的情况。这在ssreflect中是可能的吗？
通常，它将类似于(例如，使用if语句)。
have [ something | something'] := ifP但是，我无法找到适当的语法来使用max进行案例分析。
回答 1
Stack Overflow用户
回答已采纳
发布于 2022-06-21 07:36:52
您可以使用lerP或ltrP
Check lerP.
(*
lerP
: forall (R : realDomainType) (x y : R),
ler_xor_gt (R:=R) x y (minr y x) (minr x y)
(maxr y x) (maxr x y) `|(x - y)%R| `|(y - x)%R|
(x <= y)%R (y < x)%R
*)在行动中：
From mathcomp Require Import all_ssreflect all_algebra.
Import Num.Def Num.Theory.
Goal forall a b : int, maxr a b = a.
move=> a b.
case: lerP.
(*
2 goals (ID 4070)
a, b : int
============================
(a <= b)%R -> b = a
goal 2 (ID 4071) is:
(b < a)%R -> a = a
*)
Abort.我在Search maxr.中找到了它们，这不是最快的方法(它显示了几个结果)，但至少它有效。
页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持
原文链接：
https://stackoverflow.com/questions/72694848
复制相关文章
相似问题
腾讯云开发者
