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

[Jan Stolarek]

Oh, it was that simple :-) Thanks!

Janek

Dnia czwartek, 31 października 2013, Twan van Laarhoven napisał:
> 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
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda