Custom induction

Stream: new members

[Daniel Fabian]

Good evening,

As an exercise, I'm trying to formalize a piece of math that I have around Cartesian products. Because I need to know each component involved in the product, I don't think I can rely on the built-in notion of Cartesian products. E.g. Nat * Nat * Nat is not the same as (Nat * Nat) * Nat or Nat * (Nat * Nat) w.r.t. the theorems I want to talk about.

To formalize that, I tried to do it using a heterogeneous list and attach a count to get pretty much the same behavior as a Cartesian product. Here's my code I'm playing with:

universe u
inductive h_list : Type (u+1)
| nil
| cons {α : Type u} (h:α) (t:h_list) : h_list

namespace h_list

notation h :: t := cons h t

notation `[` l:(foldr `, ` (h t, cons h t) nil `]`) := l

def length : h_list → ℕ
| [] := 0
| (cons _ t) := 1 + t.length

def append : h_list → h_list → h_list
| [] ys := ys
| (x::xs) ys := x :: (append xs ys)

instance h_list_has_append : has_append h_list := ⟨append⟩

#check 3 :: "hello" :: nil
#check ['a', "bee", 3]
end h_list

def tuple (n : ℕ) := { l : h_list // l.length = n }
namespace tuple
open h_list

def cons {α n} : α → tuple n → tuple (n + 1)
| h ⟨t, h_n⟩ := ⟨h :: t, by {unfold length, rw[h_n], simp}⟩

def singleton {α} : α → tuple 1
| x := ⟨[x], by unfold length⟩

def append {n m} : tuple n → tuple m → tuple (n + m)
| ⟨l, h_n⟩ ⟨r, h_m⟩ := ⟨l ++ r, sorry⟩

notation `[` l:(foldr ` ⊗ ` (h t, cons h t) nil `]`) := l

infix ` ⊗ `:30 := append
#check append
end tuple

#check tuple.cons
#check ℕ × nat × ℤ × int
#check (1, 3, 4)
#check prod

In the bit of sorry, I would like to show the property by induction on l. When I try to use the built-in tactic, the IH is wrong; it is only getting smaller w.r.t. l and not also n. Similarly induction on n doesn't work either.

Do I understand correctly, that I need to prove a different kind of induction principle to do this kind of induction and then call the induction tactic with using?

Alternatively, is there some much less clunky way to achieve what I want?

Thanks Dany

[Simon Hudon]

Your code strikes me as having a lot of dependent types. If you need them to be this dependent, you might find all that you need in data.vector. Your tuple construction can be defined as def tuple (n : nat) := vector (Σ t : Type u, t) n.

You might find that reasoning in terms of list (Σ t : Type u, t) will be good enough for most of your theorems. Having the length in the type gets very annoying when the length varies

[Daniel Fabian]

Ok, thanks for the hints