Zulip Chat Archive

Stream: metaprogramming / tactics

Topic: has_lt for small inductive types


view this post on Zulip Johan Commelin (Oct 28 2020 at 09:24):

I have an inductive type

@[derive [decidable_eq, has_reflect, inhabited]]
inductive op | mul | add | div | sub | inv | neg

Is there an easy way to get a decidable has_lt on this type. I really don't care what the ordering is.

view this post on Zulip Johan Commelin (Oct 28 2020 at 09:24):

Reason: I want to use this as part of a key for a lookup table.

view this post on Zulip Johan Commelin (Oct 28 2020 at 09:25):

And rb_lmap wants a decidable has_lt on its key

view this post on Zulip Kevin Buzzard (Oct 28 2020 at 09:26):

does it have to be an order? Can you just define it to be "always false"?

view this post on Zulip Mario Carneiro (Oct 28 2020 at 09:28):

not fully automatic, but fairly easy:

namespace op
def to_nat : op  
| mul := 0 | add := 1 | div := 2
| sub := 3 | inv := 4 | neg := 5
end op

instance : has_lt op := λ x y, x.to_nat < y.to_nat

view this post on Zulip Johan Commelin (Oct 28 2020 at 09:33):

@Kevin Buzzard I wouldn't be surprised if rb_lmap will be angry with me if I try that trick.

view this post on Zulip Johan Commelin (Oct 28 2020 at 09:36):

@Mario Carneiro thx! How do I (easily) lift the decidability?

view this post on Zulip Mario Carneiro (Oct 28 2020 at 09:37):

unfold; apply_instance

view this post on Zulip Mario Carneiro (Oct 28 2020 at 09:39):

instance op.decidable_lt : decidable_rel ((<) : op  op  Prop) :=
by unfold has_lt.lt; apply_instance

view this post on Zulip Johan Commelin (Oct 28 2020 at 09:40):

instance : decidable_linear_order op :=
decidable_linear_order.lift to_nat (by { rintros ⟨⟩ ⟨⟩ ⟨⟩; refl })

view this post on Zulip Mario Carneiro (Oct 28 2020 at 09:41):

Unfortunately, it's not trivial to show that the decidable_eq instance induced by the order is the same as the decidable_eq instance you derived

view this post on Zulip Johan Commelin (Oct 28 2020 at 09:43):

Then I'll remove the derive

view this post on Zulip Mario Carneiro (Oct 28 2020 at 09:44):

actually I take it back, that rintros is doing more work for you than I thought

instance : decidable_linear_order op :=
{ decidable_eq := op.decidable_eq,
  ..decidable_linear_order.lift to_nat (by { rintros ⟨⟩ ⟨⟩ ⟨⟩; refl }) }

view this post on Zulip Johan Commelin (Oct 28 2020 at 09:45):

Is there benefit in using the decidable_eq from the derive handler?

view this post on Zulip Johan Commelin (Oct 28 2020 at 10:03):

I have two list names. How can I make lean print the diff?

view this post on Zulip Johan Commelin (Oct 28 2020 at 10:03):

meta def check_list : tactic unit :=
do env  tactic.get_env,
  let lems := (env.get_decls.map declaration.to_name).filter (λ n, name.is_prefix_of `baby_calc n),
  let M1 : multiset name := lookup.values,
  let M2 : multiset name := lems,
  -- what goes here?

view this post on Zulip Johan Commelin (Oct 28 2020 at 10:03):

I turned them into multisets because I don't care about the order.

view this post on Zulip Johan Commelin (Oct 28 2020 at 10:03):

(I also don't care about multiplicity, actually)

view this post on Zulip Mario Carneiro (Oct 28 2020 at 10:04):

that makes it difficult to print them though

view this post on Zulip Mario Carneiro (Oct 28 2020 at 10:04):

because printing requires an order

view this post on Zulip Mario Carneiro (Oct 28 2020 at 10:05):

so you can either sort them, don't turn them into multisets, or use unquot to unsafely get the underlying list

view this post on Zulip Johan Commelin (Oct 28 2020 at 10:05):

Ok, so I can take the unquot of M1 - M2.

view this post on Zulip Johan Commelin (Oct 28 2020 at 10:05):

But then, how do I print it?

view this post on Zulip Mario Carneiro (Oct 28 2020 at 10:05):

trace

view this post on Zulip Johan Commelin (Oct 28 2020 at 10:08):

type mismatch at application
  trace (quot.unquot D1)
term
  quot.unquot D1
has type
  list name
but is expected to have type
  string

view this post on Zulip Johan Commelin (Oct 28 2020 at 10:12):

type mismatch at application
  bind (trace (to_string (quot.unquot D1)))
term
  trace (to_string (quot.unquot D1))
has type
  thunk ?m_1  ?m_1 : Type ?
but is expected to have type
  tactic ?m_1 : Type

view this post on Zulip Johan Commelin (Oct 28 2020 at 10:12):

/me is bad at writing meta code

view this post on Zulip Mario Carneiro (Oct 28 2020 at 10:13):

tactic.trace

view this post on Zulip Johan Commelin (Oct 28 2020 at 10:15):

Aah, thx

view this post on Zulip Mario Carneiro (Oct 28 2020 at 10:15):

there is also _root_.trace which is useful for tracing pure code; it has a string argument that will be traced (you have to call to_string), followed by a thunk which is whatever the expression is actually supposed to return. The tactic tactic.trace is a bit easier to use, it takes anything that implements has_to_tactic_format which is just about everything

view this post on Zulip Johan Commelin (Oct 28 2020 at 10:24):

Thanks for that explanation!

view this post on Zulip Johan Commelin (Oct 28 2020 at 10:28):

Ok, I have a partial victory:

meta def check_list : tactic unit :=
do env  get_env,
  let lems := (env.get_decls.map declaration.to_name).filter (λ n, name.is_prefix_of `calc_step n),
  let M1 : multiset name := lookup.values.map (name.append `calc_step),
  let M2 : multiset name := lems,
  let D1 := (M1 - M2),
  let D2 := (M2 - M1),
  trace "diff 1:",
  trace D1.unquot,
  trace "diff 2:",
  trace D2.unquot

run_cmd check_list

view this post on Zulip Johan Commelin (Oct 28 2020 at 10:28):

The first difference is now empty

view this post on Zulip Johan Commelin (Oct 28 2020 at 10:28):

But the second one contains lots of auto-generated declerations

view this post on Zulip Johan Commelin (Oct 28 2020 at 10:28):

Can I somehow check whether a declaration was declared by me in the file using lemma, or auto-generated by lean?

view this post on Zulip Johan Commelin (Oct 28 2020 at 10:42):

private
meta def check_list : tactic unit :=
do env  get_env,
  let names := env.get_decls.map declaration.to_name,
  let in_scope := names.filter (λ n, name.is_prefix_of `calc_step n),
  let lems := in_scope.filter (λ n,
            !name.is_prefix_of `calc_step.side n &&
            !name.is_prefix_of `calc_step.op   n &&
            !name.is_prefix_of `calc_step.sign n &&
            !name.is_prefix_of `calc_step.rel  n &&
            !name.is_prefix_of `calc_step.lookup_list n &&
            !name.is_prefix_of `calc_step.lookup n),
  let M1 : multiset name := lookup.values.map (name.append `calc_step),
  let M2 : multiset name := lems,
  let D1 := (M1 - M2),
  let D2 := (M2 - M1),
  trace D1.unquot,
  trace D2.unquot

run_cmd check_list

view this post on Zulip Johan Commelin (Oct 28 2020 at 10:42):

This now traces [] [] :tada:
Thanks for all the help


Last updated: May 09 2021 at 23:10 UTC