기능적 추론

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을 증명하고 싶다. 끝났습니다

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없이 할 수 있습니다. 나에게 약간의 문법 설탕을 제안하자

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

이 변형의 주요 장점은 다음과 같습니다 :로

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 

그런 다음 당신이 당신의 증거를 쓸 수

• 는 래퍼 형식이 없습니다. 당신은 함수로 작업하고 있습니다.
• 중첩은 올바른 방법으로 수행됩니다. 이 질문에서 제시된 접근 방식을 사용하면 끝에 구멍을 좁힐 수는 없으므로 마지막 구멍 외부에서 코드 편집을 끝내게됩니다.

표준 라이브러리에서이 기능을 사용하는 것이 좋으며 현재 수행 할 방법은 github에서 문제를 열거 나 요청을 푸는 것입니다. 그럴 수있어?