refactor(library/init): reorganize files and cleanup notation
This commit is contained in:
Leonardo de Moura
parent
c11bcdc2fd
commit
d5a28f91cc
13 changed files with 312 additions and 221 deletions
|
|
@ -2,7 +2,7 @@
|
|||
-- Released under Apache 2.0 license as described in the file LICENSE.
|
||||
-- Author: Leonardo de Moura
|
||||
prelude
|
||||
import init.datatypes
|
||||
import init.core
|
||||
|
||||
@[inline] def {u} cond {A : Type u} : bool → A → A → A
|
||||
| tt a b := a
|
||||
|
|
|
|||
|
|
@ -1,54 +0,0 @@
|
|||
/-
|
||||
Copyright (c) 2016 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
|
||||
universe variables u v
|
||||
|
||||
/- Type class used to implement polymorphic notation for collections.
|
||||
Example: {a, b, c}. -/
|
||||
class insertable (A : Type u) (C : Type u → Type v) :=
|
||||
(empty : C A) (insert : A → C A → C A)
|
||||
|
||||
section
|
||||
variables {A : Type u} {C : Type u → Type v}
|
||||
variable [insertable A C]
|
||||
|
||||
def insert : A → C A → C A :=
|
||||
insertable.insert
|
||||
|
||||
/- The empty collection -/
|
||||
def empty_col : C A :=
|
||||
insertable.empty A C
|
||||
|
||||
notation `∅` := empty_col
|
||||
|
||||
def singleton (a : A) : C A :=
|
||||
insert a ∅
|
||||
end
|
||||
|
||||
/- Type class used to implement the notation [ a ∈ c | p a ] -/
|
||||
class decidable_separable (A : Type u) (C : Type u → Type v) :=
|
||||
(sep : ∀ (p : A → Prop) [decidable_pred p], C A → C A)
|
||||
|
||||
section
|
||||
variables {A : Type u} {C : Type u → Type v}
|
||||
variable [decidable_separable A C]
|
||||
|
||||
def dec_sep (p : A → Prop) [decidable_pred p] : C A → C A :=
|
||||
decidable_separable.sep p
|
||||
end
|
||||
|
||||
/- Type class used to implement the notation { a ∈ c | p a } -/
|
||||
class separable (A : Type u) (C : Type u → Type v) :=
|
||||
(sep : (A → Prop) → C A → C A)
|
||||
|
||||
section
|
||||
variables {A : Type u} {C : Type u → Type v}
|
||||
variable [separable A C]
|
||||
|
||||
def sep : (A → Prop) → C A → C A :=
|
||||
separable.sep
|
||||
end
|
||||
|
|
@ -3,7 +3,7 @@ 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 and notation
|
||||
notation, basic datatypes and type classes
|
||||
-/
|
||||
prelude
|
||||
|
||||
|
|
@ -11,6 +11,73 @@ notation `Prop` := Type 0
|
|||
notation `Type₂` := Type 2
|
||||
notation `Type₃` := Type 3
|
||||
|
||||
/- Logical operations and relations -/
|
||||
|
||||
reserve prefix `¬`:40
|
||||
reserve prefix `~`:40
|
||||
reserve infixr ` ∧ `:35
|
||||
reserve infixr ` /\ `:35
|
||||
reserve infixr ` \/ `:30
|
||||
reserve infixr ` ∨ `:30
|
||||
reserve infix ` <-> `:20
|
||||
reserve infix ` ↔ `:20
|
||||
reserve infix ` = `:50
|
||||
reserve infix ` ≠ `:50
|
||||
reserve infix ` ≈ `:50
|
||||
reserve infix ` ~ `:50
|
||||
reserve infix ` ≡ `:50
|
||||
reserve infixl ` ⬝ `:75
|
||||
reserve infixr ` ▸ `:75
|
||||
reserve infixr ` ▹ `:75
|
||||
|
||||
/- types and type constructors -/
|
||||
|
||||
reserve infixr ` ⊕ `:30
|
||||
reserve infixr ` × `:35
|
||||
|
||||
/- arithmetic operations -/
|
||||
|
||||
reserve infixl ` + `:65
|
||||
reserve infixl ` - `:65
|
||||
reserve infixl ` * `:70
|
||||
reserve infixl ` / `:70
|
||||
reserve infixl ` % `:70
|
||||
reserve prefix `-`:100
|
||||
reserve infix ` ^ `:80
|
||||
|
||||
reserve infixr ` ∘ `:90 -- input with \comp
|
||||
|
||||
reserve infix ` <= `:50
|
||||
reserve infix ` ≤ `:50
|
||||
reserve infix ` < `:50
|
||||
reserve infix ` >= `:50
|
||||
reserve infix ` ≥ `:50
|
||||
reserve infix ` > `:50
|
||||
|
||||
/- boolean operations -/
|
||||
|
||||
reserve infixl ` && `:70
|
||||
reserve infixl ` || `:65
|
||||
|
||||
/- set operations -/
|
||||
|
||||
reserve infix ` ∈ `:50
|
||||
reserve infix ` ∉ `:50
|
||||
reserve infixl ` ∩ `:70
|
||||
reserve infixl ` ∪ `:65
|
||||
reserve infix ` ⊆ `:50
|
||||
reserve infix ` ⊇ `:50
|
||||
reserve infix ` ⊂ `:50
|
||||
reserve infix ` ⊃ `:50
|
||||
reserve infix `\`:70
|
||||
|
||||
/- other symbols -/
|
||||
|
||||
reserve infix ` ∣ `:50
|
||||
reserve infixl ` ++ `:65
|
||||
reserve infixr ` :: `:67
|
||||
reserve infixl `; `:1
|
||||
|
||||
universe variables u v
|
||||
|
||||
inductive poly_unit : Type u
|
||||
|
|
@ -26,6 +93,9 @@ inductive false : Prop
|
|||
|
||||
inductive empty : Type
|
||||
|
||||
def not (a : Prop) := a → false
|
||||
prefix `¬` := not
|
||||
|
||||
inductive eq {A : Type u} (a : A) : A → Prop
|
||||
| refl : eq a
|
||||
|
||||
|
|
@ -92,6 +162,22 @@ inductive bool : Type
|
|||
| ff : bool
|
||||
| tt : bool
|
||||
|
||||
class inductive decidable (p : Prop)
|
||||
| is_false : ¬p → decidable
|
||||
| is_true : p → decidable
|
||||
|
||||
@[reducible]
|
||||
def decidable_pred {A : Type u} (r : A → Prop) :=
|
||||
Π (a : A), decidable (r a)
|
||||
|
||||
@[reducible]
|
||||
def decidable_rel {A : Type u} (r : A → A → Prop) :=
|
||||
Π (a b : A), decidable (r a b)
|
||||
|
||||
@[reducible]
|
||||
def decidable_eq (A : Type u) :=
|
||||
decidable_rel (@eq A)
|
||||
|
||||
inductive option (A : Type u)
|
||||
| none {} : option
|
||||
| some : A → option
|
||||
|
|
@ -109,43 +195,85 @@ inductive nat
|
|||
|
||||
/- Declare builtin and reserved notation -/
|
||||
|
||||
class has_zero (A : Type u) := (zero : A)
|
||||
class has_one (A : Type u) := (one : A)
|
||||
class has_add (A : Type u) := (add : A → A → A)
|
||||
class has_mul (A : Type u) := (mul : A → A → A)
|
||||
class has_inv (A : Type u) := (inv : A → A)
|
||||
class has_neg (A : Type u) := (neg : A → A)
|
||||
class has_sub (A : Type u) := (sub : A → A → A)
|
||||
class has_div (A : Type u) := (div : A → A → A)
|
||||
class has_dvd (A : Type u) := (dvd : A → A → Prop)
|
||||
class has_mod (A : Type u) := (mod : A → A → A)
|
||||
class has_le (A : Type u) := (le : A → A → Prop)
|
||||
class has_lt (A : Type u) := (lt : A → A → Prop)
|
||||
class has_append (A : Type u) := (append : A → A → A)
|
||||
class has_andthen(A : Type u) := (andthen : A → A → A)
|
||||
class has_zero (A : Type u) := (zero : A)
|
||||
class has_one (A : Type u) := (one : A)
|
||||
class has_add (A : Type u) := (add : A → A → A)
|
||||
class has_mul (A : Type u) := (mul : A → A → A)
|
||||
class has_inv (A : Type u) := (inv : A → A)
|
||||
class has_neg (A : Type u) := (neg : A → A)
|
||||
class has_sub (A : Type u) := (sub : A → A → A)
|
||||
class has_div (A : Type u) := (div : A → A → A)
|
||||
class has_dvd (A : Type u) := (dvd : A → A → Prop)
|
||||
class has_mod (A : Type u) := (mod : A → A → A)
|
||||
class has_le (A : Type u) := (le : A → A → Prop)
|
||||
class has_lt (A : Type u) := (lt : A → A → Prop)
|
||||
class has_append (A : Type u) := (append : A → A → A)
|
||||
class has_andthen (A : Type u) := (andthen : A → A → A)
|
||||
class has_union (A : Type u) := (union : A → A → A)
|
||||
class has_inter (A : Type u) := (inter : A → A → A)
|
||||
class has_sdiff (A : Type u) := (sdiff : A → A → A)
|
||||
class has_subset (A : Type u) := (subset : A → A → Prop)
|
||||
class has_ssubset (A : Type u) := (ssubset : A → A → Prop)
|
||||
/- Type class used to implement polymorphic notation for collections.
|
||||
Example: {a, b, c}. -/
|
||||
class insertable (A : Type u) (C : Type u → Type v) :=
|
||||
(empty : C A) (insert : A → C A → C A)
|
||||
/- Type class used to implement the notation { a ∈ c | p a } -/
|
||||
class separable (A : Type u) (C : Type u → Type v) :=
|
||||
(sep : (A → Prop) → C A → C A)
|
||||
/- Type class for set-like membership -/
|
||||
class has_mem (A : Type u) (C : Type u → Type v) := (mem : A → C A → Prop)
|
||||
|
||||
def zero {A : Type u} [has_zero A] : A := has_zero.zero A
|
||||
def one {A : Type u} [has_one A] : A := has_one.one A
|
||||
def add {A : Type u} [has_add A] : A → A → A := has_add.add
|
||||
def mul {A : Type u} [has_mul A] : A → A → A := has_mul.mul
|
||||
def sub {A : Type u} [has_sub A] : A → A → A := has_sub.sub
|
||||
def div {A : Type u} [has_div A] : A → A → A := has_div.div
|
||||
def dvd {A : Type u} [has_dvd A] : A → A → Prop := has_dvd.dvd
|
||||
def mod {A : Type u} [has_mod A] : A → A → A := has_mod.mod
|
||||
def neg {A : Type u} [has_neg A] : A → A := has_neg.neg
|
||||
def inv {A : Type u} [has_inv A] : A → A := has_inv.inv
|
||||
def le {A : Type u} [has_le A] : A → A → Prop := has_le.le
|
||||
def lt {A : Type u} [has_lt A] : A → A → Prop := has_lt.lt
|
||||
def append {A : Type u} [has_append A] : A → A → A := has_append.append
|
||||
def andthen {A : Type u} [has_andthen A] : A → A → A := has_andthen.andthen
|
||||
|
||||
@[reducible] def ge {A : Type u} [s : has_le A] (a b : A) : Prop := le b a
|
||||
@[reducible] def gt {A : Type u} [s : has_lt A] (a b : A) : Prop := lt b a
|
||||
def zero {A : Type u} [has_zero A] : A := has_zero.zero A
|
||||
def one {A : Type u} [has_one A] : A := has_one.one A
|
||||
def add {A : Type u} [has_add A] : A → A → A := has_add.add
|
||||
def mul {A : Type u} [has_mul A] : A → A → A := has_mul.mul
|
||||
def sub {A : Type u} [has_sub A] : A → A → A := has_sub.sub
|
||||
def div {A : Type u} [has_div A] : A → A → A := has_div.div
|
||||
def dvd {A : Type u} [has_dvd A] : A → A → Prop := has_dvd.dvd
|
||||
def mod {A : Type u} [has_mod A] : A → A → A := has_mod.mod
|
||||
def neg {A : Type u} [has_neg A] : A → A := has_neg.neg
|
||||
def inv {A : Type u} [has_inv A] : A → A := has_inv.inv
|
||||
def le {A : Type u} [has_le A] : A → A → Prop := has_le.le
|
||||
def lt {A : Type u} [has_lt A] : A → A → Prop := has_lt.lt
|
||||
def append {A : Type u} [has_append A] : A → A → A := has_append.append
|
||||
def andthen {A : Type u} [has_andthen A] : A → A → A := has_andthen.andthen
|
||||
def union {A : Type u} [has_union A] : A → A → A := has_union.union
|
||||
def inter {A : Type u} [has_inter A] : A → A → A := has_inter.inter
|
||||
def sdiff {A : Type u} [has_sdiff A] : A → A → A := has_sdiff.sdiff
|
||||
def subset {A : Type u} [has_subset A] : A → A → Prop := has_subset.subset
|
||||
def ssubset {A : Type u} [has_ssubset A] : A → A → Prop := has_ssubset.ssubset
|
||||
@[reducible]
|
||||
def ge {A : Type u} [has_le A] (a b : A) : Prop := le b a
|
||||
@[reducible]
|
||||
def gt {A : Type u} [has_lt A] (a b : A) : Prop := lt b a
|
||||
@[reducible]
|
||||
def superset {A : Type u} [has_subset A] (a b : A) : Prop := subset b a
|
||||
@[reducible]
|
||||
def ssuperset {A : Type u} [has_ssubset A] (a b : A) : Prop := ssubset b a
|
||||
def bit0 {A : Type u} [s : has_add A] (a : A) : A := add a a
|
||||
def bit1 {A : Type u} [s₁ : has_one A] [s₂ : has_add A] (a : A) : A := add (bit0 a) one
|
||||
|
||||
attribute [pattern] zero one bit0 bit1 add
|
||||
|
||||
def insert {A : Type u} {C : Type u → Type v} [insertable A C] : A → C A → C A :=
|
||||
insertable.insert
|
||||
|
||||
/- The empty collection -/
|
||||
def empty_col {A : Type u} {C : Type u → Type v} [insertable A C] : C A :=
|
||||
insertable.empty A C
|
||||
|
||||
def singleton {A : Type u} {C : Type u → Type v} [insertable A C] (a : A) : C A :=
|
||||
insert a empty_col
|
||||
|
||||
def sep {A : Type u} {C : Type u → Type v} [separable A C] : (A → Prop) → C A → C A :=
|
||||
separable.sep
|
||||
|
||||
def mem {A : Type u} {C : Type u → Type v} [has_mem A C] : A → C A → Prop :=
|
||||
has_mem.mem
|
||||
|
||||
/- num, pos_num instances -/
|
||||
|
||||
instance : has_zero num :=
|
||||
⟨num.zero⟩
|
||||
|
||||
|
|
@ -195,6 +323,8 @@ instance : has_add num :=
|
|||
def std.priority.default : num := 1000
|
||||
def std.priority.max : num := 4294967295
|
||||
|
||||
/- nat basic instances -/
|
||||
|
||||
namespace nat
|
||||
protected def prio := num.add std.priority.default 100
|
||||
|
||||
|
|
@ -234,92 +364,37 @@ def std.prec.max_plus :=
|
|||
num.succ (num.succ (num.succ (num.succ (num.succ (num.succ (num.succ (num.succ (num.succ
|
||||
(num.succ std.prec.max)))))))))
|
||||
|
||||
/- Logical operations and relations -/
|
||||
|
||||
reserve prefix `¬`:40
|
||||
reserve prefix `~`:40
|
||||
reserve infixr ` ∧ `:35
|
||||
reserve infixr ` /\ `:35
|
||||
reserve infixr ` \/ `:30
|
||||
reserve infixr ` ∨ `:30
|
||||
reserve infix ` <-> `:20
|
||||
reserve infix ` ↔ `:20
|
||||
reserve infix ` = `:50
|
||||
reserve infix ` ≠ `:50
|
||||
reserve infix ` ≈ `:50
|
||||
reserve infix ` ~ `:50
|
||||
reserve infix ` ≡ `:50
|
||||
reserve infixl ` ⬝ `:75
|
||||
reserve infixr ` ▸ `:75
|
||||
reserve infixr ` ▹ `:75
|
||||
|
||||
/- types and type constructors -/
|
||||
|
||||
reserve infixr ` ⊕ `:30
|
||||
reserve infixr ` × `:35
|
||||
|
||||
/- arithmetic operations -/
|
||||
|
||||
reserve infixl ` + `:65
|
||||
reserve infixl ` - `:65
|
||||
reserve infixl ` * `:70
|
||||
reserve infixl ` / `:70
|
||||
reserve infixl ` % `:70
|
||||
reserve prefix `-`:100
|
||||
reserve infix ` ^ `:80
|
||||
|
||||
reserve infixr ` ∘ `:90 -- input with \comp
|
||||
reserve postfix `⁻¹`:std.prec.max_plus -- input with \sy or \-1 or \inv
|
||||
|
||||
reserve infix ` <= `:50
|
||||
reserve infix ` ≤ `:50
|
||||
reserve infix ` < `:50
|
||||
reserve infix ` >= `:50
|
||||
reserve infix ` ≥ `:50
|
||||
reserve infix ` > `:50
|
||||
|
||||
/- boolean operations -/
|
||||
|
||||
reserve infixl ` && `:70
|
||||
reserve infixl ` || `:65
|
||||
|
||||
/- set operations -/
|
||||
|
||||
reserve infix ` ∈ `:50
|
||||
reserve infix ` ∉ `:50
|
||||
reserve infixl ` ∩ `:70
|
||||
reserve infixl ` ∪ `:65
|
||||
reserve infix ` ⊆ `:50
|
||||
reserve infix ` ⊇ `:50
|
||||
reserve infix ` ' `:75 -- for the image of a set under a function
|
||||
reserve infix ` '- `:75 -- for the preimage of a set under a function
|
||||
|
||||
/- other symbols -/
|
||||
|
||||
reserve infix ` ∣ `:50
|
||||
reserve infixl ` ++ `:65
|
||||
reserve infixr ` :: `:67
|
||||
reserve infixl `; `:1
|
||||
|
||||
infix + := add
|
||||
infix * := mul
|
||||
infix - := sub
|
||||
infix / := div
|
||||
infix ∣ := dvd
|
||||
infix % := mod
|
||||
prefix - := neg
|
||||
postfix ⁻¹ := inv
|
||||
infix <= := le
|
||||
infix >= := ge
|
||||
infix ≤ := le
|
||||
infix ≥ := ge
|
||||
infix < := lt
|
||||
infix > := gt
|
||||
infix ++ := append
|
||||
infix ; := andthen
|
||||
infix = := eq
|
||||
infix ∈ := mem
|
||||
notation a ∉ s := ¬ mem a s
|
||||
infix + := add
|
||||
infix * := mul
|
||||
infix - := sub
|
||||
infix / := div
|
||||
infix ∣ := dvd
|
||||
infix % := mod
|
||||
prefix - := neg
|
||||
postfix ⁻¹ := inv
|
||||
infix <= := le
|
||||
infix >= := ge
|
||||
infix ≤ := le
|
||||
infix ≥ := ge
|
||||
infix < := lt
|
||||
infix > := gt
|
||||
infix ++ := append
|
||||
infix ; := andthen
|
||||
notation `∅` := empty_col
|
||||
infix ∪ := union
|
||||
infix ∩ := inter
|
||||
infix ⊆ := subset
|
||||
infix ⊇ := superset
|
||||
infix ⊂ := ssubset
|
||||
infix ⊃ := ssuperset
|
||||
infix \ := sdiff
|
||||
|
||||
/- eq basic support -/
|
||||
notation a = b := eq a b
|
||||
|
||||
@[pattern] def rfl {A : Type u} {a : A} : a = a := eq.refl a
|
||||
|
||||
|
|
@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
|
|||
Authors: Leonardo de Moura
|
||||
-/
|
||||
prelude
|
||||
import init.datatypes init.logic
|
||||
import init.core init.logic
|
||||
import init.relation init.nat init.prod init.sum init.combinator
|
||||
import init.bool init.unit init.num init.sigma init.setoid init.quot
|
||||
import init.funext init.function init.subtype init.classical
|
||||
|
|
|
|||
|
|
@ -18,12 +18,52 @@ instance (A : Type u) : inhabited (list A) :=
|
|||
variables {A : Type u} {B : Type v}
|
||||
|
||||
namespace list
|
||||
def append : list A → list A → list A
|
||||
protected def append : list A → list A → list A
|
||||
| [] l := l
|
||||
| (h :: s) t := h :: (append s t)
|
||||
|
||||
instance : has_append (list A) :=
|
||||
⟨append⟩
|
||||
⟨list.append⟩
|
||||
|
||||
protected def mem : A → list A → Prop
|
||||
| a [] := false
|
||||
| a (b :: l) := a = b ∨ mem a l
|
||||
|
||||
instance : has_mem A list :=
|
||||
⟨list.mem⟩
|
||||
|
||||
instance decidable_mem [decidable_eq A] (a : A) : ∀ (l : list A), decidable (a ∈ l)
|
||||
| [] := is_false not_false
|
||||
| (b::l) :=
|
||||
if h₁ : a = b then is_true (or.inl h₁)
|
||||
else match decidable_mem l with
|
||||
| is_true h₂ := is_true (or.inr h₂)
|
||||
| is_false h₂ := is_false (not_or h₁ h₂)
|
||||
end
|
||||
|
||||
def concat : list A → A → list A
|
||||
| [] a := [a]
|
||||
| (b::l) a := b :: concat l a
|
||||
|
||||
protected def insert [decidable_eq A] (a : A) (l : list A) : list A :=
|
||||
if a ∈ l then l else concat l a
|
||||
|
||||
instance [decidable_eq A] : insertable A list :=
|
||||
⟨list.nil, list.insert⟩
|
||||
|
||||
protected def union [decidable_eq A] : list A → list A → list A
|
||||
| l₁ [] := l₁
|
||||
| l₁ (a::l₂) := union (insert a l₁) l₂
|
||||
|
||||
instance [decidable_eq A] : has_union (list A) :=
|
||||
⟨list.union⟩
|
||||
|
||||
protected def inter [decidable_eq A] : list A → list A → list A
|
||||
| [] l₂ := []
|
||||
| (a::l₁) l₂ := if a ∈ l₂ then a :: inter l₁ l₂ else inter l₁ l₂
|
||||
|
||||
instance [decidable_eq A] : has_inter (list A) :=
|
||||
⟨list.inter⟩
|
||||
|
||||
def length : list A → nat
|
||||
| [] := 0
|
||||
|
|
@ -44,13 +84,9 @@ def tail : list A → list A
|
|||
| [] := []
|
||||
| (a :: l) := l
|
||||
|
||||
def concat : Π (x : A), list A → list A
|
||||
| a [] := [a]
|
||||
| a (b :: l) := b :: concat a l
|
||||
|
||||
def reverse : list A → list A
|
||||
| [] := []
|
||||
| (a :: l) := concat a (reverse l)
|
||||
| (a :: l) := concat (reverse l) a
|
||||
|
||||
def map (f : A → B) : list A → list B
|
||||
| [] := []
|
||||
|
|
|
|||
|
|
@ -9,17 +9,14 @@ open list
|
|||
|
||||
universe variables u v
|
||||
|
||||
@[inline] def list_fmap {A : Type u} {B : Type v} (f : A → B) (l : list A) : list B :=
|
||||
map f l
|
||||
|
||||
@[inline] def list_bind {A : Type u} {B : Type v} (a : list A) (b : A → list B) : list B :=
|
||||
@[inline] def list.bind {A : Type u} {B : Type v} (a : list A) (b : A → list B) : list B :=
|
||||
join (map b a)
|
||||
|
||||
@[inline] def list_return {A : Type u} (a : A) : list A :=
|
||||
@[inline] def list.ret {A : Type u} (a : A) : list A :=
|
||||
[a]
|
||||
|
||||
instance : monad list :=
|
||||
⟨@list_fmap, @list_return, @list_bind⟩
|
||||
⟨@map, @list.ret, @list.bind⟩
|
||||
|
||||
instance : alternative list :=
|
||||
⟨@list_fmap, @list_return, @fapp _ _, @nil, @list.append⟩
|
||||
⟨@map, @list.ret, @fapp _ _, @nil, @list.append⟩
|
||||
|
|
|
|||
|
|
@ -4,7 +4,7 @@ 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
|
||||
import init.core
|
||||
|
||||
universe variables u v w
|
||||
|
||||
|
|
@ -22,9 +22,6 @@ assume hp, h₂ (h₁ hp)
|
|||
|
||||
def trivial : true := ⟨⟩
|
||||
|
||||
def not (a : Prop) := a → false
|
||||
prefix `¬` := not
|
||||
|
||||
@[inline] def absurd {a : Prop} {b : Type v} (h₁ : a) (h₂ : ¬a) : b :=
|
||||
false.rec b (h₂ h₁)
|
||||
|
||||
|
|
@ -509,6 +506,10 @@ attribute [simp]
|
|||
lemma or_self (a : Prop) : a ∨ a ↔ a :=
|
||||
iff.intro (or.rec id id) or.inl
|
||||
|
||||
lemma not_or {a b : Prop} : ¬ a → ¬ b → ¬ (a ∨ b)
|
||||
| hna hnb (or.inl ha) := absurd ha hna
|
||||
| hna hnb (or.inr hb) := absurd hb hnb
|
||||
|
||||
/- or resolution rulse -/
|
||||
|
||||
def or.resolve_left {a b : Prop} (h : a ∨ b) (na : ¬ a) : b :=
|
||||
|
|
@ -616,11 +617,10 @@ exists_congr (λ x, and_congr (h x) (forall_congr (λ y, imp_congr (h y) iff.rfl
|
|||
|
||||
/- decidable -/
|
||||
|
||||
class inductive decidable (p : Prop)
|
||||
| is_false : ¬p → decidable
|
||||
| is_true : p → decidable
|
||||
def decidable.to_bool (p : Prop) [h : decidable p] : bool :=
|
||||
decidable.cases_on h (λ h₁, bool.ff) (λ h₂, bool.tt)
|
||||
|
||||
export decidable (is_true is_false)
|
||||
export decidable (is_true is_false to_bool)
|
||||
|
||||
instance decidable.true : decidable true :=
|
||||
is_true trivial
|
||||
|
|
@ -655,9 +655,6 @@ namespace decidable
|
|||
|
||||
lemma by_contradiction [decidable p] (h : ¬p → false) : p :=
|
||||
if h₁ : p then h₁ else false.rec _ (h h₁)
|
||||
|
||||
def to_bool (p : Prop) [h : decidable p] : bool :=
|
||||
decidable.cases_on h (λ h₁, bool.ff) (λ h₂, bool.tt)
|
||||
end decidable
|
||||
|
||||
section
|
||||
|
|
@ -703,10 +700,6 @@ section
|
|||
and.decidable
|
||||
end
|
||||
|
||||
@[reducible] def decidable_pred {A : Type u} (r : A → Prop) := Π (a : A), decidable (r a)
|
||||
@[reducible] def decidable_rel {A : Type u} (r : A → A → Prop) := Π (a b : A), decidable (r a b)
|
||||
@[reducible] def decidable_eq (A : Type u) := decidable_rel (@eq A)
|
||||
|
||||
instance {A : Type u} [decidable_eq A] (a b : A) : decidable (a ≠ b) :=
|
||||
implies.decidable
|
||||
|
||||
|
|
|
|||
|
|
@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
|
|||
Authors: Leonardo de Moura
|
||||
-/
|
||||
prelude
|
||||
import init.logic init.collection
|
||||
import init.logic init.functor
|
||||
|
||||
universe variables u v
|
||||
|
||||
|
|
@ -16,19 +16,17 @@ p
|
|||
namespace set
|
||||
variables {A : Type u} {B : Type v}
|
||||
|
||||
def mem (a : A) (s : set A) :=
|
||||
protected def mem (a : A) (s : set A) :=
|
||||
s a
|
||||
|
||||
infix ∈ := mem
|
||||
notation a ∉ s := ¬ mem a s
|
||||
instance : has_mem A set :=
|
||||
⟨set.mem⟩
|
||||
|
||||
def subset (s₁ s₂ : set A) : Prop :=
|
||||
∀ ⦃a⦄, a ∈ s₁ → a ∈ s₂
|
||||
infix ⊆ := subset
|
||||
protected def subset (s₁ s₂ : set A) :=
|
||||
∀ a, a ∈ s₁ → a ∈ s₂
|
||||
|
||||
def superset (s₁ s₂ : set A) : Prop :=
|
||||
s₂ ⊆ s₁
|
||||
infix ⊇ := superset
|
||||
instance : has_subset (set A) :=
|
||||
⟨set.subset⟩
|
||||
|
||||
private def sep (p : A → Prop) (s : set A) : set A :=
|
||||
{a | a ∈ s ∧ p a}
|
||||
|
|
@ -45,13 +43,17 @@ private def insert (a : A) (s : set A) : set A :=
|
|||
instance : insertable A set :=
|
||||
⟨empty, insert⟩
|
||||
|
||||
def union (s₁ s₂ : set A) : set A :=
|
||||
protected def union (s₁ s₂ : set A) : set A :=
|
||||
{a | a ∈ s₁ ∨ a ∈ s₂}
|
||||
notation s₁ ∪ s₂ := union s₁ s₂
|
||||
|
||||
def inter (s₁ s₂ : set A) : set A :=
|
||||
instance : has_union (set A) :=
|
||||
⟨set.union⟩
|
||||
|
||||
protected def inter (s₁ s₂ : set A) : set A :=
|
||||
{a | a ∈ s₁ ∧ a ∈ s₂}
|
||||
notation s₁ ∩ s₂ := inter s₁ s₂
|
||||
|
||||
instance : has_inter (set A) :=
|
||||
⟨set.inter⟩
|
||||
|
||||
def compl (s : set A) : set A :=
|
||||
{a | a ∉ s}
|
||||
|
|
@ -59,9 +61,11 @@ def compl (s : set A) : set A :=
|
|||
instance : has_neg (set A) :=
|
||||
⟨compl⟩
|
||||
|
||||
def diff (s t : set A) : set A :=
|
||||
protected def diff (s t : set A) : set A :=
|
||||
{a ∈ s | a ∉ t}
|
||||
infix `\`:70 := diff
|
||||
|
||||
instance : has_sdiff (set A) :=
|
||||
⟨set.diff⟩
|
||||
|
||||
def powerset (s : set A) : set (set A) :=
|
||||
{t | t ⊆ s}
|
||||
|
|
@ -69,5 +73,8 @@ prefix `𝒫`:100 := powerset
|
|||
|
||||
def image (f : A → B) (s : set A) : set B :=
|
||||
{b | ∃ a, a ∈ s ∧ f a = b}
|
||||
infix ` ' ` := image
|
||||
|
||||
instance : functor set :=
|
||||
⟨@set.image⟩
|
||||
|
||||
end set
|
||||
|
|
|
|||
|
|
@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
|
|||
Author: Leonardo de Moura, Jeremy Avigad, Floris van Doorn
|
||||
-/
|
||||
prelude
|
||||
import init.datatypes init.num init.wf init.logic
|
||||
import init.logic init.num init.wf
|
||||
|
||||
definition dpair := @sigma.mk
|
||||
notation `Σ` binders `, ` r:(scoped P, sigma P) := r
|
||||
|
|
|
|||
|
|
@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
|
|||
Author: Leonardo de Moura, Jeremy Avigad
|
||||
-/
|
||||
prelude
|
||||
import init.datatypes init.logic
|
||||
import init.logic
|
||||
open decidable
|
||||
|
||||
universe variables u
|
||||
|
|
|
|||
|
|
@ -82,7 +82,7 @@ void init_token_table(token_table & t) {
|
|||
{"have", 0}, {"suppose", 0}, {"show", 0}, {"suffices", 0}, {"obtain", 0},
|
||||
{"do", 0}, {"if", 0}, {"then", 0}, {"else", 0}, {"by", 0}, {"hiding", 0}, {"replacing", 0}, {"renaming", 0},
|
||||
{"from", 0}, {"(", g_max_prec}, {"`(", g_max_prec}, {"`", g_max_prec},
|
||||
{"%%", g_max_prec}, {"()", g_max_prec}, {")", 0},
|
||||
{"%%", g_max_prec}, {"()", g_max_prec}, {")", 0}, {"'", 0},
|
||||
{"{", g_max_prec}, {"}", 0}, {"_", g_max_prec},
|
||||
{"[", g_max_prec}, {"]", 0}, {"⦃", g_max_prec}, {"⦄", 0}, {".{", 0}, {"Type", g_max_prec}, {"Type*", g_max_prec},
|
||||
{"{|", g_max_prec}, {"|}", 0}, {"(:", g_max_prec}, {":)", 0},
|
||||
|
|
|
|||
27
tests/lean/run/list_notation.lean
Normal file
27
tests/lean/run/list_notation.lean
Normal file
|
|
@ -0,0 +1,27 @@
|
|||
open nat
|
||||
|
||||
vm_eval [1, 2, 3]
|
||||
|
||||
vm_eval to_bool $ 1 ∈ [1, 2, 3]
|
||||
|
||||
vm_eval to_bool $ 4 ∈ [1, 2, 3]
|
||||
|
||||
vm_eval [1, 2, 3] ++ [3, 4]
|
||||
|
||||
vm_eval 2 :: [3, 4]
|
||||
|
||||
vm_eval ([] : list nat)
|
||||
|
||||
vm_eval (∅ : list nat)
|
||||
|
||||
vm_eval ({1, 3, 2, 2, 3, 1} : list nat)
|
||||
|
||||
vm_eval [1, 2, 3] ∪ [3, 4, 1, 5]
|
||||
|
||||
vm_eval [1, 2, 3] ∩ [3, 4, 1, 5]
|
||||
|
||||
vm_eval (mul 10) <$> [1, 2, 3]
|
||||
|
||||
check ({1, 2, 3} : list nat)
|
||||
|
||||
check ({1, 2, 3, 4} : set nat)
|
||||
|
|
@ -1,7 +1,6 @@
|
|||
alternative : (Type u → Type v) → Type (max (u+1) v)
|
||||
applicative : (Type u → Type v) → Type (max (u+1) v)
|
||||
decidable : Prop → Type
|
||||
decidable_separable : Type u → (Type u → Type v) → Type (max 1 (imax (max 1 u) (max 1 u) v))
|
||||
functor : (Type u → Type v) → Type (max (u+1) v)
|
||||
has_add : Type u → Type (max 1 u)
|
||||
has_andthen : Type u → Type (max 1 u)
|
||||
|
|
@ -12,22 +11,28 @@ has_coe_to_fun : Type u → Type (max u (v+1))
|
|||
has_coe_to_sort : Type u → Type (max u (v+1))
|
||||
has_div : Type u → Type (max 1 u)
|
||||
has_dvd : Type u → Type (max 1 u)
|
||||
has_inter : Type u → Type (max 1 u)
|
||||
has_inv : Type u → Type (max 1 u)
|
||||
has_le : Type u → Type (max 1 u)
|
||||
has_lift : Type u → Type v → Type (max 1 (imax u v))
|
||||
has_lift_t : Type u → Type v → Type (max 1 (imax u v))
|
||||
has_lt : Type u → Type (max 1 u)
|
||||
has_mem : Type u → (Type u → Type v) → Type (max 1 u v)
|
||||
has_mod : Type u → Type (max 1 u)
|
||||
has_mul : Type u → Type (max 1 u)
|
||||
has_neg : Type u → Type (max 1 u)
|
||||
has_one : Type u → Type (max 1 u)
|
||||
has_ordering : Type → Type
|
||||
has_sdiff : Type u → Type (max 1 u)
|
||||
has_sizeof : Type u → Type (max 1 u)
|
||||
has_ssubset : Type u → Type (max 1 u)
|
||||
has_sub : Type u → Type (max 1 u)
|
||||
has_subset : Type u → Type (max 1 u)
|
||||
has_to_format : Type u → Type (max 1 u)
|
||||
has_to_pexpr : Type u → Type (max 1 u)
|
||||
has_to_string : Type u → Type (max 1 u)
|
||||
has_to_tactic_format : Type → Type
|
||||
has_union : Type u → Type (max 1 u)
|
||||
has_zero : Type u → Type (max 1 u)
|
||||
inhabited : Type u → Type (max 1 u)
|
||||
insertable : Type u → (Type u → Type v) → Type (max 1 (imax u v) v)
|
||||
|
|
@ -41,7 +46,6 @@ subsingleton : Type u → Prop
|
|||
alternative : (Type u → Type v) → Type (max (u+1) v)
|
||||
applicative : (Type u → Type v) → Type (max (u+1) v)
|
||||
decidable : Prop → Type
|
||||
decidable_separable : Type u → (Type u → Type v) → Type (max 1 (imax (max 1 u) (max 1 u) v))
|
||||
functor : (Type u → Type v) → Type (max (u+1) v)
|
||||
has_add : Type u → Type (max 1 u)
|
||||
has_andthen : Type u → Type (max 1 u)
|
||||
|
|
@ -52,22 +56,28 @@ has_coe_to_fun : Type u → Type (max u (v+1))
|
|||
has_coe_to_sort : Type u → Type (max u (v+1))
|
||||
has_div : Type u → Type (max 1 u)
|
||||
has_dvd : Type u → Type (max 1 u)
|
||||
has_inter : Type u → Type (max 1 u)
|
||||
has_inv : Type u → Type (max 1 u)
|
||||
has_le : Type u → Type (max 1 u)
|
||||
has_lift : Type u → Type v → Type (max 1 (imax u v))
|
||||
has_lift_t : Type u → Type v → Type (max 1 (imax u v))
|
||||
has_lt : Type u → Type (max 1 u)
|
||||
has_mem : Type u → (Type u → Type v) → Type (max 1 u v)
|
||||
has_mod : Type u → Type (max 1 u)
|
||||
has_mul : Type u → Type (max 1 u)
|
||||
has_neg : Type u → Type (max 1 u)
|
||||
has_one : Type u → Type (max 1 u)
|
||||
has_ordering : Type → Type
|
||||
has_sdiff : Type u → Type (max 1 u)
|
||||
has_sizeof : Type u → Type (max 1 u)
|
||||
has_ssubset : Type u → Type (max 1 u)
|
||||
has_sub : Type u → Type (max 1 u)
|
||||
has_subset : Type u → Type (max 1 u)
|
||||
has_to_format : Type u → Type (max 1 u)
|
||||
has_to_pexpr : Type u → Type (max 1 u)
|
||||
has_to_string : Type u → Type (max 1 u)
|
||||
has_to_tactic_format : Type → Type
|
||||
has_union : Type u → Type (max 1 u)
|
||||
has_zero : Type u → Type (max 1 u)
|
||||
inhabited : Type u → Type (max 1 u)
|
||||
insertable : Type u → (Type u → Type v) → Type (max 1 (imax u v) v)
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue