feat(frontends/lean): apply eta-reduction in postprocessing step

Perhaps, we should add an option to disable this new feature.

Remark: this commit makes commit 46d418a redundant.
I'm keeping 46d418a because we may retract this commit in the future.

hott/algebra/category/constructions/hset.hlean

@@ -72,16 +72,20 @@ namespace category
     ua !equiv_equiv_iso
 
     definition is_univalent_hset (A B : Precategory_hset) : is_equiv (iso_of_eq : A = B → A ≅ B) :=
-    have H : is_equiv (@iso_of_equiv A B ∘ @equiv_of_eq A B ∘ subtype_eq_inv _ _ ∘
+    assert H₁ : is_equiv (@iso_of_equiv A B ∘ @equiv_of_eq A B ∘ subtype_eq_inv _ _ ∘
-      @ap _ _ (to_fun (trunctype.sigma_char 0)) A B), from
+                  @ap _ _ (to_fun (trunctype.sigma_char 0)) A B), from
-    @is_equiv_compose _ _ _ _ _
+      @is_equiv_compose _ _ _ _ _
       (@is_equiv_compose _ _ _ _ _
-        (@is_equiv_compose _ _ _ _ _
+         (@is_equiv_compose _ _ _ _ _
-          _
+           _
-          (@is_equiv_subtype_eq_inv _ _ _ _ _))
+           (@is_equiv_subtype_eq_inv _ _ _ _ _))
-        !univalence)
+         !univalence)
-      !is_equiv_iso_of_equiv,
+       !is_equiv_iso_of_equiv,
-    (iso_of_eq_eq_compose A B)⁻¹ ▸ H
+    assert H₂ : _, from (iso_of_eq_eq_compose A B)⁻¹,
+    begin
+      rewrite H₂ at H₁,
+      assumption
+    end
   end set
 
   definition category_hset [instance] : category hset :=

hott/hit/circle.hlean

@@ -213,7 +213,7 @@ namespace circle
       { exact idp},
       { intros n p,
         apply transport (λ(y : base = base), transport circle.code y _ = _), apply power_con,
-        rewrite [▸*,con_tr, transport_code_loop, ↑[circle.encode,circle.code] at p, p]},
+        rewrite [▸*,con_tr, transport_code_loop, ↑[circle.encode,circle.code] at p], krewrite p},
       { intros n p,
         apply transport (λ(y : base = base), transport circle.code y _ = _),
         { exact !power_con_inv ⬝ ap (power loop) !neg_succ⁻¹},

src/frontends/lean/util.cpp

@@ -15,6 +15,7 @@ Author: Leonardo de Moura
 #include "library/locals.h"
 #include "library/explicit.h"
 #include "library/aliases.h"
+#include "library/normalize.h"
 #include "library/placeholder.h"
 #include "library/abbreviation.h"
 #include "library/unfold_macros.h"
@@ -450,6 +451,6 @@ char const * close_binder_string(binder_info const & bi, bool unicode) {
 }
 
 expr postprocess(environment const & env, expr const & e) {
-    return expand_abbreviations(env, unfold_untrusted_macros(env, e));
+    return eta_reduce(expand_abbreviations(env, unfold_untrusted_macros(env, e)));
 }
 }

src/library/normalize.cpp

@@ -220,6 +220,10 @@ expr beta_reduce(expr t) {
     return eta_beta_reduce_fn<false, true>()(t);
 }
 
+expr eta_reduce(expr t) {
+    return eta_beta_reduce_fn<true, false>()(t);
+}
+
 expr beta_eta_reduce(expr t) {
     return eta_beta_reduce_fn<true, true>()(t);
 }

src/library/normalize.h

@@ -62,6 +62,7 @@ optional<unsigned> has_constructor_hint(environment const & env, name const & d)
 
 expr try_eta(expr const & e);
 expr beta_reduce(expr t);
+expr eta_reduce(expr t);
 expr beta_eta_reduce(expr t);
 
 void initialize_normalize();

tests/lean/550.lean.expected.out

@@ -37,4 +37,4 @@ rinv : func ∘ finv = function.id
 550.lean:43:2: error: failed to add declaration 'bijection.inv.linv' to environment, value has metavariables
 remark: set 'formatter.hide_full_terms' to false to see the complete term
   λ (A : Type) (f : …),
-    bijection.rec_on f (λ (func finv : …) (linv : …) (rinv : …), ?M_1)
+    bijection.rec_on f ?M_1

tests/lean/571.lean.expected.out

@@ -9,5 +9,4 @@ H : ∃ (n : ℕ), P n
 ⊢ ℕ
 571.lean:7:0: error: failed to add declaration 'example' to environment, value has metavariables
 remark: set 'formatter.hide_full_terms' to false to see the complete term
-  λ (P : …) (H : …),
+  ?M_1
-    ?M_1

tests/lean/583.lean.expected.out

@@ -11,5 +11,4 @@ P : f a⁻¹ * f a = 1
 583.lean:27:8: error: failed to add declaration 'group_hom.hom_map_inv' to environment, value has metavariables
 remark: set 'formatter.hide_full_terms' to false to see the complete term
   λ (A : Type) (B : Type) (s1 : …) (s2 : …) (f : …) (Hom : …) (a : A),
-    assert P : …, from …,
+    ?M_1 …
-    ?M_1

tests/lean/608.hlean.expected.out

@@ -1,9 +1,9 @@
 definition category.id [reducible] : Π {ob : Type} [C : precategory ob] {a : ob}, hom a a
-λ (ob : Type) (C : precategory ob) (a : ob), ID a
+ID
 definition function.id [reducible] : Π {A : Type}, A → A
 λ (A : Type) (a : A), a
 -----------
 definition category.id [reducible] : Π {ob : Type} [C : precategory ob] {a : ob}, hom a a
-λ (ob : Type) (C : precategory ob) (a : ob), ID a
+ID
 definition function.id [reducible] : Π {A : Type}, A → A
 λ (A : Type) (a : A), a

tests/lean/abbrev_paren.hlean.expected.out

@@ -3,5 +3,4 @@ C : Precategory
 ⊢ C = Precategory.mk (carrier C) C
 abbrev_paren.hlean:5:54: error: failed to add declaration 'example' to environment, value has metavariables
 remark: set 'formatter.hide_full_terms' to false to see the complete term
-  λ (C : Precategory),
+  ?M_1
-    ?M_1

tests/lean/apply_fail.lean.expected.out

@@ -10,5 +10,4 @@ a b : Prop
 ⊢ a ∧ b
 apply_fail.lean:4:0: error: failed to add declaration 'example' to environment, value has metavariables
 remark: set 'formatter.hide_full_terms' to false to see the complete term
-  λ (a b : Prop),
+  ?M_1
-    ?M_1

tests/lean/assert_fail.lean.expected.out

@@ -9,8 +9,7 @@ H : b ∧ a
 ⊢ a ∧ b
 assert_fail.lean:4:0: error: failed to add declaration 'example' to environment, value has metavariables
 remark: set 'formatter.hide_full_terms' to false to see the complete term
-  λ (a b : Prop) (H : …),
+  ?M_1
-    ?M_1
 assert_fail.lean:9:2: error:invalid tactic, there are no goals to be solved
 proof state:
 no goals
@@ -20,5 +19,4 @@ Ha : a
 ⊢ a
 assert_fail.lean:10:0: error: failed to add declaration 'example' to environment, value has metavariables
 remark: set 'formatter.hide_full_terms' to false to see the complete term
-  λ (a : Prop) (Ha : a),
+  ?M_1
-    ?M_1

tests/lean/beginend_bug.lean.expected.out

@@ -22,5 +22,4 @@ Hbc : b = c
 ⊢ a = c
 beginend_bug.lean:9:0: error: failed to add declaration 'foo' to environment, value has metavariables
 remark: set 'formatter.hide_full_terms' to false to see the complete term
-  λ (A : Type) (a b c : A) (Hab : …) (Hbc : …),
+  ?M_1
-    ?M_1

tests/lean/cases_failure.hlean.expected.out

@@ -30,5 +30,4 @@ s : square t b l r
 ⊢ unit
 cases_failure.hlean:13:0: error: failed to add declaration 'foo' to environment, value has metavariables
 remark: set 'formatter.hide_full_terms' to false to see the complete term
-  λ (A : Type) (x y z : A) (t : …) (b : …) (l : …) (r : …) (s : …),
+  ?M_1
-    ?M_1

tests/lean/check_expr.lean.expected.out

@@ -6,5 +6,4 @@ a b : A
 ⊢ list A
 check_expr.lean:8:0: error: failed to add declaration 'foo' to environment, value has metavariables
 remark: set 'formatter.hide_full_terms' to false to see the complete term
-  λ (A : Type) (l : …),
+  ?M_1
-    ?M_1

tests/lean/constr_tac_errors.lean.expected.out

@@ -19,8 +19,7 @@ a b : Prop
 ⊢ a → b → a ∧ b
 constr_tac_errors.lean:13:0: error: failed to add declaration 'example' to environment, value has metavariables
 remark: set 'formatter.hide_full_terms' to false to see the complete term
-  λ (a b : Prop),
+  ?M_1
-    ?M_1
 constr_tac_errors.lean:18:2: error:invalid 'constructor' tactic, goal is an inductive datatype, but it does not have 2 constructor(s)
 proof state:
 a b : Prop,
@@ -32,8 +31,7 @@ a b : Prop
 ⊢ a → b → a ∧ b
 constr_tac_errors.lean:19:0: error: failed to add declaration 'example' to environment, value has metavariables
 remark: set 'formatter.hide_full_terms' to false to see the complete term
-  λ (a b : Prop),
+  ?M_1
-    ?M_1
 constr_tac_errors.lean:31:2: error:invalid 'constructor' tactic, too many arguments have been provided
 proof state:
 a b : Prop,
@@ -45,8 +43,7 @@ a b : Prop
 ⊢ a → b → unit
 constr_tac_errors.lean:32:0: error: failed to add declaration 'example' to environment, value has metavariables
 remark: set 'formatter.hide_full_terms' to false to see the complete term
-  λ (a b : Prop),
+  ?M_1
-    ?M_1
 constr_tac_errors.lean:39:2: error:invalid 'constructor' tactic, goal is not an inductive datatype
 proof state:
 

tests/lean/crash.lean.expected.out

@@ -1,9 +1,9 @@
 crash.lean:8:12: error: type mismatch at application
-  have H' : ¬ P, from H,
+  have H' : ¬P, from H,
   ?M_1
 term
   H
 has type
   P
 but is expected to have type
-  ¬ P
+  ¬P

tests/lean/ctx.lean.expected.out

@@ -7,5 +7,4 @@ p1 p2 : A × B
 ⊢ nat
 ctx.lean:3:0: error: failed to add declaration 'foo' to environment, value has metavariables
 remark: set 'formatter.hide_full_terms' to false to see the complete term
-  λ (A B : Type) (a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 : nat) (b1 b2 b3 : bool) (h : …) (p1 p2 : …),
+  ?M_1
-    ?M_1

tests/lean/exact_partial.lean.expected.out

@@ -20,5 +20,4 @@ a b : Prop
 ⊢ a → b → a ∧ b
 exact_partial.lean:5:0: error: failed to add declaration 'example' to environment, value has metavariables
 remark: set 'formatter.hide_full_terms' to false to see the complete term
-  λ (a b : Prop),
+  ?M_1
-    ?M_1

tests/lean/exact_partial2.lean.expected.out

@@ -17,5 +17,4 @@ h₂ : b = c
 ⊢ a = c
 exact_partial2.lean:4:0: error: failed to add declaration 'example' to environment, value has metavariables
 remark: set 'formatter.hide_full_terms' to false to see the complete term
-  λ (a b c : nat) (h₁ : …) (h₂ : …),
+  ?M_1
-    ?M_1

tests/lean/finset_induction_bug.lean.expected.out

@@ -13,61 +13,49 @@ A : Type,
 h : decidable_eq A,
 P : finset A → Prop,
 H1 : P (@empty A),
-H2 : ∀ ⦃s : finset A⦄ {a : A}, not (@mem A a s) → P s → P (@insert A (λ (a b : A), h a b) a s),
+H2 : ∀ ⦃s : finset A⦄ {a : A}, not (@mem A a s) → P s → P (@insert A h a s),
 s : finset A,
 u : nodup_list A,
 l : list A,
 a : A,
 l' : list A,
-IH :
+IH : ∀ (x : @nodup A l'), P (@quot.mk (nodup_list A) (nodup_list_setoid A) (@subtype.tag (list A) (@nodup A) l' x)),
-  ∀ (x : @nodup A l'),
-    P (@quot.mk (nodup_list A) (nodup_list_setoid A) (@subtype.tag (list A) (λ (l : list A), @nodup A l) l' x)),
 nodup_al' : @nodup A (@cons A a l'),
 anl' : not (@list.mem A a l'),
 H3 : @eq (list A) (@list.insert A (λ (a b : A), h a b) a l') (@cons A a l'),
 nodup_l' : @nodup A l',
-P_l' :
+P_l' : P (@quot.mk (nodup_list A) (nodup_list_setoid A) (@subtype.tag (list A) (@nodup A) l' nodup_l')),
-  P (@quot.mk (nodup_list A) (nodup_list_setoid A) (@subtype.tag (list A) (λ (l : list A), @nodup A l) l' nodup_l')),
 H4 :
   P
     (@insert A (λ (a b : A), h a b) a
-       (@quot.mk (nodup_list A) (nodup_list_setoid A)
+       (@quot.mk (nodup_list A) (nodup_list_setoid A) (@subtype.tag (list A) (@nodup A) l' nodup_l')))
-          (@subtype.tag (list A) (λ (l : list A), @nodup A l) l' nodup_l')))
+⊢ P (@quot.mk (nodup_list A) (nodup_list_setoid A) (@subtype.tag (list A) (@nodup A) (@cons A a l') nodup_al'))
-⊢ P
-    (@quot.mk (nodup_list A) (nodup_list_setoid A)
-       (@subtype.tag (list A) (λ (l : list A), @nodup A l) (@cons A a l') nodup_al'))
 finset_induction_bug.lean:30:45: error: don't know how to synthesize placeholder
 A : Type,
 h : decidable_eq A,
 P : finset A → Prop,
 H1 : P (@empty A),
-H2 : ∀ ⦃s : finset A⦄ {a : A}, not (@mem A a s) → P s → P (@insert A (λ (a b : A), h a b) a s),
+H2 : ∀ ⦃s : finset A⦄ {a : A}, not (@mem A a s) → P s → P (@insert A h a s),
 s : finset A,
 u : nodup_list A,
 l : list A,
 a : A,
 l' : list A,
-IH :
+IH : ∀ (x : @nodup A l'), P (@quot.mk (nodup_list A) (nodup_list_setoid A) (@subtype.tag (list A) (@nodup A) l' x)),
-  ∀ (x : @nodup A l'),
-    P (@quot.mk (nodup_list A) (nodup_list_setoid A) (@subtype.tag (list A) (λ (l : list A), @nodup A l) l' x)),
 nodup_al' : @nodup A (@cons A a l'),
 anl' : not (@list.mem A a l'),
 H3 : @eq (list A) (@list.insert A (λ (a b : A), h a b) a l') (@cons A a l'),
 nodup_l' : @nodup A l',
-P_l' :
+P_l' : P (@quot.mk (nodup_list A) (nodup_list_setoid A) (@subtype.tag (list A) (@nodup A) l' nodup_l')),
-  P (@quot.mk (nodup_list A) (nodup_list_setoid A) (@subtype.tag (list A) (λ (l : list A), @nodup A l) l' nodup_l')),
 H4 :
   P
     (@insert A (λ (a b : A), h a b) a
-       (@quot.mk (nodup_list A) (nodup_list_setoid A)
+       (@quot.mk (nodup_list A) (nodup_list_setoid A) (@subtype.tag (list A) (@nodup A) l' nodup_l')))
-          (@subtype.tag (list A) (λ (l : list A), @nodup A l) l' nodup_l')))
+⊢ P (@quot.mk (nodup_list A) (nodup_list_setoid A) (@subtype.tag (list A) (@nodup A) (@cons A a l') nodup_al'))
-⊢ P
-    (@quot.mk (nodup_list A) (nodup_list_setoid A)
-       (@subtype.tag (list A) (λ (l : list A), @nodup A l) (@cons A a l') nodup_al'))
 finset_induction_bug.lean:16:5: error: failed to add declaration 'finset.induction₂' to environment, value has metavariables
 remark: set 'formatter.hide_full_terms' to false to see the complete term
   λ (A : Type) (h : …) (P : …) (H1 : …) (H2 : …) (s : …),
-    @quot.induction_on … … … s
+    @quot.induction_on … … P s
       (λ (u : …),
          @subtype.destruct … … … u
            (λ (l : …),
@@ -77,6 +65,5 @@ remark: set 'formatter.hide_full_terms' to false to see the complete term
                    assert H3 : …, from …,
                    assert nodup_l' : …, from …,
                    assert P_l' : …, from …,
-                   assert H4 : …, from …,
+                   ?M_1 …)))
-                   ?M_1)))
 finset_induction_bug.lean:30:49: error: invalid end of module, expecting 'end'

tests/lean/gen_bug.lean.expected.out

@@ -20,5 +20,4 @@ b : B
 ⊢ @heq A a B b → @heq B b A a
 gen_bug.lean:12:0: error: failed to add declaration 'tst' to environment, value has metavariables
 remark: set 'formatter.hide_full_terms' to false to see the complete term
-  λ (A B : Type) (a : A) (b : B),
+  ?M_1
-    ?M_1

tests/lean/gen_fail.lean.expected.out

@@ -17,5 +17,4 @@ v : vector ℕ n
 ⊢ v = v
 gen_fail.lean:7:0: error: failed to add declaration 'tst' to environment, value has metavariables
 remark: set 'formatter.hide_full_terms' to false to see the complete term
-  λ (n : ℕ) (v : …),
+  ?M_1
-    ?M_1

tests/lean/goals1.lean.expected.out

@@ -6,5 +6,4 @@ Hbc : eq b c
 ⊢ eq b c
 goals1.lean:9:0: error: failed to add declaration 'foo' to environment, value has metavariables
 remark: set 'formatter.hide_full_terms' to false to see the complete term
-  λ (A : Type) (a b c : A) (Hab : …) (Hbc : …),
+  ?M_1
-    ?M_1

tests/lean/inv_del.lean.expected.out

@@ -6,5 +6,4 @@ a : A
 ⊢ P (vone a)
 inv_del.lean:15:2: error: failed to add declaration 'vec.eone' to environment, value has metavariables
 remark: set 'formatter.hide_full_terms' to false to see the complete term
-  λ (A : Type) (P : …) (H : …) (v : …),
+  ?M_1
-    ?M_1

tests/lean/print_ax2.lean.expected.out

@@ -1,2 +1,2 @@
 em : ∀ (a : Prop), a ∨ ¬a
-strong_indefinite_description : Π {A : Type} (P : A → Prop), nonempty A → { (x : A)| (∃ (y : A), P y) → P x}
+strong_indefinite_description : Π {A : Type} (P : A → Prop), nonempty A → { (x : A)| Exists P → P x}

tests/lean/quasireducible.lean.expected.out

@@ -11,8 +11,7 @@ H : f a = a
 ⊢ g a = a
 quasireducible.lean:11:3: error: failed to add declaration 'example' to environment, value has metavariables
 remark: set 'formatter.hide_full_terms' to false to see the complete term
-  λ (a : nat) (H : …),
+  ?M_1
-    ?M_1
 quasireducible.lean:16:11: error:invalid 'rewrite' tactic, rewrite step failed using pattern
   f a
 no subterm in the goal matched the pattern
@@ -26,5 +25,4 @@ H : f a = a
 ⊢ g a = a
 quasireducible.lean:16:3: error: failed to add declaration 'example' to environment, value has metavariables
 remark: set 'formatter.hide_full_terms' to false to see the complete term
-  λ (a : nat) (H : …),
+  ?M_1
-    ?M_1

tests/lean/revert_fail.lean.expected.out

@@ -11,8 +11,7 @@ v : vector A n
 ⊢ v = v
 revert_fail.lean:6:0: error: failed to add declaration 'example' to environment, value has metavariables
 remark: set 'formatter.hide_full_terms' to false to see the complete term
-  λ (A : Type) (n : nat) (v : …),
+  ?M_1
-    ?M_1
 revert_fail.lean:11:2: error:invalid tactic, there are no goals to be solved
 proof state:
 no goals
@@ -21,8 +20,7 @@ n : nat
 ⊢ n = n
 revert_fail.lean:12:0: error: failed to add declaration 'example' to environment, value has metavariables
 remark: set 'formatter.hide_full_terms' to false to see the complete term
-  λ (n : nat),
+  ?M_1
-    ?M_1
 revert_fail.lean:16:2: error:invalid 'revert' tactic, unknown hypothesis 'm'
 proof state:
 n : nat
@@ -32,5 +30,4 @@ n : nat
 ⊢ n = n
 revert_fail.lean:17:0: error: failed to add declaration 'example' to environment, value has metavariables
 remark: set 'formatter.hide_full_terms' to false to see the complete term
-  λ (n : nat),
+  ?M_1
-    ?M_1

tests/lean/rewrite_fail.lean.expected.out

@@ -13,8 +13,7 @@ Hb : b = 0
 ⊢ a + b = 0
 rewrite_fail.lean:6:0: error: failed to add declaration 'example' to environment, value has metavariables
 remark: set 'formatter.hide_full_terms' to false to see the complete term
-  λ (a b : ℕ) (Ha : …) (Hb : …),
+  ?M_1
-    ?M_1
 rewrite_fail.lean:11:2: error:invalid tactic, there are no goals to be solved
 proof state:
 no goals
@@ -23,5 +22,4 @@ a : ℕ
 ⊢ a = a
 rewrite_fail.lean:12:0: error: failed to add declaration 'example' to environment, value has metavariables
 remark: set 'formatter.hide_full_terms' to false to see the complete term
-  λ (a : ℕ),
+  ?M_1
-    ?M_1

tests/lean/test.sh

@@ -12,10 +12,16 @@ if [ $# -ne 2 ]; then
 else
     INTERACTIVE=$2
 fi
+
 NUM_ERRORS=0
 for f in *.lean; do
     echo "-- testing $f"
-    "$LEAN" -t config.lean "$f" &> "$f.produced.out.1"
+    if [ ${f: -6} == ".hlean" ]; then
+        CONFIG="config.hlean"
+    else
+        CONFIG="config.lean"
+    fi
+    "$LEAN" -t $CONFIG "$f" &> "$f.produced.out.1"
     sed "/warning: imported file uses 'sorry'/d" "$f.produced.out.1" > "$f.produced.out"
     rm -f -- "$f.produced.out.1"
     if test -f "$f.expected.out"; then

tests/lean/unsolved_proof_qed.lean.expected.out

@@ -17,8 +17,7 @@ H₂ : b = c
 ⊢ a = c
 unsolved_proof_qed.lean:2:0: error: failed to add declaration 'example' to environment, value has metavariables
 remark: set 'formatter.hide_full_terms' to false to see the complete term
-  λ (a b c : nat) (H₁ : …) (H₂ : …),
+  ?M_1
-    ?M_1
 unsolved_proof_qed.lean:5:33: error: don't know how to synthesize placeholder
 a b c : nat,
 H₁ : a = b,
@@ -39,5 +38,4 @@ H₂ : b = c
 unsolved_proof_qed.lean:5:0: error: failed to add declaration 'example' to environment, value has metavariables
 remark: set 'formatter.hide_full_terms' to false to see the complete term
   λ (a b c : nat) (H₁ : …) (H₂ : …),
-    have aux : …, from ?M_1,
+    … ?M_1
-    …

tests/lean/user_rec_crash.lean.expected.out

@@ -9,5 +9,4 @@ h : a ∧ b
 ⊢ a
 user_rec_crash.lean:4:0: error: failed to add declaration 'example' to environment, value has metavariables
 remark: set 'formatter.hide_full_terms' to false to see the complete term
-  λ (a b : Prop) (h : …),
+  ?M_1
-    ?M_1

tests/lean/whnf.lean.expected.out

@@ -1,4 +1,4 @@
-succ (nat.rec 2 (λ (b₁ r : ℕ), succ r) 0)
+succ (nat.rec 2 (λ (b₁ : ℕ), succ) 0)
 3
-succ (nat.rec a (λ (b₁ r : ℕ), succ r) 0)
+succ (nat.rec a (λ (b₁ : ℕ), succ) 0)
 succ a