-
Notifications
You must be signed in to change notification settings - Fork 546
/
Copy path1234.lean
78 lines (72 loc) · 2.68 KB
/
1234.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
theorem le_of_not_lt {a b : Nat} (_: ¬ a < b): b ≤ a := sorry
theorem lt_of_succ_lt (_: a + 1 < b): a < b := sorry
theorem succ_pred_eq_of_pos (_: 0 < v): v - 1 + 1 = v := sorry
set_option trace.Meta.Tactic.simp true
--set_option trace.Debug.Meta.Tactic.simp true
/--
info: [Meta.Tactic.simp.rewrite] h₁:1000, k ≤ v - 1 ==> True
[Meta.Tactic.simp.discharge] succ_pred_eq_of_pos discharge ✅️
0 < v
[Meta.Tactic.simp.rewrite] h₂:1000, 0 < v ==> True
[Meta.Tactic.simp.rewrite] succ_pred_eq_of_pos:1000, v - 1 + 1 ==> v
[Meta.Tactic.simp.rewrite] ite_true:1000, if True then ⟨v, ⋯⟩ else ⟨v - 1, ⋯⟩ ==> ⟨v, ⋯⟩
[Meta.Tactic.simp.rewrite] eq_self:1000, ⟨v, ⋯⟩ = ⟨v, ⋯⟩ ==> True
---
warning: declaration uses 'sorry'
-/
#guard_msgs in
example (h₁: k ≤ v - 1) (h₂: 0 < v):
(if k ≤ v - 1 then Fin.mk (v-1+1) sorry else Fin.mk (v-1) sorry) = Fin.mk v sorry (n:=n) := by
simp only [
h₁, h₂,
ite_true,
succ_pred_eq_of_pos
----------------
, le_of_not_lt
, lt_of_succ_lt
]
-- it works
/--
info: [Meta.Tactic.simp.rewrite] h₁:1000, k ≤ v - 1 ==> True
[Meta.Tactic.simp.discharge] succ_pred_eq_of_pos discharge ✅️
0 < v
[Meta.Tactic.simp.rewrite] h₂:1000, 0 < v ==> True
[Meta.Tactic.simp.rewrite] succ_pred_eq_of_pos:1000, v - 1 + 1 ==> v
[Meta.Tactic.simp.rewrite] ite_true:1000, if True then ⟨v, ⋯⟩ else ⟨v - 1, ⋯⟩ ==> ⟨v, ⋯⟩
[Meta.Tactic.simp.rewrite] eq_self:1000, ⟨v, ⋯⟩ = ⟨v, ⋯⟩ ==> True
---
warning: declaration uses 'sorry'
-/
#guard_msgs in
example (h₁: k ≤ v - 1) (h₂: 0 < v):
(if k ≤ v - 1 then Fin.mk (v-1+1) sorry else Fin.mk (v-1) sorry) = Fin.mk v sorry (n:=n) := by
simp (config := { memoize := false}) only [
h₁, h₂,
ite_true,
succ_pred_eq_of_pos
----------------
, le_of_not_lt
, lt_of_succ_lt
]
/--
info: [Meta.Tactic.simp.rewrite] h₁:1000, k ≤ v - 1 ==> True
[Meta.Tactic.simp.discharge] succ_pred_eq_of_pos discharge ✅️
0 < v
[Meta.Tactic.simp.rewrite] h₂:1000, 0 < v ==> True
[Meta.Tactic.simp.rewrite] succ_pred_eq_of_pos:1000, v - 1 + 1 ==> v
[Meta.Tactic.simp.rewrite] ite_true:1000, if True then ⟨v, ⋯⟩ else ⟨v - 1, ⋯⟩ ==> ⟨v, ⋯⟩
[Meta.Tactic.simp.rewrite] eq_self:1000, ⟨v, ⋯⟩ = ⟨v, ⋯⟩ ==> True
---
warning: declaration uses 'sorry'
-/
#guard_msgs in
example (h₁: k ≤ v - 1) (h₂: 0 < v):
(if k ≤ v - 1 then Fin.mk (v-1+1) sorry else Fin.mk (v-1) sorry) = Fin.mk v sorry (n:=n) := by
simp only [
h₁, h₂,
ite_true,
succ_pred_eq_of_pos
----------------
--, le_of_not_lt
--, lt_of_succ_lt
]