[Из песочницы] От зависимых типов к гомотопической теории типов на Scala + Shapeless + ProvingGround
Комментарии (1)
22 мая 2017 в 13:18
0↑
↓
val indN_naddSm_eq_S_naddm = NatInd.induc(n :-> (m ~>: ( add(n)(succ(m)) =:= succ(add(n)(m)) ))) val hyp1 = "n+Sm=S(n+m)" :: (m ~>: ( add(n)(succ(m)) =:= succ(add(n)(m)) )) val lemma = indN_naddSm_eq_S_naddm(m :~> succ(m).refl)(n :~> (hyp1 :-> (m :~> IdentityTyp.extnslty(succ)( add(n)(succ(m)) )( succ(add(n)(m)) )( hyp1(m) ) ))) !: n ~>: m ~>: ( add(n)(succ(m)) =:= succ(add(n)(m)) ) val lemma1 = IdentityTyp.extnslty(succ)( add(n)(succ(n)) )( succ(add(n)(n)) )( lemma(n)(n) ) val indN_naddn_eq_2n = NatInd.induc(n :-> ( add(n)(n) =:= double(n) )) val hyp = "n+n=2*n" :: ( add(n)(n) =:= double(n) ) val lemma2 = IdentityTyp.extnslty( m :-> succ(succ(m)) )( add(n)(n) )( double(n) )(hyp) indN_naddn_eq_2n(zero.refl)(n :~> (hyp :-> IdentityTyp.trans(Nat)( add(succ(n))(succ(n)) )( succ(succ(add(n)(n))) )( double(succ(n)) )(lemma1)(lemma2) )) !: n ~>: ( add(n)(n) =:= double(n) )
жесть.