scoped_belongsto.agda

scoped_belongsto.agda

-- scope sensitive belongs
-- Unlike ∈, it does not allow scope insensitive proof of belongs
_∈s_ : (Name × Pointer) → Env → Set
(n , p) ∈s [] = ⊥
(n , p) ∈s ((n' , p') ∷ ρ') with n ==n n' | p ==n p'
... | false | _     = ( n , p ) ∈s ρ'
... | _     | false = ⊥
... | true  | true  = ⊤

private
  env : Env
  env = (y , 5) ∷ (x , 1) ∷ (z , 0) ∷(x , 0 ) ∷ []
  
  p₁ : (x , 1) ∈s env
  p₁ = tt

  -- this cannot be proved (◕‿◕)
  -- p₂ :  (x , 0) ∈s env
  -- p₂ = {!!}
  
-- IS IMPOSSIBLE?!
x↦n∈ρ : {x n : Nat} {ρ : Env} → (x , n) ∈s ((x ,  n ) ∷ ρ)
x↦n∈ρ {zero} {zero} = tt
x↦n∈ρ {suc x₁} {zero} = {!!}
x↦n∈ρ {zero} {suc n₁} = {!!}
x↦n∈ρ {suc x₁} {suc n₁} = {!!} -- x↦n∈ρ {x₁} {n₁}