[Agda] merging identical proofs?

[Twan van Laarhoven]

In this case I would just write the proof with `cong₂` as

     correct : (t : Term) → interp t ≡ interp (f t)
     correct (Int n) = refl
     correct (Add (Int zero) t₁) = correct t₁
     correct (Add (Int (suc x)) t₁) = cong₂ _+_ (correct (Int (suc x)))
                                                (correct t₁)
     correct (Add (Add t t₁) t₂) = cong₂ _+_ (correct (Add t t₁)) (correct t₂)

Note that you shouldn't use `with` to match on the argument `t`, because then 
the termination checker can not see that the argument passed to the recursive 
call is smaller.

If you want to only write these identical cases once, then there should also be 
just a single corresponding case in `f`. You can do this with a separate view:

     zero-view : (t : Term) → Maybe (t ≡ Int 0)
     zero-view (Int zero) = just refl
     zero-view (Int (suc x)) = nothing
     zero-view (Add t t₁) = nothing

     f' : Term → Term
     f' (Int n) = Int n
     f' (Add t t₁) with zero-view t
     f' (Add .(Int 0) t₁) | just refl = f' t₁
     f' (Add t t₁)        | nothing   = Add (f' t) (f' t₁)

     correct' : (t : Term) → interp t ≡ interp (f' t)
     correct' (Int n) = refl
     correct' (Add t t₁) with zero-view t
     correct' (Add .(Int 0) t₁) | just refl = correct' t₁
     correct' (Add t t₁) | nothing = cong₂ _+_ (correct' t) (correct' t₁)


Twan

On 14/02/14 11:32, Kenichi Asai wrote:
> I have a simple transformation that replaces all the occurrences of
> 0 + x in a formula with x and want to prove it correct.  The formula
> is simply defined by:
>
> data Term : Set where
>    Int : N -> Term
>    Add : Term -> Term -> Term
>
> and the transformation is:
>
> f : Term -> Term
> f (Int n) = Int n
> f (Add (Int 0) t1) = f t1
> f (Add t t1) = Add (f t) (f t1)
>
> When I want to prove it correct under the semantics of the formula:
>
> interp : Term -> N
> interp (Int n) = n
> interp (Add t t1) = interp t + interp t1
>
> the skeleton of the proof becomes:
>
> correct : (t : Term) -> interp t == interp (f t)
> correct (Int n) = refl
> correct (Add t t1) with t
> ... | Int 0 = correct t1	-- interesting case
> ... | Int (suc n) = ?		-- uninteresting case
> ... | Add t2 t3 = ?		-- uninteresting case
>
> where the proofs for the last two uninteresting cases are identical
> except whether t is instantiated to Int (suc n) or App t2 t3.  My
> question is: can I prove this lemma without writing the proof for
> the uninteresting cases twice?
>
> The agda file is attached.  Thank you in advance!
>
> Sincerely,
>
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>