Arend forces splitting on unnecessary variables

[ice1000]

\data T (n : Nat) \elim n
  | zero => To
  | n => Tn

\func ummm (n : Nat) (t : T n) : T n \elim t

Arend asks me to split on n as well. In Agda or Coq, they are translated into the so-called 'dotted pattern' which are not actually needed to be split.

data T : ℕ → Set where
  To : T 0
  Tn : ∀ n → T n

ummm : ∀ n → T n → T n
ummm a To = To
ummm a (Tn a) = Tn a

test : ∀ n → ummm n (Tn n) ≡ Tn n
test n = refl 

The above Agda code checks (note that the binding second pattern is not even linear, a was bound twice! But internally it is translated to the code below). Before Jesper's work, you need to write ummm as follows, but the computational behavior is the same.

ummm : ∀ n → T n → T n
ummm .0 To = To
ummm a (Tn .a) = Tn a

[marat-rkh]

Stumbled upon a similar issue while rewriting PLFA on Arend.

The "Transitivity" section in Relactions chapter demonstrates the following proof:

≤-trans : ∀ {m n p : ℕ} → m ≤ n → n ≤ p → m ≤ p
≤-trans z≤n _ =  z≤n
≤-trans (s≤s m≤n) (s≤s n≤p) = s≤s (≤-trans m≤n n≤p)

And the text stresses that this way of pattern matching is "immensely valuable":

The technique of induction on evidence that a property holds (e.g., inducting on evidence that m ≤ n)—rather than induction on values of which the property holds (e.g., inducting on m)—will turn out to be immensely valuable, and one that we use often.

In Arend I need to also pattern match on implicit variables:

\func <=-trans {m n p : Nat} (m<=n : m <= n) (n<=p : n <= p) : m <= p
  | {0}, _, _ => z<=n
  | {suc m}, {suc n}, {suc p}, s<=s m<=n, s<=s n<=p => s<=s (<=-trans m<=n n<=p)