Lean4
/-- Elaborator for the `nontriviality` tactic. -/
@[tactic nontriviality]
def elabNontriviality : Tactic := fun stx => do
let g ← getMainGoal
let α ←
match stx[1].getOptional? with
| some e =>
Term.elabType e
| none =>
(do
let mut tgt ← withReducible g.getType'
if let some tgt' := tgt.not? then
tgt ← withReducible (whnf tgt')
if let some (α, _) := tgt.eq? then
return α
if let some (α, _) := tgt.app4? ``LE.le then
return α
if let some (α, _) := tgt.app4? ``LT.lt then
return α
throwError "The goal is not an (in)equality, so you'll need to specify the desired \
`Nontrivial α` instance by invoking `nontriviality α`.")
let .sort u ← whnf (← inferType α) |
unreachable!
let some v := u.dec |
throwError "not a type{indentExpr α}"
let α : Q(Type v) := α
let tac := do
let ty := q(Nontrivial $α)
let m ← mkFreshExprMVar (some ty)
nontrivialityByAssumption m.mvarId!
g.assert `inst ty m
let g ← liftM <| tac <|> nontrivialityByElim α g stx[2][1].getSepArgs
replaceMainGoal [(← g.intro1).2]
