happy-match-indexed.rzk

#lang rzk-1

#data nat := zero | suc (n : nat)

#data vec (A : U) : nat → U
  := nil : vec A zero
   | cons (n : nat) (x : A) (xs : vec A n) : vec A (suc n)

-- match on an indexed family: one binder per method argument
-- (fields first, then the induction hypothesis for the recursive field)
#define vlen (A : U) (n : nat) (xs : vec A n) : nat
  := match xs (nil ⇒ zero | cons k x tail ih ⇒ suc ih)

#define v1 (A : U) (x : A) : vec A (suc zero)
  := cons A zero x (nil A)

#define vlen-computes (A : U) (x : A)
  : vlen A (suc zero) (v1 A x) =_{nat} suc zero
  := refl

-- an explicit "into" motive over an indexed family takes the indices
-- before the scrutinee
#define vlen' (A : U) (n : nat) (xs : vec A n) : nat
  := match xs into (\ k v → nat) (nil ⇒ zero | cons k x tail ih ⇒ suc ih)

-- a motive that genuinely uses the index: safe head, with the motive
-- computed by a nested match on the index
#define vhead (A : U) (n : nat) (xs : vec A (suc n)) : A
  := match xs into (\ k v → match k (zero ⇒ Unit | suc j jh ⇒ A))
      ( nil ⇒ unit
      | cons k x tail ih ⇒ x)

#define v2 (A : U) (x y : A) : vec A (suc (suc zero))
  := cons A (suc zero) x (cons A zero y (nil A))

#define vhead-computes (A : U) (x y : A)
  : vhead A (suc zero) (v2 A x y) =_{A} x
  := refl