3
$\begingroup$
module badequality where
open import Relation.Binary.PropositionalEquality
open import Data.Nat using (ℕ; zero; suc; _<_)
open import Data.Empty using (⊥; ⊥-elim)

postulate
  f : ℕ → ℕ

anti-cong : {x y : ℕ} → f x < f y → x ≢ y
anti-cong fx<fy = {!   !} 

How to prove above anti-cong, or it only can be introduced by postulate.

$\endgroup$
0

2 Answers 2

7
$\begingroup$

Sure: you can use the fact that _<_ is irreflexive to derive a contradiction from the assumption that both f x < f y and x ≡ y are true.

This is how it goes:

open import Data.Nat.Properties using (<-irrefl)

anti-cong : {x y : ℕ} → f x < f y → x ≢ y
anti-cong fx<fy x≡y = <-irrefl (cong f x≡y) fx<fy
$\endgroup$
1
$\begingroup$

Motivated by @gallais's solution, I think there is a more natural solution:

We can prove contraposition first, which is (A → B) → (¬ B → ¬ A). Then we prove x ≡ y → f x ≥ f y, which is the contrapositive of original proposition. Finally, we apply contraposition to the contrapositive. Here is my code

open import Data.Nat using (ℕ; zero; suc; _<_; _≥_)
open import Data.Nat.Properties using (≤-reflexive; <⇒≱)
open import Relation.Nullary using (¬_)

contraposition : ∀ {A B : Set} → (A → B) → (¬ B → ¬ A)
contraposition f ¬b a = ¬b (f a)

=≥ : {x y : ℕ} → x ≡ y → f x ≥ f y
=≥ x=y = ≤-reflexive (cong f (sym x=y))  

anti-cong : {x y : ℕ} → f x < f y → x ≢ y
anti-cong {x} {y} fx<fy = contraposition (=≥ {x} {y}) (<⇒≱ fx<fy)  
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.