-
Notifications
You must be signed in to change notification settings - Fork 335
/
FalseOrByContra.lean
66 lines (58 loc) · 2.47 KB
/
FalseOrByContra.lean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
/-
Copyright (c) 2023 Lean FRO, LLC. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Scott Morrison
-/
prelude
import Lean.Elab.Tactic.Basic
import Lean.Meta.Tactic.Apply
import Lean.Meta.Tactic.Intro
/-!
# `false_or_by_contra` tactic
Changes the goal to `False`, retaining as much information as possible:
* If the goal is `False`, do nothing.
* If the goal is an implication or a function type, introduce the argument and restart.
(In particular, if the goal is `x ≠ y`, introduce `x = y`.)
* Otherwise, for a propositional goal `P`, replace it with `¬ ¬ P`
(attempting to find a `Decidable` instance, but otherwise falling back to working classically)
and introduce `¬ P`.
* For a non-propositional goal use `False.elim`.
-/
namespace Lean.MVarId
open Lean Meta Elab Tactic
@[inherit_doc Lean.Parser.Tactic.falseOrByContra]
-- When `useClassical` is `none`, we try to find a `Decidable` instance when replacing `P` with `¬ ¬ P`,
-- but fall back to a classical instance. When it is `some true`, we always use the classical instance.
-- When it is `some false`, if there is no `Decidable` instance we don't introduce the double negation,
-- and fall back to `False.elim`.
partial def falseOrByContra (g : MVarId) (useClassical : Option Bool := none) : MetaM MVarId := do
let ty ← whnfR (← g.getType)
match ty with
| .const ``False _ => pure g
| .forallE _ _ _ _
| .app (.const ``Not _) _ =>
-- We set the transparency back to default; otherwise this breaks when run by a `simp` discharger.
falseOrByContra (← withTransparency default g.intro1P).2 useClassical
| _ =>
let gs ← if ← isProp ty then
match useClassical with
| some true => some <$> g.applyConst ``Classical.byContradiction
| some false =>
try some <$> g.applyConst ``Decidable.byContradiction
catch _ => pure none
| none =>
try some <$> g.applyConst ``Decidable.byContradiction
catch _ => some <$> g.applyConst ``Classical.byContradiction
else
pure none
if let some gs := gs then
let [g] := gs | panic! "expected one subgoal"
pure (← g.intro1).2
else
let [g] ← g.applyConst ``False.elim | panic! "expected one sugoal"
pure g
@[builtin_tactic Lean.Parser.Tactic.falseOrByContra]
def elabFalseOrByContra : Tactic
| `(tactic| false_or_by_contra) => do liftMetaTactic1 (falseOrByContra ·)
| _ => no_error_if_unused% throwUnsupportedSyntax
end Lean.MVarId