-
Notifications
You must be signed in to change notification settings - Fork 273
/
Zify.lean
116 lines (101 loc) · 4.47 KB
/
Zify.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
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
/-
Copyright (c) 2022 Moritz Doll. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Moritz Doll, Mario Carneiro, Robert Y. Lewis
-/
import Mathlib.Tactic.Basic
import Mathlib.Tactic.Attr.Register
import Mathlib.Data.Int.Cast.Basic
import Mathlib.Order.Basic
/-!
# `zify` tactic
The `zify` tactic is used to shift propositions from `Nat` to `Int`.
This is often useful since `Int` has well-behaved subtraction.
```
example (a b c x y z : Nat) (h : ¬ x*y*z < 0) : c < a + 3*b := by
zify
zify at h
/-
h : ¬↑x * ↑y * ↑z < 0
⊢ ↑c < ↑a + 3 * ↑b
-/
```
-/
namespace Mathlib.Tactic.Zify
open Lean
open Lean.Meta
open Lean.Parser.Tactic
open Lean.Elab.Tactic
/--
The `zify` tactic is used to shift propositions from `Nat` to `Int`.
This is often useful since `Int` has well-behaved subtraction.
```
example (a b c x y z : Nat) (h : ¬ x*y*z < 0) : c < a + 3*b := by
zify
zify at h
/-
h : ¬↑x * ↑y * ↑z < 0
⊢ ↑c < ↑a + 3 * ↑b
-/
```
`zify` can be given extra lemmas to use in simplification. This is especially useful in the
presence of nat subtraction: passing `≤` arguments will allow `push_cast` to do more work.
```
example (a b c : Nat) (h : a - b < c) (hab : b ≤ a) : false := by
zify [hab] at h
/- h : ↑a - ↑b < ↑c -/
```
`zify` makes use of the `@[zify_simps]` attribute to move propositions,
and the `push_cast` tactic to simplify the `Int`-valued expressions.
`zify` is in some sense dual to the `lift` tactic.
`lift (z : Int) to Nat` will change the type of an
integer `z` (in the supertype) to `Nat` (the subtype), given a proof that `z ≥ 0`;
propositions concerning `z` will still be over `Int`.
`zify` changes propositions about `Nat` (the subtype) to propositions about `Int` (the supertype),
without changing the type of any variable.
-/
syntax (name := zify) "zify" (simpArgs)? (location)? : tactic
macro_rules
| `(tactic| zify $[[$simpArgs,*]]? $[at $location]?) =>
let args := simpArgs.map (·.getElems) |>.getD #[]
`(tactic|
simp (config := {decide := false}) only [zify_simps, push_cast, $args,*] $[at $location]?)
/-- The `Simp.Context` generated by `zify`. -/
def mkZifyContext (simpArgs : Option (Syntax.TSepArray `Lean.Parser.Tactic.simpStar ",")) :
TacticM MkSimpContextResult := do
let args := simpArgs.map (·.getElems) |>.getD #[]
mkSimpContext
(← `(tactic| simp (config := {decide := false}) only [zify_simps, push_cast, $args,*])) false
/-- A variant of `applySimpResultToProp` that cannot close the goal, but does not need a meta
variable and returns a tuple of a proof and the corresponding simplified proposition. -/
def applySimpResultToProp' (proof : Expr) (prop : Expr) (r : Simp.Result) : MetaM (Expr × Expr) :=
do
match r.proof? with
| some eqProof => return (← mkExpectedTypeHint (← mkEqMP eqProof proof) r.expr, r.expr)
| none =>
if r.expr != prop then
return (← mkExpectedTypeHint proof r.expr, r.expr)
else
return (proof, r.expr)
/-- Translate a proof and the proposition into a zified form. -/
def zifyProof (simpArgs : Option (Syntax.TSepArray `Lean.Parser.Tactic.simpStar ","))
(proof : Expr) (prop : Expr) : TacticM (Expr × Expr) := do
let ctx_result ← mkZifyContext simpArgs
let (r, _) ← simp prop ctx_result.ctx
applySimpResultToProp' proof prop r
@[zify_simps] lemma nat_cast_eq (a b : Nat) : a = b ↔ (a : Int) = (b : Int) := Int.ofNat_inj.symm
@[zify_simps] lemma nat_cast_le (a b : Nat) : a ≤ b ↔ (a : Int) ≤ (b : Int) := Int.ofNat_le.symm
@[zify_simps] lemma nat_cast_lt (a b : Nat) : a < b ↔ (a : Int) < (b : Int) := Int.ofNat_lt.symm
@[zify_simps] lemma nat_cast_ne (a b : Nat) : a ≠ b ↔ (a : Int) ≠ (b : Int) :=
not_congr Int.ofNat_inj.symm
@[zify_simps] lemma nat_cast_dvd (a b : Nat) : a ∣ b ↔ (a : Int) ∣ (b : Int) := Int.ofNat_dvd.symm
-- TODO: is it worth adding lemmas for Prime and Coprime as well?
-- Doing so in this file would require adding imports.
-- `Nat.cast_sub` is already tagged as `norm_cast` but it does allow to use assumptions like
-- `m < n` or more generally `m + k ≤ n`. We add two lemmas to increase the probability that
-- `zify` will push through `ℕ` subtraction.
variable {R : Type*} [AddGroupWithOne R]
@[norm_cast] theorem Nat.cast_sub_of_add_le {m n k} (h : m + k ≤ n) :
((n - m : ℕ) : R) = n - m := Nat.cast_sub (m.le_add_right k |>.trans h)
@[norm_cast] theorem Nat.cast_sub_of_lt {m n} (h : m < n) :
((n - m : ℕ) : R) = n - m := Nat.cast_sub h.le