CODEWITHSUNDEEP
agdatheorem-proving
Sergestus
Sergestus

Reputation: 173

Proving the false case of an if and only if in Agda

I am trying to understand how to create a working "if and only if" statement in agda but have problems in proving the false cases for it, also in using induction in the proof. As an example I want to work with "less than or equal", which I define as:

data ℕ : Set where
  zero : ℕ
  succ : ℕ → ℕ

data _leq_ : ℕ → ℕ → Set where
  0≤n : ∀ {n : ℕ} → zero leq n
  Sn≤Sm : ∀ {n m : ℕ} → (n leq m) → ((succ n) leq (succ m))

To define A if and only if B, we want a pair of functions taking proofs of A to proofs of B and vice versa, so I define:

record _∧_ (A B : Set) : Set where
  constructor _,_
  field
    fst : A
    snd : B
open _∧_

_iff_ : (A B : Set) → Set
A iff B = (A → B) ∧ (B → A)

Now to my problem: I want to prove the statement that (n <= m+1) <=> (n+1 <= m+2) so formulate the following:

prop₂ : ∀ (n m : ℕ) → (n leq (succ m)) iff ((succ n) leq (succ (succ m))) 
prop₂ zero zero = (λ x → Sn≤Sm 0≤n) , λ x → 0≤n
prop₂ zero (succ b) = (λ x → Sn≤Sm 0≤n) , (λ x → 0≤n)
prop₂ (succ a) zero = ?
prop₂ (succ a) (succ b) = ?

My issues are

Upvotes: 3

Views: 601

Answers (2)

oisdk
oisdk

Reputation: 10091

I'd also like to add that this is a perfect candidate for copattern matching.

prop₂ : ∀ (n m : ℕ) → (n leq (succ m)) iff ((succ n) leq (succ (succ m)))
prop₂ n m .fst n≤m+1 = Sn≤Sm n≤m+1
prop₂ n m .snd (Sn≤Sm n≤m+1) = n≤m+1

Upvotes: 3

MrO
MrO

Reputation: 1347

If I stick to your development, the proof is done as follows:

prop₂ : ∀ (n m : ℕ) → (n leq (succ m)) iff ((succ n) leq (succ (succ m))) 
prop₂ zero zero = (λ x → Sn≤Sm 0≤n) , λ x → 0≤n
prop₂ zero (succ b) = (λ x → Sn≤Sm 0≤n) , (λ x → 0≤n)
prop₂ (succ a) zero = Sn≤Sm , λ {(Sn≤Sm x) → x}
prop₂ (succ a) (succ b) = Sn≤Sm , λ {(Sn≤Sm x) → x}

However, there is a much better way to prove such property. As you can see, there are redondancies in the code due to the fact that you case split on the parameters a and b instead of case splitting on the proof elements about them, which contain all the information you need. This leads to the following proof, which is much more elegant and concise:

prop-better : ∀ {n m : ℕ} → (n leq (succ m)) iff ((succ n) leq (succ (succ m))) 
prop-better = Sn≤Sm , λ {(Sn≤Sm x) → x}

The first direction of the equivalence is simply the Sn≤Sm constructor by definition, and the other side is done by case-splitting on the proof argument, which is necessarily of the form Sn≤Sm x since the two naturals are of the form succ y. This gives you the proof x which is exactly what you require.

Upvotes: 3

Related Questions