feat(init): add 'do' tactic

hott/init/equiv.hlean

@@ -39,10 +39,11 @@ namespace is_equiv
   variables {A B C : Type} (f : A → B) (g : B → C) {f' : A → B}
 
   -- The identity function is an equivalence.
+  -- TODO: make A explicit
   definition is_equiv_id : (@is_equiv A A id) := is_equiv.mk id (λa, idp) (λa, idp) (λa, idp)
 
   -- The composition of two equivalences is, again, an equivalence.
-  definition is_equiv_compose [Hf : is_equiv f] [Hg : is_equiv g] : (is_equiv (g ∘ f)) :=
+  definition is_equiv_compose [Hf : is_equiv f] [Hg : is_equiv g] : is_equiv (g ∘ f) :=
     is_equiv.mk ((inv f) ∘ (inv g))
                (λc, ap g (retr f (g⁻¹ c)) ⬝ retr g c)
                (λa, ap (inv f) (sect g (f a)) ⬝ sect f a)
@@ -244,7 +245,7 @@ namespace equiv
   protected definition trans (f : A ≃ B) (g: B ≃ C) : A ≃ C :=
   equiv.mk (g ∘ f) !is_equiv_compose
 
-  definition equiv_of_eq_of_equiv (f : A ≃ B) (f' : A → B) (Heq : f = f') : A ≃ B :=
+  definition equiv_of_eq_fn_of_equiv (f : A ≃ B) (f' : A → B) (Heq : f = f') : A ≃ B :=
   equiv.mk f' (is_equiv_eq_closed f Heq)
 
   definition eq_equiv_fn_eq (f : A → B) [H : is_equiv f] (a b : A) : (a = b) ≃ (f a = f b) :=
@@ -262,8 +263,13 @@ namespace equiv
 
   -- calc enviroment
   -- Note: Calculating with substitutions needs univalence
+  definition equiv_of_equiv_of_eq {A B C : Type} (p : A = B) (q : B ≃ C) : A ≃ C := p⁻¹ ▹ q
+  definition equiv_of_eq_of_equiv {A B C : Type} (p : A ≃ B) (q : B = C) : A ≃ C := q   ▹ p
+
   calc_trans equiv.trans
   calc_refl equiv.refl
   calc_symm equiv.symm
+  calc_trans equiv_of_equiv_of_eq
+  calc_trans equiv_of_eq_of_equiv
 
 end equiv

hott/init/num.hlean

@@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Module: init.num
 Authors: Leonardo de Moura
 -/
+
 prelude
 import init.logic init.bool
 open bool
@@ -119,12 +120,14 @@ namespace num
   notation a - b := sub a b
 end num
 
---- the coercion from num to nat is defined here, so that it can already be used in init.trunc
+-- the coercion from num to nat is defined here,
+-- so that it can already be used in init.trunc and init.tactic
 namespace nat
   definition add (a b : nat) : nat :=
   nat.rec_on b a (λ b₁ r, succ r)
 
   notation a + b := add a b
+
   definition of_num [coercion] (n : num) : nat :=
   num.rec zero
     (λ n, pos_num.rec (succ zero) (λ n r, r + r + (succ zero)) (λ n r, r + r) n) n

hott/init/tactic.hlean

@@ -12,7 +12,7 @@ definitions that are actually implemented in C++
 -/
 
 prelude
-import init.datatypes init.reserved_notation
+import init.datatypes init.reserved_notation init.num
 
 inductive tactic :
 Type := builtin : tactic
@@ -105,4 +105,7 @@ definition repeat1     (t : tactic) : tactic := t ; repeat t
 definition focus       (t : tactic) : tactic := focus_at t 0
 definition determ      (t : tactic) : tactic := at_most t 1
 
+definition do (n : num) (t : tactic) : tactic :=
+nat.rec id (λn t', (t;t')) (nat.of_num n)
+
 end tactic

library/init/nat.lean

@@ -6,7 +6,7 @@ Module: init.nat
 Authors: Floris van Doorn, Leonardo de Moura
 -/
 prelude
-import init.wf init.tactic
+import init.wf init.tactic init.num
 
 open eq.ops decidable
 
@@ -273,10 +273,7 @@ namespace nat
 
   notation a ≥ b := ge a b
 
-  definition add (a b : nat) : nat :=
+  -- add is defined in init.num
-  nat.rec_on b a (λ b₁ r, succ r)
-
-  notation a + b := add a b
 
   definition sub (a b : nat) : nat :=
   nat.rec_on b a (λ b₁ r, pred r)
@@ -334,8 +331,4 @@ namespace nat
     (le.refl a)
     (λ b₁ ih, le.trans !pred_le ih)
 
-  definition of_num [coercion] (n : num) : ℕ :=
-  num.rec zero
-    (λ n, pos_num.rec (succ zero) (λ n r, r + r + (succ zero)) (λ n r, r + r) n) n
 end nat
-attribute nat.of_num [reducible] -- of_num is also reducible if namespace "nat" is not opened

library/init/num.lean

@@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Module: init.num
 Authors: Leonardo de Moura
 -/
+
 prelude
 import init.logic init.bool
 open bool
@@ -118,3 +119,18 @@ namespace num
   notation a ≤ b := le a b
   notation a - b := sub a b
 end num
+
+-- the coercion from num to nat is defined here,
+-- so that it can already be used in init.tactic
+namespace nat
+
+  definition add (a b : nat) : nat :=
+  nat.rec_on b a (λ b₁ r, succ r)
+
+  notation a + b := add a b
+
+  definition of_num [coercion] (n : num) : nat :=
+  num.rec zero
+    (λ n, pos_num.rec (succ zero) (λ n r, r + r + (succ zero)) (λ n r, r + r) n) n
+end nat
+attribute nat.of_num [reducible] -- of_num is also reducible if namespace "nat" is not opened

library/init/tactic.lean

@@ -11,7 +11,7 @@ produces a term.  tactic.builtin is just a "dummy" for creating the
 definitions that are actually implemented in C++
 -/
 prelude
-import init.datatypes init.reserved_notation
+import init.datatypes init.reserved_notation init.num
 
 inductive tactic :
 Type := builtin : tactic
@@ -104,4 +104,7 @@ definition repeat1     (t : tactic) : tactic := t ; repeat t
 definition focus       (t : tactic) : tactic := focus_at t 0
 definition determ      (t : tactic) : tactic := at_most t 1
 
+definition do (n : num) (t : tactic) : tactic :=
+nat.rec id (λn t', (t;t')) (nat.of_num n)
+
 end tactic