От зависимых типов к гомотопической теории типов на Scala + Shapeless + ProvingGround

Для «реально сложных выкладок» есть более подходящие инструменты.

Я даже не могу понять где тут доказательство для базы, где для шага индукции.

Здесь фактически доказательства двух утверждений: первое —

n ~>: m ~>: ( add(n)(succ(m)) =:= succ(add(n)(m)) )

второе —

n ~>: ( add(n)(n) =:= double(n) )

Для доказательства второго мне было нужно первое и пришлось его доказать тоже. В Идрисе первое — это стандартное plusSuccRightSucc.
У первого база —

m :~> succ(m).refl

шаг —

n :~> (hyp1 :-> (m :~> 
    IdentityTyp.extnslty(succ) ...

т.е. аргументы, к которым применена индукция indN_naddSm_eq_S_naddm.
У второго база —

zero.refl

шаг —

n :~> (hyp :->
    IdentityTyp.trans(Nat) ...

т.е. аргументы, к которым применена индукция indN_naddn_eq_2n.

… то по идее в ProvingGround должны быть какие-то очень мощные эвристики.

Мощных эвристик особо не заметил :) Сиддхартха как-то пробует применять методы machine learning.
1 2 3 4

И ещё HoTT как-то упрощает формулировку и доказательство теорем по сравнению с другими подходами?

HoTT расширяет класс теорем (упрощает работу с ними). То есть не только теоремы типа (n+m)+k=n+(m+k), n+n=2*n, но и типа π₁(S¹)=Z, π₂(S²)=Z, π₃(S²)=Z.

Тот же Isabelle/HOL выглядит гораздо понятнее.

Следует отличать учебный инструмент от индустриального инструмента.
В Идрисе, например, доказательство того, что если хвосты равны, то после приклеивания одинаковых голов списки опять равны, выглядит просто как

same_cons : {xs : List a} -> {ys : List a} -> xs = ys -> x :: xs = x :: ys
same_cons Refl = Refl

В ProvingGround — как

val as = "as" :: ListA
val as1 = "as1" :: ListA
val as2 = "as2" :: ListA
val pf = "as=as1" :: ( as =:= as1 )
a :~> (as :~> (as1 :~> (pf :-> IdentityTyp.extnslty(as2 :-> cons(a)(as2))(as)(as1)(pf)
      ))) !:  a ~>: as ~>: as1 ~>: (( as =:= as1 ) ->: ( cons(a)(as) =:= cons(a)(as1) ))

которое можно записать короче:

val as = "as" :: ListA
val as1 = "as1" :: ListA
a :~> (as :~> (as1 :~> IdentityTyp.extnslty(cons(a))(as)(as1)
      )) !:  a ~>: as ~>: as1 ~>: (( as =:= as1 ) ->: ( cons(a)(as) =:= cons(a)(as1) ))

В Идрисе доказательство того, то n+0=n — это

plus_n_zero : (n : Nat) -> n + 0 = n
plus_n_zero Z = Refl
plus_n_zero (S n) = rewrite plus_n_zero n
                      in Refl

В ProvingGround —

val indN_nadd0_eq_n = NatInd.induc(n :-> ( add(n)(zero) =:= n ))
val hyp = "n+0=n" :: ( add(n)(zero) =:= n )
indN_nadd0_eq_n(zero.refl)(n :~> (hyp :-> IdentityTyp.extnslty(succ)( add(n)(zero) )(n)(hyp)
      )) !:  n ~>: ( add(n)(zero) =:= n )

или короче

val indN_nadd0_eq_n = NatInd.induc(n :-> ( add(n)(zero) =:= n ))
indN_nadd0_eq_n(zero.refl)(n :~> IdentityTyp.extnslty(succ)( add(n)(zero) )(n)
      ) !:  n ~>: ( add(n)(zero) =:= n )

Первое написать проще (и при реальной работе удобнее), но второе имхо лучше для понимания что происходит (когда разбираешься, когда пишешь учебный курс). Иначе вся магия спрятана за строчкой типа функция от Refl равна Refl, за rewrite'ами и т.д.