[Agda] Re: merging identical proofs?

[Andreas Abel]

Kenichi Asai-san,

You need an indexed data type for this view.

data IdView {Γ} : ∀ τ (t : Term Γ τ) → Set where
   isId    : ∀{τ}   → IdView (TFun τ τ) (Lam (Var hd))
   isOther : ∀{τ t} → IdView τ t

idView : ∀ {τ Γ} (t : Term Γ τ) → IdView τ t
idView (Lam (Var hd)) = isId
idView _              = isOther

-- transformation: (λx.x) M -> M
f : ∀ {τ Γ} → Term Γ τ → Term Γ τ
f (Var x) = Var x
f (Lam t) = Lam (f t)
f (App t t₁) with idView t
f (App .(Lam (Var hd)) t₁) | isId    = f t₁
f (App t               t₁) | isOther = App (f t) (f t₁)

Best regards,
Andreas

On 15.02.2014 04:18, Kenichi Asai wrote:
>> 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 t1) = nothing
>
> Thank you.  This is great.  Now, I gradually understand what the view
> is.  Let me ask one more question.  How can I define the view for a
> dependent case?  Concretely, suppose I want to replace all the
> occurrences of (\x.x) M in a term with M, where a term is defined
> typefully as usual:
>
> data Term (G : Ctx) : Type -> Set where
>    Var : forall {t} -> t in G -> Term G t
>    Lam : forall {t t'} -> Term (t :: G) t' -> Term G (TFun t t')
>    App : forall {t t'} -> Term G (TFun t t')  -> Term G t -> Term G t'
>
> When I define the translation:
>
> f : forall {t G} -> Term G t -> Term G t
> f (Var x) = Var x
> f (Lam t) = Lam (f t)
> f (App (Lam (Var hd)) t1) = f t1
> f (App t t1) = App (f t) (f t1)
>
> and want to change the last two cases using a view, I need to define a
> view something like:
>
> id-view : forall {t G} -> (T : Term G t) -> Maybe (T == Lam (Var hd))
>
> But it does not work, because the types of T and Lam (Var hd) do not
> agree.  What I want to define here would be:
>
> Given a term T for arbitrary G and t, if t has the form "TFun t' t'"
> for some t' and T == Lam (Var hd), then return just refl, otherwise
> nothing.
>
> Would this be possible?  Or should I do something else?
>
> Sincerely,
>
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>


-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Depeartment of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www2.tcs.ifi.lmu.de/~abel/