max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

refactor(frontends/lean/tactic_notation): rename note/define tactics to have/let

Browse source
This commit is contained in:
Sebastian Ullrich 2017-06-21 16:14:04 +02:00 • committed by Leonardo de Moura
parent 495093f6c0
commit 0a48809469
43 changed files with 219 additions and 201 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
library/data/bitvec.lean
View file

@ -42,9 +42,9 @@ section shift
bitvec.cong
begin
by_cases (i ≤ n),
{ note h₁ := sub_le n i,
{ have h₁ := sub_le n i,
rw [min_eq_right h], rw [min_eq_left h₁, -nat.add_sub_assoc h, add_comm, nat.add_sub_cancel] },
{ note h₁ := le_of_not_ge h,
{ have h₁ := le_of_not_ge h,
rw [min_eq_left h₁, sub_eq_zero_of_le h₁, min_zero_left, add_zero] }
end $
repeat fill (min n i) ++ₜ taken (n-i) x
@ -165,7 +165,7 @@ section conversion
simp [bits_to_nat_to_list], clear P,
unfold bits_to_nat list.foldl,
-- the next 4 lines generalize the accumulator of foldl
define x := 0,
let x := 0,
change _ = add_lsb x b + _,
generalize 0 y,
revert x, simp,
@ -192,7 +192,7 @@ section conversion
revert n,
induction k with k ; intro n,
{ unfold pow, simp [nat.mod_one], refl },
{ note h : 0 < 2, { apply le_succ },
{ have h : 0 < 2, { apply le_succ },
rw [ of_nat_succ
, to_nat_append
, ih_1

2
library/data/dlist.lean
View file

@ -68,7 +68,7 @@ by cases l; simp
lemma of_list_to_list (l : dlist α) : of_list (to_list l) = l :=
begin
cases l with xs,
note h : append (xs []) = xs,
have h : append (xs []) = xs,
{intros, apply funext, intros x, simp [invariant x]},
simp [h]
end

30
library/data/hash_map.lean
View file

@ -41,7 +41,7 @@ begin
intros,
induction j with j IH,
exact ⟨false.elim, λ⟨i, h, _⟩, absurd h (nat.not_lt_zero _)⟩,
note IH := IH (le_of_lt h),
have IH := IH (le_of_lt h),
simp[array.iterate_aux],
exact ⟨λo, or.elim o
(λm, ⟨⟨j, h⟩, nat.le_refl _, m⟩)
@ -165,10 +165,10 @@ have h1 : list.length (array.to_list bkts) - 1 - i < list.length (list.reverse (
have sigma.mk a b ∈ list.nth_le (array.to_list bkts) i (by simph[array.to_list_length]), by {rw array.to_list_nth, exact el},
begin
rw -list.nth_le_reverse at this,
note v : valid_aux (λa, (mk_idx n (hash_fn a)).1) (array.to_list bkts).reverse sz,
have v : valid_aux (λa, (mk_idx n (hash_fn a)).1) (array.to_list bkts).reverse sz,
rw array.to_list_reverse,
exact v,
note mm := @_root_.hash_map.valid_aux.eq _ _ _ _ _ _ v -- TODO (Mario): Why is explicit namespacing needed here?
have mm := @_root_.hash_map.valid_aux.eq _ _ _ _ _ _ v -- TODO (Mario): Why is explicit namespacing needed here?
(list.length (array.to_list bkts) - 1 - i) h1 a b this,
rwa [list.length_reverse, array.to_list_length, nat.sub_sub_self (show i ≤ n.1 - 1, from nat.pred_le_pred h)] at mm
end
@ -190,7 +190,7 @@ begin
let ⟨⟨a', b⟩, m1, e1⟩ := list.exists_of_mem_map m1 in
let ⟨⟨a'', b'⟩, m2, e2⟩ := list.exists_of_mem_map m2 in
match a', a'', b, b', m1, m2, e1, e2 with ._, ._, b, b', m1, m2, rfl, rfl :=
by {note hlt := al _ m1, rw v.eq _ m2 at hlt, exact lt_irrefl _ hlt}
by {have hlt := al _ m1, rw v.eq _ m2 at hlt, exact lt_irrefl _ hlt}
end,
λ⟨a, b⟩ m, or.elim m
(λm2, by rw v.eq _ m2; exact nat.le_refl _)
@ -200,7 +200,7 @@ end
theorem valid.as_list_length {n} {bkts : bucket_array α β n} {sz : nat} (v : valid bkts sz) : bkts.as_list.length = sz :=
have ∀l sz, valid_aux (λ (a : α), (mk_idx n (hash_fn a)).val) l sz → ∀t, (l.foldr (λbkt r, r ++ bkt) t).length = sz + t.length,
by {intros, induction a, simp[list.foldr], simp[list.foldr, ih_1]},
by note h := this _ _ v []; rwa -array.foldl_eq at h
by have h := this _ _ v []; rwa -array.foldl_eq at h
theorem valid.mk (n : ℕ+) : @valid n (mk_array n.1 []) 0 :=
let bkts : bucket_array α β n := mk_array n.1 [] in
@ -321,10 +321,10 @@ section
have nd' : ((u ++ v2 ++ w).map sigma.fst).nodup, begin
rw [list.map_append, list.map_append] at nd,
rw [list.map_append, list.map_append],
note ndu : (u.map sigma.fst).nodup := list.nodup_of_nodup_append_left (list.nodup_of_nodup_append_left nd),
note ndv1 : (v1.map sigma.fst).nodup := list.nodup_of_nodup_append_right (list.nodup_of_nodup_append_left nd),
note ndw : (w.map sigma.fst).nodup := list.nodup_of_nodup_append_right nd,
note djuw : (u.map sigma.fst).disjoint (w.map sigma.fst) :=
have ndu : (u.map sigma.fst).nodup := list.nodup_of_nodup_append_left (list.nodup_of_nodup_append_left nd),
have ndv1 : (v1.map sigma.fst).nodup := list.nodup_of_nodup_append_right (list.nodup_of_nodup_append_left nd),
have ndw : (w.map sigma.fst).nodup := list.nodup_of_nodup_append_right nd,
have djuw : (u.map sigma.fst).disjoint (w.map sigma.fst) :=
list.disjoint_of_disjoint_append_left_left (list.disjoint_of_nodup_append nd),
exact list.nodup_append_of_nodup_of_nodup_of_disjoint
(list.nodup_append_of_nodup_of_nodup_of_disjoint ndu hvnd djuv)
@ -487,7 +487,7 @@ suffices ∀ (l : list Σ a, β a),
∀ (t : bucket_array α β n') sz, valid hash_fn t sz → ((l ++ t.as_list).map sigma.fst).nodup →
valid hash_fn (l.foldl (λr (a : Σ a, β a), reinsert_aux hash_fn r a.1 a.2) t) (sz + l.length),
begin
note p := this bkts.as_list _ _ (valid.mk _ _),
have p := this bkts.as_list _ _ (valid.mk _ _),
rw [mk_as_list hash_fn, list.append_nil, zero_add, v.as_list_length _] at p,
rw bucket_array.foldl_eq,
exact p (v.as_list_nodup _),
@ -498,13 +498,13 @@ end,
intros t sz v nd,
rw (show sz + (c :: l).length = sz + 1 + l.length, by simp),
simp at nd,
note nc := list.not_mem_of_nodup_cons nd,
note v' := v.insert _ _ c.2
have nc := list.not_mem_of_nodup_cons nd,
have v' := v.insert _ _ c.2
(λHc, nc $ list.mem_append_right _ $
(v.contains_aux_iff _ c.1).1 Hc),
apply IH _ _ v',
simp,
note nd' := list.nodup_of_nodup_cons nd,
have nd' := list.nodup_of_nodup_cons nd,
apply list.nodup_append_of_nodup_of_nodup_of_disjoint
(list.nodup_of_nodup_append_left nd')
(v'.as_list_nodup _),
@ -576,7 +576,7 @@ if h : a = a' then by simp[h]; exact
have bkts.as_list.map sigma.fst = u.map sigma.fst ++ w.map sigma.fst, by simp [hl],
by rw this at na; exact na
| ._, or.inr ⟨b'', rfl⟩, hl := by {
note nd' := v.as_list_nodup _,
have nd' := v.as_list_nodup _,
rw hl at nd', simp at nd',
exact list.not_mem_of_nodup_cons (list.nodup_head nd') }
end,
@ -681,7 +681,7 @@ match (by apply_instance : decidable (contains_aux a bkt)) with
| ._, ._, ⟨u, w, rfl, rfl⟩, nd' := by simp; simp at nd'; exact
⟨λhm, ⟨λe, match a', e, b', hm with ._, rfl, b', hm := by {
rw -list.mem_append_iff at hm;
note hm := list.mem_map sigma.fst hm;
have hm := list.mem_map sigma.fst hm;
rw list.map_append at hm;
exact list.not_mem_of_nodup_cons (list.nodup_head nd') hm }
end, or.inr hm⟩,

4
library/data/stream.lean
View file

@ -482,8 +482,8 @@ lemma take_lemma (s₁ s₂ : stream α) : (∀ (n : nat), approx n s₁ = appro
begin
intro h, apply stream.ext, intro n,
induction n with n ih,
{ note aux := h 1, unfold approx at aux, injection aux },
{ note h₁ : some (nth (succ n) s₁) = some (nth (succ n) s₂),
{ have aux := h 1, unfold approx at aux, injection aux },
{ have h₁ : some (nth (succ n) s₁) = some (nth (succ n) s₂),
{ rw [-nth_approx, -nth_approx, h (succ (succ n))] },
injection h₁ }
end

4
library/init/algebra/functions.lean
View file

@ -299,14 +299,14 @@ or.elim (le_total b 0)
assume h4 : a < 0,
have h5 : a + b < 0,
begin
note aux := add_lt_add_of_lt_of_le h4 h2,
have aux := add_lt_add_of_lt_of_le h4 h2,
rwa [add_zero] at aux
end,
not_lt_of_ge h1 h5,
aux1 h1 (le_of_not_gt h3))
(assume h2 : 0 ≤ b,
begin
note h3 : abs (b + a) ≤ abs b + abs a,
have h3 : abs (b + a) ≤ abs b + abs a,
begin
rw add_comm at h1,
exact aux1 h1 h2

2
library/init/algebra/norm_num.lean
View file

@ -113,7 +113,7 @@ by rw [-h, mul_div_assoc]
lemma nonzero_of_div_helper [field α] (a b : α) (ha : a ≠ 0) (hb : b ≠ 0) : a / b ≠ 0 :=
begin
intro hab,
note habb : (a / b) * b = 0, rw [hab, zero_mul],
have habb : (a / b) * b = 0, rw [hab, zero_mul],
rw [div_mul_cancel _ hb] at habb,
exact ha habb
end

10
library/init/algebra/ordered_field.lean
View file

@ -329,8 +329,8 @@ calc
lemma div_mul_le_div_mul_of_div_le_div_pos {a b c d e : α} (hb : b ≠ 0) (hd : d ≠ 0) (h : a / b ≤ c / d)
(he : e > 0) : a / (b * e) ≤ c / (d * e) :=
begin
note h₁ := field.div_mul_eq_div_mul_one_div a hb (ne_of_gt he),
note h₂ := field.div_mul_eq_div_mul_one_div c hd (ne_of_gt he),
have h₁ := field.div_mul_eq_div_mul_one_div a hb (ne_of_gt he),
have h₂ := field.div_mul_eq_div_mul_one_div c hd (ne_of_gt he),
rw [h₁, h₂],
apply mul_le_mul_of_nonneg_right h,
apply le_of_lt,
@ -341,13 +341,13 @@ lemma exists_add_lt_and_pos_of_lt {a b : α} (h : b < a) : ∃ c : α, b + c < a
begin
apply exists.intro ((a - b) / (1 + 1)),
split,
{note h2 : a + a > (b + b) + (a - b),
{have h2 : a + a > (b + b) + (a - b),
calc
a + a > b + a : add_lt_add_right h _
... = b + a + b - b : by rw add_sub_cancel
... = b + b + a - b : by simp
... = (b + b) + (a - b) : by rw add_sub,
note h3 : (a + a) / 2 > ((b + b) + (a - b)) / 2,
have h3 : (a + a) / 2 > ((b + b) + (a - b)) / 2,
exact div_lt_div_of_lt_of_pos h2 two_pos,
rw [one_add_one_eq_two, sub_eq_add_neg],
rw [add_self_div_two, -div_add_div_same, add_self_div_two, sub_eq_add_neg] at h3,
@ -360,7 +360,7 @@ begin
apply le_of_not_gt,
intro hb,
cases exists_add_lt_and_pos_of_lt hb with c hc,
note hc' := h c (and.right hc),
have hc' := h c (and.right hc),
apply (not_le_of_gt (and.left hc)) (le_add_of_sub_right_le hc')
end

76
library/init/algebra/ordered_group.lean
View file

@ -262,145 +262,145 @@ by rwa neg_zero at this
lemma le_neg_of_le_neg {a b : α} (h : a ≤ -b) : b ≤ -a :=
begin
note h := neg_le_neg h,
have h := neg_le_neg h,
rwa neg_neg at h
end
lemma neg_le_of_neg_le {a b : α} (h : -a ≤ b) : -b ≤ a :=
begin
note h := neg_le_neg h,
have h := neg_le_neg h,
rwa neg_neg at h
end
lemma lt_neg_of_lt_neg {a b : α} (h : a < -b) : b < -a :=
begin
note h := neg_lt_neg h,
have h := neg_lt_neg h,
rwa neg_neg at h
end
lemma neg_lt_of_neg_lt {a b : α} (h : -a < b) : -b < a :=
begin
note h := neg_lt_neg h,
have h := neg_lt_neg h,
rwa neg_neg at h
end
lemma sub_nonneg_of_le {a b : α} (h : b ≤ a) : 0 ≤ a - b :=
begin
note h := add_le_add_right h (-b),
have h := add_le_add_right h (-b),
rwa add_right_neg at h
end
lemma le_of_sub_nonneg {a b : α} (h : 0 ≤ a - b) : b ≤ a :=
begin
note h := add_le_add_right h b,
have h := add_le_add_right h b,
rwa [sub_add_cancel, zero_add] at h
end
lemma sub_nonpos_of_le {a b : α} (h : a ≤ b) : a - b ≤ 0 :=
begin
note h := add_le_add_right h (-b),
have h := add_le_add_right h (-b),
rwa add_right_neg at h
end
lemma le_of_sub_nonpos {a b : α} (h : a - b ≤ 0) : a ≤ b :=
begin
note h := add_le_add_right h b,
have h := add_le_add_right h b,
rwa [sub_add_cancel, zero_add] at h
end
lemma sub_pos_of_lt {a b : α} (h : b < a) : 0 < a - b :=
begin
note h := add_lt_add_right h (-b),
have h := add_lt_add_right h (-b),
rwa add_right_neg at h
end
lemma lt_of_sub_pos {a b : α} (h : 0 < a - b) : b < a :=
begin
note h := add_lt_add_right h b,
have h := add_lt_add_right h b,
rwa [sub_add_cancel, zero_add] at h
end
lemma sub_neg_of_lt {a b : α} (h : a < b) : a - b < 0 :=
begin
note h := add_lt_add_right h (-b),
have h := add_lt_add_right h (-b),
rwa add_right_neg at h
end
lemma lt_of_sub_neg {a b : α} (h : a - b < 0) : a < b :=
begin
note h := add_lt_add_right h b,
have h := add_lt_add_right h b,
rwa [sub_add_cancel, zero_add] at h
end
lemma add_le_of_le_neg_add {a b c : α} (h : b ≤ -a + c) : a + b ≤ c :=
begin
note h := add_le_add_left h a,
have h := add_le_add_left h a,
rwa add_neg_cancel_left at h
end
lemma le_neg_add_of_add_le {a b c : α} (h : a + b ≤ c) : b ≤ -a + c :=
begin
note h := add_le_add_left h (-a),
have h := add_le_add_left h (-a),
rwa neg_add_cancel_left at h
end
lemma add_le_of_le_sub_left {a b c : α} (h : b ≤ c - a) : a + b ≤ c :=
begin
note h := add_le_add_left h a,
have h := add_le_add_left h a,
rwa [-add_sub_assoc, add_comm a c, add_sub_cancel] at h
end
lemma le_sub_left_of_add_le {a b c : α} (h : a + b ≤ c) : b ≤ c - a :=
begin
note h := add_le_add_right h (-a),
have h := add_le_add_right h (-a),
rwa [add_comm a b, add_neg_cancel_right] at h
end
lemma add_le_of_le_sub_right {a b c : α} (h : a ≤ c - b) : a + b ≤ c :=
begin
note h := add_le_add_right h b,
have h := add_le_add_right h b,
rwa sub_add_cancel at h
end
lemma le_sub_right_of_add_le {a b c : α} (h : a + b ≤ c) : a ≤ c - b :=
begin
note h := add_le_add_right h (-b),
have h := add_le_add_right h (-b),
rwa add_neg_cancel_right at h
end
lemma le_add_of_neg_add_le {a b c : α} (h : -b + a ≤ c) : a ≤ b + c :=
begin
note h := add_le_add_left h b,
have h := add_le_add_left h b,
rwa add_neg_cancel_left at h
end
lemma neg_add_le_of_le_add {a b c : α} (h : a ≤ b + c) : -b + a ≤ c :=
begin
note h := add_le_add_left h (-b),
have h := add_le_add_left h (-b),
rwa neg_add_cancel_left at h
end
lemma le_add_of_sub_left_le {a b c : α} (h : a - b ≤ c) : a ≤ b + c :=
begin
note h := add_le_add_right h b,
have h := add_le_add_right h b,
rwa [sub_add_cancel, add_comm] at h
end
lemma sub_left_le_of_le_add {a b c : α} (h : a ≤ b + c) : a - b ≤ c :=
begin
note h := add_le_add_right h (-b),
have h := add_le_add_right h (-b),
rwa [add_comm b c, add_neg_cancel_right] at h
end
lemma le_add_of_sub_right_le {a b c : α} (h : a - c ≤ b) : a ≤ b + c :=
begin
note h := add_le_add_right h c,
have h := add_le_add_right h c,
rwa sub_add_cancel at h
end
lemma sub_right_le_of_le_add {a b c : α} (h : a ≤ b + c) : a - c ≤ b :=
begin
note h := add_le_add_right h (-c),
have h := add_le_add_right h (-c),
rwa add_neg_cancel_right at h
end
@ -433,7 +433,7 @@ le_add_of_neg_add_le_left (add_le_of_le_sub_right h)
lemma neg_le_sub_left_of_le_add {a b c : α} (h : c ≤ a + b) : -a ≤ b - c :=
begin
note h := le_neg_add_of_add_le (sub_left_le_of_le_add h),
have h := le_neg_add_of_add_le (sub_left_le_of_le_add h),
rwa add_comm at h
end
@ -457,73 +457,73 @@ add_le_add hab (neg_le_neg hcd)
lemma add_lt_of_lt_neg_add {a b c : α} (h : b < -a + c) : a + b < c :=
begin
note h := add_lt_add_left h a,
have h := add_lt_add_left h a,
rwa add_neg_cancel_left at h
end
lemma lt_neg_add_of_add_lt {a b c : α} (h : a + b < c) : b < -a + c :=
begin
note h := add_lt_add_left h (-a),
have h := add_lt_add_left h (-a),
rwa neg_add_cancel_left at h
end
lemma add_lt_of_lt_sub_left {a b c : α} (h : b < c - a) : a + b < c :=
begin
note h := add_lt_add_left h a,
have h := add_lt_add_left h a,
rwa [-add_sub_assoc, add_comm a c, add_sub_cancel] at h
end
lemma lt_sub_left_of_add_lt {a b c : α} (h : a + b < c) : b < c - a :=
begin
note h := add_lt_add_right h (-a),
have h := add_lt_add_right h (-a),
rwa [add_comm a b, add_neg_cancel_right] at h
end
lemma add_lt_of_lt_sub_right {a b c : α} (h : a < c - b) : a + b < c :=
begin
note h := add_lt_add_right h b,
have h := add_lt_add_right h b,
rwa sub_add_cancel at h
end
lemma lt_sub_right_of_add_lt {a b c : α} (h : a + b < c) : a < c - b :=
begin
note h := add_lt_add_right h (-b),
have h := add_lt_add_right h (-b),
rwa add_neg_cancel_right at h
end
lemma lt_add_of_neg_add_lt {a b c : α} (h : -b + a < c) : a < b + c :=
begin
note h := add_lt_add_left h b,
have h := add_lt_add_left h b,
rwa add_neg_cancel_left at h
end
lemma neg_add_lt_of_lt_add {a b c : α} (h : a < b + c) : -b + a < c :=
begin
note h := add_lt_add_left h (-b),
have h := add_lt_add_left h (-b),
rwa neg_add_cancel_left at h
end
lemma lt_add_of_sub_left_lt {a b c : α} (h : a - b < c) : a < b + c :=
begin
note h := add_lt_add_right h b,
have h := add_lt_add_right h b,
rwa [sub_add_cancel, add_comm] at h
end
lemma sub_left_lt_of_lt_add {a b c : α} (h : a < b + c) : a - b < c :=
begin
note h := add_lt_add_right h (-b),
have h := add_lt_add_right h (-b),
rwa [add_comm b c, add_neg_cancel_right] at h
end
lemma lt_add_of_sub_right_lt {a b c : α} (h : a - c < b) : a < b + c :=
begin
note h := add_lt_add_right h c,
have h := add_lt_add_right h c,
rwa sub_add_cancel at h
end
lemma sub_right_lt_of_lt_add {a b c : α} (h : a < b + c) : a - c < b :=
begin
note h := add_lt_add_right h (-c),
have h := add_lt_add_right h (-c),
rwa add_neg_cancel_right at h
end
@ -556,7 +556,7 @@ lt_add_of_neg_add_lt_left (add_lt_of_lt_sub_right h)
lemma neg_lt_sub_left_of_lt_add {a b c : α} (h : c < a + b) : -a < b - c :=
begin
note h := lt_neg_add_of_add_lt (sub_left_lt_of_lt_add h),
have h := lt_neg_add_of_add_lt (sub_left_lt_of_lt_add h),
rwa add_comm at h
end

2
library/init/algebra/ordered_ring.lean
View file

@ -313,7 +313,7 @@ lt_of_mul_lt_mul_left h3 nhc
lemma zero_gt_neg_one : -1 < (0:α) :=
begin
note this := neg_lt_neg (@zero_lt_one α _),
have this := neg_lt_neg (@zero_lt_one α _),
rwa neg_zero at this
end

2
library/init/category/state.lean
View file

@ -69,7 +69,7 @@ instance (σ : Type u) (m : Type u → Type v) [monad m] : monad (state_t σ m)
id_map := begin
intros, apply funext, intro,
simp [state_t_bind, state_t_return, function.comp, return],
note h : state_t_bind._match_1 (λ (x : α) (s : σ), @pure m _ _ (x, s)) = pure,
have h : state_t_bind._match_1 (λ (x : α) (s : σ), @pure m _ _ (x, s)) = pure,
{ apply funext, intro s, cases s, apply rfl },
{ rw h, apply @monad.bind_pure _ σ },
end,

2
library/init/data/array/lemmas.lean
View file

@ -55,7 +55,7 @@ theorem mem_iff_rev_list_mem_core (a : array α n) (v : α) : Π i (h : i ≤ n)
| (i+1) h := let IH := mem_iff_rev_list_mem_core i (le_of_lt h) in
⟨λ⟨j, ji1, e⟩, or.elim (lt_or_eq_of_le $ nat.le_of_succ_le_succ ji1)
(λji, list.mem_cons_of_mem _ $ IH.1 ⟨j, ji, e⟩)
(λje, by simp[iterate_aux]; apply or.inl; note H : j = ⟨i, h⟩ := fin.eq_of_veq je; rwa [-H, e]),
(λje, by simp[iterate_aux]; apply or.inl; have H : j = ⟨i, h⟩ := fin.eq_of_veq je; rwa [-H, e]),
λm, begin
simp[iterate_aux, list.mem] at m,
cases m with e m',

2
library/init/data/char/lemmas.lean
View file

@ -18,7 +18,7 @@ begin
unfold of_nat,
cases (nat.decidable_lt n char_sz),
{reflexivity},
{note h' := not_lt_of_ge h, contradiction}
{have h' := not_lt_of_ge h, contradiction}
end
lemma of_nat_eq_of_ge {n : nat} : n ≥ char_sz → of_nat n = of_nat 0 :=

6
library/init/data/fin/ops.lean
View file

@ -38,7 +38,7 @@ private lemma modlt {a b n : nat} (h₁ : a < n) (h₂ : b < n) : a % b < n :=
begin
cases b with b,
{simp [mod_zero], assumption},
{note h : a % (succ b) < succ b,
{have h : a % (succ b) < succ b,
apply nat.mod_lt _ (nat.zero_lt_succ _),
exact lt.trans h h₂}
end
@ -110,8 +110,8 @@ lemma val_zero : (0 : fin (succ n)).val = 0 := rfl
def pred {n : nat} : ∀ i : fin (succ n), i ≠ 0 → fin n
| ⟨a, h₁⟩ h₂ := ⟨a.pred,
begin
note this : a ≠ 0,
{ note aux₁ := vne_of_ne h₂,
have this : a ≠ 0,
{ have aux₁ := vne_of_ne h₂,
dsimp at aux₁, rw val_zero at aux₁, exact aux₁ },
exact nat.pred_lt_pred this (nat.succ_ne_zero n) h₁
end⟩

4
library/init/data/int/basic.lean
View file

@ -130,14 +130,14 @@ lemma sub_nat_nat_elim (m n : ℕ) (P : ℕ → ℕ → ℤ → Prop)
(hn : ∀i m, P m (m + i + 1) (-[1+ i])) :
P m n (sub_nat_nat m n) :=
begin
note H : ∀k, n - m = k → P m n (nat.cases_on k (of_nat (m - n)) (λa, -[1+ a])),
have H : ∀k, n - m = k → P m n (nat.cases_on k (of_nat (m - n)) (λa, -[1+ a])),
{ intro k, cases k,
{ intro e,
cases (nat.le.dest (nat.le_of_sub_eq_zero e)) with k h,
rw [h.symm, nat.add_sub_cancel_left],
apply hp },
{ intro heq,
note h : m ≤ n,
have h : m ≤ n,
{ exact nat.le_of_lt (nat.lt_of_sub_eq_succ heq) },
rw [nat.sub_eq_iff_eq_add h] at heq,
rw [heq, add_comm],

2
library/init/data/int/order.lean
View file

@ -75,7 +75,7 @@ lemma coe_zero_le (n : ℕ) : 0 ≤ (↑n : ℤ) :=
coe_nat_le_coe_nat_of_le n.zero_le
lemma eq_coe_of_zero_le {a : ℤ} (h : 0 ≤ a) : ∃ n : ℕ, a = n :=
by note t := le.dest_sub h; simp at t; exact t
by have t := le.dest_sub h; simp at t; exact t
lemma lt_add_succ (a : ℤ) (n : ℕ) : a < a + ↑(nat.succ n) :=
le.intro (show a + 1 + n = a + nat.succ n, begin simp [int.coe_nat_eq], reflexivity end)

16
library/init/data/list/lemmas.lean
View file

@ -146,9 +146,9 @@ theorem nth_ge_len : Π (l : list α) (n), n ≥ length l → nth l n = none
theorem ext : Π {l₁ l₂ : list α}, (∀n, nth l₁ n = nth l₂ n) → l₁ = l₂
| [] [] h := rfl
| (a::l₁) [] h := by note h0 := h 0; contradiction
| [] (a'::l₂) h := by note h0 := h 0; contradiction
| (a::l₁) (a'::l₂) h := by note h0 : some a = some a' := h 0; injection h0 with aa; simph[ext $ λn, h (n+1)]
| (a::l₁) [] h := by have h0 := h 0; contradiction
| [] (a'::l₂) h := by have h0 := h 0; contradiction
| (a::l₁) (a'::l₂) h := by have h0 : some a = some a' := h 0; injection h0 with aa; simph[ext $ λn, h (n+1)]
theorem ext_le {l₁ l₂ : list α} (hl : length l₁ = length l₂) (h : ∀n h₁ h₂, nth_le l₁ n h₁ = nth_le l₂ n h₂) : l₁ = l₂ :=
ext $ λn, if h₁ : n < length l₁
@ -243,13 +243,13 @@ lemma nth_le_reverse_aux2 : Π (l r : list α) (i : nat) (h1) (h2),
nth_le (reverse_core l r) (length l - 1 - i) h1 = nth_le l i h2
| [] r i h1 h2 := absurd h2 (not_lt_zero _)
| (a :: l) r 0 h1 h2 := begin
note aux := nth_le_reverse_aux1 l (a :: r) 0,
have aux := nth_le_reverse_aux1 l (a :: r) 0,
rw zero_add at aux,
exact aux _ (zero_lt_succ _)
end
| (a :: l) r (i+1) h1 h2 := begin
note aux := nth_le_reverse_aux2 l (a :: r) i,
note heq := calc length (a :: l) - 1 - (i + 1)
have aux := nth_le_reverse_aux2 l (a :: r) i,
have heq := calc length (a :: l) - 1 - (i + 1)
= length l - (1 + i) : by rw add_comm; refl
... = length l - 1 - i : by rw nat.sub_sub,
rw -heq at aux,
@ -270,7 +270,7 @@ by {induction l; intros, contradiction, simph, reflexivity}
@[simp] lemma last_append {a : α} (l : list α) (h : l ++ [a] ≠ []) : last (l ++ [a]) h = a :=
begin
induction l with hd tl ih; rsimp,
note haux : tl ++ [a] ≠ [],
have haux : tl ++ [a] ≠ [],
{apply append_ne_nil_of_ne_nil_right, contradiction},
simph
end
@ -735,7 +735,7 @@ by simp [sublists]; exact
(sublist_of_cons_sublist sl) _ hs
end,
λsl, begin
note this : ∀ {a : α} {y t}, y ∈ t → y ∈ foldr (λ ys r, ys :: (a :: ys) :: r) nil t
have this : ∀ {a : α} {y t}, y ∈ t → y ∈ foldr (λ ys r, ys :: (a :: ys) :: r) nil t
∧ a :: y ∈ foldr (λ ys r, ys :: (a :: ys) :: r) nil t,
{ intros a y t yt, induction t with x t IH, exact absurd yt (not_mem_nil _),
simp, simp at yt, cases yt with yx yt,

4
library/init/data/nat/bitwise.lean
View file

@ -94,7 +94,7 @@ namespace nat
def binary_rec {C : nat → Sort u} (f : ∀ b n, C n → C (bit b n)) (z : C 0) : Π n, C n
| n := if n0 : n = 0 then by rw n0; exact z else let n' := shiftr n 1 in
have n' < n, from (div_lt_iff_lt_mul _ _ dec_trivial).2 $
by note := nat.mul_lt_mul_of_pos_left (dec_trivial : 1 < 2)
by have := nat.mul_lt_mul_of_pos_left (dec_trivial : 1 < 2)
(lt_of_le_of_ne (zero_le _) (ne.symm n0));
rwa mul_one at this,
by rw [-show bit (bodd n) n' = n, from bit_decomp n]; exact
@ -126,7 +126,7 @@ namespace nat
{ generalize (binary_rec._main._pack._proof_2 (bit b n)) e,
rw [bodd_bit, shiftr1_bit], intro e, refl },
{ generalize (binary_rec._main._pack._proof_1 (bit b n) b0) e,
note bf := bodd_bit b n, note n0 := shiftr1_bit b n,
have bf := bodd_bit b n, have n0 := shiftr1_bit b n,
rw b0 at bf n0, rw [-show ff = b, from bf, -show 0 = n, from n0], intro e,
exact h.symm },
end

38
library/init/data/nat/lemmas.lean
View file

@ -879,12 +879,12 @@ nat.strong_induction_on a $ λ n,
/- mod -/
lemma mod_def (x y : nat) : x % y = if 0 < y ∧ y ≤ x then (x - y) % y else x :=
by note h := mod_def_aux x y; rwa [dif_eq_if] at h
by have h := mod_def_aux x y; rwa [dif_eq_if] at h
lemma mod_zero (a : nat) : a % 0 = a :=
begin
rw mod_def,
note h : ¬ (0 < 0 ∧ 0 ≤ a),
have h : ¬ (0 < 0 ∧ 0 ≤ a),
simp [lt_irrefl],
simp [if_neg, h]
end
@ -892,7 +892,7 @@ end
lemma mod_eq_of_lt {a b : nat} (h : a < b) : a % b = a :=
begin
rw mod_def,
note h' : ¬(0 < b ∧ b ≤ a),
have h' : ¬(0 < b ∧ b ≤ a),
simp [not_le_of_gt h],
simp [if_neg, h']
end
@ -900,7 +900,7 @@ end
@[simp] lemma zero_mod (b : nat) : 0 % b = 0 :=
begin
rw mod_def,
note h : ¬(0 < b ∧ b ≤ 0),
have h : ¬(0 < b ∧ b ≤ 0),
{intro hn, cases hn with l r, exact absurd (lt_of_lt_of_le l r) (lt_irrefl 0)},
simp [if_neg, h]
end
@ -917,9 +917,9 @@ begin
{apply or.elim (decidable.em (succ x < y)),
{intro h₁, rwa [mod_eq_of_lt h₁]},
{intro h₁,
note h₁ : succ x % y = (succ x - y) % y, {exact mod_eq_sub_mod (le_of_not_gt h₁)},
note this : succ x - y ≤ x, {exact le_of_lt_succ (sub_lt (succ_pos x) h)},
note h₂ : (succ x - y) % y < y, {exact ih _ this},
have h₁ : succ x % y = (succ x - y) % y, {exact mod_eq_sub_mod (le_of_not_gt h₁)},
have this : succ x - y ≤ x, {exact le_of_lt_succ (sub_lt (succ_pos x) h)},
have h₂ : (succ x - y) % y < y, {exact ih _ this},
rwa -h₁ at h₂}}
end
@ -977,7 +977,7 @@ by rw [mul_comm x z, mul_comm y z, mul_comm (x % y) z]; apply mul_mod_mul_left
lemma mod_two_eq_zero_or_one (n : ℕ)
: n % 2 = 0 ∨ n % 2 = 1 :=
begin
note h : ((n % 2 < 1) ∨ (n % 2 = 1)),
have h : ((n % 2 < 1) ∨ (n % 2 = 1)),
{ apply lt_or_eq_of_le,
apply nat.le_of_succ_le_succ,
apply @nat.mod_lt n 2 (nat.le_succ _) },
@ -1004,11 +1004,11 @@ lemma sub_mul_mod (x k n : ℕ) (h₁ : n*k ≤ x) : (x - n*k) % n = x % n :=
begin
induction k with k,
{ simp },
{ note h₂ : n * k ≤ x,
{ have h₂ : n * k ≤ x,
{ rw [mul_succ] at h₁,
apply nat.le_trans _ h₁,
apply le_add_right _ n },
note h₄ : x - n * k ≥ n,
have h₄ : x - n * k ≥ n,
{ apply @nat.le_of_add_le_add_right (n*k),
rw [nat.sub_add_cancel h₂],
simp [mul_succ] at h₁, simp [h₁] },
@ -1017,7 +1017,7 @@ end
/- div & mod -/
lemma div_def (x y : nat) : x / y = if 0 < y ∧ y ≤ x then (x - y) / y + 1 else 0 :=
by note h := div_def_aux x y; rwa dif_eq_if at h
by have h := div_def_aux x y; rwa dif_eq_if at h
lemma mod_add_div (m k : ℕ)
: m % k + k * (m / k) = m :=
@ -1027,7 +1027,7 @@ begin
intros m IH,
cases decidable.em (0 < k ∧ k ≤ m) with h h',
-- 0 < k ∧ k ≤ m
{ note h' : m - k < m,
{ have h' : m - k < m,
{ apply nat.sub_lt _ h.left,
apply lt_of_lt_of_le h.left h.right },
rw [div_def, mod_def, if_pos h, if_pos h],
@ -1078,11 +1078,11 @@ begin
{ rw [h₀, nat.div_zero, nat.div_zero, nat.zero_sub] },
{ induction p with p,
{ simp },
{ note h₂ : n*p ≤ x,
{ have h₂ : n*p ≤ x,
{ transitivity,
{ apply nat.mul_le_mul_left, apply le_succ },
{ apply h₁ } },
note h₃ : x - n * p ≥ n,
have h₃ : x - n * p ≥ n,
{ apply le_of_add_le_add_right,
rw [nat.sub_add_cancel h₂, add_comm],
rw [mul_succ] at h₁,
@ -1130,7 +1130,7 @@ begin
{ rw [div_eq_sub_div Hk h],
cases x with x,
{ simp [zero_mul, zero_le_iff_true] },
{ note Hlt : y - k < y,
{ have Hlt : y - k < y,
{ apply sub_lt_of_pos_le ; assumption },
rw [ -add_one_eq_succ
, nat.add_le_add_iff_le_right
@ -1232,7 +1232,7 @@ end
theorem pow_lt_pow_of_lt_right {x : ℕ} (H : x > 1) {i j} (h : i < j) : x^i < x^j :=
begin
note xpos := lt_of_succ_lt H,
have xpos := lt_of_succ_lt H,
refine lt_of_lt_of_le _ (pow_le_pow_of_le_right xpos h),
rw [-mul_one (x^i), pow_succ],
exact nat.mul_lt_mul_of_pos_left H (pos_pow_of_pos _ xpos)
@ -1248,7 +1248,7 @@ begin
intros p IH,
cases lt_or_ge p (b^succ w) with h₁ h₁,
-- base case: p < b^succ w
{ note h₂ : p / b < b^w,
{ have h₂ : p / b < b^w,
{ rw [div_lt_iff_lt_mul p _ b_pos],
simp [pow_succ] at h₁,
simp [h₁] },
@ -1256,7 +1256,7 @@ begin
simp [mod_add_div] },
-- step: p ≥ b^succ w
{ -- Generate condiition for induction principal
note h₂ : p - b^succ w < p,
have h₂ : p - b^succ w < p,
{ apply sub_lt_of_pos_le _ _ (pos_pow_of_pos _ b_pos) h₁ },
-- Apply induction
@ -1267,7 +1267,7 @@ begin
-- Pull subtraction outside mod and div
rw [sub_mul_mod _ _ _ h₁, sub_mul_div _ _ _ h₁],
-- Cancel subtraction inside mod b^w
note p_b_ge : b^w ≤ p / b,
have p_b_ge : b^w ≤ p / b,
{ rw [le_div_iff_mul_le _ _ b_pos],
simp [h₁] },
rw [eq.symm (mod_eq_sub_mod p_b_ge)] }

2
library/init/data/option_t.lean
View file

@ -29,7 +29,7 @@ instance {m : Type u → Type v} [monad m] : monad (option_t m) :=
id_map := begin
intros,
simp [option_t_bind, function.comp],
note h : option_t_bind._match_1 option_t_return = @pure m _ (option α),
have h : option_t_bind._match_1 option_t_return = @pure m _ (option α),
{ apply funext, intro s, cases s, refl, refl },
{ simp [h], apply @monad.bind_pure _ (option α) m },
end,

2
library/init/data/sigma/lex.lean
View file

@ -40,7 +40,7 @@ section
(λ (a : α) (b₁ b₂ : β a) (h : s a b₁ b₂) (eq₂ : a = xa) (eq₃ : b₂ == xb),
begin
subst eq₂,
note new_eq₃ := eq_of_heq eq₃,
have new_eq₃ := eq_of_heq eq₃,
subst new_eq₃,
exact ihb b₁ h
end),

32
library/init/meta/interactive.lean
View file

@ -448,11 +448,14 @@ tactic.focus [tac]
/--
This tactic applies to any goal.
- `note h : T := p` adds a new hypothesis of name `h` and type `T` to the current goal if `p` a term of type `T`.
- `note h : T` adds a new hypothesis of name `h` and type `T` to the current goal and opens a new subgoal with target `T`.
The new subgoal becomes the main goal.
- `have h : T := p` adds the hypothesis `h : T` to the current goal if `p` a term of type `T`.
If `T` is omitted, it will be inferred.
- `have h : T` adds the hypothesis `h : T` to the current goal and opens a new subgoal with target `T`.
The new subgoal becomes the main goal. If `T` is omitted, it will be replaced by a fresh meta variable.
If `h` is omitted, it defaults to `this`.
-/
meta def note (h : parse ident?) (q₁ : parse (tk ":" *> texpr)?) (q₂ : parse $ (tk ":=" *> texpr)?) : tactic unit :=
meta def have_tac (h : parse ident?) (q₁ : parse (tk ":" *> texpr)?) (q₂ : parse $ (tk ":=" *> texpr)?) : tactic unit :=
let h := h.get_or_else `this in
match q₁, q₂ with
| some e, some p := do
@ -469,7 +472,16 @@ match q₁, q₂ with
tactic.assert h e
end >> skip
meta def define (h : parse ident?) (q₁ : parse (tk ":" *> texpr)?) (q₂ : parse $ (tk ":=" *> texpr)?) : tactic unit :=
/--
This tactic applies to any goal.
- `let h : T := p` adds the hypothesis `h : T := p` to the current goal if `p` a term of type `T`.
If `T` is omitted, it will be inferred.
- `let h : T` adds the hypothesis `h : T := ?M` to the current goal and opens a new subgoal `?M : T`.
The new subgoal becomes the main goal. If `T` is omitted, it will be replaced by a fresh meta variable.
If `h` is omitted, it defaults to `this`.
-/
meta def let_tac (h : parse ident?) (q₁ : parse (tk ":" *> texpr)?) (q₂ : parse $ (tk ":=" *> texpr)?) : tactic unit :=
let h := h.get_or_else `this in
match q₁, q₂ with
| some e, some p := do
@ -849,16 +861,16 @@ tactic.by_contradiction >> return ()
meta def done : tactic unit :=
tactic.done
private meta def show_goal_aux (p : pexpr) : list expr → list expr → tactic unit
| [] r := fail "show_goal tactic failed"
private meta def show_tac_aux (p : pexpr) : list expr → list expr → tactic unit
| [] r := fail "show tactic failed"
| (g::gs) r := do
do {set_goals [g], g_ty ← target, ty ← i_to_expr p, unify g_ty ty, set_goals (g :: r.reverse ++ gs), tactic.change ty}
<|>
show_goal_aux gs (g::r)
show_tac_aux gs (g::r)
meta def show_goal (q : parse texpr) : tactic unit :=
meta def show_tac (q : parse texpr) : tactic unit :=
do gs ← get_goals,
show_goal_aux q gs []
show_tac_aux q gs []
end interactive
end tactic

4
library/init/meta/smt/interactive.lean
View file

@ -77,7 +77,7 @@ tactic.interactive.change q none (loc.ns [])
meta def exact (q : parse texpr) : smt_tactic unit :=
tactic.interactive.exact q
meta def note (h : parse ident?) (q₁ : parse (tk ":" *> texpr)?) (q₂ : parse $ (tk ":=" *> texpr)?) : smt_tactic unit :=
meta def have_tac (h : parse ident?) (q₁ : parse (tk ":" *> texpr)?) (q₂ : parse $ (tk ":=" *> texpr)?) : smt_tactic unit :=
let h := h.get_or_else `this in
match q₁, q₂ with
| some e, some p := do
@ -94,7 +94,7 @@ match q₁, q₂ with
smt_tactic.assert h e
end >> return ()
meta def define (h : parse ident?) (q₁ : parse (tk ":" *> texpr)?) (q₂ : parse $ (tk ":=" *> texpr)?) : smt_tactic unit :=
meta def let_tac (h : parse ident?) (q₁ : parse (tk ":" *> texpr)?) (q₂ : parse $ (tk ":=" *> texpr)?) : smt_tactic unit :=
let h := h.get_or_else `this in
match q₁, q₂ with
| some e, some p := do

2
library/init/native/result.lean
View file

@ -50,7 +50,7 @@ section resultT
id_map := begin
intros, cases x,
dsimp [resultT.and_then],
note h : @resultT.and_then._match_1 _ m E α _ resultT.pure = pure,
have h : @resultT.and_then._match_1 _ m E α _ resultT.pure = pure,
{ apply funext, intro x,
cases x; simp [resultT.and_then, resultT.pure, resultT.and_then] },
{ rw [h, @monad.bind_pure _ (result E α) _] },

44
src/frontends/lean/tactic_notation.cpp
View file

@ -115,9 +115,36 @@ name get_interactive_tactic_full_name(name const & tac_class, name const & tac)
return name(tac_class, "interactive") + tac;
}
static bool is_curr_exact_shortcut(parser & p) {
return
p.curr_is_token(get_assume_tk()) ||
p.curr_is_token(get_calc_tk()) ||
p.curr_is_token(get_suppose_tk());
}
static bool is_keyword_tactic(parser & p) {
return
p.curr_is_token(get_let_tk()) ||
p.curr_is_token(get_have_tk()) ||
p.curr_is_token(get_show_tk());
}
static optional<name> is_interactive_tactic(parser & p, name const & tac_class) {
if (!p.curr_is_identifier()) return optional<name>();
name id = get_interactive_tactic_full_name(tac_class, p.get_name_val());
name id;
switch (p.curr()) {
case token_kind::Identifier:
id = p.get_name_val();
break;
case token_kind::Keyword:
if (is_keyword_tactic(p)) {
id = p.get_token_info().value().append_after("_tac");
break;
}
/* fall through */
default:
return {};
}
id = get_interactive_tactic_full_name(tac_class, id);
if (p.env().find(id))
return optional<name>(id);
else
@ -178,14 +205,6 @@ static expr parse_interactive_tactic(parser & p, name const & decl_name, name co
return mk_tactic_step(p, r, pos, pos, tac_class, use_istep);
}
static bool is_curr_exact_shortcut(parser & p) {
return
p.curr_is_token(get_have_tk()) ||
p.curr_is_token(get_assume_tk()) ||
p.curr_is_token(get_calc_tk()) ||
p.curr_is_token(get_suppose_tk());
}
static expr mk_tactic_unit(name const & tac_class) {
return mk_app(mk_constant(tac_class), mk_constant(get_unit_name()));
}
@ -246,11 +265,6 @@ struct parse_tactic_fn {
}
throw;
}
} else if (m_p.curr_is_token(get_show_tk())) {
m_p.next();
expr arg = parse_qexpr();
r = m_p.mk_app(m_p.save_pos(mk_constant(get_interactive_tactic_full_name(m_tac_class, "show_goal")), pos), arg, pos);
if (m_use_istep) r = mk_tactic_istep(m_p, r, pos, pos, m_tac_class);
} else if (is_curr_exact_shortcut(m_p)) {
expr arg = parse_qexpr();
r = m_p.mk_app(m_p.save_pos(mk_constant(get_interactive_tactic_full_name(m_tac_class, "exact")), pos), arg, pos);

8
tests/lean/1207.lean
View file

@ -1,12 +1,12 @@
example : true :=
begin
note H : true := (by trivial),
have H : true := (by trivial),
exact H
end
example : true :=
begin
note H : true := (by tactic.triv),
have H : true := (by tactic.triv),
exact H
end
@ -18,13 +18,13 @@ end
example : false :=
begin
note H : true := (by foo), -- ERROR
have H : true := (by foo), -- ERROR
exact sorry
end
constant P : Prop
example (p : P) : true :=
begin
note H : P := by do { p ← tactic.get_local `p, tactic.exact p },
have H : P := by do { p ← tactic.get_local `p, tactic.exact p },
trivial
end

20
tests/lean/1467.lean
View file

@ -3,8 +3,8 @@ axiom H_f_g : ∀ n, f (g n) = n
example (m : ℕ) : h m = h m :=
begin
define n : ℕ := g m,
note H : f n = m := begin dsimp, rw H_f_g end,
let n : ℕ := g m,
have H : f n = m := begin dsimp, rw H_f_g end,
subst H, -- Error here
end
@ -12,16 +12,16 @@ set_option pp.instantiate_mvars false
example (m : ℕ) : h m = h m :=
begin
define n : ℕ, -- add metavar
let n : ℕ, -- add metavar
exact g m,
note H : f n = m := begin dsimp, rw H_f_g end,
have H : f n = m := begin dsimp, rw H_f_g end,
subst H, -- Error here
end
example (m : ℕ) : h m = h m :=
begin
define n : ℕ := g m,
note H : f n = m := begin dsimp, rw H_f_g end,
let n : ℕ := g m,
have H : f n = m := begin dsimp, rw H_f_g end,
subst m, -- Error here
end
@ -29,15 +29,15 @@ set_option pp.instantiate_mvars false
example (m : ℕ) : h m = h m :=
begin
define n : ℕ, -- add metavar
let n : ℕ, -- add metavar
exact g m,
note H : f n = m := begin dsimp, rw H_f_g end,
have H : f n = m := begin dsimp, rw H_f_g end,
subst m, -- Error here
end
example (m p: ℕ) : h m = h m :=
begin
define a : ℕ := g p,
define n : ℕ := g a,
let a : ℕ := g p,
let n : ℕ := g a,
clear p -- Error here
end

4
tests/lean/auto_quote_error2.lean
View file

@ -48,6 +48,6 @@ end
example : true :=
begin
{ note h' := eq.refl _ },
{ have h' := eq.refl _ },
--^ error should be at `}`
end
end

2
tests/lean/run/assert_tac1.lean
View file

@ -28,7 +28,7 @@ by do
definition tst3 (a : nat) : a = a :=
begin
define x : nat,
let x : nat,
exact a,
revert x,
intro y,

6
tests/lean/run/assert_tac3.lean
View file

@ -26,7 +26,7 @@ by do
definition tst4 (a : nat) : a = a :=
begin
note x : nat,
have x : nat,
rotate 1,
exact eq.refl a,
exact a
@ -34,14 +34,14 @@ end
definition tst5 (a : nat) : a = a :=
begin
define x : nat := a,
let x : nat := a,
trace_state,
exact eq.refl x
end
definition tst6 (a : nat) : a = a :=
begin
define x := a,
let x := a,
trace_state,
exact eq.refl x
end

2
tests/lean/run/cases_nested.lean
View file

@ -18,7 +18,7 @@ lemma ex (t : term) (h : cidx t = 2) : term.app (tid t) (to_list t) = t :=
begin
cases t,
{simp [cidx] at h,
note h : 1 ≠ 2, tactic.comp_val,
have h : 1 ≠ 2, tactic.comp_val,
contradiction},
{simp [tid, to_list]}
end

4
tests/lean/run/cc_constructors.lean
View file

@ -25,7 +25,7 @@ begin
constructor applications. So, the following one should fail. -/
try {cc},
/- Complete it manually. TODO(Leo): we can automate it for inhabited types. -/
note h := congr_fun h1 [],
have h := congr_fun h1 [],
cc
end
@ -39,7 +39,7 @@ begin
/- In the current implementation, cc does not "complete" partially applied
constructor applications. So, the following one should fail. -/
try {cc},
note h := congr_fun h1 0,
have h := congr_fun h1 0,
cc
end

6
tests/lean/run/destruct.lean
View file

@ -16,8 +16,8 @@ axiom fax2 {α : Type u} {n : nat} (v : Vec α (nat.succ n)) : f v = 1
example {α : Type u} {n : nat} (v : Vec α n) : f v ≠ 2 :=
begin
destruct v,
{intros, intro, note h := fax1 α, cc},
intros n1 h t, intros, intro, note h := fax2 (Vec.cons h t), cc
{intros, intro, have h := fax1 α, cc},
intros n1 h t, intros, intro, have h := fax2 (Vec.cons h t), cc
end
open nat
@ -25,6 +25,6 @@ example : ∀ n, 0 < n → succ (pred n) = n :=
begin
intro n,
destruct n,
{dsimp, intros, note h := lt_irrefl 0, cc},
{dsimp, intros, have h := lt_irrefl 0, cc},
{intros, subst n, dsimp, reflexivity}
end

4
tests/lean/run/doc_string4.lean
View file

@ -123,8 +123,8 @@ lemma aval_asimp_const₃ : ∀ (a : aexp) (s : state), aval (asimp_const a) s =
| (var x) s := rfl
| (plus a₁ a₂) s :=
begin
note h₁ := aval_asimp_const₃ a₁ s,
note h₂ := aval_asimp_const₃ a₂ s,
have h₁ := aval_asimp_const₃ a₁ s,
have h₂ := aval_asimp_const₃ a₂ s,
unfold asimp_const aval,
rewrite [-h₁, -h₂],
cases (asimp_const a₁); cases (asimp_const a₂); repeat {reflexivity}

14
tests/lean/run/overload2.lean
View file

@ -22,39 +22,39 @@ open F2 nat
example : true :=
begin
note H : (1 : nat) + (1 : nat) = 2,
have H : (1 : nat) + (1 : nat) = 2,
reflexivity,
constructor
end
example : true :=
begin
note H : 1 + 1 = 2,
have H : 1 + 1 = 2,
reflexivity,
constructor
end
example : true :=
begin
note H : (1:nat) + 1 = 2,
have H : (1:nat) + 1 = 2,
reflexivity,
constructor
end
example : true :=
begin
note H : I + O = I,
have H : I + O = I,
reflexivity,
constructor
end
example : true :=
begin
note H1 : I + O = I,
have H1 : I + O = I,
reflexivity,
note H2 : 1 + 0 = 1,
have H2 : 1 + 0 = 1,
reflexivity,
note H3 : (1:int) + 0 = 1,
have H3 : (1:int) + 0 = 1,
reflexivity,
constructor
end

8
tests/lean/run/show_goal.lean
View file

@ -1,14 +1,6 @@
open tactic
lemma ex1 (a b c : nat) : a + 0 = 0 + a ∧ 0 + b = b ∧ c + b = b + c :=
begin
repeat {any_goals {constructor}},
show_goal c + b = b + c, { apply add_comm },
show_goal a + 0 = 0 + a, { simp },
show_goal 0 + b = b, { rw [zero_add] }
end
lemma ex2 (a b c : nat) : a + 0 = 0 + a ∧ 0 + b = b ∧ c + b = b + c :=
begin
repeat {any_goals {constructor}},
show c + b = b + c, { apply add_comm },

4
tests/lean/run/simp_univ_metavars.lean
View file

@ -38,8 +38,8 @@ lemma NaturalTransformations_componentwise_equal
begin
induction α with αc,
induction β with βc,
have hc : αc = βc, from funext w,
by subst hc
have hc : αc = βc := funext w,
subst hc
end
@[simp]

2
tests/lean/run/smt_assert_define.lean
View file

@ -35,6 +35,6 @@ end
lemma ex4 (a b c : nat) : a = b → p (f a) (f b) → p a b :=
begin [smt]
intros,
note h : p (f a) (f a),
have h : p (f a) (f a),
add_fact (pf _ h)
end

2
tests/lean/run/smt_destruct.lean
View file

@ -11,7 +11,7 @@ by using_smt $ do
lemma ex2 (p q : Prop) : p ∨ q → p ∨ ¬q → ¬p ∨ q → ¬p ∨ ¬q → false :=
begin [smt]
intros,
note h : p ∨ q,
have h : p ∨ q,
destruct h
end

4
tests/lean/run/smt_ematch1.lean
View file

@ -44,7 +44,7 @@ end
lemma ex6 (a b c d e : nat) : (∀ x, g x (f x) = 0) → a = f b → g b a + 0 = f 0 :=
begin [smt]
intros,
note h : ∀ x, g x (f x) = 0,
have h : ∀ x, g x (f x) = 0,
add_lemma [h, fax, add_zero],
ematch
end
@ -52,7 +52,7 @@ end
lemma ex7 (a b c d e : nat) : (∀ x, g x (f x) = 0) → a = f b → g b a + 0 = f 0 :=
begin [smt]
intros,
note h : ∀ x, g x (f x) = 0,
have h : ∀ x, g x (f x) = 0,
ematch_using [h, fax, add_zero]
end

12
tests/lean/run/tactic_mode_scope_bug.lean
View file

@ -1,15 +1,15 @@
example (p q : Prop) : p ∧ q → q ∧ p :=
begin
intro h,
have hp : p, from h^.left,
have hq : q, from h^.right,
⟨hq, hp⟩
have hp : p := h^.left,
have hq : q := h^.right,
exact ⟨hq, hp⟩
end
example (p q : Prop) (hp : q) (hq : p) : p ∧ q → q ∧ p :=
begin
intro h,
have hp : p, from h^.left,
have hq : q, from h^.right,
⟨hq, hp⟩
have hp : p := h^.left,
have hq : q := h^.right,
exact ⟨hq, hp⟩
end

8
tests/lean/run/term_app2.lean
View file

@ -1,15 +1,15 @@
lemma nat.lt_add_of_lt {a b c : nat} : a < b → a < c + b :=
begin
intro h,
note aux₁ := nat.le_add_right b c,
note aux₂ := lt_of_lt_of_le h aux₁,
have aux₁ := nat.le_add_right b c,
have aux₂ := lt_of_lt_of_le h aux₁,
rwa [add_comm] at aux₂
end
lemma nat.lt_one_add_of_lt {a b : nat} : a < b → a < 1 + b :=
begin
intro h,
note aux := lt.trans h (nat.lt_succ_self _),
have aux := lt.trans h (nat.lt_succ_self _),
rwa [-nat.add_one_eq_succ, add_comm] at aux
end
@ -31,7 +31,7 @@ lemma sizeof_lt_sizeof_of_mem {α} [has_sizeof α] {a : α} : ∀ {l : list α},
cases eq_or_mem_of_mem_cons h with h_1 h_2,
subst h_1,
{unfold_sizeof, cancel_nat_add_lt, trivial_nat_lt},
{note aux₁ := sizeof_lt_sizeof_of_mem h_2,
{have aux₁ := sizeof_lt_sizeof_of_mem h_2,
unfold_sizeof,
exact nat.lt_one_add_of_lt (nat.lt_add_of_lt aux₁)}
end

4
tests/lean/smt_begin_end1.lean
View file

@ -5,7 +5,7 @@ axiom pf (a : nat) : p (f a) (f a) → p a a
example (a b c : nat) : a = b → p (f a) (f b) → p a b :=
begin [smt]
intros,
note h : p (f a) (f a),
have h : p (f a) (f a),
trace_state,
add_fact (pf _ h)
end
@ -21,7 +21,7 @@ begin
subst h,
begin [smt]
intros,
note h₁ : p (f a) (f a),
have h₁ : p (f a) (f a),
trace_state,
add_fact (pf _ h₁)
end

6
tests/lean/tactic_state_pp.lean
View file

@ -26,8 +26,8 @@ meta instance i2 : has_to_format tactic_state :=
example {α : Type u} {n : nat} (v : Vec α n) : f v ≠ 2 :=
begin
destruct v,
intros, intro, note h := fax1 α, cc,
-- intros n1 h t, intros, intro, note h := fax2 (Vec.cons h t), cc
intros, intro, have h := fax1 α, cc,
-- intros n1 h t, intros, intro, have h := fax2 (Vec.cons h t), cc
end
open nat
@ -35,5 +35,5 @@ example : ∀ n, 0 < n → succ (pred n) = n :=
begin
intro n,
destruct n,
dsimp, intros, note h := lt_irrefl 0, cc,
dsimp, intros, have h := lt_irrefl 0, cc,
end