refactor(library/standard): organize files into a hierarchy

This commit is contained in:
Jeremy Avigad 2014-07-31 18:40:09 -07:00 committed by Leonardo de Moura
parent fbaf8b7e77
commit b2c2d1dd44
17 changed files with 87 additions and 31 deletions

View file

@ -0,0 +1,7 @@
----------------------------------------------------------------------------------------------------
-- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
-- Released under Apache 2.0 license as described in the file LICENSE.
-- Author: Jeremy Avigad
----------------------------------------------------------------------------------------------------
import data.list.basic

View file

@ -0,0 +1,7 @@
----------------------------------------------------------------------------------------------------
-- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
-- Released under Apache 2.0 license as described in the file LICENSE.
-- Author: Jeremy Avigad
----------------------------------------------------------------------------------------------------
import data.nat.nat1

View file

@ -1,7 +1,9 @@
-- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
------------------------------------------------------------------------------------------------------ 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
----------------------------------------------------------------------------------------------------
import logic.classes.inhabited
inductive option (A : Type) : Type :=
| none {} : option A

View file

@ -1,7 +1,9 @@
-- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
------------------------------------------------------------------------------------------------------ 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
----------------------------------------------------------------------------------------------------
import logic.classes.inhabited
namespace pair
inductive pair (A : Type) (B : Type) : Type :=

View file

@ -1,7 +1,9 @@
--- Copyright (c) 2014 Jeremy Avigad. All rights reserved.
------------------------------------------------------------------------------------------------------- Copyright (c) 2014 Jeremy Avigad. All rights reserved.
--- Released under Apache 2.0 license as described in the file LICENSE.
--- Author: Jeremy Avigad, Leonardo de Moura
import logic funext bool
----------------------------------------------------------------------------------------------------
import logic.axioms.funext data.bool
using eq_proofs bool
namespace set

View file

@ -1,7 +1,9 @@
-- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
------------------------------------------------------------------------------------------------------ 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
----------------------------------------------------------------------------------------------------
import logic.connectives.prop
namespace sum
inductive sum (A : Type) (B : Type) : Type :=

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 decidable
----------------------------------------------------------------------------------------------------
import logic.classes.decidable logic.classes.inhabited
using decidable
namespace unit

View file

@ -1,7 +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 logic cast
----------------------------------------------------------------------------------------------------
import logic.connectives.basic logic.connectives.quantifiers logic.connectives.cast
using eq_proofs
axiom prop_complete (a : Prop) : a = true a = false

View file

@ -1,7 +1,9 @@
-- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
------------------------------------------------------------------------------------------------------ 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 hilbert funext
-- Author: Leonardo de Moura
----------------------------------------------------------------------------------------------------
import logic.axioms.hilbert logic.axioms.funext
using eq_proofs
-- Diaconescus theorem

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 function
----------------------------------------------------------------------------------------------------
import logic.connectives.eq logic.connectives.function
using function
-- Function extensionality

View file

@ -1,7 +1,9 @@
-- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
------------------------------------------------------------------------------------------------------ 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
----------------------------------------------------------------------------------------------------
import logic.classes.inhabited
variable epsilon {A : Type} {H : inhabited A} (P : A → Prop) : A
axiom epsilon_ax {A : Type} {P : A → Prop} (Hex : ∃ a, P a) : P (@epsilon A (inhabited_exists Hex) P)

View file

@ -1,25 +1,32 @@
----------------------------------------------------------------------------------------------------
-- 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 cast
----------------------------------------------------------------------------------------------------
import logic.classes.inhabited logic.connectives.cast
-- Pi extensionality
axiom piext {A : Type} {B B' : A → Type} {H : inhabited (Π x, B x)} : (Π x, B x) = (Π x, B' x) → B = B'
axiom piext {A : Type} {B B' : A → Type} {H : inhabited (Π x, B x)} :
(Π x, B x) = (Π x, B' x) → B = B'
theorem cast_app {A : Type} {B B' : A → Type} (H : (Π x, B x) = (Π x, B' x)) (f : Π x, B x) (a : A) : cast H f a == f a :=
theorem cast_app {A : Type} {B B' : A → Type} (H : (Π x, B x) = (Π x, B' x)) (f : Π x, B x)
(a : A) : cast H f a == f a :=
have Hi [fact] : inhabited (Π x, B x), from inhabited_intro f,
have Hb : B = B', from piext H,
cast_app' Hb f a
theorem hcongr1 {A : Type} {B B' : A → Type} {f : Π x, B x} {f' : Π x, B' x} (a : A) (H : f == f') : f a == f' a :=
theorem hcongr1 {A : Type} {B B' : A → Type} {f : Π x, B x} {f' : Π x, B' x} (a : A)
(H : f == f') : f a == f' a :=
have Hi [fact] : inhabited (Π x, B x), from inhabited_intro f,
have Hb : B = B', from piext (type_eq H),
hcongr1' a H Hb
theorem hcongr {A A' : Type} {B : A → Type} {B' : A' → Type} {f : Π x, B x} {f' : Π x, B' x} {a : A} {a' : A'}
(Hff' : f == f') (Haa' : a == a') : f a == f' a' :=
theorem hcongr {A A' : Type} {B : A → Type} {B' : A' → Type}
{f : Π x, B x} {f' : Π x, B' x} {a : A} {a' : A'}
(Hff' : f == f') (Haa' : a == a') : f a == f' a' :=
have H1 : ∀ (B B' : A → Type) (f : Π x, B x) (f' : Π x, B' x), f == f' → f a == f' a, from
take B B' f f' e, hcongr1 a e,
have H2 : ∀ (B : A → Type) (B' : A' → Type) (f : Π x, B x) (f' : Π x, B' x), f == f' → f a == f' a', from
hsubst Haa' H1,
have H2 : ∀ (B : A → Type) (B' : A' → Type) (f : Π x, B x) (f' : Π x, B' x),
f == f' → f a == f' a', from hsubst Haa' H1,
H2 B B' f f' Hff'

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 classical hilbert decidable
----------------------------------------------------------------------------------------------------
import logic.axioms.classical logic.axioms.hilbert logic.classes.decidable
using decidable
-- Excluded middle + Hilbert implies every proposition is decidable

View file

@ -1,4 +1,6 @@
-- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
------------------------------------------------------------------------------------------------------ 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 tactic num string pair cast
----------------------------------------------------------------------------------------------------
import logic tools.tactic data.num data.string data.pair logic.connectives.cast

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
----------------------------------------------------------------------------------------------------
import logic.connectives.eq
using eq_proofs
namespace binary

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
----------------------------------------------------------------------------------------------------
import logic.connectives.prop
namespace equivalence
section

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 classical
----------------------------------------------------------------------------------------------------
import logic.axioms.classical
-- Well-founded relation definition
-- We are essentially saying that a relation R is well-founded
@ -28,4 +31,3 @@ by_contradiction (assume N : ¬∀x, P x,
have s2 : P r, from iH r s1,
have s3 : ¬P r, from and_elim_left Hr,
absurd s2 s3)