From 3912bc24c80beeb64bf979f9f457c6b601b329f8 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 30 Apr 2015 11:00:39 -0700 Subject: [PATCH] feat(frontends/lean): nicer syntax for 'intros' 'reverts' and 'clears' --- hott/algebra/category/adjoint.hlean | 2 +- hott/algebra/category/category.hlean | 2 +- .../category/constructions/functor.hlean | 2 +- hott/algebra/category/functor.hlean | 16 +-- hott/algebra/category/groupoid.hlean | 12 +- hott/algebra/category/iso.hlean | 8 +- hott/algebra/category/nat_trans.hlean | 2 +- hott/algebra/category/yoneda.hlean | 12 +- hott/hit/coeq.hlean | 2 +- hott/hit/colimit.hlean | 4 +- hott/hit/cylinder.hlean | 2 +- hott/hit/pushout.hlean | 2 +- hott/hit/quotient.hlean | 2 +- hott/hit/trunc.hlean | 4 +- hott/init/nat.hlean | 18 +-- hott/init/tactic.hlean | 24 ++-- hott/types/W.hlean | 30 ++--- hott/types/equiv.hlean | 22 ++-- hott/types/function.hlean | 2 +- hott/types/hprop_trunc.hlean | 10 +- hott/types/pi.hlean | 8 +- hott/types/prod.hlean | 10 +- hott/types/sigma.hlean | 28 ++--- hott/types/trunc.hlean | 38 +++---- library/algebra/ordered_field.lean | 4 +- library/algebra/ordered_ring.lean | 16 +-- library/data/encodable.lean | 2 +- library/data/fintype.lean | 8 +- library/data/list/comb.lean | 2 +- library/data/list/perm.lean | 10 +- library/data/num.lean | 104 +++++++++--------- library/data/vector.lean | 2 +- library/init/nat.lean | 24 ++-- library/init/tactic.lean | 8 +- src/frontends/lean/parser.cpp | 24 ++-- src/library/tactic/clear_tactic.cpp | 30 +++-- src/library/tactic/intros_tactic.cpp | 18 ++- src/library/tactic/revert_tactic.cpp | 25 ++--- tests/lean/errors.lean.expected.out | 2 +- 39 files changed, 268 insertions(+), 273 deletions(-) diff --git a/hott/algebra/category/adjoint.hlean b/hott/algebra/category/adjoint.hlean index 73f4a17244..82d957913d 100644 --- a/hott/algebra/category/adjoint.hlean +++ b/hott/algebra/category/adjoint.hlean @@ -78,7 +78,7 @@ namespace category : is_hprop (is_left_adjoint F) := begin apply is_hprop.mk, - intros [G, G'], cases G with [G, η, ε, H, K], cases G' with [G', η', ε', H', K'], + intro G G', cases G with G η ε H K, cases G' with G' η' ε' H' K', fapply (apd011111 is_left_adjoint.mk), { fapply functor_eq, { intro d, apply eq_of_iso, fapply iso.MK, diff --git a/hott/algebra/category/category.hlean b/hott/algebra/category/category.hlean index c6849b273f..26af0046f3 100644 --- a/hott/algebra/category/category.hlean +++ b/hott/algebra/category/category.hlean @@ -41,7 +41,7 @@ namespace category definition is_trunc_1_ob : is_trunc 1 ob := begin - apply is_trunc_succ_intro, intros [a, b], + apply is_trunc_succ_intro, intro a b, fapply is_trunc_is_equiv_closed, exact (@eq_of_iso _ _ a b), apply is_equiv_inv, diff --git a/hott/algebra/category/constructions/functor.hlean b/hott/algebra/category/constructions/functor.hlean index 660c3377d6..549922c1ef 100644 --- a/hott/algebra/category/constructions/functor.hlean +++ b/hott/algebra/category/constructions/functor.hlean @@ -123,7 +123,7 @@ namespace category begin fapply functor_eq, {exact (eq_of_iso_ob η)}, - {intros [c, c', f], --unfold eq_of_iso_ob, --TODO: report: this fails + {intro c c' f, --unfold eq_of_iso_ob, --TODO: report: this fails apply concat, {apply (ap (λx, to_hom x ∘ to_fun_hom F f ∘ _)), apply (right_inv iso_of_eq)}, apply concat, diff --git a/hott/algebra/category/functor.hlean b/hott/algebra/category/functor.hlean index 9791a9fc18..f0069c9f8a 100644 --- a/hott/algebra/category/functor.hlean +++ b/hott/algebra/category/functor.hlean @@ -137,14 +137,14 @@ namespace functor -- TODO(Leo): investigate why we need to use relaxed-exact (rexact) tactic here exact (pr₁ S.2.2), rexact (pr₂ S.2.2)}, {intro F, - cases F with [d1, d2, d3, d4], + cases F with d1 d2 d3 d4, exact ⟨d1, d2, (d3, @d4)⟩}, {intro F, cases F, apply idp}, {intro S, - cases S with [d1, S2], - cases S2 with [d2, P1], + cases S with d1 S2, + cases S2 with d2 P1, cases P1, apply idp}, end @@ -183,8 +183,8 @@ namespace functor definition functor_eq2 {F₁ F₂ : C ⇒ D} (p q : F₁ = F₂) (r : ap010 to_fun_ob p ∼ ap010 to_fun_ob q) : p = q := begin - cases F₁ with [ob₁, hom₁, id₁, comp₁], - cases F₂ with [ob₂, hom₂, id₂, comp₂], + cases F₁ with ob₁ hom₁ id₁ comp₁, + cases F₂ with ob₂ hom₂ id₂ comp₂, rewrite [-functor_eq_eta' p, -functor_eq_eta' q], apply functor_eq2', apply ap_eq_ap_of_homotopy, @@ -195,8 +195,8 @@ namespace functor -- (q : p ▹ F₁ = F₂) (c : C) : -- ap to_fun_ob (functor_eq (apd10 p) (λa b f, _)) = p := sorry -- begin - -- cases F₂, revert q, apply (homotopy.rec_on p), clear p, esimp, intros (p, q), - -- cases p, clears (e_1, e_2), + -- cases F₂, revert q, apply (homotopy.rec_on p), clear p, esimp, intros p q, + -- cases p, clear e_1 e_2, -- end -- TODO: remove sorry @@ -204,7 +204,7 @@ namespace functor (q : (λ(a b : C) (f : hom a b), hom_of_eq (p b) ∘ F₁ f ∘ inv_of_eq (p a)) ∼3 to_fun_hom F₂) (c : C) : ap010 to_fun_ob (functor_eq p q) c = p c := begin - cases F₂, revert q, apply (homotopy.rec_on p), clear p, esimp, intros [p, q], + cases F₂, revert q, apply (homotopy.rec_on p), clear p, esimp, intro p q, apply sorry, --apply (homotopy3.rec_on q), clear q, intro q, --cases p, --TODO: report: this fails diff --git a/hott/algebra/category/groupoid.hlean b/hott/algebra/category/groupoid.hlean index 17c77f3817..5407ad1f46 100644 --- a/hott/algebra/category/groupoid.hlean +++ b/hott/algebra/category/groupoid.hlean @@ -44,9 +44,9 @@ namespace category [G : groupoid ob] : group (hom (center ob) (center ob)) := begin fapply group.mk, - intros [f, g], apply (comp f g), + intro f g, apply (comp f g), apply is_hset_hom, - intros [f, g, h], apply (assoc f g h)⁻¹, + intro f g h, apply (assoc f g h)⁻¹, apply (ID (center ob)), intro f, apply id_left, intro f, apply id_right, @@ -57,9 +57,9 @@ namespace category definition group_of_groupoid_unit [G : groupoid unit] : group (hom ⋆ ⋆) := begin fapply group.mk, - intros [f, g], apply (comp f g), + intro f g, apply (comp f g), apply is_hset_hom, - intros [f, g, h], apply (assoc f g h)⁻¹, + intro f g h, apply (assoc f g h)⁻¹, apply (ID ⋆), intro f, apply id_left, intro f, apply id_right, @@ -87,9 +87,9 @@ namespace category group (hom a a) := begin fapply group.mk, - intros [f, g], apply (comp f g), + intro f g, apply (comp f g), apply is_hset_hom, - intros [f, g, h], apply (assoc f g h)⁻¹, + intros f g h, apply (assoc f g h)⁻¹, apply (ID a), intro f, apply id_left, intro f, apply id_right, diff --git a/hott/algebra/category/iso.hlean b/hott/algebra/category/iso.hlean index 20fe815ea5..b717f70959 100644 --- a/hott/algebra/category/iso.hlean +++ b/hott/algebra/category/iso.hlean @@ -113,8 +113,8 @@ namespace iso definition is_hprop_is_iso [instance] (f : hom a b) : is_hprop (is_iso f) := begin - apply is_hprop.mk, intros [H, H'], - cases H with [g, li, ri], cases H' with [g', li', ri'], + apply is_hprop.mk, intro H H', + cases H with g li ri, cases H' with g' li' ri', fapply (apd0111 (@is_iso.mk ob C a b f)), apply left_inverse_eq_right_inverse, apply li, @@ -167,7 +167,7 @@ namespace iso fapply (equiv.mk), {intro S, apply iso.mk, apply (S.2)}, {fapply adjointify, - {intro p, cases p with [f, H], exact (sigma.mk f H)}, + {intro p, cases p with f H, exact sigma.mk f H}, {intro p, cases p, apply idp}, {intro S, cases S, apply idp}}, end @@ -176,7 +176,7 @@ namespace iso definition is_hset_iso [instance] : is_hset (a ≅ b) := begin apply is_trunc_is_equiv_closed, - apply (equiv.to_is_equiv (!iso.sigma_char)), + apply equiv.to_is_equiv (!iso.sigma_char), end definition iso_of_eq (p : a = b) : a ≅ b := diff --git a/hott/algebra/category/nat_trans.hlean b/hott/algebra/category/nat_trans.hlean index 49bf05c748..54467abf54 100644 --- a/hott/algebra/category/nat_trans.hlean +++ b/hott/algebra/category/nat_trans.hlean @@ -68,7 +68,7 @@ namespace nat_trans intro H, fapply sigma.mk, intro a, exact (H a), - intros [a, b, f], exact (naturality H f), + intro a b f, exact (naturality H f), intro η, apply nat_trans_eq, intro a, apply idp, intro S, fapply sigma_eq, diff --git a/hott/algebra/category/yoneda.hlean b/hott/algebra/category/yoneda.hlean index 224f8681aa..59286e8ba6 100644 --- a/hott/algebra/category/yoneda.hlean +++ b/hott/algebra/category/yoneda.hlean @@ -30,7 +30,7 @@ namespace yoneda intro x, apply eq_of_homotopy, intro h, exact (!id_left ⬝ !id_right) end begin - intros [x, y, z, g, f], apply eq_of_homotopy, intro h, + intro x y z g f, apply eq_of_homotopy, intro h, exact (representable_functor_assoc g.2 f.2 h f.1 g.1), end end yoneda @@ -127,8 +127,8 @@ namespace functor theorem functor_uncurry_functor_curry : functor_uncurry (functor_curry F) = F := functor_eq (λp, ap (to_fun_ob F) !prod.eta) begin - intros [cd, cd', fg], - cases cd with [c,d], cases cd' with [c',d'], cases fg with [f, g], + intro cd cd' fg, + cases cd with c d, cases cd' with c' d', cases fg with f g, apply concat, apply id_leftright, show (functor_uncurry (functor_curry F)) (f, g) = F (f,g), from calc @@ -143,7 +143,7 @@ namespace functor begin fapply functor_eq, {intro d, apply idp}, - {intros [d, d', g], + {intro d d' g, apply concat, apply id_leftright, show to_fun_hom (functor_curry (functor_uncurry G) c) g = to_fun_hom (G c) g, from calc @@ -157,7 +157,7 @@ namespace functor theorem functor_curry_functor_uncurry : functor_curry (functor_uncurry G) = G := begin fapply functor_eq, exact (functor_curry_functor_uncurry_ob G), - intros [c, c', f], + intro c c' f, fapply nat_trans_eq, intro d, apply concat, @@ -190,7 +190,7 @@ namespace functor : functor_prod_flip D C ∘f (functor_prod_flip C D) = functor.id := begin fapply functor_eq, {intro p, apply prod.eta}, - intros [p, p', h], cases p with [c, d], cases p' with [c', d'], + intro p p' h, cases p with c d, cases p' with c' d', apply id_leftright, end end functor diff --git a/hott/hit/coeq.hlean b/hott/hit/coeq.hlean index 2727deb113..dbf92bf57b 100644 --- a/hott/hit/coeq.hlean +++ b/hott/hit/coeq.hlean @@ -37,7 +37,7 @@ parameters {A B : Type.{u}} (f g : A → B) begin fapply (type_quotient.rec_on y), { intro a, apply P_i}, - { intros [a, a', H], cases H, apply Pcp} + { intro a a' H, cases H, apply Pcp} end protected definition rec_on [reducible] {P : coeq → Type} (y : coeq) diff --git a/hott/hit/colimit.hlean b/hott/hit/colimit.hlean index cb3d8aac0c..4813f96c3d 100644 --- a/hott/hit/colimit.hlean +++ b/hott/hit/colimit.hlean @@ -41,7 +41,7 @@ section begin fapply (type_quotient.rec_on y), { intro a, cases a, apply Pincl}, - { intros [a, a', H], cases H, apply Pglue} + { intro a a' H, cases H, apply Pglue} end protected definition rec_on [reducible] {P : colimit → Type} (y : colimit) @@ -124,7 +124,7 @@ section begin fapply (type_quotient.rec_on aa), { intro a, cases a, apply Pincl}, - { intros [a, a', H], cases H, apply Pglue} + { intro a a' H, cases H, apply Pglue} end protected definition rec_on [reducible] {P : seq_colim → Type} (aa : seq_colim) diff --git a/hott/hit/cylinder.hlean b/hott/hit/cylinder.hlean index b7aa2c44d8..ef8c7b88f2 100644 --- a/hott/hit/cylinder.hlean +++ b/hott/hit/cylinder.hlean @@ -43,7 +43,7 @@ parameters {A B : Type.{u}} (f : A → B) { intro a, cases a, apply Pbase, apply Ptop}, - { intros [a, a', H], cases H, apply Pseg} + { intro a a' H, cases H, apply Pseg} end protected definition rec_on [reducible] {P : cylinder → Type} (x : cylinder) diff --git a/hott/hit/pushout.hlean b/hott/hit/pushout.hlean index 4d14ad8a5d..0dfdc2d68b 100644 --- a/hott/hit/pushout.hlean +++ b/hott/hit/pushout.hlean @@ -42,7 +42,7 @@ parameters {TL BL TR : Type} (f : TL → BL) (g : TL → TR) { intro a, cases a, apply Pinl, apply Pinr}, - { intros [a, a', H], cases H, apply Pglue} + { intro a a' H, cases H, apply Pglue} end protected definition rec_on [reducible] {P : pushout → Type} (y : pushout) diff --git a/hott/hit/quotient.hlean b/hott/hit/quotient.hlean index e1e534be9e..6ae09c9476 100644 --- a/hott/hit/quotient.hlean +++ b/hott/hit/quotient.hlean @@ -35,7 +35,7 @@ parameters {A : Type} (R : A → A → hprop) { intro x', apply Pt}, { intro y, fapply (type_quotient.rec_on y), { exact Pc}, - { intros [a, a', H], + { intro a a' H, apply concat, apply transport_compose;apply Pp}} end diff --git a/hott/hit/trunc.hlean b/hott/hit/trunc.hlean index ffca2a7689..54146bb427 100644 --- a/hott/hit/trunc.hlean +++ b/hott/hit/trunc.hlean @@ -84,10 +84,10 @@ namespace trunc -- begin -- fapply equiv.MK, -- apply sorry, --{exact (λpp, trunc.rec_on pp (λp, (tr p.1, tr p.2)))}, - -- apply sorry, /-{intro p, cases p with (xx, yy), + -- apply sorry, /-{intro p, cases p with xx yy, -- apply (trunc.rec_on xx), intro x, -- apply (trunc.rec_on yy), intro y, exact (tr (x,y))},-/ - -- apply sorry, /-{intro p, cases p with (xx, yy), + -- apply sorry, /-{intro p, cases p with xx yy, -- apply (trunc.rec_on xx), intro x, -- apply (trunc.rec_on yy), intro y, apply idp},-/ -- apply sorry --{intro pp, apply (trunc.rec_on pp), intro p, cases p, apply idp}, diff --git a/hott/init/nat.hlean b/hott/init/nat.hlean index 495cc4d4dd..f60074408d 100644 --- a/hott/init/nat.hlean +++ b/hott/init/nat.hlean @@ -152,9 +152,9 @@ namespace nat definition le.rec_on {a : nat} {P : nat → Type} {b : nat} (H : a ≤ b) (H₁ : P a) (H₂ : ∀ b, a < b → P b) : P b := begin - cases H with [b', hlt], + cases H with b' hlt, apply H₁, - apply (H₂ b hlt) + apply H₂ b hlt end definition lt.irrefl (a : nat) : ¬ a < a := @@ -201,23 +201,23 @@ namespace nat definition le.trans {a b c : nat} (h₁ : a ≤ b) (h₂ : b ≤ c) : a ≤ c := begin - cases h₁ with [b', hlt], + cases h₁ with b' hlt, apply h₂, - apply (lt.trans hlt h₂) + apply lt.trans hlt h₂ end definition lt.of_le_of_lt {a b c : nat} (h₁ : a ≤ b) (h₂ : b < c) : a < c := begin - cases h₁ with [b', hlt], + cases h₁ with b' hlt, apply h₂, - apply (lt.trans hlt h₂) + apply lt.trans hlt h₂ end definition lt.of_lt_of_le {a b c : nat} (h₁ : a < b) (h₂ : b ≤ c) : a < c := begin - cases h₁ with [b', hlt], - apply (lt.of_succ_lt_succ h₂), - apply (lt.trans hlt (lt.of_succ_lt_succ h₂)) + cases h₁ with b' hlt, + apply lt.of_succ_lt_succ h₂, + apply lt.trans hlt (lt.of_succ_lt_succ h₂) end definition lt.of_lt_of_eq {a b c : nat} (h₁ : a < b) (h₂ : b = c) : a < c := diff --git a/hott/init/tactic.hlean b/hott/init/tactic.hlean index 2c11101649..397c9723d5 100644 --- a/hott/init/tactic.hlean +++ b/hott/init/tactic.hlean @@ -64,19 +64,19 @@ definition identifier := expr definition identifier_list := expr_list definition opt_identifier_list := expr_list -opaque definition apply (e : expr) : tactic := builtin -opaque definition fapply (e : expr) : tactic := builtin -opaque definition rename (a b : identifier) : tactic := builtin -opaque definition intro (e : identifier) : tactic := builtin -opaque definition generalize (e : expr) : tactic := builtin -opaque definition clear (e : identifier) : tactic := builtin -opaque definition revert (e : identifier) : tactic := builtin -opaque definition refine (e : expr) : tactic := builtin -opaque definition exact (e : expr) : tactic := builtin +opaque definition apply (e : expr) : tactic := builtin +opaque definition fapply (e : expr) : tactic := builtin +opaque definition rename (a b : identifier) : tactic := builtin +opaque definition intro (e : identifier_list) : tactic := builtin +opaque definition generalize (e : expr) : tactic := builtin +opaque definition clear (e : identifier_list) : tactic := builtin +opaque definition revert (e : identifier_list) : tactic := builtin +opaque definition refine (e : expr) : tactic := builtin +opaque definition exact (e : expr) : tactic := builtin -- Relaxed version of exact that does not enforce goal type -opaque definition rexact (e : expr) : tactic := builtin -opaque definition check_expr (e : expr) : tactic := builtin -opaque definition trace (s : string) : tactic := builtin +opaque definition rexact (e : expr) : tactic := builtin +opaque definition check_expr (e : expr) : tactic := builtin +opaque definition trace (s : string) : tactic := builtin -- rewrite_tac is just a marker for the builtin 'rewrite' notation -- used to create instances of this tactic. diff --git a/hott/types/W.hlean b/hott/types/W.hlean index 8f2abbc0d2..989be8f387 100644 --- a/hott/types/W.hlean +++ b/hott/types/W.hlean @@ -63,10 +63,10 @@ namespace Wtype definition sup_path_W (p : w.1 = w'.1) (q : p ▹ w.2 = w'.2) : dpair (Wtype_eq p q)..1 (Wtype_eq p q)..2 = dpair p q := begin - reverts (p, q), - apply (cases_on w), intros (w1, w2), - apply (cases_on w'), intros (w1', w2', p), generalize w2', --change to revert - apply (path.rec_on p), intros (w2', q), + revert p q, + apply (cases_on w), intro w1 w2, + apply (cases_on w'), intro w1' w2' p, generalize w2', --change to revert + apply (path.rec_on p), intro w2' q, apply (path.rec_on q), apply idp end @@ -80,17 +80,17 @@ namespace Wtype definition eta_path_W (p : w = w') : Wtype_eq (p..1) (p..2) = p := begin apply (path.rec_on p), - apply (cases_on w), intros (w1, w2), + apply (cases_on w), intro w1 w2, apply idp end definition transport_pr1_path_W {B' : A → Type} (p : w.1 = w'.1) (q : p ▹ w.2 = w'.2) : transport (λx, B' x.1) (Wtype_eq p q) = transport B' p := begin - reverts (p, q), - apply (cases_on w), intros (w1, w2), - apply (cases_on w'), intros (w1', w2', p), generalize w2', - apply (path.rec_on p), intros (w2', q), + revert p q, + apply (cases_on w), intro w1 w2, + apply (cases_on w'), intro w1' w2' p, generalize w2', + apply (path.rec_on p), intro w2' q, apply (path.rec_on q), apply idp end @@ -131,9 +131,9 @@ namespace Wtype (∀ (b : B a) (b' : B a'), P (f b) (f' b')) → P (sup a f) (sup a' f')) : P w w' := begin revert w', - apply (rec_on w), intros (a, f, IH, w'), - apply (cases_on w'), intros (a', f'), - apply H, intros (b, b'), + apply (rec_on w), intro a f IH w', + apply (cases_on w'), intro a' f', + apply H, intro b b', apply IH end @@ -142,14 +142,14 @@ namespace Wtype definition trunc_W [instance] [FUN : funext.{v (max 1 u v)}] (n : trunc_index) [HA : is_trunc (n.+1) A] : is_trunc (n.+1) (W a, B a) := begin - fapply is_trunc_succ, intros (w, w'), - apply (double_induction_on w w'), intros (a, a', f, f', IH), + fapply is_trunc_succ, intro w w', + apply (double_induction_on w w'), intro a a' f f' IH, fapply is_trunc_equiv_closed, apply equiv_path_W, apply is_trunc_sigma, fapply (is_trunc_eq n), intro p, revert IH, generalize f', --change to revert after simpl - apply (path.rec_on p), intros (f', IH), + apply (path.rec_on p), intro f' IH, apply pi.is_trunc_eq_pi, intro b, apply IH end diff --git a/hott/types/equiv.hlean b/hott/types/equiv.hlean index 65a476910c..41846b17d1 100644 --- a/hott/types/equiv.hlean +++ b/hott/types/equiv.hlean @@ -56,9 +56,9 @@ namespace is_equiv equiv.MK (λH, ⟨inv f, right_inv f, left_inv f, adj f⟩) (λp, is_equiv.mk f p.1 p.2.1 p.2.2.1 p.2.2.2) (λp, begin - cases p with [p1, p2], - cases p2 with [p21, p22], - cases p22 with [p221, p222], + cases p with p1 p2, + cases p2 with p21 p22, + cases p22 with p221 p222, apply idp end) (λH, is_equiv.rec_on H (λH1 H2 H3 H4, idp)) @@ -118,9 +118,9 @@ namespace equiv begin fapply equiv.MK, {intro F, exact ⟨to_fun F, to_is_equiv F⟩}, - {intro p, cases p with [f, H], exact (equiv.mk f H)}, - {intro p, cases p with [f, H], exact idp}, - {intro F, cases F with [f, H], exact idp}, + {intro p, cases p with f H, exact (equiv.mk f H)}, + {intro p, cases p, exact idp}, + {intro F, cases F, exact idp}, end definition equiv_eq_char (f f' : A ≃ B) : (f = f') ≃ (to_fun f = to_fun f') := @@ -134,11 +134,11 @@ namespace equiv : is_equiv (ap to_fun : f = f' → to_fun f = to_fun f') := begin fapply adjointify, - {intro p, cases f with [f, H], cases f' with [f', H'], cases p, apply (ap (mk f')), apply is_hprop.elim}, - {intro p, cases f with [f, H], cases f' with [f', H'], cases p, - apply (@concat _ _ (ap to_fun (ap (equiv.mk f') (is_hprop.elim H H')))), {apply idp}, - generalize (is_hprop.elim H H'), intro q, cases q, apply idp}, - {intro p, cases p, cases f with [f, H], apply (ap (ap (equiv.mk f))), apply is_hset.elim} + {intro p, cases f with f H, cases f' with f' H', cases p, apply ap (mk f'), apply is_hprop.elim}, + {intro p, cases f with f H, cases f' with f' H', cases p, + apply @concat _ _ (ap to_fun (ap (equiv.mk f') (is_hprop.elim H H'))), {apply idp}, + generalize is_hprop.elim H H', intro q, cases q, apply idp}, + {intro p, cases p, cases f with f H, apply ap (ap (equiv.mk f)), apply is_hset.elim} end end equiv diff --git a/hott/types/function.hlean b/hott/types/function.hlean index 2c982a5dd8..999734fc13 100644 --- a/hott/types/function.hlean +++ b/hott/types/function.hlean @@ -48,7 +48,7 @@ namespace function (H : Π(a a' : A), f a = f a' → a = a') : is_embedding f := begin fapply is_embedding.mk, - intros [a, a'], + intro a a', fapply adjointify, {exact (H a a')}, {intro p, apply is_hset.elim}, diff --git a/hott/types/hprop_trunc.hlean b/hott/types/hprop_trunc.hlean index 1812b2d08e..07ca4ec310 100644 --- a/hott/types/hprop_trunc.hlean +++ b/hott/types/hprop_trunc.hlean @@ -20,8 +20,8 @@ namespace is_trunc begin fapply equiv.MK, { intro S, exact (is_contr.mk S.1 S.2)}, - { intro H, cases H with [H'], cases H' with [ce, co], exact ⟨ce, co⟩}, - { intro H, cases H with [H'], cases H' with [ce, co], exact idp}, + { intro H, cases H with H', cases H' with ce co, exact ⟨ce, co⟩}, + { intro H, cases H with H', cases H' with ce co, exact idp}, { intro S, cases S, apply idp} end @@ -30,7 +30,7 @@ namespace is_trunc begin fapply equiv.MK, { intro H, apply is_trunc_succ_intro}, - { intros [H, x, y], apply is_trunc_eq}, + { intro H x y, apply is_trunc_eq}, { intro H, cases H, apply idp}, { intro P, apply eq_of_homotopy, intro a, apply eq_of_homotopy, intro b, esimp [function.id,compose,is_trunc_succ_intro,is_trunc_eq], @@ -48,14 +48,14 @@ namespace is_trunc fapply sigma_eq, {apply x.2}, apply (@is_hprop.elim), apply is_trunc_pi, intro a, - apply is_hprop.mk, intros [w, z], + apply is_hprop.mk, intro w z, have H : is_hset A, begin apply is_trunc_succ, apply is_trunc_succ, apply is_contr.mk, exact y.2 end, fapply (@is_hset.elim A _ _ _ w z)}, - { intros [n', IH, A], + { intro n' IH A, apply is_trunc_is_equiv_closed, apply equiv.to_is_equiv, apply is_trunc.pi_char}, diff --git a/hott/types/pi.hlean b/hott/types/pi.hlean index d1d645fed2..e429380f86 100644 --- a/hott/types/pi.hlean +++ b/hott/types/pi.hlean @@ -157,15 +157,15 @@ namespace pi definition is_trunc_pi (B : A → Type) (n : trunc_index) [H : ∀a, is_trunc n (B a)] : is_trunc n (Πa, B a) := begin - reverts [B, H], + revert B H, apply (trunc_index.rec_on n), - {intros [B, H], + {intro B H, fapply is_contr.mk, intro a, apply center, intro f, apply eq_of_homotopy, intro x, apply (center_eq (f x))}, - {intros [n, IH, B, H], - fapply is_trunc_succ_intro, intros [f, g], + {intro n IH B H, + fapply is_trunc_succ_intro, intro f g, fapply is_trunc_equiv_closed, apply equiv.symm, apply eq_equiv_homotopy, apply IH, diff --git a/hott/types/prod.hlean b/hott/types/prod.hlean index ef1e5a200b..c38fe3e71b 100644 --- a/hott/types/prod.hlean +++ b/hott/types/prod.hlean @@ -25,11 +25,11 @@ namespace prod definition prod_eq (H₁ : pr₁ u = pr₁ v) (H₂ : pr₂ u = pr₂ v) : u = v := begin - cases u with [a₁, b₁], - cases v with [a₂, b₂], - apply (transport _ (eta (a₁, b₁))), - apply (transport _ (eta (a₂, b₂))), - apply (pair_eq H₁ H₂), + cases u with a₁ b₁, + cases v with a₂ b₂, + apply transport _ (eta (a₁, b₁)), + apply transport _ (eta (a₂, b₂)), + apply pair_eq H₁ H₂, end /- Symmetry -/ diff --git a/hott/types/sigma.hlean b/hott/types/sigma.hlean index 653b4bf5cf..11c3ab7160 100644 --- a/hott/types/sigma.hlean +++ b/hott/types/sigma.hlean @@ -141,12 +141,12 @@ namespace sigma definition sigma_eq2 {p q : u = v} (r : p..1 = q..1) (s : r ▹ p..2 = q..2) : p = q := begin - reverts [q, r, s], - cases p, cases u with [u1, u2], - intros [q, r, s], + revert q r s, + cases p, cases u with u1 u2, + intro q r s, apply concat, rotate 1, apply sigma_eq_eta, - apply (sigma_eq_eq_sigma_eq r s) + apply sigma_eq_eq_sigma_eq r s end /- In Coq they often have to give u and v explicitly when using the following definition -/ @@ -174,7 +174,7 @@ namespace sigma definition tr_eq2_nondep {C : A → Type} {D : Π a:A, B a → C a → Type} (p : a = a') (bcd : Σ(b : B a) (c : C a), D a b c) : p ▹ bcd = ⟨p ▹ bcd.1, p ▹ bcd.2.1, p ▹D2 bcd.2.2⟩ := begin - cases p, cases bcd with [b, cd], + cases p, cases bcd with b cd, cases cd, apply idp end @@ -193,8 +193,8 @@ namespace sigma ((g (f⁻¹ a'))⁻¹ (transport B' (right_inv f a')⁻¹ b')))) begin intro u', - cases u' with [a', b'], - apply (sigma_eq (right_inv f a')), + cases u' with a' b', + apply sigma_eq (right_inv f a'), -- rewrite right_inv, -- end -- "rewrite right_inv (g (f⁻¹ a'))" @@ -204,7 +204,7 @@ namespace sigma end begin intro u, - cases u with [a, b], + cases u with a b, apply (sigma_eq (left_inv f a)), show transport B (left_inv f a) ((g (f⁻¹ (f a)))⁻¹ (transport B' (right_inv f (f a))⁻¹ (g a b))) = b, from calc @@ -275,8 +275,8 @@ namespace sigma equiv.mk _ (adjointify (λav, ⟨⟨av.1, av.2.1⟩, av.2.2⟩) (λuc, ⟨uc.1.1, uc.1.2, !eta⁻¹ ▹ uc.2⟩) - begin intro uc; cases uc with [u, c]; cases u; apply idp end - begin intro av; cases av with [a, v]; cases v; apply idp end) + begin intro uc; cases uc with u c; cases u; apply idp end + begin intro av; cases av with a v; cases v; apply idp end) open prod definition assoc_equiv_prod (C : (A × A') → Type) : (Σa a', C (a,a')) ≃ (Σu, C u) := @@ -364,14 +364,14 @@ namespace sigma definition is_trunc_sigma (B : A → Type) (n : trunc_index) [HA : is_trunc n A] [HB : Πa, is_trunc n (B a)] : is_trunc n (Σa, B a) := begin - reverts [A, B, HA, HB], + revert A B HA HB, apply (trunc_index.rec_on n), - intros [A, B, HA, HB], + intro A B HA HB, fapply is_trunc.is_trunc_equiv_closed, apply equiv.symm, apply sigma_equiv_of_is_contr_pr1, - intros [n, IH, A, B, HA, HB], - fapply is_trunc.is_trunc_succ_intro, intros [u, v], + intro n IH A B HA HB, + fapply is_trunc.is_trunc_succ_intro, intro u v, fapply is_trunc.is_trunc_equiv_closed, apply equiv_sigma_eq, apply IH, diff --git a/hott/types/trunc.hlean b/hott/types/trunc.hlean index af16d80558..a59d7dba30 100644 --- a/hott/types/trunc.hlean +++ b/hott/types/trunc.hlean @@ -32,8 +32,8 @@ namespace is_trunc fapply equiv.MK, { intro A, exact (⟨carrier A, struct A⟩)}, { intro S, exact (trunctype.mk S.1 S.2)}, - { intro S, apply (sigma.rec_on S), intros [S1, S2], apply idp}, - { intro A, apply (trunctype.rec_on A), intros [A1, A2], apply idp}, + { intro S, apply (sigma.rec_on S), intro S1 S2, apply idp}, + { intro A, apply (trunctype.rec_on A), intro A1 A2, apply idp}, end definition trunctype_eq_equiv (n : trunc_index) (A B : n-Type) : @@ -48,24 +48,24 @@ namespace is_trunc definition is_trunc_is_embedding_closed (f : A → B) [Hf : is_embedding f] [HB : is_trunc n B] (Hn : -1 ≤ n) : is_trunc n A := begin - cases n with [n], - {exact (!empty.elim Hn)}, - {apply is_trunc_succ_intro, intros [a, a'], - fapply (@is_trunc_is_equiv_closed_rev _ _ n (ap f))} + cases n with n, + {exact !empty.elim Hn}, + {apply is_trunc_succ_intro, intro a a', + fapply @is_trunc_is_equiv_closed_rev _ _ n (ap f)} end definition is_trunc_is_retraction_closed (f : A → B) [Hf : is_retraction f] (n : trunc_index) [HA : is_trunc n A] : is_trunc n B := begin - reverts [A, B, f, Hf, HA], + revert A B f Hf HA, apply (trunc_index.rec_on n), - { clear n, intros [A, B, f, Hf, HA], cases Hf with [g, ε], fapply is_contr.mk, - { exact (f (center A))}, + { clear n, intro A B f Hf HA, cases Hf with g ε, fapply is_contr.mk, + { exact f (center A)}, { intro b, apply concat, { apply (ap f), exact (center_eq (g b))}, { apply ε}}}, - { clear n, intros [n, IH, A, B, f, Hf, HA], cases Hf with [g, ε], - apply is_trunc_succ_intro, intros [b, b'], + { clear n, intro n IH A B f Hf HA, cases Hf with g ε, + apply is_trunc_succ_intro, intro b b', fapply (IH (g b = g b')), { intro q, exact ((ε b)⁻¹ ⬝ ap f q ⬝ ε b')}, { apply (is_retraction.mk (ap g)), @@ -78,7 +78,7 @@ namespace is_trunc definition is_trunc_trunctype [instance] (n : trunc_index) : is_trunc n.+1 (n-Type) := begin - apply is_trunc_succ_intro, intros [X, Y], + apply is_trunc_succ_intro, intro X Y, fapply is_trunc_equiv_closed, {apply equiv.symm, apply trunctype_eq_equiv}, fapply is_trunc_equiv_closed, @@ -155,11 +155,11 @@ namespace trunc { intro p, cases p, apply (trunc.rec_on aa), intro a, esimp [trunc_eq_type,trunc.rec_on], exact (tr idp)}, { apply (trunc.rec_on aa'), apply (trunc.rec_on aa), - intros [a, a', x], esimp [trunc_eq_type, trunc.rec_on] at x, + intro a a' x, esimp [trunc_eq_type, trunc.rec_on] at x, apply (trunc.rec_on x), intro p, exact (ap tr p)}, { -- apply (trunc.rec_on aa'), apply (trunc.rec_on aa), - -- intros [a, a', x], esimp [trunc_eq_type, trunc.rec_on] at x, + -- intro a a' x, esimp [trunc_eq_type, trunc.rec_on] at x, -- apply (trunc.rec_on x), intro p, -- cases p, esimp [trunc.rec_on,eq.cases_on,compose,id], -- apply idp --? apply sorry}, @@ -173,15 +173,15 @@ namespace trunc definition is_trunc_trunc_of_is_trunc [instance] [priority 500] (A : Type) (n m : trunc_index) [H : is_trunc n A] : is_trunc n (trunc m A) := begin - reverts [A, m, H], apply (trunc_index.rec_on n), - { clear n, intros [A, m, H], apply is_contr_equiv_closed, + revert A m H, apply (trunc_index.rec_on n), + { clear n, intro A m H, apply is_contr_equiv_closed, { apply equiv_trunc, apply (@is_trunc_of_leq _ -2), exact unit.star} }, - { clear n, intros [n, IH, A, m, H], cases m with [m], + { clear n, intro n IH A m H, cases m with m, { apply (@is_trunc_of_leq _ -2), exact unit.star}, - { apply is_trunc_succ_intro, intros [aa, aa'], + { apply is_trunc_succ_intro, intro aa aa', apply (@trunc.rec_on _ _ _ aa (λy, !is_trunc_succ_of_is_hprop)), apply (@trunc.rec_on _ _ _ aa' (λy, !is_trunc_succ_of_is_hprop)), - intros [a, a'], apply (is_trunc_equiv_closed_rev), + intro a a', apply (is_trunc_equiv_closed_rev), { apply tr_eq_tr_equiv}, { exact (IH _ _ _)}}} end diff --git a/library/algebra/ordered_field.lean b/library/algebra/ordered_field.lean index 56085f4784..8186fdd5da 100644 --- a/library/algebra/ordered_field.lean +++ b/library/algebra/ordered_field.lean @@ -379,12 +379,12 @@ section discrete_linear_ordered_field theorem div_lt_div_of_pos_of_lt_of_pos (Hb : 0 < b) (H : b < a) (Hc : 0 < c) : c / a < c / b := begin - apply (iff.mp (sub_neg_iff_lt _ _)), + apply iff.mp (sub_neg_iff_lt _ _), rewrite [div_eq_mul_one_div, {c / b}div_eq_mul_one_div], rewrite -mul_sub_left_distrib, apply mul_neg_of_pos_of_neg, exact Hc, - apply (iff.mp' (sub_neg_iff_lt _ _)), + apply iff.mp' (sub_neg_iff_lt _ _), apply div_lt_div_of_lt, exact Hb, exact H end diff --git a/library/algebra/ordered_ring.lean b/library/algebra/ordered_ring.lean index dd9d5e91e6..711b147dac 100644 --- a/library/algebra/ordered_ring.lean +++ b/library/algebra/ordered_ring.lean @@ -294,14 +294,14 @@ lt.by_cases begin have H1 : 0 < a * b, from mul_pos Ha Hb, rewrite H at H1, - apply (absurd_a_lt_a H1) + apply absurd_a_lt_a H1 end) (assume Hb : 0 = b, or.inr (Hb⁻¹)) (assume Hb : 0 > b, begin have H1 : 0 > a * b, from mul_neg_of_pos_of_neg Ha Hb, rewrite H at H1, - apply (absurd_a_lt_a H1) + apply absurd_a_lt_a H1 end)) (assume Ha : 0 = a, or.inl (Ha⁻¹)) (assume Ha : 0 > a, @@ -310,14 +310,14 @@ lt.by_cases begin have H1 : 0 > a * b, from mul_neg_of_neg_of_pos Ha Hb, rewrite H at H1, - apply (absurd_a_lt_a H1) + apply absurd_a_lt_a H1 end) (assume Hb : 0 = b, or.inr (Hb⁻¹)) (assume Hb : 0 > b, begin have H1 : 0 < a * b, from mul_pos_of_neg_of_neg Ha Hb, rewrite H at H1, - apply (absurd_a_lt_a H1) + apply absurd_a_lt_a H1 end)) -- Linearity implies no zero divisors. Doesn't need commutativity. @@ -349,14 +349,14 @@ section (assume Hb : 0 = b, begin rewrite [-Hb at Hab, mul_zero at Hab], - apply (absurd_a_lt_a Hab) + apply absurd_a_lt_a Hab end) (assume Hb : b < 0, absurd Hab (lt.asymm (mul_neg_of_pos_of_neg Ha Hb)))) (assume Ha : 0 = a, begin rewrite [-Ha at Hab, zero_mul at Hab], - apply (absurd_a_lt_a Hab) + apply absurd_a_lt_a Hab end) (assume Ha : a < 0, lt.by_cases @@ -365,7 +365,7 @@ section (assume Hb : 0 = b, begin rewrite [-Hb at Hab, mul_zero at Hab], - apply (absurd_a_lt_a Hab) + apply absurd_a_lt_a Hab end) (assume Hb : b < 0, or.inr (and.intro Ha Hb))) @@ -430,7 +430,7 @@ section (assume H1 : 0 = a, begin rewrite [-H1 at H, sign_zero at H], - apply (absurd H zero_ne_one) + apply absurd H zero_ne_one end) (assume H1 : 0 > a, have H2 : -1 = 1, from (sign_of_neg H1)⁻¹ ⬝ H, diff --git a/library/data/encodable.lean b/library/data/encodable.lean index 6699560f9a..7129a392b0 100644 --- a/library/data/encodable.lean +++ b/library/data/encodable.lean @@ -42,7 +42,7 @@ encodable.mk (λ n, if n = 0 then some none else some (decode A (pred n))) (λ o, begin - cases o with [a], + cases o with a, begin esimp end, begin esimp, rewrite [if_neg !succ_ne_zero, pred_succ, encodable.encodek] end end) diff --git a/library/data/fintype.lean b/library/data/fintype.lean index 67805787ce..cb2aafe655 100644 --- a/library/data/fintype.lean +++ b/library/data/fintype.lean @@ -179,10 +179,10 @@ private theorem mem_ltype_elems {A : Type} {s : list A} {a : ⟪s⟫} | (b::l) h vainbl := or.elim (eq_or_mem_of_mem_cons vainbl) (λ vaeqb : value a = b, begin - reverts [vaeqb, h], - -- TODO(Leo): check why 'cases a with [va, ma]' produces an incorrect proof - apply (as_type.cases_on a), - intros [va, ma, vaeqb], + revert vaeqb h, + -- TODO(Leo): check why 'cases a with va, ma' produces an incorrect proof + apply as_type.cases_on a, + intro va ma vaeqb, rewrite -vaeqb, intro h, apply mem_cons end) diff --git a/library/data/list/comb.lean b/library/data/list/comb.lean index aca5408e7e..0ece60a887 100644 --- a/library/data/list/comb.lean +++ b/library/data/list/comb.lean @@ -260,7 +260,7 @@ theorem zip_unzip : ∀ (l : list (A × B)), zip (pr₁ (unzip l)) (pr₂ (unzip have r : zip (pr₁ (unzip l)) (pr₂ (unzip l)) = l, from zip_unzip l, revert r, apply prod.cases_on (unzip l), - intros [la, lb, r], + intro la lb r, rewrite -r end diff --git a/library/data/list/perm.lean b/library/data/list/perm.lean index 188d0cd4d4..55697f28bc 100644 --- a/library/data/list/perm.lean +++ b/library/data/list/perm.lean @@ -270,7 +270,7 @@ match l₂ with | [] := λ e h₁ h₂, list.no_confusion e (λ e₁ e₂, h₁ rfl e₁ e₂) | h::t := λ e h₁ h₂, begin - apply list.no_confusion e, intros [e₁, e₂], + apply list.no_confusion e, intro e₁ e₂, rewrite e₁ at h₂, exact h₂ t rfl e₂ end @@ -289,15 +289,15 @@ match l₂ with | [h₁] := λ e H₁ H₂ H₃, begin rewrite [append_cons at e, append_nil_left at e], - apply list.no_confusion e, intros [a_eq_h₁, rest], - apply list.no_confusion rest, intros [b_eq_c, l₁_eq_l₃], + apply list.no_confusion e, intro a_eq_h₁ rest, + apply list.no_confusion rest, intro b_eq_c l₁_eq_l₃, rewrite [a_eq_h₁ at H₂, b_eq_c at H₂, l₁_eq_l₃ at H₂], exact H₂ rfl rfl rfl end | h₁::h₂::t₂ := λ e H₁ H₂ H₃, begin - apply list.no_confusion e, intros [a_eq_h₁, rest], - apply list.no_confusion rest, intros [b_eq_h₂, l₁_eq], + apply list.no_confusion e, intro a_eq_h₁ rest, + apply list.no_confusion rest, intro b_eq_h₂ l₁_eq, rewrite [a_eq_h₁ at H₃, b_eq_h₂ at H₃], exact H₃ t₂ rfl l₁_eq end diff --git a/library/data/num.lean b/library/data/num.lean index 0209b937dd..0f795e9e48 100644 --- a/library/data/num.lean +++ b/library/data/num.lean @@ -124,12 +124,12 @@ namespace pos_num | (bit0 a) ⌞(bit0 a)⌟ H₁ (eq.refl (bit0 a)) := begin rewrite lt_bit0_bit0_eq_lt at H₁, - apply (ne_of_lt_eq_tt H₁ (eq.refl a)) + apply ne_of_lt_eq_tt H₁ (eq.refl a) end | (bit1 a) ⌞(bit1 a)⌟ H₁ (eq.refl (bit1 a)) := begin rewrite lt_bit1_bit1_eq_lt at H₁, - apply (ne_of_lt_eq_tt H₁ (eq.refl a)) + apply ne_of_lt_eq_tt H₁ (eq.refl a) end theorem lt_base : ∀ a : pos_num, a < succ a @@ -153,7 +153,7 @@ namespace pos_num | (bit0 a) (bit0 b) H := begin rewrite [succ_bit0, lt_bit0_bit1_eq_lt_succ, lt_bit0_bit0_eq_lt at H], - apply (lt_step H) + apply lt_step H end | (bit0 a) (bit1 b) H := begin @@ -169,7 +169,7 @@ namespace pos_num | (bit1 a) (bit1 b) H := begin rewrite [succ_bit1, lt_bit1_bit0_eq_lt, lt_bit1_bit1_eq_lt at H], - apply (lt_step H) + apply lt_step H end theorem lt_of_lt_succ_succ : ∀ {a b : pos_num}, succ a < succ b → a < b @@ -179,25 +179,25 @@ namespace pos_num | (bit0 a) one H := begin rewrite [succ_bit0 at H, succ_one at H, lt_bit1_bit0_eq_lt at H], - apply (absurd_of_eq_ff_of_eq_tt (lt_one_right_eq_ff a) H) + apply absurd_of_eq_ff_of_eq_tt (lt_one_right_eq_ff a) H end | (bit0 a) (bit0 b) H := by exact H | (bit0 a) (bit1 b) H := by exact H | (bit1 a) one H := begin rewrite [succ_bit1 at H, succ_one at H, lt_bit0_bit0_eq_lt at H], - apply (absurd_of_eq_ff_of_eq_tt (lt_one_right_eq_ff (succ a)) H) + apply absurd_of_eq_ff_of_eq_tt (lt_one_right_eq_ff (succ a)) H end | (bit1 a) (bit0 b) H := begin rewrite [succ_bit1 at H, succ_bit0 at H, lt_bit0_bit1_eq_lt_succ at H], rewrite lt_bit1_bit0_eq_lt, - apply (lt_of_lt_succ_succ H) + apply lt_of_lt_succ_succ H end | (bit1 a) (bit1 b) H := begin rewrite [lt_bit1_bit1_eq_lt, *succ_bit1 at H, lt_bit0_bit0_eq_lt at H], - apply (lt_of_lt_succ_succ H) + apply lt_of_lt_succ_succ H end theorem lt_succ_succ : ∀ {a b : pos_num}, a < b → succ a < succ b @@ -219,12 +219,12 @@ namespace pos_num | (bit1 a) (bit0 b) H := begin rewrite [succ_bit1, succ_bit0, lt_bit0_bit1_eq_lt_succ, lt_bit1_bit0_eq_lt at H], - apply (lt_succ_succ H) + apply lt_succ_succ H end | (bit1 a) (bit1 b) H := begin rewrite [lt_bit1_bit1_eq_lt at H, *succ_bit1, lt_bit0_bit0_eq_lt], - apply (lt_succ_succ H) + apply lt_succ_succ H end theorem lt_of_lt_succ : ∀ {a b : pos_num}, succ a < b → a < b @@ -236,18 +236,18 @@ namespace pos_num | (bit0 a) (bit1 b) H := begin rewrite [succ_bit0 at H, lt_bit1_bit1_eq_lt at H, lt_bit0_bit1_eq_lt_succ], - apply (lt_step H) + apply lt_step H end | (bit1 a) one H := absurd_of_eq_ff_of_eq_tt !lt_one_right_eq_ff H | (bit1 a) (bit0 b) H := begin rewrite [lt_bit1_bit0_eq_lt, succ_bit1 at H, lt_bit0_bit0_eq_lt at H], - apply (lt_of_lt_succ H) + apply lt_of_lt_succ H end | (bit1 a) (bit1 b) H := begin rewrite [succ_bit1 at H, lt_bit0_bit1_eq_lt_succ at H, lt_bit1_bit1_eq_lt], - apply (lt_of_lt_succ_succ H) + apply lt_of_lt_succ_succ H end theorem lt_of_lt_succ_of_ne : ∀ {a b : pos_num}, a < succ b → a ≠ b → a < b @@ -257,12 +257,12 @@ namespace pos_num | (bit0 a) one H₁ H₂ := begin rewrite [succ_one at H₁, lt_bit0_bit0_eq_lt at H₁], - apply (absurd_of_eq_ff_of_eq_tt (lt_one_right_eq_ff _) H₁) + apply absurd_of_eq_ff_of_eq_tt (lt_one_right_eq_ff _) H₁ end | (bit0 a) (bit0 b) H₁ H₂ := begin rewrite [lt_bit0_bit0_eq_lt, succ_bit0 at H₁, lt_bit0_bit1_eq_lt_succ at H₁], - apply (lt_of_lt_succ_of_ne H₁ (ne_of_bit0_ne_bit0 H₂)) + apply lt_of_lt_succ_of_ne H₁ (ne_of_bit0_ne_bit0 H₂) end | (bit0 a) (bit1 b) H₁ H₂ := begin @@ -272,7 +272,7 @@ namespace pos_num | (bit1 a) one H₁ H₂ := begin rewrite [succ_one at H₁, lt_bit1_bit0_eq_lt at H₁], - apply (absurd_of_eq_ff_of_eq_tt (lt_one_right_eq_ff _) H₁) + apply absurd_of_eq_ff_of_eq_tt (lt_one_right_eq_ff _) H₁ end | (bit1 a) (bit0 b) H₁ H₂ := begin @@ -282,7 +282,7 @@ namespace pos_num | (bit1 a) (bit1 b) H₁ H₂ := begin rewrite [succ_bit1 at H₁, lt_bit1_bit0_eq_lt at H₁, lt_bit1_bit1_eq_lt], - apply (lt_of_lt_succ_of_ne H₁ (ne_of_bit1_ne_bit1 H₂)) + apply lt_of_lt_succ_of_ne H₁ (ne_of_bit1_ne_bit1 H₂) end theorem lt_trans : ∀ {a b c : pos_num}, a < b → b < c → a < c @@ -292,56 +292,56 @@ namespace pos_num | a (bit1 b) one H₁ H₂ := absurd_of_eq_ff_of_eq_tt (lt_one_right_eq_ff _) H₂ | (bit0 a) (bit0 b) (bit0 c) H₁ H₂ := begin - rewrite lt_bit0_bit0_eq_lt at *, apply (lt_trans H₁ H₂) + rewrite lt_bit0_bit0_eq_lt at *, apply lt_trans H₁ H₂ end | (bit0 a) (bit0 b) (bit1 c) H₁ H₂ := begin rewrite [lt_bit0_bit1_eq_lt_succ at *, lt_bit0_bit0_eq_lt at H₁], - apply (lt_trans H₁ H₂) + apply lt_trans H₁ H₂ end | (bit0 a) (bit1 b) (bit0 c) H₁ H₂ := begin rewrite [lt_bit0_bit1_eq_lt_succ at H₁, lt_bit1_bit0_eq_lt at H₂, lt_bit0_bit0_eq_lt], - apply (@by_cases (a = b)), + apply @by_cases (a = b), begin intro H, rewrite -H at H₂, exact H₂ end, begin intro H, - apply (lt_trans (lt_of_lt_succ_of_ne H₁ H) H₂) + apply lt_trans (lt_of_lt_succ_of_ne H₁ H) H₂ end end | (bit0 a) (bit1 b) (bit1 c) H₁ H₂ := begin rewrite [lt_bit0_bit1_eq_lt_succ at *, lt_bit1_bit1_eq_lt at H₂], - apply (lt_trans H₁ (lt_succ_succ H₂)) + apply lt_trans H₁ (lt_succ_succ H₂) end | (bit1 a) (bit0 b) (bit0 c) H₁ H₂ := begin rewrite [lt_bit0_bit0_eq_lt at H₂, lt_bit1_bit0_eq_lt at *], - apply (lt_trans H₁ H₂) + apply lt_trans H₁ H₂ end | (bit1 a) (bit0 b) (bit1 c) H₁ H₂ := begin rewrite [lt_bit1_bit0_eq_lt at H₁, lt_bit0_bit1_eq_lt_succ at H₂, lt_bit1_bit1_eq_lt], - apply (@by_cases (b = c)), + apply @by_cases (b = c), begin intro H, rewrite H at H₁, exact H₁ end, begin intro H, - apply (lt_trans H₁ (lt_of_lt_succ_of_ne H₂ H)) + apply lt_trans H₁ (lt_of_lt_succ_of_ne H₂ H) end end | (bit1 a) (bit1 b) (bit0 c) H₁ H₂ := begin rewrite [lt_bit1_bit1_eq_lt at H₁, lt_bit1_bit0_eq_lt at H₂, lt_bit1_bit0_eq_lt], - apply (lt_trans H₁ H₂) + apply lt_trans H₁ H₂ end | (bit1 a) (bit1 b) (bit1 c) H₁ H₂ := begin rewrite lt_bit1_bit1_eq_lt at *, - apply (lt_trans H₁ H₂) + apply lt_trans H₁ H₂ end theorem lt_antisymm : ∀ {a b : pos_num}, a < b → b ≮ a @@ -352,7 +352,7 @@ namespace pos_num | (bit0 a) (bit0 b) H := begin rewrite lt_bit0_bit0_eq_lt at *, - apply (lt_antisymm H) + apply lt_antisymm H end | (bit0 a) (bit1 b) H := begin @@ -361,19 +361,19 @@ namespace pos_num have H₁ : succ b ≮ a, from lt_antisymm H, apply eq_ff_of_ne_tt, intro H₂, - apply (@by_cases (succ b = a)), + apply @by_cases (succ b = a), show succ b = a → false, begin intro Hp, rewrite -Hp at H, - apply (absurd_of_eq_ff_of_eq_tt (lt_irrefl (succ b)) H) + apply absurd_of_eq_ff_of_eq_tt (lt_irrefl (succ b)) H end, show succ b ≠ a → false, begin intro Hn, have H₃ : succ b < succ a, from lt_succ_succ H₂, have H₄ : succ b < a, from lt_of_lt_succ_of_ne H₃ Hn, - apply (absurd_of_eq_ff_of_eq_tt H₁ H₄) + apply absurd_of_eq_ff_of_eq_tt H₁ H₄ end, end | (bit1 a) one H := absurd H ff_ne_tt @@ -384,24 +384,24 @@ namespace pos_num have H₁ : lt b a = ff, from lt_antisymm H, apply eq_ff_of_ne_tt, intro H₂, - apply (@by_cases (b = a)), + apply @by_cases (b = a), show b = a → false, begin intro Hp, rewrite -Hp at H, - apply (absurd_of_eq_ff_of_eq_tt (lt_irrefl b) H) + apply absurd_of_eq_ff_of_eq_tt (lt_irrefl b) H end, show b ≠ a → false, begin intro Hn, have H₃ : b < a, from lt_of_lt_succ_of_ne H₂ Hn, - apply (absurd_of_eq_ff_of_eq_tt H₁ H₃) + apply absurd_of_eq_ff_of_eq_tt H₁ H₃ end, end | (bit1 a) (bit1 b) H := begin rewrite lt_bit1_bit1_eq_lt at *, - apply (lt_antisymm H) + apply lt_antisymm H end local notation a ≤ b := (le a b = tt) @@ -419,56 +419,56 @@ namespace pos_num | (bit0 a) one H₁ H₂ := begin rewrite [le_eq_lt_succ at H₁, succ_one at H₁, lt_bit0_bit0_eq_lt at H₁], - apply (absurd_of_eq_ff_of_eq_tt (lt_one_right_eq_ff _) H₁) + apply absurd_of_eq_ff_of_eq_tt (lt_one_right_eq_ff _) H₁ end | (bit0 a) (bit0 b) H₁ H₂ := begin rewrite [le_eq_lt_succ at H₁, succ_bit0 at H₁, lt_bit0_bit1_eq_lt_succ at H₁], rewrite [lt_bit0_bit0_eq_lt at H₂], - apply (not_lt_of_le H₁ H₂) + apply not_lt_of_le H₁ H₂ end | (bit0 a) (bit1 b) H₁ H₂ := begin rewrite [le_eq_lt_succ at H₁, succ_bit1 at H₁, lt_bit0_bit0_eq_lt at H₁], rewrite [lt_bit1_bit0_eq_lt at H₂], - apply (not_lt_of_le H₁ H₂) + apply not_lt_of_le H₁ H₂ end | (bit1 a) one H₁ H₂ := begin rewrite [le_eq_lt_succ at H₁, succ_one at H₁, lt_bit1_bit0_eq_lt at H₁], - apply (absurd_of_eq_ff_of_eq_tt (lt_one_right_eq_ff _) H₁) + apply absurd_of_eq_ff_of_eq_tt (lt_one_right_eq_ff _) H₁ end | (bit1 a) (bit0 b) H₁ H₂ := begin rewrite [le_eq_lt_succ at H₁, succ_bit0 at H₁, lt_bit1_bit1_eq_lt at H₁], rewrite lt_bit0_bit1_eq_lt_succ at H₂, have H₃ : a < succ b, from lt_step H₁, - apply (@by_cases (b = a)), + apply @by_cases (b = a), begin intro Hba, rewrite -Hba at H₁, - apply (absurd_of_eq_ff_of_eq_tt (lt_irrefl b) H₁) + apply absurd_of_eq_ff_of_eq_tt (lt_irrefl b) H₁ end, begin intro Hnba, have H₄ : b < a, from lt_of_lt_succ_of_ne H₂ Hnba, - apply (not_lt_of_le H₃ H₄) + apply not_lt_of_le H₃ H₄ end end | (bit1 a) (bit1 b) H₁ H₂ := begin rewrite [le_eq_lt_succ at H₁, succ_bit1 at H₁, lt_bit1_bit0_eq_lt at H₁], rewrite [lt_bit1_bit1_eq_lt at H₂], - apply (not_lt_of_le H₁ H₂) + apply not_lt_of_le H₁ H₂ end theorem le_antisymm : ∀ {a b : pos_num}, a ≤ b → b ≤ a → a = b | one one H₁ H₂ := rfl | one (bit0 b) H₁ H₂ := - by apply (absurd_of_eq_ff_of_eq_tt (lt_one_right_eq_ff b) H₂) + by apply absurd_of_eq_ff_of_eq_tt (lt_one_right_eq_ff b) H₂ | one (bit1 b) H₁ H₂ := - by apply (absurd_of_eq_ff_of_eq_tt (lt_one_right_eq_ff b) H₂) + by apply absurd_of_eq_ff_of_eq_tt (lt_one_right_eq_ff b) H₂ | (bit0 a) one H₁ H₂ := - by apply (absurd_of_eq_ff_of_eq_tt (lt_one_right_eq_ff a) H₁) + by apply absurd_of_eq_ff_of_eq_tt (lt_one_right_eq_ff a) H₁ | (bit0 a) (bit0 b) H₁ H₂ := begin rewrite [le_eq_lt_succ at *, succ_bit0 at *, lt_bit0_bit1_eq_lt_succ at *], @@ -479,15 +479,15 @@ namespace pos_num begin rewrite [le_eq_lt_succ at *, succ_bit1 at H₁, succ_bit0 at H₂], rewrite [lt_bit0_bit0_eq_lt at H₁, lt_bit1_bit1_eq_lt at H₂], - apply (false.rec _ (not_lt_of_le H₁ H₂)) + apply false.rec _ (not_lt_of_le H₁ H₂) end | (bit1 a) one H₁ H₂ := - by apply (absurd_of_eq_ff_of_eq_tt (lt_one_right_eq_ff a) H₁) + by apply absurd_of_eq_ff_of_eq_tt (lt_one_right_eq_ff a) H₁ | (bit1 a) (bit0 b) H₁ H₂ := begin rewrite [le_eq_lt_succ at *, succ_bit0 at H₁, succ_bit1 at H₂], rewrite [lt_bit1_bit1_eq_lt at H₁, lt_bit0_bit0_eq_lt at H₂], - apply (false.rec _ (not_lt_of_le H₂ H₁)) + apply false.rec _ (not_lt_of_le H₂ H₁) end | (bit1 a) (bit1 b) H₁ H₂ := begin @@ -498,16 +498,16 @@ namespace pos_num theorem le_trans {a b c : pos_num} : a ≤ b → b ≤ c → a ≤ c := begin - intros [H₁, H₂], + intro H₁ H₂, rewrite [le_eq_lt_succ at *], - apply (@by_cases (a = b)), + apply @by_cases (a = b), begin intro Hab, rewrite Hab, exact H₂ end, begin intro Hnab, have Haltb : a < b, from lt_of_lt_succ_of_ne H₁ Hnab, - apply (lt_trans Haltb H₂) + apply lt_trans Haltb H₂ end, end diff --git a/library/data/vector.lean b/library/data/vector.lean index 2231063a80..00b7934057 100644 --- a/library/data/vector.lean +++ b/library/data/vector.lean @@ -125,7 +125,7 @@ namespace vector have H₁ : append t [] == t, from append_nil t, revert H₁, generalize (append t []), rewrite [-add_eq_addl, add_zero], - intros [w, H₁], + intro w H₁, rewrite [heq.to_eq H₁], apply heq.refl end diff --git a/library/init/nat.lean b/library/init/nat.lean index 82751847e6..5d25e5911e 100644 --- a/library/init/nat.lean +++ b/library/init/nat.lean @@ -124,9 +124,9 @@ namespace nat definition eq_or_lt_of_le {a b : nat} (H : a ≤ b) : a = b ∨ a < b := begin - cases H with [b, hlt], - apply (or.inl rfl), - apply (or.inr hlt) + cases H with b hlt, + apply or.inl rfl, + apply or.inr hlt end definition le_of_eq_or_lt {a b : nat} (H : a = b ∨ a < b) : a ≤ b := @@ -139,9 +139,9 @@ namespace nat definition le.rec_on {a : nat} {P : nat → Prop} {b : nat} (H : a ≤ b) (H₁ : P a) (H₂ : ∀ b, a < b → P b) : P b := begin - cases H with [b', hlt], + cases H with b' hlt, apply H₁, - apply (H₂ b' hlt) + apply H₂ b' hlt end definition lt.irrefl (a : nat) : ¬ a < a := @@ -188,23 +188,23 @@ namespace nat definition le.trans {a b c : nat} (h₁ : a ≤ b) (h₂ : b ≤ c) : a ≤ c := begin - cases h₁ with [b', hlt], + cases h₁ with b' hlt, apply h₂, - apply (lt.trans hlt h₂) + apply lt.trans hlt h₂ end definition lt_of_le_of_lt {a b c : nat} (h₁ : a ≤ b) (h₂ : b < c) : a < c := begin - cases h₁ with [b', hlt], + cases h₁ with b' hlt, apply h₂, - apply (lt.trans hlt h₂) + apply lt.trans hlt h₂ end definition lt_of_lt_of_le {a b c : nat} (h₁ : a < b) (h₂ : b ≤ c) : a < c := begin - cases h₁ with [b', hlt], - apply (lt_of_succ_lt_succ h₂), - apply (lt.trans hlt (lt_of_succ_lt_succ h₂)) + cases h₁ with b' hlt, + apply lt_of_succ_lt_succ h₂, + apply lt.trans hlt (lt_of_succ_lt_succ h₂) end calc_trans lt.trans diff --git a/library/init/tactic.lean b/library/init/tactic.lean index ec6e5dd3fd..998225af6e 100644 --- a/library/init/tactic.lean +++ b/library/init/tactic.lean @@ -67,10 +67,10 @@ definition opt_identifier_list := expr_list opaque definition apply (e : expr) : tactic := builtin opaque definition fapply (e : expr) : tactic := builtin opaque definition rename (a b : identifier) : tactic := builtin -opaque definition intro (e : identifier) : tactic := builtin -opaque definition generalize (e : expr) : tactic := builtin -opaque definition clear (e : identifier) : tactic := builtin -opaque definition revert (e : identifier) : tactic := builtin +opaque definition intro (e : identifier_list) : tactic := builtin +opaque definition generalize (e : expr) : tactic := builtin +opaque definition clear (e : identifier_list) : tactic := builtin +opaque definition revert (e : identifier_list) : tactic := builtin opaque definition refine (e : expr) : tactic := builtin opaque definition exact (e : expr) : tactic := builtin -- Relaxed version of exact that does not enforce goal type diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index 9d2bb288f1..2dc6caf632 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -1414,15 +1414,23 @@ expr parser::parse_tactic_expr_list() { expr parser::parse_tactic_id_list() { auto p = pos(); - check_token_next(get_lbracket_tk(), "invalid tactic, '[' expected"); buffer args; - while (true) { - args.push_back(mk_local(check_id_next("invalid tactic, identifier expected"), mk_expr_placeholder())); - if (!curr_is_token(get_comma_tk())) - break; - next(); + if (curr_is_identifier()) { + while (curr_is_identifier()) { + name id = get_name_val(); + args.push_back(mk_local(id, mk_expr_placeholder())); + next(); + } + } else { + check_token_next(get_lbracket_tk(), "invalid tactic, '[' or identifier expected"); + while (true) { + args.push_back(mk_local(check_id_next("invalid tactic, identifier expected"), mk_expr_placeholder())); + if (!curr_is_token(get_comma_tk())) + break; + next(); + } + check_token_next(get_rbracket_tk(), "invalid tactic, ',' or ']' expected"); } - check_token_next(get_rbracket_tk(), "invalid tactic, ',' or ']' expected"); return mk_tactic_expr_list(args, p); } @@ -1438,7 +1446,7 @@ expr parser::parse_tactic_opt_expr_list() { } expr parser::parse_tactic_opt_id_list() { - if (curr_is_token(get_lbracket_tk())) { + if (curr_is_token(get_lbracket_tk()) || curr_is_identifier()) { return parse_tactic_id_list(); } else if (curr_is_token(get_with_tk())) { next(); diff --git a/src/library/tactic/clear_tactic.cpp b/src/library/tactic/clear_tactic.cpp index 946d319d16..6ef34dbebb 100644 --- a/src/library/tactic/clear_tactic.cpp +++ b/src/library/tactic/clear_tactic.cpp @@ -55,23 +55,19 @@ tactic clear_tactic(name const & n) { } void initialize_clear_tactic() { - register_tac(get_tactic_clear_name(), - [](type_checker &, elaborate_fn const &, expr const & e, pos_info_provider const *) { - name n = tactic_expr_to_id(app_arg(e), "invalid 'clear' tactic, argument must be an identifier"); - return clear_tactic(n); - }); - register_tac(get_tactic_clears_name(), - [](type_checker &, elaborate_fn const &, expr const & e, pos_info_provider const *) { - buffer ns; - get_tactic_id_list_elements(app_arg(e), ns, "invalid 'clears' tactic, list of identifiers expected"); - tactic r = clear_tactic(ns.back()); - ns.pop_back(); - while (!ns.empty()) { - r = then(clear_tactic(ns.back()), r); - ns.pop_back(); - } - return r; - }); + auto fn = [](type_checker &, elaborate_fn const &, expr const & e, pos_info_provider const *) { + buffer ns; + get_tactic_id_list_elements(app_arg(e), ns, "invalid 'clears' tactic, list of identifiers expected"); + tactic r = clear_tactic(ns.back()); + ns.pop_back(); + while (!ns.empty()) { + r = then(clear_tactic(ns.back()), r); + ns.pop_back(); + } + return r; + }; + register_tac(get_tactic_clear_name(), fn); + register_tac(get_tactic_clears_name(), fn); } void finalize_clear_tactic() {} } diff --git a/src/library/tactic/intros_tactic.cpp b/src/library/tactic/intros_tactic.cpp index c625191792..3cd0969e6c 100644 --- a/src/library/tactic/intros_tactic.cpp +++ b/src/library/tactic/intros_tactic.cpp @@ -60,17 +60,13 @@ tactic intros_tactic(list _ns, bool relax_main_opaque) { } void initialize_intros_tactic() { - register_tac(get_tactic_intro_name(), - [](type_checker &, elaborate_fn const &, expr const & e, pos_info_provider const *) { - name const & id = tactic_expr_to_id(app_arg(e), "invalid 'intro' tactic, argument must be an identifier"); - return intros_tactic(to_list(id)); - }); - register_tac(get_tactic_intros_name(), - [](type_checker &, elaborate_fn const &, expr const & e, pos_info_provider const *) { - buffer ns; - get_tactic_id_list_elements(app_arg(e), ns, "invalid 'intros' tactic, arguments must be identifiers"); - return intros_tactic(to_list(ns.begin(), ns.end())); - }); + auto fn = [](type_checker &, elaborate_fn const &, expr const & e, pos_info_provider const *) { + buffer ns; + get_tactic_id_list_elements(app_arg(e), ns, "invalid 'intro' tactic, arguments must be identifiers"); + return intros_tactic(to_list(ns.begin(), ns.end())); + }; + register_tac(get_tactic_intro_name(), fn); + register_tac(get_tactic_intros_name(), fn); } void finalize_intros_tactic() { diff --git a/src/library/tactic/revert_tactic.cpp b/src/library/tactic/revert_tactic.cpp index a5b85c723f..a6cf0bd356 100644 --- a/src/library/tactic/revert_tactic.cpp +++ b/src/library/tactic/revert_tactic.cpp @@ -48,21 +48,16 @@ tactic revert_tactic(name const & n) { } void initialize_revert_tactic() { - register_tac(get_tactic_revert_name(), - [](type_checker &, elaborate_fn const &, expr const & e, pos_info_provider const *) { - name n = tactic_expr_to_id(app_arg(e), "invalid 'revert' tactic, argument must be an identifier"); - return revert_tactic(n); - }); - - register_tac(get_tactic_reverts_name(), - [](type_checker &, elaborate_fn const &, expr const & e, pos_info_provider const *) { - buffer ns; - get_tactic_id_list_elements(app_arg(e), ns, "invalid 'reverts' tactic, list of identifiers expected"); - tactic r = revert_tactic(ns[0]); - for (unsigned i = 1; i < ns.size(); i++) - r = then(revert_tactic(ns[i]), r); - return r; - }); + auto fn = [](type_checker &, elaborate_fn const &, expr const & e, pos_info_provider const *) { + buffer ns; + get_tactic_id_list_elements(app_arg(e), ns, "invalid 'reverts' tactic, list of identifiers expected"); + tactic r = revert_tactic(ns[0]); + for (unsigned i = 1; i < ns.size(); i++) + r = then(revert_tactic(ns[i]), r); + return r; + }; + register_tac(get_tactic_revert_name(), fn); + register_tac(get_tactic_reverts_name(), fn); } void finalize_revert_tactic() {} } diff --git a/tests/lean/errors.lean.expected.out b/tests/lean/errors.lean.expected.out index 2cc5b45bd4..b5e731f474 100644 --- a/tests/lean/errors.lean.expected.out +++ b/tests/lean/errors.lean.expected.out @@ -1,6 +1,6 @@ errors.lean:4:0: error: unknown identifier 'a' tst1 : nat → nat → nat -errors.lean:12:12: error: invalid tactic expression +errors.lean:12:16: error: invalid 'begin-end' expression, ',' expected errors.lean:22:12: error: unknown identifier 'b' tst3 : A → A → A foo.tst1 : ℕ → ℕ → ℕ