Incorrect evidence of AST transformation in Agda

Question

I am in “simple imperative programs” in the “Software Basics” section, doing exercises with Agda too along the way. The book notes that conducting evidence on AST-s is tedious and goes on to provide automation tools in Coq.

How can I reduce boredom in Agda?

Here is a sample 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 issues here:

First, you had to write an unverified program in plain Haskell, I would drop the term recursion or use universal programming. I can also write a general conversion function in 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 " " . :

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 , - , .

EDIT:

messy 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

Answer 2

no, , :

data Dec' {p} (P : Set p) : Set p where
  yes : (p : P) → Dec' P
  no  : Dec' P

n * (n - 1) no n yes. , .

. :

vecApply : {α γ : Level} {X : Set α} {Z : Set γ} -> (n : ℕ) -> nary n X Z -> Vec X n -> Z
vecApply  0      x  _       = x
vecApply (suc n) f (x ∷ xs) = vecApply n (f x) xs

replace' : (n : ℕ) -> nary n AExp (AExp × AExp) -> AExp -> AExp
replace' n f e with getSubterms n f e
replace' n f e | nothing = e
replace' n f e | just xs with vecApply n f xs
replace' n f e | just xs |  e' , e'' with e ≟AExp e'
replace' n f e | just xs | .e  , e'' | yes refl = e''
replace' n f e | just xs |  e' , e'' | no       = e

, , n . :

_==_ : {α β : Level} {A : Set α} {B : Set β} -> A -> B -> A × B
_==_ = _,_

0+-func : AExp -> AExp × AExp
0+-func = λ a2 -> APlus (ANum 0) a2 == a2

- , , - . , .

ex1-func : (_ _ : AExp) -> AExp × AExp
ex1-func = λ a1 b1 -> AMult (APlus a1 b1) (APlus a1 b1) == ANum 0

ex1-func

let    a1 = ANum 0
in let b1 = ANum 1
in AMult (APlus a1 b1) (APlus a1 b1)

ANum 0 ∷ ANum 1 ∷ [] . "" (a1 b1 ). ( "" a1, ex1-func ( ) a1 ).

:

enlarge : AExp -> AExp
enlarge a = APlus a a

size : AExp -> ℕ
size (APlus a _) = 1 + size a
size  _          = 0

small big : AExp
small = ANum 0
big   = enlarge small

transT : Set
transT = AExp -> AExp

transTs : Set
transTs = L.List transT

left : transT
left (ANum   x  ) = ANum x
left (APlus  a b) = a
left (AMinus a b) = a
left (AMult  a b) = a

right : transT
right (ANum   x  ) = ANum x
right (APlus  a b) = b
right (AMinus a b) = b
right (AMult  a b) = b

directions : AExp -> AExp -> transTs
directions (ANum   _)     (ANum   _)     = L.[]
directions (APlus  a1 a2) (APlus  b1 b2) =
  L.map (λ f -> f ∘ left) (directions a1 b1) L.++ L.map (λ f -> f ∘ right) (directions a2 b2)
directions (AMinus a1 a2) (AMinus b1 b2) =
  L.map (λ f -> f ∘ left) (directions a1 b1) L.++ L.map (λ f -> f ∘ right) (directions a2 b2)
directions (AMult  a1 a2) (AMult  b1 b2) =
  L.map (λ f -> f ∘ left) (directions a1 b1) L.++ L.map (λ f -> f ∘ right) (directions a2 b2)
directions  _              _             = id L.∷ L.[]

add : {l : ℕ} -> ℕ -> transT -> Vec transTs l -> Vec transTs l  
add  _      d  []      = []
add  0      d (x ∷ xs) = (d L.∷ x) ∷ xs
add (suc n) d (x ∷ xs) = x ∷ add n d xs

naryApply : {α γ : Level} {X : Set α} {Z : Set γ} -> (n : ℕ) -> nary n X Z -> X -> Z
naryApply  0      x _ = x
naryApply (suc n) f x = naryApply n (f x) x

naryApplyWith : {α γ : Level} {X : Set α} {Z : Set γ}
              -> (n : ℕ) -> nary n X Z -> (X -> X) -> X -> Z
naryApplyWith  0      x _ _ = x
naryApplyWith (suc n) f g x = naryApplyWith n (f x) g (g x)

directionses : (n : ℕ) -> nary n AExp (AExp × AExp) -> Vec transTs n
directionses n f = L.foldr (λ f -> add (size (f e)) f) (replicate L.[]) $
  directions (proj₁ $ naryApply n f big) (proj₁ $ naryApply n f small) where
    e = proj₁ $ naryApplyWith n f enlarge small

open RawMonad {{...}}

getSubterms : (n : ℕ) -> nary n AExp (AExp × AExp) -> AExp -> Maybe (Vec AExp n)
getSubterms n f e = (λ _ -> map (λ fs -> lhead id fs e) dss) <$> flip (mapM M.monad) dss
  (L.sequence M.monad ∘ neighbWith (λ f g -> dec'ToMaybe⊤ $ f e ≟AExp g e)) where
    dss = directionses n f

, , . "" left ∘ right ∘ right ( , , ). . , , , ( size). , , . , (, ) " " .

replace' . , . , , .

:

replace : (n : ℕ) -> nary n AExp (AExp × AExp) -> AExp -> AExp 
replace n f = transform (replace' n f)

. .

sound' : ∀ n f
       -> soundnessProof n f
       -> ∀ e -> aeval (replace' n f e) ≡ aeval e
sound' n f p e with getSubterms n f e
sound' n f p e | nothing = refl
sound' n f p e | just xs with vecApply n f xs | vecApplyProof p xs
sound' n f p e | just xs |  e' , e'' | p' with e ≟AExp e'
sound' n f p e | just xs | .e  , e'' | p' | yes refl = p'
sound' n f p e | just xs |  e' , e'' | p' | no       = refl

- sound' .

soundnessProof : (n : ℕ) -> nary n AExp (AExp × AExp) -> Set 
soundnessProof  0      (e' , e'') = aeval e'' ≡ aeval e'
soundnessProof (suc n)     f      = ∀ x -> soundnessProof n (f x)

, f "". :

_==_ : {α β : Level} {A : Set α} {B : Set β} -> A -> B -> A × B
_==_ = _,_

0+-func : AExp -> AExp × AExp
0+-func = λ a2 -> APlus (ANum 0) a2 == a2

vecApplyProof , :

vecApplyProof : {n : ℕ} {f : nary n AExp (AExp × AExp)}
               -> soundnessProof n f -> (xs : Vec AExp n)
               -> uncurry (λ p1 p2 -> aeval p2 ≡ aeval p1) $ vecApply n f xs
vecApplyProof {0}     p  _       = p
vecApplyProof {suc n} p (x ∷ xs) = vecApplyProof {n} (p x) xs

:

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

sound : (n : ℕ) -> (f : nary n AExp (AExp × AExp))
      -> soundnessProof n f
      -> (∀ e -> aeval (replace n f e) ≡ aeval e)
sound n f p = generalize _ (sound' n f p)

:

fancy-func : (_ _ _ _ : AExp) -> AExp × AExp
fancy-func = λ a1 a2 b1 b2 -> AMult (APlus a1 a2) (APlus b1 b2) ==
  APlus (APlus (APlus (AMult a1 b1) (AMult a1 b2)) (AMult a2 b1)) (AMult a2 b2)

opt-fancy : AExp → AExp
opt-fancy = replace 4 fancy-func

test-opt-fancy :
  let    a1 = ANum 0
  in let a2 = AMinus a1 a1
  in let b1 = ANum 1
  in let b2 = AMinus b1 b1
  in opt-fancy (AMinus (AMult (APlus a1 a2) (APlus b1 b2)) (ANum 0)) ≡
    (AMinus (APlus (APlus (APlus (AMult a1 b1) (AMult a1 b2)) (AMult a2 b1)) (AMult a2 b2)) (ANum 0)) 
test-opt-fancy = 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

opt-fancy-sound : ∀ e → aeval (opt-fancy e) ≡ aeval e
opt-fancy-sound = sound 4 fancy-func
  (λ a1 a2 b1 b2 -> fancy-lem (aeval a1) (aeval a2) (aeval b1) (aeval b2))

: http://lpaste.net/106670

EDIT: directions (_∘_ left λ f -> f ∘ left). .