Zulip Chat Archive

Stream: new members

Topic: Working with constructed objects


Vincent Beffara (Feb 07 2022 at 14:13):

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 (Feb 07 2022 at 14:15):

I think this is close to optimal.

Johan Commelin (Feb 07 2022 at 14:16):

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

Johan Commelin (Feb 07 2022 at 14:17):

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 (Feb 07 2022 at 14:18):

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

Johan Commelin (Feb 07 2022 at 14:18):

But it is currently beyond my tactic writing skills.

Vincent Beffara (Feb 07 2022 at 14:26):

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.


Last updated: Dec 20 2023 at 11:08 UTC