From 06f20694c8dc54e2a3614716533e7b0e8c27d01a Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 8 Aug 2015 04:20:17 -0700
Subject: [PATCH] fix(frontends/lean/builtin_exprs): fixes #768

---
 library/data/finset/to_set.lean           |  2 +-
 library/theories/group_theory/action.lean |  8 ++++----
 src/frontends/lean/builtin_exprs.cpp      | 18 ++++++++++++++++--
 tests/lean/768.lean                       | 11 +++++++++++
 tests/lean/768.lean.expected.out          |  1 +
 5 files changed, 33 insertions(+), 7 deletions(-)
 create mode 100644 tests/lean/768.lean
 create mode 100644 tests/lean/768.lean.expected.out

diff --git a/library/data/finset/to_set.lean b/library/data/finset/to_set.lean
index 4b5edb4c0..626ea3d82 100644
--- a/library/data/finset/to_set.lean
+++ b/library/data/finset/to_set.lean
@@ -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))
diff --git a/library/theories/group_theory/action.lean b/library/theories/group_theory/action.lean
index 2a832e383..a07b43760 100644
--- a/library/theories/group_theory/action.lean
+++ b/library/theories/group_theory/action.lean
@@ -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
 
diff --git a/src/frontends/lean/builtin_exprs.cpp b/src/frontends/lean/builtin_exprs.cpp
index ca57a60b2..09a38eecd 100644
--- a/src/frontends/lean/builtin_exprs.cpp
+++ b/src/frontends/lean/builtin_exprs.cpp
@@ -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() {
diff --git a/tests/lean/768.lean b/tests/lean/768.lean
new file mode 100644
index 000000000..dcea7d200
--- /dev/null
+++ b/tests/lean/768.lean
@@ -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)
diff --git a/tests/lean/768.lean.expected.out b/tests/lean/768.lean.expected.out
new file mode 100644
index 000000000..32f8f67a6
--- /dev/null
+++ b/tests/lean/768.lean.expected.out
@@ -0,0 +1 @@
+finset.ts (finset.union s t) : set A