Idempotent substitutions in Agda

gistfile1.agda

module Preliminaries where

-- levels

postulate Level : Set
postulate LZero : Level
postulate LSuc  : Level -> Level
postulate LMax  : Level -> Level -> Level

{-# BUILTIN LEVEL     Level #-}
{-# BUILTIN LEVELZERO LZero  #-}
{-# BUILTIN LEVELSUC  LSuc   #-}
{-# BUILTIN LEVELMAX  LMax #-}

id : forall {a}{A : Set a} -> A -> A
id x = x

-- natural numbers

data Nat : Set where
  zero : Nat
  suc  : Nat -> Nat

{-# BUILTIN NATURAL Nat #-}
{-# BUILTIN ZERO zero #-}
{-# BUILTIN SUC suc #-}

-- propositional equality

data _==_ {l}{A : Set l} (x : A) : A -> Set l where
  refl : x == x

{-# BUILTIN EQUALITY _==_ #-}
{-# BUILTIN REFL refl #-}  

-- utilities about equality

cong : forall {a b}{A : Set a}{B : Set b}(f : A -> B){x y}-> x == y -> f x == f y
cong f refl = refl

cong2 : forall {a b c}{A : Set a}{B : Set b}{C : Set c}
               (f : A -> B -> C){x y u v} -> x == y -> u == v -> f x u == f y v
cong2 f refl refl = refl

sym : forall {a}{A : Set a}{x y : A} -> x == y -> y == x
sym refl = refl

-- unit type, hidden arguments and steroids.

data Unit : Set where
  unit : Unit

Hidden : forall {a} -> Set a -> Set a
Hidden A = Unit -> A

hide : forall {a b}{A : Set a}{B : A -> Set b} -> ((x : A) -> B x) -> ((x : A) -> Hidden (B x))
hide f x unit = f x

reveal : forall {a}{A : Set a} -> Hidden A -> A
reveal f = f unit

data Reveal_is_ {a} {A : Set a} (x : Hidden A) (y : A) : Set a where
  [_] : (eq : reveal x == y) -> Reveal x is y

inspect : forall {a b} {A : Set a} {B : A -> Set b}
          (f : (x : A) -> B x) (x : A) -> Reveal (hide f x) is (f x)
inspect f x = [ refl ]

-- Lists

data List {l}(A : Set l) : Set l where
  []   : List A
  _::_ : A -> List A -> List A

infixl 4 _::_

-- List membership

infixl 4 _<-_

data _<-_ {l}{A : Set l} : A -> List A -> Set l where
  here  : forall {x xs}   -> x <- (x :: xs)
  there : forall {x y ys} -> x <- ys -> x <- (y :: ys)


-------------------------------------------------------------------------------------------------------

module MySubst where

open import Preliminaries

-- type definition

Vars : Set 
Vars = List Nat

data Ty (C : Vars) : Set where
  var : forall {x}         -> x <- C -> Ty C
  app : forall (l r : Ty C) -> Ty C
  con : Nat -> Ty C


_-_ : forall {x} -> (C : Vars) -> (v : x <- C) -> Vars
[] - () 
(x :: c) - here = c
(x :: c) - (there p) = x :: (c - p)

weak : forall {x x' C} -> (p : x <- C) -> (p' : x' <- (C - p)) -> x' <- C
weak here p' = there p'
weak (there p) here = here
weak (there p) (there p') = there (weak p p')

infix 4 _<-==_

data _<-==_ {C} : forall {t t'} -> t <- C -> t' <- C -> Set where
  same : forall {t} (x : t <- C) -> x <-== x
  diff : forall {t t'} (x : t <- C ) (v : t' <- (C - x)) -> x <-== (weak x v) 

varDiff : forall {t t' C} -> (x : t <- C) (v : t' <- C) -> x <-== v
varDiff here here = same here
varDiff here (there v) = diff here v
varDiff (there x) here = diff (there x) here
varDiff (there x) (there v) with varDiff x v 
varDiff (there .v) (there v) | same .v = same (there v)
varDiff (there x) (there .(weak x v)) | diff .x v = diff (there x) (there v)

replace : forall {x C} -> (p : x <- C) -> (t : Ty (C - p)) -> Ty C -> Ty (C - p)
replace p t (var x) with varDiff p x 
replace .x₁ t (var x₁)        | same .x₁ = t
replace p t (var .(weak p v)) | diff .p v = var v
replace p t (app t' t'') = app (replace p t t') (replace p t t'')
replace p t (con x) = con x

weakTy : forall {x C} -> (p : x <- C) -> (t : Ty (C - p)) -> Ty C
weakTy p (var v) = var (weak p v)
weakTy p (app t t') = app (weakTy p t) (weakTy p t')
weakTy p (con c) = con c

replaceWeakTy : forall {x C} -> (v : x <- C) -> (t : Ty (C - v)) -> t == replace v t (weakTy v t)
replaceWeakTy v t with weakTy v t | inspect (weakTy v) t 
replaceWeakTy v (var x₂) | var x₄ | [ eq ] with varDiff v x₄ 
replaceWeakTy .x₄ (var x₂) | var x₄ | [ eq ] | same .x₄ = refl
replaceWeakTy v (var x₃) | var .(weak v v₁) | [ eq ] | diff .v v₁ = {!!}
replaceWeakTy v (app t t₁) | var x₂ | [ () ]
replaceWeakTy v (con x₁) | var x₃ | [ () ] 
replaceWeakTy v (var x₂) | app t' t'' | [ () ] 
replaceWeakTy v (app t t₁) | app t' t'' | [ eq ] with replaceWeakTy v t | replaceWeakTy v t₁ 
...| r | r' = cong2 app {!!} {!!}
replaceWeakTy v (con x₁) | app t' t'' | [ () ] 
replaceWeakTy v (var x₂) | con x₃ | [ () ] 
replaceWeakTy v (app t t₁) | con x₁ | [ () ] 
replaceWeakTy v (con x₁) | con x₂ | [ eq ] = cong (\ t -> replace v (con x₁) t) eq

replaceWeakVar : forall {x y C} -> (p : x <- C)(v : y <- C - p)(t : Ty (C - p)) -> var v == replace p t (var (weak p v)) 
replaceWeakVar p v t = {!!}

replace-idem : forall {x C} -> (v : x <- C) -> (t : Ty (C - v)) -> (t' : Ty C) -> replace v t t' == replace v t (weakTy v (replace v t t'))
replace-idem p t (var v) with varDiff p v 
replace-idem .v t (var v)          | same .v = replaceWeakTy v t
replace-idem p t (var .(weak p v)) | diff .p v = replaceWeakVar p v t
replace-idem p t (app t' t'') = cong2 app (replace-idem p t t') (replace-idem p t t'')
replace-idem p t (con c) = refl