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

feat(library/standard): port int, and reorganize a lot

Browse source
This commit is contained in:
Jeremy Avigad 2014-08-19 19:32:44 -07:00 committed by Leonardo de Moura
parent ad26c7c93c
commit 148d475421
46 changed files with 2082 additions and 605 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
library/standard/data/bool/basic.lean → library/standard/data/bool.lean
View file

@ -2,8 +2,12 @@
-- Released under Apache 2.0 license as described in the file LICENSE.
-- Author: Leonardo de Moura
import .type logic.connectives.basic logic.classes.decidable logic.classes.inhabited
using eq_proofs decidable
import logic.connectives.basic logic.classes.decidable logic.classes.inhabited
using eq_ops decidable
inductive bool : Type :=
| ff : bool
| tt : bool
namespace bool
@ -11,7 +15,7 @@ theorem induction_on {p : bool → Prop} (b : bool) (H0 : p ff) (H1 : p tt) : p
bool_rec H0 H1 b
theorem inhabited_bool [instance] : inhabited bool :=
inhabited_intro ff
inhabited_mk ff
definition cond {A : Type} (b : bool) (t e : A) :=
bool_rec e t b
@ -136,4 +140,4 @@ theorem bnot_false : !ff = tt := refl _
theorem bnot_true : !tt = ff := refl _
end bool
end bool

7
library/standard/data/bool/bool.md
View file

@ -1,7 +0,0 @@
data.bool
=========
The type of booleans.
* [type](type.lean) : the datatype
* [basic](basic.lean) : basic properties

11
library/standard/data/bool/type.lean
View file

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

3
library/standard/data/data.md
View file

@ -7,7 +7,7 @@ Basic types:
* [empty](empty.lean) : the empty type
* [unit](unit.lean) : the singleton type
* [bool](bool/bool.md) : the boolean values
* [bool](bool.lean) : the boolean values
* [num](num.lean) : generic numerals
* [string](string.lean) : ascii strings
* [nat](nat/nat.md) : the natural numbers
@ -20,5 +20,6 @@ Constructors:
* [sigma](sigma.lean) : the dependent product
* [option](option.lean)
* [subtype](subtype.lean)
* [quotient](quotient/quotient.md)
* [list](list/list.md)
* [set](set.lean)

6
library/standard/data/default.lean Normal file
View file

@ -0,0 +1,6 @@
--- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
--- Released under Apache 2.0 license as described in the file LICENSE.
--- Author: Jeremy Avigad
import .empty .unit .bool .num .string .nat .int
import .prod .sum .sigma .option .subtype .quotient .list .set

1460
library/standard/data/int/basic.lean Normal file
View file

File diff suppressed because it is too large Load diff

2
library/standard/data/bool/default.lean → library/standard/data/int/default.lean
View file

@ -2,4 +2,4 @@
-- Released under Apache 2.0 license as described in the file LICENSE.
-- Author: Jeremy Avigad
import .type .basic
import data.nat.basic

5
library/standard/data/int/int.default Normal file
View file

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

6
library/standard/data/int/int.md Normal file
View file

@ -0,0 +1,6 @@
data.int
========
The integers.
* [basic](basic.lean) : the integers, with basic operations and order.

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

@ -15,7 +15,7 @@ import logic
-- import if -- for find
using nat
using eq_proofs
using eq_ops
namespace list

43
library/standard/data/nat/basic.lean
View file

@ -1,12 +1,11 @@
----------------------------------------------------------------------------------------------------
--- 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
----------------------------------------------------------------------------------------------------
import logic data.num tools.tactic struc.binary
using num tactic binary eq_proofs
using num tactic binary eq_ops
using decidable (hiding induction_on rec_on)
using relation -- for subst_iff
-- TODO: this should go in tools, I think
namespace helper_tactics
@ -29,7 +28,19 @@ inductive nat : Type :=
| zero : nat
| succ : nat → nat
notation `ℕ` : max := nat
notation `ℕ`:max := nat
theorem nat_rec_zero {P : ℕ → Type} (x : P zero) (f : ∀m, P m → P (succ m)) : nat_rec x f zero = x
theorem nat_rec_succ {P : ℕ → Type} (x : P zero) (f : ∀m, P m → P (succ m)) (n : ℕ) :
nat_rec x f (succ n) = f n (nat_rec x f n)
theorem induction_on {P : ℕ → Prop} (a : ℕ) (H1 : P zero) (H2 : ∀ (n : ℕ) (IH : P n), P (succ n)) :
P a :=
nat_rec H1 H2 a
definition rec_on {P : ℕ → Type} (n : ℕ) (H1 : P zero) (H2 : ∀m, P m → P (succ m)) : P n :=
nat_rec H1 H2 n
-- Coercion from num
@ -42,30 +53,20 @@ definition to_nat [coercion] [inline] (n : num) : ℕ :=
num_rec zero
(λ n, pos_num_rec (succ zero) (λ n r, plus r (plus r (succ zero))) (λ n r, plus r r) n) n
theorem nat_rec_zero {P : ℕ → Type} (x : P 0) (f : ∀m, P m → P (succ m)) : nat_rec x f 0 = x
theorem nat_rec_succ {P : ℕ → Type} (x : P 0) (f : ∀m, P m → P (succ m)) (n : ℕ) :
nat_rec x f (succ n) = f n (nat_rec x f n)
theorem induction_on {P : ℕ → Prop} (a : ℕ) (H1 : P 0) (H2 : ∀ (n : ℕ) (IH : P n), P (succ n)) :
P a :=
nat_rec H1 H2 a
definition rec_on {P : ℕ → Type} (n : ℕ) (H1 : P 0) (H2 : ∀m, P m → P (succ m)) : P n :=
nat_rec H1 H2 n
-- Successor and predecessor
-- -------------------------
-- TODO: this looks like a calc bug -- calc is using subst for iff, instead of =
calc_subst subst
theorem succ_ne_zero (n : ℕ) : succ n ≠ 0 :=
assume H : succ n = 0,
have H2 : true = false, from
let f [inline] := (nat_rec false (fun a b, true)) in
calc
true = f (succ n) : _
true = f (succ n) : rfl
... = f 0 : {H}
... = false : _,
... = false : rfl,
absurd H2 true_ne_false
-- add_rewrite succ_ne_zero
@ -82,7 +83,7 @@ theorem zero_or_succ_pred (n : ℕ) : n = 0 ∨ n = succ (pred n) :=
induction_on n
(or_inl (refl 0))
(take m IH, or_inr
(show succ m = succ (pred (succ m)), from congr2 succ (pred_succ m⁻¹)))
(show succ m = succ (pred (succ m)), from congr_arg succ (pred_succ m⁻¹)))
theorem zero_or_exists_succ (n : ℕ) : n = 0 ∨ ∃k, n = succ k :=
or_imp_or (zero_or_succ_pred n) (assume H, H)
@ -122,7 +123,7 @@ have general : ∀n, decidable (n = m), from
(λ (n' : ℕ) (iH2 : decidable (n' = succ m')),
have d1 : decidable (n' = m'), from iH1 n',
decidable.rec_on d1
(assume Heq : n' = m', inl (congr2 succ Heq))
(assume Heq : n' = m', inl (congr_arg succ Heq))
(assume Hne : n' ≠ m',
have H1 : succ n' ≠ succ m', from
assume Heq, absurd (succ_inj Heq) Hne,
@ -415,4 +416,4 @@ discriminate
-- add_rewrite mul_succ_left mul_succ_right
-- add_rewrite mul_comm mul_assoc mul_left_comm
-- add_rewrite mul_distr_right mul_distr_left
end nat
end nat

11
library/standard/data/nat/order.lean
View file

@ -1,14 +1,12 @@
----------------------------------------------------------------------------------------------------
--- 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
----------------------------------------------------------------------------------------------------
import .basic
using nat eq_proofs tactic
import tools.fake_simplifier
-- until we have the simplifier...
definition simp : tactic := apply @sorry
using nat eq_ops tactic
using fake_simplifier
-- TODO: move these to logic.connectives
theorem or_imp_or_left {a b c : Prop} (H1 : a ∨ b) (H2 : a → c) : c ∨ b :=
@ -30,7 +28,6 @@ namespace nat
definition le (n m : ℕ) : Prop := exists k : nat, n + k = m
infix `<=`:50 := le
infix `≤`:50 := le
theorem le_intro {n m k : ℕ} (H : n + k = m) : n ≤ m :=
@ -583,4 +580,4 @@ mul_eq_one_left ((mul_comm n m) ▸ H)
--- theorem mul_eq_one {n m : ℕ} (H : n * m = 1) : n = 1 ∧ m = 1
--- := and_intro (mul_eq_one_left H) (mul_eq_one_right H)
end nat
end nat

10
library/standard/data/nat/sub.lean
View file

@ -1,13 +1,15 @@
----------------------------------------------------------------------------------------------------
--- 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
----------------------------------------------------------------------------------------------------
import data.nat.order
using nat eq_proofs tactic
import tools.fake_simplifier
using nat eq_ops tactic
using helper_tactics
using fake_simplifier
namespace nat
-- data.nat.basic2
@ -508,4 +510,4 @@ or_elim (le_total k l)
(assume H : k ≤ l, dist_comm l k ▸ dist_comm _ _ ▸ aux l k H)
(assume H : l ≤ k, aux k l H)
end nat
end nat

6
library/standard/data/num.lean
View file

@ -21,9 +21,9 @@ inductive num : Type :=
| pos : pos_num → num
theorem inhabited_pos_num [instance] : inhabited pos_num :=
inhabited_intro one
inhabited_mk one
theorem inhabited_num [instance] : inhabited num :=
inhabited_intro zero
inhabited_mk zero
end num
end num

8
library/standard/data/option.lean
View file

@ -4,7 +4,7 @@
-- Author: Leonardo de Moura
----------------------------------------------------------------------------------------------------
import logic.connectives.basic logic.connectives.eq logic.classes.inhabited logic.classes.decidable
using eq_proofs decidable
using eq_ops decidable
namespace option
inductive option (A : Type) : Type :=
@ -32,10 +32,10 @@ assume H : none = some a, absurd
(not_is_none_some a)
theorem some_inj {A : Type} {a₁ a₂ : A} (H : some a₁ = some a₂) : a₁ = a₂ :=
congr2 (option_rec a₁ (λ a, a)) H
congr_arg (option_rec a₁ (λ a, a)) H
theorem inhabited_option [instance] (A : Type) : inhabited (option A) :=
inhabited_intro none
inhabited_mk none
theorem decidable_eq [instance] {A : Type} {H : ∀a₁ a₂ : A, decidable (a₁ = a₂)} (o₁ o₂ : option A) : decidable (o₁ = o₂) :=
rec_on o₁
@ -45,4 +45,4 @@ rec_on o₁
(take a₂ : A, decidable.rec_on (H a₁ a₂)
(assume Heq : a₁ = a₂, inl (Heq ▸ refl _))
(assume Hne : a₁ ≠ a₂, inr (assume Hn : some a₁ = some a₂, absurd (some_inj Hn) Hne))))
end option
end option

6
library/standard/data/prod.lean
View file

@ -4,6 +4,8 @@
import logic.classes.inhabited logic.connectives.eq
using inhabited
inductive prod (A B : Type) : Type :=
| pair : A → B → prod A B
@ -39,10 +41,10 @@ section
pair_destruct p1 (take a1 b1, pair_destruct p2 (take a2 b2 H1 H2, pair_eq H1 H2))
theorem prod_inhabited (H1 : inhabited A) (H2 : inhabited B) : inhabited (prod A B) :=
inhabited_elim H1 (λa, inhabited_elim H2 (λb, inhabited_intro (pair a b)))
inhabited_destruct H1 (λa, inhabited_destruct H2 (λb, inhabited_mk (pair a b)))
end
instance prod_inhabited
end prod
end prod

175
library/standard/data/quotient/aux.lean Normal file
View file

@ -0,0 +1,175 @@
-- 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
import logic ..prod struc.relation
import tools.fake_simplifier
using prod eq_ops
using fake_simplifier
-- TODO: calc bug -- remove
calc_subst subst
namespace quotient
-- auxliary facts about products
-- -----------------------------
-- ### flip
definition flip {A B : Type} (a : A × B) : B × A := pair (pr2 a) (pr1 a)
theorem flip_def {A B : Type} (a : A × B) : flip a = pair (pr2 a) (pr1 a) := refl (flip a)
theorem flip_pair {A B : Type} (a : A) (b : B) : flip (pair a b) = pair b a := rfl
theorem flip_pr1 {A B : Type} (a : A × B) : pr1 (flip a) = pr2 a := rfl
theorem flip_pr2 {A B : Type} (a : A × B) : pr2 (flip a) = pr1 a := rfl
theorem flip_flip {A B : Type} (a : A × B) : flip (flip a) = a :=
pair_destruct a (take x y, rfl)
theorem P_flip {A B : Type} {P : A → B → Prop} {a : A × B} (H : P (pr1 a) (pr2 a))
: P (pr2 (flip a)) (pr1 (flip a)) :=
(symm (flip_pr1 a)) ▸ (symm (flip_pr2 a)) ▸ H
theorem flip_inj {A B : Type} {a b : A × B} (H : flip a = flip b) : a = b :=
have H2 : flip (flip a) = flip (flip b), from congr_arg flip H,
show a = b, from (flip_flip a) ▸ (flip_flip b) ▸ H2
-- ### coordinatewise unary maps
definition map_pair {A B : Type} (f : A → B) (a : A × A) : B × B :=
pair (f (pr1 a)) (f (pr2 a))
theorem map_pair_def {A B : Type} (f : A → B) (a : A × A)
: map_pair f a = pair (f (pr1 a)) (f (pr2 a)) :=
rfl
theorem map_pair_pair {A B : Type} (f : A → B) (a a' : A)
: map_pair f (pair a a') = pair (f a) (f a') :=
(pr1_pair a a') ▸ (pr2_pair a a') ▸ (rfl)
theorem map_pair_pr1 {A B : Type} (f : A → B) (a : A × A) : pr1 (map_pair f a) = f (pr1 a) :=
pr1_pair _ _
theorem map_pair_pr2 {A B : Type} (f : A → B) (a : A × A) : pr2 (map_pair f a) = f (pr2 a) :=
pr2_pair _ _
-- ### coordinatewise binary maps
definition map_pair2 {A B C : Type} (f : A → B → C) (a : A × A) (b : B × B) : C × C :=
pair (f (pr1 a) (pr1 b)) (f (pr2 a) (pr2 b))
theorem map_pair2_def {A B C : Type} (f : A → B → C) (a : A × A) (b : B × B) :
map_pair2 f a b = pair (f (pr1 a) (pr1 b)) (f (pr2 a) (pr2 b)) := rfl
theorem map_pair2_pair {A B C : Type} (f : A → B → C) (a a' : A) (b b' : B) :
map_pair2 f (pair a a') (pair b b') = pair (f a b) (f a' b') :=
calc
map_pair2 f (pair a a') (pair b b')
= pair (f (pr1 (pair a a')) b) (f (pr2 (pair a a')) (pr2 (pair b b')))
: {pr1_pair b b'}
... = pair (f (pr1 (pair a a')) b) (f (pr2 (pair a a')) b') : {pr2_pair b b'}
... = pair (f (pr1 (pair a a')) b) (f a' b') : {pr2_pair a a'}
... = pair (f a b) (f a' b') : {pr1_pair a a'}
theorem map_pair2_pr1 {A B C : Type} (f : A → B → C) (a : A × A) (b : B × B) :
pr1 (map_pair2 f a b) = f (pr1 a) (pr1 b) := pr1_pair _ _
theorem map_pair2_pr2 {A B C : Type} (f : A → B → C) (a : A × A) (b : B × B) :
pr2 (map_pair2 f a b) = f (pr2 a) (pr2 b) := pr2_pair _ _
theorem map_pair2_flip {A B C : Type} (f : A → B → C) (a : A × A) (b : B × B) :
flip (map_pair2 f a b) = map_pair2 f (flip a) (flip b) :=
have Hx : pr1 (flip (map_pair2 f a b)) = pr1 (map_pair2 f (flip a) (flip b)), from
calc
pr1 (flip (map_pair2 f a b)) = pr2 (map_pair2 f a b) : flip_pr1 _
... = f (pr2 a) (pr2 b) : map_pair2_pr2 f a b
... = f (pr1 (flip a)) (pr2 b) : {symm (flip_pr1 a)}
... = f (pr1 (flip a)) (pr1 (flip b)) : {symm (flip_pr1 b)}
... = pr1 (map_pair2 f (flip a) (flip b)) : symm (map_pair2_pr1 f _ _),
have Hy : pr2 (flip (map_pair2 f a b)) = pr2 (map_pair2 f (flip a) (flip b)), from
calc
pr2 (flip (map_pair2 f a b)) = pr1 (map_pair2 f a b) : flip_pr2 _
... = f (pr1 a) (pr1 b) : map_pair2_pr1 f a b
... = f (pr2 (flip a)) (pr1 b) : {symm (flip_pr2 a)}
... = f (pr2 (flip a)) (pr2 (flip b)) : {symm (flip_pr2 b)}
... = pr2 (map_pair2 f (flip a) (flip b)) : symm (map_pair2_pr2 f _ _),
pair_eq Hx Hy
-- add_rewrite flip_pr1 flip_pr2 flip_pair
-- add_rewrite map_pair_pr1 map_pair_pr2 map_pair_pair
-- add_rewrite map_pair2_pr1 map_pair2_pr2 map_pair2_pair
theorem map_pair2_comm {A B : Type} {f : A → A → B} (Hcomm : ∀a b : A, f a b = f b a)
(v w : A × A) : map_pair2 f v w = map_pair2 f w v :=
have Hx : pr1 (map_pair2 f v w) = pr1 (map_pair2 f w v), from
calc
pr1 (map_pair2 f v w) = f (pr1 v) (pr1 w) : map_pair2_pr1 f v w
... = f (pr1 w) (pr1 v) : Hcomm _ _
... = pr1 (map_pair2 f w v) : symm (map_pair2_pr1 f w v),
have Hy : pr2 (map_pair2 f v w) = pr2 (map_pair2 f w v), from
calc
pr2 (map_pair2 f v w) = f (pr2 v) (pr2 w) : map_pair2_pr2 f v w
... = f (pr2 w) (pr2 v) : Hcomm _ _
... = pr2 (map_pair2 f w v) : symm (map_pair2_pr2 f w v),
pair_eq Hx Hy
theorem map_pair2_assoc {A : Type} {f : A → A → A}
(Hassoc : ∀a b c : A, f (f a b) c = f a (f b c)) (u v w : A × A) :
map_pair2 f (map_pair2 f u v) w = map_pair2 f u (map_pair2 f v w) :=
have Hx : pr1 (map_pair2 f (map_pair2 f u v) w) =
pr1 (map_pair2 f u (map_pair2 f v w)), from
calc
pr1 (map_pair2 f (map_pair2 f u v) w)
= f (pr1 (map_pair2 f u v)) (pr1 w) : map_pair2_pr1 f _ _
... = f (f (pr1 u) (pr1 v)) (pr1 w) : {map_pair2_pr1 f _ _}
... = f (pr1 u) (f (pr1 v) (pr1 w)) : Hassoc (pr1 u) (pr1 v) (pr1 w)
... = f (pr1 u) (pr1 (map_pair2 f v w)) : {symm (map_pair2_pr1 f _ _)}
... = pr1 (map_pair2 f u (map_pair2 f v w)) : symm (map_pair2_pr1 f _ _),
have Hy : pr2 (map_pair2 f (map_pair2 f u v) w) =
pr2 (map_pair2 f u (map_pair2 f v w)), from
calc
pr2 (map_pair2 f (map_pair2 f u v) w)
= f (pr2 (map_pair2 f u v)) (pr2 w) : map_pair2_pr2 f _ _
... = f (f (pr2 u) (pr2 v)) (pr2 w) : {map_pair2_pr2 f _ _}
... = f (pr2 u) (f (pr2 v) (pr2 w)) : Hassoc (pr2 u) (pr2 v) (pr2 w)
... = f (pr2 u) (pr2 (map_pair2 f v w)) : {symm (map_pair2_pr2 f _ _)}
... = pr2 (map_pair2 f u (map_pair2 f v w)) : symm (map_pair2_pr2 f _ _),
pair_eq Hx Hy
theorem map_pair2_id_right {A B : Type} {f : A → B → A} {e : B} (Hid : ∀a : A, f a e = a)
(v : A × A) : map_pair2 f v (pair e e) = v :=
have Hx : pr1 (map_pair2 f v (pair e e)) = pr1 v, from
(calc
pr1 (map_pair2 f v (pair e e)) = f (pr1 v) (pr1 (pair e e)) : by simp
... = f (pr1 v) e : by simp
... = pr1 v : Hid (pr1 v)),
have Hy : pr2 (map_pair2 f v (pair e e)) = pr2 v, from
(calc
pr2 (map_pair2 f v (pair e e)) = f (pr2 v) (pr2 (pair e e)) : by simp
... = f (pr2 v) e : by simp
... = pr2 v : Hid (pr2 v)),
prod_eq Hx Hy
theorem map_pair2_id_left {A B : Type} {f : B → A → A} {e : B} (Hid : ∀a : A, f e a = a)
(v : A × A) : map_pair2 f (pair e e) v = v :=
have Hx : pr1 (map_pair2 f (pair e e) v) = pr1 v, from
calc
pr1 (map_pair2 f (pair e e) v) = f (pr1 (pair e e)) (pr1 v) : by simp
... = f e (pr1 v) : by simp
... = pr1 v : Hid (pr1 v),
have Hy : pr2 (map_pair2 f (pair e e) v) = pr2 v, from
calc
pr2 (map_pair2 f (pair e e) v) = f (pr2 (pair e e)) (pr2 v) : by simp
... = f e (pr2 v) : by simp
... = pr2 v : Hid (pr2 v),
prod_eq Hx Hy
opaque_hint (hiding flip map_pair map_pair2)
end quotient

306
library/standard/data/quotient.lean → library/standard/data/quotient/basic.lean
View file

@ -2,197 +2,11 @@
-- Released under Apache 2.0 license as described in the file LICENSE.
-- Author: Floris van Doorn
import logic tools.tactic .subtype logic.connectives.cast struc.relation data.prod
import logic tools.tactic ..subtype logic.connectives.cast struc.relation data.prod
import logic.connectives.instances
import .aux
-- for now: to use substitution (iff_to_eq)
import logic.axioms.classical
-- for the last section
import logic.axioms.hilbert logic.axioms.funext
using relation prod tactic eq_proofs
-- temporary: substiution for iff
theorem substi {a b : Prop} {P : Prop → Prop} (H1 : a ↔ b) (H2 : P a) : P b :=
subst (iff_to_eq H1) H2
theorem transi {a b c : Prop} (H1 : a ↔ b) (H2 : b ↔ c) : a ↔ c :=
eq_to_iff (trans (iff_to_eq H1) (iff_to_eq H2))
theorem symmi {a b : Prop} (H : a ↔ b) : b ↔ a :=
eq_to_iff (symm (iff_to_eq H))
-- until we have the simplifier...
definition simp : tactic := apply @sorry
-- TODO: find a better name, and move to logic.connectives.basic
theorem and_inhabited_left {a : Prop} (b : Prop) (Ha : a) : a ∧ b ↔ b :=
iff_intro (take Hab, and_elim_right Hab) (take Hb, and_intro Ha Hb)
-- auxliary facts about products
-- -----------------------------
-- TODO: move to data.prod?
-- ### flip
definition flip {A B : Type} (a : A × B) : B × A := pair (pr2 a) (pr1 a)
theorem flip_def {A B : Type} (a : A × B) : flip a = pair (pr2 a) (pr1 a) := refl (flip a)
theorem flip_pair {A B : Type} (a : A) (b : B) : flip (pair a b) = pair b a := rfl
theorem flip_pr1 {A B : Type} (a : A × B) : pr1 (flip a) = pr2 a := rfl
theorem flip_pr2 {A B : Type} (a : A × B) : pr2 (flip a) = pr1 a := rfl
theorem flip_flip {A B : Type} (a : A × B) : flip (flip a) = a :=
pair_destruct a (take x y, rfl)
theorem P_flip {A B : Type} {P : A → B → Prop} {a : A × B} (H : P (pr1 a) (pr2 a))
: P (pr2 (flip a)) (pr1 (flip a)) :=
(symm (flip_pr1 a)) ▸ (symm (flip_pr2 a)) ▸ H
theorem flip_inj {A B : Type} {a b : A × B} (H : flip a = flip b) : a = b :=
have H2 : flip (flip a) = flip (flip b), from congr2 flip H,
show a = b, from (flip_flip a) ▸ (flip_flip b) ▸ H2
-- ### coordinatewise unary maps
definition map_pair {A B : Type} (f : A → B) (a : A × A) : B × B :=
pair (f (pr1 a)) (f (pr2 a))
theorem map_pair_def {A B : Type} (f : A → B) (a : A × A)
: map_pair f a = pair (f (pr1 a)) (f (pr2 a)) :=
rfl
theorem map_pair_pair {A B : Type} (f : A → B) (a a' : A)
: map_pair f (pair a a') = pair (f a) (f a') :=
(pr1_pair a a') ▸ (pr2_pair a a') ▸ (rfl)
theorem map_pair_pr1 {A B : Type} (f : A → B) (a : A × A) : pr1 (map_pair f a) = f (pr1 a)
:= pr1_pair _ _
theorem map_pair_pr2 {A B : Type} (f : A → B) (a : A × A) : pr2 (map_pair f a) = f (pr2 a)
:= pr2_pair _ _
-- ### coordinatewise binary maps
definition map_pair2 {A B C : Type} (f : A → B → C) (a : A × A) (b : B × B) : C × C
:= pair (f (pr1 a) (pr1 b)) (f (pr2 a) (pr2 b))
theorem map_pair2_def {A B C : Type} (f : A → B → C) (a : A × A) (b : B × B)
: map_pair2 f a b = pair (f (pr1 a) (pr1 b)) (f (pr2 a) (pr2 b)) := rfl
theorem map_pair2_pair {A B C : Type} (f : A → B → C) (a a' : A) (b b' : B)
: map_pair2 f (pair a a') (pair b b') = pair (f a b) (f a' b') :=
calc
map_pair2 f (pair a a') (pair b b')
= pair (f (pr1 (pair a a')) b) (f (pr2 (pair a a')) (pr2 (pair b b')))
: {pr1_pair b b'}
... = pair (f (pr1 (pair a a')) b) (f (pr2 (pair a a')) b') : {pr2_pair b b'}
... = pair (f (pr1 (pair a a')) b) (f a' b') : {pr2_pair a a'}
... = pair (f a b) (f a' b') : {pr1_pair a a'}
theorem map_pair2_pr1 {A B C : Type} (f : A → B → C) (a : A × A) (b : B × B)
: pr1 (map_pair2 f a b) = f (pr1 a) (pr1 b) := pr1_pair _ _
theorem map_pair2_pr2 {A B C : Type} (f : A → B → C) (a : A × A) (b : B × B)
: pr2 (map_pair2 f a b) = f (pr2 a) (pr2 b) := pr2_pair _ _
theorem map_pair2_flip {A B C : Type} (f : A → B → C) (a : A × A) (b : B × B)
: flip (map_pair2 f a b) = map_pair2 f (flip a) (flip b) :=
have Hx : pr1 (flip (map_pair2 f a b)) = pr1 (map_pair2 f (flip a) (flip b)), from
calc
pr1 (flip (map_pair2 f a b)) = pr2 (map_pair2 f a b) : flip_pr1 _
... = f (pr2 a) (pr2 b) : map_pair2_pr2 f a b
... = f (pr1 (flip a)) (pr2 b) : {symm (flip_pr1 a)}
... = f (pr1 (flip a)) (pr1 (flip b)) : {symm (flip_pr1 b)}
... = pr1 (map_pair2 f (flip a) (flip b)) : symm (map_pair2_pr1 f _ _),
have Hy : pr2 (flip (map_pair2 f a b)) = pr2 (map_pair2 f (flip a) (flip b)), from
calc
pr2 (flip (map_pair2 f a b)) = pr1 (map_pair2 f a b) : flip_pr2 _
... = f (pr1 a) (pr1 b) : map_pair2_pr1 f a b
... = f (pr2 (flip a)) (pr1 b) : {symm (flip_pr2 a)}
... = f (pr2 (flip a)) (pr2 (flip b)) : {symm (flip_pr2 b)}
... = pr2 (map_pair2 f (flip a) (flip b)) : symm (map_pair2_pr2 f _ _),
pair_eq Hx Hy
-- add_rewrite flip_pr1 flip_pr2 flip_pair
-- add_rewrite map_pair_pr1 map_pair_pr2 map_pair_pair
-- add_rewrite map_pair2_pr1 map_pair2_pr2 map_pair2_pair
theorem map_pair2_comm {A B : Type} {f : A → A → B} (Hcomm : ∀a b : A, f a b = f b a)
(v w : A × A) : map_pair2 f v w = map_pair2 f w v :=
have Hx : pr1 (map_pair2 f v w) = pr1 (map_pair2 f w v), from
calc
pr1 (map_pair2 f v w) = f (pr1 v) (pr1 w) : map_pair2_pr1 f v w
... = f (pr1 w) (pr1 v) : Hcomm _ _
... = pr1 (map_pair2 f w v) : symm (map_pair2_pr1 f w v),
have Hy : pr2 (map_pair2 f v w) = pr2 (map_pair2 f w v), from
calc
pr2 (map_pair2 f v w) = f (pr2 v) (pr2 w) : map_pair2_pr2 f v w
... = f (pr2 w) (pr2 v) : Hcomm _ _
... = pr2 (map_pair2 f w v) : symm (map_pair2_pr2 f w v),
pair_eq Hx Hy
theorem map_pair2_assoc {A : Type} {f : A → A → A}
(Hassoc : ∀a b c : A, f (f a b) c = f a (f b c)) (u v w : A × A) :
map_pair2 f (map_pair2 f u v) w = map_pair2 f u (map_pair2 f v w) :=
have Hx : pr1 (map_pair2 f (map_pair2 f u v) w) =
pr1 (map_pair2 f u (map_pair2 f v w)), from
calc
pr1 (map_pair2 f (map_pair2 f u v) w)
= f (pr1 (map_pair2 f u v)) (pr1 w) : map_pair2_pr1 f _ _
... = f (f (pr1 u) (pr1 v)) (pr1 w) : {map_pair2_pr1 f _ _}
... = f (pr1 u) (f (pr1 v) (pr1 w)) : Hassoc (pr1 u) (pr1 v) (pr1 w)
... = f (pr1 u) (pr1 (map_pair2 f v w)) : {symm (map_pair2_pr1 f _ _)}
... = pr1 (map_pair2 f u (map_pair2 f v w)) : symm (map_pair2_pr1 f _ _),
have Hy : pr2 (map_pair2 f (map_pair2 f u v) w) =
pr2 (map_pair2 f u (map_pair2 f v w)), from
calc
pr2 (map_pair2 f (map_pair2 f u v) w)
= f (pr2 (map_pair2 f u v)) (pr2 w) : map_pair2_pr2 f _ _
... = f (f (pr2 u) (pr2 v)) (pr2 w) : {map_pair2_pr2 f _ _}
... = f (pr2 u) (f (pr2 v) (pr2 w)) : Hassoc (pr2 u) (pr2 v) (pr2 w)
... = f (pr2 u) (pr2 (map_pair2 f v w)) : {symm (map_pair2_pr2 f _ _)}
... = pr2 (map_pair2 f u (map_pair2 f v w)) : symm (map_pair2_pr2 f _ _),
pair_eq Hx Hy
theorem map_pair2_id_right {A B : Type} {f : A → B → A} {e : B} (Hid : ∀a : A, f a e = a)
(v : A × A) : map_pair2 f v (pair e e) = v :=
have Hx : pr1 (map_pair2 f v (pair e e)) = pr1 v, from
(calc
pr1 (map_pair2 f v (pair e e)) = f (pr1 v) (pr1 (pair e e)) : by simp
... = f (pr1 v) e : by simp
... = pr1 v : Hid (pr1 v)),
have Hy : pr2 (map_pair2 f v (pair e e)) = pr2 v, from
(calc
pr2 (map_pair2 f v (pair e e)) = f (pr2 v) (pr2 (pair e e)) : by simp
... = f (pr2 v) e : by simp
... = pr2 v : Hid (pr2 v)),
prod_eq Hx Hy
theorem map_pair2_id_left {A B : Type} {f : B → A → A} {e : B} (Hid : ∀a : A, f e a = a)
(v : A × A) : map_pair2 f (pair e e) v = v :=
have Hx : pr1 (map_pair2 f (pair e e) v) = pr1 v, from
calc
pr1 (map_pair2 f (pair e e) v) = f (pr1 (pair e e)) (pr1 v) : by simp
... = f e (pr1 v) : by simp
... = pr1 v : Hid (pr1 v),
have Hy : pr2 (map_pair2 f (pair e e) v) = pr2 v, from
calc
pr2 (map_pair2 f (pair e e) v) = f (pr2 (pair e e)) (pr2 v) : by simp
... = f e (pr2 v) : by simp
... = pr2 v : Hid (pr2 v),
prod_eq Hx Hy
opaque_hint (hiding flip map_pair map_pair2)
using relation prod inhabited nonempty tactic eq_ops
-- Theory data.quotient
-- ====================
@ -205,7 +19,7 @@ using subtype
-- ---------------------
-- TODO: make this a structure
definition is_quotient {A B : Type} (R : A → A → Prop) (abs : A → B) (rep : B → A) : Prop :=
abbreviation is_quotient {A B : Type} (R : A → A → Prop) (abs : A → B) (rep : B → A) : Prop :=
(∀b, abs (rep b) = b) ∧
(∀b, R (rep b) (rep b)) ∧
(∀r s, R r s ↔ (R r r ∧ R s s ∧ abs r = abs s))
@ -224,8 +38,8 @@ and_intro H1 (and_intro H2 H3)
-- (take r s,
-- have H4 : R r s ↔ R s s ∧ abs r = abs s,
-- from
-- gensubst.subst (relation.operations.symm (and_inhabited_left _ (H1 s))) (H3 r s),
-- gensubst.subst (relation.operations.symm (and_inhabited_left _ (H1 r))) H4)
-- gensubst.subst (relation.operations.symm (and_absorb_left _ (H1 s))) (H3 r s),
-- gensubst.subst (relation.operations.symm (and_absorb_left _ (H1 r))) H4)
-- these work now, but the above still does not
-- theorem test (a b c : Prop) (P : Prop → Prop) (H1 : a ↔ b) (H2 : c ∧ a) : c ∧ b :=
@ -233,7 +47,7 @@ and_intro H1 (and_intro H2 H3)
-- theorem test2 {A : Type} {R : A → A → Prop} (Q : Prop) (r s : A)
-- (H3 : R r s ↔ Q) (H1 : R s s) : Q ↔ (R s s ∧ Q) :=
-- relation.operations.symm (and_inhabited_left Q H1)
-- relation.operations.symm (and_absorb_left Q H1)
-- theorem test3 {A : Type} {R : A → A → Prop} (Q : Prop) (r s : A)
-- (H3 : R r s ↔ Q) (H1 : R s s) : R r s ↔ (R s s ∧ Q) :=
@ -241,7 +55,10 @@ and_intro H1 (and_intro H2 H3)
-- theorem test4 {A : Type} {R : A → A → Prop} (Q : Prop) (r s : A)
-- (H3 : R r s ↔ Q) (H1 : R s s) : R r s ↔ (R s s ∧ Q) :=
-- gensubst.subst (relation.operations.symm (and_inhabited_left Q H1)) H3
-- gensubst.subst (relation.operations.symm (and_absorb_left Q H1)) H3
theorem and_absorb_left {a : Prop} (b : Prop) (Ha : a) : a ∧ b ↔ b :=
iff_intro (assume Hab, and_elim_right Hab) (assume Hb, and_intro Ha Hb)
theorem intro_refl {A B : Type} {R : A → A → Prop} {abs : A → B} {rep : B → A}
(H1 : reflexive R) (H2 : ∀b, abs (rep b) = b)
@ -252,8 +69,20 @@ intro
(take r s,
have H4 : R r s ↔ R s s ∧ abs r = abs s,
from
substi (symmi (and_inhabited_left _ (H1 s))) (H3 r s),
substi (symmi (and_inhabited_left _ (H1 r))) H4)
subst_iff (iff_symm (and_absorb_left _ (H1 s))) (H3 r s),
subst_iff (iff_symm (and_absorb_left _ (H1 r))) H4)
-- theorem intro_refl {A B : Type} {R : A → A → Prop} {abs : A → B} {rep : B → A}
-- (H1 : reflexive R) (H2 : ∀b, abs (rep b) = b)
-- (H3 : ∀r s, R r s ↔ abs r = abs s) : is_quotient R abs rep :=
-- intro
-- H2
-- (take b, H1 (rep b))
-- (take r s,
-- have H4 : R r s ↔ R s s ∧ abs r = abs s,
-- from
-- substi (iff_symm (and_absorb_left _ (H1 s))) (H3 r s),
-- substi (iff_symm (and_absorb_left _ (H1 r))) H4)
theorem abs_rep {A B : Type} {R : A → A → Prop} {abs : A → B} {rep : B → A}
(Q : is_quotient R abs rep) (b : B) : abs (rep b) = b :=
@ -414,10 +243,10 @@ opaque_hint (hiding rec rec_constant rec_binary quotient_map quotient_map_binary
abbreviation image {A B : Type} (f : A → B) := subtype (fun b, ∃a, f a = b)
theorem image_inhabited {A B : Type} (f : A → B) (H : inhabited A) : inhabited (image f) :=
inhabited_intro (tag (f (default A)) (exists_intro (default A) rfl))
inhabited_mk (tag (f (default A)) (exists_intro (default A) rfl))
theorem image_inhabited2 {A B : Type} (f : A → B) (a : A) : inhabited (image f) :=
image_inhabited f (inhabited_intro a)
image_inhabited f (inhabited_mk a)
definition fun_image {A B : Type} (f : A → B) (a : A) : image f :=
tag (f a) (exists_intro a rfl)
@ -446,7 +275,7 @@ theorem fun_image_eq {A B : Type} (f : A → B) (a a' : A)
iff_intro
(assume H : f a = f a', tag_eq H)
(assume H : fun_image f a = fun_image f a',
subst (subst (congr2 elt_of H) (elt_of_fun_image f a)) (elt_of_fun_image f a'))
subst (subst (congr_arg elt_of H) (elt_of_fun_image f a)) (elt_of_fun_image f a'))
theorem idempotent_image_elt_of {A : Type} {f : A → A} (H : ∀a, f (f a) = f a) (u : image f)
: fun_image f (elt_of u) = u :=
@ -508,89 +337,30 @@ intro
obtain (a : A) (Ha : f a = elt_of u), from image_elt_of u,
subst Ha (@representative_map_refl_rep A R f H1 H2 a))
(take a a',
substi (fun_image_eq f a a') (H2 a a'))
-- TODO: fix these
-- e.g. in the next three lemmas, we should not need to specify the equivalence relation
-- but the class inference finds reflexive.class eq
theorem equiv_is_refl {A : Type} {R : A → A → Prop} (equiv : is_equivalence.class R) :=
@operations.refl _ R (@is_equivalence.is_reflexive _ _ equiv)
-- we should be able to write
-- @operations.refl _ R _
theorem equiv_is_symm {A : Type} {R : A → A → Prop} (equiv : is_equivalence.class R) :=
@operations.symm _ R (@is_equivalence.is_symmetric _ _ equiv)
theorem equiv_is_trans {A : Type} {R : A → A → Prop} (equiv : is_equivalence.class R) :=
@operations.trans _ R (@is_equivalence.is_transitive _ _ equiv)
subst_iff (fun_image_eq f a a') (H2 a a'))
theorem representative_map_equiv_inj {A : Type} {R : A → A → Prop}
(equiv : is_equivalence.class R) {f : A → A} (H1 : ∀a, R a (f a)) (H2 : ∀a b, R a b → f a = f b)
(equiv : is_equivalence R) {f : A → A} (H1 : ∀a, R a (f a)) (H2 : ∀a b, R a b → f a = f b)
{a b : A} (H3 : f a = f b) : R a b :=
-- have symmR : symmetric R, from @relation.operations.symm _ R _,
have symmR : symmetric R, from equiv_is_symm equiv,
have transR : transitive R, from equiv_is_trans equiv,
have symmR : symmetric R, from is_symmetric.infer R,
have transR : transitive R, from is_transitive.infer R,
show R a b, from
have H2 : R a (f b), from subst H3 (H1 a),
have H3 : R (f b) b, from symmR _ _ (H1 b),
transR _ _ _ H2 H3
have H3 : R (f b) b, from symmR (H1 b),
transR H2 H3
theorem representative_map_to_quotient_equiv {A : Type} {R : A → A → Prop}
(equiv : is_equivalence.class R) {f : A → A} (H1 : ∀a, R a (f a)) (H2 : ∀a b, R a b → f a = f b)
(equiv : is_equivalence R) {f : A → A} (H1 : ∀a, R a (f a)) (H2 : ∀a b, R a b → f a = f b)
: @is_quotient A (image f) R (fun_image f) elt_of :=
representative_map_to_quotient
H1
(take a b,
have reflR : reflexive R, from equiv_is_refl equiv,
have reflR : reflexive R, from is_reflexive.infer R,
have H3 : f a = f b → R a b, from representative_map_equiv_inj equiv H1 H2,
have H4 : R a b ↔ f a = f b, from iff_intro (H2 a b) H3,
have H5 : R a b ↔ R b b ∧ f a = f b,
from substi (symmi (and_inhabited_left _ (reflR b))) H4,
substi (symmi (and_inhabited_left _ (reflR a))) H5)
-- TODO: split this into another file -- it depends on hilbert
-- abstract quotient
-- -----------------
definition prelim_map {A : Type} (R : A → A → Prop) (a : A) :=
-- TODO: it is interesting how the elaborator fails here
-- epsilon (fun b, R a b)
@epsilon _ (nonempty_intro a) (fun b, R a b)
-- TODO: only needed R reflexive (or weaker: R a a)
theorem prelim_map_rel {A : Type} {R : A → A → Prop} (H : is_equivalence.class R) (a : A)
: R a (prelim_map R a) :=
have reflR : reflexive R, from equiv_is_refl H,
epsilon_spec (exists_intro a (reflR a))
-- TODO: only needed: R PER
theorem prelim_map_congr {A : Type} {R : A → A → Prop} (H1 : is_equivalence.class R) {a b : A}
(H2 : R a b) : prelim_map R a = prelim_map R b :=
have symmR : symmetric R, from equiv_is_symm H1,
have transR : transitive R, from equiv_is_trans H1,
have H3 : ∀c, R a c ↔ R b c, from
take c,
iff_intro
(assume H4 : R a c, transR b a c (symmR a b H2) H4)
(assume H4 : R b c, transR a b c H2 H4),
have H4 : (fun c, R a c) = (fun c, R b c), from funext (take c, iff_to_eq (H3 c)),
show @epsilon _ (nonempty_intro a) (λc, R a c) = @epsilon _ (nonempty_intro b) (λc, R b c),
from congr2 _ H4
definition quotient {A : Type} (R : A → A → Prop) : Type := image (prelim_map R)
definition quotient_abs {A : Type} (R : A → A → Prop) : A → quotient R :=
fun_image (prelim_map R)
definition quotient_elt_of {A : Type} (R : A → A → Prop) : quotient R → A := elt_of
theorem quotient_is_quotient {A : Type} (R : A → A → Prop) (H : is_equivalence.class R)
: is_quotient R (quotient_abs R) (quotient_elt_of R) :=
representative_map_to_quotient_equiv
H
(prelim_map_rel H)
(@prelim_map_congr _ _ H)
from subst_iff (iff_symm (and_absorb_left _ (reflR b))) H4,
subst_iff (iff_symm (and_absorb_left _ (reflR a))) H5)
-- previously:
-- opaque_hint (hiding fun_image rec is_quotient prelim_map)

56
library/standard/data/quotient/classical.lean Normal file
View file

@ -0,0 +1,56 @@
-- 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
import struc.relation logic.classes.nonempty data.subtype
import .basic
import logic.axioms.classical logic.axioms.hilbert logic.axioms.funext
namespace quotient
using relation nonempty subtype
-- abstract quotient
-- -----------------
definition prelim_map {A : Type} (R : A → A → Prop) (a : A) :=
-- TODO: it is interesting how the elaborator fails here
-- epsilon (fun b, R a b)
@epsilon _ (nonempty_intro a) (fun b, R a b)
-- TODO: only needed R reflexive (or weaker: R a a)
theorem prelim_map_rel {A : Type} {R : A → A → Prop} (H : is_equivalence R) (a : A)
: R a (prelim_map R a) :=
have reflR : reflexive R, from is_reflexive.infer R,
epsilon_spec (exists_intro a (reflR a))
-- TODO: only needed: R PER
theorem prelim_map_congr {A : Type} {R : A → A → Prop} (H1 : is_equivalence R) {a b : A}
(H2 : R a b) : prelim_map R a = prelim_map R b :=
have symmR : symmetric R, from is_symmetric.infer R,
have transR : transitive R, from is_transitive.infer R,
have H3 : ∀c, R a c ↔ R b c, from
take c,
iff_intro
(assume H4 : R a c, transR (symmR H2) H4)
(assume H4 : R b c, transR H2 H4),
have H4 : (fun c, R a c) = (fun c, R b c), from funext (take c, iff_to_eq (H3 c)),
show @epsilon _ (nonempty_intro a) (λc, R a c) = @epsilon _ (nonempty_intro b) (λc, R b c),
from congr_arg _ H4
definition quotient {A : Type} (R : A → A → Prop) : Type := image (prelim_map R)
definition quotient_abs {A : Type} (R : A → A → Prop) : A → quotient R :=
fun_image (prelim_map R)
definition quotient_elt_of {A : Type} (R : A → A → Prop) : quotient R → A := elt_of
-- TODO: I had to make is_quotient transparent -- change this?
theorem quotient_is_quotient {A : Type} (R : A → A → Prop) (H : is_equivalence R)
: is_quotient R (quotient_abs R) (quotient_elt_of R) :=
representative_map_to_quotient_equiv
H
(prelim_map_rel H)
(@prelim_map_congr _ _ H)
end quotient

5
library/standard/data/quotient/default.lean Normal file
View file

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

6
library/standard/data/quotient/quotient.md Normal file
View file

@ -0,0 +1,6 @@
data.quotient
=============
* [aux](aux.lean) : auxiliary facts about products
* [basic](basic.lean) : the constructive core of the quotient construction
* [classical](classical.lean) : the classical version, using Hilbert choice

2
library/standard/data/set.lean
View file

@ -5,7 +5,7 @@
----------------------------------------------------------------------------------------------------
import logic.axioms.funext data.bool
using eq_proofs bool
using eq_ops bool
namespace set
definition set (T : Type) := T → bool

4
library/standard/data/sigma.lean
View file

@ -4,6 +4,8 @@
import logic.classes.inhabited logic.connectives.eq
using inhabited
inductive sigma {A : Type} (B : A → Type) : Type :=
| dpair : Πx : A, B x → sigma B
@ -48,7 +50,7 @@ section
theorem sigma_inhabited (H1 : inhabited A) (H2 : inhabited (B (default A))) :
inhabited (sigma B) :=
inhabited_elim H1 (λa, inhabited_elim H2 (λb, inhabited_intro (dpair (default A) b)))
inhabited_destruct H1 (λa, inhabited_destruct H2 (λb, inhabited_mk (dpair (default A) b)))
end

10
library/standard/data/string.lean
View file

@ -1,13 +1,13 @@
----------------------------------------------------------------------------------------------------
-- 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
using bool
using bool inhabited
namespace string
inductive char : Type :=
| ascii : bool → bool → bool → bool → bool → bool → bool → bool → char
@ -16,9 +16,9 @@ inductive string : Type :=
| str : char → string → string
theorem inhabited_char [instance] : inhabited char :=
inhabited_intro (ascii ff ff ff ff ff ff ff ff)
inhabited_mk (ascii ff ff ff ff ff ff ff ff)
theorem inhabited_string [instance] : inhabited string :=
inhabited_intro empty
inhabited_mk empty
end string

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

@ -17,8 +17,8 @@ theorem unit_eq (a b : unit) : a = b :=
unit_rec (unit_rec (refl ⋆) b) a
theorem inhabited_unit [instance] : inhabited unit :=
inhabited_intro ⋆
inhabited_mk ⋆
theorem decidable_eq [instance] (a b : unit) : decidable (a = b) :=
inl (unit_eq a b)
end unit
end unit

40
library/standard/hott/inhabited.lean
View file

@ -1,40 +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
-- The predicative version of inhabited
-- TODO: restore instances
-- import logic bool
-- using logic
namespace predicative
inductive inhabited (A : Type) : Type :=
| inhabited_intro : A → inhabited A
theorem inhabited_elim {A : Type} {B : Type} (H1 : inhabited A) (H2 : A → B) : B
:= inhabited_rec H2 H1
end predicative
-- theorem inhabited_fun [instance] (A : Type) {B : Type} (H : inhabited B) : inhabited (A → B)
-- := inhabited_elim H (take (b : B), inhabited_intro (λ a : A, b))
-- theorem inhabited_sum_left [instance] {A : Type} (B : Type) (H : inhabited A) : inhabited (A + B)
-- := inhabited_elim H (λ a, inhabited_intro (inl B a))
-- theorem inhabited_sum_right [instance] (A : Type) {B : Type} (H : inhabited B) : inhabited (A + B)
-- := inhabited_elim H (λ b, inhabited_intro (inr A b))
-- theorem inhabited_product [instance] {A : Type} {B : Type} (Ha : inhabited A) (Hb : inhabited B) : inhabited (A × B)
-- := inhabited_elim Ha (λ a, (inhabited_elim Hb (λ b, inhabited_intro (a, b))))
-- theorem inhabited_bool [instance] : inhabited bool
-- := inhabited_intro true
-- theorem inhabited_unit [instance] : inhabited unit
-- := inhabited_intro ⋆
-- theorem inhabited_sigma_pr1 {A : Type} {B : A → Type} (p : Σ x, B x) : inhabited A
-- := inhabited_intro (dpr1 p)

16
library/standard/logic/axioms/classical.lean
View file

@ -4,9 +4,9 @@
-- Author: Leonardo de Moura
----------------------------------------------------------------------------------------------------
import logic.connectives.basic logic.connectives.quantifiers logic.connectives.cast
import logic.connectives.basic logic.connectives.quantifiers logic.connectives.cast struc.relation
using eq_proofs
using eq_ops
axiom prop_complete (a : Prop) : a = true ∨ a = false
@ -15,6 +15,9 @@ or_elim (prop_complete a)
(assume Ht : a = true, Ht⁻¹ ▸ H1)
(assume Hf : a = false, Hf⁻¹ ▸ H2)
theorem case_on (a : Prop) {P : Prop → Prop} (H1 : P true) (H2 : P false) : P a :=
case P H1 H2 a
theorem em (a : Prop) : a ∨ ¬a :=
or_elim (prop_complete a)
(assume Ht : a = true, or_inl (eqt_elim Ht))
@ -163,3 +166,12 @@ theorem peirce (a b : Prop) : ((a → b) → a) → a :=
assume H, by_contradiction (assume Hna : ¬a,
have Hnna : ¬¬a, from not_implies_left (mt H Hna),
absurd (not_not_elim Hnna) Hna)
-- with classical logic, every predicate respects iff
using relation
theorem iff_congr [instance] (P : Prop → Prop) : congr iff iff P :=
congr_mk
(take (a b : Prop),
assume H : a ↔ b,
show P a ↔ P b, from eq_to_iff (subst (iff_to_eq H) (refl (P a))))

2
library/standard/logic/axioms/examples/diaconescu.lean
View file

@ -3,7 +3,7 @@
-- Author: Leonardo de Moura
import logic.axioms.hilbert logic.axioms.funext
using eq_proofs
using eq_ops nonempty inhabited
-- Diaconescu’s theorem
-- Show that Excluded middle follows from

4
library/standard/logic/axioms/hilbert.lean
View file

@ -6,7 +6,7 @@ import logic.connectives.eq logic.connectives.quantifiers
import logic.classes.inhabited logic.classes.nonempty
import data.subtype data.sum
using subtype
using subtype inhabited nonempty
-- logic.axioms.hilbert
-- ====================
@ -25,7 +25,7 @@ nonempty_elim H (take x, exists_intro x trivial)
theorem nonempty_imp_inhabited {A : Type} (H : nonempty A) : inhabited A :=
let u : {x : A | (∃x : A, true) → true} := strong_indefinite_description (λa, true) H in
inhabited_intro (elt_of u)
inhabited_mk (elt_of u)
theorem inhabited_exists {A : Type} {P : A → Prop} (H : ∃x, P x) : inhabited A :=
nonempty_imp_inhabited (obtain w Hw, from H, nonempty_intro w)

12
library/standard/logic/axioms/piext.lean
View file

@ -6,27 +6,29 @@
import logic.classes.inhabited logic.connectives.cast
using inhabited
-- Pi extensionality
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 :=
have Hi [fact] : inhabited (Π x, B x), from inhabited_intro f,
have Hi [fact] : inhabited (Π x, B x), from inhabited_mk 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)
theorem hcongr_fun {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 Hi [fact] : inhabited (Π x, B x), from inhabited_mk f,
have Hb : B = B', from piext (type_eq H),
hcongr1' a H Hb
hcongr_fun' 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' :=
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,
take B B' f f' e, hcongr_fun 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,
H2 B B' f f' Hff'

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

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

6
library/standard/logic/classes/decidable.lean
View file

@ -27,12 +27,12 @@ decidable_rec H1 H2 H
theorem irrelevant {p : Prop} (d1 d2 : decidable p) : d1 = d2 :=
decidable_rec
(assume Hp1 : p, decidable_rec
(assume Hp2 : p, congr2 inl (refl Hp1)) -- using proof irrelevance for Prop
(assume Hp2 : p, congr_arg inl (refl Hp1)) -- using proof irrelevance for Prop
(assume Hnp2 : ¬p, absurd_elim (inl Hp1 = inr Hnp2) Hp1 Hnp2)
d2)
(assume Hnp1 : ¬p, decidable_rec
(assume Hp2 : p, absurd_elim (inr Hnp1 = inl Hp2) Hp2 Hnp1)
(assume Hnp2 : ¬p, congr2 inr (refl Hnp1)) -- using proof irrelevance for Prop
(assume Hnp2 : ¬p, congr_arg inr (refl Hnp1)) -- using proof irrelevance for Prop
d2)
d1
@ -87,4 +87,4 @@ rec_on Ha
theorem decidable_eq_equiv {a b : Prop} (Ha : decidable a) (H : a = b) : decidable b :=
decidable_iff_equiv Ha (eq_to_iff H)
end decidable
end decidable

14
library/standard/logic/classes/inhabited.lean
View file

@ -5,15 +5,19 @@
import logic.connectives.basic
inductive inhabited (A : Type) : Type :=
| inhabited_intro : A → inhabited A
| inhabited_mk : A → inhabited A
definition inhabited_elim {A : Type} {B : Type} (H1 : inhabited A) (H2 : A → B) : B :=
namespace inhabited
definition inhabited_destruct {A : Type} {B : Type} (H1 : inhabited A) (H2 : A → B) : B :=
inhabited_rec H2 H1
definition inhabited_Prop [instance] : inhabited Prop :=
inhabited_intro true
inhabited_mk true
definition inhabited_fun [instance] (A : Type) {B : Type} (H : inhabited B) : inhabited (A → B) :=
inhabited_elim H (take b, inhabited_intro (λa, b))
inhabited_destruct H (take b, inhabited_mk (λa, b))
definition default (A : Type) {H : inhabited A} : A := inhabited_elim H (take a, a)
definition default (A : Type) {H : inhabited A} : A := inhabited_destruct H (take a, a)
end inhabited

6
library/standard/logic/classes/nonempty.lean
View file

@ -4,6 +4,10 @@
import logic.connectives.basic .inhabited
using inhabited
namespace nonempty
inductive nonempty (A : Type) : Prop :=
| nonempty_intro : A → nonempty A
@ -12,3 +16,5 @@ nonempty_rec H2 H1
theorem inhabited_imp_nonempty [instance] {A : Type} (H : inhabited A) : nonempty A :=
nonempty_intro (default A)
end nonempty

5
library/standard/logic/connectives/basic.lean
View file

@ -1,8 +1,6 @@
----------------------------------------------------------------------------------------------------
-- 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 .prop
@ -57,6 +55,9 @@ assume Hna : ¬a, absurd (assume Ha : a, absurd_elim b Ha Hna) H
theorem not_implies_right {a b : Prop} (H : ¬(a → b)) : ¬b :=
assume Hb : b, absurd (assume Ha : a, Hb) H
theorem contrapos {a b : Prop} (Hab : a → b) : (¬b → ¬a) :=
assume Hnb Ha, Hnb (Hab Ha)
-- and
-- ---

18
library/standard/logic/connectives/cast.lean
View file

@ -6,7 +6,7 @@
import .eq .quantifiers
using eq_proofs
using eq_ops
definition cast {A B : Type} (H : A = B) (a : A) : B :=
eq_rec a H
@ -91,13 +91,13 @@ heq_to_eq (calc cast Hbc (cast Hab a) == cast Hab a : cast_heq Hbc (cas
... == a : cast_heq Hab a
... == cast (Hab ⬝ Hbc) a : hsymm (cast_heq (Hab ⬝ Hbc) a))
theorem dcongr2 {A : Type} {B : A → Type} (f : Πx, B x) {a b : A} (H : a = b) : f a == f b :=
theorem dcongr_arg {A : Type} {B : A → Type} (f : Πx, B x) {a b : A} (H : a = b) : f a == f b :=
have e1 : ∀ (H : B a = B a), cast H (f a) = f a, from
assume H, cast_eq H (f a),
have e2 : ∀ (H : B a = B b), cast H (f a) = f b, from
subst H e1,
have e3 : cast (congr2 B H) (f a) = f b, from
e2 (congr2 B H),
have e3 : cast (congr_arg B H) (f a) = f b, from
e2 (congr_arg B H),
cast_eq_to_heq e3
theorem pi_eq {A : Type} {B B' : A → Type} (H : B = B') : (Π x, B x) = (Π x, B' x) :=
@ -106,20 +106,20 @@ subst H (refl (Π x, B x))
theorem cast_app' {A : Type} {B B' : A → Type} (H : B = B') (f : Π x, B x) (a : A) :
cast (pi_eq H) f a == f a :=
have H1 : ∀ (H : (Π x, B x) = (Π x, B x)), cast H f a == f a, from
assume H, eq_to_heq (congr1 (cast_eq H f) a),
assume H, eq_to_heq (congr_fun (cast_eq H f) a),
have H2 : ∀ (H : (Π x, B x) = (Π x, B' x)), cast H f a == f a, from
subst H H1,
H2 (pi_eq H)
theorem cast_pull {A : Type} {B B' : A → Type} (H : B = B') (f : Π x, B x) (a : A) :
cast (pi_eq H) f a = cast (congr1 H a) (f a) :=
cast (pi_eq H) f a = cast (congr_fun H a) (f a) :=
heq_to_eq (calc cast (pi_eq H) f a == f a : cast_app' H f a
... == cast (congr1 H a) (f a) : hsymm (cast_heq (congr1 H a) (f a)))
... == cast (congr_fun H a) (f a) : hsymm (cast_heq (congr_fun H a) (f a)))
theorem hcongr1' {A : Type} {B B' : A → Type} {f : Π x, B x} {f' : Π x, B' x} (a : A)
theorem hcongr_fun' {A : Type} {B B' : A → Type} {f : Π x, B x} {f' : Π x, B' x} (a : A)
(H1 : f == f') (H2 : B = B')
: f a == f' a :=
heq_elim H1 (λ (Ht : (Π x, B x) = (Π x, B' x)) (Hw : cast Ht f = f'),
calc f a == cast (pi_eq H2) f a : hsymm (cast_app' H2 f a)
... = cast Ht f a : refl (cast Ht f a)
... = f' a : congr1 Hw a)
... = f' a : congr_fun Hw a)

14
library/standard/logic/connectives/eq.lean
View file

@ -54,27 +54,27 @@ theorem eq_rec_on_compose {A : Type} {a b c : A} {P : A → Type} (H1 : a = b) (
from eq_rec_on H2 (take (H2 : b = b), eq_rec_on_id H2 _))
H2
namespace eq_proofs
namespace eq_ops
postfix `⁻¹`:100 := symm
infixr `⬝`:75 := trans
infixr `▸`:75 := subst
end eq_proofs
using eq_proofs
end eq_ops
using eq_ops
theorem congr1 {A : Type} {B : A → Type} {f g : Π x, B x} (H : f = g) (a : A) : f a = g a :=
theorem congr_fun {A : Type} {B : A → Type} {f g : Π x, B x} (H : f = g) (a : A) : f a = g a :=
H ▸ refl (f a)
theorem congr2 {A : Type} {B : Type} {a b : A} (f : A → B) (H : a = b) : f a = f b :=
theorem congr_arg {A : Type} {B : Type} {a b : A} (f : A → B) (H : a = b) : f a = f b :=
H ▸ refl (f a)
theorem congr {A : Type} {B : Type} {f g : A → B} {a b : A} (H1 : f = g) (H2 : a = b) : f a = g b :=
H1 ▸ H2 ▸ refl (f a)
theorem equal_f {A : Type} {B : A → Type} {f g : Π x, B x} (H : f = g) : ∀x, f x = g x :=
take x, congr1 H x
take x, congr_fun H x
theorem not_congr {a b : Prop} (H : a = b) : (¬a) = (¬b) :=
congr2 not H
congr_arg not H
theorem eqmp {a b : Prop} (H1 : a = b) (H2 : a) : b :=
H1 ▸ H2

17
library/standard/logic/connectives/examples/instances_test.lean
View file

@ -6,11 +6,12 @@ import ..instances
using relation
using relation.general_operations
using relation.iff_ops
using eq_ops
section
using relation.operations
theorem test1 (a b : Prop) (H : a ↔ b) (H1 : a) : b := mp H H1
end
@ -18,10 +19,8 @@ end
section
using gensubst
theorem test2 (a b c d e : Prop) (H1 : a ↔ b) (H2 : a ∨ c → ¬(d → a)) : b ∨ c → ¬(d → b) :=
subst H1 H2
subst iff H1 H2
theorem test3 (a b c d e : Prop) (H1 : a ↔ b) (H2 : a ∨ c → ¬(d → a)) : b ∨ c → ¬(d → b) :=
H1 ▸ H2
@ -35,12 +34,16 @@ congr.infer iff iff (λa, (a ∨ c → ¬(d → a))) H1
section
using relation.symbols
theorem test5 (T : Type) (a b c d : T) (H1 : a = b) (H2 : c = b) (H3 : c = d) : a = d :=
H1 ⬝ H2⁻¹ ⬝ H3
theorem test6 (a b c d : Prop) (H1 : a ↔ b) (H2 : c ↔ b) (H3 : c ↔ d) : a ↔ d :=
H1 ⬝ (H2⁻¹ ⬝ H3)
theorem test7 (T : Type) (a b c d : T) (H1 : a = b) (H2 : c = b) (H3 : c = d) : a = d :=
trans H1 (trans (symm H2) H3)
theorem test8 (a b c d : Prop) (H1 : a ↔ b) (H2 : c ↔ b) (H3 : c ↔ d) : a ↔ d :=
trans iff H1 (trans iff (symm iff H2) H3)
end

2
library/standard/logic/connectives/if.lean
View file

@ -5,7 +5,7 @@
----------------------------------------------------------------------------------------------------
import logic.classes.decidable tools.tactic
using decidable tactic eq_proofs
using decidable tactic eq_ops
definition ite (c : Prop) {H : decidable c} {A : Type} (t e : A) : A :=
rec_on H (assume Hc, t) (assume Hnc, e)

97
library/standard/logic/connectives/instances.lean
View file

@ -4,44 +4,46 @@
import logic.connectives.basic logic.connectives.eq struc.relation
namespace relation
using relation
-- Congruences for logic
-- ---------------------
theorem congr_not : congr.class iff iff not :=
congr.mk
theorem congr_not : congr iff iff not :=
congr_mk
(take a b,
assume H : a ↔ b, iff_intro
(assume H1 : ¬a, assume H2 : b, H1 (iff_elim_right H H2))
(assume H1 : ¬b, assume H2 : a, H1 (iff_elim_left H H2)))
theorem congr_and : congr.class2 iff iff iff and :=
congr.mk2
theorem congr_and : congr2 iff iff iff and :=
congr2_mk
(take a1 b1 a2 b2,
assume H1 : a1 ↔ b1, assume H2 : a2 ↔ b2,
iff_intro
(assume H3 : a1 ∧ a2, and_imp_and H3 (iff_elim_left H1) (iff_elim_left H2))
(assume H3 : b1 ∧ b2, and_imp_and H3 (iff_elim_right H1) (iff_elim_right H2)))
theorem congr_or : congr.class2 iff iff iff or :=
congr.mk2
theorem congr_or : congr2 iff iff iff or :=
congr2_mk
(take a1 b1 a2 b2,
assume H1 : a1 ↔ b1, assume H2 : a2 ↔ b2,
iff_intro
(assume H3 : a1 ∨ a2, or_imp_or H3 (iff_elim_left H1) (iff_elim_left H2))
(assume H3 : b1 ∨ b2, or_imp_or H3 (iff_elim_right H1) (iff_elim_right H2)))
theorem congr_imp : congr.class2 iff iff iff imp :=
congr.mk2
theorem congr_imp : congr2 iff iff iff imp :=
congr2_mk
(take a1 b1 a2 b2,
assume H1 : a1 ↔ b1, assume H2 : a2 ↔ b2,
iff_intro
(assume H3 : a1 → a2, assume Hb1 : b1, iff_elim_left H2 (H3 ((iff_elim_right H1) Hb1)))
(assume H3 : b1 → b2, assume Ha1 : a1, iff_elim_right H2 (H3 ((iff_elim_left H1) Ha1))))
theorem congr_iff : congr.class2 iff iff iff iff :=
congr.mk2
theorem congr_iff : congr2 iff iff iff iff :=
congr2_mk
(take a1 b1 a2 b2,
assume H1 : a1 ↔ b1, assume H2 : a2 ↔ b2,
iff_intro
@ -59,62 +61,87 @@ theorem congr_iff_compose [instance] := congr.compose21 congr_iff
-- Generalized substitution
-- ------------------------
namespace gensubst
-- TODO: note that the target has to be "iff". Otherwise, there is not enough
-- information to infer an mp-like relation.
theorem subst {T : Type} {R : T → T → Prop} {P : T → Prop} {C : congr.class R iff P}
namespace general_operations
theorem subst {T : Type} (R : T → T → Prop) ⦃P : T → Prop⦄ {C : congr R iff P}
{a b : T} (H : R a b) (H1 : P a) : P b := iff_elim_left (congr.app C H) H1
infixr `▸`:75 := subst
end gensubst
end general_operations
-- = is an equivalence relation
-- ----------------------------
theorem is_reflexive_eq [instance] (T : Type) : relation.is_reflexive.class (@eq T) :=
relation.is_reflexive.mk (@refl T)
theorem is_reflexive_eq [instance] (T : Type) : relation.is_reflexive (@eq T) :=
relation.is_reflexive_mk (@refl T)
theorem is_symmetric_eq [instance] (T : Type) : relation.is_symmetric.class (@eq T) :=
relation.is_symmetric.mk (@symm T)
theorem is_symmetric_eq [instance] (T : Type) : relation.is_symmetric (@eq T) :=
relation.is_symmetric_mk (@symm T)
theorem is_transitive_eq [instance] (T : Type) : relation.is_transitive.class (@eq T) :=
relation.is_transitive.mk (@trans T)
theorem is_transitive_eq [instance] (T : Type) : relation.is_transitive (@eq T) :=
relation.is_transitive_mk (@trans T)
-- TODO: this is only temporary, needed to inform Lean that is_equivalence is a class
theorem is_equivalence_eq [instance] (T : Type) : relation.is_equivalence (@eq T) :=
relation.is_equivalence_mk _ _ _
-- iff is an equivalence relation
-- ------------------------------
theorem is_reflexive_iff [instance] : relation.is_reflexive.class iff :=
relation.is_reflexive.mk (@iff_refl)
theorem is_reflexive_iff [instance] : relation.is_reflexive iff :=
relation.is_reflexive_mk (@iff_refl)
theorem is_symmetric_iff [instance] : relation.is_symmetric.class iff :=
relation.is_symmetric.mk (@iff_symm)
theorem is_symmetric_iff [instance] : relation.is_symmetric iff :=
relation.is_symmetric_mk (@iff_symm)
theorem is_transitive_iff [instance] : relation.is_transitive.class iff :=
relation.is_transitive.mk (@iff_trans)
theorem is_transitive_iff [instance] : relation.is_transitive iff :=
relation.is_transitive_mk (@iff_trans)
-- Mp-like for iff
-- ---------------
theorem mp_like_iff [instance] (a b : Prop) (H : a ↔ b) : relation.mp_like.class H :=
relation.mp_like.mk (iff_elim_left H)
theorem mp_like_iff [instance] (a b : Prop) (H : a ↔ b) : relation.mp_like H :=
relation.mp_like_mk (iff_elim_left H)
-- Substition for iff
-- ------------------
theorem subst_iff {P : Prop → Prop} {C : congr iff iff P} {a b : Prop} (H : a ↔ b) (H1 : P a) :
P b :=
@general_operations.subst Prop iff P C a b H H1
-- Support for calc
-- ----------------
calc_refl iff_refl
calc_subst subst_iff
calc_trans iff_trans
namespace iff_ops
postfix `⁻¹`:100 := iff_symm
infixr `⬝`:75 := iff_trans
infixr `▸`:75 := subst_iff
end iff_ops
-- Boolean calculations
-- --------------------
-- TODO: move these to new file
-- TODO: declare trans
-- TODO: move these somewhere
theorem or_right_comm (a b c : Prop) : (a ∨ b) ∨ c ↔ (a ∨ c) ∨ b :=
calc
(a ∨ b) ∨ c ↔ a ∨ (b ∨ c) : or_assoc _ _ _
... ↔ a ∨ (c ∨ b) : congr.infer iff iff _ (or_comm b c)
... ↔ (a ∨ c) ∨ b : iff_symm (or_assoc _ _ _)
... ↔ a ∨ (c ∨ b) : {or_comm b c}
... ↔ (a ∨ c) ∨ b : iff_symm (or_assoc _ _ _)
-- TODO: add or_left_comm, and_right_comm, and_left_comm
end relation

6
library/standard/logic/connectives/quantifiers.lean
View file

@ -4,6 +4,8 @@
import .basic .eq ..classes.nonempty
using inhabited nonempty
inductive Exists {A : Type} (P : A → Prop) : Prop :=
| exists_intro : ∀ (a : A), P a → Exists P
@ -52,12 +54,12 @@ theorem forall_true_iff_true (A : Type) : (∀x : A, true) ↔ true :=
iff_intro (assume H, trivial) (assume H, take x, trivial)
theorem forall_p_iff_p (A : Type) {H : inhabited A} (p : Prop) : (∀x : A, p) ↔ p :=
iff_intro (assume Hl, inhabited_elim H (take x, Hl x)) (assume Hr, take x, Hr)
iff_intro (assume Hl, inhabited_destruct H (take x, Hl x)) (assume Hr, take x, Hr)
theorem exists_p_iff_p (A : Type) {H : inhabited A} (p : Prop) : (∃x : A, p) ↔ p :=
iff_intro
(assume Hl, obtain a Hp, from Hl, Hp)
(assume Hr, inhabited_elim H (take a, exists_intro a Hr))
(assume Hr, inhabited_destruct H (take a, exists_intro a Hr))
theorem forall_and_distribute {A : Type} (φ ψ : A → Prop) : (∀x, φ x ∧ ψ x) ↔ (∀x, φ x) ∧ (∀x, ψ x) :=
iff_intro

2
library/standard/struc/binary.lean
View file

@ -5,7 +5,7 @@
----------------------------------------------------------------------------------------------------
import logic.connectives.eq
using eq_proofs
using eq_ops
namespace binary
section

31
library/standard/struc/equivalence.lean
View file

@ -1,31 +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.prop
namespace equivalence
section
parameter {A : Type}
parameter p : A → A → Prop
infix `∼`:50 := p
definition reflexive := ∀a, a ∼ a
definition symmetric := ∀a b, a ∼ b → b ∼ a
definition transitive := ∀a b c, a ∼ b → b ∼ c → a ∼ c
end
inductive equivalence {A : Type} (p : A → A → Prop) : Prop :=
| equivalence_intro : reflexive p → symmetric p → transitive p → equivalence p
theorem equivalence_reflexive [instance] {A : Type} {p : A → A → Prop} (H : equivalence p) : reflexive p :=
equivalence_rec (λ r s t, r) H
theorem equivalence_symmetric [instance] {A : Type} {p : A → A → Prop} (H : equivalence p) : symmetric p :=
equivalence_rec (λ r s t, s) H
theorem equivalence_transitive [instance] {A : Type} {p : A → A → Prop} (H : equivalence p) : transitive p :=
equivalence_rec (λ r s t, t) H
end equivalence

217
library/standard/struc/relation.lean
View file

@ -4,69 +4,72 @@
import logic.connectives.prop
-- General properties of relations
-- -------------------------------
namespace relation
abbreviation reflexive {T : Type} (R : T → T → Type) : Type := ∀x, R x x
abbreviation symmetric {T : Type} (R : T → T → Type) : Type := ∀x y, R x y → R y x
abbreviation transitive {T : Type} (R : T → T → Type) : Type := ∀x y z, R x y → R y z → R x z
abbreviation symmetric {T : Type} (R : T → T → Type) : Type := ∀⦃x y⦄, R x y → R y x
abbreviation transitive {T : Type} (R : T → T → Type) : Type := ∀⦃x y z⦄, R x y → R y z → R x z
inductive is_reflexive {T : Type} (R : T → T → Type) : Prop :=
| is_reflexive_mk : reflexive R → is_reflexive R
namespace is_reflexive
inductive class {T : Type} (R : T → T → Type) : Prop :=
| mk : reflexive R → class R
abbreviation app ⦃T : Type⦄ {R : T → T → Type} (C : is_reflexive R) : reflexive R :=
is_reflexive_rec (λu, u) C
abbreviation app ⦃T : Type⦄ {R : T → T → Type} (C : class R) : reflexive R :=
class_rec (λu, u) C
abbreviation infer ⦃T : Type⦄ {R : T → T → Type} {C : class R} : reflexive R :=
class_rec (λu, u) C
abbreviation infer ⦃T : Type⦄ (R : T → T → Type) {C : is_reflexive R} : reflexive R :=
is_reflexive_rec (λu, u) C
end is_reflexive
inductive is_symmetric {T : Type} (R : T → T → Type) : Prop :=
| is_symmetric_mk : symmetric R → is_symmetric R
namespace is_symmetric
inductive class {T : Type} (R : T → T → Type) : Prop :=
| mk : symmetric R → class R
abbreviation app ⦃T : Type⦄ {R : T → T → Type} (C : is_symmetric R) : symmetric R :=
is_symmetric_rec (λu, u) C
abbreviation app ⦃T : Type⦄ {R : T → T → Type} (C : class R) ⦃x y : T⦄ (H : R x y) : R y x :=
class_rec (λu, u) C x y H
abbreviation infer ⦃T : Type⦄ {R : T → T → Type} {C : class R} ⦃x y : T⦄ (H : R x y) : R y x :=
class_rec (λu, u) C x y H
abbreviation infer ⦃T : Type⦄ (R : T → T → Type) {C : is_symmetric R} : symmetric R :=
is_symmetric_rec (λu, u) C
end is_symmetric
inductive is_transitive {T : Type} (R : T → T → Type) : Prop :=
| is_transitive_mk : transitive R → is_transitive R
namespace is_transitive
inductive class {T : Type} (R : T → T → Type) : Prop :=
| mk : transitive R → class R
abbreviation app ⦃T : Type⦄ {R : T → T → Type} (C : is_transitive R) : transitive R :=
is_transitive_rec (λu, u) C
abbreviation app ⦃T : Type⦄ {R : T → T → Type} (C : class R) ⦃x y z : T⦄ (H1 : R x y)
(H2 : R y z) : R x z :=
class_rec (λu, u) C x y z H1 H2
abbreviation infer ⦃T : Type⦄ {R : T → T → Type} {C : class R} ⦃x y z : T⦄ (H1 : R x y)
(H2 : R y z) : R x z :=
class_rec (λu, u) C x y z H1 H2
abbreviation infer ⦃T : Type⦄ (R : T → T → Type) {C : is_transitive R} : transitive R :=
is_transitive_rec (λu, u) C
end is_transitive
inductive is_equivalence {T : Type} (R : T → T → Type) : Prop :=
| is_equivalence_mk : is_reflexive R → is_symmetric R → is_transitive R → is_equivalence R
namespace is_equivalence
inductive class {T : Type} (R : T → T → Type) : Prop :=
| mk : is_reflexive.class R → is_symmetric.class R → is_transitive.class R → class R
theorem is_reflexive {T : Type} (R : T → T → Type) {C : is_equivalence R} : is_reflexive R :=
is_equivalence_rec (λx y z, x) C
theorem is_reflexive {T : Type} {R : T → T → Type} {C : class R} : is_reflexive.class R :=
class_rec (λx y z, x) C
theorem is_symmetric {T : Type} {R : T → T → Type} {C : is_equivalence R} : is_symmetric R :=
is_equivalence_rec (λx y z, y) C
theorem is_symmetric {T : Type} {R : T → T → Type} {C : class R} : is_symmetric.class R :=
class_rec (λx y z, y) C
theorem is_transitive {T : Type} {R : T → T → Type} {C : class R} : is_transitive.class R :=
class_rec (λx y z, z) C
theorem is_transitive {T : Type} {R : T → T → Type} {C : is_equivalence R} : is_transitive R :=
is_equivalence_rec (λx y z, z) C
end is_equivalence
@ -74,112 +77,109 @@ instance is_equivalence.is_reflexive
instance is_equivalence.is_symmetric
instance is_equivalence.is_transitive
-- partial equivalence relation
inductive is_PER {T : Type} (R : T → T → Type) : Prop :=
| is_PER_mk : is_symmetric R → is_transitive R → is_PER R
namespace is_PER
inductive class {T : Type} (R : T → T → Type) : Prop :=
| mk : is_symmetric.class R → is_transitive.class R → class R
theorem is_symmetric {T : Type} {R : T → T → Type} {C : is_PER R} : is_symmetric R :=
is_PER_rec (λx y, x) C
theorem is_symmetric {T : Type} {R : T → T → Type} {C : class R} : is_symmetric.class R :=
class_rec (λx y, x) C
theorem is_transitive {T : Type} {R : T → T → Type} {C : class R} : is_transitive.class R :=
class_rec (λx y, y) C
theorem is_transitive {T : Type} {R : T → T → Type} {C : is_PER R} : is_transitive R :=
is_PER_rec (λx y, y) C
end is_PER
-- instance is_PER.is_symmetric
instance is_PER.is_symmetric
instance is_PER.is_transitive
-- Congruence for unary and binary functions
-- -----------------------------------------
namespace congr
inductive class {T1 : Type} (R1 : T1 → T1 → Prop) {T2 : Type} (R2 : T2 → T2 → Prop)
inductive congr {T1 : Type} (R1 : T1 → T1 → Prop) {T2 : Type} (R2 : T2 → T2 → Prop)
(f : T1 → T2) : Prop :=
| mk : (∀x y, R1 x y → R2 (f x) (f y)) → class R1 R2 f
abbreviation app {T1 : Type} {R1 : T1 → T1 → Prop} {T2 : Type} {R2 : T2 → T2 → Prop}
{f : T1 → T2} (C : class R1 R2 f) ⦃x y : T1⦄ : R1 x y → R2 (f x) (f y) :=
class_rec (λu, u) C x y
theorem infer {T1 : Type} (R1 : T1 → T1 → Prop) {T2 : Type} (R2 : T2 → T2 → Prop)
(f : T1 → T2) {C : class R1 R2 f} ⦃x y : T1⦄ : R1 x y → R2 (f x) (f y) :=
class_rec (λu, u) C x y
| congr_mk : (∀x y, R1 x y → R2 (f x) (f y)) → congr R1 R2 f
-- for binary functions
inductive class2 {T1 : Type} (R1 : T1 → T1 → Prop) {T2 : Type} (R2 : T2 → T2 → Prop)
inductive congr2 {T1 : Type} (R1 : T1 → T1 → Prop) {T2 : Type} (R2 : T2 → T2 → Prop)
{T3 : Type} (R3 : T3 → T3 → Prop) (f : T1 → T2 → T3) : Prop :=
| mk2 : (∀(x1 y1 : T1) (x2 y2 : T2), R1 x1 y1 → R2 x2 y2 → R3 (f x1 x2) (f y1 y2)) →
class2 R1 R2 R3 f
| congr2_mk : (∀(x1 y1 : T1) (x2 y2 : T2), R1 x1 y1 → R2 x2 y2 → R3 (f x1 x2) (f y1 y2)) →
congr2 R1 R2 R3 f
abbreviation app2 {T1 : Type} {R1 : T1 → T1 → Prop} {T2 : Type} {R2 : T2 → T2 → Prop}
{T3 : Type} {R3 : T3 → T3 → Prop}
{f : T1 → T2 → T3} (C : class2 R1 R2 R3 f) ⦃x1 y1 : T1⦄ ⦃x2 y2 : T2⦄
: R1 x1 y1 → R2 x2 y2 → R3 (f x1 x2) (f y1 y2) :=
class2_rec (λu, u) C x1 y1 x2 y2
namespace congr
abbreviation app {T1 : Type} {R1 : T1 → T1 → Prop} {T2 : Type} {R2 : T2 → T2 → Prop}
{f : T1 → T2} (C : congr R1 R2 f) ⦃x y : T1⦄ : R1 x y → R2 (f x) (f y) :=
congr_rec (λu, u) C x y
theorem infer {T1 : Type} (R1 : T1 → T1 → Prop) {T2 : Type} (R2 : T2 → T2 → Prop)
(f : T1 → T2) {C : congr R1 R2 f} ⦃x y : T1⦄ : R1 x y → R2 (f x) (f y) :=
congr_rec (λu, u) C x y
abbreviation app2 {T1 : Type} {R1 : T1 → T1 → Prop} {T2 : Type} {R2 : T2 → T2 → Prop}
{T3 : Type} {R3 : T3 → T3 → Prop}
{f : T1 → T2 → T3} (C : congr2 R1 R2 R3 f) ⦃x1 y1 : T1⦄ ⦃x2 y2 : T2⦄ :
R1 x1 y1 → R2 x2 y2 → R3 (f x1 x2) (f y1 y2) :=
congr2_rec (λu, u) C x1 y1 x2 y2
-- ### general tools to build instances
theorem compose
{T2 : Type} {R2 : T2 → T2 → Prop}
{T3 : Type} {R3 : T3 → T3 → Prop}
{g : T2 → T3} (C2 : congr.class R2 R3 g)
{{T1 : Type}} {R1 : T1 → T1 → Prop}
{f : T1 → T2} (C1 : congr.class R1 R2 f) :
congr.class R1 R3 (λx, g (f x)) :=
mk (λx1 x2 H, app C2 (app C1 H))
theorem compose
{T2 : Type} {R2 : T2 → T2 → Prop}
{T3 : Type} {R3 : T3 → T3 → Prop}
{g : T2 → T3} (C2 : congr R2 R3 g)
⦃T1 : Type⦄ {R1 : T1 → T1 → Prop}
{f : T1 → T2} (C1 : congr R1 R2 f) :
congr R1 R3 (λx, g (f x)) :=
congr_mk (λx1 x2 H, app C2 (app C1 H))
theorem compose21
{T2 : Type} {R2 : T2 → T2 → Prop}
{T3 : Type} {R3 : T3 → T3 → Prop}
{T4 : Type} {R4 : T4 → T4 → Prop}
{g : T2 → T3 → T4} (C3 : congr.class2 R2 R3 R4 g)
⦃T1 : Type⦄ {R1 : T1 → T1 → Prop}
{f1 : T1 → T2} (C1 : congr.class R1 R2 f1)
{f2 : T1 → T3} (C2 : congr.class R1 R3 f2) :
congr.class R1 R4 (λx, g (f1 x) (f2 x)) :=
mk (λx1 x2 H, app2 C3 (app C1 H) (app C2 H))
theorem compose21
{T2 : Type} {R2 : T2 → T2 → Prop}
{T3 : Type} {R3 : T3 → T3 → Prop}
{T4 : Type} {R4 : T4 → T4 → Prop}
{g : T2 → T3 → T4} (C3 : congr2 R2 R3 R4 g)
⦃T1 : Type⦄ {R1 : T1 → T1 → Prop}
{f1 : T1 → T2} (C1 : congr R1 R2 f1)
{f2 : T1 → T3} (C2 : congr R1 R3 f2) :
congr R1 R4 (λx, g (f1 x) (f2 x)) :=
congr_mk (λx1 x2 H, app2 C3 (app C1 H) (app C2 H))
theorem const {T2 : Type} (R2 : T2 → T2 → Prop) (H : relation.reflexive R2)
⦃T1 : Type⦄ (R1 : T1 → T1 → Prop) (c : T2) :
class R1 R2 (λu : T1, c) :=
mk (λx y H1, H c)
theorem const {T2 : Type} (R2 : T2 → T2 → Prop) (H : relation.reflexive R2)
⦃T1 : Type⦄ (R1 : T1 → T1 → Prop) (c : T2) :
congr R1 R2 (λu : T1, c) :=
congr_mk (λx y H1, H c)
end congr
end relation
-- TODO: notice these can't be in the congr namespace, if we want it visible without
-- Notice these can't be in the congr namespace, if we want it visible without
-- using congr.
theorem congr_const [instance] {T2 : Type} (R2 : T2 → T2 → Prop)
{C : relation.is_reflexive.class R2} ⦃T1 : Type⦄ (R1 : T1 → T1 → Prop) (c : T2) :
relation.congr.class R1 R2 (λu : T1, c) :=
relation.congr.const R2 (relation.is_reflexive.app C) R1 c
{C : is_reflexive R2} ⦃T1 : Type⦄ (R1 : T1 → T1 → Prop) (c : T2) :
congr R1 R2 (λu : T1, c) :=
congr.const R2 (is_reflexive.app C) R1 c
theorem congr_trivial [instance] {T : Type} (R : T → T → Prop) :
relation.congr.class R R (λu, u) :=
relation.congr.mk (λx y H, H)
congr R R (λu, u) :=
congr_mk (λx y H, H)
-- Relations that can be coerced to functions / implications
-- ---------------------------------------------------------
namespace relation
inductive mp_like {R : Type → Type → Prop} {a b : Type} (H : R a b) : Prop :=
| mp_like_mk {} : (a → b) → @mp_like R a b H
namespace mp_like
inductive class {R : Type → Type → Prop} {a b : Type} (H : R a b) : Prop :=
| mk {} : (a → b) → @class R a b H
definition app {R : Type → Type → Prop} {a : Type} {b : Type} {H : R a b}
(C : mp_like H) : a → b := mp_like_rec (λx, x) C
definition app {R : Type → Type → Prop} {a : Type} {b : Type} {H : R a b}
(C : class H) : a → b := class_rec (λx, x) C
definition infer ⦃R : Type → Type → Prop⦄ {a : Type} {b : Type} (H : R a b)
{C : class H} : a → b := class_rec (λx, x) C
definition infer ⦃R : Type → Type → Prop⦄ {a : Type} {b : Type} (H : R a b)
{C : mp_like H} : a → b := mp_like_rec (λx, x) C
end mp_like
@ -187,20 +187,21 @@ end mp_like
-- Notation for operations on general symbols
-- ------------------------------------------
namespace operations
namespace general_operations
-- e.g. if R is an instance of the class, then "refl R" is reflexivity for the class
definition refl := is_reflexive.infer
definition symm := is_symmetric.infer
definition trans := is_transitive.infer
definition mp := mp_like.infer
end operations
end general_operations
namespace symbols
-- namespace
--
-- postfix `⁻¹`:100 := operations.symm
-- infixr `⬝`:75 := operations.trans
postfix `⁻¹`:100 := operations.symm
infixr `⬝`:75 := operations.trans
end symbols
-- end symbols
end relation

9
library/standard/tools/fake_simplifier.lean Normal file
View file

@ -0,0 +1,9 @@
import .tactic
using tactic
namespace fake_simplifier
-- until we have the simplifier...
definition simp : tactic := apply @sorry
end fake_simplifier

1
library/standard/tools/tactic.lean
View file

@ -54,4 +54,5 @@ notation `?` t:max := try t
definition repeat1 (t : tactic) : tactic := t ; !t
definition focus (t : tactic) : tactic := focus_at t 0
definition determ (t : tactic) : tactic := at_most t 1
end tactic