功能推理

Question

首先是一些导入和定义。

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

现在我想以一种很好的方式证明{n : ℕ} -> Even (n ^2) -> Even n，类似于 ≡-Reasoning。我已经完成了

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))

是否有针对此类目的的标准推理？

Answer 1

我不知道 Agda 标准库中的任何内容，但它几乎提供了您在 Function 模块中所需的内容。你可以不用∈Wrap。让我提出一点语法糖：

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

那么你可以把你的证明写成：

...
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)) ⟧

这种变体的主要好处是：

• 没有包装器类型。您只是在处理函数。
• 嵌套以正确的方式完成。使用问题中提出的方法，您无法在末尾使用 _$⟨_⟩_ 优化漏洞，因此您总是在最后一个漏洞之外编辑代码。

如果在标准库中有这个功能会很好，目前的方法是在github 上打开一个问题或拉取请求。你能做到吗？