[Agda] uniform normalization

[Andreas Abel]

Since (f n) does not reduce to 0 (both equations are more specific), you 
have to split on n.

You could implement a tactic using Agda's new tactic language that does 
such routine jobs for you.

On 11.04.2016 18:28, Sergei Meshveliani wrote:
> Hello, All.
>
> I have the following question.
> The program
>
> -------------------------------------------------
> open import Relation.Binary.PropositionalEquality
> open import Data.Nat
>
> f : ℕ → ℕ
> f 0       = 0
> f (suc _) = 0
>
> theorem :  ∀ n → f n ≡ 0
> theorem _ =  refl
> --------------------------------------------------
>
> is not type-checked, because Agda expects the two proofs to be given.
> One for the case 0, another for the case (suc _).
> Both proofs can be set `refl', that is -- by normalization.
>
> Could the type checker check the proof by a single `refl', by
> normalizing each branch?
> (this will simplify many proofs).
>
> Thanks,
>
> ------
> Sergei
>
> _______________________________________________
> 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/