Как я могу убедить Агду, что моя функция имеет определенную ценность? - PullRequest
Новая
       69

Как я могу убедить Агду, что моя функция имеет определенную ценность?

0 голосов
/ 01 июля 2018

Я привык писать человеческие доказательства в математике, но я совсем новичок в написании Агды. Следующее - игрушечный пример чего-то, что я не могу понять, как доказать с Agda.

Неформально я хочу написать функцию f, которая принимает натуральное число x и пару натуральных чисел. Если первый элемент в паре равен x, вернуть второй элемент в паре. В противном случае верните 0.

Вот мои определения для равенства натуральных чисел: 

data N : Set where
  zero : N
  s : N → N

data _≡_ {X : Set} : X → X → Set where
  refl : (x : X) → (x ≡ x)

data _≢_ : N → N → Set where
  <   : {n : N} → (zero ≢ (s n))
  >   : {n : N} → ((s n) ≢ zero)
  rec : {n m : N} → (n ≢ m) → ((s n) ≢ (s m))

data _=?_ (n m : N) : Set where
  true  : (n ≡ m) → (n =? m)
  false : (n ≢ m) → (n =? m)

equal? : (n m : N) → (n =? m)
equal? zero zero = true (refl zero)
equal? zero (s _) = false <
equal? (s _) zero = false >
equal? (s n) (s m) with (equal? n m)
... | (true (refl a)) = (true (refl (s a)))
... | (false p) = (false (rec p))

и вот функция. 

data Npair : Set where
  pair : (n m : N) → Npair

f : N → Npair → N
f a (pair b c) with equal? a b
... | (true (refl _)) = c
... | (false _) = zero

Я не могу доказать 

lemma : (x y : N) → (y ≡ (f x (pair x y)))

потому что когда я пытаюсь ввести в определение конструктор refl, он жалуется, что 

y != f x (pair x y) | equal? x x of type N

Что я должен изменить, чтобы доказать эту лемму?

1 Ответ

0 голосов
/ 01 июля 2018

В lemma вам нужно сопоставить шаблон с equal? x x, потому что f также совпадает с этим, и вы не можете рассуждать о выводе f, пока не сделаете такое же совпадение. Тем не менее, вы получите два случая для equal? x x: 

lemma : (x y : N) → (y ≡ (f x (pair x y)))
lemma x y with equal? x x 
... | true (refl _) = refl _
... | false _       = ?

Из этого второй случай невозможен. Чтобы исключить это, вам нужно доказать ∀ n → equal? n n ≡ true (refl _): 

equal?-true : ∀ n → equal? n n ≡ true (refl _)
equal?-true zero = refl _
equal?-true (s n) with equal? n n | equal?-true n
... | true (refl _) | q = refl _
... | false x       | ()

lemma : (x y : N) → (y ≡ (f x (pair x y)))
lemma x y with equal? x x | equal?-true x
... | true (refl _) | _ = refl _
... | false _       | ()

Однако вам не нужно выполнять дополнительную работу, если вы определяете неравенство просто как отрицание равенства, потому что тогда x ≢ x немедленно подразумевает ⊥. 

data ⊥ : Set where

⊥-elim : ⊥ → {A : Set} → A
⊥-elim ()

_≢_ = λ {A : Set}(x y : A) → x ≡ y → ⊥

data _=?_ (n m : N) : Set where
  true  : (n ≡ m) → (n =? m)
  false : (n ≢ m) → (n =? m)

equal? : ∀ n m → n =? m
equal? zero zero   = true (refl zero)
equal? zero (s m)  = false (λ ())
equal? (s n) zero  = false (λ ())
equal? (s n) (s m) with equal? n m
... | true  (refl _) = true (refl _)
... | false p        = false λ {(refl _) → p (refl n)}

data Npair : Set where
  pair : (n m : N) → Npair

f : N → Npair → N
f a (pair b c) with equal? a b
... | (true (refl _)) = c
... | (false _)       = zero

lemma : (x y : N) → (y ≡ (f x (pair x y)))
lemma x y with equal? x x
... | true (refl .x) = refl y
... | false p        = ⊥-elim (p (refl _))
...