[Agda] simple question

[Andreas Abel]

Andrew,

You cannot do an inductive proof, like eq-plus-req, using natrec.  You 
need the corresponding induction principle,

   nat-ind : (P : Nat -> Set)
          -> P zero
          -> ((n : Nat) -> P n -> P (suc n))
          -> (m : Nat) -> P m

Or you do case distinction on n and call eq-plus-req recursively for the 
induction hypothesis.

Cheers,
Andreas

P.S.: cong is eq-succ generalized to arbitrary functions instead of 
succ.  So cong succ is the same as eq-succ.

On 14.10.2014 13:58, Andrew Harris wrote:
> @andreas and kyle,
>
> Thanks -- it seems like the following definition type-checks:
>
> {- proof of eq-succ -}
> eq-succ : {n m : Nat} → n == m → succ n == succ m
> eq-succ (refl m) = refl (succ m)
>
> However, the exercise is to define this eq-succ function above that is
> to be used in a proof of the equivalence of + versus "plus":
>
> eq-plus-req : (n m : Nat) → (n + m) == (plus n m)
> eq-plus-req n m = natrec (refl m) (\k' ih → eq-succ ih) n
>
> (this function definition is provided in the paper).  However, this
> function no longer typechecks, I think it has something to do with the
> definition of eq-succ above.  In the paper, it says explicitly that the
> eq-succ can be proved using "natrec" -- that's why I was trying to
> define it with natrec in my original question.  I certainly do think
> that the definition you suggested makes more sense to me but I'm
> wondering why it causes eq-plus-req not to typecheck (here is the error
> I get):
>
> Refuse to construct infinite term by instantiating _58 to succ
> (_n_58 n m k')
> when checking that the expression eq-succ ih has type
> _n_58 n m (succ k') == _m_59 n m (succ k')
>
> @mateusz and silvio,
>
> Thanks for this suggestion.  I will investigate what "cong suc" means --
> I certainly don't know currently.  It is not something that I have seen
> discussed in the previous sections of the paper that I'm reading.  And
> this paper is serving as my introduction to Agda...
>
> -andrew
>
> On Tue, Oct 14, 2014 at 5:55 AM, <silvio at cs.ioc.ee
> <mailto:silvio at cs.ioc.ee>> wrote:
>
>     Hi All,
>
>             Hello,
>
>                 I'm trying to follow along in the very good paper
>             "Dependent Types At
>             Work" written by Ana Bove and Peter Dybjer.  I'm stuck at
>             trying to prove
>             "eq-succ", which is one of the exercises in Section 4.4.
>             The closest I can
>             make it is the following:
>
>
>     CUT
>
>
>         This is probably a stupid question considering I haven't looked
>         at the
>         cited work, but what's wrong with just ?cong suc??
>
>         --
>         Mateusz K.
>
>
>     I agree with Mateusz. This is actually how I did it when I was doing
>     the same exercise.
>
>     Best regards,
>
>     Silvio
>
>
>     _________________________________________________
>     Agda mailing list
>     Agda at lists.chalmers.se <mailto:Agda at lists.chalmers.se>
>     https://lists.chalmers.se/__mailman/listinfo/agda
>     <https://lists.chalmers.se/mailman/listinfo/agda>
>
>
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>


-- 
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/