我怎样才能让 Agda 相信我的函数具有一定的价值?
How can I convince Agda that my function has a certain value?
我习惯于在数学中编写人类证明,但我对编写 Agda 非常陌生。以下是我不知道如何用 Agda 证明的东西的玩具示例。
非正式地,我想编写一个函数 f,它接受一个自然数 x 和一对自然数。如果对中的第一个元素等于 x,则 return 对中的第二个元素。否则,return 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
为了证明这个引理,我必须改变什么?
在 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 _))
我习惯于在数学中编写人类证明,但我对编写 Agda 非常陌生。以下是我不知道如何用 Agda 证明的东西的玩具示例。
非正式地,我想编写一个函数 f,它接受一个自然数 x 和一对自然数。如果对中的第一个元素等于 x,则 return 对中的第二个元素。否则,return 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
为了证明这个引理,我必须改变什么?
在 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 _))