[Agda] Proving m + (1 + n) == 1 + (m + n)

[Twan van Laarhoven]

Your subst function is defined with type

 > subst : {A : Set}{P : A → Prp} → {a b : A} → a == b → P a → P b

So it takes only two explicit argument, the equality and the P a. Compared to 
subst in the standard library, which also makes P explicit, i.e.

 > subst : {A : Set} (P : A → Prp) → {a b : A} → a == b → P a → P b

In _++'_ you do give an explicit argument for P, Vec X. The typechecker 
therefore complains that you give too many arguments.


Twan

On 31/10/13 12:59, Jan Stolarek wrote:
> Hi *,
>
> I'm trying to figure out how to prove things like m + (1 + n) == 1 + (m + n) so that I can write
> reverse-append function for vectors. I found materials for Computer Aided Formal Reasoning
> (http://www.cs.nott.ac.uk/~txa/g53cfr/) to be quite accessible, but there are some things I don't
> understand. Lecture 9 gives a proof of correctness for reverse-append:
>
> _++'_ : {X : Set} {n m : ℕ} → Vec X n → Vec X m → Vec X (n + m)
> _++'_ {X} {zero } {m} []       ys = ys
> _++'_ {X} {suc n} {m} (x :: xs) ys =
>    subst (Vec X) (sym (+suc n  m)) (xs ++' (x :: ys))
>
> where
>
> +suc : (m n : ℕ) → suc (m + n) ≡ m + (suc n)
> +suc zero n = refl
> +suc (suc m) n = cong suc (+suc m n)
>
> and cong, subst, refl and sym are imported from Relation.Binary.PropositionalEquality, Nat is from
> Data.Nat and Vec is from Data.Vec. However, if remove import of PropositionalEquality and use
> definitions of cong, subst, refl and sym that were given earlier in the course (lecture 7):
>
> Prp : Set1
> Prp = Set
>
> data _==_ {A : Set} : A → A → Prp where
>      refl : {a : A} → a == a
>
> sym : {A : Set} → {a b : A} → a == b → b == a
> sym refl = refl
>
> cong : {A B : Set} (f : A → B) → forall {x y} → x == y → f x == f y
> cong f refl = refl
>
> subst : {A : Set}{P : A → Prp} → {a b : A} → a == b → P a → P b
> subst refl p = p
>
> I get error when typechecking second case of _++'_. Typechecker higlights Vec X (first argument to
> subst) and produces an error:
>
>    ℕ → Set !=< _a_55 n x xs ys ≡ _b_56 n x xs ys of type Set₁
>    when checking that the expression Vec X has type
>    _a_55 n x xs ys ≡ _b_56 n x xs ys
>
> I can't figure out goes wrong here. I looked at the definitions of refl, sym and other functions
> in standard library to see how they differ. I see that refl in std lib operates on other levels
> than just Set. As for other functions thier definition in the library is too difficult for me to
> understand. I would appreciate if someone could explain why the typechecker complains and how to
> fix definitions of refl & friends so that it works.
>
> Janek
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>