CODEWITHSUNDEEP
proofidris2
Hermes
Hermes

Reputation: 21

Prove max x y = y given that x <= y in Idris 2?

I am new to Idris2 and need some guidance on proving the following relationship:

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

I read in the docs that the constructors for LTE aren't exported so I don't even know where to start.

Upvotes: 1

Views: 45

Answers (1)

Hermes
Hermes

Reputation: 21

A solution using maximum instead of max is

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

Upvotes: 1

Related Questions