feat(frontends/lean): change subtype notation (again)
We had conflicts with the set notation.
This commit is contained in:
Leonardo de Moura
parent
973bc5f1d6
commit
b7abd61579
24 changed files with 112 additions and 126 deletions
|
|
@ -11,58 +11,58 @@ universe variables u v
|
|||
/- the axiom -/
|
||||
|
||||
-- In the presence of classical logic, we could prove this from a weaker statement:
|
||||
-- axiom indefinite_description {A : Type u} {P : A->Prop} (H : ∃ x, P x) : {x : A, P x}
|
||||
axiom strong_indefinite_description {A : Type u} (P : A → Prop) (H : nonempty A) :
|
||||
{ x \ (∃ y : A, P y) → P x}
|
||||
-- axiom indefinite_description {A : Type u} {p : A->Prop} (H : ∃ x, p x) : {x : A, p x}
|
||||
axiom strong_indefinite_description {A : Type u} (p : A → Prop) (H : nonempty A) :
|
||||
{ x : A // (∃ y : A, p y) → p x}
|
||||
|
||||
theorem exists_true_of_nonempty {A : Type u} (H : nonempty A) : ∃ x : A, true :=
|
||||
nonempty.elim H (take x, ⟨x, trivial⟩)
|
||||
theorem exists_true_of_nonempty {A : Type u} (h : nonempty A) : ∃ x : A, true :=
|
||||
nonempty.elim h (take x, ⟨x, trivial⟩)
|
||||
|
||||
noncomputable definition inhabited_of_nonempty {A : Type u} (H : nonempty A) : inhabited A :=
|
||||
⟨elt_of (strong_indefinite_description (λ a, true) H)⟩
|
||||
noncomputable definition inhabited_of_nonempty {A : Type u} (h : nonempty A) : inhabited A :=
|
||||
⟨elt_of (strong_indefinite_description (λ a, true) h)⟩
|
||||
|
||||
noncomputable definition inhabited_of_exists {A : Type u} {P : A → Prop} (H : ∃ x, P x) : inhabited A :=
|
||||
noncomputable definition inhabited_of_exists {A : Type u} {p : A → Prop} (H : ∃ x, p x) : inhabited A :=
|
||||
inhabited_of_nonempty (exists.elim H (λ w Hw, ⟨w⟩))
|
||||
|
||||
/- the Hilbert epsilon function -/
|
||||
|
||||
noncomputable definition epsilon {A : Type u} [H : nonempty A] (P : A → Prop) : A :=
|
||||
elt_of (strong_indefinite_description P H)
|
||||
noncomputable definition epsilon {A : Type u} [h : nonempty A] (p : A → Prop) : A :=
|
||||
elt_of (strong_indefinite_description p h)
|
||||
|
||||
theorem epsilon_spec_aux {A : Type u} (H : nonempty A) (P : A → Prop) (Hex : ∃ y, P y) :
|
||||
P (@epsilon A H P) :=
|
||||
have aux : (∃ y, P y) → P (elt_of (strong_indefinite_description P H)), from has_property (strong_indefinite_description P H),
|
||||
aux Hex
|
||||
theorem epsilon_spec_aux {A : Type u} (h : nonempty A) (p : A → Prop) (hex : ∃ y, p y) :
|
||||
p (@epsilon A h p) :=
|
||||
have aux : (∃ y, p y) → p (elt_of (strong_indefinite_description p h)), from has_property (strong_indefinite_description p h),
|
||||
aux hex
|
||||
|
||||
theorem epsilon_spec {A : Type u} {P : A → Prop} (Hex : ∃ y, P y) :
|
||||
P (@epsilon A (nonempty_of_exists Hex) P) :=
|
||||
epsilon_spec_aux (nonempty_of_exists Hex) P Hex
|
||||
theorem epsilon_spec {A : Type u} {p : A → Prop} (hex : ∃ y, p y) :
|
||||
p (@epsilon A (nonempty_of_exists hex) p) :=
|
||||
epsilon_spec_aux (nonempty_of_exists hex) p hex
|
||||
|
||||
theorem epsilon_singleton {A : Type u} (a : A) : @epsilon A ⟨a⟩ (λ x, x = a) = a :=
|
||||
@epsilon_spec A (λ x, x = a) ⟨a, rfl⟩
|
||||
|
||||
noncomputable definition some {A : Type u} {P : A → Prop} (H : ∃ x, P x) : A :=
|
||||
@epsilon A (nonempty_of_exists H) P
|
||||
noncomputable definition some {A : Type u} {p : A → Prop} (h : ∃ x, p x) : A :=
|
||||
@epsilon A (nonempty_of_exists h) p
|
||||
|
||||
theorem some_spec {A : Type u} {P : A → Prop} (H : ∃ x, P x) : P (some H) :=
|
||||
epsilon_spec H
|
||||
theorem some_spec {A : Type u} {p : A → Prop} (h : ∃ x, p x) : p (some h) :=
|
||||
epsilon_spec h
|
||||
|
||||
/- the axiom of choice -/
|
||||
|
||||
theorem axiom_of_choice {A : Type u} {B : A → Type v} {R : Π x, B x → Prop} (H : ∀ x, ∃ y, R x y) :
|
||||
theorem axiom_of_choice {A : Type u} {B : A → Type v} {R : Π x, B x → Prop} (h : ∀ x, ∃ y, R x y) :
|
||||
∃ (f : Π x, B x), ∀ x, R x (f x) :=
|
||||
have H : ∀ x, R x (some (H x)), from take x, some_spec (H x),
|
||||
⟨_, H⟩
|
||||
have h : ∀ x, R x (some (h x)), from take x, some_spec (h x),
|
||||
⟨_, h⟩
|
||||
|
||||
theorem skolem {A : Type u} {B : A → Type v} {P : Π x, B x → Prop} :
|
||||
(∀ x, ∃ y, P x y) ↔ ∃ (f : Π x, B x) , (∀ x, P x (f x)) :=
|
||||
theorem skolem {A : Type u} {B : A → Type v} {p : Π x, B x → Prop} :
|
||||
(∀ x, ∃ y, p x y) ↔ ∃ (f : Π x, B x) , (∀ x, p x (f x)) :=
|
||||
iff.intro
|
||||
(assume H : (∀ x, ∃ y, P x y), axiom_of_choice H)
|
||||
(assume H : (∃ (f : Π x, B x), (∀ x, P x (f x))),
|
||||
take x, exists.elim H (λ (fw : ∀ x, B x) (Hw : ∀ x, P x (fw x)),
|
||||
⟨fw x, Hw x⟩))
|
||||
(assume h : (∀ x, ∃ y, p x y), axiom_of_choice h)
|
||||
(assume h : (∃ (f : Π x, B x), (∀ x, p x (f x))),
|
||||
take x, exists.elim h (λ (fw : ∀ x, B x) (hw : ∀ x, p x (fw x)),
|
||||
⟨fw x, hw x⟩))
|
||||
/-
|
||||
Prove excluded middle using Hilbert's choice
|
||||
Prove excluded middle using hilbert's choice
|
||||
The proof follows Diaconescu proof that shows that the axiom of choice implies the excluded middle.
|
||||
-/
|
||||
section diaconescu
|
||||
|
|
@ -82,32 +82,32 @@ epsilon_spec ⟨false, or.inl rfl⟩
|
|||
|
||||
private lemma not_uv_or_p : ¬(u = v) ∨ p :=
|
||||
or.elim u_def
|
||||
(assume Hut : u = true,
|
||||
(assume hut : u = true,
|
||||
or.elim v_def
|
||||
(assume Hvf : v = false,
|
||||
have Hne : ¬(u = v), from eq.symm Hvf ▸ eq.symm Hut ▸ true_ne_false,
|
||||
or.inl Hne)
|
||||
(assume Hp : p, or.inr Hp))
|
||||
(assume Hp : p, or.inr Hp)
|
||||
(assume hvf : v = false,
|
||||
have hne : ¬(u = v), from eq.symm hvf ▸ eq.symm hut ▸ true_ne_false,
|
||||
or.inl hne)
|
||||
(assume hp : p, or.inr hp))
|
||||
(assume hp : p, or.inr hp)
|
||||
|
||||
private lemma p_implies_uv : p → u = v :=
|
||||
assume Hp : p,
|
||||
have Hpred : U = V, from
|
||||
assume hp : p,
|
||||
have hpred : U = V, from
|
||||
funext (take x : Prop,
|
||||
have Hl : (x = true ∨ p) → (x = false ∨ p), from
|
||||
assume A, or.inr Hp,
|
||||
have Hr : (x = false ∨ p) → (x = true ∨ p), from
|
||||
assume A, or.inr Hp,
|
||||
have hl : (x = true ∨ p) → (x = false ∨ p), from
|
||||
assume A, or.inr hp,
|
||||
have hr : (x = false ∨ p) → (x = true ∨ p), from
|
||||
assume A, or.inr hp,
|
||||
show (x = true ∨ p) = (x = false ∨ p), from
|
||||
propext (iff.intro Hl Hr)),
|
||||
have H' : epsilon U = epsilon V, from Hpred ▸ rfl,
|
||||
show u = v, from H'
|
||||
propext (iff.intro hl hr)),
|
||||
have h' : epsilon U = epsilon V, from hpred ▸ rfl,
|
||||
show u = v, from h'
|
||||
|
||||
theorem em : p ∨ ¬p :=
|
||||
have H : ¬(u = v) → ¬p, from mt p_implies_uv,
|
||||
have h : ¬(u = v) → ¬p, from mt p_implies_uv,
|
||||
or.elim not_uv_or_p
|
||||
(assume Hne : ¬(u = v), or.inr (H Hne))
|
||||
(assume Hp : p, or.inl Hp)
|
||||
(assume hne : ¬(u = v), or.inr (h hne))
|
||||
(assume hp : p, or.inl hp)
|
||||
end diaconescu
|
||||
|
||||
theorem prop_complete (a : Prop) : a = true ∨ a = false :=
|
||||
|
|
@ -119,23 +119,23 @@ definition eq_true_or_eq_false := prop_complete
|
|||
|
||||
section aux
|
||||
attribute [elab_as_eliminator]
|
||||
theorem cases_true_false (P : Prop → Prop) (H1 : P true) (H2 : P false) (a : Prop) : P a :=
|
||||
theorem cases_true_false (p : Prop → Prop) (h1 : p true) (h2 : p false) (a : Prop) : p a :=
|
||||
or.elim (prop_complete a)
|
||||
(assume Ht : a = true, eq.symm Ht ▸ H1)
|
||||
(assume Hf : a = false, eq.symm Hf ▸ H2)
|
||||
(assume ht : a = true, eq.symm ht ▸ h1)
|
||||
(assume hf : a = false, eq.symm hf ▸ h2)
|
||||
|
||||
theorem cases_on (a : Prop) {P : Prop → Prop} (H1 : P true) (H2 : P false) : P a :=
|
||||
cases_true_false P H1 H2 a
|
||||
theorem cases_on (a : Prop) {p : Prop → Prop} (h1 : p true) (h2 : p false) : p a :=
|
||||
cases_true_false p h1 h2 a
|
||||
|
||||
-- this supercedes by_cases in decidable
|
||||
definition by_cases {p q : Prop} (Hpq : p → q) (Hnpq : ¬p → q) : q :=
|
||||
or.elim (em p) (assume Hp, Hpq Hp) (assume Hnp, Hnpq Hnp)
|
||||
definition by_cases {p q : Prop} (hpq : p → q) (hnpq : ¬p → q) : q :=
|
||||
or.elim (em p) (assume hp, hpq hp) (assume hnp, hnpq hnp)
|
||||
|
||||
-- this supercedes by_contradiction in decidable
|
||||
theorem by_contradiction {p : Prop} (H : ¬p → false) : p :=
|
||||
theorem by_contradiction {p : Prop} (h : ¬p → false) : p :=
|
||||
by_cases
|
||||
(assume H1 : p, H1)
|
||||
(assume H1 : ¬p, false.rec _ (H H1))
|
||||
(assume h1 : p, h1)
|
||||
(assume h1 : ¬p, false.rec _ (h h1))
|
||||
|
||||
theorem eq_false_or_eq_true (a : Prop) : a = false ∨ a = true :=
|
||||
cases_true_false (λ x, x = false ∨ x = true)
|
||||
|
|
@ -143,13 +143,13 @@ cases_true_false (λ x, x = false ∨ x = true)
|
|||
(or.inl rfl)
|
||||
a
|
||||
|
||||
theorem eq.of_iff {a b : Prop} (H : a ↔ b) : a = b :=
|
||||
iff.elim (assume H1 H2, propext (iff.intro H1 H2)) H
|
||||
theorem eq.of_iff {a b : Prop} (h : a ↔ b) : a = b :=
|
||||
iff.elim (assume h1 h2, propext (iff.intro h1 h2)) h
|
||||
|
||||
theorem iff_eq_eq {a b : Prop} : (a ↔ b) = (a = b) :=
|
||||
propext (iff.intro
|
||||
(assume H, eq.of_iff H)
|
||||
(assume H, iff.of_eq H))
|
||||
(assume h, eq.of_iff h)
|
||||
(assume h, iff.of_eq h))
|
||||
|
||||
lemma eq_false {a : Prop} : (a = false) = (¬ a) :=
|
||||
have (a ↔ false) = (¬ a), from propext (iff_false a),
|
||||
|
|
@ -164,8 +164,8 @@ end aux
|
|||
noncomputable definition decidable_inhabited (a : Prop) : inhabited (decidable a) :=
|
||||
inhabited_of_nonempty
|
||||
(or.elim (em a)
|
||||
(assume Ha, ⟨is_true Ha⟩)
|
||||
(assume Hna, ⟨is_false Hna⟩))
|
||||
(assume ha, ⟨is_true ha⟩)
|
||||
(assume hna, ⟨is_false hna⟩))
|
||||
local attribute decidable_inhabited [instance]
|
||||
|
||||
noncomputable definition prop_decidable (a : Prop) : decidable a :=
|
||||
|
|
@ -177,8 +177,8 @@ noncomputable definition type_decidable_eq (A : Type u) : decidable_eq A :=
|
|||
|
||||
noncomputable definition type_decidable (A : Type u) : sum A (A → false) :=
|
||||
match (prop_decidable (nonempty A)) with
|
||||
| (is_true Hp) := sum.inl (inhabited.value (inhabited_of_nonempty Hp))
|
||||
| (is_false Hn) := sum.inr (λ a, absurd (nonempty.intro a) Hn)
|
||||
| (is_true hp) := sum.inl (inhabited.value (inhabited_of_nonempty hp))
|
||||
| (is_false hn) := sum.inr (λ a, absurd (nonempty.intro a) hn)
|
||||
end
|
||||
|
||||
end classical
|
||||
|
|
|
|||
|
|
@ -125,7 +125,7 @@ definition coe_decidable_eq (b : bool) : decidable (coe b) :=
|
|||
show decidable (b = tt), from bool.has_decidable_eq b tt
|
||||
|
||||
attribute [instance]
|
||||
definition coe_subtype {A : Type u} {P : A → Prop} : has_coe {a \ P a} A :=
|
||||
definition coe_subtype {A : Type u} {p : A → Prop} : has_coe {a // p a} A :=
|
||||
⟨λ s, subtype.elt_of s⟩
|
||||
|
||||
/- Basic lifts -/
|
||||
|
|
|
|||
|
|
@ -9,7 +9,7 @@ open tactic subtype
|
|||
universe variables u v
|
||||
|
||||
attribute [instance]
|
||||
definition subtype_decidable_eq {A : Type u} {P : A → Prop} [decidable_eq A] : decidable_eq {x \ P x} :=
|
||||
definition subtype_decidable_eq {A : Type u} {p : A → Prop} [decidable_eq A] : decidable_eq {x : A // p x} :=
|
||||
by mk_dec_eq_instance
|
||||
|
||||
set_option trace.app_builder true
|
||||
|
|
|
|||
|
|
@ -14,7 +14,7 @@ tag :: (elt_of : A) (has_property : p elt_of)
|
|||
|
||||
namespace subtype
|
||||
|
||||
definition exists_of_subtype {A : Type u} {p : A → Prop} : { x \ p x } → ∃ x, p x
|
||||
definition exists_of_subtype {A : Type u} {p : A → Prop} : { x // p x } → ∃ x, p x
|
||||
| ⟨a, h⟩ := ⟨a, h⟩
|
||||
|
||||
variables {A : Type u} {p : A → Prop}
|
||||
|
|
@ -22,7 +22,7 @@ namespace subtype
|
|||
theorem tag_irrelevant {a : A} (h1 h2 : p a) : tag a h1 = tag a h2 :=
|
||||
rfl
|
||||
|
||||
protected theorem eq : ∀ {a1 a2 : {x \ p x}}, elt_of a1 = elt_of a2 → a1 = a2
|
||||
protected theorem eq : ∀ {a1 a2 : {x // p x}}, elt_of a1 = elt_of a2 → a1 = a2
|
||||
| ⟨x, h1⟩ ⟨.x, h2⟩ rfl := rfl
|
||||
|
||||
end subtype
|
||||
|
|
@ -32,5 +32,5 @@ open subtype
|
|||
variables {A : Type u} {p : A → Prop}
|
||||
|
||||
attribute [instance]
|
||||
protected definition subtype.is_inhabited {a : A} (h : p a) : inhabited {x \ p x} :=
|
||||
protected definition subtype.is_inhabited {a : A} (h : p a) : inhabited {x // p x} :=
|
||||
⟨⟨a, h⟩⟩
|
||||
|
|
|
|||
|
|
@ -12,7 +12,7 @@ Author: Leonardo de Moura
|
|||
#include "frontends/lean/tokens.h"
|
||||
|
||||
namespace lean {
|
||||
/* Parse rest of the subtype expression prefix '{' id ':' expr '\' ... */
|
||||
/* Parse rest of the subtype expression prefix '{' id ':' expr '\\' ... */
|
||||
static expr parse_subtype(parser & p, pos_info const & pos, expr const & local) {
|
||||
parser::local_scope scope(p);
|
||||
p.add_local(local);
|
||||
|
|
@ -90,7 +90,7 @@ expr parse_curly_bracket(parser & p, unsigned, expr const *, pos_info const & po
|
|||
auto id_pos = p.pos();
|
||||
name id = p.get_name_val();
|
||||
p.next();
|
||||
if (p.curr_is_token(get_backslash_tk())) {
|
||||
if (p.curr_is_token(get_dslash_tk())) {
|
||||
expr type = p.save_pos(mk_expr_placeholder(), id_pos);
|
||||
expr local = p.save_pos(mk_local(id, type), id_pos);
|
||||
p.next();
|
||||
|
|
@ -99,7 +99,7 @@ expr parse_curly_bracket(parser & p, unsigned, expr const *, pos_info const & po
|
|||
p.next();
|
||||
expr type = p.parse_expr();
|
||||
expr local = p.save_pos(mk_local(id, type), id_pos);
|
||||
p.check_token_next(get_backslash_tk(), "invalid subtype, '\' expected");
|
||||
p.check_token_next(get_dslash_tk(), "invalid subtype, '//' expected");
|
||||
return parse_subtype(p, pos, local);
|
||||
} else if (p.curr_is_token(get_period_tk())) {
|
||||
p.next();
|
||||
|
|
@ -132,7 +132,7 @@ expr parse_curly_bracket(parser & p, unsigned, expr const *, pos_info const & po
|
|||
p.next();
|
||||
return parse_monadic_comprehension(p, pos, e);
|
||||
} else {
|
||||
throw parser_error("invalid '{' expression, ',', '}', 'with', `\\` or `|` expected", p.pos());
|
||||
throw parser_error("invalid '{' expression, ',', '}', 'with', `//` or `|` expected", p.pos());
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -1470,7 +1470,7 @@ auto pretty_fn::pp_subtype(expr const & e) -> result {
|
|||
auto p = binding_body_fresh(pred, true);
|
||||
expr body = p.first;
|
||||
expr local = p.second;
|
||||
format r = bracket("{", format(local_pp_name(local)) + space() + format("\\") + space() + pp_child(body, 0).fmt(), "}");
|
||||
format r = bracket("{", format(local_pp_name(local)) + space() + format("//") + space() + pp_child(body, 0).fmt(), "}");
|
||||
return result(r);
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -87,7 +87,7 @@ void init_token_table(token_table & t) {
|
|||
{"[", 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},
|
||||
{"⊢", 0}, {"⟨", g_max_prec}, {"⟩", 0}, {"^", 0}, {"↑", 0}, {"▸", 0},
|
||||
{"\\", 0}, {"|", 0}, {"!", g_max_prec}, {"?", 0}, {"with", 0}, {"...", 0}, {",", 0},
|
||||
{"//", 0}, {"|", 0}, {"!", g_max_prec}, {"?", 0}, {"with", 0}, {"...", 0}, {",", 0},
|
||||
{".", 0}, {":", 0}, {"::", 0}, {"calc", 0}, {"as", 0}, {":=", 0}, {"--", 0}, {"#", 0},
|
||||
{"(*", 0}, {"/-", 0}, {"begin", g_max_prec}, {"abstract", g_max_prec},
|
||||
{"@@", g_max_prec}, {"@", g_max_prec},
|
||||
|
|
|
|||
|
|
@ -6,7 +6,7 @@ namespace lean{
|
|||
static name const * g_aliases_tk = nullptr;
|
||||
static name const * g_period_tk = nullptr;
|
||||
static name const * g_backtick_tk = nullptr;
|
||||
static name const * g_backslash_tk = nullptr;
|
||||
static name const * g_dslash_tk = nullptr;
|
||||
static name const * g_fieldarrow_tk = nullptr;
|
||||
static name const * g_placeholder_tk = nullptr;
|
||||
static name const * g_colon_tk = nullptr;
|
||||
|
|
@ -127,7 +127,7 @@ void initialize_tokens() {
|
|||
g_aliases_tk = new name{"aliases"};
|
||||
g_period_tk = new name{"."};
|
||||
g_backtick_tk = new name{"`"};
|
||||
g_backslash_tk = new name{"\\"};
|
||||
g_dslash_tk = new name{"//"};
|
||||
g_fieldarrow_tk = new name{"~>"};
|
||||
g_placeholder_tk = new name{"_"};
|
||||
g_colon_tk = new name{":"};
|
||||
|
|
@ -249,7 +249,7 @@ void finalize_tokens() {
|
|||
delete g_aliases_tk;
|
||||
delete g_period_tk;
|
||||
delete g_backtick_tk;
|
||||
delete g_backslash_tk;
|
||||
delete g_dslash_tk;
|
||||
delete g_fieldarrow_tk;
|
||||
delete g_placeholder_tk;
|
||||
delete g_colon_tk;
|
||||
|
|
@ -370,7 +370,7 @@ void finalize_tokens() {
|
|||
name const & get_aliases_tk() { return *g_aliases_tk; }
|
||||
name const & get_period_tk() { return *g_period_tk; }
|
||||
name const & get_backtick_tk() { return *g_backtick_tk; }
|
||||
name const & get_backslash_tk() { return *g_backslash_tk; }
|
||||
name const & get_dslash_tk() { return *g_dslash_tk; }
|
||||
name const & get_fieldarrow_tk() { return *g_fieldarrow_tk; }
|
||||
name const & get_placeholder_tk() { return *g_placeholder_tk; }
|
||||
name const & get_colon_tk() { return *g_colon_tk; }
|
||||
|
|
|
|||
|
|
@ -8,7 +8,7 @@ void finalize_tokens();
|
|||
name const & get_aliases_tk();
|
||||
name const & get_period_tk();
|
||||
name const & get_backtick_tk();
|
||||
name const & get_backslash_tk();
|
||||
name const & get_dslash_tk();
|
||||
name const & get_fieldarrow_tk();
|
||||
name const & get_placeholder_tk();
|
||||
name const & get_colon_tk();
|
||||
|
|
|
|||
|
|
@ -1,7 +1,7 @@
|
|||
aliases aliases
|
||||
period .
|
||||
backtick `
|
||||
backslash \\
|
||||
dslash //
|
||||
fieldarrow ~>
|
||||
placeholder _
|
||||
colon :
|
||||
|
|
|
|||
|
|
@ -15,3 +15,12 @@ check { a ∈ s1 | a > 1 }
|
|||
check { a in s1 | a > 1 }
|
||||
set_option pp.unicode false
|
||||
check { a ∈ s1 | a > 2 }
|
||||
|
||||
|
||||
definition a := 10
|
||||
|
||||
check ({a, a} : set nat)
|
||||
check ({a, 1, a} : set nat)
|
||||
check ({a} : set nat)
|
||||
|
||||
check { a // a > 0 }
|
||||
|
|
|
|||
|
|
@ -10,3 +10,7 @@ definition s3 : set string :=
|
|||
{a ∈ s1 | a > 1} : set ℕ
|
||||
{a ∈ s1 | a > 1} : set ℕ
|
||||
{a in s1 | a > 2} : set nat
|
||||
{a, a} : set nat
|
||||
{a, 1, a} : set nat
|
||||
{a} : set nat
|
||||
{a // a > 0} : Type
|
||||
|
|
|
|||
|
|
@ -1,3 +1,3 @@
|
|||
quot.sound : ∀ {A : Type u} [s : setoid A] {a b : A}, a ≈ b → ⟦a⟧ = ⟦b⟧
|
||||
classical.strong_indefinite_description : Π {A : Type u} (P : A → Prop), nonempty A → {x \ Exists P → P x}
|
||||
classical.strong_indefinite_description : Π {A : Type u} (p : A → Prop), nonempty A → {x // Exists p → p x}
|
||||
propext : ∀ {a b : Prop}, (a ↔ b) → a = b
|
||||
|
|
|
|||
|
|
@ -1,3 +1,3 @@
|
|||
quot.sound : ∀ {A : Type u} [s : setoid A] {a b : A}, a ≈ b → ⟦a⟧ = ⟦b⟧
|
||||
classical.strong_indefinite_description : Π {A : Type u} (P : A → Prop), nonempty A → {x \ Exists P → P x}
|
||||
classical.strong_indefinite_description : Π {A : Type u} (p : A → Prop), nonempty A → {x // Exists p → p x}
|
||||
propext : ∀ {a b : Prop}, (a ↔ b) → a = b
|
||||
|
|
|
|||
|
|
@ -1,7 +1,7 @@
|
|||
no axioms
|
||||
------
|
||||
quot.sound : ∀ {A : Type u} [s : setoid A] {a b : A}, a ≈ b → ⟦a⟧ = ⟦b⟧
|
||||
classical.strong_indefinite_description : Π {A : Type u} (P : A → Prop), nonempty A → {x \ Exists P → P x}
|
||||
classical.strong_indefinite_description : Π {A : Type u} (p : A → Prop), nonempty A → {x // Exists p → p x}
|
||||
propext : ∀ {a b : Prop}, (a ↔ b) → a = b
|
||||
------
|
||||
theorem foo3 : 0 = 0 :=
|
||||
|
|
|
|||
|
|
@ -1,9 +1,5 @@
|
|||
definition set (A : Type) := A → Prop
|
||||
definition mem {A : Type} (a : A) (s : set A) : Prop :=
|
||||
s a
|
||||
definition range (lower : nat) (upper : nat) : set nat :=
|
||||
λ a, lower ≤ a ∧ a ≤ upper
|
||||
infix ` ∈ ` := mem
|
||||
|
||||
local notation `[` L `, ` U `]` := range L U
|
||||
|
||||
|
|
|
|||
|
|
@ -2,6 +2,6 @@ inductive imf (f : nat → nat) : nat → Type
|
|||
| mk1 : ∀ (a : nat), imf (f a)
|
||||
| mk2 : imf (f 0 + 1)
|
||||
|
||||
definition inv_2 (f : nat → nat) : ∀ (b : nat), imf f b → {x : nat \ x > b} →nat
|
||||
definition inv_2 (f : nat → nat) : ∀ (b : nat), imf f b → {x : nat // x > b} → nat
|
||||
| .(f a) (imf.mk1 .f a) x := a
|
||||
| .(f 0 + 1) (imf.mk2 .f) x := subtype.elt_of x
|
||||
|
|
|
|||
|
|
@ -1,7 +0,0 @@
|
|||
open bool nat
|
||||
|
||||
definition set (T : Type) := T → bool
|
||||
definition mem {A : Type} (x : A) (s : set A) := s x
|
||||
infix ` ∈ ` := mem
|
||||
|
||||
check 1 ∈ (λ x : nat, tt)
|
||||
|
|
@ -1,19 +0,0 @@
|
|||
open bool
|
||||
|
||||
namespace set
|
||||
|
||||
definition set (T : Type) := T → bool
|
||||
definition mem {T : Type} (a : T) (s : set T) := s a = tt
|
||||
infix `∈` := mem
|
||||
|
||||
section
|
||||
variable {T : Type}
|
||||
|
||||
definition empty : set T := λx, ff
|
||||
notation `∅` := empty
|
||||
|
||||
theorem mem_empty (x : T) : ¬ (x ∈ ∅)
|
||||
:= not.intro (λH : x ∈ ∅, absurd H ff_ne_tt)
|
||||
end
|
||||
|
||||
end set
|
||||
|
|
@ -1,3 +1,2 @@
|
|||
notation `{` binders:55 ` \ ` r:(scoped P, subtype P) `}` := r
|
||||
check { x : nat \ x > 0 }
|
||||
check { (x : nat → nat) \ true }
|
||||
check { x : nat // x > 0 }
|
||||
check { x : nat → nat // true }
|
||||
|
|
|
|||
|
|
@ -1,2 +1,2 @@
|
|||
open nat subtype
|
||||
check { x : nat \ x > 0}
|
||||
check { x : nat // x > 0}
|
||||
|
|
|
|||
|
|
@ -1,6 +1,7 @@
|
|||
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)
|
||||
|
|
@ -29,15 +30,18 @@ has_to_string : Type u → Type (max 1 u)
|
|||
has_to_tactic_format : Type → Type
|
||||
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)
|
||||
is_associative : Π {A : Type u}, (A → A → A) → Type
|
||||
monad : (Type u → Type v) → Type (max (u+1) v)
|
||||
nonempty : Type u → Prop
|
||||
point : Type u_1 → Type u_2 → Type (max 1 u_1 u_2)
|
||||
separable : Type u → (Type u → Type v) → Type (max 1 (imax (max 1 u) v))
|
||||
setoid : Type u → Type (max 1 u)
|
||||
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)
|
||||
|
|
@ -66,9 +70,11 @@ has_to_string : Type u → Type (max 1 u)
|
|||
has_to_tactic_format : Type → Type
|
||||
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)
|
||||
is_associative : Π {A : Type u}, (A → A → A) → Type
|
||||
monad : (Type u → Type v) → Type (max (u+1) v)
|
||||
nonempty : Type u → Prop
|
||||
point : Type u_1 → Type u_2 → Type (max 1 u_1 u_2)
|
||||
separable : Type u → (Type u → Type v) → Type (max 1 (imax (max 1 u) v))
|
||||
setoid : Type u → Type (max 1 u)
|
||||
subsingleton : Type u → Prop
|
||||
|
|
|
|||
|
|
@ -1,4 +1,2 @@
|
|||
--
|
||||
open nat subtype
|
||||
|
||||
check {x : nat \ x > 0 }
|
||||
check {x : nat // x > 0 }
|
||||
|
|
|
|||
|
|
@ -1 +1 @@
|
|||
{x \ x > 0} : Type
|
||||
{x // x > 0} : Type
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue