From a35cce38b36fed525e9424338eae7b766d9f07ea Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 11 Feb 2015 12:49:27 -0800 Subject: [PATCH] feat(frontends/lean): new semantics for "protected" declarations closes #426 --- hott/algebra/precategory/constructions.hlean | 2 +- .../precategory/natural_transformation.hlean | 14 +- hott/init/axioms/funext.hlean | 2 +- hott/init/bool.hlean | 8 +- hott/init/equiv.hlean | 12 +- hott/init/logic.hlean | 10 +- hott/init/nat.hlean | 60 ++--- hott/init/num.hlean | 26 +-- hott/init/path.hlean | 210 +++++++++--------- hott/init/types/empty.hlean | 2 +- hott/init/types/prod.hlean | 6 +- hott/init/wf.hlean | 2 +- .../category/natural_transformation.lean | 18 +- library/data/bool.lean | 58 ++--- library/data/empty.lean | 2 +- library/data/int/basic.lean | 60 ++--- library/data/int/order.lean | 8 +- library/data/list/basic.lean | 14 +- library/data/nat/basic.lean | 42 ++-- library/data/nat/div.lean | 20 +- library/data/nat/order.lean | 10 +- library/data/nat/sub.lean | 14 +- library/data/num.lean | 6 +- library/data/option.lean | 12 +- library/data/sum.lean | 8 +- library/data/unit.lean | 4 +- library/init/bool.lean | 8 +- library/init/datatypes.lean | 4 +- library/init/logic.lean | 20 +- library/init/nat.lean | 40 ++-- library/init/num.lean | 22 +- library/init/prod.lean | 6 +- library/init/sigma.lean | 4 +- library/logic/cast.lean | 2 +- library/logic/eq.lean | 12 +- library/logic/subsingleton.lean | 2 +- src/frontends/lean/parser.cpp | 4 +- src/frontends/lean/pp.cpp | 5 +- src/frontends/lean/server.cpp | 10 +- tests/lean/hott/noc.hlean | 2 +- tests/lean/hott/noc_list.hlean | 6 +- tests/lean/hott/sig_noc.hlean | 4 +- tests/lean/interactive/auto_comp.input | 15 ++ .../interactive/auto_comp.input.expected.out | 12 + tests/lean/interactive/eq2.input | 2 +- tests/lean/interactive/eq2.lean | 4 +- tests/lean/interactive/extra_type.input | 28 +-- .../interactive/extra_type.input.expected.out | 4 +- .../lean/interactive/num2.input.expected.out | 4 - tests/lean/protected_test.lean | 11 + tests/lean/protected_test.lean.expected.out | 7 + tests/lean/run/class_bug1.lean | 4 +- tests/lean/run/class_bug2.lean | 4 +- tests/lean/run/div2.lean | 4 +- tests/lean/run/enum.lean | 4 +- tests/lean/run/example1.lean | 2 +- tests/lean/run/fib_brec.lean | 22 +- tests/lean/run/ftree_brec.lean | 26 +-- tests/lean/run/inf_tree.lean | 2 +- tests/lean/run/inf_tree2.lean | 2 +- tests/lean/run/lift.lean | 4 +- tests/lean/run/nat_bug.lean | 4 +- tests/lean/run/nat_bug5.lean | 2 +- tests/lean/run/nested_begin.lean | 12 +- tests/lean/run/sigma_no_confusion.lean | 10 +- tests/lean/run/sum_bug.lean | 12 +- tests/lean/run/tree.lean | 16 +- tests/lean/run/tree2.lean | 16 +- tests/lean/run/tree3.lean | 6 +- tests/lean/run/tree_height.lean | 2 +- tests/lean/run/univ_problem.lean | 40 ++-- tests/lean/run/vector.lean | 37 +-- tests/lean/run/vector2.lean | 2 +- tests/lean/run/vector3.lean | 4 +- tests/lean/slow/nat_bug2.lean | 64 +++--- tests/lean/slow/nat_wo_hints.lean | 64 +++--- tests/lean/slow/path_groupoids.lean | 186 ++++++++-------- 77 files changed, 738 insertions(+), 681 deletions(-) create mode 100644 tests/lean/interactive/auto_comp.input create mode 100644 tests/lean/interactive/auto_comp.input.expected.out create mode 100644 tests/lean/protected_test.lean create mode 100644 tests/lean/protected_test.lean.expected.out diff --git a/hott/algebra/precategory/constructions.hlean b/hott/algebra/precategory/constructions.hlean index 5b8bfe8d2..a1a2b1e3b 100644 --- a/hott/algebra/precategory/constructions.hlean +++ b/hott/algebra/precategory/constructions.hlean @@ -38,7 +38,7 @@ namespace precategory -- symmetric associativity proof. definition op_op' {ob : Type} (C : precategory ob) : opposite (opposite C) = C := begin - apply (rec_on C), intros (hom', homH', comp', ID', assoc', id_left', id_right'), + apply (precategory.rec_on C), intros (hom', homH', comp', ID', assoc', id_left', id_right'), apply (ap (λassoc'', precategory.mk hom' @homH' comp' ID' assoc'' id_left' id_right')), repeat ( apply funext.path_pi ; intros ), apply ap, diff --git a/hott/algebra/precategory/natural_transformation.hlean b/hott/algebra/precategory/natural_transformation.hlean index b3283a160..5af8fa6e1 100644 --- a/hott/algebra/precategory/natural_transformation.hlean +++ b/hott/algebra/precategory/natural_transformation.hlean @@ -16,10 +16,10 @@ namespace natural_transformation variables {C D : Precategory} {F G H I : functor C D} definition natural_map [coercion] (η : F ⟹ G) : Π (a : C), F a ⟶ G a := - rec (λ x y, x) η + natural_transformation.rec (λ x y, x) η theorem naturality (η : F ⟹ G) : Π⦃a b : C⦄ (f : a ⟶ b), G f ∘ η a = η b ∘ F f := - rec (λ x y, y) η + natural_transformation.rec (λ x y, y) η protected definition compose (η : G ⟹ H) (θ : F ⟹ G) : F ⟹ H := natural_transformation.mk @@ -52,9 +52,9 @@ namespace natural_transformation protected definition assoc (η₃ : H ⟹ I) (η₂ : G ⟹ H) (η₁ : F ⟹ G) : η₃ ∘n (η₂ ∘n η₁) = (η₃ ∘n η₂) ∘n η₁ := begin - apply (rec_on η₃), intros (η₃1, η₃2), - apply (rec_on η₂), intros (η₂1, η₂2), - apply (rec_on η₁), intros (η₁1, η₁2), + apply (natural_transformation.rec_on η₃), intros (η₃1, η₃2), + apply (natural_transformation.rec_on η₂), intros (η₂1, η₂2), + apply (natural_transformation.rec_on η₁), intros (η₁1, η₁2), fapply natural_transformation.congr, apply funext.path_pi, intro a, apply assoc, @@ -72,7 +72,7 @@ namespace natural_transformation protected definition id_left (η : F ⟹ G) : id ∘n η = η := begin - apply (rec_on η), intros (η₁, nat₁), + apply (natural_transformation.rec_on η), intros (η₁, nat₁), fapply (natural_transformation.congr F G), apply funext.path_pi, intro a, apply id_left, @@ -84,7 +84,7 @@ namespace natural_transformation protected definition id_right (η : F ⟹ G) : η ∘n id = η := begin - apply (rec_on η), intros (η₁, nat₁), + apply (natural_transformation.rec_on η), intros (η₁, nat₁), fapply (natural_transformation.congr F G), apply funext.path_pi, intro a, apply id_right, diff --git a/hott/init/axioms/funext.hlean b/hott/init/axioms/funext.hlean index 110b876ac..d5c68242d 100644 --- a/hott/init/axioms/funext.hlean +++ b/hott/init/axioms/funext.hlean @@ -21,7 +21,7 @@ namespace funext include F protected definition ap [instance] (f g : Π x, P x) : is_equiv (@apD10 A P f g) := - rec_on F (λ(H : Π A P f g, _), !H) + funext.rec_on F (λ(H : Π A P f g, _), !H) definition path_pi {f g : Π x, P x} : f ∼ g → f = g := is_equiv.inv (@apD10 A P f g) diff --git a/hott/init/bool.hlean b/hott/init/bool.hlean index 51893d3e4..e24781b79 100644 --- a/hott/init/bool.hlean +++ b/hott/init/bool.hlean @@ -8,18 +8,18 @@ import init.datatypes init.reserved_notation namespace bool definition cond {A : Type} (b : bool) (t e : A) := - rec_on b e t + bool.rec_on b e t definition bor (a b : bool) := - rec_on a (rec_on b ff tt) tt + bool.rec_on a (bool.rec_on b ff tt) tt notation a || b := bor a b definition band (a b : bool) := - rec_on a ff (rec_on b ff tt) + bool.rec_on a ff (bool.rec_on b ff tt) notation a && b := band a b definition bnot (a : bool) := - rec_on a tt ff + bool.rec_on a tt ff end bool diff --git a/hott/init/equiv.hlean b/hott/init/equiv.hlean index ba11648af..7af8b842a 100644 --- a/hott/init/equiv.hlean +++ b/hott/init/equiv.hlean @@ -145,13 +145,15 @@ namespace is_equiv variables {B C : Type} (f : A → B) {f' : A → B} [Hf : is_equiv f] include Hf + variable (g : B → C) + definition cancel_R (g : B → C) [Hgf : is_equiv (g ∘ f)] : (is_equiv g) := have Hfinv [visible] : is_equiv (f⁻¹), from inv_closed f, - @homotopy_closed _ _ _ _ (compose (f⁻¹) (g ∘ f)) (λb, ap g (@retr _ _ f _ b)) + @homotopy_closed _ _ _ _ (is_equiv.compose (f⁻¹) (g ∘ f)) (λb, ap g (@retr _ _ f _ b)) definition cancel_L (g : C → A) [Hgf : is_equiv (f ∘ g)] : (is_equiv g) := have Hfinv [visible] : is_equiv (f⁻¹), from inv_closed f, - @homotopy_closed _ _ _ _ (compose (f ∘ g) (f⁻¹)) (λa, sect f (g a)) + @homotopy_closed _ _ _ _ (is_equiv.compose (f ∘ g) (f⁻¹)) (λa, sect f (g a)) --Rewrite rules definition moveR_M {x : A} {y : B} (p : x = (inv f) y) : (f x = y) := @@ -260,8 +262,8 @@ namespace equiv -- calc enviroment -- Note: Calculating with substitutions needs univalence - calc_trans trans - calc_refl refl - calc_symm symm + calc_trans equiv.trans + calc_refl equiv.refl + calc_symm equiv.symm end equiv diff --git a/hott/init/logic.hlean b/hott/init/logic.hlean index 12dbff7ab..1067fd16c 100644 --- a/hott/init/logic.hlean +++ b/hott/init/logic.hlean @@ -46,7 +46,7 @@ namespace eq variables {a b c a' : A} definition subst {P : A → Type} (H₁ : a = b) (H₂ : P a) : P b := - rec H₂ H₁ + eq.rec H₂ H₁ definition trans (H₁ : a = b) (H₂ : b = c) : a = c := subst H₂ H₁ @@ -211,13 +211,13 @@ namespace decidable variables {p q : Type} definition pos_witness [C : decidable p] (H : p) : p := - rec_on C (λ Hp, Hp) (λ Hnp, absurd H Hnp) + decidable.rec_on C (λ Hp, Hp) (λ Hnp, absurd H Hnp) definition neg_witness [C : decidable p] (H : ¬ p) : ¬ p := - rec_on C (λ Hp, absurd Hp H) (λ Hnp, Hnp) + decidable.rec_on C (λ Hp, absurd Hp H) (λ Hnp, Hnp) definition by_cases {q : Type} [C : decidable p] (Hpq : p → q) (Hnpq : ¬p → q) : q := - rec_on C (assume Hp, Hpq Hp) (assume Hnp, Hnpq Hnp) + decidable.rec_on C (assume Hp, Hpq Hp) (assume Hnp, Hnpq Hnp) definition em (p : Type) [H : decidable p] : sum p ¬p := by_cases (λ Hp, sum.inl Hp) (λ Hnp, sum.inr Hnp) @@ -228,7 +228,7 @@ namespace decidable (assume H₁ : ¬p, empty.rec (λ e, p) (H H₁)) definition decidable_iff_equiv (Hp : decidable p) (H : p ↔ q) : decidable q := - rec_on Hp + decidable.rec_on Hp (assume Hp : p, inl (iff.elim_left H Hp)) (assume Hnp : ¬p, inr (iff.elim_left (iff.flip_sign H) Hnp)) diff --git a/hott/init/nat.hlean b/hott/init/nat.hlean index c85aae01d..9ad758ab6 100644 --- a/hott/init/nat.hlean +++ b/hott/init/nat.hlean @@ -23,7 +23,7 @@ namespace nat notation a ≤ b := le a b definition pred (a : nat) : nat := - cases_on a zero (λ a₁, a₁) + nat.cases_on a zero (λ a₁, a₁) protected definition is_inhabited [instance] : inhabited nat := inhabited.mk zero @@ -31,39 +31,39 @@ namespace nat protected definition has_decidable_eq [instance] : decidable_eq nat := λn m : nat, have general : ∀n, decidable (n = m), from - rec_on m - (λ n, cases_on n + nat.rec_on m + (λ n, nat.cases_on n (inl rfl) - (λ m, inr (λ (e : succ m = zero), down (no_confusion e)))) - (λ (m' : nat) (ih : ∀n, decidable (n = m')) (n : nat), cases_on n - (inr (λ h, down (no_confusion h))) + (λ m, inr (λ (e : succ m = zero), down (nat.no_confusion e)))) + (λ (m' : nat) (ih : ∀n, decidable (n = m')) (n : nat), nat.cases_on n + (inr (λ h, down (nat.no_confusion h))) (λ (n' : nat), decidable.rec_on (ih n') (assume Heq : n' = m', inl (eq.rec_on Heq rfl)) (assume Hne : n' ≠ m', have H1 : succ n' ≠ succ m', from - assume Heq, down (no_confusion Heq (λ e : n' = m', Hne e)), + assume Heq, down (nat.no_confusion Heq (λ e : n' = m', Hne e)), inr H1))), general n -- less-than is well-founded definition lt.wf [instance] : well_founded lt := - well_founded.intro (λn, rec_on n + well_founded.intro (λn, nat.rec_on n (acc.intro zero (λ (y : nat) (hlt : y < zero), have aux : ∀ {n₁}, y < n₁ → zero = n₁ → acc lt y, from λ n₁ hlt, lt.cases_on hlt - (λ heq, down (no_confusion heq)) - (λ b hlt heq, down (no_confusion heq)), + (λ heq, down (nat.no_confusion heq)) + (λ b hlt heq, down (nat.no_confusion heq)), aux hlt rfl)) (λ (n : nat) (ih : acc lt n), acc.intro (succ n) (λ (m : nat) (hlt : m < succ n), have aux : ∀ {n₁} (hlt : m < n₁), succ n = n₁ → acc lt m, from λ n₁ hlt, lt.cases_on hlt (λ (heq : succ n = succ m), - down (no_confusion heq (λ (e : n = m), + down (nat.no_confusion heq (λ (e : n = m), eq.rec_on e ih))) (λ b (hlt : m < b) (heq : succ n = succ b), - down (no_confusion heq (λ (e : n = b), + down (nat.no_confusion heq (λ (e : n = b), acc.inv (eq.rec_on e ih) hlt))), aux hlt rfl))) @@ -76,12 +76,12 @@ namespace nat definition not_lt_zero (a : nat) : ¬ a < zero := have aux : ∀ {b}, a < b → b = zero → empty, from λ b H, lt.cases_on H - (λ heq, down (no_confusion heq)) - (λ b h₁ heq, down (no_confusion heq)), + (λ heq, down (nat.no_confusion heq)) + (λ b h₁ heq, down (nat.no_confusion heq)), λ H, aux H rfl definition zero_lt_succ (a : nat) : zero < succ a := - rec_on a + nat.rec_on a (lt.base zero) (λ a (hlt : zero < succ a), lt.step hlt) @@ -114,9 +114,9 @@ namespace nat aux definition lt.is_decidable_rel [instance] : decidable_rel lt := - λ a b, rec_on b + λ a b, nat.rec_on b (λ (a : nat), inr (not_lt_zero a)) - (λ (b₁ : nat) (ih : ∀ a, decidable (a < b₁)) (a : nat), cases_on a + (λ (b₁ : nat) (ih : ∀ a, decidable (a < b₁)) (a : nat), nat.cases_on a (inl !zero_lt_succ) (λ a, decidable.rec_on (ih a) (λ h_pos : a < b₁, inl (lt.succ_of_lt h_pos)) @@ -135,8 +135,8 @@ namespace nat definition eq_or_lt_of_le {a b : nat} (H : a ≤ b) : sum (a = b) (a < b) := have aux : Π (a₁ b₁ : nat) (hlt : a₁ < b₁), a₁ = a → b₁ = (succ b) → sum (a = b) (a < b), from λ a₁ b₁ hlt, lt.rec_on hlt - (λ h₁, eq.rec_on h₁ (λ h₂, down (no_confusion h₂ (λ h₃, eq.rec_on h₃ (sum.inl rfl))))) - (λ b₁ hlt ih h₁, eq.rec_on h₁ (λ h₂, down (no_confusion h₂ (λ h₃, eq.rec_on h₃ (sum.inr hlt))))), + (λ h₁, eq.rec_on h₁ (λ h₂, down (nat.no_confusion h₂ (λ h₃, eq.rec_on h₃ (sum.inl rfl))))) + (λ b₁ hlt ih h₁, eq.rec_on h₁ (λ h₂, down (nat.no_confusion h₂ (λ h₃, eq.rec_on h₃ (sum.inr hlt))))), aux a (succ b) H rfl rfl definition le.of_eq_or_lt {a b : nat} (H : sum (a = b) (a < b)) : a ≤ b := @@ -155,7 +155,7 @@ namespace nat end definition lt.irrefl (a : nat) : ¬ a < a := - rec_on a + nat.rec_on a !not_lt_zero (λ (a : nat) (ih : ¬ a < a) (h : succ a < succ a), ih (lt.of_succ_lt_succ h)) @@ -166,11 +166,11 @@ namespace nat (λ b hlt (ih : ¬ b < a) (h : succ b < a), ih (lt.of_succ_lt h)) definition lt.trichotomy (a b : nat) : a < b ⊎ a = b ⊎ b < a := - rec_on b - (λa, cases_on a + nat.rec_on b + (λa, nat.cases_on a (sum.inr (sum.inl rfl)) (λ a₁, sum.inr (sum.inr !zero_lt_succ))) - (λ b₁ (ih : ∀a, a < b₁ ⊎ a = b₁ ⊎ b₁ < a) (a : nat), cases_on a + (λ b₁ (ih : ∀a, a < b₁ ⊎ a = b₁ ⊎ b₁ < a) (a : nat), nat.cases_on a (sum.inl !zero_lt_succ) (λ a, sum.rec_on (ih a) (λ h : a < b₁, sum.inl (lt.succ_of_lt h)) @@ -282,23 +282,23 @@ namespace nat notation a ≥ b := ge a b definition add (a b : nat) : nat := - rec_on b a (λ b₁ r, succ r) + nat.rec_on b a (λ b₁ r, succ r) notation a + b := add a b definition sub (a b : nat) : nat := - rec_on b a (λ b₁ r, pred r) + nat.rec_on b a (λ b₁ r, pred r) notation a - b := sub a b definition mul (a b : nat) : nat := - rec_on b zero (λ b₁ r, r + a) + nat.rec_on b zero (λ b₁ r, r + a) notation a * b := mul a b local attribute sub [reducible] definition succ_sub_succ_eq_sub (a b : nat) : succ a - succ b = a - b := - rec_on b + nat.rec_on b rfl (λ b₁ (ih : succ a - succ b₁ = a - b₁), eq.rec_on ih (eq.refl (pred (succ a - succ b₁)))) @@ -307,7 +307,7 @@ namespace nat eq.rec_on (succ_sub_succ_eq_sub a b) rfl definition zero_sub_eq_zero (a : nat) : zero - a = zero := - rec_on a + nat.rec_on a rfl (λ a₁ (ih : zero - a₁ = zero), calc zero - succ a₁ = pred (zero - a₁) : rfl @@ -333,12 +333,12 @@ namespace nat λ h₁ h₂, aux h₁ h₂ definition pred_le (a : nat) : pred a ≤ a := - cases_on a + nat.cases_on a (le.refl zero) (λ a₁, le.of_lt (lt.base a₁)) definition sub_le (a b : nat) : a - b ≤ a := - rec_on b + nat.rec_on b (le.refl a) (λ b₁ ih, le.trans !pred_le ih) diff --git a/hott/init/num.hlean b/hott/init/num.hlean index a3eed88bc..0de327bb9 100644 --- a/hott/init/num.hlean +++ b/hott/init/num.hlean @@ -13,25 +13,25 @@ inhabited.mk pos_num.one namespace pos_num definition succ (a : pos_num) : pos_num := - rec_on a (bit0 one) (λn r, bit0 r) (λn r, bit1 n) + pos_num.rec_on a (bit0 one) (λn r, bit0 r) (λn r, bit1 n) definition is_one (a : pos_num) : bool := - rec_on a tt (λn r, ff) (λn r, ff) + pos_num.rec_on a tt (λn r, ff) (λn r, ff) definition pred (a : pos_num) : pos_num := - rec_on a one (λn r, bit0 n) (λn r, cond (is_one n) one (bit1 r)) + pos_num.rec_on a one (λn r, bit0 n) (λn r, cond (is_one n) one (bit1 r)) definition size (a : pos_num) : pos_num := - rec_on a one (λn r, succ r) (λn r, succ r) + pos_num.rec_on a one (λn r, succ r) (λn r, succ r) definition add (a b : pos_num) : pos_num := - rec_on a + pos_num.rec_on a succ - (λn f b, rec_on b + (λn f b, pos_num.rec_on b (succ (bit1 n)) (λm r, succ (bit1 (f m))) (λm r, bit1 (f m))) - (λn f b, rec_on b + (λn f b, pos_num.rec_on b (bit1 n) (λm r, bit1 (f m)) (λm r, bit0 (f m))) @@ -40,7 +40,7 @@ namespace pos_num notation a + b := add a b definition mul (a b : pos_num) : pos_num := - rec_on a + pos_num.rec_on a b (λn r, bit0 r + b) (λn r, bit0 r) @@ -55,19 +55,19 @@ inhabited.mk num.zero namespace num open pos_num definition succ (a : num) : num := - rec_on a (pos one) (λp, pos (succ p)) + num.rec_on a (pos one) (λp, pos (succ p)) definition pred (a : num) : num := - rec_on a zero (λp, cond (is_one p) zero (pos (pred p))) + num.rec_on a zero (λp, cond (is_one p) zero (pos (pred p))) definition size (a : num) : num := - rec_on a (pos one) (λp, pos (size p)) + num.rec_on a (pos one) (λp, pos (size p)) definition add (a b : num) : num := - rec_on a b (λp_a, rec_on b (pos p_a) (λp_b, pos (pos_num.add p_a p_b))) + num.rec_on a b (λp_a, num.rec_on b (pos p_a) (λp_b, pos (pos_num.add p_a p_b))) definition mul (a b : num) : num := - rec_on a zero (λp_a, rec_on b zero (λp_b, pos (pos_num.mul p_a p_b))) + num.rec_on a zero (λp_a, num.rec_on b zero (λp_b, pos (pos_num.mul p_a p_b))) notation a + b := add a b notation a * b := mul a b diff --git a/hott/init/path.hlean b/hott/init/path.hlean index 9aee35576..4a92903f9 100644 --- a/hott/init/path.hlean +++ b/hott/init/path.hlean @@ -48,128 +48,128 @@ namespace eq -- The identity path is a right unit. definition concat_p1 (p : x = y) : p ⬝ idp = p := - rec_on p idp + eq.rec_on p idp -- The identity path is a right unit. definition concat_1p (p : x = y) : idp ⬝ p = p := - rec_on p idp + eq.rec_on p idp -- Concatenation is associative. definition concat_p_pp (p : x = y) (q : y = z) (r : z = t) : p ⬝ (q ⬝ r) = (p ⬝ q) ⬝ r := - rec_on r (rec_on q idp) + eq.rec_on r (eq.rec_on q idp) definition concat_pp_p (p : x = y) (q : y = z) (r : z = t) : (p ⬝ q) ⬝ r = p ⬝ (q ⬝ r) := - rec_on r (rec_on q idp) + eq.rec_on r (eq.rec_on q idp) -- The left inverse law. definition concat_pV (p : x = y) : p ⬝ p⁻¹ = idp := - rec_on p idp + eq.rec_on p idp -- The right inverse law. definition concat_Vp (p : x = y) : p⁻¹ ⬝ p = idp := - rec_on p idp + eq.rec_on p idp -- Several auxiliary theorems about canceling inverses across associativity. These are somewhat -- redundant, following from earlier theorems. definition concat_V_pp (p : x = y) (q : y = z) : p⁻¹ ⬝ (p ⬝ q) = q := - rec_on q (rec_on p idp) + eq.rec_on q (eq.rec_on p idp) definition concat_p_Vp (p : x = y) (q : x = z) : p ⬝ (p⁻¹ ⬝ q) = q := - rec_on q (rec_on p idp) + eq.rec_on q (eq.rec_on p idp) definition concat_pp_V (p : x = y) (q : y = z) : (p ⬝ q) ⬝ q⁻¹ = p := - rec_on q (rec_on p idp) + eq.rec_on q (eq.rec_on p idp) definition concat_pV_p (p : x = z) (q : y = z) : (p ⬝ q⁻¹) ⬝ q = p := - rec_on q (take p, rec_on p idp) p + eq.rec_on q (take p, eq.rec_on p idp) p -- Inverse distributes over concatenation definition inv_pp (p : x = y) (q : y = z) : (p ⬝ q)⁻¹ = q⁻¹ ⬝ p⁻¹ := - rec_on q (rec_on p idp) + eq.rec_on q (eq.rec_on p idp) definition inv_Vp (p : y = x) (q : y = z) : (p⁻¹ ⬝ q)⁻¹ = q⁻¹ ⬝ p := - rec_on q (rec_on p idp) + eq.rec_on q (eq.rec_on p idp) -- universe metavariables definition inv_pV (p : x = y) (q : z = y) : (p ⬝ q⁻¹)⁻¹ = q ⬝ p⁻¹ := - rec_on p (take q, rec_on q idp) q + eq.rec_on p (take q, eq.rec_on q idp) q definition inv_VV (p : y = x) (q : z = y) : (p⁻¹ ⬝ q⁻¹)⁻¹ = q ⬝ p := - rec_on p (rec_on q idp) + eq.rec_on p (eq.rec_on q idp) -- Inverse is an involution. definition inv_V (p : x = y) : p⁻¹⁻¹ = p := - rec_on p idp + eq.rec_on p idp -- Theorems for moving things around in equations -- ---------------------------------------------- definition moveR_Mp (p : x = z) (q : y = z) (r : y = x) : p = (r⁻¹ ⬝ q) → (r ⬝ p) = q := - rec_on r (take p h, concat_1p _ ⬝ h ⬝ concat_1p _) p + eq.rec_on r (take p h, concat_1p _ ⬝ h ⬝ concat_1p _) p definition moveR_pM (p : x = z) (q : y = z) (r : y = x) : r = q ⬝ p⁻¹ → r ⬝ p = q := - rec_on p (take q h, (concat_p1 _ ⬝ h ⬝ concat_p1 _)) q + eq.rec_on p (take q h, (concat_p1 _ ⬝ h ⬝ concat_p1 _)) q definition moveR_Vp (p : x = z) (q : y = z) (r : x = y) : p = r ⬝ q → r⁻¹ ⬝ p = q := - rec_on r (take q h, concat_1p _ ⬝ h ⬝ concat_1p _) q + eq.rec_on r (take q h, concat_1p _ ⬝ h ⬝ concat_1p _) q definition moveR_pV (p : z = x) (q : y = z) (r : y = x) : r = q ⬝ p → r ⬝ p⁻¹ = q := - rec_on p (take r h, concat_p1 _ ⬝ h ⬝ concat_p1 _) r + eq.rec_on p (take r h, concat_p1 _ ⬝ h ⬝ concat_p1 _) r definition moveL_Mp (p : x = z) (q : y = z) (r : y = x) : r⁻¹ ⬝ q = p → q = r ⬝ p := - rec_on r (take p h, (concat_1p _)⁻¹ ⬝ h ⬝ (concat_1p _)⁻¹) p + eq.rec_on r (take p h, (concat_1p _)⁻¹ ⬝ h ⬝ (concat_1p _)⁻¹) p definition moveL_pM (p : x = z) (q : y = z) (r : y = x) : q ⬝ p⁻¹ = r → q = r ⬝ p := - rec_on p (take q h, (concat_p1 _)⁻¹ ⬝ h ⬝ (concat_p1 _)⁻¹) q + eq.rec_on p (take q h, (concat_p1 _)⁻¹ ⬝ h ⬝ (concat_p1 _)⁻¹) q definition moveL_Vp (p : x = z) (q : y = z) (r : x = y) : r ⬝ q = p → q = r⁻¹ ⬝ p := - rec_on r (take q h, (concat_1p _)⁻¹ ⬝ h ⬝ (concat_1p _)⁻¹) q + eq.rec_on r (take q h, (concat_1p _)⁻¹ ⬝ h ⬝ (concat_1p _)⁻¹) q definition moveL_pV (p : z = x) (q : y = z) (r : y = x) : q ⬝ p = r → q = r ⬝ p⁻¹ := - rec_on p (take r h, (concat_p1 _)⁻¹ ⬝ h ⬝ (concat_p1 _)⁻¹) r + eq.rec_on p (take r h, (concat_p1 _)⁻¹ ⬝ h ⬝ (concat_p1 _)⁻¹) r definition moveL_1M (p q : x = y) : p ⬝ q⁻¹ = idp → p = q := - rec_on q (take p h, (concat_p1 _)⁻¹ ⬝ h) p + eq.rec_on q (take p h, (concat_p1 _)⁻¹ ⬝ h) p definition moveL_M1 (p q : x = y) : q⁻¹ ⬝ p = idp → p = q := - rec_on q (take p h, (concat_1p _)⁻¹ ⬝ h) p + eq.rec_on q (take p h, (concat_1p _)⁻¹ ⬝ h) p definition moveL_1V (p : x = y) (q : y = x) : p ⬝ q = idp → p = q⁻¹ := - rec_on q (take p h, (concat_p1 _)⁻¹ ⬝ h) p + eq.rec_on q (take p h, (concat_p1 _)⁻¹ ⬝ h) p definition moveL_V1 (p : x = y) (q : y = x) : q ⬝ p = idp → p = q⁻¹ := - rec_on q (take p h, (concat_1p _)⁻¹ ⬝ h) p + eq.rec_on q (take p h, (concat_1p _)⁻¹ ⬝ h) p definition moveR_M1 (p q : x = y) : idp = p⁻¹ ⬝ q → p = q := - rec_on p (take q h, h ⬝ (concat_1p _)) q + eq.rec_on p (take q h, h ⬝ (concat_1p _)) q definition moveR_1M (p q : x = y) : idp = q ⬝ p⁻¹ → p = q := - rec_on p (take q h, h ⬝ (concat_p1 _)) q + eq.rec_on p (take q h, h ⬝ (concat_p1 _)) q definition moveR_1V (p : x = y) (q : y = x) : idp = q ⬝ p → p⁻¹ = q := - rec_on p (take q h, h ⬝ (concat_p1 _)) q + eq.rec_on p (take q h, h ⬝ (concat_p1 _)) q definition moveR_V1 (p : x = y) (q : y = x) : idp = p ⬝ q → p⁻¹ = q := - rec_on p (take q h, h ⬝ (concat_1p _)) q + eq.rec_on p (take q h, h ⬝ (concat_1p _)) q -- Transport @@ -197,10 +197,10 @@ namespace eq definition ap10 {f g : A → B} (H : f = g) : f ∼ g := apD10 H definition ap11 {f g : A → B} (H : f = g) {x y : A} (p : x = y) : f x = g y := - rec_on H (rec_on p idp) + eq.rec_on H (eq.rec_on p idp) definition apD (f : Πa:A, P a) {x y : A} (p : x = y) : p ▹ (f x) = f y := - rec_on p idp + eq.rec_on p idp -- calc enviroment @@ -216,19 +216,19 @@ namespace eq definition moveR_transport_p (P : A → Type) {x y : A} (p : x = y) (u : P x) (v : P y) : u = p⁻¹ ▹ v → p ▹ u = v := - rec_on p (take v, id) v + eq.rec_on p (take v, id) v definition moveR_transport_V (P : A → Type) {x y : A} (p : y = x) (u : P x) (v : P y) : u = p ▹ v → p⁻¹ ▹ u = v := - rec_on p (take u, id) u + eq.rec_on p (take u, id) u definition moveL_transport_V (P : A → Type) {x y : A} (p : x = y) (u : P x) (v : P y) : p ▹ u = v → u = p⁻¹ ▹ v := - rec_on p (take v, id) v + eq.rec_on p (take v, id) v definition moveL_transport_p (P : A → Type) {x y : A} (p : y = x) (u : P x) (v : P y) : p⁻¹ ▹ u = v → u = p ▹ v := - rec_on p (take u, id) u + eq.rec_on p (take u, id) u -- Functoriality of functions -- -------------------------- @@ -244,111 +244,111 @@ namespace eq -- Functions commute with concatenation. definition ap_pp (f : A → B) {x y z : A} (p : x = y) (q : y = z) : ap f (p ⬝ q) = (ap f p) ⬝ (ap f q) := - rec_on q (rec_on p idp) + eq.rec_on q (eq.rec_on p idp) definition ap_p_pp (f : A → B) {w x y z : A} (r : f w = f x) (p : x = y) (q : y = z) : r ⬝ (ap f (p ⬝ q)) = (r ⬝ ap f p) ⬝ (ap f q) := - rec_on q (take p, rec_on p (concat_p_pp r idp idp)) p + eq.rec_on q (take p, eq.rec_on p (concat_p_pp r idp idp)) p definition ap_pp_p (f : A → B) {w x y z : A} (p : x = y) (q : y = z) (r : f z = f w) : (ap f (p ⬝ q)) ⬝ r = (ap f p) ⬝ (ap f q ⬝ r) := - rec_on q (rec_on p (take r, concat_pp_p _ _ _)) r + eq.rec_on q (eq.rec_on p (take r, concat_pp_p _ _ _)) r -- Functions commute with path inverses. definition inverse_ap (f : A → B) {x y : A} (p : x = y) : (ap f p)⁻¹ = ap f (p⁻¹) := - rec_on p idp + eq.rec_on p idp definition ap_V {A B : Type} (f : A → B) {x y : A} (p : x = y) : ap f (p⁻¹) = (ap f p)⁻¹ := - rec_on p idp + eq.rec_on p idp -- [ap] itself is functorial in the first argument. definition ap_idmap (p : x = y) : ap id p = p := - rec_on p idp + eq.rec_on p idp definition ap_compose (f : A → B) (g : B → C) {x y : A} (p : x = y) : ap (g ∘ f) p = ap g (ap f p) := - rec_on p idp + eq.rec_on p idp -- Sometimes we don't have the actual function [compose]. definition ap_compose' (f : A → B) (g : B → C) {x y : A} (p : x = y) : ap (λa, g (f a)) p = ap g (ap f p) := - rec_on p idp + eq.rec_on p idp -- The action of constant maps. definition ap_const (p : x = y) (z : B) : ap (λu, z) p = idp := - rec_on p idp + eq.rec_on p idp -- Naturality of [ap]. definition concat_Ap {f g : A → B} (p : Π x, f x = g x) {x y : A} (q : x = y) : (ap f q) ⬝ (p y) = (p x) ⬝ (ap g q) := - rec_on q (concat_1p _ ⬝ (concat_p1 _)⁻¹) + eq.rec_on q (concat_1p _ ⬝ (concat_p1 _)⁻¹) -- Naturality of [ap] at identity. definition concat_A1p {f : A → A} (p : Πx, f x = x) {x y : A} (q : x = y) : (ap f q) ⬝ (p y) = (p x) ⬝ q := - rec_on q (concat_1p _ ⬝ (concat_p1 _)⁻¹) + eq.rec_on q (concat_1p _ ⬝ (concat_p1 _)⁻¹) definition concat_pA1 {f : A → A} (p : Πx, x = f x) {x y : A} (q : x = y) : (p x) ⬝ (ap f q) = q ⬝ (p y) := - rec_on q (concat_p1 _ ⬝ (concat_1p _)⁻¹) + eq.rec_on q (concat_p1 _ ⬝ (concat_1p _)⁻¹) -- Naturality with other paths hanging around. definition concat_pA_pp {f g : A → B} (p : Πx, f x = g x) {x y : A} (q : x = y) {w z : B} (r : w = f x) (s : g y = z) : (r ⬝ ap f q) ⬝ (p y ⬝ s) = (r ⬝ p x) ⬝ (ap g q ⬝ s) := - rec_on s (rec_on q idp) + eq.rec_on s (eq.rec_on q idp) definition concat_pA_p {f g : A → B} (p : Πx, f x = g x) {x y : A} (q : x = y) {w : B} (r : w = f x) : (r ⬝ ap f q) ⬝ p y = (r ⬝ p x) ⬝ ap g q := - rec_on q idp + eq.rec_on q idp -- TODO: try this using the simplifier, and compare proofs definition concat_A_pp {f g : A → B} (p : Πx, f x = g x) {x y : A} (q : x = y) {z : B} (s : g y = z) : (ap f q) ⬝ (p y ⬝ s) = (p x) ⬝ (ap g q ⬝ s) := - rec_on s (rec_on q + eq.rec_on s (eq.rec_on q (calc (ap f idp) ⬝ (p x ⬝ idp) = idp ⬝ p x : idp ... = p x : concat_1p _ ... = (p x) ⬝ (ap g idp ⬝ idp) : idp)) -- This also works: - -- rec_on s (rec_on q (concat_1p _ ▹ idp)) + -- eq.rec_on s (eq.rec_on q (concat_1p _ ▹ idp)) definition concat_pA1_pp {f : A → A} (p : Πx, f x = x) {x y : A} (q : x = y) {w z : A} (r : w = f x) (s : y = z) : (r ⬝ ap f q) ⬝ (p y ⬝ s) = (r ⬝ p x) ⬝ (q ⬝ s) := - rec_on s (rec_on q idp) + eq.rec_on s (eq.rec_on q idp) definition concat_pp_A1p {g : A → A} (p : Πx, x = g x) {x y : A} (q : x = y) {w z : A} (r : w = x) (s : g y = z) : (r ⬝ p x) ⬝ (ap g q ⬝ s) = (r ⬝ q) ⬝ (p y ⬝ s) := - rec_on s (rec_on q idp) + eq.rec_on s (eq.rec_on q idp) definition concat_pA1_p {f : A → A} (p : Πx, f x = x) {x y : A} (q : x = y) {w : A} (r : w = f x) : (r ⬝ ap f q) ⬝ p y = (r ⬝ p x) ⬝ q := - rec_on q idp + eq.rec_on q idp definition concat_A1_pp {f : A → A} (p : Πx, f x = x) {x y : A} (q : x = y) {z : A} (s : y = z) : (ap f q) ⬝ (p y ⬝ s) = (p x) ⬝ (q ⬝ s) := - rec_on s (rec_on q (concat_1p _ ▹ idp)) + eq.rec_on s (eq.rec_on q (concat_1p _ ▹ idp)) definition concat_pp_A1 {g : A → A} (p : Πx, x = g x) {x y : A} (q : x = y) {w : A} (r : w = x) : (r ⬝ p x) ⬝ ap g q = (r ⬝ q) ⬝ p y := - rec_on q idp + eq.rec_on q idp definition concat_p_A1p {g : A → A} (p : Πx, x = g x) {x y : A} (q : x = y) {z : A} (s : g y = z) : p x ⬝ (ap g q ⬝ s) = q ⬝ (p y ⬝ s) := begin - apply (rec_on s), - apply (rec_on q), + apply (eq.rec_on s), + apply (eq.rec_on q), apply (concat_1p (p x) ▹ idp) end @@ -361,11 +361,11 @@ namespace eq definition apD10_pp {f f' f'' : Πx, P x} (h : f = f') (h' : f' = f'') (x : A) : apD10 (h ⬝ h') x = apD10 h x ⬝ apD10 h' x := - rec_on h (take h', rec_on h' idp) h' + eq.rec_on h (take h', eq.rec_on h' idp) h' definition apD10_V {f g : Πx : A, P x} (h : f = g) (x : A) : apD10 (h⁻¹) x = (apD10 h x)⁻¹ := - rec_on h idp + eq.rec_on h idp definition ap10_1 {f : A → B} (x : A) : ap10 (refl f) x = idp := idp @@ -378,7 +378,7 @@ namespace eq -- [ap10] also behaves nicely on paths produced by [ap] definition ap_ap10 (f g : A → B) (h : B → C) (p : f = g) (a : A) : ap h (ap10 p a) = ap10 (ap (λ f', h ∘ f') p) a:= - rec_on p idp + eq.rec_on p idp -- Transport and the groupoid structure of paths @@ -389,7 +389,7 @@ namespace eq definition transport_pp (P : A → Type) {x y z : A} (p : x = y) (q : y = z) (u : P x) : p ⬝ q ▹ u = q ▹ p ▹ u := - rec_on q (rec_on p idp) + eq.rec_on q (eq.rec_on p idp) definition transport_pV (P : A → Type) {x y : A} (p : x = y) (z : P y) : p ▹ p⁻¹ ▹ z = z := @@ -405,18 +405,18 @@ namespace eq ap (transport P r) (transport_pp P p q u) = (transport_pp P p (q ⬝ r) u) ⬝ (transport_pp P q r (p ▹ u)) :> ((p ⬝ (q ⬝ r)) ▹ u = r ▹ q ▹ p ▹ u) := - rec_on r (rec_on q (rec_on p idp)) + eq.rec_on r (eq.rec_on q (eq.rec_on p idp)) -- Here is another coherence lemma for transport. definition transport_pVp (P : A → Type) {x y : A} (p : x = y) (z : P x) : transport_pV P p (transport P p z) = ap (transport P p) (transport_Vp P p z) := - rec_on p idp + eq.rec_on p idp -- Dependent transport in a doubly dependent type. -- should P, Q and y all be explicit here? definition transportD (P : A → Type) (Q : Π a : A, P a → Type) {a a' : A} (p : a = a') (b : P a) (z : Q a b) : Q a' (p ▹ b) := - rec_on p z + eq.rec_on p z -- In Coq the variables B, C and y are explicit, but in Lean we can probably have them implicit using the following notation notation p `▹D`:65 x:64 := transportD _ _ p _ x @@ -431,32 +431,32 @@ namespace eq definition transport2_is_ap10 (Q : A → Type) {x y : A} {p q : x = y} (r : p = q) (z : Q x) : transport2 Q r z = ap10 (ap (transport Q) r) z := - rec_on r idp + eq.rec_on r idp definition transport2_p2p (P : A → Type) {x y : A} {p1 p2 p3 : x = y} (r1 : p1 = p2) (r2 : p2 = p3) (z : P x) : transport2 P (r1 ⬝ r2) z = transport2 P r1 z ⬝ transport2 P r2 z := - rec_on r1 (rec_on r2 idp) + eq.rec_on r1 (eq.rec_on r2 idp) definition transport2_V (Q : A → Type) {x y : A} {p q : x = y} (r : p = q) (z : Q x) : transport2 Q (r⁻¹) z = ((transport2 Q r z)⁻¹) := - rec_on r idp + eq.rec_on r idp definition transportD2 (B C : A → Type) (D : Π(a:A), B a → C a → Type) {x1 x2 : A} (p : x1 = x2) (y : B x1) (z : C x1) (w : D x1 y z) : D x2 (p ▹ y) (p ▹ z) := - rec_on p w + eq.rec_on p w notation p `▹D2`:65 x:64 := transportD2 _ _ _ p _ _ x definition concat_AT (P : A → Type) {x y : A} {p q : x = y} {z w : P x} (r : p = q) (s : z = w) : ap (transport P p) s ⬝ transport2 P r w = transport2 P r z ⬝ ap (transport P q) s := - rec_on r (concat_p1 _ ⬝ (concat_1p _)⁻¹) + eq.rec_on r (concat_p1 _ ⬝ (concat_1p _)⁻¹) -- TODO (from Coq library): What should this be called? definition ap_transport {P Q : A → Type} {x y : A} (p : x = y) (f : Πx, P x → Q x) (z : P x) : f y (p ▹ z) = (p ▹ (f x z)) := - rec_on p idp + eq.rec_on p idp -- Transporting in particular fibrations @@ -473,34 +473,34 @@ namespace eq -- Transporting in a constant fibration. definition transport_const (p : x = y) (z : B) : transport (λx, B) p z = z := - rec_on p idp + eq.rec_on p idp definition transport2_const {p q : x = y} (r : p = q) (z : B) : transport_const p z = transport2 (λu, B) r z ⬝ transport_const q z := - rec_on r (concat_1p _)⁻¹ + eq.rec_on r (concat_1p _)⁻¹ -- Transporting in a pulled back fibration. -- TODO: P can probably be implicit definition transport_compose (P : B → Type) (f : A → B) (p : x = y) (z : P (f x)) : transport (P ∘ f) p z = transport P (ap f p) z := - rec_on p idp + eq.rec_on p idp definition transport_precompose (f : A → B) (g g' : B → C) (p : g = g') : transport (λh : B → C, g ∘ f = h ∘ f) p idp = ap (λh, h ∘ f) p := - rec_on p idp + eq.rec_on p idp definition apD10_ap_precompose (f : A → B) (g g' : B → C) (p : g = g') (a : A) : apD10 (ap (λh : B → C, h ∘ f) p) a = apD10 p (f a) := - rec_on p idp + eq.rec_on p idp definition apD10_ap_postcompose (f : B → C) (g g' : A → B) (p : g = g') (a : A) : apD10 (ap (λh : A → B, f ∘ h) p) a = ap f (apD10 p a) := - rec_on p idp + eq.rec_on p idp -- A special case of [transport_compose] which seems to come up a lot. definition transport_idmap_ap (P : A → Type) x y (p : x = y) (u : P x) : transport P p u = transport (λz, z) (ap P p) u := - rec_on p idp + eq.rec_on p idp -- The behavior of [ap] and [apD] @@ -509,7 +509,7 @@ namespace eq -- In a constant fibration, [apD] reduces to [ap], modulo [transport_const]. definition apD_const (f : A → B) (p: x = y) : apD f p = transport_const p (f x) ⬝ ap f p := - rec_on p idp + eq.rec_on p idp -- The 2-dimensional groupoid structure @@ -518,13 +518,13 @@ namespace eq -- Horizontal composition of 2-dimensional paths. definition concat2 {p p' : x = y} {q q' : y = z} (h : p = p') (h' : q = q') : p ⬝ q = p' ⬝ q' := - rec_on h (rec_on h' idp) + eq.rec_on h (eq.rec_on h' idp) infixl `◾`:75 := concat2 -- 2-dimensional path inversion definition inverse2 {p q : x = y} (h : p = q) : p⁻¹ = q⁻¹ := - rec_on h idp + eq.rec_on h idp -- Whiskering @@ -539,47 +539,47 @@ namespace eq -- Unwhiskering, a.k.a. cancelling definition cancelL {x y z : A} (p : x = y) (q r : y = z) : (p ⬝ q = p ⬝ r) → (q = r) := - rec_on p (take r, rec_on r (take q a, (concat_1p q)⁻¹ ⬝ a)) r q + eq.rec_on p (take r, eq.rec_on r (take q a, (concat_1p q)⁻¹ ⬝ a)) r q definition cancelR {x y z : A} (p q : x = y) (r : y = z) : (p ⬝ r = q ⬝ r) → (p = q) := - rec_on r (rec_on p (take q a, a ⬝ concat_p1 q)) q + eq.rec_on r (eq.rec_on p (take q a, a ⬝ concat_p1 q)) q -- Whiskering and identity paths. definition whiskerR_p1 {p q : x = y} (h : p = q) : (concat_p1 p)⁻¹ ⬝ whiskerR h idp ⬝ concat_p1 q = h := - rec_on h (rec_on p idp) + eq.rec_on h (eq.rec_on p idp) definition whiskerR_1p (p : x = y) (q : y = z) : whiskerR idp q = idp :> (p ⬝ q = p ⬝ q) := - rec_on q idp + eq.rec_on q idp definition whiskerL_p1 (p : x = y) (q : y = z) : whiskerL p idp = idp :> (p ⬝ q = p ⬝ q) := - rec_on q idp + eq.rec_on q idp definition whiskerL_1p {p q : x = y} (h : p = q) : (concat_1p p) ⁻¹ ⬝ whiskerL idp h ⬝ concat_1p q = h := - rec_on h (rec_on p idp) + eq.rec_on h (eq.rec_on p idp) definition concat2_p1 {p q : x = y} (h : p = q) : h ◾ idp = whiskerR h idp :> (p ⬝ idp = q ⬝ idp) := - rec_on h idp + eq.rec_on h idp definition concat2_1p {p q : x = y} (h : p = q) : idp ◾ h = whiskerL idp h :> (idp ⬝ p = idp ⬝ q) := - rec_on h idp + eq.rec_on h idp -- TODO: note, 4 inductions -- The interchange law for concatenation. definition concat_concat2 {p p' p'' : x = y} {q q' q'' : y = z} (a : p = p') (b : p' = p'') (c : q = q') (d : q' = q'') : (a ◾ c) ⬝ (b ◾ d) = (a ⬝ b) ◾ (c ⬝ d) := - rec_on d (rec_on c (rec_on b (rec_on a idp))) + eq.rec_on d (eq.rec_on c (eq.rec_on b (eq.rec_on a idp))) definition concat_whisker {x y z : A} (p p' : x = y) (q q' : y = z) (a : p = p') (b : q = q') : (whiskerR a q) ⬝ (whiskerL p' b) = (whiskerL p b) ⬝ (whiskerR a q') := - rec_on b (rec_on a (concat_1p _)⁻¹) + eq.rec_on b (eq.rec_on a (concat_1p _)⁻¹) -- Structure corresponding to the coherence equations of a bicategory. @@ -589,12 +589,12 @@ namespace eq ⬝ concat_p_pp p (q ⬝ r) s ⬝ whiskerR (concat_p_pp p q r) s = concat_p_pp p q (r ⬝ s) ⬝ concat_p_pp (p ⬝ q) r s := - rec_on s (rec_on r (rec_on q (rec_on p idp))) + eq.rec_on s (eq.rec_on r (eq.rec_on q (eq.rec_on p idp))) -- The 3-cell witnessing the left unit triangle. definition triangulator (p : x = y) (q : y = z) : concat_p_pp p idp q ⬝ whiskerR (concat_p1 p) q = whiskerL p (concat_1p q) := - rec_on q (rec_on p idp) + eq.rec_on q (eq.rec_on p idp) definition eckmann_hilton {x:A} (p q : idp = idp :> (x = x)) : p ⬝ q = q ⬝ p := (!whiskerR_p1 ◾ !whiskerL_1p)⁻¹ @@ -607,23 +607,23 @@ namespace eq -- The action of functions on 2-dimensional paths definition ap02 (f:A → B) {x y : A} {p q : x = y} (r : p = q) : ap f p = ap f q := - rec_on r idp + eq.rec_on r idp definition ap02_pp (f : A → B) {x y : A} {p p' p'' : x = y} (r : p = p') (r' : p' = p'') : ap02 f (r ⬝ r') = ap02 f r ⬝ ap02 f r' := - rec_on r (rec_on r' idp) + eq.rec_on r (eq.rec_on r' idp) definition ap02_p2p (f : A → B) {x y z : A} {p p' : x = y} {q q' :y = z} (r : p = p') (s : q = q') : ap02 f (r ◾ s) = ap_pp f p q ⬝ (ap02 f r ◾ ap02 f s) ⬝ (ap_pp f p' q')⁻¹ := - rec_on r (rec_on s (rec_on q (rec_on p idp))) - -- rec_on r (rec_on s (rec_on p (rec_on q idp))) + eq.rec_on r (eq.rec_on s (eq.rec_on q (eq.rec_on p idp))) + -- eq.rec_on r (eq.rec_on s (eq.rec_on p (eq.rec_on q idp))) definition apD02 {p q : x = y} (f : Π x, P x) (r : p = q) : apD f p = transport2 P r (f x) ⬝ apD f q := - rec_on r (concat_1p _)⁻¹ + eq.rec_on r (concat_1p _)⁻¹ -- And now for a lemma whose statement is much longer than its proof. definition apD02_pp (P : A → Type) (f : Π x:A, P x) {x y : A} @@ -632,22 +632,22 @@ namespace eq ⬝ whiskerL (transport2 P r1 (f x)) (apD02 f r2) ⬝ concat_p_pp _ _ _ ⬝ (whiskerR ((transport2_p2p P r1 r2 (f x))⁻¹) (apD f p3)) := - rec_on r2 (rec_on r1 (rec_on p1 idp)) + eq.rec_on r2 (eq.rec_on r1 (eq.rec_on p1 idp)) end eq namespace eq variables {A B C D E : Type} {a a' : A} {b b' : B} {c c' : C} {d d' : D} theorem congr_arg2 (f : A → B → C) (Ha : a = a') (Hb : b = b') : f a b = f a' b' := -rec_on Ha (rec_on Hb idp) +eq.rec_on Ha (eq.rec_on Hb idp) theorem congr_arg3 (f : A → B → C → D) (Ha : a = a') (Hb : b = b') (Hc : c = c') : f a b c = f a' b' c' := -rec_on Ha (congr_arg2 (f a) Hb Hc) +eq.rec_on Ha (congr_arg2 (f a) Hb Hc) theorem congr_arg4 (f : A → B → C → D → E) (Ha : a = a') (Hb : b = b') (Hc : c = c') (Hd : d = d') : f a b c d = f a' b' c' d' := -rec_on Ha (congr_arg3 (f a) Hb Hc Hd) +eq.rec_on Ha (congr_arg3 (f a) Hb Hc Hd) end eq @@ -661,7 +661,7 @@ variables {a a' : A} theorem dcongr_arg2 (f : Πa, B a → F) (Ha : a = a') (Hb : (Ha ▹ b) = b') : f a b = f a' b' := -rec_on Hb (rec_on Ha idp) +eq.rec_on Hb (eq.rec_on Ha idp) /- From the Coq version: diff --git a/hott/init/types/empty.hlean b/hott/init/types/empty.hlean index fea08e5b5..077c7cd59 100644 --- a/hott/init/types/empty.hlean +++ b/hott/init/types/empty.hlean @@ -11,7 +11,7 @@ import ..datatypes ..logic namespace empty protected theorem elim (A : Type) (H : empty) : A := - rec (λe, A) H + empty.rec (λe, A) H end empty diff --git a/hott/init/types/prod.hlean b/hott/init/types/prod.hlean index a9e99c5cf..127759c2a 100644 --- a/hott/init/types/prod.hlean +++ b/hott/init/types/prod.hlean @@ -60,8 +60,8 @@ namespace prod (iHb : ∀y, Rb y xb → acc (lex Ra Rb) (xa, y)), acc.intro (xa, xb) (λp (lt : p ≺ (xa, xb)), have aux : xa = xa → xb = xb → acc (lex Ra Rb) p, from - @lex.rec_on A B Ra Rb (λp₁ p₂ h, pr₁ p₂ = xa → pr₂ p₂ = xb → acc (lex Ra Rb) p₁) - p (xa, xb) lt + @prod.lex.rec_on A B Ra Rb (λp₁ p₂ h, pr₁ p₂ = xa → pr₂ p₂ = xb → acc (lex Ra Rb) p₁) + p (xa, xb) lt (λa₁ b₁ a₂ b₂ (H : Ra a₁ a₂) (eq₂ : a₂ = xa) (eq₃ : b₂ = xb), show acc (lex Ra Rb) (a₁, b₁), from have Ra₁ : Ra a₁ xa, from eq.rec_on eq₂ H, @@ -79,7 +79,7 @@ namespace prod -- Relational product is a subrelation of the lex definition rprod.sub_lex : ∀ a b, rprod Ra Rb a b → lex Ra Rb a b := - λa b H, rprod.rec_on H (λ a₁ b₁ a₂ b₂ H₁ H₂, lex.left Rb a₂ b₂ H₁) + λa b H, prod.rprod.rec_on H (λ a₁ b₁ a₂ b₂ H₁ H₂, lex.left Rb a₂ b₂ H₁) -- The relational product of well founded relations is well-founded definition rprod.wf (Ha : well_founded Ra) (Hb : well_founded Rb) : well_founded (rprod Ra Rb) := diff --git a/hott/init/wf.hlean b/hott/init/wf.hlean index 53073f42a..27df72e53 100644 --- a/hott/init/wf.hlean +++ b/hott/init/wf.hlean @@ -13,7 +13,7 @@ namespace acc variables {A : Type} {R : A → A → Type} definition inv {x y : A} (H₁ : acc R x) (H₂ : R y x) : acc R y := - rec_on H₁ (λ x₁ ac₁ iH H₂, ac₁ y H₂) H₂ + acc.rec_on H₁ (λ x₁ ac₁ iH H₂, ac₁ y H₂) H₂ end acc inductive well_founded [class] {A : Type} (R : A → A → Type) : Type := diff --git a/library/algebra/category/natural_transformation.lean b/library/algebra/category/natural_transformation.lean index dc7798655..7610c2722 100644 --- a/library/algebra/category/natural_transformation.lean +++ b/library/algebra/category/natural_transformation.lean @@ -19,21 +19,21 @@ namespace natural_transformation variables {C D : Category} {F G H I : functor C D} definition natural_map [coercion] (η : F ⟹ G) : Π(a : C), F a ⟶ G a := - rec (λ x y, x) η + natural_transformation.rec (λ x y, x) η theorem naturality (η : F ⟹ G) : Π⦃a b : C⦄ (f : a ⟶ b), G f ∘ η a = η b ∘ F f := - rec (λ x y, y) η + natural_transformation.rec (λ x y, y) η protected definition compose (η : G ⟹ H) (θ : F ⟹ G) : F ⟹ H := natural_transformation.mk (λ a, η a ∘ θ a) (λ a b f, calc - H f ∘ (η a ∘ θ a) = (H f ∘ η a) ∘ θ a : assoc - ... = (η b ∘ G f) ∘ θ a : naturality η f - ... = η b ∘ (G f ∘ θ a) : assoc - ... = η b ∘ (θ b ∘ F f) : naturality θ f - ... = (η b ∘ θ b) ∘ F f : assoc) + H f ∘ (η a ∘ θ a) = (H f ∘ η a) ∘ θ a : assoc + ... = (η b ∘ G f) ∘ θ a : naturality η f + ... = η b ∘ (G f ∘ θ a) : assoc + ... = η b ∘ (θ b ∘ F f) : naturality θ f + ... = (η b ∘ θ b) ∘ F f : assoc) --congr_arg (λx, η b ∘ x) (naturality θ f) -- this needed to be explicit for some reason (on Oct 24) infixr `∘n`:60 := compose @@ -46,8 +46,8 @@ namespace natural_transformation protected definition ID {C D : Category} (F : functor C D) : natural_transformation F F := id protected theorem id_left (η : F ⟹ G) : natural_transformation.compose id η = η := - rec (λf H, dcongr_arg2 mk (funext (take x, !id_left)) !proof_irrel) η + natural_transformation.rec (λf H, dcongr_arg2 mk (funext (take x, !id_left)) !proof_irrel) η protected theorem id_right (η : F ⟹ G) : natural_transformation.compose η id = η := - rec (λf H, dcongr_arg2 mk (funext (take x, !id_right)) !proof_irrel) η + natural_transformation.rec (λf H, dcongr_arg2 mk (funext (take x, !id_right)) !proof_irrel) η end natural_transformation diff --git a/library/data/bool.lean b/library/data/bool.lean index 452c578f6..1e564097a 100644 --- a/library/data/bool.lean +++ b/library/data/bool.lean @@ -14,7 +14,7 @@ namespace bool local attribute band [reducible] theorem dichotomy (b : bool) : b = ff ∨ b = tt := - cases_on b (or.inl rfl) (or.inr rfl) + bool.cases_on b (or.inl rfl) (or.inr rfl) theorem cond.ff {A : Type} (t e : A) : cond ff t e = e := rfl @@ -35,24 +35,24 @@ namespace bool notation a || b := bor a b theorem bor.tt_right (a : bool) : a || tt = tt := - cases_on a rfl rfl + bool.cases_on a rfl rfl theorem bor.ff_left (a : bool) : ff || a = a := - cases_on a rfl rfl + bool.cases_on a rfl rfl theorem bor.ff_right (a : bool) : a || ff = a := - cases_on a rfl rfl + bool.cases_on a rfl rfl theorem bor.id (a : bool) : a || a = a := - cases_on a rfl rfl + bool.cases_on a rfl rfl theorem bor.comm (a b : bool) : a || b = b || a := - cases_on a - (cases_on b rfl rfl) - (cases_on b rfl rfl) + bool.cases_on a + (bool.cases_on b rfl rfl) + (bool.cases_on b rfl rfl) theorem bor.assoc (a b c : bool) : (a || b) || c = a || (b || c) := - cases_on a + bool.cases_on a (calc (ff || b) || c = b || c : {!bor.ff_left} ... = ff || (b || c) : !bor.ff_left⁻¹) (calc (tt || b) || c = tt || c : {!bor.tt_left} @@ -60,7 +60,7 @@ namespace bool ... = tt || (b || c) : !bor.tt_left⁻¹) theorem bor.to_or {a b : bool} : a || b = tt → a = tt ∨ b = tt := - rec_on a + bool.rec_on a (assume H : ff || b = tt, have Hb : b = tt, from !bor.ff_left ▸ H, or.inr Hb) @@ -70,24 +70,24 @@ namespace bool rfl theorem band.tt_left (a : bool) : tt && a = a := - cases_on a rfl rfl + bool.cases_on a rfl rfl theorem band.ff_right (a : bool) : a && ff = ff := - cases_on a rfl rfl + bool.cases_on a rfl rfl theorem band.tt_right (a : bool) : a && tt = a := - cases_on a rfl rfl + bool.cases_on a rfl rfl theorem band.id (a : bool) : a && a = a := - cases_on a rfl rfl + bool.cases_on a rfl rfl theorem band.comm (a b : bool) : a && b = b && a := - cases_on a - (cases_on b rfl rfl) - (cases_on b rfl rfl) + bool.cases_on a + (bool.cases_on b rfl rfl) + (bool.cases_on b rfl rfl) theorem band.assoc (a b c : bool) : (a && b) && c = a && (b && c) := - cases_on a + bool.cases_on a (calc (ff && b) && c = ff && c : {!band.ff_left} ... = ff : !band.ff_left ... = ff && (b && c) : !band.ff_left⁻¹) @@ -108,7 +108,7 @@ namespace bool band.eq_tt_elim_left (!band.comm ⬝ H) theorem bnot.bnot (a : bool) : bnot (bnot a) = a := - cases_on a rfl rfl + bool.cases_on a rfl rfl theorem bnot.false : bnot ff = tt := rfl @@ -116,13 +116,15 @@ namespace bool theorem bnot.true : bnot tt = ff := rfl - protected definition is_inhabited [instance] : inhabited bool := - inhabited.mk ff - - protected definition has_decidable_eq [instance] : decidable_eq bool := - take a b : bool, - rec_on a - (rec_on b (inl rfl) (inr ff_ne_tt)) - (rec_on b (inr (ne.symm ff_ne_tt)) (inl rfl)) - end bool + +open bool + +protected definition bool.inhabited [instance] : inhabited bool := +inhabited.mk ff + +protected definition bool.decidable_eq [instance] : decidable_eq bool := +take a b : bool, + bool.rec_on a + (bool.rec_on b (inl rfl) (inr ff_ne_tt)) + (bool.rec_on b (inr (ne.symm ff_ne_tt)) (inl rfl)) diff --git a/library/data/empty.lean b/library/data/empty.lean index c3ed86852..96bd1495d 100644 --- a/library/data/empty.lean +++ b/library/data/empty.lean @@ -10,7 +10,7 @@ import logic.cast logic.subsingleton namespace empty protected theorem elim (A : Type) (H : empty) : A := - rec (λe, A) H + empty.rec (λe, A) H protected theorem subsingleton [instance] : subsingleton empty := subsingleton.intro (λ a b, !elim a) diff --git a/library/data/int/basic.lean b/library/data/int/basic.lean index 4a058d7d3..baf8f658d 100644 --- a/library/data/int/basic.lean +++ b/library/data/int/basic.lean @@ -57,30 +57,30 @@ nat.cases_on (n - m) (take k, neg_succ_of_nat k) -- m < n, and n - m = succ k definition neg (a : ℤ) : ℤ := - cases_on a + int.cases_on a (take m, -- a = of_nat m nat.cases_on m 0 (take m', neg_succ_of_nat m')) (take m, of_nat (succ m)) -- a = neg_succ_of_nat m definition add (a b : ℤ) : ℤ := - cases_on a + int.cases_on a (take m, -- a = of_nat m - cases_on b + int.cases_on b (take n, of_nat (m + n)) -- b = of_nat n (take n, sub_nat_nat m (succ n))) -- b = neg_succ_of_nat n (take m, -- a = neg_succ_of_nat m - cases_on b + int.cases_on b (take n, sub_nat_nat n (succ m)) -- b = of_nat n (take n, neg_of_nat (succ m + succ n))) -- b = neg_succ_of_nat n definition mul (a b : ℤ) : ℤ := - cases_on a + int.cases_on a (take m, -- a = of_nat m - cases_on b + int.cases_on b (take n, of_nat (m * n)) -- b = of_nat n (take n, neg_of_nat (m * succ n))) -- b = neg_succ_of_nat n (take m, -- a = neg_succ_of_nat m - cases_on b + int.cases_on b (take n, neg_of_nat (succ m * n)) -- b = of_nat n (take n, of_nat (succ m * succ n))) -- b = neg_succ_of_nat n @@ -94,22 +94,22 @@ infix * := int.mul /- some basic functions and properties -/ theorem of_nat_inj {m n : ℕ} (H : of_nat m = of_nat n) : m = n := -no_confusion H (λe, e) +int.no_confusion H (λe, e) theorem neg_succ_of_nat_inj {m n : ℕ} (H : neg_succ_of_nat m = neg_succ_of_nat n) : m = n := -no_confusion H (λe, e) +int.no_confusion H (λe, e) definition has_decidable_eq [instance] : decidable_eq ℤ := take a b, -cases_on a +int.cases_on a (take m, - cases_on b + int.cases_on b (take n, if H : m = n then inl (congr_arg of_nat H) else inr (take H1, H (of_nat_inj H1))) - (take n', inr (assume H, no_confusion H))) + (take n', inr (assume H, int.no_confusion H))) (take m', - cases_on b - (take n, inr (assume H, no_confusion H)) + int.cases_on b + (take n, inr (assume H, int.no_confusion H)) (take n', (if H : m' = n' then inl (congr_arg neg_succ_of_nat H) else inr (take H1, H (neg_succ_of_nat_inj H1))))) @@ -137,12 +137,12 @@ calc ... = neg_succ_of_nat (pred (n - m)) : rfl end -definition nat_abs (a : ℤ) : ℕ := cases_on a (take n, n) (take n', succ n') +definition nat_abs (a : ℤ) : ℕ := int.cases_on a (take n, n) (take n', succ n') theorem nat_abs_of_nat (n : ℕ) : nat_abs (of_nat n) = n := rfl theorem nat_abs_eq_zero {a : ℤ} : nat_abs a = 0 → a = 0 := -cases_on a +int.cases_on a (take m, assume H : nat_abs (of_nat m) = 0, congr_arg of_nat H) (take m', assume H : nat_abs (neg_succ_of_nat m') = 0, absurd H (succ_ne_zero _)) @@ -206,10 +206,10 @@ theorem abstr_of_lt {p : ℕ × ℕ} (H : pr1 p < pr2 p) : abstr p = neg_succ_of_nat (pred (pr2 p - pr1 p)) := sub_nat_nat_of_lt H -definition repr (a : ℤ) : ℕ × ℕ := cases_on a (take m, (m, 0)) (take m, (0, succ m)) +definition repr (a : ℤ) : ℕ × ℕ := int.cases_on a (take m, (m, 0)) (take m, (0, succ m)) theorem abstr_repr (a : ℤ) : abstr (repr a) = a := -cases_on a (take m, (sub_nat_nat_of_ge (zero_le m))) (take m, rfl) +int.cases_on a (take m, (sub_nat_nat_of_ge (zero_le m))) (take m, rfl) theorem repr_sub_nat_nat (m n : ℕ) : repr (sub_nat_nat m n) ≡ (m, n) := or.elim (@le_or_gt n m) @@ -299,7 +299,7 @@ or.elim (@le_or_gt n m) end theorem cases_of_nat (a : ℤ) : (∃n : ℕ, a = of_nat n) ∨ (∃n : ℕ, a = - of_nat n) := -cases_on a +int.cases_on a (take n, or.inl (exists.intro n rfl)) (take n', or.inr (exists.intro (succ n') rfl)) @@ -329,9 +329,9 @@ or.elim (cases_of_nat_succ a) definition padd (p q : ℕ × ℕ) : ℕ × ℕ := (pr1 p + pr1 q, pr2 p + pr2 q) theorem repr_add (a b : ℤ) : repr (add a b) ≡ padd (repr a) (repr b) := -cases_on a +int.cases_on a (take m, - cases_on b + int.cases_on b (take n, !equiv.refl) (take n', have H1 : equiv (repr (add (of_nat m) (neg_succ_of_nat n'))) (m, succ n'), @@ -340,7 +340,7 @@ cases_on a from rfl, (!zero_add ▸ H2)⁻¹ ▸ H1)) (take m', - cases_on b + int.cases_on b (take n, have H1 : equiv (repr (add (neg_succ_of_nat m') (of_nat n))) (n, succ m'), from !repr_sub_nat_nat, @@ -394,7 +394,7 @@ begin apply H2 end -theorem add_zero (a : ℤ) : a + 0 = a := cases_on a (take m, rfl) (take m', rfl) +theorem add_zero (a : ℤ) : a + 0 = a := int.cases_on a (take m, rfl) (take m', rfl) theorem zero_add (a : ℤ) : 0 + a = a := add.comm a 0 ▸ add_zero a @@ -404,7 +404,7 @@ definition pneg (p : ℕ × ℕ) : ℕ × ℕ := (pr2 p, pr1 p) -- note: this is =, not just ≡ theorem repr_neg (a : ℤ) : repr (- a) = pneg (repr a) := -cases_on a +int.cases_on a (take m, nat.cases_on m rfl (take m', rfl)) (take m', rfl) @@ -465,13 +465,13 @@ H⁻¹ ▸ H1⁻¹ ▸ H2⁻¹ ▸ H3 context attribute nat_abs [reducible] theorem mul_nat_abs (a b : ℤ) : nat_abs (a * b) = #nat (nat_abs a) * (nat_abs b) := -cases_on a +int.cases_on a (take m, - cases_on b + int.cases_on b (take n, rfl) (take n', !nat_abs_neg ▸ rfl)) (take m', - cases_on b + int.cases_on b (take n, !nat_abs_neg ▸ rfl) (take n', rfl)) end @@ -486,9 +486,9 @@ nat.cases_on m rfl (take m', rfl) -- note: we have =, not just ≡ theorem repr_mul (a b : ℤ) : repr (mul a b) = pmul (repr a) (repr b) := -cases_on a +int.cases_on a (take m, - cases_on b + int.cases_on b (take n, (calc pmul (repr m) (repr n) = (m * n + 0 * 0, m * 0 + 0 * n) : rfl @@ -500,7 +500,7 @@ cases_on a ... = (m * 0 + 0, m * succ n' + 0 * 0) : zero_mul ... = repr (mul m (neg_succ_of_nat n')) : repr_neg_of_nat)⁻¹)) (take m', - cases_on b + int.cases_on b (take n, (calc pmul (repr (neg_succ_of_nat m')) (repr n) = diff --git a/library/data/int/order.lean b/library/data/int/order.lean index e0ac1ce03..ff93fb170 100644 --- a/library/data/int/order.lean +++ b/library/data/int/order.lean @@ -16,7 +16,7 @@ open int eq.ops namespace int -private definition nonneg (a : ℤ) : Prop := cases_on a (take n, true) (take n, false) +private definition nonneg (a : ℤ) : Prop := int.cases_on a (take n, true) (take n, false) definition le (a b : ℤ) : Prop := nonneg (sub b a) definition lt (a b : ℤ) : Prop := le (add a 1) b @@ -25,15 +25,15 @@ infix <= := int.le infix ≤ := int.le infix < := int.lt -private definition decidable_nonneg [instance] (a : ℤ) : decidable (nonneg a) := cases_on a _ _ +private definition decidable_nonneg [instance] (a : ℤ) : decidable (nonneg a) := int.cases_on a _ _ definition decidable_le [instance] (a b : ℤ) : decidable (a ≤ b) := decidable_nonneg _ definition decidable_lt [instance] (a b : ℤ) : decidable (a < b) := decidable_nonneg _ private theorem nonneg.elim {a : ℤ} : nonneg a → ∃n : ℕ, a = n := -cases_on a (take n H, exists.intro n rfl) (take n' H, false.elim H) +int.cases_on a (take n H, exists.intro n rfl) (take n' H, false.elim H) private theorem nonneg_or_nonneg_neg (a : ℤ) : nonneg a ∨ nonneg (-a) := -cases_on a (take n, or.inl trivial) (take n, or.inr trivial) +int.cases_on a (take n, or.inl trivial) (take n, or.inr trivial) theorem le.intro {a b : ℤ} {n : ℕ} (H : a + n = b) : a ≤ b := have H1 : b - a = n, from (eq_add_neg_of_add_eq (!add.comm ▸ H))⁻¹, diff --git a/library/data/list/basic.lean b/library/data/list/basic.lean index 7d30a58a5..7f132c52a 100644 --- a/library/data/list/basic.lean +++ b/library/data/list/basic.lean @@ -137,7 +137,7 @@ head (a :: l) := a theorem head_cons [h : inhabited T] (a : T) (l : list T) : head (a::l) = a theorem head_concat [h : inhabited T] {s : list T} (t : list T) : s ≠ nil → head (s ++ t) = head s := -cases_on s +list.cases_on s (take H : nil ≠ nil, absurd rfl H) (take (x : T) (s : list T), take H : x::s ≠ nil, calc @@ -154,7 +154,7 @@ theorem tail_nil : tail (@nil T) = nil theorem tail_cons (a : T) (l : list T) : tail (a::l) = l theorem cons_head_tail [h : inhabited T] {l : list T} : l ≠ nil → (head l)::(tail l) = l := -cases_on l +list.cases_on l (assume H : nil ≠ nil, absurd rfl H) (take x l, assume H : x::l ≠ nil, rfl) @@ -173,7 +173,7 @@ theorem mem_cons (x y : T) (l : list T) : x ∈ y::l ↔ (x = y ∨ x ∈ l) := iff.rfl theorem mem_concat_imp_or {x : T} {s t : list T} : x ∈ s ++ t → x ∈ s ∨ x ∈ t := -induction_on s or.inr +list.induction_on s or.inr (take y s, assume IH : x ∈ s ++ t → x ∈ s ∨ x ∈ t, assume H1 : x ∈ y::s ++ t, @@ -182,7 +182,7 @@ induction_on s or.inr iff.elim_right or.assoc H3) theorem mem_or_imp_concat {x : T} {s t : list T} : x ∈ s ∨ x ∈ t → x ∈ s ++ t := -induction_on s +list.induction_on s (take H, or.elim H false.elim (assume H, H)) (take y s, assume IH : x ∈ s ∨ x ∈ t → x ∈ s ++ t, @@ -200,7 +200,7 @@ iff.intro mem_concat_imp_or mem_or_imp_concat local attribute mem [reducible] local attribute append [reducible] theorem mem_split {x : T} {l : list T} : x ∈ l → ∃s t : list T, l = s ++ (x::t) := -induction_on l +list.induction_on l (take H : x ∈ nil, false.elim (iff.elim_left !mem_nil H)) (take y l, assume IH : x ∈ l → ∃s t : list T, l = s ++ (x::t), @@ -216,7 +216,7 @@ induction_on l !exists.intro (!exists.intro H4))) definition mem.is_decidable [instance] (H : decidable_eq T) (x : T) (l : list T) : decidable (x ∈ l) := -rec_on l +list.rec_on l (decidable.inr (not_of_iff_false !mem_nil)) (take (h : T) (l : list T) (iH : decidable (x ∈ l)), show decidable (x ∈ h::l), from @@ -255,7 +255,7 @@ theorem find_nil (x : T) : find x nil = 0 theorem find_cons (x y : T) (l : list T) : find x (y::l) = if x = y then 0 else succ (find x l) theorem find.not_mem {l : list T} {x : T} : ¬x ∈ l → find x l = length l := -rec_on l +list.rec_on l (assume P₁ : ¬x ∈ nil, _) (take y l, assume iH : ¬x ∈ l → find x l = length l, diff --git a/library/data/nat/basic.lean b/library/data/nat/basic.lean index 58208fcde..a4a6a8306 100644 --- a/library/data/nat/basic.lean +++ b/library/data/nat/basic.lean @@ -47,7 +47,7 @@ nat.induction_on x /- successor and predecessor -/ theorem succ_ne_zero (n : ℕ) : succ n ≠ 0 := -assume H, no_confusion H +assume H, nat.no_confusion H -- add_rewrite succ_ne_zero @@ -58,7 +58,7 @@ theorem pred_succ (n : ℕ) : pred (succ n) = n := rfl theorem eq_zero_or_eq_succ_pred (n : ℕ) : n = 0 ∨ n = succ (pred n) := -induction_on n +nat.induction_on n (or.inl rfl) (take m IH, or.inr (show succ m = succ (pred (succ m)), from congr_arg succ !pred_succ⁻¹)) @@ -67,23 +67,23 @@ theorem exists_eq_succ_of_ne_zero {n : ℕ} (H : n ≠ 0) : ∃k : ℕ, n = succ exists.intro _ (or_resolve_right !eq_zero_or_eq_succ_pred H) theorem succ.inj {n m : ℕ} (H : succ n = succ m) : n = m := -no_confusion H (λe, e) +nat.no_confusion H (λe, e) theorem succ.ne_self {n : ℕ} : succ n ≠ n := -induction_on n +nat.induction_on n (take H : 1 = 0, have ne : 1 ≠ 0, from !succ_ne_zero, absurd H ne) (take k IH H, IH (succ.inj H)) theorem discriminate {B : Prop} {n : ℕ} (H1: n = 0 → B) (H2 : ∀m, n = succ m → B) : B := -have H : n = n → B, from cases_on n H1 H2, +have H : n = n → B, from nat.cases_on n H1 H2, H rfl theorem two_step_induction_on {P : ℕ → Prop} (a : ℕ) (H1 : P 0) (H2 : P 1) (H3 : ∀ (n : ℕ) (IH1 : P n) (IH2 : P (succ n)), P (succ (succ n))) : P a := have stronger : P a ∧ P (succ a), from - induction_on a + nat.induction_on a (and.intro H1 H2) (take k IH, have IH1 : P k, from and.elim_left IH, @@ -93,12 +93,12 @@ have stronger : P a ∧ P (succ a), from theorem sub_induction {P : ℕ → ℕ → Prop} (n m : ℕ) (H1 : ∀m, P 0 m) (H2 : ∀n, P (succ n) 0) (H3 : ∀n m, P n m → P (succ n) (succ m)) : P n m := -have general : ∀m, P n m, from induction_on n +have general : ∀m, P n m, from nat.induction_on n (take m : ℕ, H1 m) (take k : ℕ, assume IH : ∀m, P k m, take m : ℕ, - cases_on m (H2 k) (take l, (H3 k l (IH l)))), + nat.cases_on m (H2 k) (take l, (H3 k l (IH l)))), general m /- addition -/ @@ -110,7 +110,7 @@ theorem add_succ (n m : ℕ) : n + succ m = succ (n + m) := rfl theorem zero_add (n : ℕ) : 0 + n = n := -induction_on n +nat.induction_on n !add_zero (take m IH, show 0 + succ m = succ m, from calc @@ -118,7 +118,7 @@ induction_on n ... = succ m : IH) theorem add.succ_left (n m : ℕ) : (succ n) + m = succ (n + m) := -induction_on m +nat.induction_on m (!add_zero ▸ !add_zero) (take k IH, calc succ n + succ k = succ (succ n + k) : add_succ @@ -126,7 +126,7 @@ induction_on m ... = succ (n + succ k) : add_succ) theorem add.comm (n m : ℕ) : n + m = m + n := -induction_on m +nat.induction_on m (!add_zero ⬝ !zero_add⁻¹) (take k IH, calc n + succ k = succ (n+k) : add_succ @@ -137,7 +137,7 @@ theorem succ_add_eq_add_succ (n m : ℕ) : succ n + m = n + succ m := !add.succ_left ⬝ !add_succ⁻¹ theorem add.assoc (n m k : ℕ) : (n + m) + k = n + (m + k) := -induction_on k +nat.induction_on k (!add_zero ▸ !add_zero) (take l IH, calc @@ -153,7 +153,7 @@ theorem add.right_comm (n m k : ℕ) : n + m + k = n + k + m := right_comm add.comm add.assoc n m k theorem add.cancel_left {n m k : ℕ} : n + m = n + k → m = k := -induction_on n +nat.induction_on n (take H : 0 + m = 0 + k, !zero_add⁻¹ ⬝ H ⬝ !zero_add) (take (n : ℕ) (IH : n + m = n + k → m = k) (H : succ n + m = succ n + k), @@ -170,7 +170,7 @@ have H2 : m + n = m + k, from !add.comm ⬝ H ⬝ !add.comm, add.cancel_left H2 theorem eq_zero_of_add_eq_zero_right {n m : ℕ} : n + m = 0 → n = 0 := -induction_on n +nat.induction_on n (take (H : 0 + m = 0), rfl) (take k IH, assume H : succ k + m = 0, @@ -203,12 +203,12 @@ rfl -- commutativity, distributivity, associativity, identity theorem zero_mul (n : ℕ) : 0 * n = 0 := -induction_on n +nat.induction_on n !mul_zero (take m IH, !mul_succ ⬝ !add_zero ⬝ IH) theorem succ_mul (n m : ℕ) : (succ n) * m = (n * m) + m := -induction_on m +nat.induction_on m (!mul_zero ⬝ !mul_zero⁻¹ ⬝ !add_zero⁻¹) (take k IH, calc succ n * succ k = succ n * k + succ n : mul_succ @@ -220,7 +220,7 @@ induction_on m ... = n * succ k + succ k : mul_succ) theorem mul.comm (n m : ℕ) : n * m = m * n := -induction_on m +nat.induction_on m (!mul_zero ⬝ !zero_mul⁻¹) (take k IH, calc n * succ k = n * k + n : mul_succ @@ -228,7 +228,7 @@ induction_on m ... = (succ k) * n : succ_mul) theorem mul.right_distrib (n m k : ℕ) : (n + m) * k = n * k + m * k := -induction_on k +nat.induction_on k (calc (n + m) * 0 = 0 : mul_zero ... = 0 + 0 : add_zero @@ -251,7 +251,7 @@ calc ... = n * m + n * k : mul.comm theorem mul.assoc (n m k : ℕ) : (n * m) * k = n * (m * k) := -induction_on k +nat.induction_on k (calc (n * m) * 0 = n * (m * 0) : mul_zero) (take l IH, @@ -273,10 +273,10 @@ calc ... = n : mul_one theorem eq_zero_or_eq_zero_of_mul_eq_zero {n m : ℕ} : n * m = 0 → n = 0 ∨ m = 0 := -cases_on n +nat.cases_on n (assume H, or.inl rfl) (take n', - cases_on m + nat.cases_on m (assume H, or.inr rfl) (take m', assume H : succ n' * succ m' = 0, diff --git a/library/data/nat/div.lean b/library/data/nat/div.lean index 8ceeb7aa0..7d8093f6b 100644 --- a/library/data/nat/div.lean +++ b/library/data/nat/div.lean @@ -52,7 +52,7 @@ theorem add_div_self_left {x : ℕ} (z : ℕ) (H : x > 0) : (x + z) div x = succ !add.comm ▸ !add_div_self_right H theorem add_mul_div_self_right {x y z : ℕ} (H : z > 0) : (x + y * z) div z = x div z + y := -induction_on y +nat.induction_on y (calc (x + zero * z) div z = (x + zero) div z : zero_mul ... = x div z : add_zero ... = x div z + zero : add_zero) @@ -107,7 +107,7 @@ theorem add_mod_right {x z : ℕ} (H : x > 0) : (x + z) mod x = z mod x := !add.comm ▸ add_mod_left H theorem add_mul_mod_self_right {x y z : ℕ} (H : z > 0) : (x + y * z) mod z = x mod z := -induction_on y +nat.induction_on y (calc (x + zero * z) mod z = (x + zero) mod z : zero_mul ... = x mod z : add_zero) (take y, @@ -131,7 +131,7 @@ theorem mul_mod_right {m n : ℕ} : (m * n) mod m = 0 := !mul.comm ▸ !mul_mod_left theorem mod_lt {x y : ℕ} (H : y > 0) : x mod y < y := -case_strong_induction_on x +nat.case_strong_induction_on x (show 0 mod y < y, from !zero_mod⁻¹ ▸ H) (take x, assume IH : ∀x', x' ≤ x → x' mod y < y, @@ -160,7 +160,7 @@ by_cases_zero_pos y (take y, assume H : y > 0, show x = x div y * y + x mod y, from - case_strong_induction_on x + nat.case_strong_induction_on x (show 0 = (0 div y) * y + 0 mod y, by simp) (take x, assume IH : ∀x', x' ≤ x → x' = x' div y * y + x' mod y, @@ -254,7 +254,7 @@ have H1 : n mod 1 < 1, from mod_lt !succ_pos, eq_zero_of_le_zero (le_of_lt_succ H1) theorem mod_self (n : ℕ) : n mod n = 0 := -cases_on n (by simp) +nat.cases_on n (by simp) (take n, have H : (succ n * 1) mod (succ n * 1) = succ n * (1 mod 1), from !mul_mod_mul_left, @@ -411,7 +411,7 @@ private definition gcd.lt.dec (x y₁ : nat) : (succ y₁, x mod succ y₁) ≺ mod_lt (succ_pos y₁) definition gcd.F (p₁ : nat × nat) : (Π p₂ : nat × nat, p₂ ≺ p₁ → nat) → nat := -prod.cases_on p₁ (λx y, cases_on y +prod.cases_on p₁ (λx y, nat.cases_on y (λ f, x) (λ y₁ (f : Πp₂, p₂ ≺ (x, succ y₁) → nat), f (succ y₁, x mod succ y₁) !gcd.lt.dec)) @@ -429,7 +429,7 @@ calc gcd n 1 = gcd 1 (n mod 1) : gcd_succ n zero ... = 1 : gcd_zero_right theorem gcd_def (x y : ℕ) : gcd x y = if y = 0 then x else gcd y (x mod y) := -cases_on y +nat.cases_on y (calc gcd x 0 = x : gcd_zero_right x ... = if 0 = 0 then x else gcd zero (x mod zero) : (if_pos rfl)⁻¹) (λy₁, calc @@ -437,7 +437,7 @@ cases_on y ... = if succ y₁ = 0 then x else gcd (succ y₁) (x mod succ y₁) : (if_neg (succ_ne_zero y₁))⁻¹) theorem gcd_self (n : ℕ) : gcd n n = n := -cases_on n +nat.cases_on n rfl (λn₁, calc gcd (succ n₁) (succ n₁) = gcd (succ n₁) (succ n₁ mod succ n₁) : gcd_succ (succ n₁) n₁ @@ -445,7 +445,7 @@ cases_on n ... = succ n₁ : gcd_zero_right) theorem gcd_zero_left (n : nat) : gcd 0 n = n := -cases_on n +nat.cases_on n rfl (λ n₁, calc gcd 0 (succ n₁) = gcd (succ n₁) (0 mod succ n₁) : gcd_succ @@ -471,7 +471,7 @@ theorem gcd.induction {P : ℕ → ℕ → Prop} let Q : nat × nat → Prop := λ p : nat × nat, P (pr₁ p) (pr₂ p) in have aux : Q (m, n), from well_founded.induction (m, n) (λp, prod.cases_on p - (λm n, cases_on n + (λm n, nat.cases_on n (λ ih, show P (pr₁ (m, 0)) (pr₂ (m, 0)), from H0 m) (λ n₁ (ih : ∀p₂, p₂ ≺ (m, succ n₁) → P (pr₁ p₂) (pr₂ p₂)), have hlt₁ : 0 < succ n₁, from succ_pos n₁, diff --git a/library/data/nat/order.lean b/library/data/nat/order.lean index 2230c39a5..9d4b7d9ad 100644 --- a/library/data/nat/order.lean +++ b/library/data/nat/order.lean @@ -43,7 +43,7 @@ iff.intro (take H, lt_of_le_and_ne (and.elim_left H) (and.elim_right H)) theorem le_add_right (n k : ℕ) : n ≤ n + k := -induction_on k +nat.induction_on k (calc n ≤ n : le.refl n ... = n + zero : add_zero) (λ k (ih : n ≤ n + k), calc @@ -340,7 +340,7 @@ or_of_or_of_imp_left (succ_le_or_eq_of_le H) (take H2 : succ n ≤ succ m, show n ≤ m, from le_of_succ_le_succ H2) theorem le_pred_self (n : ℕ) : pred n ≤ n := -cases_on n +nat.cases_on n (pred_zero⁻¹ ▸ !le.refl) (take k : ℕ, (!pred_succ)⁻¹ ▸ !self_le_succ) @@ -367,7 +367,7 @@ protected theorem strong_induction_on {P : nat → Prop} (n : ℕ) (H : ∀n, ( P n := have H1 : ∀ {n m : nat}, m < n → P m, from take n, - induction_on n + nat.induction_on n (show ∀m, m < 0 → P m, from take m H, absurd H !not_lt_zero) (take n', assume IH : ∀ {m : nat}, m < n' → P m, @@ -385,7 +385,7 @@ protected theorem case_strong_induction_on {P : nat → Prop} (a : nat) (H0 : P strong_induction_on a ( take n, show (∀m, m < n → P m) → P n, from - cases_on n + nat.cases_on n (assume H : (∀m, m < 0 → P m), show P 0, from H0) (take n, assume H : (∀m, m < succ n → P m), @@ -395,7 +395,7 @@ strong_induction_on a ( /- pos -/ theorem by_cases_zero_pos {P : ℕ → Prop} (y : ℕ) (H0 : P 0) (H1 : ∀ {y : nat}, y > 0 → P y) : P y := -cases_on y H0 (take y, H1 !succ_pos) +nat.cases_on y H0 (take y, H1 !succ_pos) theorem eq_zero_or_pos (n : ℕ) : n = 0 ∨ n > 0 := or_of_or_of_imp_left diff --git a/library/data/nat/sub.lean b/library/data/nat/sub.lean index 4efa45bb7..74cbd9226 100644 --- a/library/data/nat/sub.lean +++ b/library/data/nat/sub.lean @@ -23,7 +23,7 @@ theorem sub_succ (n m : ℕ) : n - succ m = pred (n - m) := rfl theorem zero_sub (n : ℕ) : 0 - n = 0 := -induction_on n !sub_zero +nat.induction_on n !sub_zero (take k : nat, assume IH : 0 - k = 0, calc @@ -35,10 +35,10 @@ theorem succ_sub_succ (n m : ℕ) : succ n - succ m = n - m := succ_sub_succ_eq_sub n m theorem sub_self (n : ℕ) : n - n = 0 := -induction_on n !sub_zero (take k IH, !succ_sub_succ ⬝ IH) +nat.induction_on n !sub_zero (take k IH, !succ_sub_succ ⬝ IH) theorem add_sub_add_right (n k m : ℕ) : (n + k) - (m + k) = n - m := -induction_on k +nat.induction_on k (calc (n + 0) - (m + 0) = n - (m + 0) : {!add_zero} ... = n - m : {!add_zero}) @@ -54,7 +54,7 @@ theorem add_sub_add_left (k n m : ℕ) : (k + n) - (k + m) = n - m := !add.comm ▸ !add.comm ▸ !add_sub_add_right theorem add_sub_cancel (n m : ℕ) : n + m - m = n := -induction_on m +nat.induction_on m (!add_zero⁻¹ ▸ !sub_zero) (take k : ℕ, assume IH : n + k - k = n, @@ -67,7 +67,7 @@ theorem add_sub_cancel_left (n m : ℕ) : n + m - n = m := !add.comm ▸ !add_sub_cancel theorem sub_sub (n m k : ℕ) : n - m - k = n - (m + k) := -induction_on k +nat.induction_on k (calc n - m - 0 = n - m : sub_zero ... = n - (m + 0) : add_zero) @@ -107,7 +107,7 @@ rfl /- interaction with multiplication -/ theorem mul_pred_left (n m : ℕ) : pred n * m = n * m - m := -induction_on n +nat.induction_on n (calc pred 0 * m = 0 * m : pred_zero ... = 0 : zero_mul @@ -127,7 +127,7 @@ calc ... = n * m - n : mul.comm theorem mul_sub_right_distrib (n m k : ℕ) : (n - m) * k = n * k - m * k := -induction_on m +nat.induction_on m (calc (n - 0) * k = n * k : sub_zero ... = n * k - 0 : sub_zero diff --git a/library/data/num.lean b/library/data/num.lean index 01f68a9bb..8f9650b20 100644 --- a/library/data/num.lean +++ b/library/data/num.lean @@ -11,10 +11,10 @@ open bool namespace pos_num theorem succ_not_is_one (a : pos_num) : is_one (succ a) = ff := - induction_on a rfl (take n iH, rfl) (take n iH, rfl) + pos_num.induction_on a rfl (take n iH, rfl) (take n iH, rfl) theorem pred.succ (a : pos_num) : pred (succ a) = a := - rec_on a + pos_num.rec_on a rfl (take (n : pos_num) (iH : pred (succ n) = n), calc @@ -59,7 +59,7 @@ namespace pos_num rfl theorem mul.one_right (a : pos_num) : a * one = a := - induction_on a + pos_num.induction_on a rfl (take (n : pos_num) (iH : n * one = n), calc bit1 n * one = bit0 (n * one) + one : rfl diff --git a/library/data/option.lean b/library/data/option.lean index a2c2ddadb..ff3ec6560 100644 --- a/library/data/option.lean +++ b/library/data/option.lean @@ -11,7 +11,7 @@ open eq.ops decidable namespace option definition is_none {A : Type} (o : option A) : Prop := - rec true (λ a, false) o + option.rec true (λ a, false) o theorem is_none_none {A : Type} : is_none (@none A) := trivial @@ -20,19 +20,19 @@ namespace option not_false theorem none_ne_some {A : Type} (a : A) : none ≠ some a := - assume H, no_confusion H + assume H, option.no_confusion H theorem some.inj {A : Type} {a₁ a₂ : A} (H : some a₁ = some a₂) : a₁ = a₂ := - no_confusion H (λe, e) + option.no_confusion H (λe, e) protected definition is_inhabited [instance] (A : Type) : inhabited (option A) := inhabited.mk none protected definition has_decidable_eq [instance] {A : Type} (H : decidable_eq A) : decidable_eq (option A) := take o₁ o₂ : option A, - rec_on o₁ - (rec_on o₂ (inl rfl) (take a₂, (inr (none_ne_some a₂)))) - (take a₁ : A, rec_on o₂ + option.rec_on o₁ + (option.rec_on o₂ (inl rfl) (take a₂, (inr (none_ne_some a₂)))) + (take a₁ : A, option.rec_on o₂ (inr (ne.symm (none_ne_some a₁))) (take a₂ : A, decidable.rec_on (H a₁ a₂) (assume Heq : a₁ = a₂, inl (Heq ▸ rfl)) diff --git a/library/data/sum.lean b/library/data/sum.lean index cac92fa86..1086f1178 100644 --- a/library/data/sum.lean +++ b/library/data/sum.lean @@ -22,16 +22,16 @@ namespace sum variables {A B : Type} definition inl_ne_inr (a : A) (b : B) : inl a ≠ inr b := - assume H, no_confusion H + assume H, sum.no_confusion H definition inr_ne_inl (b : B) (a : A) : inr b ≠ inl a := - assume H, no_confusion H + assume H, sum.no_confusion H definition inl_inj {a₁ a₂ : A} : intro_left B a₁ = intro_left B a₂ → a₁ = a₂ := - assume H, no_confusion H (λe, e) + assume H, sum.no_confusion H (λe, e) definition inr_inj {b₁ b₂ : B} : intro_right A b₁ = intro_right A b₂ → b₁ = b₂ := - assume H, no_confusion H (λe, e) + assume H, sum.no_confusion H (λe, e) protected definition is_inhabited_left [instance] : inhabited A → inhabited (A + B) := assume H : inhabited A, inhabited.mk (inl (default A)) diff --git a/library/data/unit.lean b/library/data/unit.lean index 1ff796278..6c8568193 100644 --- a/library/data/unit.lean +++ b/library/data/unit.lean @@ -12,10 +12,10 @@ namespace unit notation `⋆` := star protected theorem equal (a b : unit) : a = b := - rec_on a (rec_on b rfl) + unit.rec_on a (unit.rec_on b rfl) theorem eq_star (a : unit) : a = star := - equal a star + unit.equal a star protected theorem subsingleton [instance] : subsingleton unit := subsingleton.intro (λ a b, equal a b) diff --git a/library/init/bool.lean b/library/init/bool.lean index 4b7b08baf..bcb60b755 100644 --- a/library/init/bool.lean +++ b/library/init/bool.lean @@ -6,18 +6,18 @@ import init.datatypes init.reserved_notation namespace bool definition cond {A : Type} (b : bool) (t e : A) := - rec_on b e t + bool.rec_on b e t definition bor (a b : bool) := - rec_on a (rec_on b ff tt) tt + bool.rec_on a (bool.rec_on b ff tt) tt notation a || b := bor a b definition band (a b : bool) := - rec_on a ff (rec_on b ff tt) + bool.rec_on a ff (bool.rec_on b ff tt) notation a && b := band a b definition bnot (a : bool) := - rec_on a tt ff + bool.rec_on a tt ff end bool diff --git a/library/init/datatypes.lean b/library/init/datatypes.lean index 0b7b9a96f..814626fb1 100644 --- a/library/init/datatypes.lean +++ b/library/init/datatypes.lean @@ -82,7 +82,7 @@ bit0 : pos_num → pos_num namespace pos_num definition succ (a : pos_num) : pos_num := - rec_on a (bit0 one) (λn r, bit0 r) (λn r, bit1 n) + pos_num.rec_on a (bit0 one) (λn r, bit0 r) (λn r, bit1 n) end pos_num inductive num : Type := @@ -92,7 +92,7 @@ pos : pos_num → num namespace num open pos_num definition succ (a : num) : num := - rec_on a (pos one) (λp, pos (succ p)) + num.rec_on a (pos one) (λp, pos (succ p)) end num inductive bool : Type := diff --git a/library/init/logic.lean b/library/init/logic.lean index 556c9a111..f9ab4baef 100644 --- a/library/init/logic.lean +++ b/library/init/logic.lean @@ -37,13 +37,13 @@ namespace eq variables {a b c a': A} theorem subst {P : A → Prop} (H₁ : a = b) (H₂ : P a) : P b := - rec H₂ H₁ + eq.rec H₂ H₁ theorem trans (H₁ : a = b) (H₂ : b = c) : a = c := subst H₂ H₁ definition symm (H : a = b) : b = a := - rec (refl a) H + eq.rec (refl a) H namespace ops notation H `⁻¹` := symm H --input with \sy or \-1 or \inv @@ -124,10 +124,10 @@ namespace heq eq.rec_on (to_eq H₁) H₂ theorem subst {P : ∀T : Type, T → Prop} (H₁ : a == b) (H₂ : P A a) : P B b := - rec_on H₁ H₂ + heq.rec_on H₁ H₂ theorem symm (H : a == b) : b == a := - rec_on H (refl a) + heq.rec_on H (refl a) theorem of_eq (H : a = a') : a == a' := eq.subst H (refl a) @@ -167,7 +167,7 @@ notation a ∨ b := or a b namespace or theorem elim (H₁ : a ∨ b) (H₂ : a → c) (H₃ : b → c) : c := - rec H₂ H₃ H₁ + or.rec H₂ H₃ H₁ end or /- iff -/ @@ -254,15 +254,15 @@ namespace decidable variables {p q : Prop} definition rec_on_true [H : decidable p] {H1 : p → Type} {H2 : ¬p → Type} (H3 : p) (H4 : H1 H3) - : rec_on H H1 H2 := - rec_on H (λh, H4) (λh, !false.rec (h H3)) + : decidable.rec_on H H1 H2 := + decidable.rec_on H (λh, H4) (λh, !false.rec (h H3)) definition rec_on_false [H : decidable p] {H1 : p → Type} {H2 : ¬p → Type} (H3 : ¬p) (H4 : H2 H3) - : rec_on H H1 H2 := - rec_on H (λh, false.rec _ (H3 h)) (λh, H4) + : decidable.rec_on H H1 H2 := + decidable.rec_on H (λh, false.rec _ (H3 h)) (λh, H4) definition by_cases {q : Type} [C : decidable p] (Hpq : p → q) (Hnpq : ¬p → q) : q := - rec_on C (assume Hp, Hpq Hp) (assume Hnp, Hnpq Hnp) + decidable.rec_on C (assume Hp, Hpq Hp) (assume Hnp, Hnpq Hnp) theorem em (p : Prop) [H : decidable p] : p ∨ ¬p := by_cases (λ Hp, or.inl Hp) (λ Hnp, or.inr Hnp) diff --git a/library/init/nat.lean b/library/init/nat.lean index 858ef868d..30330cda1 100644 --- a/library/init/nat.lean +++ b/library/init/nat.lean @@ -24,7 +24,7 @@ namespace nat notation a ≤ b := le a b definition pred (a : nat) : nat := - cases_on a zero (λ a₁, a₁) + nat.cases_on a zero (λ a₁, a₁) protected definition is_inhabited [instance] : inhabited nat := inhabited.mk zero @@ -40,17 +40,17 @@ namespace nat -- less-than is well-founded definition lt.wf [instance] : well_founded lt := - well_founded.intro (λn, rec_on n + well_founded.intro (λn, nat.rec_on n (acc.intro zero (λ (y : nat) (hlt : y < zero), have aux : ∀ {n₁}, y < n₁ → zero = n₁ → acc lt y, from - λ n₁ hlt, lt.cases_on hlt - (λ heq, no_confusion heq) - (λ b hlt heq, no_confusion heq), + λ n₁ hlt, nat.lt.cases_on hlt + (λ heq, nat.no_confusion heq) + (λ b hlt heq, nat.no_confusion heq), aux hlt rfl)) (λ (n : nat) (ih : acc lt n), acc.intro (succ n) (λ (m : nat) (hlt : m < succ n), have aux : ∀ {n₁} (hlt : m < n₁), succ n = n₁ → acc lt m, from - λ n₁ hlt, lt.cases_on hlt + λ n₁ hlt, nat.lt.cases_on hlt (λ (heq : succ n = succ m), nat.no_confusion heq (λ (e : n = m), eq.rec_on e ih)) @@ -73,7 +73,7 @@ namespace nat λ H, aux H rfl definition zero_lt_succ (a : nat) : zero < succ a := - rec_on a + nat.rec_on a (lt.base zero) (λ a (hlt : zero < succ a), lt.step hlt) @@ -106,9 +106,9 @@ namespace nat aux definition lt.is_decidable_rel [instance] : decidable_rel lt := - λ a b, rec_on b + λ a b, nat.rec_on b (λ (a : nat), inr (not_lt_zero a)) - (λ (b₁ : nat) (ih : ∀ a, decidable (a < b₁)) (a : nat), cases_on a + (λ (b₁ : nat) (ih : ∀ a, decidable (a < b₁)) (a : nat), nat.cases_on a (inl !zero_lt_succ) (λ a, decidable.rec_on (ih a) (λ h_pos : a < b₁, inl (succ_lt_succ h_pos)) @@ -147,7 +147,7 @@ namespace nat end definition lt.irrefl (a : nat) : ¬ a < a := - rec_on a + nat.rec_on a !not_lt_zero (λ (a : nat) (ih : ¬ a < a) (h : succ a < succ a), ih (lt_of_succ_lt_succ h)) @@ -158,11 +158,11 @@ namespace nat (λ b hlt (ih : ¬ b < a) (h : succ b < a), ih (lt_of_succ_lt h)) definition lt.trichotomy (a b : nat) : a < b ∨ a = b ∨ b < a := - rec_on b - (λa, cases_on a + nat.rec_on b + (λa, nat.cases_on a (or.inr (or.inl rfl)) (λ a₁, or.inr (or.inr !zero_lt_succ))) - (λ b₁ (ih : ∀a, a < b₁ ∨ a = b₁ ∨ b₁ < a) (a : nat), cases_on a + (λ b₁ (ih : ∀a, a < b₁ ∨ a = b₁ ∨ b₁ < a) (a : nat), nat.cases_on a (or.inl !zero_lt_succ) (λ a, or.rec_on (ih a) (λ h : a < b₁, or.inl (succ_lt_succ h)) @@ -274,24 +274,24 @@ namespace nat notation a ≥ b := ge a b definition add (a b : nat) : nat := - rec_on b a (λ b₁ r, succ r) + nat.rec_on b a (λ b₁ r, succ r) notation a + b := add a b definition sub (a b : nat) : nat := - rec_on b a (λ b₁ r, pred r) + nat.rec_on b a (λ b₁ r, pred r) notation a - b := sub a b definition mul (a b : nat) : nat := - rec_on b zero (λ b₁ r, r + a) + nat.rec_on b zero (λ b₁ r, r + a) notation a * b := mul a b context attribute sub [reducible] definition succ_sub_succ_eq_sub (a b : nat) : succ a - succ b = a - b := - induction_on b + nat.induction_on b rfl (λ b₁ (ih : succ a - succ b₁ = a - b₁), eq.rec_on ih (eq.refl (pred (succ a - succ b₁)))) @@ -301,7 +301,7 @@ namespace nat eq.rec_on (succ_sub_succ_eq_sub a b) rfl definition zero_sub_eq_zero (a : nat) : zero - a = zero := - induction_on a + nat.induction_on a rfl (λ a₁ (ih : zero - a₁ = zero), eq.rec_on ih (eq.refl (pred (zero - a₁)))) @@ -325,12 +325,12 @@ namespace nat λ h₁ h₂, aux h₁ h₂ definition pred_le (a : nat) : pred a ≤ a := - cases_on a + nat.cases_on a (le.refl zero) (λ a₁, le_of_lt (lt.base a₁)) definition sub_le (a b : nat) : a - b ≤ a := - induction_on b + nat.induction_on b (le.refl a) (λ b₁ ih, le.trans !pred_le ih) diff --git a/library/init/num.lean b/library/init/num.lean index c20d55bc5..d94c40475 100644 --- a/library/init/num.lean +++ b/library/init/num.lean @@ -14,22 +14,22 @@ inhabited.mk pos_num.one namespace pos_num definition is_one (a : pos_num) : bool := - rec_on a tt (λn r, ff) (λn r, ff) + pos_num.rec_on a tt (λn r, ff) (λn r, ff) definition pred (a : pos_num) : pos_num := - rec_on a one (λn r, bit0 n) (λn r, cond (is_one n) one (bit1 r)) + pos_num.rec_on a one (λn r, bit0 n) (λn r, cond (is_one n) one (bit1 r)) definition size (a : pos_num) : pos_num := - rec_on a one (λn r, succ r) (λn r, succ r) + pos_num.rec_on a one (λn r, succ r) (λn r, succ r) definition add (a b : pos_num) : pos_num := - rec_on a + pos_num.rec_on a succ - (λn f b, rec_on b + (λn f b, pos_num.rec_on b (succ (bit1 n)) (λm r, succ (bit1 (f m))) (λm r, bit1 (f m))) - (λn f b, rec_on b + (λn f b, pos_num.rec_on b (bit1 n) (λm r, bit1 (f m)) (λm r, bit0 (f m))) @@ -38,7 +38,7 @@ namespace pos_num notation a + b := add a b definition mul (a b : pos_num) : pos_num := - rec_on a + pos_num.rec_on a b (λn r, bit0 r + b) (λn r, bit0 r) @@ -54,16 +54,16 @@ namespace num open pos_num definition pred (a : num) : num := - rec_on a zero (λp, cond (is_one p) zero (pos (pred p))) + num.rec_on a zero (λp, cond (is_one p) zero (pos (pred p))) definition size (a : num) : num := - rec_on a (pos one) (λp, pos (size p)) + num.rec_on a (pos one) (λp, pos (size p)) definition add (a b : num) : num := - rec_on a b (λp_a, rec_on b (pos p_a) (λp_b, pos (pos_num.add p_a p_b))) + num.rec_on a b (λp_a, num.rec_on b (pos p_a) (λp_b, pos (pos_num.add p_a p_b))) definition mul (a b : num) : num := - rec_on a zero (λp_a, rec_on b zero (λp_b, pos (pos_num.mul p_a p_b))) + num.rec_on a zero (λp_a, num.rec_on b zero (λp_b, pos (pos_num.mul p_a p_b))) notation a + b := add a b notation a * b := mul a b diff --git a/library/init/prod.lean b/library/init/prod.lean index 417d4e13f..02be42cb4 100644 --- a/library/init/prod.lean +++ b/library/init/prod.lean @@ -59,8 +59,8 @@ namespace prod (iHb : ∀y, Rb y xb → acc (lex Ra Rb) (xa, y)), acc.intro (xa, xb) (λp (lt : p ≺ (xa, xb)), have aux : xa = xa → xb = xb → acc (lex Ra Rb) p, from - @lex.rec_on A B Ra Rb (λp₁ p₂, pr₁ p₂ = xa → pr₂ p₂ = xb → acc (lex Ra Rb) p₁) - p (xa, xb) lt + @prod.lex.rec_on A B Ra Rb (λp₁ p₂, pr₁ p₂ = xa → pr₂ p₂ = xb → acc (lex Ra Rb) p₁) + p (xa, xb) lt (λa₁ b₁ a₂ b₂ (H : Ra a₁ a₂) (eq₂ : a₂ = xa) (eq₃ : b₂ = xb), show acc (lex Ra Rb) (a₁, b₁), from have Ra₁ : Ra a₁ xa, from eq.rec_on eq₂ H, @@ -78,7 +78,7 @@ namespace prod -- Relational product is a subrelation of the lex definition rprod.sub_lex : ∀ a b, rprod Ra Rb a b → lex Ra Rb a b := - λa b H, rprod.rec_on H (λ a₁ b₁ a₂ b₂ H₁ H₂, lex.left Rb a₂ b₂ H₁) + λa b H, prod.rprod.rec_on H (λ a₁ b₁ a₂ b₂ H₁ H₂, lex.left Rb a₂ b₂ H₁) -- The relational product of well founded relations is well-founded definition rprod.wf (Ha : well_founded Ra) (Hb : well_founded Rb) : well_founded (rprod Ra Rb) := diff --git a/library/init/sigma.lean b/library/init/sigma.lean index 95d2c4929..1692d22f7 100644 --- a/library/init/sigma.lean +++ b/library/init/sigma.lean @@ -48,8 +48,8 @@ namespace sigma (iHb : ∀ (y : B xa), Rb xa y xb → acc (lex Ra Rb) ⟨xa, y⟩), acc.intro ⟨xa, xb⟩ (λp (lt : p ≺ ⟨xa, xb⟩), have aux : xa = xa → xb == xb → acc (lex Ra Rb) p, from - @lex.rec_on A B Ra Rb (λp₁ p₂, p₂.1 = xa → p₂.2 == xb → acc (lex Ra Rb) p₁) - p ⟨xa, xb⟩ lt + @sigma.lex.rec_on A B Ra Rb (λp₁ p₂, p₂.1 = xa → p₂.2 == xb → acc (lex Ra Rb) p₁) + p ⟨xa, xb⟩ lt (λ (a₁ : A) (b₁ : B a₁) (a₂ : A) (b₂ : B a₂) (H : Ra a₁ a₂) (eq₂ : a₂ = xa) (eq₃ : b₂ == xb), begin cases eq₂, exact (iHa a₁ H b₁) end) (λ (a : A) (b₁ b₂ : B a) (H : Rb a b₁ b₂) (eq₂ : a = xa) (eq₃ : b₂ == xb), diff --git a/library/logic/cast.lean b/library/logic/cast.lean index 6291b7bb8..dc06984f9 100644 --- a/library/logic/cast.lean +++ b/library/logic/cast.lean @@ -36,7 +36,7 @@ namespace heq theorem drec_on {C : Π {B : Type} (b : B), a == b → Type} (H₁ : a == b) (H₂ : C a (refl a)) : C b H₁ := - rec (λ H₁ : a == a, show C a H₁, from H₂) H₁ H₁ + heq.rec (λ H₁ : a == a, show C a H₁, from H₂) H₁ H₁ theorem to_cast_eq (H : a == b) : cast (type_eq H) a = b := drec_on H !cast_eq diff --git a/library/logic/eq.lean b/library/logic/eq.lean index 53110825b..12db9e237 100644 --- a/library/logic/eq.lean +++ b/library/logic/eq.lean @@ -22,17 +22,17 @@ namespace eq definition drec_on {B : Πa' : A, a = a' → Type} (H₁ : a = a') (H₂ : B a (refl a)) : B a' H₁ := eq.rec (λH₁ : a = a, show B a H₁, from H₂) H₁ H₁ - theorem rec_on_id {B : A → Type} (H : a = a) (b : B a) : rec_on H b = b := + theorem rec_on_id {B : A → Type} (H : a = a) (b : B a) : eq.rec_on H b = b := rfl - theorem rec_on_constant (H : a = a') {B : Type} (b : B) : rec_on H b = b := + theorem rec_on_constant (H : a = a') {B : Type} (b : B) : eq.rec_on H b = b := drec_on H rfl - theorem rec_on_constant2 (H₁ : a₁ = a₂) (H₂ : a₃ = a₄) (b : B) : rec_on H₁ b = rec_on H₂ b := + theorem rec_on_constant2 (H₁ : a₁ = a₂) (H₂ : a₃ = a₄) (b : B) : eq.rec_on H₁ b = eq.rec_on H₂ b := rec_on_constant H₁ b ⬝ (rec_on_constant H₂ b)⁻¹ theorem rec_on_irrel_arg {f : A → B} {D : B → Type} (H : a = a') (H' : f a = f a') (b : D (f a)) : - rec_on H b = rec_on H' b := + eq.rec_on H b = eq.rec_on H' b := drec_on H (λ(H' : f a = f a), !rec_on_id⁻¹) H' theorem rec_on_irrel {a a' : A} {D : A → Type} (H H' : a = a') (b : D a) : @@ -40,8 +40,8 @@ namespace eq proof_irrel H H' ▸ rfl theorem rec_on_compose {a b c : A} {P : A → Type} (H₁ : a = b) (H₂ : b = c) - (u : P a) : rec_on H₂ (rec_on H₁ u) = rec_on (trans H₁ H₂) u := - (show ∀ H₂ : b = c, rec_on H₂ (rec_on H₁ u) = rec_on (trans H₁ H₂) u, + (u : P a) : eq.rec_on H₂ (eq.rec_on H₁ u) = eq.rec_on (trans H₁ H₂) u := + (show ∀ H₂ : b = c, eq.rec_on H₂ (eq.rec_on H₁ u) = eq.rec_on (trans H₁ H₂) u, from drec_on H₂ (take (H₂ : b = b), rec_on_id H₂ _)) H₂ end eq diff --git a/library/logic/subsingleton.lean b/library/logic/subsingleton.lean index 0fe2e0ddc..2fd975be8 100644 --- a/library/logic/subsingleton.lean +++ b/library/logic/subsingleton.lean @@ -12,7 +12,7 @@ inductive subsingleton [class] (A : Type) : Prop := intro : (∀ a b : A, a = b) → subsingleton A namespace subsingleton -definition elim {A : Type} {H : subsingleton A} : ∀(a b : A), a = b := rec (fun p, p) H +definition elim {A : Type} {H : subsingleton A} : ∀(a b : A), a = b := subsingleton.rec (fun p, p) H end subsingleton protected definition prop.subsingleton [instance] (P : Prop) : subsingleton P := diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index f1d41fddb..f8db02923 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -22,6 +22,7 @@ Author: Leonardo de Moura #include "library/parser_nested_exception.h" #include "library/aliases.h" #include "library/private.h" +#include "library/protected.h" #include "library/choice.h" #include "library/placeholder.h" #include "library/deep_copy.h" @@ -1086,7 +1087,8 @@ expr parser::id_to_expr(name const & id, pos_info const & p) { for (name const & ns : get_namespaces(m_env)) { auto new_id = ns + id; - if (!ns.is_anonymous() && m_env.find(new_id)) { + if (!ns.is_anonymous() && m_env.find(new_id) && + (!id.is_atomic() || !is_protected(m_env, new_id))) { auto r = save_pos(mk_constant(new_id, ls), p); save_type_info(r); add_ref_index(new_id, p); diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp index f0d7b9c2c..4503bbce5 100644 --- a/src/frontends/lean/pp.cpp +++ b/src/frontends/lean/pp.cpp @@ -18,6 +18,7 @@ Author: Leonardo de Moura #include "library/expr_pair.h" #include "library/placeholder.h" #include "library/private.h" +#include "library/protected.h" #include "library/explicit.h" #include "library/typed_expr.h" #include "library/num.h" @@ -418,7 +419,9 @@ auto pretty_fn::pp_const(expr const & e) -> result { for (name const & ns : get_namespaces(m_env)) { if (!ns.is_anonymous()) { name new_n = n.replace_prefix(ns, name()); - if (new_n != n && !new_n.is_anonymous()) { + if (new_n != n && + !new_n.is_anonymous() && + (!new_n.is_atomic() || !is_protected(m_env, n))) { n = new_n; break; } diff --git a/src/frontends/lean/server.cpp b/src/frontends/lean/server.cpp index 4c6a2bfb3..e4d46d107 100644 --- a/src/frontends/lean/server.cpp +++ b/src/frontends/lean/server.cpp @@ -17,6 +17,7 @@ Author: Leonardo de Moura #include "library/aliases.h" #include "library/type_util.h" #include "library/unifier.h" +#include "library/protected.h" #include "library/reducible.h" #include "library/projection.h" #include "library/scoped_ext.h" @@ -571,7 +572,7 @@ optional is_essentially_atomic(environment const & env, name const & n) { for (name const & ns : ns_list) { if (is_prefix_of(ns, n)) { auto n_prime = n.replace_prefix(ns, name()); - if (n_prime.is_atomic()) + if (n_prime.is_atomic() && !is_protected(env, n)) return optional(n_prime); break; } @@ -586,8 +587,11 @@ void server::display_decl(name const & d, environment const & env, options const // using namespace override resolution rule list const & ns_list = get_namespaces(env); for (name const & ns : ns_list) { - if (is_prefix_of(ns, d) && ns != d) { - display_decl(d.replace_prefix(ns, name()), d, env, o); + name new_d = d.replace_prefix(ns, name()); + if (new_d != d && + !new_d.is_anonymous() && + (!new_d.is_atomic() || !is_protected(env, d))) { + display_decl(new_d, d, env, o); return; } } diff --git a/tests/lean/hott/noc.hlean b/tests/lean/hott/noc.hlean index 263a5939d..50eaa5fa9 100644 --- a/tests/lean/hott/noc.hlean +++ b/tests/lean/hott/noc.hlean @@ -10,6 +10,6 @@ namespace foo {A₂ : Type} {B₂ : A₂ → Type} {a₂ : A₂} {b₂ : B₂ a₂} (H : foo.mk A₁ B₁ a₁ b₁ = foo.mk A₂ B₂ a₂ b₂) : A₁ = A₂ - := lift.down (no_confusion H (λ e₁ e₂ e₃ e₄, e₁)) + := lift.down (foo.no_confusion H (λ e₁ e₂ e₃ e₄, e₁)) end foo diff --git a/tests/lean/hott/noc_list.hlean b/tests/lean/hott/noc_list.hlean index d61ccbfc6..c31b66c7a 100644 --- a/tests/lean/hott/noc_list.hlean +++ b/tests/lean/hott/noc_list.hlean @@ -6,12 +6,12 @@ namespace list open lift theorem nil_ne_cons {A : Type} (a : A) (v : list A) : nil ≠ cons a v := - λ H, down (no_confusion H) + λ H, down (list.no_confusion H) theorem cons.inj₁ {A : Type} (a₁ a₂ : A) (v₁ v₂ : list A) : cons a₁ v₁ = cons a₂ v₂ → a₁ = a₂ := - λ H, down (no_confusion H (λ (h₁ : a₁ = a₂) (h₂ : v₁ = v₂), h₁)) + λ H, down (list.no_confusion H (λ (h₁ : a₁ = a₂) (h₂ : v₁ = v₂), h₁)) theorem cons.inj₂ {A : Type} (a₁ a₂ : A) (v₁ v₂ : list A) : cons a₁ v₁ = cons a₂ v₂ → v₁ = v₂ := - λ H, down (no_confusion H (λ (h₁ : a₁ = a₂) (h₂ : v₁ = v₂), h₂)) + λ H, down (list.no_confusion H (λ (h₁ : a₁ = a₂) (h₂ : v₁ = v₂), h₂)) end list diff --git a/tests/lean/hott/sig_noc.hlean b/tests/lean/hott/sig_noc.hlean index 63735732c..90c3c798e 100644 --- a/tests/lean/hott/sig_noc.hlean +++ b/tests/lean/hott/sig_noc.hlean @@ -6,7 +6,7 @@ namespace sigma variables {a₁ a₂ : A} {b₁ : B a₁} {b₂ : B a₂} definition dpair.inj (H : ⟨a₁, b₁⟩ = ⟨a₂, b₂⟩) : Σ (e₁ : a₁ = a₂), eq.rec b₁ e₁ = b₂ := - down (no_confusion H (λ e₁ e₂, ⟨e₁, e₂⟩)) + down (sigma.no_confusion H (λ e₁ e₂, ⟨e₁, e₂⟩)) definition dpair.inj₁ (H : ⟨a₁, b₁⟩ = ⟨a₂, b₂⟩) : a₁ = a₂ := (dpair.inj H).1 @@ -29,7 +29,7 @@ namespace foo definition foo.inj (H : mk A₁ B₁ a₁ b₁ = mk A₂ B₂ a₂ b₂) : Σ (e₁ : A₁ = A₂) (e₂ : eq.rec B₁ e₁ = B₂) (e₃ : eq.rec a₁ e₁ = a₂), eq.rec (eq.rec (eq.rec b₁ e₁) e₂) e₃ = b₂ := - down (no_confusion H (λ e₁ e₂ e₃ e₄, ⟨e₁, e₂, e₃, e₄⟩)) + down (foo.no_confusion H (λ e₁ e₂ e₃ e₄, ⟨e₁, e₂, e₃, e₄⟩)) definition foo.inj₁ (H : mk A₁ B₁ a₁ b₁ = mk A₂ B₂ a₂ b₂) : A₁ = A₂ := (foo.inj H).1 diff --git a/tests/lean/interactive/auto_comp.input b/tests/lean/interactive/auto_comp.input new file mode 100644 index 000000000..9e4a44f08 --- /dev/null +++ b/tests/lean/interactive/auto_comp.input @@ -0,0 +1,15 @@ +VISIT auto_comp.lean +SYNC 8 +prelude +inductive nat := zero : nat, succ : nat → nat +inductive bool := ff, tt +namespace nat + inductive le : nat → nat → Type.{0} := refl : Π a, le a a + +end nat + +WAIT +FINDP 6 +rec_on +FINDP 8 +rec_on \ No newline at end of file diff --git a/tests/lean/interactive/auto_comp.input.expected.out b/tests/lean/interactive/auto_comp.input.expected.out new file mode 100644 index 000000000..2880ae1b5 --- /dev/null +++ b/tests/lean/interactive/auto_comp.input.expected.out @@ -0,0 +1,12 @@ +-- BEGINWAIT +-- ENDWAIT +-- BEGINFINDP +le.rec_on|le ?a ?a → (Π (a : nat), ?C a a) → ?C ?a ?a +nat.rec_on|Π (n : nat), ?C zero → (Π (a : nat), ?C a → ?C (succ a)) → ?C n +bool.rec_on|Π (n : bool), ?C bool.ff → ?C bool.tt → ?C n +-- ENDFINDP +-- BEGINFINDP +nat.le.rec_on|nat.le ?a ?a → (Π (a : nat), ?C a a) → ?C ?a ?a +nat.rec_on|Π (n : nat), ?C nat.zero → (Π (a : nat), ?C a → ?C (nat.succ a)) → ?C n +bool.rec_on|Π (n : bool), ?C bool.ff → ?C bool.tt → ?C n +-- ENDFINDP diff --git a/tests/lean/interactive/eq2.input b/tests/lean/interactive/eq2.input index 36c3fe147..abbe4bdf4 100644 --- a/tests/lean/interactive/eq2.input +++ b/tests/lean/interactive/eq2.input @@ -1,7 +1,7 @@ VISIT eq2.lean WAIT REPLACE 134 - (λ (b₂ : B a₁) (H₂ : b₁ = b₂) (c₂ : C a₁ b₂) (H₃ : (rec_on (congr_arg2_dep C (refl a₁) H₂) c₁) = c₂), + (λ (b₂ : B a₁) (H₂ : b₁ = b₂) (c₂ : C a₁ b₂) (H₃ : (eq.rec_on (congr_arg2_dep C (refl a₁) H₂) c₁) = c₂), WAIT REPLACE 134 (λ (b₂ : B a₁) (H₂ : b₁ = b₂) (c₂ : C a₁ b₂) (H₃ : _ = c₂), diff --git a/tests/lean/interactive/eq2.lean b/tests/lean/interactive/eq2.lean index 5000440e9..282bbfeb9 100644 --- a/tests/lean/interactive/eq2.lean +++ b/tests/lean/interactive/eq2.lean @@ -28,7 +28,7 @@ namespace eq proof_irrel theorem subst {A : Type} {a b : A} {P : A → Prop} (H1 : a = b) (H2 : P a) : P b := - rec H2 H1 + eq.rec H2 H1 theorem trans {A : Type} {a b c : A} (H1 : a = b) (H2 : b = c) : a = c := subst H2 H1 @@ -69,7 +69,7 @@ namespace eq theorem drec_on_irrel {A B : Type} {a a' : A} {f : A → B} {D : B → Type} (H : a = a') (H' : f a = f a') (b : D (f a)) : drec_on H b = drec_on H' b := drec_on H (λ(H : a = a) (H' : f a = f a), drec_on_id H b ⬝ drec_on_id H' b⁻¹) H H' - theorem rec_id {A : Type} {a : A} {B : A → Type} (H : a = a) (b : B a) : rec b H = b := + theorem rec_id {A : Type} {a : A} {B : A → Type} (H : a = a) (b : B a) : eq.rec b H = b := id_refl H⁻¹ ▸ refl (eq.rec b (refl a)) theorem drec_on_compose {A : Type} {a b c : A} {P : A → Type} (H1 : a = b) (H2 : b = c) diff --git a/tests/lean/interactive/extra_type.input b/tests/lean/interactive/extra_type.input index 21885b759..b1c3006ff 100644 --- a/tests/lean/interactive/extra_type.input +++ b/tests/lean/interactive/extra_type.input @@ -2,26 +2,26 @@ VISIT extra_type.lean SET pp.notation false SYNC 20 -import general_notation -import logic.connectives logic.decidable logic.inhabited - -open eq eq.ops decidable - +prelude +definition Prop := Type.{0} +inductive eq {A : Type} (a : A) : A → Prop := refl : eq a a +infix `=`:50 := eq +definition rfl {A : Type} {a : A} := eq.refl a +inductive or (A B : Prop) : Prop := inl {} : A → or A B, inr {} : B → or A B +infix `∨`:35 := or inductive bool : Type := ff : bool, tt : bool namespace bool - protected definition rec_on {C : bool → Type} (b : bool) (H₁ : C ff) (H₂ : C tt) : C b := - rec H₁ H₂ b - - protected definition cases_on {p : bool → Prop} (b : bool) (H₁ : p ff) (H₂ : p tt) : p b := - rec H₁ H₂ b - + protected definition rec_on2 {C : bool → Type} (b : bool) (H₁ : C ff) (H₂ : C tt) : C b := + bool.rec H₁ H₂ b + protected definition cases_on2 {p : bool → Prop} (b : bool) (H₁ : p ff) (H₂ : p tt) : p b := + bool.rec H₁ H₂ b definition cond {A : Type} (b : bool) (t e : A) := - rec_on b e t + bool.rec_on b e t theorem dichotomy (b : bool) : b = ff ∨ b = tt := - cases_on b (or.inl rfl) (or.inr rfl) + bool.cases_on2 b (or.inl rfl) (or.inr rfl) end bool WAIT -INFO 20 13 +INFO 20 19 diff --git a/tests/lean/interactive/extra_type.input.expected.out b/tests/lean/interactive/extra_type.input.expected.out index 1b694477e..d1b71814e 100644 --- a/tests/lean/interactive/extra_type.input.expected.out +++ b/tests/lean/interactive/extra_type.input.expected.out @@ -4,12 +4,12 @@ -- BEGINWAIT -- ENDWAIT -- BEGININFO --- EXTRA_TYPE|20|13 +-- EXTRA_TYPE|20|19 or.inl rfl -- or (eq ff ff) (eq ff tt) -- ACK --- SYMBOL|20|13 +-- SYMBOL|20|19 ( -- ACK -- ENDINFO diff --git a/tests/lean/interactive/num2.input.expected.out b/tests/lean/interactive/num2.input.expected.out index 81e7502c8..2ed166687 100644 --- a/tests/lean/interactive/num2.input.expected.out +++ b/tests/lean/interactive/num2.input.expected.out @@ -7,7 +7,6 @@ pos_num.size|pos_num → pos_num pos_num.bit0|pos_num → pos_num pos_num.is_inhabited|inhabited pos_num pos_num.is_one|pos_num → bool -pos_num.inc|pos_num → pos_num pos_num.ibelow|pos_num → Prop pos_num.binduction_on|Π (n : pos_num), (Π (n : pos_num), pos_num.ibelow n → ?C n) → ?C n pos_num.induction_on|Π (n : pos_num), ?C pos_num.one → (Π (a : pos_num), ?C a → ?C (pos_num.bit1 a)) → (Π (a : pos_num), ?C a → ?C (pos_num.bit0 a)) → ?C n @@ -20,7 +19,6 @@ pos_num.cases_on|Π (n : pos_num), ?C pos_num.one → (Π (a : pos_num), ?C (pos pos_num.pred|pos_num → pos_num pos_num.mul|pos_num → pos_num → pos_num pos_num.no_confusion_type|Type → pos_num → pos_num → Type -pos_num.num_bits|pos_num → pos_num pos_num.no_confusion|eq ?v1 ?v2 → pos_num.no_confusion_type ?P ?v1 ?v2 pos_num.rec_on|Π (n : pos_num), ?C pos_num.one → (Π (a : pos_num), ?C a → ?C (pos_num.bit1 a)) → (Π (a : pos_num), ?C a → ?C (pos_num.bit0 a)) → ?C n pos_num.brec_on|Π (n : pos_num), (Π (n : pos_num), pos_num.below n → ?C n) → ?C n @@ -36,7 +34,6 @@ pos_num.size|pos_num → pos_num pos_num.bit0|pos_num → pos_num pos_num.is_inhabited|inhabited pos_num pos_num.is_one|pos_num → bool -pos_num.inc|pos_num → pos_num pos_num.ibelow|pos_num → Prop pos_num.binduction_on|Π (n : pos_num), (Π (n : pos_num), pos_num.ibelow n → ?C n) → ?C n pos_num.induction_on|Π (n : pos_num), ?C pos_num.one → (Π (a : pos_num), ?C a → ?C (pos_num.bit1 a)) → (Π (a : pos_num), ?C a → ?C (pos_num.bit0 a)) → ?C n @@ -60,7 +57,6 @@ pos_num.size|pos_num → pos_num pos_num.bit0|pos_num → pos_num pos_num.is_inhabited|inhabited pos_num pos_num.is_one|pos_num → bool -pos_num.inc|pos_num → pos_num pos_num.ibelow|pos_num → Prop pos_num.binduction_on|Π (n : pos_num), (Π (n : pos_num), pos_num.ibelow n → ?C n) → ?C n pos_num.induction_on|Π (n : pos_num), ?C pos_num.one → (Π (a : pos_num), ?C a → ?C (pos_num.bit1 a)) → (Π (a : pos_num), ?C a → ?C (pos_num.bit0 a)) → ?C n diff --git a/tests/lean/protected_test.lean b/tests/lean/protected_test.lean new file mode 100644 index 000000000..d97d0363b --- /dev/null +++ b/tests/lean/protected_test.lean @@ -0,0 +1,11 @@ +namespace nat + check induction_on -- ERROR + check rec_on -- ERROR + check nat.induction_on + check lt.rec_on -- OK + check nat.lt.rec_on + namespace lt + check rec_on -- ERROR + check lt.rec_on + end lt +end nat diff --git a/tests/lean/protected_test.lean.expected.out b/tests/lean/protected_test.lean.expected.out new file mode 100644 index 000000000..fdab38648 --- /dev/null +++ b/tests/lean/protected_test.lean.expected.out @@ -0,0 +1,7 @@ +protected_test.lean:2:8: error: unknown identifier 'induction_on' +protected_test.lean:3:8: error: unknown identifier 'rec_on' +nat.induction_on : ∀ (n : ℕ), ?C 0 → (∀ (a : ℕ), ?C a → ?C (succ a)) → ?C n +lt.rec_on : ?a < ?a_1 → ?C (succ ?a) → (∀ {b : ℕ}, ?a < b → ?C b → ?C (succ b)) → ?C ?a_1 +lt.rec_on : ?a < ?a_1 → ?C (succ ?a) → (∀ {b : ℕ}, ?a < b → ?C b → ?C (succ b)) → ?C ?a_1 +protected_test.lean:8:10: error: unknown identifier 'rec_on' +lt.rec_on : ?a < ?a_1 → ?C (succ ?a) → (∀ {b : ℕ}, ?a < b → ?C b → ?C (succ b)) → ?C ?a_1 diff --git a/tests/lean/run/class_bug1.lean b/tests/lean/run/class_bug1.lean index 4f1755ab3..d085d603e 100644 --- a/tests/lean/run/class_bug1.lean +++ b/tests/lean/run/class_bug1.lean @@ -18,8 +18,8 @@ context sec_cat attribute foo [class] parameters {ob : Type} {mor : ob → ob → Type} {Cat : category ob mor} - definition compose := rec (λ comp id assoc idr idl, comp) Cat - definition id := rec (λ comp id assoc idr idl, id) Cat + definition compose := category.rec (λ comp id assoc idr idl, comp) Cat + definition id := category.rec (λ comp id assoc idr idl, id) Cat infixr ∘ := compose inductive is_section {A B : ob} (f : mor A B) : Type := mk : ∀g, g ∘ f = id → is_section f diff --git a/tests/lean/run/class_bug2.lean b/tests/lean/run/class_bug2.lean index 247e40a97..7eee3a4c3 100644 --- a/tests/lean/run/class_bug2.lean +++ b/tests/lean/run/class_bug2.lean @@ -18,8 +18,8 @@ section sec_cat attribute foo [class] variables {ob : Type} {mor : ob → ob → Type} {Cat : category ob mor} - definition compose := rec (λ comp id assoc idr idl, comp) Cat - definition id := rec (λ comp id assoc idr idl, id) Cat + definition compose := category.rec (λ comp id assoc idr idl, comp) Cat + definition id := category.rec (λ comp id assoc idr idl, id) Cat infixr ∘ := compose end sec_cat end category diff --git a/tests/lean/run/div2.lean b/tests/lean/run/div2.lean index 014d24531..7e20d825e 100644 --- a/tests/lean/run/div2.lean +++ b/tests/lean/run/div2.lean @@ -44,7 +44,7 @@ if_neg H definition rec_measure_aux {dom codom : Type} (default : codom) (measure : dom → ℕ) (rec_val : dom → (dom → codom) → codom) : ℕ → dom → codom := -rec (λx, default) (λm g x, if measure x < succ m then rec_val x g else default) +nat.rec (λx, default) (λm g x, if measure x < succ m then rec_val x g else default) definition rec_measure {dom codom : Type} (default : codom) (measure : dom → ℕ) (rec_val : dom → (dom → codom) → codom) (x : dom) : codom := @@ -62,7 +62,7 @@ theorem rec_measure_aux_spec {dom codom : Type} (default : codom) (measure : dom ∀x, f' m x = restrict default measure f m x := let f' := rec_measure_aux default measure rec_val in let f := rec_measure default measure rec_val in -case_strong_induction_on m +nat.case_strong_induction_on m (take x, have H1 : f' 0 x = default, from rfl, have H2 : ¬ measure x < 0, from !not_lt_zero, diff --git a/tests/lean/run/enum.lean b/tests/lean/run/enum.lean index 06c8b4476..306a4d7f7 100644 --- a/tests/lean/run/enum.lean +++ b/tests/lean/run/enum.lean @@ -8,9 +8,9 @@ two : Three namespace Three theorem disj (a : Three) : a = zero ∨ a = one ∨ a = two := - rec (or.inl rfl) (or.inr (or.inl rfl)) (or.inr (or.inr rfl)) a + Three.rec (or.inl rfl) (or.inr (or.inl rfl)) (or.inr (or.inr rfl)) a example (a : Three) : a ≠ zero → a ≠ one → a = two := - rec (λ h₁ h₂, absurd rfl h₁) (λ h₁ h₂, absurd rfl h₂) (λ h₁ h₂, rfl) a + Three.rec (λ h₁ h₂, absurd rfl h₁) (λ h₁ h₂, absurd rfl h₂) (λ h₁ h₂, rfl) a end Three diff --git a/tests/lean/run/example1.lean b/tests/lean/run/example1.lean index 52a75a207..4ff3cb4db 100644 --- a/tests/lean/run/example1.lean +++ b/tests/lean/run/example1.lean @@ -6,7 +6,7 @@ monday, tuesday, wednesday, thursday, friday, saturday, sunday namespace day definition next_weekday d := - rec_on d tuesday wednesday thursday friday monday monday monday + day.rec_on d tuesday wednesday thursday friday monday monday monday example : next_weekday (next_weekday saturday) = tuesday := rfl diff --git a/tests/lean/run/fib_brec.lean b/tests/lean/run/fib_brec.lean index 2f2462c71..2ccf338e9 100644 --- a/tests/lean/run/fib_brec.lean +++ b/tests/lean/run/fib_brec.lean @@ -3,12 +3,12 @@ open prod namespace nat namespace manual - definition brec_on {C : nat → Type} (n : nat) (F : Π (n : nat), @below C n → C n) : C n := - have general : C n × @below C n, from - rec_on n + definition brec_on {C : nat → Type} (n : nat) (F : Π (n : nat), @nat.below C n → C n) : C n := + have general : C n × @nat.below C n, from + nat.rec_on n (pair (F zero unit.star) unit.star) - (λ (n₁ : nat) (r₁ : C n₁ × @below C n₁), - have b : @below C (succ n₁), from + (λ (n₁ : nat) (r₁ : C n₁ × @nat.below C n₁), + have b : @nat.below C (succ n₁), from r₁, have c : C (succ n₁), from F (succ n₁) b, @@ -17,12 +17,12 @@ namespace nat end manual definition fib (n : nat) := - brec_on n (λ (n : nat), - cases_on n - (λ (b₀ : below zero), succ zero) - (λ (n₁ : nat), cases_on n₁ - (λ b₁ : below (succ zero), succ zero) - (λ (n₂ : nat) (b₂ : below (succ (succ n₂))), pr₁ b₂ + pr₁ (pr₂ b₂)))) + nat.brec_on n (λ (n : nat), + nat.cases_on n + (λ (b₀ : nat.below zero), succ zero) + (λ (n₁ : nat), nat.cases_on n₁ + (λ b₁ : nat.below (succ zero), succ zero) + (λ (n₂ : nat) (b₂ : nat.below (succ (succ n₂))), pr₁ b₂ + pr₁ (pr₂ b₂)))) theorem fib_0 : fib 0 = 1 := rfl diff --git a/tests/lean/run/ftree_brec.lean b/tests/lean/run/ftree_brec.lean index 6cb01353b..69f9f28c1 100644 --- a/tests/lean/run/ftree_brec.lean +++ b/tests/lean/run/ftree_brec.lean @@ -12,7 +12,7 @@ namespace ftree namespace manual definition below.{l l₁ l₂} {A : Type.{l₁}} {B : Type.{l₂}} (C : ftree A B → Type.{l+1}) (t : ftree A B) : Type.{max l₁ l₂ (l+1)} := -@rec.{(max l₁ l₂ (l+1))+1 l₁ l₂} +@ftree.rec.{(max l₁ l₂ (l+1))+1 l₁ l₂} A B (λ t : ftree A B, Type.{max l₁ l₂ (l+1)}) @@ -32,7 +32,7 @@ definition below.{l l₁ l₂} {A : Type.{l₁}} {B : Type.{l₂}} (C : ftree A definition pbelow.{l₁ l₂} {A : Type.{l₁}} {B : Type.{l₂}} (C : ftree A B → Prop) (t : ftree A B) : Prop := -@rec.{1 l₁ l₂} +@ftree.rec.{1 l₁ l₂} A B (λ t : ftree A B, Prop) @@ -55,7 +55,7 @@ definition brec_on.{l l₁ l₂} {A : Type.{l₁}} {B : Type.{l₂}} {C : ftree (F : Π (t : ftree A B), @below A B C t → C t) : C t := have gen : prod.{(l+1) (max l₁ l₂ (l+1))} (C t) (@below A B C t), from - @rec.{(max l₁ l₂ (l+1)) l₁ l₂} + @ftree.rec.{(max l₁ l₂ (l+1)) l₁ l₂} A B (λ t : ftree A B, prod.{(l+1) (max l₁ l₂ (l+1))} (C t) (@below A B C t)) @@ -82,27 +82,27 @@ prod.pr1 gen definition binduction_on.{l₁ l₂} {A : Type.{l₁}} {B : Type.{l₂}} {C : ftree A B → Prop} (t : ftree A B) - (F : Π (t : ftree A B), @ibelow A B C t → C t) + (F : Π (t : ftree A B), @ftree.ibelow A B C t → C t) : C t := -have gen : C t ∧ @ibelow A B C t, from - @rec.{0 l₁ l₂} +have gen : C t ∧ @ftree.ibelow A B C t, from + @ftree.rec.{0 l₁ l₂} A B - (λ t : ftree A B, C t ∧ @ibelow A B C t) - (have b : @ibelow A B C (leafa A B), from + (λ t : ftree A B, C t ∧ @ftree.ibelow A B C t) + (have b : @ftree.ibelow A B C (leafa A B), from true.intro, have c : C (leafa A B), from F (leafa A B) b, and.intro c b) (λ (f₁ : A → B → ftree A B) (f₂ : B → ftree A B) - (r₁ : ∀ (a : A) (b : B), C (f₁ a b) ∧ @ibelow A B C (f₁ a b)) - (r₂ : ∀ (b : B), C (f₂ b) ∧ @ibelow A B C (f₂ b)), + (r₁ : ∀ (a : A) (b : B), C (f₁ a b) ∧ @ftree.ibelow A B C (f₁ a b)) + (r₂ : ∀ (b : B), C (f₂ b) ∧ @ftree.ibelow A B C (f₂ b)), let fc₁ : ∀ (a : A) (b : B), C (f₁ a b) := λ (a : A) (b : B), and.elim_left (r₁ a b) in - let fr₁ : ∀ (a : A) (b : B), @ibelow A B C (f₁ a b) := λ (a : A) (b : B), and.elim_right (r₁ a b) in + let fr₁ : ∀ (a : A) (b : B), @ftree.ibelow A B C (f₁ a b) := λ (a : A) (b : B), and.elim_right (r₁ a b) in let fc₂ : ∀ (b : B), C (f₂ b) := λ (b : B), and.elim_left (r₂ b) in - let fr₂ : ∀ (b : B), @ibelow A B C (f₂ b) := λ (b : B), and.elim_right (r₂ b) in - have b : @ibelow A B C (node f₁ f₂), from + let fr₂ : ∀ (b : B), @ftree.ibelow A B C (f₂ b) := λ (b : B), and.elim_right (r₂ b) in + have b : @ftree.ibelow A B C (node f₁ f₂), from and.intro (and.intro fc₁ fr₁) (and.intro fc₂ fr₂), have c : C (node f₁ f₂), from F (node f₁ f₂) b, diff --git a/tests/lean/run/inf_tree.lean b/tests/lean/run/inf_tree.lean index 2f5d341cb..8cc310f55 100644 --- a/tests/lean/run/inf_tree.lean +++ b/tests/lean/run/inf_tree.lean @@ -24,7 +24,7 @@ namespace inftree definition dsub.wf (A : Type) : well_founded (@dsub A) := well_founded.intro (λ (t : inftree A), - rec_on t + inftree.rec_on t (λ a, dsub.leaf.acc a) (λ f (ih :∀a, acc dsub (f a)), dsub.node.acc f ih)) diff --git a/tests/lean/run/inf_tree2.lean b/tests/lean/run/inf_tree2.lean index 11636a5bd..dab0f1f0f 100644 --- a/tests/lean/run/inf_tree2.lean +++ b/tests/lean/run/inf_tree2.lean @@ -21,7 +21,7 @@ namespace inftree definition dsub.wf (A : Type) : well_founded (@dsub A) := well_founded.intro (λ (t : inftree A), - rec_on t + inftree.rec_on t (λ a, dsub.leaf.acc a) (λ f t (ihf :∀a, acc dsub (f a)) (iht : acc dsub t), dsub.node.acc f ihf t iht)) diff --git a/tests/lean/run/lift.lean b/tests/lean/run/lift.lean index fb38cf488..9932cc478 100644 --- a/tests/lean/run/lift.lean +++ b/tests/lean/run/lift.lean @@ -6,14 +6,14 @@ up : A → lift A namespace lift definition down {A : Type} (a : lift A) : A := -rec (λ a, a) a +lift.rec (λ a, a) a theorem down_up {A : Type} (a : A) : down (up a) = a := rfl theorem up_down {A : Type} (a' : lift A) : up (down a') = a' := -induction_on a' (λ a, rfl) +lift.induction_on a' (λ a, rfl) end lift diff --git a/tests/lean/run/nat_bug.lean b/tests/lean/run/nat_bug.lean index 4fc773f97..16cfd6a95 100644 --- a/tests/lean/run/nat_bug.lean +++ b/tests/lean/run/nat_bug.lean @@ -13,13 +13,13 @@ theorem pred_zero : pred zero = zero := refl _ theorem pred_succ (n : nat) : pred (succ n) = n := refl _ theorem zero_or_succ (n : nat) : n = zero ∨ n = succ (pred n) -:= induction_on n +:= nat.induction_on n (or.intro_left _ (refl zero)) (take m IH, or.intro_right _ (show succ m = succ (pred (succ m)), from congr_arg succ (symm (pred_succ m)))) theorem zero_or_succ2 (n : nat) : n = zero ∨ n = succ (pred n) -:= @induction_on _ n +:= @nat.induction_on _ n (or.intro_left _ (refl zero)) (take m IH, or.intro_right _ (show succ m = succ (pred (succ m)), from congr_arg succ (symm (pred_succ m)))) diff --git a/tests/lean/run/nat_bug5.lean b/tests/lean/run/nat_bug5.lean index f5895d4f0..d40536216 100644 --- a/tests/lean/run/nat_bug5.lean +++ b/tests/lean/run/nat_bug5.lean @@ -19,7 +19,7 @@ axiom add_assoc (n m k : nat) : (n + m) + k = n + (m + k) axiom add_right_comm (n m k : nat) : n + m + k = n + k + m set_option unifier.max_steps 50000 theorem mul_add_distr_left (n m k : nat) : (n + m) * k = n * k + m * k -:= induction_on k +:= nat.induction_on k (calc (n + m) * zero = zero : eq.refl _ ... = n * zero + m * zero : eq.refl _) diff --git a/tests/lean/run/nested_begin.lean b/tests/lean/run/nested_begin.lean index 0e352e569..7765f7ef8 100644 --- a/tests/lean/run/nested_begin.lean +++ b/tests/lean/run/nested_begin.lean @@ -6,14 +6,14 @@ vnil : vector A zero, vcons : Π {n : nat}, A → vector A n → vector A (succ n) namespace vector - definition no_confusion2 {A : Type} {n : nat} {P : Type} {v₁ v₂ : vector A n} : v₁ = v₂ → no_confusion_type P v₁ v₂ := + definition no_confusion2 {A : Type} {n : nat} {P : Type} {v₁ v₂ : vector A n} : v₁ = v₂ → vector.no_confusion_type P v₁ v₂ := assume H₁₂ : v₁ = v₂, begin - show no_confusion_type P v₁ v₂, from - have aux : v₁ = v₁ → no_confusion_type P v₁ v₁, from + show vector.no_confusion_type P v₁ v₂, from + have aux : v₁ = v₁ → vector.no_confusion_type P v₁ v₁, from take H₁₁, begin - apply (cases_on v₁), + apply (vector.cases_on v₁), exact (assume h : P, h), intros (n, a, v, h), @@ -26,11 +26,11 @@ namespace vector theorem vcons.inj₁ {A : Type} {n : nat} (a₁ a₂ : A) (v₁ v₂ : vector A n) : vcons a₁ v₁ = vcons a₂ v₂ → a₁ = a₂ := begin - intro h, apply (no_confusion h), intros, assumption + intro h, apply (vector.no_confusion h), intros, assumption end theorem vcons.inj₂ {A : Type} {n : nat} (a₁ a₂ : A) (v₁ v₂ : vector A n) : vcons a₁ v₁ = vcons a₂ v₂ → v₁ == v₂ := begin - intro h, apply (no_confusion h), intros, eassumption + intro h, apply (vector.no_confusion h), intros, eassumption end end vector diff --git a/tests/lean/run/sigma_no_confusion.lean b/tests/lean/run/sigma_no_confusion.lean index f41b5ca1d..8894e45b0 100644 --- a/tests/lean/run/sigma_no_confusion.lean +++ b/tests/lean/run/sigma_no_confusion.lean @@ -3,15 +3,15 @@ import data.sigma namespace sigma namespace manual definition no_confusion_type {A : Type} {B : A → Type} (P : Type) (v₁ v₂ : sigma B) : Type := - rec_on v₁ - (λ (a₁ : A) (b₁ : B a₁), rec_on v₂ + sigma.rec_on v₁ + (λ (a₁ : A) (b₁ : B a₁), sigma.rec_on v₂ (λ (a₂ : A) (b₂ : B a₂), (Π (eq₁ : a₁ = a₂), eq.rec_on eq₁ b₁ = b₂ → P) → P)) definition no_confusion {A : Type} {B : A → Type} {P : Type} {v₁ v₂ : sigma B} : v₁ = v₂ → no_confusion_type P v₁ v₂ := assume H₁₂ : v₁ = v₂, have aux : v₁ = v₁ → no_confusion_type P v₁ v₁, from - assume H₁₁, rec_on v₁ + assume H₁₁, sigma.rec_on v₁ (λ (a₁ : A) (b₁ : B a₁) (h : Π (eq₁ : a₁ = a₁), eq.rec_on eq₁ b₁ = b₁ → P), h rfl rfl), eq.rec_on H₁₂ aux H₁₂ @@ -19,11 +19,11 @@ namespace sigma theorem sigma.mk.inj_1 {A : Type} {B : A → Type} {a₁ a₂ : A} {b₁ : B a₁} {b₂ : B a₂} (Heq : mk a₁ b₁ = mk a₂ b₂) : a₁ = a₂ := begin - apply (no_confusion Heq), intros, assumption + apply (sigma.no_confusion Heq), intros, assumption end theorem sigma.mk.inj_2 {A : Type} {B : A → Type} (a₁ a₂ : A) (b₁ : B a₁) (b₂ : B a₂) (Heq : mk a₁ b₁ = mk a₂ b₂) : b₁ == b₂ := begin - apply (no_confusion Heq), intros, eassumption + apply (sigma.no_confusion Heq), intros, eassumption end end sigma diff --git a/tests/lean/run/sum_bug.lean b/tests/lean/run/sum_bug.lean index 0cecf9d7d..a4735900c 100644 --- a/tests/lean/run/sum_bug.lean +++ b/tests/lean/run/sum_bug.lean @@ -16,19 +16,19 @@ infixr `+` := sum open eq theorem inl_inj {A B : Type} {a1 a2 : A} (H : inl B a1 = inl B a2) : a1 = a2 := -let f := λs, rec_on s (λa, a1 = a) (λb, false) in +let f := λs, sum.rec_on s (λa, a1 = a) (λb, false) in have H1 : f (inl B a1), from rfl, have H2 : f (inl B a2), from subst H H1, H2 theorem inl_neq_inr {A B : Type} {a : A} {b : B} (H : inl B a = inr A b) : false := -let f := λs, rec_on s (λa', a = a') (λb, false) in +let f := λs, sum.rec_on s (λa', a = a') (λb, false) in have H1 : f (inl B a), from rfl, have H2 : f (inr A b), from subst H H1, H2 theorem inr_inj {A B : Type} {b1 b2 : B} (H : inr A b1 = inr A b2) : b1 = b2 := -let f := λs, rec_on s (λa, false) (λb, b1 = b) in +let f := λs, sum.rec_on s (λa, false) (λb, b1 = b) in have H1 : f (inr A b1), from rfl, have H2 : f (inr A b2), from subst H H1, H2 @@ -42,16 +42,16 @@ inhabited.mk (inr A (default B)) theorem sum_eq_decidable [instance] {A B : Type} (s1 s2 : A + B) (H1 : ∀a1 a2 : A, decidable (inl B a1 = inl B a2)) (H2 : ∀b1 b2 : B, decidable (inr A b1 = inr A b2)) : decidable (s1 = s2) := -rec_on s1 +sum.rec_on s1 (take a1, show decidable (inl B a1 = s2), from - rec_on s2 + sum.rec_on s2 (take a2, show decidable (inl B a1 = inl B a2), from H1 a1 a2) (take b2, have H3 : (inl B a1 = inr A b2) ↔ false, from iff.intro inl_neq_inr (assume H4, false.elim H4), show decidable (inl B a1 = inr A b2), from decidable_of_decidable_of_iff _ (iff.symm H3))) (take b1, show decidable (inr A b1 = s2), from - rec_on s2 + sum.rec_on s2 (take a2, have H3 : (inr A b1 = inl B a2) ↔ false, from iff.intro (assume H4, inl_neq_inr (symm H4)) (assume H4, false.elim H4), diff --git a/tests/lean/run/tree.lean b/tests/lean/run/tree.lean index caf4af0cb..f635168aa 100644 --- a/tests/lean/run/tree.lean +++ b/tests/lean/run/tree.lean @@ -17,7 +17,7 @@ namespace manual variable {A : Type.{l₁}} variable (C : tree A → Type.{l₂}) definition below (t : tree A) : Type := - rec_on t (λ a, one.{l₂}) (λ t₁ t₂ r₁ r₂, C t₁ × C t₂ × r₁ × r₂) + tree.rec_on t (λ a, one.{l₂}) (λ t₁ t₂ r₁ r₂, C t₁ × C t₂ × r₁ × r₂) end section @@ -26,7 +26,7 @@ namespace manual variable {C : tree A → Type.{l₂}} definition below_rec_on (t : tree A) (H : Π (n : tree A), below C n → C n) : C t := have general : C t × below C t, from - rec_on t + tree.rec_on t (λa, (H (leaf a) one.star, one.star)) (λ (l r : tree A) (Hl : C l × below C l) (Hr : C r × below C r), have b : below C (node l r), from @@ -41,12 +41,12 @@ end manual universe variables l₁ l₂ variable {A : Type.{l₁}} variable {C : tree A → Type.{l₂+1}} - definition below_rec_on (t : tree A) (H : Π (n : tree A), @below A C n → C n) : C t - := have general : C t × @below A C t, from - rec_on t + definition below_rec_on (t : tree A) (H : Π (n : tree A), @tree.below A C n → C n) : C t + := have general : C t × @tree.below A C t, from + tree.rec_on t (λa, (H (leaf a) unit.star, unit.star)) - (λ (l r : tree A) (Hl : C l × @below A C l) (Hr : C r × @below A C r), - have b : @below A C (node l r), from + (λ (l r : tree A) (Hl : C l × @tree.below A C l) (Hr : C r × @tree.below A C r), + have b : @tree.below A C (node l r), from ((pr₁ Hl, pr₂ Hl), (pr₁ Hr, pr₂ Hr)), have c : C (node l r), from H (node l r) b, @@ -58,5 +58,5 @@ end manual theorem leaf_ne_tree {A : Type} (a : A) (l r : tree A) : leaf a ≠ node l r := assume h : leaf a = node l r, - no_confusion h + tree.no_confusion h end tree diff --git a/tests/lean/run/tree2.lean b/tests/lean/run/tree2.lean index 7d1a6841e..15da3feb0 100644 --- a/tests/lean/run/tree2.lean +++ b/tests/lean/run/tree2.lean @@ -17,7 +17,7 @@ namespace tree variable {A : Type.{l₁}} variable (C : tree A → Type.{l₂}) definition below (t : tree A) : Type := - rec_on t (λ a, one.{l₂}) (λ t₁ t₂ r₁ r₂, C t₁ × C t₂ × r₁ × r₂) + tree.rec_on t (λ a, one.{l₂}) (λ t₁ t₂ r₁ r₂, C t₁ × C t₂ × r₁ × r₂) end section @@ -26,7 +26,7 @@ namespace tree variable {C : tree A → Type.{l₂}} definition below_rec_on (t : tree A) (H : Π (n : tree A), below C n → C n) : C t := have general : C t × below C t, from - rec_on t + tree.rec_on t (λa, (H (leaf a) one.star, one.star)) (λ (l r : tree A) (Hl : C l × below C l) (Hr : C r × below C r), have b : below C (node l r), from @@ -38,29 +38,29 @@ namespace tree end end manual - check no_confusion + check tree.no_confusion theorem leaf_ne_tree {A : Type} (a : A) (l r : tree A) : leaf a ≠ node l r := assume h : leaf a = node l r, - no_confusion h + tree.no_confusion h constant A : Type₁ constants l₁ l₂ r₁ r₂ : tree A axiom node_eq : node l₁ r₁ = node l₂ r₂ - check no_confusion node_eq + check tree.no_confusion node_eq - definition tst : (l₁ = l₂ → r₁ = r₂ → l₁ = l₂) → l₁ = l₂ := no_confusion node_eq + definition tst : (l₁ = l₂ → r₁ = r₂ → l₁ = l₂) → l₁ = l₂ := tree.no_confusion node_eq check tst (λ e₁ e₂, e₁) theorem node.inj1 {A : Type} (l₁ l₂ r₁ r₂ : tree A) : node l₁ r₁ = node l₂ r₂ → l₁ = l₂ := assume h, - have trivial : (l₁ = l₂ → r₁ = r₂ → l₁ = l₂) → l₁ = l₂, from no_confusion h, + have trivial : (l₁ = l₂ → r₁ = r₂ → l₁ = l₂) → l₁ = l₂, from tree.no_confusion h, trivial (λ e₁ e₂, e₁) theorem node.inj2 {A : Type} (l₁ l₂ r₁ r₂ : tree A) : node l₁ r₁ = node l₂ r₂ → l₁ = l₂ := begin intro h, - apply (no_confusion h), + apply (tree.no_confusion h), intros, assumption end end tree diff --git a/tests/lean/run/tree3.lean b/tests/lean/run/tree3.lean index 2d90f878d..b2a3028f1 100644 --- a/tests/lean/run/tree3.lean +++ b/tests/lean/run/tree3.lean @@ -17,7 +17,7 @@ namespace tree variable {A : Type.{l₁}} variable (C : tree A → Type.{l₂}) definition below (t : tree A) : Type := - rec_on t (λ a, one.{l₂}) (λ t₁ t₂ r₁ r₂, C t₁ × C t₂ × r₁ × r₂) + tree.rec_on t (λ a, one.{l₂}) (λ t₁ t₂ r₁ r₂, C t₁ × C t₂ × r₁ × r₂) end section @@ -26,7 +26,7 @@ namespace tree variable {C : tree A → Type.{l₂}} definition below_rec_on (t : tree A) (H : Π (n : tree A), below C n → C n) : C t := have general : C t × below C t, from - rec_on t + tree.rec_on t (λa, (H (leaf a) one.star, one.star)) (λ (l r : tree A) (Hl : C l × below C l) (Hr : C r × below C r), have b : below C (node l r), from @@ -37,7 +37,7 @@ namespace tree pr₁ general end end manual - + local abbreviation no_confusion := @tree.no_confusion check no_confusion theorem leaf_ne_tree {A : Type} (a : A) (l r : tree A) : leaf a ≠ node l r := diff --git a/tests/lean/run/tree_height.lean b/tests/lean/run/tree_height.lean index 1393abf0f..bb66b851c 100644 --- a/tests/lean/run/tree_height.lean +++ b/tests/lean/run/tree_height.lean @@ -8,7 +8,7 @@ node : tree A → tree A → tree A namespace tree definition height {A : Type} (t : tree A) : nat := -rec_on t +tree.rec_on t (λ a, zero) (λ t₁ t₂ h₁ h₂, succ (max h₁ h₂)) diff --git a/tests/lean/run/univ_problem.lean b/tests/lean/run/univ_problem.lean index 08d91e52b..b5eae2982 100644 --- a/tests/lean/run/univ_problem.lean +++ b/tests/lean/run/univ_problem.lean @@ -6,7 +6,7 @@ vnil {} : vector A zero, vcons : Π {n : nat}, A → vector A n → vector A (succ n) namespace vector - print definition no_confusion + print definition vector.no_confusion infixr `::` := vcons namespace play @@ -14,12 +14,12 @@ namespace vector universe variables l₁ l₂ variable {A : Type.{l₁}} variable {C : Π (n : nat), vector A n → Type.{l₂+1}} - definition brec_on {n : nat} (v : vector A n) (H : Π (n : nat) (v : vector A n), @below A C n v → C n v) : C n v := - have general : C n v × @below A C n v, from - rec_on v + definition brec_on {n : nat} (v : vector A n) (H : Π (n : nat) (v : vector A n), @vector.below A C n v → C n v) : C n v := + have general : C n v × @vector.below A C n v, from + vector.rec_on v (pair (H zero vnil unit.star) unit.star) - (λ (n₁ : nat) (a₁ : A) (v₁ : vector A n₁) (r₁ : C n₁ v₁ × @below A C n₁ v₁), - have b : @below A C _ (vcons a₁ v₁), from + (λ (n₁ : nat) (a₁ : A) (v₁ : vector A n₁) (r₁ : C n₁ v₁ × @vector.below A C n₁ v₁), + have b : @vector.below A C _ (vcons a₁ v₁), from r₁, have c : C (succ n₁) (vcons a₁ v₁), from H (succ n₁) (vcons a₁ v₁) b, @@ -30,19 +30,19 @@ namespace vector print "=====================" definition append {A : Type} {n m : nat} (w : vector A m) (v : vector A n) : vector A (n + m) := - brec_on w (λ (n : nat) (w : vector A n), - cases_on w - (λ (B : below vnil), v) - (λ (n₁ : nat) (a₁ : A) (v₁ : vector A n₁) (B : below (vcons a₁ v₁)), + vector.brec_on w (λ (n : nat) (w : vector A n), + vector.cases_on w + (λ (B : vector.below vnil), v) + (λ (n₁ : nat) (a₁ : A) (v₁ : vector A n₁) (B : vector.below (vcons a₁ v₁)), vcons a₁ (pr₁ B))) exit - check brec_on - definition bw := @below + check vector.brec_on + definition bw := @vector.below definition sum {n : nat} (v : vector nat n) : nat := - brec_on v (λ (n : nat) (v : vector nat n), - cases_on v + vector.brec_on v (λ (n : nat) (v : vector nat n), + vector.cases_on v (λ (B : bw vnil), zero) (λ (n₁ : nat) (a : nat) (v₁ : vector nat n₁) (B : bw (vcons a v₁)), a + pr₁ B)) @@ -51,8 +51,8 @@ namespace vector rfl definition addk {n : nat} (v : vector nat n) (k : nat) : vector nat n := - brec_on v (λ (n : nat) (v : vector nat n), - cases_on v + vector.brec_on v (λ (n : nat) (v : vector nat n), + vector.cases_on v (λ (B : bw vnil), vnil) (λ (n₁ : nat) (a₁ : nat) (v₁ : vector nat n₁) (B : bw (vcons a₁ v₁)), vcons (a₁+k) (pr₁ B))) @@ -64,22 +64,22 @@ namespace vector rfl definition head {A : Type} {n : nat} (v : vector A (succ n)) : A := - cases_on v + nat.cases_on v (λ H : succ n = 0, nat.no_confusion H) (λn' h t (H : succ n = succ n'), h) rfl definition tail {A : Type} {n : nat} (v : vector A (succ n)) : vector A n := - @cases_on A (λn' v, succ n = n' → vector A (pred n')) (succ n) v + @nat.cases_on A (λn' v, succ n = n' → vector A (pred n')) (succ n) v (λ H : succ n = 0, nat.no_confusion H) (λ (n' : nat) (h : A) (t : vector A n') (H : succ n = succ n'), t) rfl definition add {n : nat} (w v : vector nat n) : vector nat n := - @brec_on nat (λ (n : nat) (v : vector nat n), vector nat n → vector nat n) n w + @nat.brec_on nat (λ (n : nat) (v : vector nat n), vector nat n → vector nat n) n w (λ (n : nat) (w : vector nat n), - cases_on w + vector.cases_on w (λ (B : bw vnil) (w : vector nat zero), vnil) (λ (n₁ : nat) (a₁ : nat) (v₁ : vector nat n₁) (B : bw (vcons a₁ v₁)) (v : vector nat (succ n₁)), vcons (a₁ + head v) (pr₁ B (tail v)))) v diff --git a/tests/lean/run/vector.lean b/tests/lean/run/vector.lean index 5b381f9ce..7689c6649 100644 --- a/tests/lean/run/vector.lean +++ b/tests/lean/run/vector.lean @@ -9,6 +9,9 @@ namespace vector -- print definition no_confusion infixr `::` := vcons + local abbreviation no_confusion := @vector.no_confusion + local abbreviation below := @vector.below + theorem vcons.inj₁ {A : Type} {n : nat} (a₁ a₂ : A) (v₁ v₂ : vector A n) : vcons a₁ v₁ = vcons a₂ v₂ → a₁ = a₂ := begin intro h, apply (no_confusion h), intros, assumption @@ -27,12 +30,12 @@ namespace vector universe variables l₁ l₂ variable {A : Type.{l₁}} variable {C : Π (n : nat), vector A n → Type.{l₂}} - definition brec_on {n : nat} (v : vector A n) (H : Π (n : nat) (v : vector A n), @below A C n v → C n v) : C n v := - have general : C n v × @below A C n v, from - rec_on v + definition brec_on {n : nat} (v : vector A n) (H : Π (n : nat) (v : vector A n), @vector.below A C n v → C n v) : C n v := + have general : C n v × @vector.below A C n v, from + vector.rec_on v (pair (H zero vnil unit.star) unit.star) - (λ (n₁ : nat) (a₁ : A) (v₁ : vector A n₁) (r₁ : C n₁ v₁ × @below A C n₁ v₁), - have b : @below A C _ (vcons a₁ v₁), from + (λ (n₁ : nat) (a₁ : A) (v₁ : vector A n₁) (r₁ : C n₁ v₁ × @vector.below A C n₁ v₁), + have b : @vector.below A C _ (vcons a₁ v₁), from r₁, have c : C (succ n₁) (vcons a₁ v₁), from H (succ n₁) (vcons a₁ v₁) b, @@ -41,13 +44,13 @@ namespace vector end end manual - -- check brec_on + -- check vector.brec_on definition bw := @below definition sum {n : nat} (v : vector nat n) : nat := - brec_on v (λ (n : nat) (v : vector nat n), - cases_on v + vector.brec_on v (λ (n : nat) (v : vector nat n), + vector.cases_on v (λ (B : bw vnil), zero) (λ (n₁ : nat) (a : nat) (v₁ : vector nat n₁) (B : bw (vcons a v₁)), a + pr₁ B)) @@ -56,8 +59,8 @@ namespace vector rfl definition addk {n : nat} (v : vector nat n) (k : nat) : vector nat n := - brec_on v (λ (n : nat) (v : vector nat n), - cases_on v + vector.brec_on v (λ (n : nat) (v : vector nat n), + vector.cases_on v (λ (B : bw vnil), vnil) (λ (n₁ : nat) (a₁ : nat) (v₁ : vector nat n₁) (B : bw (vcons a₁ v₁)), vcons (a₁+k) (pr₁ B))) @@ -66,8 +69,8 @@ namespace vector rfl definition append.{l} {A : Type.{l+1}} {n m : nat} (w : vector A m) (v : vector A n) : vector A (n + m) := - brec_on w (λ (n : nat) (w : vector A n), - cases_on w + vector.brec_on w (λ (n : nat) (w : vector A n), + vector.cases_on w (λ (B : bw vnil), v) (λ (n₁ : nat) (a₁ : A) (v₁ : vector A n₁) (B : bw (vcons a₁ v₁)), vcons a₁ (pr₁ B))) @@ -76,22 +79,22 @@ namespace vector rfl definition head {A : Type} {n : nat} (v : vector A (succ n)) : A := - cases_on v + vector.cases_on v (λ H : succ n = 0, nat.no_confusion H) (λn' h t (H : succ n = succ n'), h) rfl definition tail {A : Type} {n : nat} (v : vector A (succ n)) : vector A n := - @cases_on A (λn' v, succ n = n' → vector A (pred n')) (succ n) v + @vector.cases_on A (λn' v, succ n = n' → vector A (pred n')) (succ n) v (λ H : succ n = 0, nat.no_confusion H) (λ (n' : nat) (h : A) (t : vector A n') (H : succ n = succ n'), t) rfl definition add {n : nat} (w v : vector nat n) : vector nat n := - @brec_on nat (λ (n : nat) (v : vector nat n), vector nat n → vector nat n) n w + @vector.brec_on nat (λ (n : nat) (v : vector nat n), vector nat n → vector nat n) n w (λ (n : nat) (w : vector nat n), - cases_on w + vector.cases_on w (λ (B : bw vnil) (w : vector nat zero), vnil) (λ (n₁ : nat) (a₁ : nat) (v₁ : vector nat n₁) (B : bw (vcons a₁ v₁)) (v : vector nat (succ n₁)), vcons (a₁ + head v) (pr₁ B (tail v)))) v @@ -101,7 +104,7 @@ namespace vector definition map {A B C : Type} {n : nat} (f : A → B → C) (w : vector A n) (v : vector B n) : vector C n := let P := λ (n : nat) (v : vector A n), vector B n → vector C n in - @brec_on A P n w + @vector.brec_on A P n w (λ (n : nat) (w : vector A n), begin cases w with (n₁, h₁, t₁), diff --git a/tests/lean/run/vector2.lean b/tests/lean/run/vector2.lean index 287e9c0cc..32a9b49e4 100644 --- a/tests/lean/run/vector2.lean +++ b/tests/lean/run/vector2.lean @@ -7,6 +7,6 @@ vcons : Π {n : nat}, A → vector A n → vector A (succ n) namespace vector theorem vcons.inj₁ {A : Type} {n : nat} (a₁ a₂ : A) (v₁ v₂ : vector A n) : vcons a₁ v₁ = vcons a₂ v₂ → a₁ = a₂ := - assume h, no_confusion h (λ n h t, h) + assume h, vector.no_confusion h (λ n h t, h) end vector diff --git a/tests/lean/run/vector3.lean b/tests/lean/run/vector3.lean index 21b6b0124..6ffa45c6c 100644 --- a/tests/lean/run/vector3.lean +++ b/tests/lean/run/vector3.lean @@ -7,8 +7,8 @@ vcons : Π {n : nat}, A → vector A n → vector A (succ n) namespace vector theorem vcons.inj₁ {A : Type} {n : nat} (a₁ a₂ : A) (v₁ v₂ : vector A n) : vcons a₁ v₁ = vcons a₂ v₂ → a₁ = a₂ := - assume h, no_confusion h (λ n h t, h) + assume h, vector.no_confusion h (λ n h t, h) theorem vcons.inj₂ {A : Type} {n : nat} (a₁ a₂ : A) (v₁ v₂ : vector A n) : vcons a₁ v₁ = vcons a₂ v₂ → v₁ == v₂ := - assume h, no_confusion h (λ n h t, t) + assume h, vector.no_confusion h (λ n h t, t) end vector diff --git a/tests/lean/slow/nat_bug2.lean b/tests/lean/slow/nat_bug2.lean index 5a993dcdd..f12bbcc76 100644 --- a/tests/lean/slow/nat_bug2.lean +++ b/tests/lean/slow/nat_bug2.lean @@ -54,7 +54,7 @@ theorem pred_zero : pred 0 = 0 theorem pred_succ (n : ℕ) : pred (succ n) = n theorem zero_or_succ (n : ℕ) : n = 0 ∨ n = succ (pred n) -:= induction_on n +:= nat.induction_on n (or.intro_left _ (refl 0)) (take m IH, or.intro_right _ (show succ m = succ (pred (succ m)), from congr_arg succ ((pred_succ m)⁻¹))) @@ -63,7 +63,7 @@ theorem zero_or_succ2 (n : ℕ) : n = 0 ∨ ∃k, n = succ k := or_of_or_of_imp_of_imp (zero_or_succ n) (assume H, H) (assume H : n = succ (pred n), exists.intro (pred n) H) theorem case {P : ℕ → Prop} (n : ℕ) (H1: P 0) (H2 : ∀m, P (succ m)) : P n -:= induction_on n H1 (take m IH, H2 m) +:= nat.induction_on n H1 (take m IH, H2 m) theorem discriminate {B : Prop} {n : ℕ} (H1: n = 0 → B) (H2 : ∀m, n = succ m → B) : B := or.elim (zero_or_succ n) @@ -77,7 +77,7 @@ theorem succ_inj {n m : ℕ} (H : succ n = succ m) : n = m ... = m : pred_succ m theorem succ_ne_self (n : ℕ) : succ n ≠ n -:= induction_on n +:= nat.induction_on n (take H : 1 = 0, have ne : 1 ≠ 0, from succ_ne_zero 0, absurd H ne) @@ -85,13 +85,13 @@ theorem succ_ne_self (n : ℕ) : succ n ≠ n theorem decidable_eq [instance] (n m : ℕ) : decidable (n = m) := have general : ∀n, decidable (n = m), from - rec_on m + nat.rec_on m (take n, - rec_on n + nat.rec_on n (inl (refl 0)) (λ m iH, inr (succ_ne_zero m))) (λ (m' : ℕ) (iH1 : ∀n, decidable (n = m')), - take n, rec_on n + take n, nat.rec_on n (inr (ne.symm (succ_ne_zero m'))) (λ (n' : ℕ) (iH2 : decidable (n' = succ m')), have d1 : decidable (n' = m'), from iH1 n', @@ -106,7 +106,7 @@ theorem decidable_eq [instance] (n m : ℕ) : decidable (n = m) theorem two_step_induction_on {P : ℕ → Prop} (a : ℕ) (H1 : P 0) (H2 : P 1) (H3 : ∀ (n : ℕ) (IH1 : P n) (IH2 : P (succ n)), P (succ (succ n))) : P a := have stronger : P a ∧ P (succ a), from - induction_on a + nat.induction_on a (and_intro H1 H2) (take k IH, have IH1 : P k, from and.elim_left IH, @@ -116,7 +116,7 @@ theorem two_step_induction_on {P : ℕ → Prop} (a : ℕ) (H1 : P 0) (H2 : P 1) theorem sub_induction {P : ℕ → ℕ → Prop} (n m : ℕ) (H1 : ∀m, P 0 m) (H2 : ∀n, P (succ n) 0) (H3 : ∀n m, P n m → P (succ n) (succ m)) : P n m -:= have general : ∀m, P n m, from induction_on n +:= have general : ∀m, P n m, from nat.induction_on n (take m : ℕ, H1 m) (take k : ℕ, assume IH : ∀m, P k m, @@ -137,7 +137,7 @@ theorem add_succ (n m : ℕ) : n + succ m = succ (n + m) ---------- comm, assoc theorem zero_add (n : ℕ) : 0 + n = n -:= induction_on n +:= nat.induction_on n (add_zero 0) (take m IH, show 0 + succ m = succ m, from calc @@ -145,7 +145,7 @@ theorem zero_add (n : ℕ) : 0 + n = n ... = succ m : {IH}) theorem succ_add (n m : ℕ) : (succ n) + m = succ (n + m) -:= induction_on m +:= nat.induction_on m (calc succ n + 0 = succ n : add_zero (succ n) ... = succ (n + 0) : {symm (add_zero n)}) @@ -156,7 +156,7 @@ theorem succ_add (n m : ℕ) : (succ n) + m = succ (n + m) ... = succ (n + succ k) : {symm (add_succ _ _)}) theorem add_comm (n m : ℕ) : n + m = m + n -:= induction_on m +:= nat.induction_on m (trans (add_zero _) (symm (zero_add _))) (take k IH, calc @@ -175,7 +175,7 @@ theorem add_comm_succ (n m : ℕ) : n + succ m = m + succ n ... = m + succ n : add_comm (succ n) m theorem add_assoc (n m k : ℕ) : (n + m) + k = n + (m + k) -:= induction_on k +:= nat.induction_on k (calc (n + m) + 0 = n + m : add_zero _ ... = n + (m + 0) : {symm (add_zero m)}) @@ -197,7 +197,7 @@ theorem add_right_comm (n m k : ℕ) : n + m + k = n + k + m theorem add_cancel_left {n m k : ℕ} : n + m = n + k → m = k := - induction_on n + nat.induction_on n (take H : 0 + m = 0 + k, calc m = 0 + m : symm (zero_add m) @@ -224,7 +224,7 @@ theorem add_cancel_right {n m k : ℕ} (H : n + m = k + m) : n = k theorem eq_zero_of_add_eq_zero_right {n m : ℕ} : n + m = 0 → n = 0 := - induction_on n + nat.induction_on n (take (H : 0 + m = 0), refl 0) (take k IH, assume (H : succ k + m = 0), @@ -273,7 +273,7 @@ set_option unifier.max_steps 100000 ---------- comm, distr, assoc, identity theorem mul_zero_left (n:ℕ) : 0 * n = 0 -:= induction_on n +:= nat.induction_on n (mul_zero_right 0) (take m IH, calc @@ -282,7 +282,7 @@ theorem mul_zero_left (n:ℕ) : 0 * n = 0 ... = 0 : IH) theorem mul_succ_left (n m:ℕ) : (succ n) * m = (n * m) + m -:= induction_on m +:= nat.induction_on m (calc succ n * 0 = 0 : mul_zero_right _ ... = n * 0 : symm (mul_zero_right _) @@ -297,7 +297,7 @@ theorem mul_succ_left (n m:ℕ) : (succ n) * m = (n * m) + m ... = (n * succ k) + succ k : {symm (mul_succ_right n k)}) theorem mul_comm (n m:ℕ) : n * m = m * n -:= induction_on m +:= nat.induction_on m (trans (mul_zero_right _) (symm (mul_zero_left _))) (take k IH, calc @@ -306,7 +306,7 @@ theorem mul_comm (n m:ℕ) : n * m = m * n ... = (succ k) * n : symm (mul_succ_left _ _)) theorem mul_add_distr_left (n m k : ℕ) : (n + m) * k = n * k + m * k -:= induction_on k +:= nat.induction_on k (calc (n + m) * 0 = 0 : mul_zero_right _ ... = 0 + 0 : symm (add_zero _) @@ -329,7 +329,7 @@ theorem mul_add_distr_right (n m k : ℕ) : n * (m + k) = n * m + n * k ... = n * m + n * k : {mul_comm _ _} theorem mul_assoc (n m k:ℕ) : (n * m) * k = n * (m * k) -:= induction_on k +:= nat.induction_on k (calc (n * m) * 0 = 0 : mul_zero_right _ ... = n * 0 : symm (mul_zero_right _) @@ -629,7 +629,7 @@ theorem pred_le_imp_le_or_eq {n m : ℕ} (H : pred n ≤ m) : n ≤ m ∨ n = su theorem mul_le_left {n m : ℕ} (H : n ≤ m) (k : ℕ) : k * n ≤ k * m := obtain (l : ℕ) (Hl : n + l = m), from (le_elim H), - induction_on k + nat.induction_on k (have H2 : 0 * n = 0 * m, from calc 0 * n = 0 : mul_zero_left n @@ -779,7 +779,7 @@ theorem succ_lt_right {n m : ℕ} (H : n < m) : n < succ m ---------- totality of lt and le theorem le_or_lt (n m : ℕ) : n ≤ m ∨ m < n -:= induction_on n +:= nat.induction_on n (or_intro_left _ (zero_le m)) (take (k : ℕ), assume IH : k ≤ m ∨ m < k, @@ -818,7 +818,7 @@ theorem le_total (n m : ℕ) : n ≤ m ∨ m ≤ n theorem strong_induction_on {P : ℕ → Prop} (n : ℕ) (IH : ∀n, (∀m, m < n → P m) → P n) : P n := have stronger : ∀k, k ≤ n → P k, from - induction_on n + nat.induction_on n (take (k : ℕ), assume H : k ≤ 0, have H2 : k = 0, from le_zero_inv H, @@ -946,7 +946,7 @@ theorem mul_positive_inv_right {n m : ℕ} (H : n * m > 0) : m > 0 theorem mul_left_inj {n m k : ℕ} (Hn : n > 0) (H : n * m = n * k) : m = k := have general : ∀m, n * m = n * k → m = k, from - induction_on k + nat.induction_on k (take m:ℕ, assume H : n * m = n * 0, have H2 : n * m = 0, @@ -1006,7 +1006,7 @@ theorem mul_lt {n m k l : ℕ} (H1 : n < k) (H2 : m < l) : n * m < k * l theorem mul_lt_left_inv {n m k : ℕ} (H : k * n < k * m) : n < m := have general : ∀ m, k * n < k * m → n < m, from - induction_on n + nat.induction_on n (take m : ℕ, assume H2 : k * 0 < k * m, have H3 : 0 < k * m, from mul_zero_right k ▸ H2, @@ -1067,7 +1067,7 @@ theorem sub_zero_right (n : ℕ) : n - 0 = n theorem sub_succ_right (n m : ℕ) : n - succ m = pred (n - m) theorem sub_zero_left (n : ℕ) : 0 - n = 0 -:= induction_on n (sub_zero_right 0) +:= nat.induction_on n (sub_zero_right 0) (take k : ℕ, assume IH : 0 - k = 0, calc @@ -1076,7 +1076,7 @@ theorem sub_zero_left (n : ℕ) : 0 - n = 0 ... = 0 : pred_zero) theorem sub_succ_succ (n m : ℕ) : succ n - succ m = n - m -:= induction_on m +:= nat.induction_on m (calc succ n - 1 = pred (succ n - 0) : sub_succ_right (succ n) 0 ... = pred (succ n) : {sub_zero_right (succ n)} @@ -1095,10 +1095,10 @@ theorem sub_one (n : ℕ) : n - 1 = pred n ... = pred n : {sub_zero_right n} theorem sub_self (n : ℕ) : n - n = 0 -:= induction_on n (sub_zero_right 0) (take k IH, trans (sub_succ_succ k k) IH) +:= nat.induction_on n (sub_zero_right 0) (take k IH, trans (sub_succ_succ k k) IH) theorem sub_add_add_right (n m k : ℕ) : (n + k) - (m + k) = n - m -:= induction_on k +:= nat.induction_on k (calc (n + 0) - (m + 0) = n - (m + 0) : {add_zero _} ... = n - m : {add_zero _}) @@ -1114,7 +1114,7 @@ theorem sub_add_add_left (n m k : ℕ) : (k + n) - (k + m) = n - m := subst (add_comm m k) (subst (add_comm n k) (sub_add_add_right n m k)) theorem sub_add_left (n m : ℕ) : n + m - m = n -:= induction_on m +:= nat.induction_on m (subst (symm (add_zero n)) (sub_zero_right n)) (take k : ℕ, assume IH : n + k - k = n, @@ -1124,7 +1124,7 @@ theorem sub_add_left (n m : ℕ) : n + m - m = n ... = n : IH) theorem sub_sub (n m k : ℕ) : n - m - k = n - (m + k) -:= induction_on k +:= nat.induction_on k (calc n - m - 0 = n - m : sub_zero_right _ ... = n - (m + 0) : {symm (add_zero m)}) @@ -1161,7 +1161,7 @@ theorem succ_sub_one (n : ℕ) : succ n - 1 = n ---------- mul theorem mul_pred_left (n m : ℕ) : pred n * m = n * m - m -:= induction_on n +:= nat.induction_on n (calc pred 0 * m = 0 * m : {pred_zero} ... = 0 : mul_zero_left _ @@ -1180,7 +1180,7 @@ theorem mul_pred_right (n m : ℕ) : n * pred m = n * m - n ... = n * m - n : {mul_comm m n} theorem mul_sub_distr_left (n m k : ℕ) : (n - m) * k = n * k - m * k -:= induction_on m +:= nat.induction_on m (calc (n - 0) * k = n * k : {sub_zero_right n} ... = n * k - 0 : symm (sub_zero_right _) diff --git a/tests/lean/slow/nat_wo_hints.lean b/tests/lean/slow/nat_wo_hints.lean index 8218e0277..4f75a184c 100644 --- a/tests/lean/slow/nat_wo_hints.lean +++ b/tests/lean/slow/nat_wo_hints.lean @@ -48,7 +48,7 @@ theorem pred_zero : pred 0 = 0 theorem pred_succ (n : ℕ) : pred (succ n) = n theorem zero_or_succ (n : ℕ) : n = 0 ∨ n = succ (pred n) -:= induction_on n +:= nat.induction_on n (or.intro_left _ (eq.refl 0)) (take m IH, or.intro_right _ (show succ m = succ (pred (succ m)), from congr_arg succ ((pred_succ m)⁻¹))) @@ -57,7 +57,7 @@ theorem zero_or_succ2 (n : ℕ) : n = 0 ∨ ∃k, n = succ k := or_of_or_of_imp_of_imp (zero_or_succ n) (assume H, H) (assume H : n = succ (pred n), exists.intro (pred n) H) theorem case {P : ℕ → Prop} (n : ℕ) (H1: P 0) (H2 : ∀m, P (succ m)) : P n -:= induction_on n H1 (take m IH, H2 m) +:= nat.induction_on n H1 (take m IH, H2 m) theorem discriminate {B : Prop} {n : ℕ} (H1: n = 0 → B) (H2 : ∀m, n = succ m → B) : B := or.elim (zero_or_succ n) @@ -71,7 +71,7 @@ theorem succ_inj {n m : ℕ} (H : succ n = succ m) : n = m ... = m : pred_succ m theorem succ_ne_self (n : ℕ) : succ n ≠ n -:= induction_on n +:= nat.induction_on n (take H : 1 = 0, have ne : 1 ≠ 0, from succ_ne_zero 0, absurd H ne) @@ -79,13 +79,13 @@ theorem succ_ne_self (n : ℕ) : succ n ≠ n theorem decidable_eq [instance] (n m : ℕ) : decidable (n = m) := have general : ∀n, decidable (n = m), from - rec_on m + nat.rec_on m (take n, - rec_on n + nat.rec_on n (inl (eq.refl 0)) (λ m iH, inr (succ_ne_zero m))) (λ (m' : ℕ) (iH1 : ∀n, decidable (n = m')), - take n, rec_on n + take n, nat.rec_on n (inr (ne.symm (succ_ne_zero m'))) (λ (n' : ℕ) (iH2 : decidable (n' = succ m')), have d1 : decidable (n' = m'), from iH1 n', @@ -100,7 +100,7 @@ theorem decidable_eq [instance] (n m : ℕ) : decidable (n = m) theorem two_step_induction_on {P : ℕ → Prop} (a : ℕ) (H1 : P 0) (H2 : P 1) (H3 : ∀ (n : ℕ) (IH1 : P n) (IH2 : P (succ n)), P (succ (succ n))) : P a := have stronger : P a ∧ P (succ a), from - induction_on a + nat.induction_on a (and.intro H1 H2) (take k IH, have IH1 : P k, from and.elim_left IH, @@ -110,7 +110,7 @@ theorem two_step_induction_on {P : ℕ → Prop} (a : ℕ) (H1 : P 0) (H2 : P 1) theorem sub_induction {P : ℕ → ℕ → Prop} (n m : ℕ) (H1 : ∀m, P 0 m) (H2 : ∀n, P (succ n) 0) (H3 : ∀n m, P n m → P (succ n) (succ m)) : P n m -:= have general : ∀m, P n m, from induction_on n +:= have general : ∀m, P n m, from nat.induction_on n (take m : ℕ, H1 m) (take k : ℕ, assume IH : ∀m, P k m, @@ -131,7 +131,7 @@ theorem add_succ (n m : ℕ) : n + succ m = succ (n + m) ---------- comm, assoc theorem zero_add (n : ℕ) : 0 + n = n -:= induction_on n +:= nat.induction_on n (add_zero 0) (take m IH, show 0 + succ m = succ m, from calc @@ -139,7 +139,7 @@ theorem zero_add (n : ℕ) : 0 + n = n ... = succ m : {IH}) theorem succ_add (n m : ℕ) : (succ n) + m = succ (n + m) -:= induction_on m +:= nat.induction_on m (calc succ n + 0 = succ n : add_zero (succ n) ... = succ (n + 0) : {symm (add_zero n)}) @@ -150,7 +150,7 @@ theorem succ_add (n m : ℕ) : (succ n) + m = succ (n + m) ... = succ (n + succ k) : {symm (add_succ _ _)}) theorem add_comm (n m : ℕ) : n + m = m + n -:= induction_on m +:= nat.induction_on m (trans (add_zero _) (symm (zero_add _))) (take k IH, calc @@ -169,7 +169,7 @@ theorem add_comm_succ (n m : ℕ) : n + succ m = m + succ n ... = m + succ n : add_comm (succ n) m theorem add_assoc (n m k : ℕ) : (n + m) + k = n + (m + k) -:= induction_on k +:= nat.induction_on k (calc (n + m) + 0 = n + m : add_zero _ ... = n + (m + 0) : {symm (add_zero m)}) @@ -191,7 +191,7 @@ theorem add_right_comm (n m k : ℕ) : n + m + k = n + k + m theorem add_cancel_left {n m k : ℕ} : n + m = n + k → m = k := - induction_on n + nat.induction_on n (take H : 0 + m = 0 + k, calc m = 0 + m : symm (zero_add m) @@ -218,7 +218,7 @@ theorem add_cancel_right {n m k : ℕ} (H : n + m = k + m) : n = k theorem eq_zero_of_add_eq_zero_right {n m : ℕ} : n + m = 0 → n = 0 := - induction_on n + nat.induction_on n (take (H : 0 + m = 0), eq.refl 0) (take k IH, assume (H : succ k + m = 0), @@ -267,7 +267,7 @@ set_option unifier.max_steps 100000 ---------- comm, distr, assoc, identity theorem mul_zero_left (n:ℕ) : 0 * n = 0 -:= induction_on n +:= nat.induction_on n (mul_zero_right 0) (take m IH, calc @@ -276,7 +276,7 @@ theorem mul_zero_left (n:ℕ) : 0 * n = 0 ... = 0 : IH) theorem mul_succ_left (n m:ℕ) : (succ n) * m = (n * m) + m -:= induction_on m +:= nat.induction_on m (calc succ n * 0 = 0 : mul_zero_right _ ... = n * 0 : symm (mul_zero_right _) @@ -291,7 +291,7 @@ theorem mul_succ_left (n m:ℕ) : (succ n) * m = (n * m) + m ... = (n * succ k) + succ k : {symm (mul_succ_right n k)}) theorem mul_comm (n m:ℕ) : n * m = m * n -:= induction_on m +:= nat.induction_on m (trans (mul_zero_right _) (symm (mul_zero_left _))) (take k IH, calc @@ -300,7 +300,7 @@ theorem mul_comm (n m:ℕ) : n * m = m * n ... = (succ k) * n : symm (mul_succ_left _ _)) theorem mul_add_distr_left (n m k : ℕ) : (n + m) * k = n * k + m * k -:= induction_on k +:= nat.induction_on k (calc (n + m) * 0 = 0 : mul_zero_right _ ... = 0 + 0 : symm (add_zero _) @@ -323,7 +323,7 @@ theorem mul_add_distr_right (n m k : ℕ) : n * (m + k) = n * m + n * k ... = n * m + n * k : {mul_comm _ _} theorem mul_assoc (n m k:ℕ) : (n * m) * k = n * (m * k) -:= induction_on k +:= nat.induction_on k (calc (n * m) * 0 = 0 : mul_zero_right _ ... = n * 0 : symm (mul_zero_right _) @@ -627,7 +627,7 @@ theorem pred_le_imp_le_or_eq {n m : ℕ} (H : pred n ≤ m) : n ≤ m ∨ n = su theorem mul_le_left {n m : ℕ} (H : n ≤ m) (k : ℕ) : k * n ≤ k * m := obtain (l : ℕ) (Hl : n + l = m), from (le_elim H), - induction_on k + nat.induction_on k (have H2 : 0 * n = 0 * m, from calc 0 * n = 0 : mul_zero_left n @@ -777,7 +777,7 @@ theorem succ_lt_right {n m : ℕ} (H : n < m) : n < succ m ---------- totality of lt and le theorem le_or_lt (n m : ℕ) : n ≤ m ∨ m < n -:= induction_on n +:= nat.induction_on n (or.intro_left _ (zero_le m)) (take (k : ℕ), assume IH : k ≤ m ∨ m < k, @@ -816,7 +816,7 @@ theorem le_total (n m : ℕ) : n ≤ m ∨ m ≤ n theorem strong_induction_on {P : ℕ → Prop} (n : ℕ) (IH : ∀n, (∀m, m < n → P m) → P n) : P n := have stronger : ∀k, k ≤ n → P k, from - induction_on n + nat.induction_on n (take (k : ℕ), assume H : k ≤ 0, have H2 : k = 0, from le_zero_inv H, @@ -950,7 +950,7 @@ theorem mul_positive_inv_right {n m : ℕ} (H : n * m > 0) : m > 0 theorem mul_left_inj {n m k : ℕ} (Hn : n > 0) (H : n * m = n * k) : m = k := have general : ∀m, n * m = n * k → m = k, from - induction_on k + nat.induction_on k (take m:ℕ, assume H : n * m = n * 0, have H2 : n * m = 0, @@ -1010,7 +1010,7 @@ theorem mul_lt {n m k l : ℕ} (H1 : n < k) (H2 : m < l) : n * m < k * l theorem mul_lt_left_inv {n m k : ℕ} (H : k * n < k * m) : n < m := have general : ∀ m, k * n < k * m → n < m, from - induction_on n + nat.induction_on n (take m : ℕ, assume H2 : k * 0 < k * m, have H3 : 0 < k * m, from mul_zero_right k ▸ H2, @@ -1071,7 +1071,7 @@ theorem sub_zero_right (n : ℕ) : n - 0 = n theorem sub_succ_right (n m : ℕ) : n - succ m = pred (n - m) theorem sub_zero_left (n : ℕ) : 0 - n = 0 -:= induction_on n (sub_zero_right 0) +:= nat.induction_on n (sub_zero_right 0) (take k : ℕ, assume IH : 0 - k = 0, calc @@ -1080,7 +1080,7 @@ theorem sub_zero_left (n : ℕ) : 0 - n = 0 ... = 0 : pred_zero) theorem sub_succ_succ (n m : ℕ) : succ n - succ m = n - m -:= induction_on m +:= nat.induction_on m (calc succ n - 1 = pred (succ n - 0) : sub_succ_right (succ n) 0 ... = pred (succ n) : {sub_zero_right (succ n)} @@ -1099,10 +1099,10 @@ theorem sub_one (n : ℕ) : n - 1 = pred n ... = pred n : {sub_zero_right n} theorem sub_self (n : ℕ) : n - n = 0 -:= induction_on n (sub_zero_right 0) (take k IH, trans (sub_succ_succ k k) IH) +:= nat.induction_on n (sub_zero_right 0) (take k IH, trans (sub_succ_succ k k) IH) theorem sub_add_add_right (n m k : ℕ) : (n + k) - (m + k) = n - m -:= induction_on k +:= nat.induction_on k (calc (n + 0) - (m + 0) = n - (m + 0) : {add_zero _} ... = n - m : {add_zero _}) @@ -1118,7 +1118,7 @@ theorem sub_add_add_left (n m k : ℕ) : (k + n) - (k + m) = n - m := subst (add_comm m k) (subst (add_comm n k) (sub_add_add_right n m k)) theorem sub_add_left (n m : ℕ) : n + m - m = n -:= induction_on m +:= nat.induction_on m (subst (symm (add_zero n)) (sub_zero_right n)) (take k : ℕ, assume IH : n + k - k = n, @@ -1128,7 +1128,7 @@ theorem sub_add_left (n m : ℕ) : n + m - m = n ... = n : IH) theorem sub_sub (n m k : ℕ) : n - m - k = n - (m + k) -:= induction_on k +:= nat.induction_on k (calc n - m - 0 = n - m : sub_zero_right _ ... = n - (m + 0) : {symm (add_zero m)}) @@ -1165,7 +1165,7 @@ theorem succ_sub_one (n : ℕ) : succ n - 1 = n ---------- mul theorem mul_pred_left (n m : ℕ) : pred n * m = n * m - m -:= induction_on n +:= nat.induction_on n (calc pred 0 * m = 0 * m : {pred_zero} ... = 0 : mul_zero_left _ @@ -1184,7 +1184,7 @@ theorem mul_pred_right (n m : ℕ) : n * pred m = n * m - n ... = n * m - n : {mul_comm m n} theorem mul_sub_distr_left (n m k : ℕ) : (n - m) * k = n * k - m * k -:= induction_on m +:= nat.induction_on m (calc (n - 0) * k = n * k : {sub_zero_right n} ... = n * k - 0 : symm (sub_zero_right _) diff --git a/tests/lean/slow/path_groupoids.lean b/tests/lean/slow/path_groupoids.lean index f71fb7d85..528f9afc9 100644 --- a/tests/lean/slow/path_groupoids.lean +++ b/tests/lean/slow/path_groupoids.lean @@ -42,62 +42,62 @@ definition concat_11 {A : Type} (x : A) : idpath x ⬝ idpath x ≈ idpath x := -- The identity path is a right unit. definition concat_p1 {A : Type} {x y : A} (p : x ≈ y) : p ⬝ idp ≈ p := -rec_on p idp +path.rec_on p idp -- The identity path is a right unit. definition concat_1p {A : Type} {x y : A} (p : x ≈ y) : idp ⬝ p ≈ p := -rec_on p idp +path.rec_on p idp -- Concatenation is associative. definition concat_p_pp {A : Type} {x y z t : A} (p : x ≈ y) (q : y ≈ z) (r : z ≈ t) : p ⬝ (q ⬝ r) ≈ (p ⬝ q) ⬝ r := -rec_on r (rec_on q idp) +path.rec_on r (path.rec_on q idp) definition concat_pp_p {A : Type} {x y z t : A} (p : x ≈ y) (q : y ≈ z) (r : z ≈ t) : (p ⬝ q) ⬝ r ≈ p ⬝ (q ⬝ r) := -rec_on r (rec_on q idp) +path.rec_on r (path.rec_on q idp) -- The left inverse law. definition concat_pV {A : Type} {x y : A} (p : x ≈ y) : p ⬝ p^ ≈ idp := -rec_on p idp +path.rec_on p idp -- The right inverse law. definition concat_Vp {A : Type} {x y : A} (p : x ≈ y) : p^ ⬝ p ≈ idp := -rec_on p idp +path.rec_on p idp -- Several auxiliary theorems about canceling inverses across associativity. These are somewhat -- redundant, following from earlier theorems. definition concat_V_pp {A : Type} {x y z : A} (p : x ≈ y) (q : y ≈ z) : p^ ⬝ (p ⬝ q) ≈ q := -rec_on q (rec_on p idp) +path.rec_on q (path.rec_on p idp) definition concat_p_Vp {A : Type} {x y z : A} (p : x ≈ y) (q : x ≈ z) : p ⬝ (p^ ⬝ q) ≈ q := -rec_on q (rec_on p idp) +path.rec_on q (path.rec_on p idp) definition concat_pp_V {A : Type} {x y z : A} (p : x ≈ y) (q : y ≈ z) : (p ⬝ q) ⬝ q^ ≈ p := -rec_on q (rec_on p idp) +path.rec_on q (path.rec_on p idp) definition concat_pV_p {A : Type} {x y z : A} (p : x ≈ z) (q : y ≈ z) : (p ⬝ q^) ⬝ q ≈ p := -rec_on q (take p, rec_on p idp) p +path.rec_on q (take p, path.rec_on p idp) p -- Inverse distributes over concatenation definition inv_pp {A : Type} {x y z : A} (p : x ≈ y) (q : y ≈ z) : (p ⬝ q)^ ≈ q^ ⬝ p^ := -rec_on q (rec_on p idp) +path.rec_on q (path.rec_on p idp) definition inv_Vp {A : Type} {x y z : A} (p : y ≈ x) (q : y ≈ z) : (p^ ⬝ q)^ ≈ q^ ⬝ p := -rec_on q (rec_on p idp) +path.rec_on q (path.rec_on p idp) -- universe metavariables definition inv_pV {A : Type} {x y z : A} (p : x ≈ y) (q : z ≈ y) : (p ⬝ q^)^ ≈ q ⬝ p^ := -rec_on p (λq, rec_on q idp) q +path.rec_on p (λq, path.rec_on q idp) q definition inv_VV {A : Type} {x y z : A} (p : y ≈ x) (q : z ≈ y) : (p^ ⬝ q^)^ ≈ q ⬝ p := -rec_on p (rec_on q idp) +path.rec_on p (path.rec_on q idp) -- Inverse is an involution. definition inv_V {A : Type} {x y : A} (p : x ≈ y) : p^^ ≈ p := -rec_on p idp +path.rec_on p idp -- Theorems for moving things around in equations @@ -106,7 +106,7 @@ rec_on p idp definition moveR_Mp {A : Type} {x y z : A} (p : x ≈ z) (q : y ≈ z) (r : y ≈ x) : p ≈ (r^ ⬝ q) → (r ⬝ p) ≈ q := have gen : Πp q, p ≈ (r^ ⬝ q) → (r ⬝ p) ≈ q, from - rec_on r + path.rec_on r (take p q, assume h : p ≈ idp^ ⬝ q, show idp ⬝ p ≈ q, from concat_1p _ ⬝ h ⬝ concat_1p _), @@ -114,63 +114,63 @@ gen p q definition moveR_pM {A : Type} {x y z : A} (p : x ≈ z) (q : y ≈ z) (r : y ≈ x) : r ≈ q ⬝ p^ → r ⬝ p ≈ q := -rec_on p (take q r h, (concat_p1 _ ⬝ h ⬝ concat_p1 _)) q r +path.rec_on p (take q r h, (concat_p1 _ ⬝ h ⬝ concat_p1 _)) q r definition moveR_Vp {A : Type} {x y z : A} (p : x ≈ z) (q : y ≈ z) (r : x ≈ y) : p ≈ r ⬝ q → r^ ⬝ p ≈ q := -rec_on r (take p q h, concat_1p _ ⬝ h ⬝ concat_1p _) p q +path.rec_on r (take p q h, concat_1p _ ⬝ h ⬝ concat_1p _) p q definition moveR_pV {A : Type} {x y z : A} (p : z ≈ x) (q : y ≈ z) (r : y ≈ x) : r ≈ q ⬝ p → r ⬝ p^ ≈ q := -rec_on p (take q r h, concat_p1 _ ⬝ h ⬝ concat_p1 _) q r +path.rec_on p (take q r h, concat_p1 _ ⬝ h ⬝ concat_p1 _) q r definition moveL_Mp {A : Type} {x y z : A} (p : x ≈ z) (q : y ≈ z) (r : y ≈ x) : r^ ⬝ q ≈ p → q ≈ r ⬝ p := -rec_on r (take p q h, (concat_1p _)^ ⬝ h ⬝ (concat_1p _)^) p q +path.rec_on r (take p q h, (concat_1p _)^ ⬝ h ⬝ (concat_1p _)^) p q definition moveL_pM {A : Type} {x y z : A} (p : x ≈ z) (q : y ≈ z) (r : y ≈ x) : q ⬝ p^ ≈ r → q ≈ r ⬝ p := -rec_on p (take q r h, (concat_p1 _)^ ⬝ h ⬝ (concat_p1 _)^) q r +path.rec_on p (take q r h, (concat_p1 _)^ ⬝ h ⬝ (concat_p1 _)^) q r definition moveL_Vp {A : Type} {x y z : A} (p : x ≈ z) (q : y ≈ z) (r : x ≈ y) : r ⬝ q ≈ p → q ≈ r^ ⬝ p := -rec_on r (take p q h, (concat_1p _)^ ⬝ h ⬝ (concat_1p _)^) p q +path.rec_on r (take p q h, (concat_1p _)^ ⬝ h ⬝ (concat_1p _)^) p q definition moveL_pV {A : Type} {x y z : A} (p : z ≈ x) (q : y ≈ z) (r : y ≈ x) : q ⬝ p ≈ r → q ≈ r ⬝ p^ := -rec_on p (take q r h, (concat_p1 _)^ ⬝ h ⬝ (concat_p1 _)^) q r +path.rec_on p (take q r h, (concat_p1 _)^ ⬝ h ⬝ (concat_p1 _)^) q r definition moveL_1M {A : Type} {x y : A} (p q : x ≈ y) : p ⬝ q^ ≈ idp → p ≈ q := -rec_on q (take p h, (concat_p1 _)^ ⬝ h) p +path.rec_on q (take p h, (concat_p1 _)^ ⬝ h) p definition moveL_M1 {A : Type} {x y : A} (p q : x ≈ y) : q^ ⬝ p ≈ idp → p ≈ q := -rec_on q (take p h, (concat_1p _)^ ⬝ h) p +path.rec_on q (take p h, (concat_1p _)^ ⬝ h) p definition moveL_1V {A : Type} {x y : A} (p : x ≈ y) (q : y ≈ x) : p ⬝ q ≈ idp → p ≈ q^ := -rec_on q (take p h, (concat_p1 _)^ ⬝ h) p +path.rec_on q (take p h, (concat_p1 _)^ ⬝ h) p definition moveL_V1 {A : Type} {x y : A} (p : x ≈ y) (q : y ≈ x) : q ⬝ p ≈ idp → p ≈ q^ := -rec_on q (take p h, (concat_1p _)^ ⬝ h) p +path.rec_on q (take p h, (concat_1p _)^ ⬝ h) p definition moveR_M1 {A : Type} {x y : A} (p q : x ≈ y) : idp ≈ p^ ⬝ q → p ≈ q := -rec_on p (take q h, h ⬝ (concat_1p _)) q +path.rec_on p (take q h, h ⬝ (concat_1p _)) q definition moveR_1M {A : Type} {x y : A} (p q : x ≈ y) : idp ≈ q ⬝ p^ → p ≈ q := -rec_on p (take q h, h ⬝ (concat_p1 _)) q +path.rec_on p (take q h, h ⬝ (concat_p1 _)) q definition moveR_1V {A : Type} {x y : A} (p : x ≈ y) (q : y ≈ x) : idp ≈ q ⬝ p → p^ ≈ q := -rec_on p (take q h, h ⬝ (concat_p1 _)) q +path.rec_on p (take q h, h ⬝ (concat_p1 _)) q definition moveR_V1 {A : Type} {x y : A} (p : x ≈ y) (q : y ≈ x) : idp ≈ p ⬝ q → p^ ≈ q := -rec_on p (take q h, h ⬝ (concat_1p _)) q +path.rec_on p (take q h, h ⬝ (concat_1p _)) q -- Transport @@ -205,13 +205,13 @@ definition apD10 {A} {B : A → Type} {f g : Πx, B x} (H : f ≈ g) : f ∼ g : definition ap10 {A B} {f g : A → B} (H : f ≈ g) : f ∼ g := apD10 H definition ap11 {A B} {f g : A → B} (H : f ≈ g) {x y : A} (p : x ≈ y) : f x ≈ g y := -rec_on H (rec_on p idp) +path.rec_on H (path.rec_on p idp) -- TODO: Note that the next line breaks the proof! --- opaque_hint (hiding rec_on) +-- opaque_hint (hiding path.rec_on) -- set_option pp.implicit true definition apD {A:Type} {B : A → Type} (f : Πa:A, B a) {x y : A} (p : x ≈ y) : p # (f x) ≈ f y := -rec_on p idp +path.rec_on p idp -- More theorems for moving things around in equations @@ -219,19 +219,19 @@ rec_on p idp definition moveR_transport_p {A : Type} (P : A → Type) {x y : A} (p : x ≈ y) (u : P x) (v : P y) : u ≈ p^ # v → p # u ≈ v := -rec_on p (take u v, id) u v +path.rec_on p (take u v, id) u v definition moveR_transport_V {A : Type} (P : A → Type) {x y : A} (p : y ≈ x) (u : P x) (v : P y) : u ≈ p # v → p^ # u ≈ v := -rec_on p (take u v, id) u v +path.rec_on p (take u v, id) u v definition moveL_transport_V {A : Type} (P : A → Type) {x y : A} (p : x ≈ y) (u : P x) (v : P y) : p # u ≈ v → u ≈ p^ # v := -rec_on p (take u v, id) u v +path.rec_on p (take u v, id) u v definition moveL_transport_p {A : Type} (P : A → Type) {x y : A} (p : y ≈ x) (u : P x) (v : P y) : p^ # u ≈ v → u ≈ p # v := -rec_on p (take u v, id) u v +path.rec_on p (take u v, id) u v -- Functoriality of functions @@ -248,54 +248,54 @@ definition apD_1 {A B} (x : A) (f : forall x : A, B x) : apD f idp ≈ idp :> (f -- Functions commute with concatenation. definition ap_pp {A B : Type} (f : A → B) {x y z : A} (p : x ≈ y) (q : y ≈ z) : ap f (p ⬝ q) ≈ (ap f p) ⬝ (ap f q) := -rec_on q (rec_on p idp) +path.rec_on q (path.rec_on p idp) definition ap_p_pp {A B : Type} (f : A → B) {w x y z : A} (r : f w ≈ f x) (p : x ≈ y) (q : y ≈ z) : r ⬝ (ap f (p ⬝ q)) ≈ (r ⬝ ap f p) ⬝ (ap f q) := -rec_on p (take r q, rec_on q (concat_p_pp r idp idp)) r q +path.rec_on p (take r q, path.rec_on q (concat_p_pp r idp idp)) r q definition ap_pp_p {A B : Type} (f : A → B) {w x y z : A} (p : x ≈ y) (q : y ≈ z) (r : f z ≈ f w) : (ap f (p ⬝ q)) ⬝ r ≈ (ap f p) ⬝ (ap f q ⬝ r) := -rec_on p (take q, rec_on q (take r, concat_pp_p _ _ _)) q r +path.rec_on p (take q, path.rec_on q (take r, concat_pp_p _ _ _)) q r -- Functions commute with path inverses. definition inverse_ap {A B : Type} (f : A → B) {x y : A} (p : x ≈ y) : (ap f p)^ ≈ ap f (p^) := -rec_on p idp +path.rec_on p idp definition ap_V {A B : Type} (f : A → B) {x y : A} (p : x ≈ y) : ap f (p^) ≈ (ap f p)^ := -rec_on p idp +path.rec_on p idp -- TODO: rename id to idmap? definition ap_idmap {A : Type} {x y : A} (p : x ≈ y) : ap id p ≈ p := -rec_on p idp +path.rec_on p idp definition ap_compose {A B C : Type} (f : A → B) (g : B → C) {x y : A} (p : x ≈ y) : ap (g ∘ f) p ≈ ap g (ap f p) := -rec_on p idp +path.rec_on p idp -- Sometimes we don't have the actual function [compose]. definition ap_compose' {A B C : Type} (f : A → B) (g : B → C) {x y : A} (p : x ≈ y) : ap (λa, g (f a)) p ≈ ap g (ap f p) := -rec_on p idp +path.rec_on p idp -- The action of constant maps. definition ap_const {A B : Type} {x y : A} (p : x ≈ y) (z : B) : ap (λu, z) p ≈ idp := -rec_on p idp +path.rec_on p idp -- Naturality of [ap]. definition concat_Ap {A B : Type} {f g : A → B} (p : forall x, f x ≈ g x) {x y : A} (q : x ≈ y) : (ap f q) ⬝ (p y) ≈ (p x) ⬝ (ap g q) := -rec_on q (concat_1p _ ⬝ (concat_p1 _)^) +path.rec_on q (concat_1p _ ⬝ (concat_p1 _)^) -- Naturality of [ap] at identity. definition concat_A1p {A : Type} {f : A → A} (p : forall x, f x ≈ x) {x y : A} (q : x ≈ y) : (ap f q) ⬝ (p y) ≈ (p x) ⬝ q := -rec_on q (concat_1p _ ⬝ (concat_p1 _)^) +path.rec_on q (concat_1p _ ⬝ (concat_p1 _)^) definition concat_pA1 {A : Type} {f : A → A} (p : forall x, x ≈ f x) {x y : A} (q : x ≈ y) : (p x) ⬝ (ap f q) ≈ q ⬝ (p y) := -rec_on q (concat_p1 _ ⬝ (concat_1p _)^) +path.rec_on q (concat_p1 _ ⬝ (concat_1p _)^) --TODO: note that the Coq proof for the preceding is -- @@ -310,7 +310,7 @@ definition concat_pA_pp {A B : Type} {f g : A → B} (p : forall x, f x ≈ g x) {x y : A} (q : x ≈ y) {w z : B} (r : w ≈ f x) (s : g y ≈ z) : (r ⬝ ap f q) ⬝ (p y ⬝ s) ≈ (r ⬝ p x) ⬝ (ap g q ⬝ s) := -rec_on q (take s, rec_on s (take r, idp)) s r +path.rec_on q (take s, path.rec_on s (take r, idp)) s r -- Action of [apD10] and [ap10] on paths -- ------------------------------------- @@ -321,11 +321,11 @@ definition apD10_1 {A} {B : A → Type} (f : Πx, B x) (x : A) : apD10 (idpath f definition apD10_pp {A} {B : A → Type} {f f' f'' : Πx, B x} (h : f ≈ f') (h' : f' ≈ f'') (x : A) : apD10 (h ⬝ h') x ≈ apD10 h x ⬝ apD10 h' x := -rec_on h (take h', rec_on h' idp) h' +path.rec_on h (take h', path.rec_on h' idp) h' definition apD10_V {A : Type} {B : A → Type} {f g : Πx : A, B x} (h : f ≈ g) (x : A) : apD10 (h^) x ≈ (apD10 h x)^ := -rec_on h idp +path.rec_on h idp definition ap10_1 {A B} {f : A → B} (x : A) : ap10 (idpath f) x ≈ idp := idp @@ -337,7 +337,7 @@ definition ap10_V {A B} {f g : A→B} (h : f ≈ g) (x:A) : ap10 (h^) x ≈ (ap1 -- [ap10] also behaves nicely on paths produced by [ap] definition ap_ap10 {A B C} (f g : A → B) (h : B → C) (p : f ≈ g) (a : A) : ap h (ap10 p a) ≈ ap10 (ap (λ f', h ∘ f') p) a:= -rec_on p idp +path.rec_on p idp -- Transport and the groupoid structure of paths @@ -349,7 +349,7 @@ rec_on p idp definition transport_pp {A : Type} (P : A → Type) {x y z : A} (p : x ≈ y) (q : y ≈ z) (u : P x) : p ⬝ q # u ≈ q # p # u := -rec_on q (rec_on p idp) +path.rec_on q (path.rec_on p idp) definition transport_pV {A : Type} (P : A → Type) {x y : A} (p : x ≈ y) (z : P y) : p # p^ # z ≈ z := @@ -369,27 +369,27 @@ theorem double_induction {C : Π(x y z : A), Π(p : x ≈ y), Π(q : y ≈ z), Type} (H : C x x x (idpath x) (idpath x)) : C x y z p q := -rec_on p (take z q, rec_on q H) z q +path.rec_on p (take z q, path.rec_on q H) z q theorem double_induction2 {A : Type} {x y z : A} (p : x ≈ y) (q : z ≈ y) {C : Π(x y z : A), Π(p : x ≈ y), Π(q : z ≈ y), Type} (H : C z z z (idpath z) (idpath z)) : C x y z p q := -rec_on p (take y q, rec_on q H) y q +path.rec_on p (take y q, path.rec_on q H) y q theorem double_induction2' {A : Type} {x y z : A} (p : x ≈ y) (q : z ≈ y) {C : Π(x y z : A), Π(p : x ≈ y), Π(q : z ≈ y), Type} (H : C z z z (idpath z) (idpath z)) : C x y z p q := -rec_on p (take y q, rec_on q H) y q +path.rec_on p (take y q, path.rec_on q H) y q theorem triple_induction {A : Type} {x y z w : A} (p : x ≈ y) (q : y ≈ z) (r : z ≈ w) {C : Π(x y z w : A), Π(p : x ≈ y), Π(q : y ≈ z), Π(r: z ≈ w), Type} (H : C x x x x (idpath x) (idpath x) (idpath x)) : C x y z w p q r := -rec_on p (take z q, rec_on q (take w r, rec_on r H)) z q w r +path.rec_on p (take z q, path.rec_on q (take w r, path.rec_on r H)) z q w r -- try this again definition concat_pV_p_new {A : Type} {x y z : A} (p : x ≈ z) (q : y ≈ z) : (p ⬝ q^) ⬝ q ≈ p := @@ -406,13 +406,13 @@ triple_induction p q r (take u, idp) u -- Here is another coherence lemma for transport. definition transport_pVp {A} (P : A → Type) {x y : A} (p : x ≈ y) (z : P x) : transport_pV P p (transport P p z) ≈ ap (transport P p) (transport_Vp P p z) -:= rec_on p idp +:= path.rec_on p idp -- Dependent transport in a doubly dependent type. definition transportD {A : Type} (B : A → Type) (C : Π a : A, B a → Type) {x1 x2 : A} (p : x1 ≈ x2) (y : B x1) (z : C x1 y) : C x2 (p # y) := -rec_on p z +path.rec_on p z -- Transporting along higher-dimensional paths definition transport2 {A : Type} (P : A → Type) {x y : A} {p q : x ≈ y} (r : p ≈ q) (z : P x) : @@ -422,28 +422,28 @@ definition transport2 {A : Type} (P : A → Type) {x y : A} {p q : x ≈ y} (r : definition transport2_is_ap10 {A : Type} (Q : A → Type) {x y : A} {p q : x ≈ y} (r : p ≈ q) (z : Q x) : transport2 Q r z ≈ ap10 (ap (transport Q) r) z := -rec_on r idp +path.rec_on r idp definition transport2_p2p {A : Type} (P : A → Type) {x y : A} {p1 p2 p3 : x ≈ y} (r1 : p1 ≈ p2) (r2 : p2 ≈ p3) (z : P x) : transport2 P (r1 ⬝ r2) z ≈ transport2 P r1 z ⬝ transport2 P r2 z := -rec_on r1 (rec_on r2 idp) +path.rec_on r1 (path.rec_on r2 idp) -- TODO: another interesting case definition transport2_V {A : Type} (Q : A → Type) {x y : A} {p q : x ≈ y} (r : p ≈ q) (z : Q x) : transport2 Q (r^) z ≈ ((transport2 Q r z)^) := --- rec_on r idp -- doesn't work -rec_on r (idpath (inverse (transport2 Q (idpath p) z))) +-- path.rec_on r idp -- doesn't work +path.rec_on r (idpath (inverse (transport2 Q (idpath p) z))) definition concat_AT {A : Type} (P : A → Type) {x y : A} {p q : x ≈ y} {z w : P x} (r : p ≈ q) (s : z ≈ w) : ap (transport P p) s ⬝ transport2 P r w ≈ transport2 P r z ⬝ ap (transport P q) s := -rec_on r (concat_p1 _ ⬝ (concat_1p _)^) +path.rec_on r (concat_p1 _ ⬝ (concat_1p _)^) -- TODO (from Coq library): What should this be called? definition ap_transport {A} {P Q : A → Type} {x y : A} (p : x ≈ y) (f : Πx, P x → Q x) (z : P x) : f y (p # z) ≈ (p # (f x z)) := -rec_on p idp +path.rec_on p idp -- Transporting in particular fibrations @@ -461,34 +461,34 @@ subdirectory. Here we consider only the most basic cases. -- Transporting in a constant fibration. definition transport_const {A B : Type} {x1 x2 : A} (p : x1 ≈ x2) (y : B) : transport (λx, B) p y ≈ y := -rec_on p idp +path.rec_on p idp definition transport2_const {A B : Type} {x1 x2 : A} {p q : x1 ≈ x2} (r : p ≈ q) (y : B) : transport_const p y ≈ transport2 (λu, B) r y ⬝ transport_const q y := -rec_on r (concat_1p _)^ +path.rec_on r (concat_1p _)^ -- Transporting in a pulled back fibration. definition transport_compose {A B} {x y : A} (P : B → Type) (f : A → B) (p : x ≈ y) (z : P (f x)) : transport (λx, P (f x)) p z ≈ transport P (ap f p) z := -rec_on p idp +path.rec_on p idp definition transport_precompose {A B C} (f : A → B) (g g' : B → C) (p : g ≈ g') : transport (λh : B → C, g ∘ f ≈ h ∘ f) p idp ≈ ap (λh, h ∘ f) p := -rec_on p idp +path.rec_on p idp definition apD10_ap_precompose {A B C} (f : A → B) (g g' : B → C) (p : g ≈ g') (a : A) : apD10 (ap (λh : B → C, h ∘ f) p) a ≈ apD10 p (f a) := -rec_on p idp +path.rec_on p idp definition apD10_ap_postcompose {A B C} (f : B → C) (g g' : A → B) (p : g ≈ g') (a : A) : apD10 (ap (λh : A → B, f ∘ h) p) a ≈ ap f (apD10 p a) := -rec_on p idp +path.rec_on p idp -- TODO: another example where a term has to be given explicitly -- A special case of [transport_compose] which seems to come up a lot. definition transport_idmap_ap A (P : A → Type) x y (p : x ≈ y) (u : P x) : transport P p u ≈ transport (λz, z) (ap P p) u := -rec_on p (idpath (transport (λ (z : Type), z) (ap P (idpath x)) u)) +path.rec_on p (idpath (transport (λ (z : Type), z) (ap P (idpath x)) u)) -- The behavior of [ap] and [apD] @@ -497,7 +497,7 @@ rec_on p (idpath (transport (λ (z : Type), z) (ap P (idpath x)) u)) -- In a constant fibration, [apD] reduces to [ap], modulo [transport_const]. definition apD_const {A B} {x y : A} (f : A → B) (p: x ≈ y) : apD f p ≈ transport_const p (f x) ⬝ ap f p := -rec_on p idp +path.rec_on p idp -- The 2-dimensional groupoid structure @@ -506,13 +506,13 @@ rec_on p idp -- Horizontal composition of 2-dimensional paths. definition concat2 {A} {x y z : A} {p p' : x ≈ y} {q q' : y ≈ z} (h : p ≈ p') (h' : q ≈ q') : p ⬝ q ≈ p' ⬝ q' := -rec_on h (rec_on h' idp) +path.rec_on h (path.rec_on h' idp) infixl `⬝⬝`:75 := concat2 -- 2-dimensional path inversion definition inverse2 {A : Type} {x y : A} {p q : x ≈ y} (h : p ≈ q) : p^ ≈ q^ := -rec_on h idp +path.rec_on h idp -- Whiskering -- ---------- @@ -528,47 +528,47 @@ h ⬝⬝ idp -- ------------------------------- definition cancelL {A} {x y z : A} (p : x ≈ y) (q r : y ≈ z) : (p ⬝ q ≈ p ⬝ r) → (q ≈ r) := -rec_on p (take r, rec_on r (take q a, (concat_1p q)^ ⬝ a)) r q +path.rec_on p (take r, path.rec_on r (take q a, (concat_1p q)^ ⬝ a)) r q definition cancelR {A} {x y z : A} (p q : x ≈ y) (r : y ≈ z) : (p ⬝ r ≈ q ⬝ r) → (p ≈ q) := -rec_on r (take p, rec_on p (take q a, a ⬝ concat_p1 q)) p q +path.rec_on r (take p, path.rec_on p (take q a, a ⬝ concat_p1 q)) p q -- Whiskering and identity paths. definition whiskerR_p1 {A : Type} {x y : A} {p q : x ≈ y} (h : p ≈ q) : (concat_p1 p)^ ⬝ whiskerR h idp ⬝ concat_p1 q ≈ h := -rec_on h (rec_on p idp) +path.rec_on h (path.rec_on p idp) definition whiskerR_1p {A : Type} {x y z : A} (p : x ≈ y) (q : y ≈ z) : whiskerR idp q ≈ idp :> (p ⬝ q ≈ p ⬝ q) := -rec_on q idp +path.rec_on q idp definition whiskerL_p1 {A : Type} {x y z : A} (p : x ≈ y) (q : y ≈ z) : whiskerL p idp ≈ idp :> (p ⬝ q ≈ p ⬝ q) := -rec_on q idp +path.rec_on q idp definition whiskerL_1p {A : Type} {x y : A} {p q : x ≈ y} (h : p ≈ q) : (concat_1p p) ^ ⬝ whiskerL idp h ⬝ concat_1p q ≈ h := -rec_on h (rec_on p idp) +path.rec_on h (path.rec_on p idp) definition concat2_p1 {A : Type} {x y : A} {p q : x ≈ y} (h : p ≈ q) : h ⬝⬝ idp ≈ whiskerR h idp :> (p ⬝ idp ≈ q ⬝ idp) := -rec_on h idp +path.rec_on h idp definition concat2_1p {A : Type} {x y : A} {p q : x ≈ y} (h : p ≈ q) : idp ⬝⬝ h ≈ whiskerL idp h :> (idp ⬝ p ≈ idp ⬝ q) := -rec_on h idp +path.rec_on h idp -- TODO: note, 4 inductions -- The interchange law for concatenation. definition concat_concat2 {A : Type} {x y z : A} {p p' p'' : x ≈ y} {q q' q'' : y ≈ z} (a : p ≈ p') (b : p' ≈ p'') (c : q ≈ q') (d : q' ≈ q'') : (a ⬝⬝ c) ⬝ (b ⬝⬝ d) ≈ (a ⬝ b) ⬝⬝ (c ⬝ d) := -rec_on d (rec_on c (rec_on b (rec_on a idp))) +path.rec_on d (path.rec_on c (path.rec_on b (path.rec_on a idp))) definition concat_whisker {A} {x y z : A} (p p' : x ≈ y) (q q' : y ≈ z) (a : p ≈ p') (b : q ≈ q') : (whiskerR a q) ⬝ (whiskerL p' b) ≈ (whiskerL p b) ⬝ (whiskerR a q') := -rec_on b (rec_on a (concat_1p _)^) +path.rec_on b (path.rec_on a (concat_1p _)^) -- Structure corresponding to the coherence equations of a bicategory. @@ -578,12 +578,12 @@ definition pentagon {A : Type} {v w x y z : A} (p : v ≈ w) (q : w ≈ x) (r : ⬝ concat_p_pp p (q ⬝ r) s ⬝ whiskerR (concat_p_pp p q r) s ≈ concat_p_pp p q (r ⬝ s) ⬝ concat_p_pp (p ⬝ q) r s := -rec_on p (take q, rec_on q (take r, rec_on r (take s, rec_on s idp))) q r s +path.rec_on p (take q, path.rec_on q (take r, path.rec_on r (take s, path.rec_on s idp))) q r s -- The 3-cell witnessing the left unit triangle. definition triangulator {A : Type} {x y z : A} (p : x ≈ y) (q : y ≈ z) : concat_p_pp p idp q ⬝ whiskerR (concat_p1 p) q ≈ whiskerL p (concat_1p q) := -rec_on p (take q, rec_on q idp) q +path.rec_on p (take q, path.rec_on q idp) q definition eckmann_hilton {A : Type} {x:A} (p q : idp ≈ idp :> (x ≈ x)) : p ⬝ q ≈ q ⬝ p := (whiskerR_p1 p ⬝⬝ whiskerL_1p q)^ @@ -597,20 +597,20 @@ definition eckmann_hilton {A : Type} {x:A} (p q : idp ≈ idp :> (x ≈ x)) : p -- The action of functions on 2-dimensional paths definition ap02 {A B : Type} (f:A → B) {x y : A} {p q : x ≈ y} (r : p ≈ q) : ap f p ≈ ap f q := -rec_on r idp +path.rec_on r idp definition ap02_pp {A B} (f : A → B) {x y : A} {p p' p'' : x ≈ y} (r : p ≈ p') (r' : p' ≈ p'') : ap02 f (r ⬝ r') ≈ ap02 f r ⬝ ap02 f r' := -rec_on r (rec_on r' idp) +path.rec_on r (path.rec_on r' idp) definition ap02_p2p {A B} (f : A→B) {x y z : A} {p p' : x ≈ y} {q q' :y ≈ z} (r : p ≈ p') (s : q ≈ q') : ap02 f (r ⬝⬝ s) ≈ ap_pp f p q ⬝ (ap02 f r ⬝⬝ ap02 f s) ⬝ (ap_pp f p' q')^ := -rec_on r (rec_on s (rec_on q (rec_on p idp))) +path.rec_on r (path.rec_on s (path.rec_on q (path.rec_on p idp))) definition apD02 {A : Type} {B : A → Type} {x y : A} {p q : x ≈ y} (f : Π x, B x) (r : p ≈ q) : apD f p ≈ transport2 B r (f x) ⬝ apD f q := -rec_on r (concat_1p _)^ +path.rec_on r (concat_1p _)^ end path