making mynat an add_comm_monoid

Stream: maths

[Kevin Buzzard]

I was trying to prove that a home-rolled nat was an add_comm_monoid in a way which was maximally mathematician-friendly, e.g. no leakage of le or zero: see gist.

My understanding of how Lean works is that I am supposed to come up with a canonical representative for things like mynat.zero -- I choose 0, and similarly I choose 1 for one. That's right, right?

On line 56 I have a zero which is something I never really wanted to see again. Is there a more high-powered tactic which will preserve my choice for 0 as the "canonical representative" of mynat.zero?

Is there a tactic that makes that instance on line 77 by just matching on names?

Finally lines 142 and 146 -- what is the incantation which makes these? I am so bad at making structures. Let's say that you must make an instance of add_semigroup mynat before you make the instance of add_comm_semigroup mynat.

[Keeley Hoek]

Kevin I think your by common_sense actually is a pretty easily makable tactic

[Keeley Hoek]

I'll give it a go

[Keeley Hoek]

...

end mynat

namespace tactic.interactive
open tactic

meta def replace_special_names : name → name
| `add := `has_add.add
| n := n

meta def common_sense : tactic unit :=
do t ← target,
   env ← get_env,
   match t with
   | expr.app (expr.const sn _) e :=
    match env.structure_fields sn with
    | some l :=
    do n :: _ ← tactic.open_namespaces,
       let lf := l.map replace_special_names,
       v ← lf.mmap resolve_name,
       let s : structure_instance_info := {
           struct := some sn,
           field_names := l,
           field_values := v,
       },
       e ← to_expr $ pexpr.mk_structure_instance s,
       tactic.exact e
    | none := fail "goal not a structure"
    end
   | _ := fail "unsupported goal"
   end

end tactic.interactive

namespace mynat

instance : add_monoid mynat := by common_sense

...

[Kevin Buzzard]

It works! Thanks! I hate making structures. I will use it forever.

[Kevin Buzzard]

Oh this is great. I have no clue how you're supposed to prove that mynat is a comm_semiring. You seem to have to perform the incantations all in exactly the right order in the official way to do it. This way I can just not even care. I went to the end of my multiplication file and typed instance : comm_semiring mynat := by common_sense and it just gave me a list of the fields for which it has failed and what the error messages were for each. I can then just make them at the end of my multiplication file as part of an api. This is brilliant.

It's sort-of an idiot-proof structure maker.

[Scott Morrison]

Can we have this in mathlib? Maybe called structure_helper?

[Patrick Massot]

Kevin, could you post an updated gist using this tactic? It would make this conversation easier to understand

[Kevin Buzzard]

Structure tactic

add_comm_monoid nat

[Patrick Massot]

Nice! I hope mathlib's naming convention won't interfere with merging this useful tactic

[Kevin Buzzard]

@Keeley Hoek

I can't make preorders because they have this weird lt_iff_not_le field.

set_option auto_param.check_exists false
class preorder (α : Type u) extends has_le α, has_lt α :=
(le_refl : ∀ a : α, a ≤ a)
(le_trans : ∀ a b c : α, a ≤ b → b ≤ c → a ≤ c)
(lt := λ a b, a ≤ b ∧ ¬ b ≤ a)
(lt_iff_le_not_le : ∀ a b : α, a < b ↔ (a ≤ b ∧ ¬ b ≤ a) . order_laws_tac)

I just want to not define lt or lt_iff_le_not_le

-- import the tactic
inductive mynat : Type

namespace mynat

def le : mynat → mynat → Prop := sorry
instance : has_le mynat := ⟨le⟩
def le_refl : ∀ a : mynat, a ≤ a := sorry
-- I think a,b,c should be implicit but Lean doesn't
def le_trans : ∀ a b c : mynat, a ≤ b → b ≤ c → a ≤ c := sorry

--instance : preorder mynat := by i_checked_all_teh_axioms -- fails
-- unknown identifier 'lt'

def lt : mynat → mynat → Prop :=  λ a b, a ≤ b ∧ ¬ b ≤ a

-- instance : preorder mynat := by i_checked_all_teh_axioms -- fails
/-
type mismatch at field 'lt_iff_le_not_le'
  lt_iff_le_not_le
has type
  ?m_3 < ?m_4 ↔ ?m_3 ≤ ?m_4 ∧ ¬?m_4 ≤ ?m_3
but is expected to have type
  auto_param (∀ (a b : mynat), a < b ↔ a ≤ b ∧ ¬b ≤ a) (name.mk_string "order_laws_tac" name.anonymous)
-/

end mynat
/-
class preorder (α : Type u) extends has_le α, has_lt α :=
(le_refl : ∀ a : α, a ≤ a)
(le_trans : ∀ a b c : α, a ≤ b → b ≤ c → a ≤ c)
(lt := λ a b, a ≤ b ∧ ¬ b ≤ a)
(lt_iff_le_not_le : ∀ a b : α, a < b ↔ (a ≤ b ∧ ¬ b ≤ a) . order_laws_tac)
-/

[Scott Morrison]

Ah, we'll have to add something that checks if a field is wrapped with auto_param, and then tries running the embedded tactic.

[Mario Carneiro]

or opt_param in the case of lt

[Andrew Ashworth]

hmm, wasn't there a hole tactic that did this as well that I saw posted awhile back? I may be misremembering

[Patrick Massot]

Do you mean https://github.com/leanprover-community/mathlib/blob/d001abfd48d64ac27310590458132009f47c852d/src/tactic/core.lean#L718? It's slightly different

[Andrew Ashworth]

ah, I think that is what I was thinking of

[Kevin Buzzard]

I just want to not even bother defining lt and lt_iff_le_not_le here

[Scott Morrison]

Yes, that's what we're proposing. Keeley's tactic should be able to identify opt_param or auto_param fields, and handle them automatically.

[Keeley Hoek]

I'm glad it helped! Yes this should be easy to fix...

[Keeley Hoek]

Oh hmm turns out it's a bit yuck...

[Kevin Buzzard]

instance : canonically_ordered_comm_semiring mynat :=
{ add := (+),
  add_assoc := add_assoc,
  zero := 0,
  zero_add := zero_add,
  add_zero := add_zero,
  add_comm := add_comm,
  le := (≤),
  le_refl := le_refl,
  le_trans := le_trans,
  le_antisymm := λ a b, le_antisymm,
  add_le_add_left := add_le_add_left,
  lt_of_add_lt_add_left := lt_if_add_lt_add_left,
  bot := _,
  bot_le := bot_le,
  le_iff_exists_add := le_iff_exists_add,
  mul := (*),
  mul_assoc := mul_assoc,
  one := 1,
  one_mul := one_mul,
  mul_one := mul_one,
  left_distrib := left_distrib,
  right_distrib := right_distrib,
  zero_mul := zero_mul,
  mul_zero := _,
  mul_comm := _,
  zero_ne_one := _,
  mul_eq_zero_iff := _ }

Also yuck.

[Keeley Hoek]

ha! its literally 3am where I am at the moment so I'm going to throw in the towel until morning---but just one last sorried function needs filling in:

[Keeley Hoek]

namespace tactic.interactive
open tactic

meta def replace_special_names : name → name
| `add := `has_add.add
| n := n

meta def get_type_of_nth_arg_core : ℕ → expr → expr
| _ _ := sorry

meta def get_type_of_nth_arg (n : name) (k : ℕ) : tactic expr :=
get_type_of_nth_arg_core k <$> (resolve_name n >>= to_expr >>= infer_type)

meta def run_tac (n : expr) : tactic unit :=
do n ← eval_expr name n,
   e ← resolve_name n >>= to_expr,
   tac ← eval_expr (tactic unit) e,
   tac

meta def resolve_name_or_use_autoparam (sn : name) (n : ℕ × name) : tactic (name × pexpr) :=
do pe ← resolve_name (replace_special_names n.2) <|>
        do { t : expr ← get_type_of_nth_arg (sn ++ `mk) n.1,
             match t with
             | `(auto_param %%t %%tac) :=
               lock_tactic_state $ do
                 m ← mk_meta_var t,
                 set_goals [m],
                 run_tac tac,
                 to_pexpr <$> instantiate_mvars m
             | _ := failed
             end
           },
   return (n.2, pe)

meta def i_checked_all_teh_axioms : tactic unit :=
do t ← target,
   env ← get_env,
   match t with
   | expr.app (expr.const sn _) e :=
    tactic.trace (env.structure_fields sn) >>
    match env.structure_fields sn with
    | some l :=
    do n :: _ ← tactic.open_namespaces,
       let l := (list.range l.length).zip l,
       v ← l.mfilter_map $ resolve_name_or_use_autoparam sn,
       tactic.trace v,
       let s : structure_instance_info := {
           struct := some sn,
           field_names := v.map prod.fst,
           field_values := v.map prod.snd,
       },
       tactic.trace v,
       e ← to_expr $ pexpr.mk_structure_instance s,
       tactic.exact e
    | none := fail "goal not a structure"
    end
   | _ := fail "unsupported goal"
end

end tactic.interactive

[Keeley Hoek]

haha funnily enough run_tac is equivalent to the ridiculous composite

meta def run_tac' (n : expr) : tactic unit :=
do tac ← eval_expr name n >>= resolve_name >>= to_expr >>= eval_expr (tactic unit),
   tac

[Kevin Buzzard]

instance : canonically_ordered_comm_semiring mynat :=
{ add := (+),
  add_assoc := add_assoc,
  zero := 0,
  zero_add := zero_add,
  add_zero := add_zero,
  add_comm := add_comm,
  le := (≤),
  le_refl := le_refl,
  le_trans := le_trans,
  le_antisymm := λ a b, le_antisymm,
  add_le_add_left := add_le_add_left,
  lt_of_add_lt_add_left := lt_if_add_lt_add_left,
  bot := ⊥,
  bot_le := bot_le,
  le_iff_exists_add := le_iff_exists_add,
  mul := (*),
  mul_assoc := mul_assoc,
  one := 1,
  one_mul := one_mul,
  mul_one := mul_one,
  left_distrib := left_distrib,
  right_distrib := right_distrib,
  zero_mul := zero_mul,
  mul_zero := mul_zero,
  mul_comm := mul_comm,
  zero_ne_one := zero_ne_one,
  mul_eq_zero_iff := mul_eq_zero_iff }

I finished my proof.

[Kenny Lau]

how about decidable le?

[Kevin Buzzard]

Oh that's not maths, that's not in this game

[Kevin Buzzard]

That is generated without telling the user

[Kevin Buzzard]

how about decidable le?

decidable le uses recursion. I am trying to box off what is done by recursion, because mathematicians put it in a different box to induction.

Example: one could present the natural numbers mynat as having two constants mynat.zero and mynat.succ, two axioms mynat.zero_ne_succ and mynat.succ_inj, and one key fact: you can use the induction n tactic if you have n : mynat. The two axioms are proved by Lean using recursion via nat.rec; succ_inj can be proved easily using the completely artificial function pred which no mathematician has ever seen or uses (because it allows 0 as an input and gives the wrong answer), and zero_ne_succ can be proved by defining a function which sends 0 to tt and succ n to ff, again a function which can be defined by recursion but is of no use to us in practice.

If you present nat this way and present addition similarly (mynat.add is a constant, we will always use the + notation, add_zero and add_succ are axioms, don't worry about how it was defined) then one can "prove" things like the "theorem" add_monoid mynat (because now it is a theorem -- all the data has been given to you and there's only a theorem left) purely within tactic mode, by supplying tactic proofs of each of the fields in whatever order you like.

I am looking at what happens to nat if you try and isolate all the computational content and "proofs and data constructed via recursion" and just give the user an inductive principle which can only be used to construct proofs. One way of looking at it is you could say that I was trying to isolate "the bit which mathematicians like best".

[Keeley Hoek]

Update: it almost works, but its hard to tell when a structure has optional parameters (the "auto-param" kind is fine). It turns out that the generated constructors don't have the opt_param part...

[Keeley Hoek]

But otherwise it's a lot more robust than before now

[Keeley Hoek]

Okay I found a tricksy way (not intended, but I don't think there is an API for this...)

[Keeley Hoek]

Ok its even tricker than I thought, extra idea...

[Keeley Hoek]

Yeah ok I'm really struggling. There is a lot of code now, and by some tricks I can find out which fields have optional/default values, but I can't find a way to determine what the values actually are. Secretly lean knows, but I think it might not be exposed. Does anyone know of a way to find the default value of a field declared opt_param?

[Keeley Hoek]

(Sounds like this might be a job for lean 3.5.0, just need to add a function)

[Keeley Hoek]

Here is the current state: https://gist.github.com/khoek/b820b0b242909a22bfd3b16a046eb9de
It does everything you want Kevin except for the lt problem.

[Mario Carneiro]

try_apply_opt_auto_param_for_apply might help as a template. It uses

when cfg.opt_param (try apply_opt_param) >>
when cfg.auto_param (try apply_auto_param)

[Mario Carneiro]

which are themselves implemented in lean in the obvious way

[Mario Carneiro]

but they are expecting the opt/auto_param to be the main goal, not sure if that's true in your case

[Keeley Hoek]

I can do the handling of those cases just fine (and that code is in the gist), the problem is that there is no way at all I can find to programmically get the opt_param blah associated to an optional field of a structure.

[Keeley Hoek]

If you make an example structure which has an optional and auto param for comparison, the autogenerated .mk retains the autoparam but drops the optional

[Mario Carneiro]

An optional field has the type opt_param type default_value

[Keeley Hoek]

Sure, but this information is not exposed by lean

[Mario Carneiro]

it's literally in the expr

[Keeley Hoek]

The expr for what?

[Mario Carneiro]

the type of the projection

[Keeley Hoek]

oooooooh!

[Keeley Hoek]

Hang on

[Keeley Hoek]

run_cmd (do
  tactic.mk_const `preorder.lt >>= tactic.infer_type >>= pp >>= tactic.trace
)

[Keeley Hoek]

I don't see any reference to the opt_param

[Keeley Hoek]

The constructor preorder.mk is the same; auto_param fields are replicated, the optional ones are dropped

[Mario Carneiro]

Oh, that's weird... I found a strange parsing issue while investigating this too

structure preorder1 (α : Type) [has_le α] :=
(le_refl : ∀ a : α, a ≤ a)
(le_trans : ∀ a b c : α, a ≤ b → b ≤ c → a ≤ c)
(lt := λ a b : α, a ≤ b ∧ ¬ b ≤ a)
(lt_iff_le_not_le : ∀ a b : α, lt a b ↔ (a ≤ b ∧ ¬ b ≤ a) := λ _ _, iff.rfl)

structure preorder2 (α : Type) [has_le α] :=
(le_refl : ∀ a : α, a ≤ a)
(le_trans : ∀ a b c : α, a ≤ b → b ≤ c → a ≤ c)
(lt : α → α → Prop := λ a b : α, a ≤ b ∧ ¬ b ≤ a)
(lt_iff_le_not_le : ∀ a b : α, lt a b ↔ (a ≤ b ∧ ¬ b ≤ a) . order_laws_tac)

The type of lt_iff_le_not_le is different in the two cases. preorder2 is the right one. preorder1.lt_iff_le_not_le is trivial as evidenced by the rfl proof. @Sebastian Ullrich Are you aware of this? It looks like that thing you pointed out a while back where structures could define lets and notation and other crazy things. Somehow lt is treated as a notation for the purposes of lt_iff_le_not_le, but it is also an actual field...?

[Keeley Hoek]

:0

[Mario Carneiro]

The other weird thing about this is that lt is already defined in the case of preorder, in has_lt, and it's getting "redefined" with a new defeq type in preorder

[Mario Carneiro]

I can already predict that the lean C++ code to make sense of all this is a rats nest

[Sebastian Ullrich]

Looks like a straight bug

[Patrick Massot]

Now is the time were Sebastian will paste that url to the commit which fixed that bug in Lean 4 months ago

[Kevin Buzzard]

I can make a preorder by just ignoring the lt and lt_iff_whatever fields completely. It's not possible to emulate that behaviour with a tactic?

[Keeley Hoek]

It appears that lean does not provide a way for lean to access the pre-set optional values of structures, eg. lt in this case.
I think I make it work but it'll be a little bit less robust than I had hoped

[Keeley Hoek]

@Kevin Buzzard Here is a link to something that works, at least on the two add_monoid and preorder examples I've seen! https://gist.github.com/khoek/cfb72fe41b0725269a14bf9196bb9c73

[Keeley Hoek]

Are you able to make a canonically_ordered_comm_semiring using it?

[Kevin Buzzard]

I'm now seeing all sorts of errors like

type mismatch at field 'lt_of_add_lt_add_left'
  lt_of_add_lt_add_left
has type
  ?m_3 + ?m_4 < ?m_3 + ?m_5 → ?m_4 < ?m_5
but is expected to have type
  ∀ (a b c : mynat), a + b < a + c → b < c

but this is not your fault -- I have defined lt_of_add_lt_add_left with the inputs implicit but apparently Lean wants them explicit. Nearly there now, just fixing all of them.

[Kevin Buzzard]

instance : canonically_ordered_comm_semiring mynat := by structure_helper -- works!

[Kevin Buzzard]

How do I get a complete list of all the typeclasses X such that type class inference can find a term of type X nat ?

[Kevin Buzzard]

But it works :-) Many thanks Keeley!

[Kevin Buzzard]

Ultimately I would rather lt_of_add_lt_add_left : ∀ {a b c : mynat}, a + b < a + c → b < c := ... because I believe that this is the idiomatic way to define this function, with a, b, c implicit. It stops the tactic working through. We can put that down to "further work if someone can be bothered".

[Kevin Buzzard]

@Mario Carneiro you were talking about a bug in Lean. Can this bug be easily fixed in 3.5.1? Would a consequence be that a whole bunch of _'s would need to be removed from mathlib? I feel like the definition of canonically_ordered_comm_semiring.lt_of_add_lt_add_left is "wrong".

canonically_ordered_comm_semiring.lt_of_add_lt_add_left : ∀ (a b c : ?M_1), a + b < a + c → b < c

I want to write some sort of front end for Lean where the user just has to type in simple proofs in tactic mode and that's all they can do. For this project, I don't care about mathlib and I don't care if I'm running a non-standard Lean. On the other hand if people change the behaviour of core tactics like induction then it will break everything I guess.

[Mario Carneiro]

You should just be using lt_of_add_lt_add_left

[Mario Carneiro]

which has the right binders

[Kevin Buzzard]

ooh. ordered_cancel_comm_monoid

[Kevin Buzzard]

I love that there are just a gazillion really stupid-in-my-eyes classes which are just out there and I don't know the names of any of them.

[Kevin Buzzard]

I don't want to use it, I want the user to prove it.

[Mario Carneiro]

There is a tactic that does the restating automatically

[Kevin Buzzard]

Yeah but I don't want to restate it, I want the user to prove it.

[Kevin Buzzard]

We're building nat from scratch.

[Mario Carneiro]

The binders don't matter if you are proving it

[Mario Carneiro]

it's lambda regardless

[Kevin Buzzard]

I know, I just feel like I'm lying to the user.

[Mario Carneiro]

In fact, it's usually better for the axiom to have all explicit or semi implicit binders when proving it

[Kevin Buzzard]

@Keeley Hoek I would like an over-ride. I'd like to define mynat.lt_of_add_lt_add_left with semi-implicit or implicit binders, and then define mynat.lt_of_add_le_add_left' to be the thing with the stupid binders and then tell your tactic to use the stupid version with the ' just for that field only.

[Mario Carneiro]

For instance, you might have an assumption that says ∀ (a b c : A), a + b < a + c → b < c and you want to pass it in; if the assumption is implicit then the arguments will get auto applied and it won't fit

[Mario Carneiro]

I would assume that for Keeley's tactic you can define the binders however you like

[Keeley Hoek]

Unfortunately Mario it seems that the structure-builder notation refuses to accept specifying a field with different binders =/

[Keeley Hoek]

Perhaps another bug?

[Keeley Hoek]

MWE:

structure thingo :=
(func : Π (a : ℕ), ℕ)

-- works
def foo : thingo := {func := λ {a : ℕ}, a + 1}

def concrete {a : ℕ} : ℕ := a + 1
-- doesn't
def bar : thingo := {func := concrete}

[Kevin Buzzard]

canonically_ordered_comm_semiring
  canonically_ordered_monoid,
    ordered_comm_monoid
      add_comm_monoid
      partial_order
    lattice.order_bot
      partial_order
  comm_semiring
  zero_ne_one_class

Generated by hand -- each thing extends the things one level of indentation below it.

[Kevin Buzzard]

That's funny because you would imagine that lam a, f is syntactically equal to lam {a}, f

[Kevin Buzzard]

structure thingo :=
(func : Π (a : ℕ), ℕ)

-- works
def foo : thingo := {func := λ {a : ℕ}, a + 1}

-- also works!
def concrete {{a : ℕ}} : ℕ := a + 1

def bar : thingo := {func := concrete}

[Mario Carneiro]

that's not a bug, that's by design

[Mario Carneiro]

and that's also why I said semi-implicit is a good choice here

[Kevin Buzzard]

Is there a "correct" decision for the variables in lt_of_add_le_add_left ? Or do you sometimes need one thing and sometimes another?

[Mario Carneiro]

It might work to use apply to figure out the right number of arguments

[Keeley Hoek]

ooh, well my tactic could count the number of expected explicit arguments and then instead of fn := fn not compiling fn := \lambda a b, @fn _ a b would compile. Would that have defeq problems?

[Mario Carneiro]

no

[Mario Carneiro]

In principle this is what apply is supposed to do, but it may not work for you

[Keeley Hoek]

Yes, due to the aforementioned opt_param problems the only way I can get those fields filled is using a structure_instance_info, which needs explicit pexprs to be provided.

[Keeley Hoek]

Also, is your "no" an answer to my question, or "no that won't work"?

[Mario Carneiro]

no defeq problems

[Mario Carneiro]

You can elaborate an expr using apply and then quote it to turn it into a pexpr

[Keeley Hoek]

Oh ok, I see what you are saying. I tried something like this for a bit but there were problems I think with the inter-dependence of the fields and things like le not being decided when le_refl was being decided using an apply. I guess you could build everything consistently so that all the fields of the structure had metavariables in their type in common when they correspond to the same thing? But this seems like some work

[Kevin Buzzard]

I am using Mario's approach of {{ }} when necessary