# Zulip Chat Archive

## Stream: new members

### Topic: Custom induction

#### Daniel Fabian (Aug 20 2019 at 19:26):

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 (Aug 20 2019 at 19:35):

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 (Aug 20 2019 at 19:40):

Ok, thanks for the hints

Last updated: May 16 2021 at 20:13 UTC