agda

Non-tedious AST transformation proofs in Agda

I'm at the "simple imperative programs" chapter in Software Foundations, doing exercises with Agda too along the way. The book notes that doing proofs on AST-s is tedious and proceeds to present automation tools in Coq.

How can I reduce the tedium in Agda?

Here's an example code:

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

Some specific problems here:

First, were I to write a non-verified program in plain Haskell, I would factor out term recursion or use generic programming. I can write a generic transform function in Agda too:

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

But then the proofs become horrible. I also tried to define a standard catamorphism, and then define both evaluation and transformation in terms of that, and then tried to prove things in terms of the functions (corresponding to constructors) that are arguments to the catamorphism, but I pretty much failed with that approach. So, here I'd like to know if there is a feasible "generic" approach to proof writing, which focuses only on the relevant cases and skips over others.

Second, Agda doesn't take into account "catch all" patterns when unfolding function definitions. Recall this part from my proof:

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

In all the cases below the first line, Agda doesn't remember that we've already covered the only relevant case to opt-0+ and thus we have to write out every constructor again. This issue grows markedly more irksome as the number of constructors increases. Is there a trick to eliminate the boilerplate cases?

Solution

  • Let's generalize your transform a little:

    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)

    Now we can write this function:

    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

    So if we have such functions f0, f1, f2 and f3, that don't change the "meaning" of any appropriate subexpression (Num _ for f0, APlus _ _ for f1 and so on), than we can fold any expression with these functions without changing its "meaning". Here is a trivial example:

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

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

    Now we need decidable equality machinery for "remembering" covered cases. I'll post a link to the whole code below, since there is a lot of boilerplate. And here is the lemma, you want to prove:

    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)

    Let's prove more fancy lemma.

    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

    Now we want to make such optimization on an AExp term:

    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

    And the soundness proof:

    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

    Here is the whole code: http://lpaste.net/106481 It's possible to reduce amount of boilerplate in generalize and ≟AExp. The trick is described here: http://rubrication.blogspot.ru/2012/03/decidable-equality-in-agda.html Sorry, if something is shown silly, my browser became crazy.

    EDIT:

    There was no need in messy foldAExp stuff. Usual transform makes things much easier. Here are some definitions:

    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)

    And the whole code: http://lpaste.net/106500