why does my def call _main?

Stream: new members

[Chris M]

The following code:

def append {α : Type*} : list α → list α → list α
| []     l := l
| (h::t) l := h :: append t l

#print append

Generates the following printed message:

def append : Π {α : Type u_1}, list α → list α → list α :=
λ {α : Type u_1}, append._main

In order to get the full definition, I apparently need to write #print append._main instead, which gives:

def append._main : Π {α : Type _aux_param_0}, list α → list α → list α :=
λ {α : Type _aux_param_0} (a a_1 : list α),
  a.brec_on
    (λ (a : list α) (_F : list.below α a) (a_1 : list α),
       (λ (a a_1 : list α) (_F : list.below α a),
          a.cases_on (λ (_F : list.below α list.nil), id_rhs (list α) a_1)
            (λ (a_hd : α) (a_tl : list α) (_F : list.below α (a_hd :: a_tl)),
               id_rhs (list α) (a_hd :: _F.fst.fst a_1))
            _F)
         a
         a_1
         _F)
    a_1

What is this _main object? Why is it used, and do I need to think about it?

[Kenny Lau]

don't unfold definitions; the only things you need is the API

[Chris M]

What API do you mean?

[Chris B]

It's because you defined it using the equation compiler (by using pattern matching syntax). You actually get a couple of definitions that you can see with #print prefix append :

append : Π {α : Type u_1}, list α → list α → list α
append._main : Π {α : Type _aux_param_0}, list α → list α → list α
append._main._meta_aux : Π {α : Type _aux_param_0}, list α → list α → list α
append._main.equations._eqn_1 : ∀ {α : Type _aux_param_0} (l : list α), append._main list.nil l = l
append._main.equations._eqn_2 : ∀ {α : Type _aux_param_0} (h : α) (t l : list α), append._main (h :: t) l = h :: append._main t l
append._sunfold : Π {α : Type u_1}, list α → list α → list α
append.equations._eqn_1 : ∀ {α : Type u_1} (l : list α), append list.nil l = l
append.equations._eqn_2 : ∀ {α : Type u_1} (h : α) (t l : list α), append (h :: t) l = h :: append t l

The ones with _eqn_ are useful sometimes if you want to explicitly do a rewrite using the definition of a particular branch of your function after like cases l or something.

[Kenny Lau]

nil_append and cons_append

[Kevin Buzzard]

The first two things you should prove about append are nil_append and cons_append, that is, that append satisfies the two things which define it. If you are lucky the proofs are rfl, and in this case you don't ever need to think about append._main because you just proved the two theorems which completely characterise append.

[Kevin Buzzard]

Sometimes with a more complex inductive type where pattern matching is done in a more obscure way under the hood, these proofs might not be rfl and then you'll have to dig a bit deeper to find that actually the proof is called foo.equations._eqn_37 or whatever

[Kevin Buzzard]

but I bet nil_append and cons_append (which are _eqn_1 and _eqn_2) are provable with rfl