[Agda] uniform normalization

[Bradley Hardy]

By the new tactic language, do you mean the improved reflection capabilities in 2.5, or has something more Coq-like recently been implemented?


> On 11 Apr 2016, at 20:14, Andreas Abel <andreas.abel at ifi.lmu.de> wrote:
> 
> 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/
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda