Functional reasoning

Question

Some imports and definitions first.

open import Level hiding (suc)
open import Relation.Binary.PropositionalEquality
open import Data.Nat
open import Algebra
open import Data.Nat.Properties
open CommutativeSemiring commutativeSemiring hiding (_+_; _*_; sym)

data Even : ℕ -> Set where
  ezero : Even 0
  esuc  : {n : ℕ} -> Even n -> Even (suc (suc n))

_^2 : ℕ -> ℕ
n ^2 = n * n

unEsuc : {n : ℕ} -> Even (suc (suc n)) -> Even n
unEsuc (esuc e) = e

remove-*2 : (n : ℕ) -> {m : ℕ} -> Even (n + n + m) -> Even m
remove-*2  0          e = e
remove-*2 (suc n) {m} e
    with subst (λ n' -> Even (suc (n' + m))) (+-comm n (suc n)) e
... | esuc e1 = remove-*2 n e1

Now I want to prove {n : ℕ} -> Even (n ^2) -> Even n in a nice way, similar to ≡-Reasoning. I've finished with

infix 4 ∈_

data ∈Wrap {α : Level} {A : Set α} : A -> Set α where
  ∈_ : (x : A) -> ∈Wrap x

infix 3 #⟨_⟩_
infixl 2 _$⟨_⟩'_ _$⟨_⟩_

#⟨_⟩_ : {α : Level} {A : Set α} -> A -> ∈Wrap A -> A
#⟨ x ⟩ _ = x

_$⟨_⟩'_ : {α β : Level} {A : Set α} {B : A -> Set β}
        -> (x : A) -> (f : (x : A) -> B x) -> ∈Wrap (B x) -> B x
x $⟨ f ⟩' _ = f x

_$⟨_⟩_ : {α β : Level} {A : Set α} {B : Set β}
       -> A -> (A -> B) -> ∈Wrap B -> B
_$⟨_⟩_ = _$⟨_⟩'_

even-sqrt : {n : ℕ} -> Even (n ^2) -> Even n
even-sqrt {0}            ezero   = ezero
even-sqrt {1}            ()
even-sqrt {suc (suc n)} (esuc e) =
    #⟨ e ⟩ ∈
  Even (n + suc (suc (n + n * suc (suc n))))
    $⟨ subst Even (+-comm n (suc (suc (n + n * suc (suc n))))) ⟩ ∈
  Even (suc (suc (n + n * suc (suc n) + n)))
    $⟨ unEsuc ⟩ ∈
  Even (n + n * suc (suc n) + n)
    $⟨ subst (λ n' -> Even (n' + n)) (+-comm n (n * suc (suc n))) ⟩ ∈
  Even (n * suc (suc n) + n + n)
    $⟨ subst (λ n' -> Even (n' + n + n)) (*-comm n (suc (suc n))) ⟩ ∈
  Even (n + (n + n * n) + n + n)
    $⟨ subst (λ n' -> Even (n' + n + n)) (sym (+-assoc n n (n * n))) ⟩ ∈
  Even (n + n + n * n + n + n)
    $⟨ subst Even (+-assoc (n + n + n * n) n n) ⟩ ∈
  Even (n + n + n * n + (n + n))
    $⟨ subst Even (+-assoc (n + n) (n * n) (n + n)) ⟩ ∈
  Even (n + n + (n * n + (n + n)))
    $⟨ remove-*2 n ⟩ ∈
  Even (n * n + (n + n))
    $⟨ subst Even (+-comm (n * n) (n + n)) ⟩ ∈
  Even (n + n + n * n)
    $⟨ remove-*2 n ⟩ ∈
  Even (n * n)
    $⟨ even-sqrt ⟩ ∈
  Even n
    $⟨ esuc ⟩ ∈
  Even (suc (suc n))

Is there any standard reasoning for such purposes?

Answer 1

I am not aware of anything inside Agda's standard library, but it provides almost what you need in the Function module. You can do without ∈Wrap. Let me propose a little syntactic sugar:

infix 4 _⟧
infixr 3 _─_⟶_
infix 2 _⟦_

_⟧ : ∀ {α} → (A : Set α) → A → A
_⟧ _ = id

_⟦_ : ∀ {α β} {A : Set α} → (a : A) → {B : A → Set β} → ((x : A) → B x) → B a
a ⟦ f = f a

_─_⟶_ : ∀ {α β γ} (A : Set α) → {B : A → Set β} → (f : (a : A) → B a) →
        {C : {a : A} → (b : B a) → Set γ} → (∀ {a} → (b : B a) → C b) →
        (a : A) → C (f a)
A ─ f ⟶ g = g ∘ f

Then you can write your proof as:

...
even-sqrt {suc (suc n)} (esuc e) = e ⟦
  Even (n + suc (suc (n + n * suc (suc n))))
    ─ subst Even (+-comm n (suc (suc (n + n * suc (suc n))))) ⟶
...
    ─ remove-*2 n ⟶
  Even (n * n)
    ─ even-sqrt2 {n} ⟶
  Even n
    ─ esuc ⟶
  Even (suc (suc n)) ⟧

The main benefits of this variant are:

• There is no wrapper type. You are just working with functions.
• The nesting is done the right way. With the approach presented in the question, you cannot refine a hole at the end with _$⟨_⟩_, so you always end up editing code outside the last hole.

It would be nice to have this functionality in the standard library and the way to do that currently is to open an issue or pull request on github. Can you do that?