Working with constructed objects

Stream: new members

[Vincent Beffara]

Hi, this is kind of a vague question. Sometimes I end up constructing an object in a convoluted way using lots of scaffolding involving things like auxiliary functions, classical.some and nat.find and whatever, and I then need to prove properties of this object. Then the proof of the property ends up looking exactly like the construction with classical.some_spec and nat.find_spec and nat.find_eq_iff and so on instead at the same places, and there is a lot of repetition, which feels sad.

At the moment I end up with code like this,

def thing_aux (assumptions) : {x // P1 x ∧ P2 x ∧ P3 x} := sorry

def thing (assumptions) := (thing_aux (assumptions)).val

lemma prop1 {assumptions} : P1 (thing (assumptions)) := (thing_aux (assumptions)).prop.1

and so on, which feels a little bit better because the scaffolding needs to be constructed only once, but I feel like there must be a nicer way to proceed. What is the recommended best practice?

[Johan Commelin]

I think this is close to optimal.

[Johan Commelin]

You could imagine that after you have thing_aux, it should be a one-liner to extract thing, prop1, prop2, etc...

[Johan Commelin]

Coincidentally, @Mario Carneiro recently wrote an unpack command for approximately that scenario. I'll copy his code here:

noncomputable def Exists.some {α} {P : α → Prop} (h : ∃ x, P x) : α := classical.some h
theorem Exists.some_spec {α} {P : α → Prop} (h : ∃ x, P x) : P h.some := classical.some_spec h

namespace tactic
open lean.parser interactive.types

meta inductive tuple
| one : name → tuple
| many : list tuple → tuple

meta def tuple_parser : lean.parser tuple
| e := (tuple.one <$> ident_ <|>
  brackets "⟨" "⟩" (tuple.many <$> sep_by (skip_info (tk ",")) tuple_parser)) e

meta def tuple.split : tuple → name ⊕ (tuple × tuple)
| (tuple.one n) := sum.inl n
| (tuple.many []) := sum.inl `_
| (tuple.many [t, t2]) := sum.inr (t, t2)
| (tuple.many (t :: ts)) := sum.inr (t, tuple.many ts)

meta def run_unpack : tuple → expr → expr → lean.parser unit
| t ty pr := match t.split with
  | sum.inl `_ := pure ()
  | sum.inl n := do
    ty ← pp ty,
    pr ← pp pr,
    with_input command_like sformat!"lemma {n} : {ty} := {pr}",
    pure ()
  | sum.inr (t₁, t₂) := match ty with
    | `(Exists %%(expr.lam _ bi d ty)) := do
      sum.inl n ← pure t₁.split | fail "pattern matching exists not supported",
      pd ← pp d,
      ppr ← (mk_app ``Exists.some [pr] >>= pp : tactic _),
      with_input command_like sformat!"def {n} : {pd} := {ppr}",
      var ← (resolve_name n >>= to_expr : tactic _),
      mk_app ``Exists.some_spec [pr] >>= run_unpack t₂ (ty.instantiate_var var)
    | `(%%ty₁ ∧ %%ty₂) := do
      mk_app ``and.left [pr] >>= run_unpack t₁ ty₁,
      mk_app ``and.right [pr] >>= run_unpack t₂ ty₂
    | _ := fail "pattern matching on this type not supported"
    end
  end

@[user_command] meta def unpack (_ : interactive.parse (tk "unpack")) : lean.parser unit := do
  args ← tuple_parser,
  tk ":=",
  e ← lean.parser.pexpr 0,
  e ← tactic.to_expr e,
  ty ← (infer_type e : tactic _),
  tactic.set_options $ options.mk.set_bool `pp.all tt,
  run_unpack args ty e

end tactic

[Johan Commelin]

It might be possible to adapt this so that it doesn't only work with ∃ but also with subtypes.

[Johan Commelin]

But it is currently beyond my tactic writing skills.

[Vincent Beffara]

Nice! Going back and forth between exists and subtype with subtype.exists_of_subtype and classical.subtype_of_exists is always an option, I only chose the subtype because I got the impression that it was better to confine the classical part to one lemma rather than to use some all over the place.