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

refactor(library): add 'init' folder

Browse source
This commit is contained in:
Leonardo de Moura 2014-11-30 20:34:12 -08:00
parent 8dfd22e66c
commit 697d4359e3
73 changed files with 913 additions and 973 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
library/algebra/function.lean
View file

@ -7,9 +7,6 @@ Author: Leonardo de Moura
General operations on functions.
-/
import general_notation
namespace function
variables {A : Type} {B : Type} {C : Type} {D : Type} {E : Type}

3
library/algebra/group.lean
View file

@ -8,8 +8,7 @@ Authors: Jeremy Avigad, Leonardo de Moura
Various multiplicative and additive structures. Partially modeled on Isabelle's library.
-/
import logic.eq logic.connectives
import data.unit data.sigma data.prod
import logic.eq data.unit data.sigma data.prod
import algebra.function algebra.binary
open eq eq.ops -- note: ⁻¹ will be overloaded

2
library/algebra/order.lean
View file

@ -15,7 +15,7 @@ These might not hold constructively in some applications, but we can define addi
with both < and ≤ as needed.
-/
import logic.eq logic.connectives
import logic.eq
import data.unit data.sigma data.prod
import algebra.function algebra.binary

3
library/algebra/ordered_group.lean
View file

@ -9,8 +9,7 @@ Partially ordered additive groups. Modeled on Isabelle's library. The comments b
we could refine the structures, though we would have to declare more inheritance paths.
-/
import logic.eq logic.connectives
import data.unit data.sigma data.prod
import logic.eq data.unit data.sigma data.prod
import algebra.function algebra.binary
import algebra.group algebra.order

2
library/algebra/relation.lean
View file

@ -8,8 +8,6 @@ Author: Jeremy Avigad
General properties of relations, and classes for equivalence relations and congruences.
-/
import logic.prop
namespace relation
/- properties of binary relations -/

3
library/algebra/ring.lean
View file

@ -9,8 +9,7 @@ Structures with multiplicative and additive components, including semirings, rin
The development is modeled after Isabelle's library.
-/
import logic.eq logic.connectives
import data.unit data.sigma data.prod
import logic.eq data.unit data.sigma data.prod
import algebra.function algebra.binary algebra.group
open eq eq.ops

8
library/data/bool/decl.lean
View file

@ -1,8 +0,0 @@
-- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
-- Released under Apache 2.0 license as described in the file LICENSE.
-- Author: Leonardo de Moura
import data.unit.decl
inductive bool : Type :=
ff : bool,
tt : bool

2
library/data/bool/default.lean
View file

@ -1,4 +1,4 @@
-- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
-- Released under Apache 2.0 license as described in the file LICENSE.
-- Author: Leonardo de Moura
import data.bool.decl data.bool.ops data.bool.thms
import data.bool.thms

4
library/data/bool/thms.lean
View file

@ -1,9 +1,7 @@
-- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
-- Released under Apache 2.0 license as described in the file LICENSE.
-- Author: Leonardo de Moura
import data.bool.ops
import logic.connectives logic.decidable logic.inhabited
import logic.eq
open eq eq.ops decidable
namespace bool

8
library/data/empty.lean
View file

@ -4,10 +4,7 @@
-- Empty type
-- ----------
import logic.cast
inductive empty : Type
import logic.cast logic.subsingleton
namespace empty
protected theorem elim (A : Type) (H : empty) : A :=
@ -17,6 +14,9 @@ namespace empty
subsingleton.intro (λ a b, !elim a)
end empty
protected definition empty.has_decidable_eq [instance] : decidable_eq empty :=
take (a b : empty), decidable.inl (!empty.elim a)
definition tneg.tneg (A : Type) := A → empty
prefix `~` := tneg.tneg
namespace tneg

2
library/data/int/basic.lean
View file

@ -7,7 +7,7 @@
-- The integers, with addition, multiplication, and subtraction.
import data.nat.basic data.nat.order data.nat.sub data.prod data.quotient tools.tactic algebra.relation
import data.nat.basic data.nat.order data.nat.sub data.prod data.quotient algebra.relation
import algebra.binary
import tools.fake_simplifier

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

@ -3,7 +3,7 @@
--- Released under Apache 2.0 license as described in the file LICENSE.
--- Authors: Parikshit Khanna, Jeremy Avigad, Leonardo de Moura
----------------------------------------------------------------------------------------------------
import logic tools.helper_tactics tools.tactic data.nat.basic
import logic tools.helper_tactics data.nat.basic
-- Theory list
-- ===========

2
library/data/nat/basic.lean
View file

@ -4,7 +4,7 @@
-- Basic operations on the natural numbers.
import .decl data.num algebra.binary
import data.num algebra.binary
open eq.ops binary

2
library/data/nat/div.lean
View file

@ -8,7 +8,7 @@
-- This is a continuation of the development of the natural numbers, with a general way of
-- defining recursive functions, and definitions of div, mod, and gcd.
import data.nat.sub logic data.prod.wf
import data.nat.sub logic
import algebra.relation
import tools.fake_simplifier

17
library/data/num/decl.lean
View file

@ -1,17 +0,0 @@
----------------------------------------------------------------------------------------------------
-- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
-- Released under Apache 2.0 license as described in the file LICENSE.
-- Author: Leonardo de Moura
----------------------------------------------------------------------------------------------------
import data.unit.decl
-- 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

2
library/data/num/default.lean
View file

@ -3,4 +3,4 @@
-- Released under Apache 2.0 license as described in the file LICENSE.
-- Author: Leonardo de Moura
----------------------------------------------------------------------------------------------------
import data.num.decl data.num.ops data.num.thms
import data.num.thms

2
library/data/num/thms.lean
View file

@ -3,7 +3,7 @@
-- Released under Apache 2.0 license as described in the file LICENSE.
-- Author: Leonardo de Moura
----------------------------------------------------------------------------------------------------
import data.num.ops logic.eq
import logic.eq
open bool
namespace pos_num

4
library/data/option.lean
View file

@ -1,7 +1,7 @@
-- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
-- Released under Apache 2.0 license as described in the file LICENSE.
-- Author: Leonardo de Moura
import logic.eq logic.inhabited logic.decidable
import logic.eq
open eq.ops decidable
inductive option (A : Type) : Type :=
@ -16,7 +16,7 @@ namespace option
trivial
theorem not_is_none_some {A : Type} (a : A) : ¬ is_none (some a) :=
not_false_trivial
not_false
theorem none_ne_some {A : Type} (a : A) : none ≠ some a :=
assume H, no_confusion H

29
library/data/prod/decl.lean
View file

@ -1,29 +0,0 @@
/-
Copyright (c) 2014 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Module: data.prod.decl
Author: Leonardo de Moura, Jeremy Avigad
-/
import data.unit.decl logic.eq
structure prod (A B : Type) :=
mk :: (pr1 : A) (pr2 : B)
definition pair := @prod.mk
namespace prod
notation A * B := prod A B
notation A × B := prod A B
namespace low_precedence_times
reserve infixr `*`:30 -- conflicts with notation for multiplication
infixr `*` := prod
end low_precedence_times
notation `pr₁` := pr1
notation `pr₂` := pr2
-- notation for n-ary tuples
notation `(` h `,` t:(foldl `,` (e r, prod.mk r e) h) `)` := t
end prod

2
library/data/prod/default.lean
View file

@ -1,4 +1,4 @@
-- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
-- Released under Apache 2.0 license as described in the file LICENSE.
-- Author: Leonardo de Moura, Jeremy Avigad
import data.prod.decl data.prod.thms data.prod.wf
import data.prod.thms

3
library/data/prod/thms.lean
View file

@ -1,8 +1,7 @@
-- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
-- Released under Apache 2.0 license as described in the file LICENSE.
-- Author: Leonardo de Moura, Jeremy Avigad
import data.prod.decl logic.inhabited logic.eq logic.decidable
import logic.eq
open inhabited decidable eq.ops
namespace prod

2
library/data/quotient/basic.lean
View file

@ -5,7 +5,7 @@
-- Theory data.quotient
-- ====================
import logic tools.tactic data.subtype logic.cast algebra.relation data.prod
import logic data.subtype logic.cast algebra.relation data.prod
import logic.instances
import .util

3
library/data/quotient/classical.lean
View file

@ -2,8 +2,7 @@
-- Released under Apache 2.0 license as described in the file LICENSE.
-- Author: Floris van Doorn
import algebra.relation logic.nonempty data.subtype
import logic.axioms.classical logic.axioms.hilbert logic.axioms.funext
import algebra.relation data.subtype logic.axioms.classical logic.axioms.hilbert logic.axioms.funext
import .basic
namespace quotient

21
library/data/sigma/decl.lean
View file

@ -1,21 +0,0 @@
-- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
-- Released under Apache 2.0 license as described in the file LICENSE.
-- Author: Leonardo de Moura, Jeremy Avigad, Floris van Doorn
import logic.eq logic.heq data.unit data.num.ops
structure sigma {A : Type} (B : A → Type) :=
dpair :: (dpr1 : A) (dpr2 : B dpr1)
notation `Σ` binders `,` r:(scoped P, sigma P) := r
namespace sigma
notation `dpr₁` := dpr1
notation `dpr₂` := dpr2
namespace ops
postfix `.1`:(max+1) := dpr1
postfix `.2`:(max+1) := dpr2
notation `⟨` t:(foldr `,` (e r, sigma.dpair e r)) `⟩`:0 := t --input ⟨ ⟩ as \< \>
end ops
end sigma

2
library/data/sigma/default.lean
View file

@ -1,4 +1,4 @@
-- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
-- Released under Apache 2.0 license as described in the file LICENSE.
-- Author: Leonardo de Moura, Jeremy Avigad, Floris van Doorn
import data.sigma.decl data.sigma.thms data.sigma.wf
import data.sigma.thms

2
library/data/sigma/thms.lean
View file

@ -1,7 +1,7 @@
-- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
-- Released under Apache 2.0 license as described in the file LICENSE.
-- Author: Leonardo de Moura, Jeremy Avigad, Floris van Doorn
import data.sigma.decl
import logic.cast
open inhabited eq.ops sigma.ops
namespace sigma

11
library/data/string/decl.lean
View file

@ -1,11 +0,0 @@
-- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
-- Released under Apache 2.0 license as described in the file LICENSE.
-- Author: Leonardo de Moura
import data.bool.decl
inductive char : Type :=
mk : bool → bool → bool → bool → bool → bool → bool → bool → char
inductive string : Type :=
empty : string,
str : char → string → string

2
library/data/string/default.lean
View file

@ -1,4 +1,4 @@
-- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
-- Released under Apache 2.0 license as described in the file LICENSE.
-- Author: Leonardo de Moura
import data.string.decl data.string.thms
import data.string.thms

2
library/data/string/thms.lean
View file

@ -1,7 +1,7 @@
-- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
-- Released under Apache 2.0 license as described in the file LICENSE.
-- Author: Leonardo de Moura
import data.string.decl data.bool
import data.bool
open bool inhabited
namespace char

3
library/data/subtype.lean
View file

@ -1,9 +1,6 @@
-- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
-- Released under Apache 2.0 license as described in the file LICENSE.
-- Author: Leonardo de Moura, Jeremy Avigad
import logic.inhabited logic.eq logic.decidable
open decidable
structure subtype {A : Type} (P : A → Prop) :=

6
library/data/sum.lean
View file

@ -7,14 +7,8 @@ Authors: Leonardo de Moura, Jeremy Avigad
The sum type, aka disjoint union.
-/
import logic.prop logic.inhabited logic.decidable
open inhabited decidable eq.ops
inductive sum (A B : Type) : Type :=
inl : A → sum A B,
inr : B → sum A B
namespace sum
notation A ⊎ B := sum A B
notation A + B := sum A B

5
library/data/unit/basic.lean
View file

@ -1,5 +0,0 @@
-- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
-- Released under Apache 2.0 license as described in the file LICENSE.
-- Author: Leonardo de Moura
inductive unit.{l} : Type.{l} :=
star : unit

9
library/data/unit/decl.lean
View file

@ -1,9 +0,0 @@
-- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
-- Released under Apache 2.0 license as described in the file LICENSE.
-- Author: Leonardo de Moura
inductive unit.{l} : Type.{l} :=
star : unit
namespace unit
notation `⋆` := star
end unit

5
library/data/unit/default.lean
View file

@ -1,4 +1,7 @@
-- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
-- Released under Apache 2.0 license as described in the file LICENSE.
-- Author: Leonardo de Moura
import data.unit.decl data.unit.thms data.unit.insts
import data.unit.thms data.unit.insts
namespace unit
notation `⋆` := star
end unit

4
library/data/unit/insts.lean
View file

@ -1,7 +1,7 @@
-- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
-- Released under Apache 2.0 license as described in the file LICENSE.
-- Author: Leonardo de Moura
import data.unit.decl data.unit.thms logic.decidable logic.inhabited
import data.unit.thms logic.subsingleton
open decidable
namespace unit
@ -9,7 +9,7 @@ namespace unit
subsingleton.intro (λ a b, equal a b)
protected definition is_inhabited [instance] : inhabited unit :=
inhabited.mk ⋆
inhabited.mk unit.star
protected definition has_decidable_eq [instance] : decidable_eq unit :=
take (a b : unit), inl (equal a b)

2
library/data/unit/thms.lean
View file

@ -1,7 +1,7 @@
-- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
-- Released under Apache 2.0 license as described in the file LICENSE.
-- Author: Leonardo de Moura
import data.unit.decl logic.eq
import logic.eq
namespace unit
protected theorem equal (a b : unit) : a = b :=

2
library/hott/path.lean
View file

@ -8,7 +8,7 @@
-- o Try doing these proofs with tactics.
-- o Try using the simplifier on some of these proofs.
import general_notation type algebra.function tools.tactic
import algebra.function
open function

3
library/data/bool/ops.lean → library/init/bool.lean
View file

@ -1,7 +1,8 @@
-- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
-- Released under Apache 2.0 license as described in the file LICENSE.
-- Author: Leonardo de Moura
import general_notation data.bool.decl
prelude
import init.datatypes init.reserved_notation
namespace bool
definition cond {A : Type} (b : bool) (t e : A) :=

72
library/init/datatypes.lean Normal file
View file

@ -0,0 +1,72 @@
/-
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
notation `Prop` := Type.{0}
notation [parsing-only] `Type'` := Type.{_+1}
notation [parsing-only] `Type₊` := Type.{_+1}
notation `Type₁` := Type.{1}
notation `Type₂` := Type.{2}
notation `Type₃` := Type.{3}
inductive unit.{l} : Type.{l} :=
star : unit
inductive true : Prop :=
intro : true
inductive false : Prop
inductive empty : Type
inductive eq {A : Type} (a : A) : A → Prop :=
refl : eq a a
inductive heq {A : Type} (a : A) : Π {B : Type}, B → Prop :=
refl : heq a a
structure prod (A B : Type) :=
mk :: (pr1 : A) (pr2 : B)
inductive and (a b : Prop) : Prop :=
intro : a → b → and a b
inductive sum (A B : Type) : Type :=
inl : A → sum A B,
inr : B → sum A B
inductive or (a b : Prop) : Prop :=
intro_left : a → or a b,
intro_right : b → or 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

3
library/init/default.lean
View file

@ -5,3 +5,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
prelude
import init.datatypes init.reserved_notation init.tactic init.logic
import init.relation init.wf init.nat init.wf_k init.prod init.priority
import init.bool init.num init.sigma

617
library/init/logic.lean Normal file
View file

@ -0,0 +1,617 @@
/-
Copyright (c) 2014 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura, Jeremy Avigad, Floris van Doorn
-/
prelude
import init.datatypes init.reserved_notation
-- implication
-- -----------
definition imp (a b : Prop) : Prop := a → b
-- make c explicit and rename to false.elim
theorem false_elim {c : Prop} (H : false) : c :=
false.rec c H
definition trivial := true.intro
definition not (a : Prop) := a → false
prefix `¬` := not
definition absurd {a : Prop} {b : Type} (H1 : a) (H2 : ¬a) : b :=
false.rec b (H2 H1)
theorem mt {a b : Prop} (H1 : a → b) (H2 : ¬b) : ¬a :=
assume Ha : a, absurd (H1 Ha) H2
-- not
-- ---
theorem not_false : ¬false :=
assume H : false, H
theorem not_not_intro {a : Prop} (Ha : a) : ¬¬a :=
assume Hna : ¬a, absurd Ha Hna
theorem not_intro {a : Prop} (H : a → false) : ¬a := H
theorem not_elim {a : Prop} (H1 : ¬a) (H2 : a) : false := H1 H2
theorem not_implies_left {a b : Prop} (H : ¬(a → b)) : ¬¬a :=
assume Hna : ¬a, absurd (assume Ha : a, absurd Ha Hna) H
theorem not_implies_right {a b : Prop} (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
-- proof irrelevance is built in
theorem proof_irrel {a : Prop} (H₁ H₂ : a) : H₁ = H₂ :=
rfl
namespace eq
variables {A : Type}
variables {a b c a': A}
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 id_refl (H₁ : a = a) : H₁ = (eq.refl a) :=
rfl
theorem irrel (H₁ H₂ : a = b) : H₁ = H₂ :=
!proof_irrel
theorem subst {P : A → Prop} (H₁ : a = b) (H₂ : P a) : P b :=
rec H₂ H₁
theorem trans (H₁ : a = b) (H₂ : b = c) : a = c :=
subst H₂ H₁
theorem 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
variable {p : Prop}
open ops
theorem true_elim (H : p = true) : p :=
H⁻¹ ▸ trivial
theorem false_elim (H : p = false) : ¬p :=
assume Hp, H ▸ Hp
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 → false) → a ≠ b :=
assume H, H
theorem elim : a ≠ b → a = b → false :=
assume H₁ H₂, H₁ H₂
theorem irrefl : a ≠ a → false :=
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 → false :=
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
infixl `==`:50 := heq
namespace heq
universe variable u
variables {A B C : Type.{u}} {a a' : A} {b b' : B} {c : C}
definition to_eq (H : a == a') : a = a' :=
have H₁ : ∀ (Ht : A = A), eq.rec_on Ht a = a, from
λ Ht, eq.refl (eq.rec_on Ht a),
heq.rec_on H H₁ (eq.refl A)
definition elim {A : Type} {a : A} {P : A → Type} {b : A} (H₁ : a == b) (H₂ : P a) : P b :=
eq.rec_on (to_eq H₁) H₂
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₁
theorem subst {P : ∀T : Type, T → Prop} (H₁ : a == b) (H₂ : P A a) : P B b :=
rec_on H₁ H₂
theorem symm (H : a == b) : b == a :=
rec_on H (refl a)
definition type_eq (H : a == b) : A = B :=
heq.rec_on H (eq.refl A)
theorem from_eq (H : a = a') : a == a' :=
eq.subst H (refl a)
theorem trans (H₁ : a == b) (H₂ : b == c) : a == c :=
subst H₂ H₁
theorem trans_left (H₁ : a == b) (H₂ : b = b') : a == b' :=
trans H₁ (from_eq H₂)
theorem trans_right (H₁ : a = a') (H₂ : a' == b) : a == b :=
trans (from_eq H₁) H₂
theorem true_elim {a : Prop} (H : a == true) : a :=
eq.true_elim (heq.to_eq H)
end heq
calc_trans heq.trans
calc_trans heq.trans_left
calc_trans heq.trans_right
calc_symm heq.symm
theorem eq_rec_heq {A : Type} {P : A → Type} {a a' : A} (H : a = a') (p : P a) : eq.rec_on H p == p :=
eq.drec_on H !heq.refl
section
universe variables u v
variables {A A' B C : Type.{u}} {P P' : A → Type.{v}} {a a' : A} {b : B}
theorem hcongr_fun {f : Π x, P x} {f' : Π x, P' x} (a : A) (H₁ : f == f') (H₂ : P = P') : f a == f' a :=
have aux : ∀ (f : Π x, P x) (f' : Π x, P x), f == f' → f a == f' a, from
take f f' H, heq.to_eq H ▸ heq.refl (f a),
(H₂ ▸ aux) f f' H₁
theorem hcongr {P' : A' → Type} {f : Π a, P a} {f' : Π a', P' a'} {a : A} {a' : A'}
(Hf : f == f') (HP : P == P') (Ha : a == a') : f a == f' a' :=
have H1 : ∀ (B P' : A → Type) (f : Π x, P x) (f' : Π x, P' x), f == f' → (λx, P x) == (λx, P' x)
→ f a == f' a, from
take P P' f f' Hf HB, hcongr_fun a Hf (heq.to_eq HB),
have H2 : ∀ (B : A → Type) (P' : A' → Type) (f : Π x, P x) (f' : Π x, P' x),
f == f' → (λx, P x) == (λx, P' x) → f a == f' a', from heq.subst Ha H1,
H2 P P' f f' Hf HP
theorem hcongr_arg (f : Πx, P x) {a b : A} (H : a = b) : f a == f b :=
H ▸ (heq.refl (f a))
end
section
variables {A : Type} {B : A → Type} {C : Πa, B a → Type} {D : Πa b, C a b → Type}
variables {a a' : A} {b : B a} {b' : B a'} {c : C a b} {c' : C a' b'}
theorem hcongr_arg2 (f : Πa b, C a b) (Ha : a = a') (Hb : b == b') : f a b == f a' b' :=
hcongr (hcongr_arg f Ha) (hcongr_arg C Ha) Hb
theorem hcongr_arg3 (f : Πa b c, D a b c) (Ha : a = a') (Hb : b == b') (Hc : c == c')
: f a b c == f a' b' c' :=
hcongr (hcongr_arg2 f Ha Hb) (hcongr_arg2 D Ha Hb) Hc
end
-- and
-- ---
notation a /\ b := and a b
notation a ∧ b := and a b
variables {a b c d : Prop}
namespace and
theorem elim (H₁ : a ∧ b) (H₂ : a → b → c) : c :=
rec H₂ H₁
definition elim_left (H : a ∧ b) : a :=
rec (λa b, a) H
definition elim_right (H : a ∧ b) : b :=
rec (λa b, b) H
theorem swap (H : a ∧ b) : b ∧ a :=
intro (elim_right H) (elim_left H)
definition not_left (b : Prop) (Hna : ¬a) : ¬(a ∧ b) :=
assume H : a ∧ b, absurd (elim_left H) Hna
definition not_right (a : Prop) {b : Prop} (Hnb : ¬b) : ¬(a ∧ b) :=
assume H : a ∧ b, absurd (elim_right H) Hnb
theorem imp_and (H₁ : a ∧ b) (H₂ : a → c) (H₃ : b → d) : c ∧ d :=
elim H₁ (assume Ha : a, assume Hb : b, intro (H₂ Ha) (H₃ Hb))
theorem imp_left (H₁ : a ∧ c) (H : a → b) : b ∧ c :=
elim H₁ (assume Ha : a, assume Hc : c, intro (H Ha) Hc)
theorem imp_right (H₁ : c ∧ a) (H : a → b) : c ∧ b :=
elim H₁ (assume Hc : c, assume Ha : a, intro Hc (H Ha))
end and
-- or
-- --
notation a `\/` b := or a b
notation a ∨ b := or a b
namespace or
definition inl (Ha : a) : a ∨ b :=
intro_left b Ha
definition inr (Hb : b) : a ∨ b :=
intro_right a Hb
theorem elim (H₁ : a ∨ b) (H₂ : a → c) (H₃ : b → c) : c :=
rec H₂ H₃ H₁
theorem elim3 (H : a ∨ b ∨ c) (Ha : a → d) (Hb : b → d) (Hc : c → d) : d :=
elim H Ha (assume H₂, elim H₂ Hb Hc)
theorem resolve_right (H₁ : a ∨ b) (H₂ : ¬a) : b :=
elim H₁ (assume Ha, absurd Ha H₂) (assume Hb, Hb)
theorem resolve_left (H₁ : a ∨ b) (H₂ : ¬b) : a :=
elim H₁ (assume Ha, Ha) (assume Hb, absurd Hb H₂)
theorem swap (H : a ∨ b) : b ∨ a :=
elim H (assume Ha, inr Ha) (assume Hb, inl Hb)
definition not_intro (Hna : ¬a) (Hnb : ¬b) : ¬(a ∨ b) :=
assume H : a ∨ b, or.rec_on H
(assume Ha, absurd Ha Hna)
(assume Hb, absurd Hb Hnb)
theorem imp_or (H₁ : a ∨ b) (H₂ : a → c) (H₃ : b → d) : c ∨ d :=
elim H₁
(assume Ha : a, inl (H₂ Ha))
(assume Hb : b, inr (H₃ Hb))
theorem imp_or_left (H₁ : a ∨ c) (H : a → b) : b ∨ c :=
elim H₁
(assume H₂ : a, inl (H H₂))
(assume H₂ : c, inr H₂)
theorem imp_or_right (H₁ : c ∨ a) (H : a → b) : c ∨ b :=
elim H₁
(assume H₂ : c, inl H₂)
(assume H₂ : a, inr (H H₂))
end or
theorem not_not_em {p : Prop} : ¬¬(p ∨ ¬p) :=
assume not_em : ¬(p ∨ ¬p),
have Hnp : ¬p, from
assume Hp : p, absurd (or.inl Hp) not_em,
absurd (or.inr Hnp) not_em
-- iff
-- ---
definition iff (a b : Prop) := (a → b) ∧ (b → a)
notation a <-> b := iff a b
notation a ↔ b := iff a b
namespace iff
definition def : (a ↔ b) = ((a → b) ∧ (b → a)) :=
rfl
definition intro (H₁ : a → b) (H₂ : b → a) : a ↔ b :=
and.intro H₁ H₂
definition elim (H₁ : (a → b) → (b → a) → c) (H₂ : a ↔ b) : c :=
and.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 : Prop) : a ↔ a :=
intro (assume H, H) (assume H, H)
definition rfl {a : Prop} : 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 ↔ true) : a :=
mp (symm H) trivial
theorem false_elim (H : a ↔ false) : ¬a :=
assume Ha : a, mp H Ha
open eq.ops
theorem of_eq {a b : Prop} (H : a = b) : a ↔ b :=
iff.intro (λ Ha, H ▸ Ha) (λ Hb, H⁻¹ ▸ Hb)
end iff
calc_refl iff.refl
calc_trans iff.trans
-- comm and assoc for and / or
-- ---------------------------
namespace and
theorem comm : a ∧ b ↔ b ∧ a :=
iff.intro (λH, swap H) (λH, swap H)
theorem assoc : (a ∧ b) ∧ c ↔ a ∧ (b ∧ c) :=
iff.intro
(assume H, intro
(elim_left (elim_left H))
(intro (elim_right (elim_left H)) (elim_right H)))
(assume H, intro
(intro (elim_left H) (elim_left (elim_right H)))
(elim_right (elim_right H)))
end and
namespace or
theorem comm : a ∨ b ↔ b ∨ a :=
iff.intro (λH, swap H) (λH, swap H)
theorem assoc : (a ∨ b) ∨ c ↔ a ∨ (b ∨ c) :=
iff.intro
(assume H, elim H
(assume H₁, elim H₁
(assume Ha, inl Ha)
(assume Hb, inr (inl Hb)))
(assume Hc, inr (inr Hc)))
(assume H, elim H
(assume Ha, (inl (inl Ha)))
(assume H₁, elim H₁
(assume Hb, inl (inr Hb))
(assume Hc, inr Hc)))
end or
inductive Exists {A : Type} (P : A → Prop) : Prop :=
intro : ∀ (a : A), P a → Exists P
definition exists_intro := @Exists.intro
notation `exists` binders `,` r:(scoped P, Exists P) := r
notation `∃` binders `,` r:(scoped P, Exists P) := r
theorem exists_elim {A : Type} {p : A → Prop} {B : Prop} (H1 : ∃x, p x) (H2 : ∀ (a : A) (H : p a), B) : B :=
Exists.rec H2 H1
definition exists_unique {A : Type} (p : A → Prop) :=
∃x, p x ∧ ∀y, p y → y = x
notation `∃!` binders `,` r:(scoped P, exists_unique P) := r
theorem exists_unique_intro {A : Type} {p : A → Prop} (w : A) (H1 : p w) (H2 : ∀y, p y → y = w) : ∃!x, p x :=
exists_intro w (and.intro H1 H2)
theorem exists_unique_elim {A : Type} {p : A → Prop} {b : Prop}
(H2 : ∃!x, p x) (H1 : ∀x, p x → (∀y, p y → y = x) → b) : b :=
obtain w Hw, from H2,
H1 w (and.elim_left Hw) (and.elim_right Hw)
inductive decidable [class] (p : Prop) : Type :=
inl : p → decidable p,
inr : ¬p → decidable p
definition true.decidable [instance] : decidable true :=
decidable.inl trivial
definition false.decidable [instance] : decidable false :=
decidable.inr not_false
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))
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)
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 : Prop) [H : decidable p] : p ∨ ¬p :=
by_cases (λ Hp, or.inl Hp) (λ Hnp, or.inr Hnp)
theorem by_contradiction [Hp : decidable p] (H : ¬p → false) : p :=
by_cases
(assume H1 : p, H1)
(assume H1 : ¬p, false_elim (H H1))
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 (Hp : decidable p) (H : p = q) : decidable q :=
decidable_iff_equiv Hp (iff.of_eq H)
end decidable
section
variables {p q : Prop}
open decidable (rec_on inl inr)
definition and.decidable [instance] (Hp : decidable p) (Hq : decidable q) : decidable (p ∧ q) :=
rec_on Hp
(assume Hp : p, rec_on Hq
(assume Hq : q, inl (and.intro Hp Hq))
(assume Hnq : ¬q, inr (and.not_right p Hnq)))
(assume Hnp : ¬p, inr (and.not_left q Hnp))
definition or.decidable [instance] (Hp : decidable p) (Hq : decidable q) : decidable (p ∨ q) :=
rec_on Hp
(assume Hp : p, inl (or.inl Hp))
(assume Hnp : ¬p, rec_on Hq
(assume Hq : q, inl (or.inr Hq))
(assume Hnq : ¬q, inr (or.not_intro Hnp 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 → Prop) := Π (a : A), decidable (R a)
definition decidable_rel {A : Type} (R : A → A → Prop) := Π (a b : A), decidable (R a b)
definition decidable_eq (A : Type) := decidable_rel (@eq A)
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 Prop_inhabited [instance] : inhabited Prop :=
mk true
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
inductive nonempty [class] (A : Type) : Prop :=
intro : A → nonempty A
namespace nonempty
protected definition elim {A : Type} {B : Prop} (H1 : nonempty A) (H2 : A → B) : B :=
rec H2 H1
theorem inhabited_imp_nonempty [instance] {A : Type} (H : inhabited A) : nonempty A :=
intro (inhabited.default A)
end nonempty
definition ite (c : Prop) [H : decidable c] {A : Type} (t e : A) : A :=
decidable.rec_on H (λ Hc, t) (λ Hnc, e)
notation `if` c `then` t:45 `else` e:45 := ite c t e
definition if_pos {c : Prop} [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 : Prop} [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 : Prop) [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_true {A : Type} (t e : A) : (if true then t else e) = t :=
if_pos trivial
definition if_false {A : Type} (t e : A) : (if false then t else e) = e :=
if_neg not_false
theorem if_cond_congr {c₁ c₂ : Prop} [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₂ : Prop} [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₂ : Prop} [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 : Prop) [H : decidable c] {A : Type} (t : c → A) (e : ¬ c → A) : A :=
decidable.rec_on H (λ Hc, t Hc) (λ Hnc, e Hnc)
notation `dif` c `then` t:45 `else` e:45 := dite c t e
definition dif_pos {c : Prop} [H : decidable c] (Hc : c) {A : Type} {t : c → A} {e : ¬ c → A} : (dif c then t else e) = t 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 : Prop} [H : decidable c] (Hnc : ¬c) {A : Type} {t : c → A} {e : ¬ c → A} : (dif c then t else e) = e 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 : Prop) [H : decidable c] {A : Type} (t : A) (e : A) : dite c (λh, t) (λh, e) = ite c t e :=
rfl

15
library/data/nat/decl.lean → library/init/nat.lean
View file

@ -1,14 +1,13 @@
--- Copyright (c) 2014 Floris van Doorn. All rights reserved.
--- Released under Apache 2.0 license as described in the file LICENSE.
--- Author: Floris van Doorn, Leonardo de Moura
import logic.eq logic.heq logic.wf logic.decidable logic.if data.prod
/-
Copyright (c) 2014 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Floris van Doorn, Leonardo de Moura
-/
prelude
import init.wf init.tactic
open eq.ops decidable
inductive nat :=
zero : nat,
succ : nat → nat
namespace nat
notation `ℕ` := nat

14
library/data/num/ops.lean → library/init/num.lean
View file

@ -1,9 +1,11 @@
----------------------------------------------------------------------------------------------------
-- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
-- Released under Apache 2.0 license as described in the file LICENSE.
-- Author: Leonardo de Moura
----------------------------------------------------------------------------------------------------
import data.num.decl logic.inhabited data.bool
/-
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 :=

10
library/init/priority.lean 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

31
library/data/prod/wf.lean → library/init/prod.lean
View file

@ -1,10 +1,31 @@
-- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
-- Released under Apache 2.0 license as described in the file LICENSE.
-- Author: Leonardo de Moura
import data.prod.decl logic.wf
open well_founded
/-
Copyright (c) 2014 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Module: data.prod.decl
Author: Leonardo de Moura, Jeremy Avigad
-/
prelude
import init.wf
definition pair := @prod.mk
namespace prod
notation A * B := prod A B
notation A × B := prod A B
namespace low_precedence_times
reserve infixr `*`:30 -- conflicts with notation for multiplication
infixr `*` := prod
end low_precedence_times
notation `pr₁` := pr1
notation `pr₂` := pr2
-- notation for n-ary tuples
notation `(` h `,` t:(foldl `,` (e r, prod.mk r e) h) `)` := t
open well_founded
section
variables {A B : Type}
variable (Ra : A → A → Prop)

11
library/logic/relation.lean → library/init/relation.lean
View file

@ -1,7 +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
import logic.eq
/-
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.

5
library/general_notation.lean → library/init/reserved_notation.lean
View file

@ -5,9 +5,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
Module: general_notation
Authors: Leonardo de Moura, Jeremy Avigad
-/
import data.num.decl
/- General operations -/
prelude
import init.datatypes
notation `assume` binders `,` r:(scoped f, f) := r
notation `take` binders `,` r:(scoped f, f) := r

37
library/data/sigma/wf.lean → library/init/sigma.lean
View file

@ -1,10 +1,27 @@
-- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
-- Released under Apache 2.0 license as described in the file LICENSE.
-- Author: Leonardo de Moura
import data.sigma.decl logic.wf logic.cast
open well_founded
-- Author: Leonardo de Moura, Jeremy Avigad, Floris van Doorn
prelude
import init.num init.wf init.logic init.tactic
structure sigma {A : Type} (B : A → Type) :=
dpair :: (dpr1 : A) (dpr2 : B dpr1)
notation `Σ` binders `,` r:(scoped P, sigma P) := r
namespace sigma
notation `dpr₁` := dpr1
notation `dpr₂` := dpr2
namespace ops
postfix `.1`:(max+1) := dpr1
postfix `.2`:(max+1) := dpr2
notation `⟨` t:(foldr `,` (e r, sigma.dpair e r)) `⟩`:0 := t --input ⟨ ⟩ as \< \>
end ops
open well_founded
section
variables {A : Type} {B : A → Type}
variable (Ra : A → A → Prop)
@ -23,6 +40,19 @@ namespace sigma
set_option pp.beta true
variables {C : Πa, B a → Type} {D : Πa b, C a b → Type}
variables {a a' : A}
{b : B a} {b' : B a'}
{c : C a b} {c' : C a' b'}
{d : D a b c} {d' : D a' b' c'}
private theorem hcongr_arg2 (f : Πa b, C a b) (Ha : a = a') (Hb : b == b') : f a b == f a' b' :=
hcongr (hcongr_arg f Ha) (hcongr_arg C Ha) Hb
private theorem hcongr_arg3 (f : Πa b c, D a b c) (Ha : a = a') (Hb : b == b') (Hc : c == c')
: f a b c == f a' b' c' :=
hcongr (hcongr_arg2 f Ha Hb) (hcongr_arg2 D Ha Hb) Hc
definition lex.accessible {a} (aca : acc Ra a) (acb : ∀a, well_founded (Rb a)) : ∀ (b : B a), acc (lex Ra Rb) (dpair a b) :=
acc.rec_on aca
(λxa aca (iHa : ∀y, Ra y xa → ∀b : B y, acc (lex Ra Rb) (dpair y b)),
@ -61,5 +91,4 @@ namespace sigma
well_founded.intro (λp, destruct p (λa b, lex.accessible (Ha a) Hb b))
end
end sigma

29
library/tools/tactic.lean → library/init/tactic.lean
View file

@ -1,16 +1,19 @@
----------------------------------------------------------------------------------------------------
-- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
-- Released under Apache 2.0 license as described in the file LICENSE.
-- Author: Leonardo de Moura
----------------------------------------------------------------------------------------------------
import data.string.decl data.num.decl general_notation
-- 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++
inductive tactic : Type :=
builtin : tactic
/-
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

11
library/logic/wf.lean → library/init/wf.lean
View file

@ -1,7 +1,10 @@
-- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
-- Released under Apache 2.0 license as described in the file LICENSE.
-- Author: Leonardo de Moura
import logic.eq logic.relation
/-
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.relation
inductive acc {A : Type} (R : A → A → Prop) : A → Prop :=
intro : ∀x, (∀ y, R y x → acc R y) → acc R x

4
library/logic/wf_k.lean → library/init/wf_k.lean
View file

@ -1,10 +1,10 @@
-- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
-- Released under Apache 2.0 license as described in the file LICENSE.
-- Author: Leonardo de Moura
import logic.wf data.nat.basic
prelude
import init.nat
namespace well_founded
-- This is an auxiliary definition that useful for generating a new "proof" for (well_founded R)
-- that allows us to use well_founded.fix and execute the definitions up to k nested recursive
-- calls without "computing" with the proofs in Hwf.

8
library/logic/axioms/classical.lean
View file

@ -23,8 +23,8 @@ cases P H1 H2 a
-- this supercedes the em in decidable
theorem em (a : Prop) : a ∨ ¬a :=
or.elim (prop_complete a)
(assume Ht : a = true, or.inl (eq_true_elim Ht))
(assume Hf : a = false, or.inr (eq_false_elim Hf))
(assume Ht : a = true, or.inl (eq.true_elim Ht))
(assume Hf : a = false, or.inr (eq.false_elim Hf))
theorem prop_complete_swapped (a : Prop) : a = false ∨ a = true :=
cases (λ x, x = false ∨ x = true)
@ -36,9 +36,9 @@ theorem propext {a b : Prop} (Hab : a → b) (Hba : b → a) : a = b :=
or.elim (prop_complete a)
(assume Hat, or.elim (prop_complete b)
(assume Hbt, Hat ⬝ Hbt⁻¹)
(assume Hbf, false_elim (Hbf ▸ (Hab (eq_true_elim Hat)))))
(assume Hbf, false_elim (Hbf ▸ (Hab (eq.true_elim Hat)))))
(assume Haf, or.elim (prop_complete b)
(assume Hbt, false_elim (Haf ▸ (Hba (eq_true_elim Hbt))))
(assume Hbt, false_elim (Haf ▸ (Hba (eq.true_elim Hbt))))
(assume Hbf, Haf ⬝ Hbf⁻¹))
theorem eq.of_iff {a b : Prop} (H : a ↔ b) : a = b :=

2
library/logic/axioms/hilbert.lean
View file

@ -7,9 +7,7 @@
-- Follows Coq.Logic.ClassicalEpsilon (but our definition of "inhabited" is the
-- constructive one).
import logic.quantifiers
import logic.inhabited logic.nonempty
import data.subtype data.sum
open subtype inhabited nonempty

2
library/logic/axioms/prop_decidable.lean
View file

@ -5,7 +5,7 @@
-- logic.axioms.prop_decidable
-- ===========================
import logic.axioms.classical logic.axioms.hilbert logic.decidable
import logic.axioms.classical logic.axioms.hilbert
open decidable inhabited nonempty
-- Excluded middle + Hilbert implies every proposition is decidable

28
library/logic/cast.lean
View file

@ -1,7 +1,7 @@
-- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
-- Released under Apache 2.0 license as described in the file LICENSE.
-- Author: Leonardo de Moura
import logic.eq logic.heq logic.quantifiers
import logic.eq logic.quantifiers
open eq.ops
-- cast.lean
@ -35,9 +35,6 @@ section
universe variables u v
variables {A A' B C : Type.{u}} {P P' : A → Type.{v}} {a a' : A} {b : B}
theorem eq_rec_heq (H : a = a') (p : P a) : eq.rec_on H p == p :=
eq.drec_on H !heq.refl
-- should H₁ be explicit (useful in e.g. hproof_irrel)
theorem eq_rec_to_heq {H₁ : a = a'} {p : P a} {p' : P a'} (H₂ : eq.rec_on H₁ p = p') : p == p' :=
calc
@ -61,19 +58,11 @@ section
theorem pi_eq (H : P = P') : (Π x, P x) = (Π x, P' x) :=
H ▸ (eq.refl (Π x, P x))
theorem hcongr_arg (f : Πx, P x) {a b : A} (H : a = b) : f a == f b :=
H ▸ (heq.refl (f a))
theorem rec_on_app (H : P = P') (f : Π x, P x) (a : A) : eq.rec_on H f a == f a :=
have aux : ∀ H : P = P, eq.rec_on H f a == f a, from
take H : P = P, heq.refl (eq.rec_on H f a),
(H ▸ aux) H
theorem hcongr_fun {f : Π x, P x} {f' : Π x, P' x} (a : A) (H₁ : f == f') (H₂ : P = P') : f a == f' a :=
have aux : ∀ (f : Π x, P x) (f' : Π x, P x), f == f' → f a == f' a, from
take f f' H, heq.to_eq H ▸ heq.refl (f a),
(H₂ ▸ aux) f f' H₁
theorem rec_on_pull (H : P = P') (f : Π x, P x) (a : A) : eq.rec_on H f a = eq.rec_on (congr_fun H a) (f a) :=
heq.to_eq (calc
eq.rec_on H f a == f a : rec_on_app H f a
@ -86,14 +75,6 @@ section
H ▸ H₁,
H₂ (pi_eq H)
theorem hcongr {P' : A' → Type} {f : Π a, P a} {f' : Π a', P' a'} {a : A} {a' : A'}
(Hf : f == f') (HP : P == P') (Ha : a == a') : f a == f' a' :=
have H1 : ∀ (B P' : A → Type) (f : Π x, P x) (f' : Π x, P' x), f == f' → (λx, P x) == (λx, P' x)
→ f a == f' a, from
take P P' f f' Hf HB, hcongr_fun a Hf (heq.to_eq HB),
have H2 : ∀ (B : A → Type) (P' : A' → Type) (f : Π x, P x) (f' : Π x, P' x),
f == f' → (λx, P x) == (λx, P' x) → f a == f' a', from heq.subst Ha H1,
H2 P P' f f' Hf HP
end
section
@ -104,13 +85,6 @@ section
{c : C a b} {c' : C a' b'}
{d : D a b c} {d' : D a' b' c'}
theorem hcongr_arg2 (f : Πa b, C a b) (Ha : a = a') (Hb : b == b') : f a b == f a' b' :=
hcongr (hcongr_arg f Ha) (hcongr_arg C Ha) Hb
theorem hcongr_arg3 (f : Πa b c, D a b c) (Ha : a = a') (Hb : b == b') (Hc : c == c')
: f a b c == f a' b' c' :=
hcongr (hcongr_arg2 f Ha Hb) (hcongr_arg2 D Ha Hb) Hc
theorem hcongr_arg4 (f : Πa b c d, E a b c d)
(Ha : a = a') (Hb : b == b') (Hc : c == c') (Hd : d == d') : f a b c d == f a' b' c' d' :=
hcongr (hcongr_arg3 f Ha Hb Hc) (hcongr_arg3 E Ha Hb Hc) Hd

196
library/logic/connectives.lean
View file

@ -1,196 +0,0 @@
-- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
-- Released under Apache 2.0 license as described in the file LICENSE.
-- Authors: Leonardo de Moura, Jeremy Avigad
import general_notation .eq
-- and
-- ---
inductive and (a b : Prop) : Prop :=
intro : a → b → and a b
notation a /\ b := and a b
notation a ∧ b := and a b
variables {a b c d : Prop}
namespace and
theorem elim (H₁ : a ∧ b) (H₂ : a → b → c) : c :=
rec H₂ H₁
definition elim_left (H : a ∧ b) : a :=
rec (λa b, a) H
definition elim_right (H : a ∧ b) : b :=
rec (λa b, b) H
theorem swap (H : a ∧ b) : b ∧ a :=
intro (elim_right H) (elim_left H)
definition not_left (b : Prop) (Hna : ¬a) : ¬(a ∧ b) :=
assume H : a ∧ b, absurd (elim_left H) Hna
definition not_right (a : Prop) {b : Prop} (Hnb : ¬b) : ¬(a ∧ b) :=
assume H : a ∧ b, absurd (elim_right H) Hnb
theorem imp_and (H₁ : a ∧ b) (H₂ : a → c) (H₃ : b → d) : c ∧ d :=
elim H₁ (assume Ha : a, assume Hb : b, intro (H₂ Ha) (H₃ Hb))
theorem imp_left (H₁ : a ∧ c) (H : a → b) : b ∧ c :=
elim H₁ (assume Ha : a, assume Hc : c, intro (H Ha) Hc)
theorem imp_right (H₁ : c ∧ a) (H : a → b) : c ∧ b :=
elim H₁ (assume Hc : c, assume Ha : a, intro Hc (H Ha))
end and
-- or
-- --
inductive or (a b : Prop) : Prop :=
intro_left : a → or a b,
intro_right : b → or a b
notation a `\/` b := or a b
notation a ∨ b := or a b
namespace or
definition inl (Ha : a) : a ∨ b :=
intro_left b Ha
definition inr (Hb : b) : a ∨ b :=
intro_right a Hb
theorem elim (H₁ : a ∨ b) (H₂ : a → c) (H₃ : b → c) : c :=
rec H₂ H₃ H₁
theorem elim3 (H : a ∨ b ∨ c) (Ha : a → d) (Hb : b → d) (Hc : c → d) : d :=
elim H Ha (assume H₂, elim H₂ Hb Hc)
theorem resolve_right (H₁ : a ∨ b) (H₂ : ¬a) : b :=
elim H₁ (assume Ha, absurd Ha H₂) (assume Hb, Hb)
theorem resolve_left (H₁ : a ∨ b) (H₂ : ¬b) : a :=
elim H₁ (assume Ha, Ha) (assume Hb, absurd Hb H₂)
theorem swap (H : a ∨ b) : b ∨ a :=
elim H (assume Ha, inr Ha) (assume Hb, inl Hb)
definition not_intro (Hna : ¬a) (Hnb : ¬b) : ¬(a ∨ b) :=
assume H : a ∨ b, or.rec_on H
(assume Ha, absurd Ha Hna)
(assume Hb, absurd Hb Hnb)
theorem imp_or (H₁ : a ∨ b) (H₂ : a → c) (H₃ : b → d) : c ∨ d :=
elim H₁
(assume Ha : a, inl (H₂ Ha))
(assume Hb : b, inr (H₃ Hb))
theorem imp_or_left (H₁ : a ∨ c) (H : a → b) : b ∨ c :=
elim H₁
(assume H₂ : a, inl (H H₂))
(assume H₂ : c, inr H₂)
theorem imp_or_right (H₁ : c ∨ a) (H : a → b) : c ∨ b :=
elim H₁
(assume H₂ : c, inl H₂)
(assume H₂ : a, inr (H H₂))
end or
theorem not_not_em {p : Prop} : ¬¬(p ∨ ¬p) :=
assume not_em : ¬(p ∨ ¬p),
have Hnp : ¬p, from
assume Hp : p, absurd (or.inl Hp) not_em,
absurd (or.inr Hnp) not_em
-- iff
-- ---
definition iff (a b : Prop) := (a → b) ∧ (b → a)
notation a <-> b := iff a b
notation a ↔ b := iff a b
namespace iff
definition def : (a ↔ b) = ((a → b) ∧ (b → a)) :=
rfl
definition intro (H₁ : a → b) (H₂ : b → a) : a ↔ b :=
and.intro H₁ H₂
definition elim (H₁ : (a → b) → (b → a) → c) (H₂ : a ↔ b) : c :=
and.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 : Prop) : a ↔ a :=
intro (assume H, H) (assume H, H)
definition rfl {a : Prop} : 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 ↔ true) : a :=
mp (symm H) trivial
theorem false_elim (H : a ↔ false) : ¬a :=
assume Ha : a, mp H Ha
open eq.ops
theorem of_eq {a b : Prop} (H : a = b) : a ↔ b :=
iff.intro (λ Ha, H ▸ Ha) (λ Hb, H⁻¹ ▸ Hb)
end iff
calc_refl iff.refl
calc_trans iff.trans
-- comm and assoc for and / or
-- ---------------------------
namespace and
theorem comm : a ∧ b ↔ b ∧ a :=
iff.intro (λH, swap H) (λH, swap H)
theorem assoc : (a ∧ b) ∧ c ↔ a ∧ (b ∧ c) :=
iff.intro
(assume H, intro
(elim_left (elim_left H))
(intro (elim_right (elim_left H)) (elim_right H)))
(assume H, intro
(intro (elim_left H) (elim_left (elim_right H)))
(elim_right (elim_right H)))
end and
namespace or
theorem comm : a ∨ b ↔ b ∨ a :=
iff.intro (λH, swap H) (λH, swap H)
theorem assoc : (a ∨ b) ∨ c ↔ a ∨ (b ∨ c) :=
iff.intro
(assume H, elim H
(assume H₁, elim H₁
(assume Ha, inl Ha)
(assume Hb, inr (inl Hb)))
(assume Hc, inr (inr Hc)))
(assume H, elim H
(assume Ha, (inl (inl Ha)))
(assume H₁, elim H₁
(assume Hb, inl (inr Hb))
(assume Hc, inr Hc)))
end or

100
library/logic/decidable.lean
View file

@ -1,100 +0,0 @@
-- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
-- Released under Apache 2.0 license as described in the file LICENSE.
-- Author: Leonardo de Moura
import logic.connectives data.empty
inductive decidable [class] (p : Prop) : Type :=
inl : p → decidable p,
inr : ¬p → decidable p
namespace decidable
definition true_decidable [instance] : decidable true :=
inl trivial
definition false_decidable [instance] : decidable false :=
inr not_false_trivial
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))
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)
theorem irrelevant [instance] : subsingleton (decidable p) :=
subsingleton.intro (fun d1 d2,
decidable.rec
(assume Hp1 : p, decidable.rec
(assume Hp2 : p, congr_arg inl (eq.refl Hp1)) -- using proof irrelevance for Prop
(assume Hnp2 : ¬p, absurd Hp1 Hnp2)
d2)
(assume Hnp1 : ¬p, decidable.rec
(assume Hp2 : p, absurd Hp2 Hnp1)
(assume Hnp2 : ¬p, congr_arg inr (eq.refl Hnp1)) -- using proof irrelevance for Prop
d2)
d1)
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 : Prop) [H : decidable p] : p ∨ ¬p :=
by_cases (λ Hp, or.inl Hp) (λ Hnp, or.inr Hnp)
theorem by_contradiction [Hp : decidable p] (H : ¬p → false) : p :=
by_cases
(assume H1 : p, H1)
(assume H1 : ¬p, false_elim (H H1))
definition and_decidable [instance] (Hp : decidable p) (Hq : decidable q) : decidable (p ∧ q) :=
rec_on Hp
(assume Hp : p, rec_on Hq
(assume Hq : q, inl (and.intro Hp Hq))
(assume Hnq : ¬q, inr (and.not_right p Hnq)))
(assume Hnp : ¬p, inr (and.not_left q Hnp))
definition or_decidable [instance] (Hp : decidable p) (Hq : decidable q) : decidable (p ∨ q) :=
rec_on Hp
(assume Hp : p, inl (or.inl Hp))
(assume Hnp : ¬p, rec_on Hq
(assume Hq : q, inl (or.inr Hq))
(assume Hnq : ¬q, inr (or.not_intro Hnp 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) := _
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 (Hp : decidable p) (H : p = q) : decidable q :=
decidable_iff_equiv Hp (iff.of_eq H)
protected theorem rec_subsingleton [instance] [H : decidable p] {H1 : p → Type} {H2 : ¬p → Type}
(H3 : Π(h : p), subsingleton (H1 h)) (H4 : Π(h : ¬p), subsingleton (H2 h))
: subsingleton (rec_on H H1 H2) :=
rec_on H (λh, H3 h) (λh, H4 h) --this can be proven using dependent version of "by_cases"
end decidable
definition decidable_pred {A : Type} (R : A → Prop) := Π (a : A), decidable (R a)
definition decidable_rel {A : Type} (R : A → A → Prop) := Π (a b : A), decidable (R a b)
definition decidable_eq (A : Type) := decidable_rel (@eq A)
--empty cannot depend on decidable, so we prove this here
protected definition empty.has_decidable_eq [instance] : decidable_eq empty :=
take (a b : empty), decidable.inl (!empty.elim a)

10
library/logic/default.lean
View file

@ -2,11 +2,5 @@
--- Released under Apache 2.0 license as described in the file LICENSE.
--- Author: Jeremy Avigad
import logic.connectives logic.eq logic.heq
import logic.cast logic.wf logic.wf_k
-- We need unit and prod available for generating constructions used by definitional package
import data.unit.decl data.prod.decl
import logic.quantifiers logic.if
import logic.decidable logic.inhabited logic.nonempty
import logic.instances
import logic.identities
import logic.eq logic.cast logic.subsingleton
import logic.quantifiers logic.instances logic.identities

149
library/logic/eq.lean
View file

@ -1,88 +1,20 @@
-- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
-- Released under Apache 2.0 license as described in the file LICENSE.
-- Authors: Leonardo de Moura, Jeremy Avigad, Floris van Doorn
import general_notation logic.prop data.unit.decl
/-
Copyright (c) 2014 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura, Jeremy Avigad, Floris van Doorn
Additional declarations/theorems about equality
-/
-- logic.eq
-- ====================
-- ========
-- Equality.
-- eq
-- --
inductive eq {A : Type} (a : A) : A → Prop :=
refl : eq a a
notation a = b := eq a b
definition rfl {A : Type} {a : A} := eq.refl a
-- proof irrelevance is built in
theorem proof_irrel {a : Prop} (H₁ H₂ : a) : H₁ = H₂ :=
rfl
namespace eq
variables {A : Type}
variables {a b c : A}
theorem id_refl (H₁ : a = a) : H₁ = (eq.refl a) :=
rfl
theorem irrel (H₁ H₂ : a = b) : H₁ = H₂ :=
!proof_irrel
theorem subst {P : A → Prop} (H₁ : a = b) (H₂ : P a) : P b :=
rec H₂ H₁
theorem trans (H₁ : a = b) (H₂ : b = c) : a = c :=
subst H₂ H₁
theorem 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
open eq.ops
namespace eq
variables {A B : Type} {a a' a₁ a₂ a₃ a₄ : A}
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₁
--can we remove the theorems about drec_on and only have the rec_on versions?
-- theorem drec_on_id {B : Πa' : A, a = a' → Type} (H : a = a) (b : B a H) : drec_on H b = b :=
-- rfl
-- theorem drec_on_constant (H : a = a') {B : Type} (b : B) : drec_on H b = b :=
-- drec_on H rfl
-- theorem drec_on_constant2 (H₁ : a₁ = a₂) (H₂ : a₃ = a₄) (b : B) : drec_on H₁ b = drec_on H₂ b :=
-- drec_on_constant H₁ b ⬝ (drec_on_constant H₂ b)⁻¹
-- theorem drec_on_irrel_arg {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' : f a = f a), !drec_on_id⁻¹) H'
-- theorem drec_on_irrel {D : A → Type} (H H' : a = a') (b : D a) :
-- drec_on H b = drec_on H' b :=
-- !drec_on_irrel_arg
-- theorem drec_on_compose {a b c : A} {P : A → Type} (H₁ : a = b) (H₂ : b = c)
-- (u : P a) : drec_on H₂ (drec_on H₁ u) = drec_on (trans H₁ H₂) u :=
-- (show ∀ H₂ : b = c, drec_on H₂ (drec_on H₁ u) = drec_on (trans H₁ H₂) u,
-- from drec_on H₂ (take (H₂ : b = b), drec_on_id H₂ _))
-- H₂
theorem rec_on_id {B : A → Type} (H : a = a) (b : B a) : rec_on H b = b :=
rfl
@ -100,16 +32,6 @@ namespace eq
drec_on H b = drec_on H' b :=
!rec_on_irrel_arg
--do we need the following?
-- theorem rec_on_irrel_fun {B : A → Type} {a : A} {f f' : Π x, B x} {D : Π a, B a → Type} (H : f = f') (H' : f a = f' a) (b : D a (f a)) :
-- rec_on H b = rec_on H' b :=
-- sorry
-- the
-- theorem rec_on_comm_ap {B : A → Type} {C : Πa, B a → Type} {a a' : A} {f : Π x, C a x}
-- (H : a = a') (H' : a = a') (b : B a) : rec_on H f b = rec_on H' (f b) :=
-- sorry
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,
@ -178,12 +100,6 @@ section
theorem eqmpr (H₁ : a = b) (H₂ : b) : a :=
H₁⁻¹ ▸ H₂
theorem eq_true_elim (H : a = true) : a :=
H⁻¹ ▸ trivial
theorem eq_false_elim (H : a = false) : ¬a :=
assume Ha : a, H ▸ Ha
theorem imp_trans (H₁ : a → b) (H₂ : b → c) : a → c :=
assume Ha, H₂ (H₁ Ha)
@ -194,45 +110,6 @@ section
assume Ha, H₂ (H₁ ▸ Ha)
end
-- ne
-- --
definition ne {A : Type} (a b : A) := ¬(a = b)
notation a ≠ b := ne a b
namespace ne
variable {A : Type}
variables {a b : A}
theorem intro : (a = b → false) → a ≠ b :=
assume H, H
theorem elim : a ≠ b → a = b → false :=
assume H₁ H₂, H₁ H₂
theorem irrefl : a ≠ a → false :=
assume H, H rfl
theorem symm : a ≠ b → b ≠ a :=
assume (H : a ≠ b) (H₁ : b = a), H (H₁⁻¹)
end ne
section
variables {A : Type} {a b c : A}
theorem a_neq_a_elim : a ≠ a → false :=
assume H, H rfl
theorem eq_ne_trans : a = b → b ≠ c → a ≠ c :=
assume H₁ H₂, H₁⁻¹ ▸ H₂
theorem ne_eq_trans : a ≠ b → b = c → a ≠ c :=
assume H₁ H₂, H₂ ▸ H₁
end
calc_trans eq_ne_trans
calc_trans ne_eq_trans
section
variables {p : Prop}
@ -246,13 +123,3 @@ end
theorem true_ne_false : ¬true = false :=
assume H : true = false,
H ▸ trivial
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
end subsingleton
protected definition prop.subsingleton [instance] (P : Prop) : subsingleton P :=
subsingleton.intro (λa b, !proof_irrel)

54
library/logic/heq.lean
View file

@ -1,54 +0,0 @@
-- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
-- Released under Apache 2.0 license as described in the file LICENSE.
-- Author: Leonardo de Moura
import logic.eq
inductive heq {A : Type} (a : A) : Π {B : Type}, B → Prop :=
refl : heq a a
infixl `==`:50 := heq
namespace heq
universe variable u
variables {A B C : Type.{u}} {a a' : A} {b b' : B} {c : C}
definition to_eq (H : a == a') : a = a' :=
have H₁ : ∀ (Ht : A = A), eq.rec_on Ht a = a, from
λ Ht, eq.refl (eq.rec_on Ht a),
heq.rec_on H H₁ (eq.refl A)
definition elim {A : Type} {a : A} {P : A → Type} {b : A} (H₁ : a == b) (H₂ : P a) : P b :=
eq.rec_on (to_eq H₁) H₂
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₁
theorem subst {P : ∀T : Type, T → Prop} (H₁ : a == b) (H₂ : P A a) : P B b :=
rec_on H₁ H₂
theorem symm (H : a == b) : b == a :=
rec_on H (refl a)
definition type_eq (H : a == b) : A = B :=
heq.rec_on H (eq.refl A)
theorem from_eq (H : a = a') : a == a' :=
eq.subst H (refl a)
theorem trans (H₁ : a == b) (H₂ : b == c) : a == c :=
subst H₂ H₁
theorem trans_left (H₁ : a == b) (H₂ : b = b') : a == b' :=
trans H₁ (from_eq H₂)
theorem trans_right (H₁ : a = a') (H₂ : a' == b) : a == b :=
trans (from_eq H₁) H₂
theorem true_elim {a : Prop} (H : a == true) : a :=
eq_true_elim (heq.to_eq H)
end heq
calc_trans heq.trans
calc_trans heq.trans_left
calc_trans heq.trans_right
calc_symm heq.symm

14
library/logic/identities.lean
View file

@ -8,7 +8,7 @@
-- Useful logical identities. In the absence of propositional extensionality, some of the
-- calculations use the type class support provided by logic.instances
import logic.instances logic.decidable logic.quantifiers logic.cast
import logic.instances logic.quantifiers logic.cast
open relation decidable relation.iff_ops
@ -46,10 +46,10 @@ iff.intro
theorem not_not_elim {a : Prop} [D : decidable a] (H : ¬¬a) : a :=
iff.mp not_not_iff H
theorem not_true : (¬true) ↔ false :=
theorem not_true_iff_false : (¬true) ↔ false :=
iff.intro (assume H, H trivial) false_elim
theorem not_false : (¬false) ↔ true :=
theorem not_false_iff_true : (¬false) ↔ true :=
iff.intro (assume H, trivial) (assume H H', H')
theorem not_or {a b : Prop} [Da : decidable a] [Db : decidable b] : (¬(a ∨ b)) ↔ (¬a ∧ ¬b) :=
@ -104,7 +104,7 @@ theorem not_forall_exists {A : Type} {P : A → Prop} [D : ∀x, decidable (P x)
[D' : decidable (∃x, ¬P x)] (H : ¬∀x, P x) :
∃x, ¬P x :=
@by_contradiction _ D' (assume H1 : ¬∃x, ¬P x,
have H2 : ∀x, ¬¬P x, from @not_exists_forall _ _ (take x, not_decidable (D x)) H1,
have H2 : ∀x, ¬¬P x, from @not_exists_forall _ _ (take x, not.decidable (D x)) H1,
have H3 : ∀x, P x, from take x, @not_not_elim _ (D x) (H2 x),
absurd H3 H)
@ -120,7 +120,7 @@ iff.intro
theorem a_neq_a {A : Type} (a : A) : (a ≠ a) ↔ false :=
iff.intro
(assume H, a_neq_a_elim H)
(assume H, false.of_ne H)
(assume H, false_elim H)
theorem eq_id {A : Type} (a : A) : (a = a) ↔ true :=
@ -137,10 +137,10 @@ iff.intro
(assume H, false_elim H)
theorem true_eq_false : (true ↔ false) ↔ false :=
not_true ▸ (a_iff_not_a true)
not_true_iff_false ▸ (a_iff_not_a true)
theorem false_eq_true : (false ↔ true) ↔ false :=
not_false ▸ (a_iff_not_a false)
not_false_iff_true ▸ (a_iff_not_a false)
theorem a_eq_true (a : Prop) : (a ↔ true) ↔ a :=
iff.intro (assume H, iff.true_elim H) (assume H, iff_true_intro H)

80
library/logic/if.lean
View file

@ -1,80 +0,0 @@
----------------------------------------------------------------------------------------------------
-- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
-- Released under Apache 2.0 license as described in the file LICENSE.
-- Author: Leonardo de Moura
----------------------------------------------------------------------------------------------------
import logic.decidable tools.tactic
open decidable tactic eq.ops
definition ite (c : Prop) [H : decidable c] {A : Type} (t e : A) : A :=
decidable.rec_on H (λ Hc, t) (λ Hnc, e)
notation `if` c `then` t:45 `else` e:45 := ite c t e
definition if_pos {c : Prop} [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 (inl Hc) A t e))
(λ Hnc : ¬c, absurd Hc Hnc)
H
definition if_neg {c : Prop} [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 (inr Hnc) A t e))
H
definition if_t_t (c : Prop) [H : decidable c] {A : Type} (t : A) : (if c then t else t) = t :=
decidable.rec
(λ Hc : c, eq.refl (@ite c (inl Hc) A t t))
(λ Hnc : ¬c, eq.refl (@ite c (inr Hnc) A t t))
H
definition if_true {A : Type} (t e : A) : (if true then t else e) = t :=
if_pos trivial
definition if_false {A : Type} (t e : A) : (if false then t else e) = e :=
if_neg not_false_trivial
theorem if_cond_congr {c₁ c₂ : Prop} [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₂ : Prop} [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₂ : Prop} [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_iff_equiv H₁ Hc) A t₂ e₂) :=
have H2 [visible] : decidable c₂, from (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 : Prop) [H : decidable c] {A : Type} (t : c → A) (e : ¬ c → A) : A :=
decidable.rec_on H (λ Hc, t Hc) (λ Hnc, e Hnc)
notation `dif` c `then` t:45 `else` e:45 := dite c t e
definition dif_pos {c : Prop} [H : decidable c] (Hc : c) {A : Type} {t : c → A} {e : ¬ c → A} : (dif c then t else e) = t Hc :=
decidable.rec
(λ Hc : c, eq.refl (@dite c (inl Hc) A t e))
(λ Hnc : ¬c, absurd Hc Hnc)
H
definition dif_neg {c : Prop} [H : decidable c] (Hnc : ¬c) {A : Type} {t : c → A} {e : ¬ c → A} : (dif c then t else e) = e Hnc :=
decidable.rec
(λ Hc : c, absurd Hc Hnc)
(λ Hnc : ¬c, eq.refl (@dite c (inr Hnc) A t e))
H
-- Remark: dite and ite are "definitionally equal" when we ignore the proofs.
theorem dite_ite_eq (c : Prop) [H : decidable c] {A : Type} (t : A) (e : A) : dite c (λh, t) (λh, e) = ite c t e :=
rfl

27
library/logic/inhabited.lean
View file

@ -1,27 +0,0 @@
-- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
-- Released under Apache 2.0 license as described in the file LICENSE.
-- Authors: Leonardo de Moura, Jeremy Avigad
import logic.connectives
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 Prop_inhabited [instance] : inhabited Prop :=
mk true
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

2
library/logic/instances.lean
View file

@ -8,7 +8,7 @@ Author: Jeremy Avigad
Class instances for iff and eq.
-/
import logic.connectives algebra.relation
import algebra.relation
namespace relation

16
library/logic/nonempty.lean
View file

@ -1,16 +0,0 @@
-- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
-- Released under Apache 2.0 license as described in the file LICENSE.
-- Authors: Leonardo de Moura, Jeremy Avigad
import .inhabited
open inhabited
inductive nonempty [class] (A : Type) : Prop :=
intro : A → nonempty A
namespace nonempty
protected definition elim {A : Type} {B : Prop} (H1 : nonempty A) (H2 : A → B) : B :=
rec H2 H1
theorem inhabited_imp_nonempty [instance] {A : Type} (H : inhabited A) : nonempty A :=
intro (default A)
end nonempty

56
library/logic/prop.lean
View file

@ -1,56 +0,0 @@
-- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
-- Released under Apache 2.0 license as described in the file LICENSE.
-- Authors: Leonardo de Moura, Jeremy Avigad
import general_notation type
-- implication
-- -----------
definition imp (a b : Prop) : Prop := a → b
-- true and false
-- --------------
inductive false : Prop
-- make c explicit and rename to false.elim
theorem false_elim {c : Prop} (H : false) : c :=
false.rec c H
inductive true : Prop :=
intro : true
definition trivial := true.intro
definition not (a : Prop) := a → false
prefix `¬` := not
-- not
-- ---
--rename to not.intro or neg.intro
theorem not_intro {a : Prop} (H : a → false) : ¬a := H
--rename to not.elim or neg.elim
theorem not_elim {a : Prop} (H1 : ¬a) (H2 : a) : false := H1 H2
definition absurd {a : Prop} {b : Type} (H1 : a) (H2 : ¬a) : b :=
false.rec b (H2 H1)
theorem not_not_intro {a : Prop} (Ha : a) : ¬¬a :=
assume Hna : ¬a, absurd Ha Hna
theorem mt {a b : Prop} (H1 : a → b) (H2 : ¬b) : ¬a :=
assume Ha : a, absurd (H1 Ha) H2
theorem not_false_trivial : ¬false :=
assume H : false, H
theorem not_implies_left {a b : Prop} (H : ¬(a → b)) : ¬¬a :=
assume Hna : ¬a, absurd (assume Ha : a, absurd Ha Hna) H
theorem not_implies_right {a b : Prop} (H : ¬(a → b)) : ¬b :=
assume Hb : b, absurd (assume Ha : a, Hb) H

27
library/logic/quantifiers.lean
View file

@ -1,22 +1,8 @@
-- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
-- Released under Apache 2.0 license as described in the file LICENSE.
-- Authors: Leonardo de Moura, Jeremy Avigad
import logic.connectives logic.nonempty
open inhabited nonempty
inductive Exists {A : Type} (P : A → Prop) : Prop :=
intro : ∀ (a : A), P a → Exists P
definition exists_intro := @Exists.intro
notation `exists` binders `,` r:(scoped P, Exists P) := r
notation `∃` binders `,` r:(scoped P, Exists P) := r
theorem exists_elim {A : Type} {p : A → Prop} {B : Prop} (H1 : ∃x, p x) (H2 : ∀ (a : A) (H : p a), B) : B :=
Exists.rec H2 H1
theorem exists_not_forall {A : Type} {p : A → Prop} (H : ∃x, p x) : ¬∀x, ¬p x :=
assume H1 : ∀x, ¬p x,
obtain (w : A) (Hw : p w), from H,
@ -27,19 +13,6 @@ assume H1 : ∃x, ¬p x,
obtain (w : A) (Hw : ¬p w), from H1,
absurd (H2 w) Hw
definition exists_unique {A : Type} (p : A → Prop) :=
∃x, p x ∧ ∀y, p y → y = x
notation `∃!` binders `,` r:(scoped P, exists_unique P) := r
theorem exists_unique_intro {A : Type} {p : A → Prop} (w : A) (H1 : p w) (H2 : ∀y, p y → y = w) : ∃!x, p x :=
exists_intro w (and.intro H1 H2)
theorem exists_unique_elim {A : Type} {p : A → Prop} {b : Prop}
(H2 : ∃!x, p x) (H1 : ∀x, p x → (∀y, p y → y = x) → b) : b :=
obtain w Hw, from H2,
H1 w (and.elim_left Hw) (and.elim_right Hw)
theorem forall_congr {A : Type} {φ ψ : A → Prop} (H : ∀x, φ x ↔ ψ x) : (∀x, φ x) ↔ (∀x, ψ x) :=
iff.intro
(assume Hl, take x, iff.elim_left (H x) (Hl x))

34
library/logic/subsingleton.lean Normal file
View file

@ -0,0 +1,34 @@
/-
Copyright (c) 2014 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Floris van Doorn
-/
import logic.eq
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
end subsingleton
protected definition prop.subsingleton [instance] (P : Prop) : subsingleton P :=
subsingleton.intro (λa b, !proof_irrel)
theorem irrelevant [instance] (p : Prop) : subsingleton (decidable p) :=
subsingleton.intro (fun d1 d2,
decidable.rec
(assume Hp1 : p, decidable.rec
(assume Hp2 : p, congr_arg decidable.inl (eq.refl Hp1)) -- using proof irrelevance for Prop
(assume Hnp2 : ¬p, absurd Hp1 Hnp2)
d2)
(assume Hnp1 : ¬p, decidable.rec
(assume Hp2 : p, absurd Hp2 Hnp1)
(assume Hnp2 : ¬p, congr_arg decidable.inr (eq.refl Hnp1)) -- using proof irrelevance for Prop
d2)
d1)
protected theorem rec_subsingleton [instance] {p : Prop} [H : decidable p] {H1 : p → Type} {H2 : ¬p → Type}
(H3 : Π(h : p), subsingleton (H1 h)) (H4 : Π(h : ¬p), subsingleton (H2 h))
: subsingleton (decidable.rec_on H H1 H2) :=
decidable.rec_on H (λh, H3 h) (λh, H4 h) --this can be proven using dependent version of "by_cases"

4
library/priority.lean
View file

@ -1,4 +0,0 @@
import data.num.decl
definition std.priority.default : num := 1000
definition std.priority.max : num := 4294967295

2
library/standard.lean
View file

@ -7,4 +7,4 @@
-- The constructive core of Lean's library.
import type logic data tools.tactic
import logic data

1
library/tools/fake_simplifier.lean
View file

@ -1,4 +1,3 @@
import .tactic
open tactic
namespace fake_simplifier

2
library/tools/helper_tactics.lean
View file

@ -7,7 +7,7 @@
-- Useful tactics.
import tools.tactic logic.eq
import logic.eq
open tactic

10
library/type.lean
View file

@ -1,10 +0,0 @@
-- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
-- Released under Apache 2.0 license as described in the file LICENSE.
-- Authors: Leonardo de Moura
notation `Prop` := Type.{0}
notation [parsing-only] `Type'` := Type.{_+1}
notation [parsing-only] `Type₊` := Type.{_+1}
notation `Type₁` := Type.{1}
notation `Type₂` := Type.{2}
notation `Type₃` := Type.{3}