diff --git a/library/algebra/function.lean b/library/algebra/function.lean index 22aaf36ffa..4bb598290d 100644 --- a/library/algebra/function.lean +++ b/library/algebra/function.lean @@ -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} diff --git a/library/algebra/group.lean b/library/algebra/group.lean index 8be2b7cb12..b1adb386d9 100644 --- a/library/algebra/group.lean +++ b/library/algebra/group.lean @@ -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 diff --git a/library/algebra/order.lean b/library/algebra/order.lean index b2182ab179..25e4993ce6 100644 --- a/library/algebra/order.lean +++ b/library/algebra/order.lean @@ -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 diff --git a/library/algebra/ordered_group.lean b/library/algebra/ordered_group.lean index 721636d2a5..b3aaa2639e 100644 --- a/library/algebra/ordered_group.lean +++ b/library/algebra/ordered_group.lean @@ -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 diff --git a/library/algebra/relation.lean b/library/algebra/relation.lean index 4e60c45959..b8412353e3 100644 --- a/library/algebra/relation.lean +++ b/library/algebra/relation.lean @@ -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 -/ diff --git a/library/algebra/ring.lean b/library/algebra/ring.lean index 9033d1ba6c..cf42c9d91b 100644 --- a/library/algebra/ring.lean +++ b/library/algebra/ring.lean @@ -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 diff --git a/library/data/bool/decl.lean b/library/data/bool/decl.lean deleted file mode 100644 index 6eac93fb4d..0000000000 --- a/library/data/bool/decl.lean +++ /dev/null @@ -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 diff --git a/library/data/bool/default.lean b/library/data/bool/default.lean index 8d4c46ff6c..e34eb42e65 100644 --- a/library/data/bool/default.lean +++ b/library/data/bool/default.lean @@ -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 diff --git a/library/data/bool/thms.lean b/library/data/bool/thms.lean index 5539056e10..7b28f2609c 100644 --- a/library/data/bool/thms.lean +++ b/library/data/bool/thms.lean @@ -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 diff --git a/library/data/empty.lean b/library/data/empty.lean index e1fbcd9ada..d9f398127d 100644 --- a/library/data/empty.lean +++ b/library/data/empty.lean @@ -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 diff --git a/library/data/int/basic.lean b/library/data/int/basic.lean index fa8670a420..ce0d7bd5d5 100644 --- a/library/data/int/basic.lean +++ b/library/data/int/basic.lean @@ -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 diff --git a/library/data/list/basic.lean b/library/data/list/basic.lean index e7cd3009bd..dc0c3ff3a5 100644 --- a/library/data/list/basic.lean +++ b/library/data/list/basic.lean @@ -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 -- =========== diff --git a/library/data/nat/basic.lean b/library/data/nat/basic.lean index d0f0710832..9afb91f72e 100644 --- a/library/data/nat/basic.lean +++ b/library/data/nat/basic.lean @@ -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 diff --git a/library/data/nat/div.lean b/library/data/nat/div.lean index ac7b3370fb..53825bb55f 100644 --- a/library/data/nat/div.lean +++ b/library/data/nat/div.lean @@ -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 diff --git a/library/data/num/decl.lean b/library/data/num/decl.lean deleted file mode 100644 index f27e0e13a1..0000000000 --- a/library/data/num/decl.lean +++ /dev/null @@ -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 diff --git a/library/data/num/default.lean b/library/data/num/default.lean index 4fdc6da6c5..2d864d935d 100644 --- a/library/data/num/default.lean +++ b/library/data/num/default.lean @@ -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 diff --git a/library/data/num/thms.lean b/library/data/num/thms.lean index 087a62a166..21d40d0b69 100644 --- a/library/data/num/thms.lean +++ b/library/data/num/thms.lean @@ -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 diff --git a/library/data/option.lean b/library/data/option.lean index 193c903561..c2e3c1b324 100644 --- a/library/data/option.lean +++ b/library/data/option.lean @@ -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 diff --git a/library/data/prod/decl.lean b/library/data/prod/decl.lean deleted file mode 100644 index e7cd143aa8..0000000000 --- a/library/data/prod/decl.lean +++ /dev/null @@ -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 diff --git a/library/data/prod/default.lean b/library/data/prod/default.lean index d3e25a6d4f..968cf5aee6 100644 --- a/library/data/prod/default.lean +++ b/library/data/prod/default.lean @@ -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 diff --git a/library/data/prod/thms.lean b/library/data/prod/thms.lean index 088692a809..b354269214 100644 --- a/library/data/prod/thms.lean +++ b/library/data/prod/thms.lean @@ -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 diff --git a/library/data/quotient/basic.lean b/library/data/quotient/basic.lean index b91ad3cea3..ab3fdb212f 100644 --- a/library/data/quotient/basic.lean +++ b/library/data/quotient/basic.lean @@ -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 diff --git a/library/data/quotient/classical.lean b/library/data/quotient/classical.lean index 7729f8229d..c21609c83c 100644 --- a/library/data/quotient/classical.lean +++ b/library/data/quotient/classical.lean @@ -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 diff --git a/library/data/sigma/decl.lean b/library/data/sigma/decl.lean deleted file mode 100644 index 75af80744f..0000000000 --- a/library/data/sigma/decl.lean +++ /dev/null @@ -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 diff --git a/library/data/sigma/default.lean b/library/data/sigma/default.lean index ae9f0b096e..b2ab21f7fc 100644 --- a/library/data/sigma/default.lean +++ b/library/data/sigma/default.lean @@ -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 diff --git a/library/data/sigma/thms.lean b/library/data/sigma/thms.lean index 720b700bc0..0bc91aa30f 100644 --- a/library/data/sigma/thms.lean +++ b/library/data/sigma/thms.lean @@ -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 diff --git a/library/data/string/decl.lean b/library/data/string/decl.lean deleted file mode 100644 index 361fd6a5d2..0000000000 --- a/library/data/string/decl.lean +++ /dev/null @@ -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 diff --git a/library/data/string/default.lean b/library/data/string/default.lean index 1a20b29a43..081e1feb2c 100644 --- a/library/data/string/default.lean +++ b/library/data/string/default.lean @@ -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 diff --git a/library/data/string/thms.lean b/library/data/string/thms.lean index 30e045b35a..2858b8babd 100644 --- a/library/data/string/thms.lean +++ b/library/data/string/thms.lean @@ -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 diff --git a/library/data/subtype.lean b/library/data/subtype.lean index 78fc94bc1b..dbceffb92d 100644 --- a/library/data/subtype.lean +++ b/library/data/subtype.lean @@ -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) := diff --git a/library/data/sum.lean b/library/data/sum.lean index 4bd1674006..0f355b316a 100644 --- a/library/data/sum.lean +++ b/library/data/sum.lean @@ -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 diff --git a/library/data/unit/basic.lean b/library/data/unit/basic.lean deleted file mode 100644 index df303f48e0..0000000000 --- a/library/data/unit/basic.lean +++ /dev/null @@ -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 diff --git a/library/data/unit/decl.lean b/library/data/unit/decl.lean deleted file mode 100644 index 2860fbec1a..0000000000 --- a/library/data/unit/decl.lean +++ /dev/null @@ -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 diff --git a/library/data/unit/default.lean b/library/data/unit/default.lean index 7b2dbca50f..5c8eace3db 100644 --- a/library/data/unit/default.lean +++ b/library/data/unit/default.lean @@ -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 diff --git a/library/data/unit/insts.lean b/library/data/unit/insts.lean index 6f7cf442e4..69704064ca 100644 --- a/library/data/unit/insts.lean +++ b/library/data/unit/insts.lean @@ -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) diff --git a/library/data/unit/thms.lean b/library/data/unit/thms.lean index 1ac15428f5..571668fc62 100644 --- a/library/data/unit/thms.lean +++ b/library/data/unit/thms.lean @@ -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 := diff --git a/library/hott/path.lean b/library/hott/path.lean index 5850fbc36c..16044d2620 100644 --- a/library/hott/path.lean +++ b/library/hott/path.lean @@ -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 diff --git a/library/data/bool/ops.lean b/library/init/bool.lean similarity index 90% rename from library/data/bool/ops.lean rename to library/init/bool.lean index 2318ec5f92..4b7b08baf5 100644 --- a/library/data/bool/ops.lean +++ b/library/init/bool.lean @@ -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) := diff --git a/library/init/datatypes.lean b/library/init/datatypes.lean new file mode 100644 index 0000000000..a7b8f5bf2c --- /dev/null +++ b/library/init/datatypes.lean @@ -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 diff --git a/library/init/default.lean b/library/init/default.lean index cdddf8b436..41d8783c68 100644 --- a/library/init/default.lean +++ b/library/init/default.lean @@ -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 diff --git a/library/init/logic.lean b/library/init/logic.lean new file mode 100644 index 0000000000..fda94906fc --- /dev/null +++ b/library/init/logic.lean @@ -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 diff --git a/library/data/nat/decl.lean b/library/init/nat.lean similarity index 97% rename from library/data/nat/decl.lean rename to library/init/nat.lean index c203c1ac7e..a937da29fa 100644 --- a/library/data/nat/decl.lean +++ b/library/init/nat.lean @@ -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 diff --git a/library/data/num/ops.lean b/library/init/num.lean similarity index 79% rename from library/data/num/ops.lean rename to library/init/num.lean index b9b9bc0930..a3eed88bcd 100644 --- a/library/data/num/ops.lean +++ b/library/init/num.lean @@ -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 := diff --git a/library/init/priority.lean b/library/init/priority.lean new file mode 100644 index 0000000000..8a23b06957 --- /dev/null +++ b/library/init/priority.lean @@ -0,0 +1,10 @@ +/- +Copyright (c) 2014 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Authors: Leonardo de Moura +-/ +prelude +import init.datatypes +definition std.priority.default : num := 1000 +definition std.priority.max : num := 4294967295 diff --git a/library/data/prod/wf.lean b/library/init/prod.lean similarity index 80% rename from library/data/prod/wf.lean rename to library/init/prod.lean index ffbda1bad0..d9bc84388c 100644 --- a/library/data/prod/wf.lean +++ b/library/init/prod.lean @@ -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) diff --git a/library/logic/relation.lean b/library/init/relation.lean similarity index 86% rename from library/logic/relation.lean rename to library/init/relation.lean index e4613d88f9..6774c6b7c2 100644 --- a/library/logic/relation.lean +++ b/library/init/relation.lean @@ -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. diff --git a/library/general_notation.lean b/library/init/reserved_notation.lean similarity index 97% rename from library/general_notation.lean rename to library/init/reserved_notation.lean index ca0428be46..38ef1c3871 100644 --- a/library/general_notation.lean +++ b/library/init/reserved_notation.lean @@ -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 diff --git a/library/data/sigma/wf.lean b/library/init/sigma.lean similarity index 75% rename from library/data/sigma/wf.lean rename to library/init/sigma.lean index f035d580f3..2ec84d5a56 100644 --- a/library/data/sigma/wf.lean +++ b/library/init/sigma.lean @@ -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 diff --git a/library/tools/tactic.lean b/library/init/tactic.lean similarity index 85% rename from library/tools/tactic.lean rename to library/init/tactic.lean index 3301a95747..27be915884 100644 --- a/library/tools/tactic.lean +++ b/library/init/tactic.lean @@ -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 diff --git a/library/logic/wf.lean b/library/init/wf.lean similarity index 95% rename from library/logic/wf.lean rename to library/init/wf.lean index 4ce9fd92f6..db9d632b65 100644 --- a/library/logic/wf.lean +++ b/library/init/wf.lean @@ -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 diff --git a/library/logic/wf_k.lean b/library/init/wf_k.lean similarity index 95% rename from library/logic/wf_k.lean rename to library/init/wf_k.lean index 9c91cc2f65..03dde4d751 100644 --- a/library/logic/wf_k.lean +++ b/library/init/wf_k.lean @@ -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. diff --git a/library/logic/axioms/classical.lean b/library/logic/axioms/classical.lean index 19c6caba10..6dfa78d6ee 100644 --- a/library/logic/axioms/classical.lean +++ b/library/logic/axioms/classical.lean @@ -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 := diff --git a/library/logic/axioms/hilbert.lean b/library/logic/axioms/hilbert.lean index 7cd5debd4b..fa72569124 100644 --- a/library/logic/axioms/hilbert.lean +++ b/library/logic/axioms/hilbert.lean @@ -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 diff --git a/library/logic/axioms/prop_decidable.lean b/library/logic/axioms/prop_decidable.lean index 63b16a0231..2bac46053a 100644 --- a/library/logic/axioms/prop_decidable.lean +++ b/library/logic/axioms/prop_decidable.lean @@ -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 diff --git a/library/logic/cast.lean b/library/logic/cast.lean index 2e5f427783..ea5bb83005 100644 --- a/library/logic/cast.lean +++ b/library/logic/cast.lean @@ -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 diff --git a/library/logic/connectives.lean b/library/logic/connectives.lean deleted file mode 100644 index d380f20260..0000000000 --- a/library/logic/connectives.lean +++ /dev/null @@ -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 diff --git a/library/logic/decidable.lean b/library/logic/decidable.lean deleted file mode 100644 index 31ce10560d..0000000000 --- a/library/logic/decidable.lean +++ /dev/null @@ -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) diff --git a/library/logic/default.lean b/library/logic/default.lean index 1481ed31ca..3f3114f9e0 100644 --- a/library/logic/default.lean +++ b/library/logic/default.lean @@ -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 diff --git a/library/logic/eq.lean b/library/logic/eq.lean index 75d0942766..5491c007ca 100644 --- a/library/logic/eq.lean +++ b/library/logic/eq.lean @@ -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 @@ -96,20 +28,10 @@ namespace eq rec_on H b = rec_on H' b := drec_on H (λ(H' : f a = f a), !rec_on_id⁻¹) H' - theorem rec_on_irrel {a a' : A} {D : A → Type} (H H' : a = a') (b : D a) : + theorem rec_on_irrel {a a' : A} {D : A → Type} (H H' : a = a') (b : D a) : 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, @@ -135,7 +57,7 @@ section theorem congr_arg2 (f : A → B → C) (Ha : a = a') (Hb : b = b') : f a b = f a' b' := congr (congr_arg f Ha) Hb - theorem congr_arg3 (f : A → B → C → D) (Ha : a = a') (Hb : b = b') (Hc : c = c') + theorem congr_arg3 (f : A → B → C → D) (Ha : a = a') (Hb : b = b') (Hc : c = c') : f a b c = f a' b' c' := congr (congr_arg2 f Ha Hb) Hc @@ -143,24 +65,24 @@ section : f a b c d = f a' b' c' d' := congr (congr_arg3 f Ha Hb Hc) Hd - theorem congr_arg5 (f : A → B → C → D → E → F) - (Ha : a = a') (Hb : b = b') (Hc : c = c') (Hd : d = d') (He : e = e') + theorem congr_arg5 (f : A → B → C → D → E → F) + (Ha : a = a') (Hb : b = b') (Hc : c = c') (Hd : d = d') (He : e = e') : f a b c d e = f a' b' c' d' e' := congr (congr_arg4 f Ha Hb Hc Hd) He theorem congr2 (f f' : A → B → C) (Hf : f = f') (Ha : a = a') (Hb : b = b') : f a b = f' a' b' := Hf ▸ congr_arg2 f Ha Hb - theorem congr3 (f f' : A → B → C → D) (Hf : f = f') (Ha : a = a') (Hb : b = b') (Hc : c = c') + theorem congr3 (f f' : A → B → C → D) (Hf : f = f') (Ha : a = a') (Hb : b = b') (Hc : c = c') : f a b c = f' a' b' c' := Hf ▸ congr_arg3 f Ha Hb Hc - theorem congr4 (f f' : A → B → C → D → E) + theorem congr4 (f f' : A → B → C → D → E) (Hf : f = f') (Ha : a = a') (Hb : b = b') (Hc : c = c') (Hd : d = d') : f a b c d = f' a' b' c' d' := Hf ▸ congr_arg4 f Ha Hb Hc Hd - theorem congr5 (f f' : A → B → C → D → E → F) + theorem congr5 (f f' : A → B → C → D → E → F) (Hf : f = f') (Ha : a = a') (Hb : b = b') (Hc : c = c') (Hd : d = d') (He : e = e') : f a b c d e = f' a' b' c' d' e' := Hf ▸ congr_arg5 f Ha Hb Hc Hd He @@ -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) diff --git a/library/logic/heq.lean b/library/logic/heq.lean deleted file mode 100644 index 52c7b6866b..0000000000 --- a/library/logic/heq.lean +++ /dev/null @@ -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 diff --git a/library/logic/identities.lean b/library/logic/identities.lean index 0e609a9310..7cc97b1d34 100644 --- a/library/logic/identities.lean +++ b/library/logic/identities.lean @@ -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) diff --git a/library/logic/if.lean b/library/logic/if.lean deleted file mode 100644 index 2944aed52a..0000000000 --- a/library/logic/if.lean +++ /dev/null @@ -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 diff --git a/library/logic/inhabited.lean b/library/logic/inhabited.lean deleted file mode 100644 index 0ddb60662e..0000000000 --- a/library/logic/inhabited.lean +++ /dev/null @@ -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 diff --git a/library/logic/instances.lean b/library/logic/instances.lean index 44d1ebee75..c5b36b990c 100644 --- a/library/logic/instances.lean +++ b/library/logic/instances.lean @@ -8,7 +8,7 @@ Author: Jeremy Avigad Class instances for iff and eq. -/ -import logic.connectives algebra.relation +import algebra.relation namespace relation diff --git a/library/logic/nonempty.lean b/library/logic/nonempty.lean deleted file mode 100644 index c620c76da7..0000000000 --- a/library/logic/nonempty.lean +++ /dev/null @@ -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 diff --git a/library/logic/prop.lean b/library/logic/prop.lean deleted file mode 100644 index f2df940968..0000000000 --- a/library/logic/prop.lean +++ /dev/null @@ -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 diff --git a/library/logic/quantifiers.lean b/library/logic/quantifiers.lean index 97b4de1160..cd078af8a5 100644 --- a/library/logic/quantifiers.lean +++ b/library/logic/quantifiers.lean @@ -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)) diff --git a/library/logic/subsingleton.lean b/library/logic/subsingleton.lean new file mode 100644 index 0000000000..2efb271254 --- /dev/null +++ b/library/logic/subsingleton.lean @@ -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" diff --git a/library/priority.lean b/library/priority.lean deleted file mode 100644 index 930c7ec62f..0000000000 --- a/library/priority.lean +++ /dev/null @@ -1,4 +0,0 @@ -import data.num.decl - -definition std.priority.default : num := 1000 -definition std.priority.max : num := 4294967295 diff --git a/library/standard.lean b/library/standard.lean index 68fdba1c64..1e27aeb263 100644 --- a/library/standard.lean +++ b/library/standard.lean @@ -7,4 +7,4 @@ -- The constructive core of Lean's library. -import type logic data tools.tactic +import logic data diff --git a/library/tools/fake_simplifier.lean b/library/tools/fake_simplifier.lean index 2d01a65c3a..4f3bf07022 100644 --- a/library/tools/fake_simplifier.lean +++ b/library/tools/fake_simplifier.lean @@ -1,4 +1,3 @@ -import .tactic open tactic namespace fake_simplifier diff --git a/library/tools/helper_tactics.lean b/library/tools/helper_tactics.lean index cba7c953dc..0a1bf7fcc3 100644 --- a/library/tools/helper_tactics.lean +++ b/library/tools/helper_tactics.lean @@ -7,7 +7,7 @@ -- Useful tactics. -import tools.tactic logic.eq +import logic.eq open tactic diff --git a/library/type.lean b/library/type.lean deleted file mode 100644 index bc25cc3208..0000000000 --- a/library/type.lean +++ /dev/null @@ -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}