[Agda] Termination checking

[Andreas Abel]

The subterm checker of the termination checker is probably not working.

It works if you use an explicit equality constraint in constructor ⟦_⟫_⟧.

     ⟦_⟫_⟧ : ∀ {d d₁ d₂ ol l nl} {eq : d ≡ d₁ + d₂} → Subst d₁ ol l -> 
Subst d₂ l nl -> Subst (suc d) ol nl

lookup .(suc d) v       (⟦_⟫_⟧ {d} {eq = eq} ρ σ) = lookup d v (_⟫_ {eq 
= eq} ρ σ)


Full code attached.


On 08.11.2014 14:10, Francesco Mazzoli wrote:
> mutual
>    data Tm (l : ℕ) : Set where
>      var   : Fin l -> Tm l
>      _·_   : Tm l -> Tm l -> Tm l
>      lam   : Tm (suc l) -> Tm l
>      ⟦_,_⟧ : ∀ {d ol} -> Tm ol -> Subst d ol l -> Tm l
>
>    data Subst : (d : ℕ)(ol : ℕ)(nl : ℕ) -> Set where
>      id    : ∀ {ol} -> Subst 0 ol ol
>      _∷_   : ∀ {d ol nl} -> Tm nl -> Subst d ol nl -> Subst d (suc ol) nl
>      ⟦_⟫_⟧ : ∀ {d₁ d₂ ol l nl} -> Subst d₁ ol l -> Subst d₂ l nl ->
> Subst (suc (d₁ + d₂)) ol nl
>
> _⟫_ : ∀ {d₁ d₂ ol l nl} -> Subst d₁ ol l -> Subst d₂ l nl -> Subst (d₁
> + d₂) ol nl
> id ⟫ σ = σ
> (t ∷ ρ) ⟫ σ = ⟦ t , σ ⟧ ∷ (ρ ⟫ σ)
> _⟫_ .{suc (d₁ + d₂)} {d₃} {ol} {_} {nl} (⟦_⟫_⟧ {d₁} {d₂} ρ σ) γ =
>    subst (λ d → Subst d ol nl) (lm d₁ d₂ d₃) (ρ ⟫ ⟦ σ ⟫ γ ⟧)
>    where
>      lm : ∀ n m k -> n + suc (m + k) ≡ suc (n + m + k)
>      lm zero m k = refl
>      lm (suc n) m k = cong suc (lm n m k)
>
> lookup : ∀ {ol nl} d -> Fin ol -> Subst d ol nl -> Tm nl
> lookup .0               v       id                    = var v
> lookup d                zero    (t ∷ ρ)               = t
> lookup d                (suc v) (t ∷ ρ)               = lookup d v ρ
> lookup .(suc (d₁ + d₂)) v       (⟦_⟫_⟧ {d₁} {d₂} ρ σ) = lookup (d₁ +
> d₂) v (ρ ⟫ σ)



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

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

andreas.abel at gu.se
http://www2.tcs.ifi.lmu.de/~abel/
-------------- next part --------------
open import Data.Nat
open import Data.Nat.Properties.Simple using (+-suc)
open import Data.Fin using (Fin; zero; suc)
open import Relation.Binary.PropositionalEquality

mutual
  data Tm (l : ℕ) : Set where
    var   : Fin l -> Tm l
    _·_   : Tm l -> Tm l -> Tm l
    lam   : Tm (suc l) -> Tm l
    _⟦_⟧ : ∀ {d ol} -> Tm ol -> Subst d ol l -> Tm l

  data Subst : (d : ℕ)(ol : ℕ)(nl : ℕ) -> Set where
    id    : ∀ {ol} -> Subst 0 ol ol
    _∷_   : ∀ {d ol nl} -> Tm nl -> Subst d ol nl -> Subst d (suc ol) nl
    ⟦_⟫_⟧ : ∀ {d d₁ d₂ ol l nl} {eq : d ≡ d₁ + d₂} → Subst d₁ ol l -> Subst d₂ l nl -> Subst (suc d) ol nl

_⟫_ : ∀ {d d₁ d₂ ol l nl}{eq : d ≡ d₁ + d₂} -> Subst d₁ ol l -> Subst d₂ l nl -> Subst d ol nl
_⟫_ {eq = refl} id                                σ = σ
_⟫_ {eq = eq  } (t ∷ ρ)                           σ = (t ⟦ σ ⟧) ∷ (_⟫_ {eq = eq} ρ σ)
_⟫_ {eq = refl} (⟦_⟫_⟧ {d₁ = d₁} {eq = refl} γ ρ) σ = _⟫_ {eq = lm d₁} γ (⟦_⟫_⟧ {eq = refl} ρ σ)
  where
    lm : ∀ n {m k} -> suc (n + m + k) ≡ n + suc (m + k)
    lm zero    = refl
    lm (suc n) = cong suc (lm n)

lookup : ∀ {ol nl} d -> Fin ol -> Subst d ol nl -> Tm nl
lookup .0       v       id                       = var v
lookup d        zero    (t ∷ ρ)                  = t
lookup d        (suc v) (t ∷ ρ)                  = lookup d v ρ
lookup .(suc d) v       (⟦_⟫_⟧ {d} {eq = eq} ρ σ) = lookup d v (_⟫_ {eq = eq} ρ σ)