2014-03-27 77 views
1

一些導入和定義第一。功能推理

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

是否有任何標準推理用於這種目的?

回答

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上打開問題或請求請求,那就太好了。你能做到嗎?

+0

我沒有github帳戶。如果沒有人在三天內解決問題,我會打開它。 爲什麼不是 ____::{αβ} {A:集合α}→(a:A)→{B:A→集合β}→((x:A)→B x)→B a a⟦f⟧= fa – user3237465

+1

由於支撐,您無法合併這些功能。讓我給一個小例子添加明確的大括號:'x⟦(t1 - f1⟶(t2⟧))''。這是因爲使用了「infixr」而不是「infixl」,這使得使用孔更容易。 'PreorderReasoning'具有相同的'infixr'。 –

+1

https://github.com/agda/agda-stdlib/issues/15 –