has_lt for small inductive types

Stream: metaprogramming / tactics

[Johan Commelin]

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.

[Johan Commelin]

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

[Johan Commelin]

And rb_lmap wants a decidable has_lt on its key

[Kevin Buzzard]

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

[Mario Carneiro]

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⟩

[Johan Commelin]

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

[Johan Commelin]

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

[Mario Carneiro]

unfold; apply_instance

[Mario Carneiro]

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

[Johan Commelin]

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

[Mario Carneiro]

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

[Johan Commelin]

Then I'll remove the derive

[Mario Carneiro]

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 }) }

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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?

[Johan Commelin]

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

[Johan Commelin]

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

[Mario Carneiro]

that makes it difficult to print them though

[Mario Carneiro]

because printing requires an order

[Mario Carneiro]

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

[Johan Commelin]

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

[Johan Commelin]

But then, how do I print it?

[Mario Carneiro]

trace

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

/me is bad at writing meta code

[Mario Carneiro]

tactic.trace

[Johan Commelin]

Aah, thx

[Mario Carneiro]

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

[Johan Commelin]

Thanks for that explanation!

[Johan Commelin]

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

[Johan Commelin]

The first difference is now empty

[Johan Commelin]

But the second one contains lots of auto-generated declerations

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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