fix(frontends/lean/builtin_exprs): fixes #768

This commit is contained in:
Leonardo de Moura 2015-08-08 04:20:17 -07:00
parent d46dbce86e
commit 06f20694c8
5 changed files with 33 additions and 7 deletions

View file

@ -29,7 +29,7 @@ definition to_set.inj {s₁ s₂ : finset A} : to_set s₁ = to_set s₂ → s
/- operations -/
theorem mem_to_set_empty : (x ∈ ts ∅) = (x ∈ ∅) := rfl
theorem to_set_empty : ts ∅ = (∅ : set A) := rfl
theorem to_set_empty : ts ∅ = (@set.empty A) := rfl
theorem mem_to_set_univ [h : fintype A] : (x ∈ ts univ) = (x ∈ set.univ) :=
propext (iff.intro (assume H, trivial) (assume H, !mem_univ))

View file

@ -138,7 +138,7 @@ assert hom g a = hom h a, from of_mem_filter Pg, calc
hom (h⁻¹*g) a = perm.f ((hom h⁻¹) * (hom g)) a : by rewrite (is_hom hom)
... = ((hom h⁻¹) ∘ hom g) a : by rewrite perm_f_mul
... = perm.f ((hom h)⁻¹ * hom h) a : by unfold compose; rewrite [this, perm_f_mul, hom_map_inv hom h]
... = (1 : perm S) a : by rewrite (mul.left_inv (hom h))
... = perm.f (1 : perm S) a : by rewrite (mul.left_inv (hom h))
... = a : by esimp
lemma moverset_inj_on_orbit : set.inj_on (moverset hom H a) (ts (orbit hom H a)) :=
@ -177,8 +177,8 @@ lemma subg_stab_closed : finset_mul_closed_on (stab hom H a) :=
lemma subg_stab_has_one : 1 ∈ stab hom H a :=
assert P : hom 1 a = a, from calc
hom 1 a = (1 : perm S) a : {hom_map_one hom}
... = a : rfl,
hom 1 a = perm.f (1 : perm S) a : {hom_map_one hom}
... = a : rfl,
assert PoneinH : 1 ∈ H, from finsubg_has_one H,
mem_filter_of_mem PoneinH P
@ -189,7 +189,7 @@ lemma subg_stab_has_inv : finset_has_inv (stab hom H a) :=
... = perm.f ((hom f⁻¹) * (hom f)) a : by rewrite perm_f_mul
... = hom (f⁻¹ * f) a : by rewrite (is_hom hom)
... = hom 1 a : by rewrite mul.left_inv
... = (1 : perm S) a : by rewrite (hom_map_one hom),
... = perm.f (1 : perm S) a : by rewrite (hom_map_one hom),
assert PfinvinH : f⁻¹ ∈ H, from finsubg_has_inv H (mem_of_mem_filter Pfstab),
mem_filter_of_mem PfinvinH Pfinv

View file

@ -72,6 +72,20 @@ static void parse_let_modifiers(parser & p, bool & is_visible) {
}
}
// Distribute mk_typed_expr over choice expression.
// see issue #768
static expr mk_typed_expr_distrib_choice(parser & p, expr const & type, expr const & value, pos_info const & pos) {
if (is_choice(value)) {
buffer<expr> new_choices;
for (unsigned i = 0; i < get_num_choices(value); i++) {
new_choices.push_back(mk_typed_expr_distrib_choice(p, type, get_choice(value, i), pos));
}
return p.save_pos(mk_choice(new_choices.size(), new_choices.data()), pos);
} else {
return p.save_pos(mk_typed_expr(type, value), pos);
}
}
static expr parse_let(parser & p, pos_info const & pos) {
parser::local_scope scope1(p);
if (p.parse_local_notation_decl()) {
@ -107,7 +121,7 @@ static expr parse_let(parser & p, pos_info const & pos) {
}
expr v;
if (type)
v = p.save_pos(mk_typed_expr(*type, value), p.pos_of(value));
v = mk_typed_expr_distrib_choice(p, *type, value, p.pos_of(value));
else
v = value;
v = p.save_pos(mk_let_value(v), id_pos);
@ -668,7 +682,7 @@ static expr parse_inaccessible(parser & p, unsigned, expr const * args, pos_info
}
static expr parse_typed_expr(parser & p, unsigned, expr const * args, pos_info const & pos) {
return p.save_pos(mk_typed_expr(args[1], args[0]), pos);
return mk_typed_expr_distrib_choice(p, args[1], args[0], pos);
}
parse_table init_nud_table() {

11
tests/lean/768.lean Normal file
View file

@ -0,0 +1,11 @@
import data.set data.finset
open set finset
variables (A : Type) [deceqA : decidable_eq A]
include deceqA
variables s t : finset A
set_option pp.coercions true
set_option pp.notation false
set_option pp.full_names true
check (s t : set A)

View file

@ -0,0 +1 @@
finset.ts (finset.union s t) : set A