agda - Agda 中非繁琐的 AST 转换证明

Question

我在 "simple imperative programs"软件基础一章，一路上也用 Agda 做练习。该书指出，在 AST-s 上进行证明是乏味的，并继续介绍 Coq 中的自动化工具。

如何减少 Agda 的乏味？

这是一个示例代码:

open import Data.Nat hiding (_≤?_)
open import Function
open import Data.Bool
open import Relation.Binary.PropositionalEquality
open import Data.Empty
open import Data.Product
open import Data.Unit hiding (_≤?_)

data AExp : Set where
  ANum : ℕ → AExp
  APlus AMinus AMult : AExp → AExp → AExp

aeval : AExp → ℕ
aeval (ANum x) = x
aeval (APlus a b) = aeval a + aeval b 
aeval (AMinus a b) = aeval a ∸ aeval b  
aeval (AMult a b) = aeval a * aeval b

opt-0+ : AExp → AExp
opt-0+ (ANum x) = ANum x
opt-0+ (APlus (ANum 0) b) = b
opt-0+ (APlus a b) = APlus (opt-0+ a) (opt-0+ b)
opt-0+ (AMinus a b) = AMinus (opt-0+ a) (opt-0+ b)
opt-0+ (AMult a b) = AMult (opt-0+ a) (opt-0+ b)

opt-0+-sound : ∀ e → aeval (opt-0+ e) ≡ aeval e
opt-0+-sound (ANum x) = refl
opt-0+-sound (APlus (ANum zero) b) rewrite opt-0+-sound b = refl
opt-0+-sound (APlus (ANum (suc x)) b) rewrite opt-0+-sound b = refl
opt-0+-sound (APlus (APlus a a₁) b) rewrite opt-0+-sound (APlus a a₁) | opt-0+-sound b = refl
opt-0+-sound (APlus (AMinus a a₁) b) rewrite opt-0+-sound (AMinus a a₁) | opt-0+-sound b = refl
opt-0+-sound (APlus (AMult a a₁) b) rewrite opt-0+-sound (AMult a a₁) | opt-0+-sound b = refl
opt-0+-sound (AMinus a b) rewrite opt-0+-sound a | opt-0+-sound b = refl
opt-0+-sound (AMult a b) rewrite opt-0+-sound a | opt-0+-sound b = refl

这里有一些具体问题:

首先，如果我用普通的 Haskell 编写一个未经验证的程序，我会排除术语递归或使用泛型编程。我也可以在 Agda 中编写一个通用的转换函数:

transform : (AExp → AExp) → AExp → AExp
transform f (ANum x)     = f (ANum x)
transform f (APlus a b)  = f (APlus  (transform f a) (transform f b))
transform f (AMinus a b) = f (AMinus (transform f a) (transform f b))
transform f (AMult a b)  = f (AMult  (transform f a) (transform f b))

opt-0+ : AExp → AExp
opt-0+ = transform (λ {(APlus (ANum 0) b) → b; x → x})

但随后证明变得可怕。我还尝试定义一个标准的变态，然后根据它定义评估和转换，然后尝试根据作为变态参数的函数(对应于构造函数)来证明事情，但我几乎失败了这种方法。所以，在这里我想知道是否有一种可行的“通用”方法来证明写作，它只关注相关案例而跳过其他案例。

其次，Agda 在展开函数定义时没有考虑“catch all”模式。记忆一下我的证明中的这一部分:

opt-0+-sound (APlus (ANum zero) b) rewrite opt-0+-sound b = refl
opt-0+-sound (APlus (ANum (suc x)) b) rewrite opt-0+-sound b = refl
opt-0+-sound (APlus (APlus a a₁) b) rewrite opt-0+-sound (APlus a a₁) | opt-0+-sound b = refl
opt-0+-sound (APlus (AMinus a a₁) b) rewrite opt-0+-sound (AMinus a a₁) | opt-0+-sound b = refl
opt-0+-sound (APlus (AMult a a₁) b) rewrite opt-0+-sound (AMult a a₁) | opt-0+-sound b = refl

在第一行以下的所有案例中，Agda 不记得我们已经涵盖了与 opt-0+ 唯一相关的案例。因此我们必须再次写出每个构造函数。随着构造函数数量的增加，这个问题变得更加令人讨厌。
是否有消除样板案例的技巧？

Answer 1

让我们概括一下您的 transform一点:

foldAExp : {A : Set} -> (ℕ -> A) -> (_ _ _ : A -> A -> A) -> AExp -> A
foldAExp f0 f1 f2 f3 (ANum x)     = f0 x
foldAExp f0 f1 f2 f3 (APlus a b)  = f1 (foldAExp f0 f1 f2 f3 a) (foldAExp f0 f1 f2 f3 b)
foldAExp f0 f1 f2 f3 (AMinus a b) = f2 (foldAExp f0 f1 f2 f3 a) (foldAExp f0 f1 f2 f3 b)
foldAExp f0 f1 f2 f3 (AMult a b)  = f3 (foldAExp f0 f1 f2 f3 a) (foldAExp f0 f1 f2 f3 b)

现在我们可以编写这个函数:

generalize : ∀ f0 f1 f2 f3
           -> (∀ x   -> aeval (f0 x)   ≡ aeval (ANum x))
           -> (∀ a b -> aeval (f1 a b) ≡ aeval (APlus a b))
           -> (∀ a b -> aeval (f2 a b) ≡ aeval (AMinus a b))
           -> (∀ a b -> aeval (f3 a b) ≡ aeval (AMult a b))
           -> (∀ e -> aeval (foldAExp f0 f1 f2 f3 e) ≡ aeval e)
generalize f0 f1 f2 f3 p0 p1 p2 p3 (ANum x) = p0 x
generalize f0 f1 f2 f3 p0 p1 p2 p3 (APlus a b)
  rewrite p1 (foldAExp f0 f1 f2 f3 a) (foldAExp f0 f1 f2 f3 b)
  | generalize f0 f1 f2 f3 p0 p1 p2 p3 a | generalize f0 f1 f2 f3 p0 p1 p2 p3 b = refl
generalize f0 f1 f2 f3 p0 p1 p2 p3 (AMinus a b)
  rewrite p2 (foldAExp f0 f1 f2 f3 a) (foldAExp f0 f1 f2 f3 b)
  | generalize f0 f1 f2 f3 p0 p1 p2 p3 a | generalize f0 f1 f2 f3 p0 p1 p2 p3 b = refl
generalize f0 f1 f2 f3 p0 p1 p2 p3 (AMult a b)
  rewrite p3 (foldAExp f0 f1 f2 f3 a) (foldAExp f0 f1 f2 f3 b)
  | generalize f0 f1 f2 f3 p0 p1 p2 p3 a | generalize f0 f1 f2 f3 p0 p1 p2 p3 b = refl

所以如果我们有这样的功能 f0 , f1 , f2和 f3 ，不改变任何适当子表达式的“含义”( Num _ 用于 f0， APlus _ _ 用于 f1 等等)，我们可以使用这些函数折叠任何表达式而不改变其“含义” .这是一个简单的例子:

idAExp : AExp → AExp
idAExp = foldAExp ANum APlus AMinus AMult

idAExp-sound : ∀ e → aeval (idAExp e) ≡ aeval e
idAExp-sound = generalize _ _ _ _ (λ _ → refl) (λ _ _ → refl) (λ _ _ → refl) (λ _ _ → refl)

现在我们需要可判定的平等机制来“记住”涵盖的案例。我将在下面发布整个代码的链接，因为有很多样板。这是引理，你想证明:

0+-f1 : AExp -> AExp -> AExp
0+-f1 a         b with a ≟AExp ANum 0
0+-f1 .(ANum 0) b | yes refl = b
0+-f1  a        b | no  p    = APlus a b

opt-0+ : AExp → AExp
opt-0+ = foldAExp ANum 0+-f1 AMinus AMult

0+-p1 : ∀ a b -> aeval (0+-f1 a b) ≡ aeval (APlus a b)
0+-p1  a        b with a ≟AExp ANum 0
0+-p1 .(ANum 0) b | yes refl = refl
0+-p1  a        b | no  p    = refl

opt-0+-sound : ∀ e → aeval (opt-0+ e) ≡ aeval e
opt-0+-sound = generalize _ _ _ _ (λ _ → refl) 0+-p1 (λ _ _ → refl) (λ _ _ → refl)

让我们证明更花哨的引理。

fancy-lem : ∀ a1 a2 b1 b2 -> a1 * b1 + a1 * b2 + a2 * b1 + a2 *  b2 ≡ (a1 + a2) * (b1 + b2)
fancy-lem = solve
  4
  (λ a1 a2 b1 b2 → a1 :* b1 :+ a1 :* b2 :+ a2 :* b1 :+ a2 :* b2 := (a1 :+ a2) :* (b1 :+ b2))
  refl
    where
      import Data.Nat.Properties
      open Data.Nat.Properties.SemiringSolver

现在我们要对 AExp 进行这样的优化。学期:

left : AExp -> AExp
left (ANum   x  ) = ANum x
left (APlus  a b) = a
left (AMinus a b) = a
left (AMult  a b) = a

right : AExp -> AExp
right (ANum x    ) = ANum x
right (APlus a b ) = b
right (AMinus a b) = b
right (AMult  a b) = b

fancy-f3 : AExp -> AExp -> AExp
fancy-f3 a b with left a | right a | left b | right b
fancy-f3 a b | a1 | a2 | b1 | b2 with a ≟AExp APlus a1 a2 | b ≟AExp APlus b1 b2
fancy-f3 .(APlus a1 a2) .(APlus b1 b2) | a1 | a2 | b1 | b2 | yes refl | yes refl =
  APlus (APlus (APlus (AMult a1 b1) (AMult a1 b2)) (AMult a2 b1)) (AMult a2 b2)
fancy-f3  a              b             | a1 | a2 | b1 | b2 | _        | _        = AMult a 

opt-fancy : AExp → AExp
opt-fancy = foldAExp ANum APlus AMinus fancy-f3

和健全性证明:

fancy-p3 : ∀ a b -> aeval (fancy-f3 a b) ≡ aeval (AMult a b)
fancy-p3 a b with left a | right a | left b | right b
fancy-p3 a b | a1 | a2 | b1 | b2 with a ≟AExp APlus a1 a2 | b ≟AExp APlus b1 b2
fancy-p3 .(APlus a1 a2) .(APlus b1 b2) | a1 | a2 | b1 | b2 | yes refl | yes refl =
  fancy-lem (aeval a1) (aeval a2) (aeval b1) (aeval b2)
fancy-p3 .(APlus a1 a2)  b             | a1 | a2 | b1 | b2 | yes refl | no  _    = refl
fancy-p3  a             .(APlus b1 b2) | a1 | a2 | b1 | b2 | no  _    | yes refl = refl
fancy-p3  a              b             | a1 | a2 | b1 | b2 | no  _    | no  _    = refl

opt-fancy-sound : ∀ e → aeval (opt-fancy e) ≡ aeval e
opt-fancy-sound = generalize _ _ _ _ (λ _ → refl) (λ _ _ → refl) (λ _ _ → refl) fancy-p3

这是整个代码: http://lpaste.net/106481
可以减少 generalize 中的样板数量和 ≟AExp .技巧在这里描述: http://rubrication.blogspot.ru/2012/03/decidable-equality-in-agda.html
抱歉，如果显示某些内容很愚蠢，我的浏览器就会发疯。

编辑:

没必要乱七八糟 foldAExp东西。平时 transform让事情变得更容易。以下是一些定义:

transform : (AExp → AExp) → AExp → AExp
transform f (ANum x)     = f (ANum x)
transform f (APlus a b)  = f (APlus  (transform f a) (transform f b))
transform f (AMinus a b) = f (AMinus (transform f a) (transform f b))
transform f (AMult a b)  = f (AMult  (transform f a) (transform f b))

generalize : ∀ f -> (∀ e -> aeval (f e) ≡ aeval e)
           -> (∀ e -> aeval (transform f e) ≡ aeval e)
generalize f p (ANum x)    = p (ANum x)
generalize f p (APlus a b)  rewrite p (APlus  (transform f a) (transform f b))
  | generalize f p a | generalize f p b = refl
generalize f p (AMinus a b) rewrite p (AMinus (transform f a) (transform f b))
  | generalize f p a | generalize f p b = refl
generalize f p (AMult a b)  rewrite p (AMult  (transform f a) (transform f b))
  | generalize f p a | generalize f p b = refl

idAExp : AExp → AExp
idAExp = transform id

idAExp-sound : ∀ e → aeval (idAExp e) ≡ aeval e
idAExp-sound = generalize _ (λ _ → refl)

以及整个代码: http://lpaste.net/106500