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