<div dir="ltr">Hi, I'm trying to do an exercise from "Dependent Types at Work". The exercise is from section 4.4 and asks to prove eq-succ and eq-mult-rec. My problem is I don't understand some of the typing issues.<div>
<br></div><div>Here's what I have so far:</div><div><br></div><div>>>></div><div><div>module exercises where</div><div><br></div><div>--</div><div><br></div><div>data Nat : Set where</div><div> zero : Nat</div>
<div> succ : Nat -> Nat</div><div><br></div><div>_+_ : Nat -> Nat -> Nat</div><div>zero + m = m</div><div>succ n + m = succ (n + m)</div><div><br></div><div>natrec : {C : Nat -> Set} -> (C zero) -></div>
<div> ((m : Nat) -> C m -> C (succ m)) -> (n : Nat) -> C n</div><div>natrec p h zero = p</div>
<div>natrec p h (succ n) = h n (natrec p h n)</div><div><br></div><div>plus : Nat -> Nat -> Nat</div><div>plus n m = natrec m (λ x y -> succ y) n</div><div><br></div><div>--<br></div><div><br></div><div>data _==_ {A : Set} : A -> A -> Set where</div>
<div> refl : (a : A) -> a == a</div><div><br></div><div>subst : {A : Set} -> {C : A -> Set} -> {a' a'' : A} -></div><div> a' == a'' -> C a' -> C a''</div><div>
subst (refl a) c = c</div><div><br></div><div>--</div><div><br></div><div>eq-succ : {n m : Nat} -> n == m -> succ n == succ m</div><div>eq-succ (refl m) = refl (succ m)</div><div><br></div><div>eq-plus-rec : (n m : Nat) -> (n + m) == (plus n m)</div>
<div>eq-plus-rec n m = natrec (refl m) (λ j ih -> {! !}) n</div></div><div><br></div><div><<<</div><div><br></div><div>When I replace the hole with 'eq-succ ih', like it is in the pdf, agda gives an error:</div>
<div><br></div><div>>>></div><div>Refuse to construct infinite term by instantiating _47 to succ</div><div>(_n_47 n m k)</div><div>when checking that the expression eq-succ ih has type</div><div>_n_47 n m (succ k) == _m_48 n m (succ k)</div>
<div><<<</div><div><br></div><div>Sticking a hole in there to try and typing 'c-c c-,' to try and understand what's happening agda tells me:</div><div><br></div><div>>>></div><div>ih : _C_41 n m k'</div>
<div>k' : Nat</div><div>m : Nat</div><div>n : Nat</div><div><<<</div><div><br></div><div>Typing 'c-c c-l' to see what _C_41 is tells me that it has type 'Nat -> Set'. So is ih a parameterized type? Or is it just a list of types?</div>
<div><br></div><div>If I put 'eq-succ ih' in the hole and type 'c-c c-.' agda tells me</div><div><br></div><div>>>></div><div>Goal: _n_50 n m (succ k') == _m_51 n m (succ k')</div><div>Have: succ (_n_50 n m k') == succ (_m_51 n m k')</div>
<div>----</div><div>ih : _n_50 n m k' == _m_51 n m k'</div><div>...</div><div><<<</div><div><br></div><div>So I see that to make the definition work I somehow have to move the succ from the outside to the k' but I don't know what _n_50 n m k' is.</div>
<div><br></div><div>So three questions; how is it I'm constructing an infinite type when I replace the hole with 'eq-succ ih'? What is '_C_41 n m k'' and '_n_50 n m k'' and what do I do with them? It's probably a stupid question but I'm stumped.</div>
</div>