michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(frontends/lean): nicer syntax for 'intros' 'reverts' and 'clears'

Browse source
This commit is contained in:
Leonardo de Moura 2015-04-30 11:00:39 -07:00
parent f60dc8ae8f
commit 3912bc24c8
39 changed files with 268 additions and 273 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
hott/algebra/category/adjoint.hlean
View file

@ -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,

2
hott/algebra/category/category.hlean
View file

@ -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,

2
hott/algebra/category/constructions/functor.hlean
View file

@ -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,

16
hott/algebra/category/functor.hlean
View file

@ -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

12
hott/algebra/category/groupoid.hlean
View file

@ -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,

8
hott/algebra/category/iso.hlean
View file

@ -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 :=

2
hott/algebra/category/nat_trans.hlean
View file

@ -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,

12
hott/algebra/category/yoneda.hlean
View file

@ -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

2
hott/hit/coeq.hlean
View file

@ -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)

4
hott/hit/colimit.hlean
View file

@ -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)

2
hott/hit/cylinder.hlean
View file

@ -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)

2
hott/hit/pushout.hlean
View file

@ -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)

2
hott/hit/quotient.hlean
View file

@ -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

4
hott/hit/trunc.hlean
View file

@ -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},

18
hott/init/nat.hlean
View file

@ -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 :=

24
hott/init/tactic.hlean
View file

@ -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.

30
hott/types/W.hlean
View file

@ -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

22
hott/types/equiv.hlean
View file

@ -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

2
hott/types/function.hlean
View file

@ -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},

10
hott/types/hprop_trunc.hlean
View file

@ -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},

8
hott/types/pi.hlean
View file

@ -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,

10
hott/types/prod.hlean
View file

@ -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 -/

28
hott/types/sigma.hlean
View file

@ -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,

38
hott/types/trunc.hlean
View file

@ -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

4
library/algebra/ordered_field.lean
View file

@ -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

16
library/algebra/ordered_ring.lean
View file

@ -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,

2
library/data/encodable.lean
View file

@ -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)

8
library/data/fintype.lean
View file

@ -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)

2
library/data/list/comb.lean
View file

@ -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

10
library/data/list/perm.lean
View file

@ -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

104
library/data/num.lean
View file

@ -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

2
library/data/vector.lean
View file

@ -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

24
library/init/nat.lean
View file

@ -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

8
library/init/tactic.lean
View file

@ -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

24
src/frontends/lean/parser.cpp
View file

@ -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<expr> 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();

30
src/library/tactic/clear_tactic.cpp
View file

@ -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<name> 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<name> 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() {}
}

18
src/library/tactic/intros_tactic.cpp
View file

@ -60,17 +60,13 @@ tactic intros_tactic(list<name> _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<name> 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<name> 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() {

25
src/library/tactic/revert_tactic.cpp
View file

@ -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<name> 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<name> 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() {}
}

2
tests/lean/errors.lean.expected.out
View file

@ -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 : ℕ → ℕ → ℕ