Lean4
/-- Changes `(h : ∀ xs, ∃ a:α, p a) ⊢ g` to `(d : ∀ xs, a) ⊢ (s : ∀ xs, p (d xs)) → g` and
`(h : ∀ xs, p xs ∧ q xs) ⊢ g` to `(d : ∀ xs, p xs) ⊢ (s : ∀ xs, q xs) → g`.
`choose1` returns a tuple of
- the error result (see `ElimStatus`)
- the data new free variable that was "chosen"
- the new goal (which contains the spec of the data as domain of an arrow type)
If `nondep` is true and `α` is inhabited, then it will remove the dependency of `d` on
all propositional assumptions in `xs`. For example if `ys` are propositions then
`(h : ∀ xs ys, ∃ a:α, p a) ⊢ g` becomes `(d : ∀ xs, a) (s : ∀ xs ys, p (d xs)) ⊢ g`. -/
def choose1 (g : MVarId) (nondep : Bool) (h : Option Expr) (data : Name) : MetaM (ElimStatus × Expr × MVarId) := do
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 ctx t ↦ do
(← withTransparency .all (whnf t)).withApp fun
| .const ``Exists [u], #[α, p] => do
let data ← mkFreshNameFrom data ((← p.getBinderName).getD `h)
let ((neFail : ElimStatus), (nonemp : Option Expr)) ←
if nondep then
let ne := (Expr.const ``Nonempty [u]).app α
let m ← mkFreshExprMVar ne
let mut g' := m.mvarId!
for e in ctx do
if (← isProof e) then
continue
let ty ← whnf (← inferType e)
let nety := (Expr.const ``Nonempty [u]).app ty
let neval := mkApp2 (Expr.const ``Nonempty.intro [u]) ty e
g' ← g'.assert .anonymous nety neval
(_, g') ← g'.intros
g'.withContext
(do
match ← synthInstance? (← g'.getType) with
| some e =>
do
g'.assign e
let m ← instantiateMVars m
pure (.success, some m)
| none =>
pure (.failure [ne], none))
else
pure (.failure [], none)
let ctx' ←
if nonemp.isSome then
ctx.filterM (not <$> isProof ·)
else
pure ctx
let dataTy ← mkForallFVars ctx' α
let mut dataVal := mkApp3 (.const ``Classical.choose [u]) α p (mkAppN h ctx)
let mut specVal := mkApp3 (.const ``Classical.choose_spec [u]) α p (mkAppN h ctx)
if let some nonemp := nonemp then
(dataVal, specVal) ← mk_sometimes u α nonemp p ctx.toList (dataVal, specVal)
dataVal ← mkLambdaFVars ctx' dataVal
specVal ← mkLambdaFVars ctx specVal
let (fvar, g) ←
withLocalDeclD .anonymous dataTy fun d ↦ do
let specTy ← mkForallFVars ctx (p.app (mkAppN d ctx')).headBeta
g.withContext <|
withLocalDeclD data dataTy fun d' ↦ do
let mvarTy ← mkArrow (specTy.replaceFVar d d') (← g.getType)
let newMVar ← mkFreshExprSyntheticOpaqueMVar mvarTy (← g.getTag)
g.assign <| mkApp2 (← mkLambdaFVars #[d'] newMVar) dataVal specVal
pure (d', newMVar.mvarId!)
let g ←
match h with
| .fvar v =>
g.clear v
| _ =>
pure g
return (neFail, fvar, g)
| .const ``And _, #[p, q] => do
let data ← mkFreshNameFrom data `h
let e1 ← mkLambdaFVars ctx <| mkApp3 (.const ``And.left []) p q (mkAppN h ctx)
let e2 ← mkLambdaFVars ctx <| mkApp3 (.const ``And.right []) p q (mkAppN h ctx)
let t1 ← inferType e1
let t2 ← inferType e2
let (fvar, g) ← (← (← g.assert .anonymous t2 e2).assert data t1 e1).intro1P
let g ←
match h with
| .fvar v =>
g.clear v
| _ =>
pure g
return
(.success, .fvar fvar, g)
-- TODO: support Σ, ×, or even any inductive type with 1 constructor ?
| _, _ => throwError"expected a term of the shape `∀ xs, ∃ a, p xs a` or `∀ xs, p xs ∧ q xs`"
