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

feat(hott/init): add initialization files

Browse source
This commit is contained in:
Leonardo de Moura 2014-12-05 15:47:04 -08:00
parent d52fc83274
commit 1dc0790004
9 changed files with 720 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

25
hott/init/bool.hlean Normal file
View file

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

40
hott/init/datatypes.hlean
View file

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

3
hott/init/default.hlean
View file

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

341
hott/init/logic.hlean Normal file
View file

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

74
hott/init/num.hlean Normal file
View file

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

10
hott/init/priority.hlean Normal file
View file

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

40
hott/init/relation.hlean Normal file
View file

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

89
hott/init/reserved_notation.hlean Normal file
View file

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

100
hott/init/tactic.hlean Normal file
View file

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