Default proofs

Stream: general

[Yaël Dillies]

So I know how I can provide default arguments to fields of a class, but how can I provide default proofs about them? I know that for nsmul we use a tactic, which makes me fear I can't write a default as I would have wanted to.

Here's what I'm working on (wink wink Anne):

import data.finset.basic

class locally_finite_order (α : Type*) [preorder α] [decidable_rel ((≤) : α → α → Prop)] :=
(finset_Icc : α → α → finset α)
(finset_Ico : α → α → finset α := λ a b, (finset_Icc a b).filter (λ x, ¬b ≤ x))
(finset_Ioc : α → α → finset α := λ a b, (finset_Icc a b).filter (λ x, ¬a ≤ x))
(finset_Ioo : α → α → finset α := λ a b, (finset_Icc a b).filter (λ x, ¬a ≤ x ∧ ¬b ≤ x))
(finset_mem_Icc : ∀ a b x : α, x ∈ finset_Icc a b ↔ a ≤ x ∧ x ≤ b)
(finset_mem_Ico : ∀ a b x : α, x ∈ finset_Ico a b ↔ a ≤ x ∧ x ≤ b :=  λ a b x, begin
  -- I would like to replace `finset_Ico` by `(finset_Icc a b).filter (λ x, ¬a ≤ x)`
end)
(finset_mem_Ioc : ∀ a b x : α, x ∈ finset_Ioc a b ↔ a ≤ x ∧ x ≤ b)
(finset_mem_Ioo : ∀ a b x : α, x ∈ finset_Ioo a b ↔ a ≤ x ∧ x ≤ b)

[Yury G. Kudryashov]

Indeed, you can only use := default_val syntax if default_val works always, not only for default arguments.

[Yury G. Kudryashov]

You can create a bunch of lemmas, write a tactic meta def mytac := [apply_rules [my_lemmas]], then use . mytac`.

[Yaël Dillies]

Should be pretty easy here!

[Yaël Dillies]

But that's disappointing Lean doesn't allow that. Is there any technical limitation?

[Mario Carneiro]

Yes, the field has to be type correct

[Mario Carneiro]

I suppose you could call that a technical limitation

[Yaël Dillies]

Hmm... :thinking:

[Mario Carneiro]

The standard workaround for this is to use tactics instead, like Yury says. For example see the lt fields in docs#preorder

[Yaël Dillies]

The technical limitation rather sounds like you can't "undefault" a field that depends on another default field that's been provided by the user.

[Mario Carneiro]

order_laws_tac is just intros; refl

[Mario Carneiro]

Exactly; you would be in trouble if you have def foo (a := 1) (b : a = 1 := rfl) and then decided to use foo 2 _

[Mario Carneiro]

or more to the point, @foo 2

[Mario Carneiro]

which has the type \forall (b : 2 = 1 := rfl), ... which doesn't typecheck

[Yaël Dillies]

I guess I don't know how default arguments work.

[Mario Carneiro]

A default argument (a : nat := 1) is just sugar for (a : opt_param nat 1)

[Yaël Dillies]

I guess I don't know how out_param works :rofl:

[Mario Carneiro]

and the type signature of docs#opt_param makes it clear that you can't put a default value that doesn't match the type

[Mario Carneiro]

that is, opt_param (2 = 1) rfl doesn't typecheck because rfl : 2 = 1 fails

[Mario Carneiro]

this is before we've even used the definition, mind

[Yaël Dillies]

Urf, yeah

[Mario Carneiro]

using tactics ("auto_param") works around this because we don't try to elaborate it until the definition is used

[Kevin Buzzard]

Yaël Dillies said:

I guess I don't know how out_param works :rofl:

@[reducible] def out_param (α : Sort u) : Sort u := α

What could be simpler? It's just id!

[Mario Carneiro]

unfortunately you can't actually specify a tactic block in lean 3 (lean 4 lets you do this) because tactic is meta so terms of that type can't appear in definitions, so instead you have to specify the name of a tactic like order_laws_tac

[Mario Carneiro]

which is the reason for all the indirection

[Mario Carneiro]

actually that's out_param, not opt_param

[Mario Carneiro]

opt_param is only slightly more complicated:

@[reducible] def opt_param (α : Sort u) (default : α) : Sort u := α

[Kevin Buzzard]

In maths we call that $pr_1$

[Kevin Buzzard]

It was when you were working on modules a few years ago that it all dawned on me that stuff like id can be harder than it looks.

[Eric Wieser]

When does the elaborator populate an opt_param with its default vs leaving it as a binder?

[Mario Carneiro]

If it is a regular application f a b and the third argument is c := ... then it will insert the default value

[Mario Carneiro]

basically, if there are any pis left over in a regular application and they are auto/opt params then it will insert them

[Mario Carneiro]

Unlike implicits and typeclass args, they don't work if used out of order:

def foo (a := 1) (b : ℕ) := 1
#check foo _ 3 -- foo ?M_1 3 : ℕ

[Mario Carneiro]

If you use @foo or @@foo then it will disable all argument insertion

[Yaël Dillies]

Mario Carneiro said:

using tactics ("auto_param") works around this because we don't try to elaborate it until the definition is used

Why can't this be the default behavior?

[Yaël Dillies]

Also, I tried the customized tactic trick, but I'm stuck because I can't reproduce the state that the tactic must solve. With the same example as above, if I do not provide finset_Ico, I get in finset_mem_Ico the goal I expect except for the fact that finset_Icc has been replaced by its definition (which stops me from using finset_mem_Icc). But when I do not provide finset_mem_Ico either, my tactic sees a goal where finset_Ico nor finset_Icc have been replaced by their definitions, but unfold locally_finite_order.finset_Ico or rw locally_finite_order.finset_Icowon't do anything.

[Yaël Dillies]

/me is writing a MWE

[Yaël Dillies]

I don't understand what's happening in either case.

import data.set.finite

section tactic
open tactic

meta def finset_Ico_laws_tac : tactic unit :=
whnf_target >> intros >> to_expr``(begin
  unfold locally_finite_order.finset_Ico,
  rw [finset.mem_filter, finset_mem_Icc, and_assoc, lt_iff_le_not_le]
end) >>= exact

end tactic

open finset

class locally_finite_order (α : Type*) [preorder α] [decidable_rel ((≤) : α → α → Prop)] :=
(finset_Icc : α → α → finset α)
(finset_Ico : α → α → finset α := λ a b, (finset_Icc a b).filter (λ x, ¬b ≤ x))
(finset_mem_Icc : ∀ a b x : α, x ∈ finset_Icc a b ↔ a ≤ x ∧ x ≤ b)
(finset_mem_Ico : ∀ a b x : α, x ∈ finset_Ico a b ↔ a ≤ x ∧ x < b . finset_Ico_laws_tac)

variables {α : Type*} [preorder α] [decidable_rel ((≤) : α → α → Prop)]

noncomputable def locally_finite_order_of_finite_Icc'
  (h : ∀ a b : α, (set.Icc a b).finite) :
  locally_finite_order α :=
{ finset_Icc := λ a b, (h a b).to_finset,
  finset_mem_Icc := λ a b x, by rw [set.finite.mem_to_finset, set.mem_Icc] }
/-simplify tactic failed to simplify
state:
α : Type u_1,
_inst_1 : preorder α,
_inst_2 : decidable_rel has_le.le,
h : ∀ (a b : α), (set.Icc a b).finite,
a b x : α
⊢ ?m_1
state:
α : Type u_1,
_inst_1 : preorder α,
_inst_2 : decidable_rel has_le.le,
h : ∀ (a b : α), (set.Icc a b).finite,
a b x : α
⊢ x ∈ filter (λ (x : α), ¬preorder.le b x) _.to_finset ↔ a ≤ x ∧ x < b-/

noncomputable def locally_finite_order_of_finite_Icc
  (h : ∀ a b : α, (set.Icc a b).finite) :
  locally_finite_order α :=
{ finset_Icc := λ a b, (h a b).to_finset,
  finset_mem_Icc := λ a b x, by rw [set.finite.mem_to_finset, set.mem_Icc],
  finset_mem_Ico := λ a b x, begin
    rw [finset.mem_filter, finset_mem_Icc, and_assoc, lt_iff_le_not_le], -- finset_mem_Icc
  end }

[Yaël Dillies]

Bump! Has anybody ideas?

[Yaël Dillies]

I switched to change and it seems more reliable, but I'm still blindcoding

[Mario Carneiro]

Why don't you just write a lemma instead of reproving the lemma every time someone uses your theorem?

[Mario Carneiro]

Hm, this has the unfortunate requirement that it needs finset_mem_Icc to be a hypothesis in scope, so you have to write the thing a little weirdly if you want to avoid repeating yourself:

import data.set.finite

theorem locally_finite_order.mem_Ico_of_mem_Icc
  {α : Type*} [preorder α] [decidable_rel ((≤) : α → α → Prop)]
  {finset_Icc : α → α → finset α}
  (finset_mem_Icc : ∀ a b x : α, x ∈ finset_Icc a b ↔ a ≤ x ∧ x ≤ b)
  (a b x : α) : x ∈ (finset_Icc a b).filter (λ x, ¬b ≤ x) ↔ a ≤ x ∧ x < b :=
by rw [finset.mem_filter, finset_mem_Icc, and_assoc, lt_iff_le_not_le]

meta def finset_Ico_laws_tac : tactic unit :=
`[exact locally_finite_order.mem_Ico_of_mem_Icc finset_mem_Icc]

class locally_finite_order (α : Type*) [preorder α] [decidable_rel ((≤) : α → α → Prop)] :=
(finset_Icc : α → α → finset α)
(finset_Ico : α → α → finset α := λ a b, (finset_Icc a b).filter (λ x, ¬b ≤ x))
(finset_mem_Icc : ∀ a b x : α, x ∈ finset_Icc a b ↔ a ≤ x ∧ x ≤ b)
(finset_mem_Ico : ∀ a b x : α, x ∈ finset_Ico a b ↔ a ≤ x ∧ x < b . finset_Ico_laws_tac)

variables {α : Type*} [preorder α] [decidable_rel ((≤) : α → α → Prop)]

noncomputable def locally_finite_order_of_finite_Icc'
  (h : ∀ a b : α, (set.Icc a b).finite) :
  locally_finite_order α :=
begin
  suffices finset_mem_Icc,
  exact { finset_Icc := λ a b, (h a b).to_finset,
          finset_mem_Icc := finset_mem_Icc },
  exact λ a b x, by rw [set.finite.mem_to_finset, set.mem_Icc],
end

[Mario Carneiro]

@Yaël Dillies

[Yaël Dillies]

Why can order_laws_tac work using the definition of ≤ whilefinset_Ico_laws_tac can't use finset_mem_Icc?

[Yaël Dillies]

Is what I'm trying to achieve that exotic?

[Mario Carneiro]

Because order_laws_tac doesn't need to reference anything outside its own statement for the proof, the proof is just rfl if you leave the default alone

[Mario Carneiro]

In your case, the proof for finset_mem_Ico depends on the proof of finset_mem_Icc

[Mario Carneiro]

I have a very hackish idea to get around this that would look for the current goal metavariable in the "result" (the term under construction), and hunt around in the parent of that expression to find the sibling proof of finset_mem_Ico

[Yaël Dillies]

That's the behavior I would have expected :smiley:

[Yaël Dillies]

because you can make fields dependent on others anyway, so that makes sense to be able to reference them.

[Mario Carneiro]

Here's a way to use spurious dependencies to make it work:

import data.set.finite

abbreviation id_annotate {α} (a : α) {β} (b : β) := b

theorem locally_finite_order.mem_Ico_of_mem_Icc
  {α : Type*} [preorder α] [decidable_rel ((≤) : α → α → Prop)]
  {finset_Icc : α → α → finset α}
  (finset_mem_Icc : ∀ a b x : α, x ∈ finset_Icc a b ↔ a ≤ x ∧ x ≤ b) :
  id_annotate finset_mem_Icc
    (∀ a b x : α, x ∈ (finset_Icc a b).filter (λ x, ¬b ≤ x) ↔ a ≤ x ∧ x < b) :=
λ a b x, by rw [finset.mem_filter, finset_mem_Icc, and_assoc, lt_iff_le_not_le]

meta def finset_Ico_laws_tac : tactic unit :=
`[exact locally_finite_order.mem_Ico_of_mem_Icc _]

class locally_finite_order (α : Type*) [preorder α] [decidable_rel ((≤) : α → α → Prop)] :=
(finset_Icc : α → α → finset α)
(finset_Ico : α → α → finset α := λ a b, (finset_Icc a b).filter (λ x, ¬b ≤ x))
(finset_mem_Icc : ∀ a b x : α, x ∈ finset_Icc a b ↔ a ≤ x ∧ x ≤ b)
(finset_mem_Ico : id_annotate finset_mem_Icc (∀ a b x : α, x ∈ finset_Ico a b ↔ a ≤ x ∧ x < b) . finset_Ico_laws_tac)

variables {α : Type*} [preorder α] [decidable_rel ((≤) : α → α → Prop)]

noncomputable def locally_finite_order_of_finite_Icc'
  (h : ∀ a b : α, (set.Icc a b).finite) :
  locally_finite_order α :=
{ finset_Icc := λ a b, (h a b).to_finset,
  finset_mem_Icc := λ a b x, by rw [set.finite.mem_to_finset, set.mem_Icc] }

[Yaël Dillies]

Ahah! The trick is to force finset_mem_Icc to appear in the context?

[Yaël Dillies]

You're a wizard, Mario. Thank you.

[Mario Carneiro]

in this case, we aren't putting it in the context, we're putting it in the type of the goal

[Mario Carneiro]

so lean can figure it out by unification

[Yaël Dillies]

I'm not sure I understand, but I'll keep that in mind for when I'll learn more about metaprogramming.

[Mario Carneiro]

If you actually want to prove finset_mem_Ico it is now uglified a bit, but autoparams also uglify the goal so I guess it's not that much worse

[Mario Carneiro]

this is actually pretty light on actual metaprogramming, this is more like elaborator-programming

[Yaël Dillies]

Can the abbreviation be made local?

[Mario Carneiro]

Actually I would probably want to lift it to init.core or logic.basic or so

[Mario Carneiro]

as you can see it's quite general

[Mario Carneiro]

But I didn't see an exact match among the annotation identity functions that lean has already

[Yaël Dillies]

Ah yeah, why not (even though it probably already exists?), but I was more thinking about stopping it from appearing in the goal.

[Mario Carneiro]

it's reducible so probably breathing lightly on it will make it go away

[Mario Carneiro]

in particular, if you want to prove that goal the first thing you do will probably be intros a b x and that will get rid of the junk

[Yaël Dillies]

What a metaphor. What else is there to scare it away?

[Yaël Dillies]

Ah yeah! then that's probably fine.

[Yaël Dillies]

Mario Carneiro said:

Actually I would probably want to lift it to init.core or logic.basic or so

Do you want to do that? I have no idea how to name it nor where to put it further than what you said.

[Mario Carneiro]

Put it in the miscellaneous section of logic.basic for now, if you are working on a PR

[Itai Bar-Natan]

Perhaps it's possible to use something like ite to make the dependent field only take a default value if the base field is the default value? Something that looks roughly like

finset_mem_Ico : ite (finset_Ico = default_value)
  (opt_param (∀ a b x : α, x ∈ finset_Icc a b ↔ a ≤ x ∧ x ≤ b) (...))
  (∀ a b x : α, x ∈ finset_Icc a b ↔ a ≤ x ∧ x ≤ b)

I don't think ite is definitionally equal to the opt_param option and even if it is I'm worried the optional parameter mechanism won't evaluate the type to recognize opt_param, but maybe some modification of this (perhaps with the ". tactic" system that I haven't learned yet) can be used for a general mechanism for dependent optional parameters.

[Yaël Dillies]

This can't work like that because finset_Ico = default_value is always true for correct locally_finite_order declarations. = can't distinguish between propositional and definitional equality. But maybe you can instead put in a tactic that tries refl and changes branch depending on its success or failure?
Also note that an itecan't do it because you need the hypothesis finset_Ico = default_value to fill in the (...). You must use dite instead.