From 1dc07900045240e117788460844ac4e2ab4fdaf1 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 5 Dec 2014 15:47:04 -0800
Subject: [PATCH] feat(hott/init): add initialization files

---
 hott/init/bool.hlean              |  25 +++
 hott/init/datatypes.hlean         |  40 +++-
 hott/init/default.hlean           |   3 +-
 hott/init/logic.hlean             | 341 ++++++++++++++++++++++++++++++
 hott/init/num.hlean               |  74 +++++++
 hott/init/priority.hlean          |  10 +
 hott/init/relation.hlean          |  40 ++++
 hott/init/reserved_notation.hlean |  89 ++++++++
 hott/init/tactic.hlean            | 100 +++++++++
 9 files changed, 720 insertions(+), 2 deletions(-)
 create mode 100644 hott/init/bool.hlean
 create mode 100644 hott/init/logic.hlean
 create mode 100644 hott/init/num.hlean
 create mode 100644 hott/init/priority.hlean
 create mode 100644 hott/init/relation.hlean
 create mode 100644 hott/init/reserved_notation.hlean
 create mode 100644 hott/init/tactic.hlean

diff --git a/hott/init/bool.hlean b/hott/init/bool.hlean
new file mode 100644
index 0000000000..51893d3e45
--- /dev/null
+++ b/hott/init/bool.hlean
@@ -0,0 +1,25 @@
+/-
+Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Leonardo de Moura
+-/
+prelude
+import init.datatypes init.reserved_notation
+
+namespace bool
+  definition cond {A : Type} (b : bool) (t e : A) :=
+  rec_on b e t
+
+  definition bor (a b : bool) :=
+  rec_on a (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)
+
+  notation a && b := band a b
+
+  definition bnot (a : bool) :=
+  rec_on a tt ff
+end bool
diff --git a/hott/init/datatypes.hlean b/hott/init/datatypes.hlean
index ccab2ba018..fec97587da 100644
--- a/hott/init/datatypes.hlean
+++ b/hott/init/datatypes.hlean
@@ -14,10 +14,48 @@ notation `Type₁` := Type.{1}
 notation `Type₂` := Type.{2}
 notation `Type₃` := Type.{3}
 
-inductive unit : Type :=
+inductive unit.{l} : Type.{l} :=
 star : unit
 
 inductive empty : Type
 
+inductive eq {A : Type} (a : A) : A → Type :=
+refl : eq a a
+
 structure prod (A B : Type) :=
 mk :: (pr1 : A) (pr2 : B)
+
+inductive sum (A B : Type) : Type :=
+inl {} : A → sum A B,
+inr {} : B → sum A B
+
+-- pos_num and num are two auxiliary datatypes used when parsing numerals such as 13, 0, 26.
+-- The parser will generate the terms (pos (bit1 (bit1 (bit0 one)))), zero, and (pos (bit0 (bit1 (bit1 one)))).
+-- This representation can be coerced in whatever we want (e.g., naturals, integers, reals, etc).
+inductive pos_num : Type :=
+one  : pos_num,
+bit1 : pos_num → pos_num,
+bit0 : pos_num → pos_num
+
+inductive num : Type :=
+zero  : num,
+pos   : pos_num → num
+
+inductive bool : Type :=
+ff : bool,
+tt : bool
+
+inductive char : Type :=
+mk : bool → bool → bool → bool → bool → bool → bool → bool → char
+
+inductive string : Type :=
+empty : string,
+str   : char → string → string
+
+inductive nat :=
+zero : nat,
+succ : nat → nat
+
+inductive option (A : Type) : Type :=
+none {} : option A,
+some    : A → option A
diff --git a/hott/init/default.hlean b/hott/init/default.hlean
index 981b2aaf0a..baec1ce6c8 100644
--- a/hott/init/default.hlean
+++ b/hott/init/default.hlean
@@ -5,4 +5,5 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import init.datatypes
+import init.datatypes init.reserved_notation init.tactic init.logic
+import init.bool init.num init.priority init.relation
diff --git a/hott/init/logic.hlean b/hott/init/logic.hlean
new file mode 100644
index 0000000000..f0117e6e82
--- /dev/null
+++ b/hott/init/logic.hlean
@@ -0,0 +1,341 @@
+/-
+Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Authors: Leonardo de Moura
+-/
+prelude
+import init.datatypes init.reserved_notation
+
+definition not (a : Type) := a → empty
+prefix `¬` := not
+
+definition absurd {a : Type} {b : Type} (H₁ : a) (H₂ : ¬a) : b :=
+empty.rec (λ e, b) (H₂ H₁)
+
+theorem mt {a b : Type} (H₁ : a → b) (H₂ : ¬b) : ¬a :=
+assume Ha : a, absurd (H₁ Ha) H₂
+
+-- not
+-- ---
+
+theorem not_empty : ¬ empty :=
+assume H : empty, H
+
+theorem not_not_intro {a : Type} (Ha : a) : ¬¬a :=
+assume Hna : ¬a, absurd Ha Hna
+
+theorem not_intro {a : Type} (H : a → empty) : ¬a := H
+
+theorem not_elim {a : Type} (H₁ : ¬a) (H₂ : a) : empty := H₁ H₂
+
+theorem not_implies_left {a b : Type} (H : ¬(a → b)) : ¬¬a :=
+assume Hna : ¬a, absurd (assume Ha : a, absurd Ha Hna) H
+
+theorem not_implies_right {a b : Type} (H : ¬(a → b)) : ¬b :=
+assume Hb : b, absurd (assume Ha : a, Hb) H
+
+-- eq
+-- --
+
+notation a = b := eq a b
+definition rfl {A : Type} {a : A} := eq.refl a
+
+namespace eq
+  variables {A : Type}
+  variables {a b c a': A}
+
+  theorem subst {P : A → Type} (H₁ : a = b) (H₂ : P a) : P b :=
+  rec H₂ H₁
+
+  theorem trans (H₁ : a = b) (H₂ : b = c) : a = c :=
+  subst H₂ H₁
+
+  definition symm (H : a = b) : b = a :=
+  subst H (refl a)
+
+  namespace ops
+    notation H `⁻¹` := symm H --input with \sy or \-1 or \inv
+    notation H1 ⬝ H2 := trans H1 H2
+    notation H1 ▸ H2 := subst H1 H2
+  end ops
+end eq
+
+calc_subst eq.subst
+calc_refl  eq.refl
+calc_trans eq.trans
+calc_symm  eq.symm
+
+-- ne
+-- --
+
+definition ne {A : Type} (a b : A) := ¬(a = b)
+notation a ≠ b := ne a b
+
+namespace ne
+  open eq.ops
+  variable {A : Type}
+  variables {a b : A}
+
+  theorem intro : (a = b → empty) → a ≠ b :=
+  assume H, H
+
+  theorem elim : a ≠ b → a = b → empty :=
+  assume H₁ H₂, H₁ H₂
+
+  theorem irrefl : a ≠ a → empty :=
+  assume H, H rfl
+
+  theorem symm : a ≠ b → b ≠ a :=
+  assume (H : a ≠ b) (H₁ : b = a), H (H₁⁻¹)
+end ne
+
+section
+  open eq.ops
+  variables {A : Type} {a b c : A}
+
+  theorem false.of_ne : a ≠ a → empty :=
+  assume H, H rfl
+
+  theorem ne.of_eq_of_ne : a = b → b ≠ c → a ≠ c :=
+  assume H₁ H₂, H₁⁻¹ ▸ H₂
+
+  theorem ne.of_ne_of_eq : a ≠ b → b = c → a ≠ c :=
+  assume H₁ H₂, H₂ ▸ H₁
+end
+
+calc_trans ne.of_eq_of_ne
+calc_trans ne.of_ne_of_eq
+
+-- iff
+-- ---
+
+definition iff (a b : Type) := prod (a → b) (b → a)
+
+notation a <-> b := iff a b
+notation a ↔ b := iff a b
+
+namespace iff
+  variables {a b c : Type}
+
+  definition def : (a ↔ b) = (prod (a → b) (b → a)) :=
+  rfl
+
+  definition intro (H₁ : a → b) (H₂ : b → a) : a ↔ b :=
+  prod.mk H₁ H₂
+
+  definition elim (H₁ : (a → b) → (b → a) → c) (H₂ : a ↔ b) : c :=
+  prod.rec H₁ H₂
+
+  definition elim_left (H : a ↔ b) : a → b :=
+  elim (assume H₁ H₂, H₁) H
+
+  definition mp := @elim_left
+
+  definition elim_right (H : a ↔ b) : b → a :=
+  elim (assume H₁ H₂, H₂) H
+
+  definition flip_sign (H₁ : a ↔ b) : ¬a ↔ ¬b :=
+  intro
+    (assume Hna, mt (elim_right H₁) Hna)
+    (assume Hnb, mt (elim_left H₁) Hnb)
+
+  definition refl (a : Type) : a ↔ a :=
+  intro (assume H, H) (assume H, H)
+
+  definition rfl {a : Type} : a ↔ a :=
+  refl a
+
+  theorem trans (H₁ : a ↔ b) (H₂ : b ↔ c) : a ↔ c :=
+  intro
+    (assume Ha, elim_left H₂ (elim_left H₁ Ha))
+    (assume Hc, elim_right H₁ (elim_right H₂ Hc))
+
+  theorem symm (H : a ↔ b) : b ↔ a :=
+  intro
+    (assume Hb, elim_right H Hb)
+    (assume Ha, elim_left H Ha)
+
+  theorem true_elim (H : a ↔ unit) : a :=
+  mp (symm H) unit.star
+
+  theorem false_elim (H : a ↔ empty) : ¬a :=
+  assume Ha : a, mp H Ha
+
+  open eq.ops
+  theorem of_eq {a b : Type} (H : a = b) : a ↔ b :=
+  iff.intro (λ Ha, H ▸ Ha) (λ Hb, H⁻¹ ▸ Hb)
+end iff
+
+calc_refl iff.refl
+calc_trans iff.trans
+
+-- inhabited
+-- ---------
+
+inductive inhabited [class] (A : Type) : Type :=
+mk : A → inhabited A
+
+namespace inhabited
+
+protected definition destruct {A : Type} {B : Type} (H1 : inhabited A) (H2 : A → B) : B :=
+inhabited.rec H2 H1
+
+definition fun_inhabited [instance] (A : Type) {B : Type} (H : inhabited B) : inhabited (A → B) :=
+destruct H (λb, mk (λa, b))
+
+definition dfun_inhabited [instance] (A : Type) {B : A → Type} (H : Πx, inhabited (B x)) :
+  inhabited (Πx, B x) :=
+mk (λa, destruct (H a) (λb, b))
+
+definition default (A : Type) [H : inhabited A] : A := destruct H (take a, a)
+
+end inhabited
+
+-- decidable
+-- ---------
+
+inductive decidable [class] (p : Type) : Type :=
+inl :  p → decidable p,
+inr : ¬p → decidable p
+
+namespace decidable
+  variables {p q : Type}
+
+  definition pos_witness [C : decidable p] (H : p) : p :=
+  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)
+
+  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)
+
+  theorem em (p : Type) [H : decidable p] : sum p ¬p :=
+  by_cases (λ Hp, sum.inl Hp) (λ Hnp, sum.inr Hnp)
+
+  theorem by_contradiction [Hp : decidable p] (H : ¬p → empty) : p :=
+  by_cases
+    (assume H₁ : p, H₁)
+    (assume H₁ : ¬p, empty.rec (λ e, p) (H H₁))
+
+  definition decidable_iff_equiv (Hp : decidable p) (H : p ↔ q) : decidable q :=
+  rec_on Hp
+    (assume Hp : p,   inl (iff.elim_left H Hp))
+    (assume Hnp : ¬p, inr (iff.elim_left (iff.flip_sign H) Hnp))
+
+  definition decidable_eq_equiv.{l} {p q : Type.{l}} (Hp : decidable p) (H : p = q) : decidable q :=
+  decidable_iff_equiv Hp (iff.of_eq H)
+end decidable
+
+section
+  variables {p q : Type}
+  open decidable (rec_on inl inr)
+
+  definition unit.decidable [instance] : decidable unit :=
+  inl unit.star
+
+  definition empty.decidable [instance] : decidable empty :=
+  inr not_empty
+
+  definition prod.decidable [instance] (Hp : decidable p) (Hq : decidable q) : decidable (prod p q) :=
+  rec_on Hp
+    (assume Hp  : p, rec_on Hq
+      (assume Hq  : q,  inl (prod.mk Hp Hq))
+      (assume Hnq : ¬q, inr (λ H : prod p q, prod.rec_on H (λ Hp Hq, absurd Hq Hnq))))
+    (assume Hnp : ¬p, inr (λ H : prod p q, prod.rec_on H (λ Hp Hq, absurd Hp Hnp)))
+
+  definition sum.decidable [instance] (Hp : decidable p) (Hq : decidable q) : decidable (sum p q) :=
+  rec_on Hp
+    (assume Hp  : p, inl (sum.inl Hp))
+    (assume Hnp : ¬p, rec_on Hq
+      (assume Hq  : q,  inl (sum.inr Hq))
+      (assume Hnq : ¬q, inr (λ H : sum p q, sum.rec_on H (λ Hp, absurd Hp Hnp) (λ Hq, absurd Hq Hnq))))
+
+  definition not.decidable [instance] (Hp : decidable p) : decidable (¬p) :=
+  rec_on Hp
+    (assume Hp,  inr (not_not_intro Hp))
+    (assume Hnp, inl Hnp)
+
+  definition implies.decidable [instance] (Hp : decidable p) (Hq : decidable q) : decidable (p → q) :=
+  rec_on Hp
+    (assume Hp  : p, rec_on Hq
+      (assume Hq  : q,  inl (assume H, Hq))
+      (assume Hnq : ¬q, inr (assume H : p → q, absurd (H Hp) Hnq)))
+    (assume Hnp : ¬p, inl (assume Hp, absurd Hp Hnp))
+
+  definition iff.decidable [instance] (Hp : decidable p) (Hq : decidable q) : decidable (p ↔ q) := _
+end
+
+definition decidable_pred {A : Type} (R : A   →   Type) := Π (a   : A), decidable (R a)
+definition decidable_rel  {A : Type} (R : A → A → Type) := Π (a b : A), decidable (R a b)
+definition decidable_eq   (A : Type) := decidable_rel (@eq A)
+
+definition ite (c : Type) [H : decidable c] {A : Type} (t e : A) : A :=
+decidable.rec_on H (λ Hc, t) (λ Hnc, e)
+
+definition if_pos {c : Type} [H : decidable c] (Hc : c) {A : Type} {t e : A} : (if c then t else e) = t :=
+decidable.rec
+  (λ Hc : c,    eq.refl (@ite c (decidable.inl Hc) A t e))
+  (λ Hnc : ¬c,  absurd Hc Hnc)
+  H
+
+definition if_neg {c : Type} [H : decidable c] (Hnc : ¬c) {A : Type} {t e : A} : (if c then t else e) = e :=
+decidable.rec
+  (λ Hc : c,    absurd Hc Hnc)
+  (λ Hnc : ¬c,  eq.refl (@ite c (decidable.inr Hnc) A t e))
+  H
+
+definition if_t_t (c : Type) [H : decidable c] {A : Type} (t : A) : (if c then t else t) = t :=
+decidable.rec
+  (λ Hc  : c,  eq.refl (@ite c (decidable.inl Hc)  A t t))
+  (λ Hnc : ¬c, eq.refl (@ite c (decidable.inr Hnc) A t t))
+  H
+
+definition if_unit {A : Type} (t e : A) : (if unit then t else e) = t :=
+if_pos unit.star
+
+definition if_empty {A : Type} (t e : A) : (if empty then t else e) = e :=
+if_neg not_empty
+
+theorem if_cond_congr {c₁ c₂ : Type} [H₁ : decidable c₁] [H₂ : decidable c₂] (Heq : c₁ ↔ c₂) {A : Type} (t e : A)
+                      : (if c₁ then t else e) = (if c₂ then t else e) :=
+decidable.rec_on H₁
+ (λ Hc₁  : c₁,  decidable.rec_on H₂
+   (λ Hc₂  : c₂,  if_pos Hc₁ ⬝ (if_pos Hc₂)⁻¹)
+   (λ Hnc₂ : ¬c₂, absurd (iff.elim_left Heq Hc₁) Hnc₂))
+ (λ Hnc₁ : ¬c₁, decidable.rec_on H₂
+   (λ Hc₂  : c₂,  absurd (iff.elim_right Heq Hc₂) Hnc₁)
+   (λ Hnc₂ : ¬c₂, if_neg Hnc₁ ⬝ (if_neg Hnc₂)⁻¹))
+
+theorem if_congr_aux {c₁ c₂ : Type} [H₁ : decidable c₁] [H₂ : decidable c₂] {A : Type} {t₁ t₂ e₁ e₂ : A}
+                     (Hc : c₁ ↔ c₂) (Ht : t₁ = t₂) (He : e₁ = e₂) :
+                 (if c₁ then t₁ else e₁) = (if c₂ then t₂ else e₂) :=
+Ht ▸ He ▸ (if_cond_congr Hc t₁ e₁)
+
+theorem if_congr {c₁ c₂ : Type} [H₁ : decidable c₁] {A : Type} {t₁ t₂ e₁ e₂ : A} (Hc : c₁ ↔ c₂) (Ht : t₁ = t₂) (He : e₁ = e₂) :
+                 (if c₁ then t₁ else e₁) = (@ite c₂ (decidable.decidable_iff_equiv H₁ Hc) A t₂ e₂) :=
+have H2 [visible] : decidable c₂, from (decidable.decidable_iff_equiv H₁ Hc),
+if_congr_aux Hc Ht He
+
+
+-- We use "dependent" if-then-else to be able to communicate the if-then-else condition
+-- to the branches
+definition dite (c : Type) [H : decidable c] {A : Type} (t : c → A) (e : ¬ c → A) : A :=
+decidable.rec_on H (λ Hc, t Hc) (λ Hnc, e Hnc)
+
+definition dif_pos {c : Type} [H : decidable c] (Hc : c) {A : Type} {t : c → A} {e : ¬ c → A} : (if H : c then t H else e H) = t (decidable.pos_witness Hc) :=
+decidable.rec
+  (λ Hc : c,    eq.refl (@dite c (decidable.inl Hc) A t e))
+  (λ Hnc : ¬c,  absurd Hc Hnc)
+  H
+
+definition dif_neg {c : Type} [H : decidable c] (Hnc : ¬c) {A : Type} {t : c → A} {e : ¬ c → A} : (if H : c then t H else e H) = e (decidable.neg_witness Hnc) :=
+decidable.rec
+  (λ Hc : c,    absurd Hc Hnc)
+  (λ Hnc : ¬c,  eq.refl (@dite c (decidable.inr Hnc) A t e))
+  H
+
+-- Remark: dite and ite are "definitionally equal" when we ignore the proofs.
+theorem dite_ite_eq (c : Type) [H : decidable c] {A : Type} (t : A) (e : A) : dite c (λh, t) (λh, e) = ite c t e :=
+rfl
diff --git a/hott/init/num.hlean b/hott/init/num.hlean
new file mode 100644
index 0000000000..a3eed88bcd
--- /dev/null
+++ b/hott/init/num.hlean
@@ -0,0 +1,74 @@
+/-
+Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Authors: Leonardo de Moura
+-/
+prelude
+import init.logic init.bool
+open bool
+
+definition pos_num.is_inhabited [instance] : inhabited pos_num :=
+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)
+
+  definition is_one (a : pos_num) : bool :=
+  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))
+
+  definition size (a : pos_num) : 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
+    succ
+    (λn f b, rec_on b
+      (succ (bit1 n))
+      (λm r, succ (bit1 (f m)))
+      (λm r, bit1 (f m)))
+    (λn f b, rec_on b
+      (bit1 n)
+      (λm r, bit1 (f m))
+      (λm r, bit0 (f m)))
+    b
+
+  notation a + b := add a b
+
+  definition mul (a b : pos_num) : pos_num :=
+  rec_on a
+    b
+    (λn r, bit0 r + b)
+    (λn r, bit0 r)
+
+  notation a * b := mul a b
+
+end pos_num
+
+definition num.is_inhabited [instance] : inhabited num :=
+inhabited.mk num.zero
+
+namespace num
+  open pos_num
+  definition succ (a : num) : 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)))
+
+  definition size (a : num) : 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)))
+
+  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)))
+
+  notation a + b := add a b
+  notation a * b := mul a b
+end num
diff --git a/hott/init/priority.hlean b/hott/init/priority.hlean
new file mode 100644
index 0000000000..8a23b06957
--- /dev/null
+++ b/hott/init/priority.hlean
@@ -0,0 +1,10 @@
+/-
+Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Authors: Leonardo de Moura
+-/
+prelude
+import init.datatypes
+definition std.priority.default : num := 1000
+definition std.priority.max     : num := 4294967295
diff --git a/hott/init/relation.hlean b/hott/init/relation.hlean
new file mode 100644
index 0000000000..29935d81f7
--- /dev/null
+++ b/hott/init/relation.hlean
@@ -0,0 +1,40 @@
+/-
+Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import init.logic
+
+-- TODO(Leo): remove duplication between this file and algebra/relation.lean
+-- We need some of the following definitions asap when "initializing" Lean.
+
+variables {A B : Type} (R : B → B → Type)
+infix [local] `≺`:50 := R
+
+definition reflexive := ∀x, x ≺ x
+
+definition symmetric := ∀⦃x y⦄, x ≺ y → y ≺ x
+
+definition transitive := ∀⦃x y z⦄, x ≺ y → y ≺ z → x ≺ z
+
+definition irreflexive := ∀x, ¬ x ≺ x
+
+definition anti_symmetric := ∀⦃x y⦄, x ≺ y → y ≺ x → x = y
+
+definition empty_relation := λa₁ a₂ : A, empty
+
+definition subrelation (Q R : B → B → Type) := ∀⦃x y⦄, Q x y → R x y
+
+definition inv_image (f : A → B) : A → A → Type :=
+λa₁ a₂, f a₁ ≺ f a₂
+
+theorem inv_image.trans (f : A → B) (H : transitive R) : transitive (inv_image R f) :=
+λ (a₁ a₂ a₃ : A) (H₁ : inv_image R f a₁ a₂) (H₂ : inv_image R f a₂ a₃), H H₁ H₂
+
+theorem inv_image.irreflexive (f : A → B) (H : irreflexive R) : irreflexive (inv_image R f) :=
+λ (a : A) (H₁ : inv_image R f a a), H (f a) H₁
+
+inductive tc {A : Type} (R : A → A → Type) : A → A → Type :=
+base  : ∀a b, R a b → tc R a b,
+trans : ∀a b c, tc R a b → tc R b c → tc R a c
diff --git a/hott/init/reserved_notation.hlean b/hott/init/reserved_notation.hlean
new file mode 100644
index 0000000000..4f7d4651ae
--- /dev/null
+++ b/hott/init/reserved_notation.hlean
@@ -0,0 +1,89 @@
+/-
+Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Authors: Leonardo de Moura
+
+Basic datatypes
+-/
+prelude
+import init.datatypes
+
+notation `assume` binders `,` r:(scoped f, f) := r
+notation `take`   binders `,` r:(scoped f, f) := r
+
+/-
+  Global declarations of right binding strength
+
+  If a module reassigns these, it will be incompatible with other modules that adhere to these
+  conventions.
+
+  When hovering over a symbol, use "C-u C-x =" to see how to input it.
+-/
+
+/- Logical operations and relations -/
+
+definition std.prec.max   : num := 1024 -- reflects max precedence used internally
+definition std.prec.arrow : num := 25
+
+reserve prefix `¬`:40
+reserve prefix `~`:40
+reserve infixr `∧`:35
+reserve infixr `/\`:35
+reserve infixr `\/`:30
+reserve infixr `∨`:30
+reserve infix `<->`:25
+reserve infix `↔`:25
+reserve infix `=`:50
+reserve infix `≠`:50
+reserve infix `≈`:50
+reserve infix `∼`:50
+
+reserve infixr `∘`:60      -- input with \comp
+reserve postfix `⁻¹`:100  --input with \sy or \-1 or \inv
+reserve infixl `⬝`:75
+reserve infixr `▸`:75
+
+/- types and type constructors -/
+
+reserve infixl `⊎`:25
+reserve infixl `×`:30
+
+/- arithmetic operations -/
+
+reserve infixl `+`:65
+reserve infixl `-`:65
+reserve infixl `*`:70
+reserve infixl `div`:70
+reserve infixl `mod`:70
+reserve prefix `-`:100
+
+reserve infix `<=`:50
+reserve infix `≤`:50
+reserve infix `<`:50
+reserve infix `>=`:50
+reserve infix `≥`:50
+reserve infix `>`:50
+
+/- boolean operations -/
+
+reserve infixl `&&`:70
+reserve infixl `||`:65
+
+/- set operations -/
+
+reserve infix `∈`:50
+reserve infixl `∩`:70
+reserve infixl `∪`:65
+
+/- other symbols -/
+
+precedence `|`:55
+reserve notation | a:55 |
+reserve infixl `++`:65
+reserve infixr `::`:65
+
+-- Yet another trick to anotate an expression with a type
+definition is_typeof (A : Type) (a : A) : A := a
+
+notation `typeof` t `:` T  := is_typeof T t
diff --git a/hott/init/tactic.hlean b/hott/init/tactic.hlean
new file mode 100644
index 0000000000..27be915884
--- /dev/null
+++ b/hott/init/tactic.hlean
@@ -0,0 +1,100 @@
+/-
+Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+
+This is just a trick to embed the 'tactic language' as a Lean
+expression. We should view 'tactic' as automation that when execute
+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
+
+inductive tactic :
+Type := builtin : tactic
+
+namespace tactic
+-- Remark the following names are not arbitrary, the tactic module
+-- uses them when converting Lean expressions into actual tactic objects.
+-- The bultin 'by' construct triggers the process of converting a
+-- a term of type 'tactic' into a tactic that sythesizes a term
+opaque definition and_then    (t1 t2 : tactic) : tactic := builtin
+opaque definition or_else     (t1 t2 : tactic) : tactic := builtin
+opaque definition append      (t1 t2 : tactic) : tactic := builtin
+opaque definition interleave  (t1 t2 : tactic) : tactic := builtin
+opaque definition par         (t1 t2 : tactic) : tactic := builtin
+opaque definition fixpoint    (f : tactic → tactic) : tactic := builtin
+opaque definition repeat      (t : tactic) : tactic := builtin
+opaque definition at_most     (t : tactic) (k : num)  : tactic := builtin
+opaque definition discard     (t : tactic) (k : num)  : tactic := builtin
+opaque definition focus_at    (t : tactic) (i : num)  : tactic := builtin
+opaque definition try_for     (t : tactic) (ms : num) : tactic := builtin
+opaque definition now         : tactic := builtin
+opaque definition assumption  : tactic := builtin
+opaque definition eassumption : tactic := builtin
+opaque definition state       : tactic := builtin
+opaque definition fail        : tactic := builtin
+opaque definition id          : tactic := builtin
+opaque definition beta        : tactic := builtin
+opaque definition info        : tactic := builtin
+opaque definition whnf        : tactic := builtin
+opaque definition rotate_left (k : num) := builtin
+opaque definition rotate_right (k : num) := builtin
+definition rotate (k : num) := rotate_left k
+
+-- This is just a trick to embed expressions into tactics.
+-- The nested expressions are "raw". They tactic should
+-- elaborate them when it is executed.
+inductive expr : Type :=
+builtin : expr
+
+opaque definition apply      (e : expr)   : tactic := builtin
+opaque definition rapply     (e : expr)   : tactic := builtin
+opaque definition fapply     (e : expr)   : tactic := builtin
+opaque definition rename     (a b : expr) : tactic := builtin
+opaque definition intro      (e : expr)   : tactic := builtin
+opaque definition generalize (e : expr)   : tactic := builtin
+opaque definition clear      (e : expr)   : tactic := builtin
+opaque definition revert     (e : expr)   : tactic := builtin
+opaque definition unfold     (e : expr)   : tactic := builtin
+opaque definition exact      (e : expr)   : tactic := builtin
+opaque definition trace      (s : string) : tactic := builtin
+opaque definition inversion  (id : expr)  : tactic := builtin
+
+notation a `↦` b:max := rename a b
+
+inductive expr_list : Type :=
+nil  : expr_list,
+cons : expr → expr_list → expr_list
+
+opaque definition inversion_with  (id : expr) (ids : expr_list) : tactic := builtin
+notation `cases` a:max := inversion a
+notation `cases` a:max `with` `(` l:(foldr `,` (h t, expr_list.cons h t) expr_list.nil) `)` := inversion_with a l
+
+opaque definition intro_lst (ids : expr_list) : tactic := builtin
+notation `intros`   := intro_lst expr_list.nil
+notation `intros` `(` l:(foldr `,` (h t, expr_list.cons h t) expr_list.nil) `)` := intro_lst l
+
+opaque definition generalize_lst (es : expr_list) : tactic := builtin
+notation `generalizes` `(` l:(foldr `,` (h t, expr_list.cons h t) expr_list.nil) `)` := generalize_lst l
+
+opaque definition clear_lst  (ids : expr_list) : tactic := builtin
+notation `clears` `(` l:(foldr `,` (h t, expr_list.cons h t) expr_list.nil) `)` := clear_lst l
+
+opaque definition revert_lst (ids : expr_list) : tactic := builtin
+notation `reverts` `(` l:(foldr `,` (h t, expr_list.cons h t) expr_list.nil) `)` := revert_lst l
+
+opaque definition assert_hypothesis (id : expr) (e : expr) : tactic := builtin
+notation `assert` `(` id `:` ty `)` := assert_hypothesis id ty
+
+infixl `;`:15 := and_then
+notation `[` h:10 `|`:10 r:(foldl:10 `|` (e r, or_else r e) h) `]` := r
+
+definition try         (t : tactic) : tactic := [t | id]
+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
+
+end tactic