证明 max x y = y 给定 x <= y in Idris 2?

Question

我是 Idris2 的新手，需要一些指导来证明以下关系：

simplify_max : (LTE x y) -> (max x y) = y
simplify_max prf = ?code

我在文档中读到，LTE 的构造函数没有导出，所以我什至不知道从哪里开始。

Answer 1

使用

maximum

代替

max

的解决方案是

simplify_max : (a: Nat) -> (b: Nat) -> LTE a b -> maximum a b = b
simplify_max Z Z _ = Refl
simplify_max Z (S k) _ = Refl
simplify_max (S k) (S j) prf = let e = simplify_max k j (fromLteSucc prf) in
                                rewrite e in Refl