Zulip Chat Archive

Stream: general

Topic: statement linter


view this post on Zulip Patrick Massot (Jul 25 2018 at 22:20):

I have a new challenge in the same style as the print_names command, but harder. We all know how to produce the list of everything defined in the current Lean file. Now we want to filter the result, keeping only lemmas or theorems whose input contains two instances for the same type class. For instance, running this command in https://github.com/leanprover/mathlib/blob/master/analysis/topology/continuity.lean must return (among others) is_closed_diagonal since:

import analysis.topology.continuity

#check @is_closed_diagonal
/-
is_closed_diagonal :
  ∀ {α : Type u_1} [_inst_1 : topological_space α] [_inst_4 : topological_space α] [_inst_5 : t2_space α],
    is_closed {p : α × α | p.fst = p.snd}
-/

(this is due to instance explicitly asked for in the statement but already present as variables).

view this post on Zulip Reid Barton (Jul 25 2018 at 23:19):

oops!

view this post on Zulip Simon Hudon (Jul 26 2018 at 00:34):

Hint: if t is the type of is_closed_diagonal, t.is_pi will return tt (true) because t is a pi type (the assumptions are basically function arguments). t.binding_domain will gives you the type of the first assumption or variable (i.e. Type u_1) and t.binding_body will be the rest (i.e. ∀ [_inst_1 : topological_space α] [_inst_4 : topological_space α] [_inst_5 : t2_space α], is_closed {p : α × α | p.fst = p.snd}). Look at their definition and write a arguments : expr → tactic (list expr) function. This will bring you closer to a solution.

view this post on Zulip Patrick Massot (Jul 26 2018 at 07:58):

Thank you very much, I'll try to work on this exercise soon (but not right now).


Last updated: May 12 2021 at 05:19 UTC