Zulip Chat Archive

Stream: new members

Topic: why does my def call _main?


Chris M (Aug 08 2020 at 03:40):

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 (Aug 08 2020 at 03:45):

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

Chris M (Aug 08 2020 at 03:46):

What API do you mean?

Chris B (Aug 08 2020 at 03:48):

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 (Aug 08 2020 at 03:48):

nil_append and cons_append

Kevin Buzzard (Aug 10 2020 at 12:15):

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 (Aug 10 2020 at 12:17):

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 (Aug 10 2020 at 12:18):

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


Last updated: Dec 20 2023 at 11:08 UTC