最大值的案例分析

Question

我的目标有以下内容：

maxr x0 x

我想进行案例分析，以考虑在X0最大的情况下发生的情况，而X的情况是最大的。这可以在sssreflect中吗？

通常，这将是类似的（例如使用语句），

have [ something | something'] := ifP

但是，我找不到适当的语法可以使用Max进行案例分析。

Answer 1

您可以使用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。 ，这不是最快的方法（它显示了几个结果），但至少它有效。