hidden function

Stream: general

[Mario Carneiro]

I just noticed a very clever trick that was used in a Coq development. We can define the following function:

@[reducible] def hidden {α : Sort*} {a : α} := a

This obviously isn't a very ergonomic function to write directly, but it can be used in tactics that have to manipulate large proof states and display them to the user, without getting in the way of any automation. (I should investigate if this is an appropriate use of abbreviation.) For example, we could have a tactic hide x which changes the type of x : T to x : @hidden _ T. The zero arg version could just do this for all assumptions whose pp is above a certain length. The Coq example was using this when proving theorems about large programs, to hide the "rest" of the program when working one statement at a time.

[Mario Carneiro]

demo:

@[reducible] def hidden {α : Sort*} {a : α} := a

open tactic
meta def repl : expr → ℕ → tactic expr
| e 0 := do
  t ← infer_type e,
  expr.sort u ← infer_type t,
  return (expr.app (expr.const ``hidden [u]) t e)
| (expr.app f x) (i+1) := do f' ← repl f (i+1), x' ← repl x i, return (f' x')
| (expr.lam n b d e) (i+1) := do
  var ← mk_local' n b d,
  e' ← repl (expr.instantiate_var e var) i,
  return (expr.lam n b d (expr.abstract_local e' var.local_uniq_name))
| e (i+1) := return e

meta def tactic.interactive.elide (n : ℕ) : tactic unit :=
do t ← target,
  t' ← repl t n,
  tactic.change t'

example : 2 + 2 = 4 :=
begin
  dunfold has_add.add, delta nat.add,
  -- ⊢ nat.brec_on 2
  --       (λ (a : ℕ) (_F : nat.below (λ (a : ℕ), ℕ → ℕ) a) (a_1 : ℕ),
  --         (λ (a a_1 : ℕ) (_F : nat.below (λ (a : ℕ), ℕ → ℕ) a_1),
  --             nat.cases_on a_1 (λ (_F : nat.below (λ (a : ℕ), ℕ → ℕ) 0), id_rhs ℕ a)
  --               (λ (a_1 : ℕ) (_F : nat.below (λ (a : ℕ), ℕ → ℕ) (nat.succ a_1)),
  --                 id_rhs ℕ (nat.succ ((_F.fst).fst a)))
  --               _F)
  --           a_1
  --           a
  --           _F)
  --       2 =
  --     4
  elide 5,
  -- ⊢ nat.brec_on 2 (λ (a : ℕ) (_F : nat.below (λ (a : ℕ), ℕ → ℕ) a) (a_1 : ℕ), hidden) 2 = 4
  refl
end

[Kevin Buzzard]

that's pretty cool :-)

[Patrick Massot]

It looks pretty cool. What is the exact meaning of the numeric parameter?

[Mario Carneiro]

it's the depth at which to start replacing subterms by hidden

[Mario Carneiro]

so higher means less hidden

[Reid Barton]

Would it be possible to have a version which replaces proofs by proof_of P, where @[reducible] def proof_of (P : Prop) {p : P} := p

[Reid Barton]

and then maybe add some notation for proof_of P to match \f<P\f>

[Reid Barton]

I thought that some combination of pp options was supposed to do this already, but I never figured out how

[Mario Carneiro]

well, just replacing that on its own won't work since it's still a prop so it gets displayed as _ anyway

[Reid Barton]

Oh dang

[Mario Carneiro]

but if you turn off pp.proofs then you can see it

[Mario Carneiro]

Then again, I think tactics can change options so you could have a tactic like elide that turns of pp.proofs at the same time as the replacement

[Reid Barton]

Oh, turn off? Okay, that's one thing that confused me

[Mario Carneiro]

oh that's a good point, I forget the polarity

[Kenny Lau]

and what difference does reducible make?

[Reid Barton]

actually now I'm doubly confused

[Reid Barton]

By experiment, I find that set_option pp.proofs true will display proofs

[Mario Carneiro]

but that's the default?

[Reid Barton]

Yes

[Reid Barton]

That is what is confusing me

[Reid Barton]

At least, that's what the autocompletion menu claims is the default. But setting it to true still causes proofs to be printed, and false causes them to be elided (which they are by default)

[Mario Carneiro]

reducible doesn't matter much, but it makes these identity functions not interfere with other tactics

[Mario Carneiro]

also the option description is a bit interesting -

(pretty printer) if set to false, the type will be displayed instead of the value for every proof appearing as an argument to a function

[Reid Barton]

Okay, that's where I saw it. I knew I'd seen it claimed somewhere that this feature already existed

[Reid Barton]

Maybe there are like... two options with the same name or something

[Mario Carneiro]

I think the description is outdated... it used to do that and I recall lobbying for the _ behavior

[Mario Carneiro]

I'm not sure if the type display thing was removed or replaced

[Mario Carneiro]

at least in the original version it just put the type instead of the proof and it was really confusing because it wasn't typecorrect

[Mario Carneiro]

looking at the code, I see no evidence that it does anything other than put _ in places, and only when pp.proofs = false

[Reid Barton]

I see. That does sound confusing, if there was nothing distinguishing the types of proofs from actual terms

[Mario Carneiro]

but I still can't figure out how the default turns out to be false, the code says it's true

[Kenny Lau]

truth is an illusion

[Gabriel Ebner]

There is no constant default: :smile: https://github.com/leanprover/lean/blob/30d883efef422facab3bf351d9fcff90c943298f/src/frontends/lean/pp.cpp#L1911-L1917

[Mario Carneiro]

wtf is that special case

[Mario Carneiro]

so sneaky

[Mario Carneiro]

I guess this is so that #print theorem doesn't show theorem thm : T := _ which would not be nice