Zulip Chat Archive

def choose1 (nondep : Bool) (h : Option Expr) (data : Name) :
  TacticM ElimStatus := do
  let g ← getMainGoal
  let (g, h) ← match h with
  | some e => pure (g, e)
  | none   => do
    let (e, g) ← g.intro1P
    pure (g, .fvar e)
  g.withContext do
    let h ← instantiateMVars h
    let t ← inferType h
    forallTelescopeReducing t $ fun ctxt t => do
      let t ← withTransparency .all (whnf t)
      match t.getAppFnArgs with
      | (`Exists, #[α, p]) => do
        let ne_fail : ElimStatus := .failure []
        let nonemp : Option Expr := none
        let ctxt' ← if nonemp.isSome then ctxt.filterM (fun e => not <$> isProof e) else pure ctxt
        let data_ty ← mkForallFVars ctxt' α
        let data_val ← mkAppM ``Classical.choose #[mkAppN h ctxt]
        let (d, g) ← (← g.assert data data_ty data_val).intro1P
        let spec_ty ← mkForallFVars ctxt (p.app (mkAppN (.fvar d) ctxt')).headBeta
        let spec_val ← mkAppM ``Classical.choose_spec #[mkAppN h ctxt]
        let mut g ← g.assert .anonymous spec_ty spec_val
        match h with
        | .fvar v => g ← g.clear v
        | _ => pure ()
        replaceMainGoal [g]
        return ne_fail
        | (`And, #[p, q]) => throwError "not implemented yet"
        -- TODO: support Σ, × ?
        | _ => throwError "expected a term of the shape `∀xs, ∃a, p xs a` or `∀xs, p xs ∧ q xs`"

Johan Commelin (Sep 15 2022 at 09:00):

We have a g.withContext do block, but inside it we change g. That seems fishy.

Johan Commelin (Sep 15 2022 at 09:01):

Are we supposed to break this into new withContext do blocks every time the goal changes?

Mario Carneiro (Sep 15 2022 at 09:09):

only if the local context of the new metavariable is different from the old one

Johan Commelin (Sep 15 2022 at 09:10):

which is the case here, because we have an intro1P halfway that code block

Mario Carneiro (Sep 15 2022 at 09:10):

are you using expressions which refer to the newly introduced fvar?

Mario Carneiro (Sep 15 2022 at 09:11):

oh yes you are

Johan Commelin (Sep 15 2022 at 09:11):

indeed!

Johan Commelin (Sep 15 2022 at 09:11):

but the tactic still works :shock:

Mario Carneiro (Sep 15 2022 at 09:13):

it's not typechecking everything you give it unless it needs to

Johan Commelin (Sep 15 2022 at 09:14):

right, so it works, but what we do is really bad style. Is that a good summary?

Johan Commelin (Sep 15 2022 at 09:14):

Should we just nest the g.withContext dos?

Johan Commelin (Sep 15 2022 at 09:15):

The number of indentations quickly adds up...

Johan Commelin (Sep 15 2022 at 09:15):

What is the idiomatic way here?

Mario Carneiro (Sep 15 2022 at 09:15):

Only the part which is in the new context

Mario Carneiro (Sep 15 2022 at 09:16):

also, you can just not indent

Mario Carneiro (Sep 15 2022 at 09:16):

you will find those occasionally

Mario Carneiro (Sep 15 2022 at 09:18):

another thing you can do is to create let bindings with the tail of the program and call them inside the withContext. This does tend to turn the program upside down though

Johan Commelin (Sep 15 2022 at 09:21):

Mario Carneiro said:

Only the part which is in the new context

I tried nesting g.withContext do and I get a panic.

Mario Carneiro (Sep 15 2022 at 09:38):

that's definitely a misattribution of blame

Mario Carneiro (Sep 15 2022 at 09:38):

is this on a branch I can test?

Mario Carneiro (Sep 15 2022 at 09:41):

by the way your indentation of the match arms after the return ne_fail is cursed

Mario Carneiro (Sep 15 2022 at 10:00):

Aha, I see. When you are inside the forallTelescopeReducing callback, you have an extended local context containing the variables in ctxt. If you use g.withContext it will reset the context to the one for g, making the let spec_ty line fail because it makes reference to free variables from ctxt

Johan Commelin (Sep 15 2022 at 10:46):

Mario Carneiro said:

is this on a branch I can test?

yes, on choose

Mario Carneiro (Sep 15 2022 at 11:56):

@Johan Commelin @Reid Barton I pushed some stuff to the choose branch which should fix the issues

Johan Commelin (Sep 15 2022 at 12:23):

Thanks!!

Johan Commelin (Sep 15 2022 at 13:07):

Why do you need

  g.withContext do
    Elab.Term.addLocalVarInfo data fvar

Mario Carneiro (Sep 15 2022 at 13:11):

Try removing it. The tactic will still work, but the variable will not appear blue in the tactic application

Johan Commelin (Sep 15 2022 at 13:11):

wild

Mario Carneiro (Sep 15 2022 at 13:12):

it also handles go-to-definition queries for when you use the variable in a later expression

Johan Commelin (Sep 16 2022 at 07:54):

I think the port of choose is converging. But I'm stumped on some final bits. If an expert could look at the lines 100 - 120 of Choose.lean on the branch choose, that would be great.

Johan Commelin (Sep 16 2022 at 07:55):

I tried to extrapolate from Mario's changes yesterday. But I clearly didn't yet pick up all the tricks I need.

Johan Commelin (Sep 16 2022 at 20:00):

mathlib4#420 -- with many thanks to Mario and Reid!

Johan Commelin (Sep 17 2022 at 07:52):

https://github.com/leanprover-community/mathlib4/actions/runs/3072454842/jobs/4963956923 it fails at "check that all files are imported". But of course Tactic/Choose isn't imported anywhere. What should I do?

Alex J. Best (Sep 17 2022 at 11:28):

You have to add all the files you added to Mathlib.lean

Alex J. Best (Sep 17 2022 at 11:29):

You could even use the diff in that actions log, or do it manually

Johan Commelin (Sep 17 2022 at 12:40):

Aha, I see.

Johan Commelin (Sep 17 2022 at 12:40):

But adding a transitive reduction is good enough, I guess?

Johan Commelin (Sep 17 2022 at 14:47):

Apparently not. I added all the files, and now CI is happy.

Last updated: Dec 20 2023 at 11:08 UTC