Getting better inference for agda proofs

Question

Suppose I have the following Agda code which compiles (where +-assoc and +-comm are taken from the plf course. It seems labourious to require the explicit sub expressions in each step in order for the code to simplify; however removing any one of the explicit expressions causes the code to fail to compile.

How can I get better type inference when writing proofs?

+-swap : ∀ (m n p : ℕ) -> m + (n + p) ≡ n + (m + p)
+-swap zero n p = refl
+-swap (suc m) n p =
  begin
    suc m + (n + p)
    ≡⟨ +-comm (suc m) (n + p) ⟩
    (n + p) + (suc m)
    ≡⟨ +-assoc n p (suc m) ⟩
    n + (p + suc m)
    ≡⟨ cong (n +_) (+-comm p (suc m)) ⟩
    n + (suc m + p)
  ∎

MrO MrO · Accepted Answer · 2020-06-30T11:48:10

If my understanding of your requirement is correct, you would like to be able to omit the intermediate expressions such as suc m + (n + p)

The whole point of the ≡-Reasoning module which provides the user with operators such as _∎, _≡⟨_⟩_ and begin_ is to make these quantities explicit so that the proof is more readable, and each reasoning step can be shown and understood clearly.

This means that if you want to omit these quantities, you should not use this library, and instead use one of the following methods to prove such equality proofs.

In a purpose of self-containment, here are the required imports:

module EqProofs where

open import Data.Nat
open import Data.Nat.Properties
open import Relation.Binary.PropositionalEquality
open ≡-Reasoning

A first possibility is to use the equality reasoning module, as you did:

+-swap₁ : ∀ (m n p : ℕ) → m + (n + p) ≡ n + (m + p)
+-swap₁ zero n p = refl
+-swap₁ (suc m) n p = begin
  suc m + (n + p)   ≡⟨ +-comm (suc m) (n + p) ⟩
  (n + p) + (suc m) ≡⟨ +-assoc n p (suc m) ⟩
  n + (p + suc m)   ≡⟨ cong (n +_) (+-comm p (suc m)) ⟩
  n + (suc m + p)   ∎

But you can also give the term explicitly using the transitivity of the equality:

+-swap₂ : ∀ (m n p : ℕ) → m + (n + p) ≡ n + (m + p)
+-swap₂ zero _ _ = refl
+-swap₂ (suc m) n p =
  trans
    (+-comm (suc m) (n + p))
    (trans
      (+-assoc n p (suc m))
      (cong (n +_) (+-comm p (suc m))))

Or you can use rewrite to simplify the goal using equality proofs:

+-swap₃ : ∀ (m n p : ℕ) → m + (n + p) ≡ n + (m + p)
+-swap₃ zero _ _ = refl
+-swap₃ (suc m) n p
  rewrite +-comm (suc m) (n + p)
  | +-assoc n p (suc m)
  | cong (n +_) (+-comm p (suc m)) = refl

In the two last possibilities, the intermediate quantity are hidded (and easily inferred by Agda), as you wanted.

Edit:

You can omit some of (not all of them though, since the type checker needs information to solve constraints) the required parameters using underscores. This can be done in all cases except when using rewrite, as follows:

+-swap₁ : ∀ (m n p : ℕ) → m + (n + p) ≡ n + (m + p)
+-swap₁ zero n p = refl
+-swap₁ (suc m) n p = begin
  suc m + (n + p)   ≡⟨ +-comm _ (n + p) ⟩
  (n + p) + (suc m) ≡⟨ +-assoc n p _ ⟩
  n + (p + suc m)   ≡⟨ cong (n +_) (+-comm p _) ⟩
  n + (suc m + p)   ∎

+-swap₂ : ∀ (m n p : ℕ) → m + (n + p) ≡ n + (m + p)
+-swap₂ zero _ _ = refl
+-swap₂ (suc m) n p =
  trans
    (+-comm _ (n + p))
    (trans
      (+-assoc n p _)
      (cong (n +_) (+-comm p _)))

+-swap₃ : ∀ (m n p : ℕ) → m + (n + p) ≡ n + (m + p)
+-swap₃ zero _ _ = refl
+-swap₃ (suc m) n p
  rewrite +-comm (suc m) (n + p)
  | +-assoc n p (suc m)
  | cong (n +_) (+-comm p (suc m)) = refl

Edit n°2:

As a side note, you can prove this property without having to pattern match on either of its arguments. Here is this proof, using chained equality. You can noticed that only a few parameters have to be explicitly provided, while the others can be replaced by underscores:

+-swap₄ : ∀ (m n p : ℕ) → m + (n + p) ≡ n + (m + p)
+-swap₄ m n p = begin
  m + (n + p) ≡⟨ +-assoc m _ _ ⟩
  (m + n) + p ≡⟨ cong (_+ p) (+-comm m _) ⟩
  (n + m) + p ≡⟨ +-assoc n _ _ ⟩
  n + (m + p)  ∎

Getting better inference for agda proofs

1 Answers