Induction not correct for List(A) when replacement of type A is done.

[DmytroMitin]

After

  import TLImplicits._
  import shapeless._
  val A = "A" :: Type
  val B = "B" :: Type
  val a = "a" :: A
  val a1 = "a1" :: A
  val b = "b" :: B

  val Nat = "Nat" :: Type
  val n = "n" :: Nat
  val m = "m" :: Nat
  val NatInd = ("0" ::: Nat) |: ("succ" ::: Nat -->>: Nat) =: Nat
  val zero :: succ :: HNil = NatInd.intros
  val one = succ(zero)
  val two = succ(one)
  val three = succ(two)

  val recNNN = NatInd.rec(Nat ->: Nat)
  val addn ="add(n)" :: Nat ->: Nat
  val add = recNNN(m :-> m)(n :-> (addn :-> (m :-> succ(addn(m)) )))

  val Bool = "Boolean" :: Type
  val bool = "b" :: Bool
  val BoolInd = ("true" ::: Bool) |: ("false" ::: Bool) =: Bool
  val tru :: fls :: HNil = BoolInd.intros
  val recBoolBool = BoolInd.rec(Bool)
  val not = recBoolBool(fls)(tru)
  val recBoolAAA = BoolInd.rec(A ->: A ->: A)
  val ifElse = A :~> recBoolAAA(a :-> (a1 :-> a))(a :-> (a1 :-> a1))

  val recNatBool = NatInd.rec(Bool)
  val isEven = recNatBool(tru)(n :-> (bool :-> not(bool)))

  val List = "List" :: Type ->: Type
  val ListInd = ("nil" ::: A ~>>: (List -> List(A))) |: ("cons" ::: A ~>>: (A ->>: (List :> List(A)) -->>: (List -> List(A)) )) =:: List
  val nil :: cons :: HNil = ListInd.intros
  val list = cons(Nat)(zero)(cons(Nat)(one)(cons(Nat)(two)(nil(Nat))))

  val recLALB = ListInd.rec(List(B))
  val f = "f" :: A ->: B
  val as = "as" :: List(A)
  val as1 = "as1" :: List(A)
  val bs = "bs" :: List(B)
  val mapf = recLALB(A :-> nil(B))(A :~> (a :-> (as :-> (bs :-> cons(B)(f(a))(bs) ))))
  val map = A :~> (B :~> (f :-> mapf(A)))

map(Nat)(Nat)(succ)(list).fansi produces cons(Nat)(f(0))(cons(Nat)(f(succ(0)))(cons(Nat)(f(succ(succ(0))))(nil(Nat)))) rather than cons(Nat)(succ(0))(cons(Nat)(succ(succ(0)))(cons(Nat)(succ(succ(succ(0))))(nil(Nat))))

After

  val indLALA = ListInd.induc(A :~> (as :-> List(A)))
  val p = "p" :: A ->: Bool
  val filterp = indLALA(A :~> nil(A))(A :~> (a :-> (as :-> (as1 :-> ifElse(List(A))(p(a))(cons(A)(a)(as1))(as1) ))))
  val filter = A :~> (p :-> filterp(A))

filter(Nat)(isEven)(list).fansi produces (((<function1>) ((p : ((Nat : 𝒰 _0) → (Boolean : 𝒰 _0))) (0 : (Nat : 𝒰 _0)) : (Boolean : 𝒰 _0)) : (((List : ((𝒰 _0) → (𝒰 _0))) (Nat : 𝒰 _0) : 𝒰 _0) → (((List : ((𝒰 _0) → (𝒰 _0))) (Nat : 𝒰 _0) : 𝒰 _0) → ((List : ((𝒰 _0) → (𝒰 _0))) (Nat : 𝒰 _0) : 𝒰 _0)))) ((((cons : ($i : 𝒰 _0 ~> ($i : 𝒰 _0) → (((List : ((𝒰 _0) → (𝒰 _0))) ($i : 𝒰 _0) : 𝒰 _0) → ((List : ((𝒰 _0) → (𝒰 _0))) ($i : 𝒰 _0) : 𝒰 _0)))) (Nat : 𝒰 _0) : ((Nat : 𝒰 _0) → (((List : ((𝒰 _0) → (𝒰 _0))) (Nat : 𝒰 _0) : 𝒰 _0) → ((List : ((𝒰 _0) → (𝒰 _0))) (Nat : 𝒰 _0) : 𝒰 _0)))) (0 : (Nat : 𝒰 _0)) : (((List : ((𝒰 _0) → (𝒰 _0))) (Nat : 𝒰 _0) : 𝒰 _0) → ((List : ((𝒰 _0) → (𝒰 _0))) (Nat : 𝒰 _0) : 𝒰 _0))) ((((<function1>) ((p : ((Nat : 𝒰 _0) → (Boolean : 𝒰 _0))) ((succ : ((Nat : 𝒰 _0) → (Nat : 𝒰 _0))) (0 : (Nat : 𝒰 _0)) : (Nat : 𝒰 _0)) : (Boolean : 𝒰 _0)) : (((List : ((𝒰 _0) → (𝒰 _0))) (Nat : 𝒰 _0) : 𝒰 _0) → (((List : ((𝒰 _0) → (𝒰 _0))) (Nat : 𝒰 _... rather than cons(Nat)(zero)(cons(Nat)(two)(nil(Nat)))

After

  val opBAB = "op" :: B ->: A ->: B
  val seed = "seed" :: B
  val fbb = "f" :: B ->: B
  val recLABB = ListInd.rec(B ->: B)
  val foldlop = recLABB(A :-> (seed :-> seed))(A :~> (a :-> (as :-> (fbb :-> (seed :-> fbb(opBAB(seed)(a)) )))))
  val foldl = B :~> (A :~> (opBAB :-> (seed :-> foldlop(A))))

foldl(Nat)(Nat)(add)(zero)(list).fansi produces (seed : Nat) ↦ op(op(op(seed)(0))(succ(0)))(succ(succ(0))) rather than succ(succ(succ(0)))

After

  val recLAB = ListInd.rec(B)
  val opABB = "op" :: A ->: B ->: B
  val foldrop = recLAB(A :-> seed)(A :~> (a :-> (as :-> (b :-> opABB(a)(b) ))))
  val foldr = A :~> (B :~> (opABB :-> (seed :-> foldrop(A))))

foldr(Nat)(Nat)(add)(zero)(list).fansi produces op(0)(op(succ(0))(op(succ(succ(0)))(0))) rather than succ(succ(succ(0)))

[siddhartha-gadgil]

This seems to be a problem with the actual induction code, not .fansi (even the expanded form in map(Nat)(Nat)(succ)(list) has f in the expression, but all instances should be replaced by succ. Looks as if some nested replace is not going deep enough.

[siddhartha-gadgil]

There is already some problem with substitution of the introduction rules, e.g., with the list example above.

(A :~> (a :-> (as :-> (bs :-> cons(B)(g(a))(bs) )))).replace(g, f).fansi 
res77: String = "(A : 𝒰 ) ↦ (a : A) ↦ (as : List(A)) ↦ (bs : List(B)) ↦ cons(B)(g(a))(bs)"

we should have f in place of g in the result.

On the other hand, as expected:

( (a :-> (as :-> (bs :-> cons(B)(g(a))(bs) )))).replace(g, f).fansi 
res80: String = "(a : A) ↦ (as : List(A)) ↦ (bs : List(B)) ↦ cons(B)(f(a))(bs)"

The difference appears to be the appearance of A, which is an index.

[siddhartha-gadgil]

The above is actually expected behaviour, as A gets replaced by A.newobj so g is also changed in the closure of this. This seems to be the behaviour in all the examples, where f. op etc are used in a lambda and one defines a lambda in terms of these.

It appears the correct way would be to define, for example

val f = "f" :: A ~>: (B ~>:(A ->: B)))

and then use f(A)(B) etc while making definitions. I have not tested this.

Concretely, if f has domain A, or more generally depends on A, then the nesting f :~> ...A ~>: ... f( ) is not valid. One should instead make f a function of its domain and apply A.

[DmytroMitin]

Yes, with last changes this works. Thanks.

[siddhartha-gadgil]

Thanks a lot. You are now the expert on working concretely with my HoTT implementation (ahead of me). As usual, pull requests are gratefully accepted.

best regards, Siddhartha

On Tue, Feb 28, 2017 at 4:22 PM Dmytro Mitin notifications@github.com wrote:

Yes, with last changes this works. Thanks.

— You are receiving this because you commented. Reply to this email directly, view it on GitHub https://github.com/siddhartha-gadgil/ProvingGround/issues/113#issuecomment-283007662, or mute the thread https://github.com/notifications/unsubscribe-auth/ADatpJsrJwZPAMyLMMCL-8zvFrjDZ5xlks5rg_xPgaJpZM4MMDfv .