[Agda] Re: merging identical proofs?

[Kenichi Asai]

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

-- 
Kenichi Asai
-------------- next part --------------
module stlc where

open import Data.Nat
open import Data.List
open import Relation.Binary.PropositionalEquality
open ??Reasoning

-- functional extensionality
postulate
  extensionality : forall {A B : Set} {f g : A -> B} -> (??(a : A) -> f a ??g a) -> f ??g

-- list membership
infix 4 _??
data _?? {A : Set} (x : A) : List A ??Set where
  hd : ??{xs} ??x ??x ??xs
  tl : ??{y xs} ??x ??xs ??x ??y ??xs

-- Types
data Type : Set where
  TInt : Type
  TFun : Type ??Type ??Type

-- Contexts
Ctx : Set
Ctx = List Type

-- Terms
data Term (? : Ctx) : Type ??Set where
  Var : ??{?} ??? ??? ??Term ? ?
  Lam : ??{? ?'} ??Term (? ???) ?' ??Term ? (TFun ? ?')
  App : ??{? ?'} ??Term ? (TFun ? ?')  ??Term ? ? ??Term ? ?'

-- ?x.x
term1 : Term [] (TFun TInt TInt)
term1 = Lam (Var hd)

-- (?x.x)(?x.x)
term2 : Term [] (TFun TInt TInt)
term2 = App (Lam (Var hd)) (Lam (Var hd))

-- Interpretation of types
typeDenote : Type ??Set
typeDenote TInt = ??typeDenote (TFun ?????? = typeDenote ?????typeDenote ???
-- Environments
data Env : Ctx ??Set where 
  [] : Env []
  _?? : ??{? ?} ??typeDenote ? ??Env ? ??Env (? ???)

lookup : ??{ ? ? } ??? ??? ??Env ? ??typeDenote ?
lookup hd (x ??env) = x
lookup (tl v) (x ??env) = lookup v env

-- Interpreter
expDenote : ??{? ?} ??Term ? ? ??Env ? ??typeDenote ?
expDenote (Var x) env = lookup x env
expDenote (Lam e) env = ? x ??expDenote e (x ??env)
expDenote (App e f) env = expDenote e env (expDenote f env)

-- transformation: (?x.x) M -> M
f : ??{? ?} ??Term ? ? ??Term ? ?
f (Var x) = Var x
f (Lam t) = Lam (f t)
f (App (Lam (Var hd)) t?? = f t??f (App t t?? = App (f t) (f t??

-- f ((?x.x)(?x.x)) = ?x.x
ex1 : f term2 ??term1
ex1 = refl

-- id-view
-- id-view : ??{? ?} ??(t : Term ? ?) ??Maybe (t ??Lam (Var hd))
-- id-view t = ?

-- Correctness
correct : ??{? ?} ??(t : Term ? ?) ??(env : Env ?) ??expDenote t env ??expDenote (f t) env
correct (Var x) env = refl
correct (Lam t) env = extensionality (? x ??correct t (x ??env))
correct (App t t?? env = {!!}