feat(library/unifier): remove "eager delta hack", use is_def_eq when delta-constraint does not have metavariables anymore

The "eager-delta hack" was added to minimize problems in the interaction
between coercions and delta-constraints.

hott/types/trunc.hlean

@@ -173,8 +173,10 @@ namespace is_trunc
 
   theorem is_contr_loop_of_is_trunc (n : ℕ) (A : Type*) [H : is_trunc (n.-2.+1) A] :
     is_contr (Ω[n] A) :=
-  by induction A; exact iff.mp !is_trunc_iff_is_contr_loop _ _
-
+  begin
+    induction A,
+    apply iff.mp !is_trunc_iff_is_contr_loop H
+  end
 
 end is_trunc open is_trunc
 

library/data/real/complete.lean

@@ -512,7 +512,7 @@ assert int.of_nat n ≥ ceil (2 / ε),
   by rewrite of_nat_nat_abs; apply le_abs_self,
 have int.of_nat (succ n) ≥ ceil (2 / ε),
   begin apply le.trans, exact this, apply int.of_nat_le_of_nat_of_le, apply le_succ end,
-have H₁ : succ n ≥ ceil (2 / ε), from of_int_le_of_int_of_le this,
+have H₁ : int.succ n ≥ ceil (2 / ε), from of_int_le_of_int_of_le this,
 have H₂ : succ n ≥ 2 / ε, from !le.trans !le_ceil H₁,
 have H₃ : 2 / ε > 0, from div_pos_of_pos_of_pos two_pos H,
 have 1 / succ n < ε, from calc

src/library/unifier.cpp

@@ -1023,14 +1023,9 @@ struct unifier_fn {
         }
 
         if (is_eq_deltas(lhs, rhs)) {
-            if (!split_delta(lhs) && is_type(lhs)) {
-                // If lhs (and consequently rhs) is a type, and not case-split is generated, then process delta constraint eagerly.
-                return process_delta(c);
-            } else {
-                // we need to create a backtracking point for this one
-                add_cnstr(c, cnstr_group::Basic);
-                return true;
-            }
+            // we need to create a backtracking point for this one
+            add_cnstr(c, cnstr_group::Basic);
+            return true;
         } else if (is_meta(lhs) && is_meta(rhs)) {
             // flex-flex constraints are delayed the most.
             unsigned cidx = add_cnstr(c, cnstr_group::FlexFlex);
@@ -2681,7 +2676,7 @@ struct unifier_fn {
                 }
             } else {
                 lean_assert(is_eq_cnstr(c));
-                if (is_delta_cnstr(c)) {
+                if (is_delta_cnstr(c) && (!modified || has_expr_metavar_relaxed(cnstr_lhs_expr(c)) || has_expr_metavar_relaxed(cnstr_rhs_expr(c)))) {
                     return process_delta(c);
                 } else if (modified) {
                     return is_def_eq(cnstr_lhs_expr(c), cnstr_rhs_expr(c), c.get_justification());

tests/lean/hott/delta_issue2.hlean

@@ -0,0 +1,17 @@
+open nat eq
+
+theorem add_assoc₁ : Π (a b c : ℕ), (a + b) + c = a + (b + c)
+| a b 0 := eq.refl (nat.rec a (λ x, succ) b)
+| a b (succ n) :=
+  calc (a + b) + (succ n) = succ ((a + b) + n) : rfl
+                      ... = succ (a + (b + n)) : ap succ (add_assoc₁ a b n)
+                      ... = a + (succ (b + n)) : rfl
+                      ... = a + (b + (succ n)) : rfl
+
+theorem add_assoc₂ : Π (a b c : ℕ), (a + b) + c = a + (b + c)
+| a b 0        := eq.refl (nat.rec a (λ x, succ) b)
+| a b (succ n) := ap succ (add_assoc₂ a b n)
+
+theorem add_assoc₃ : Π (a b c : ℕ), (a + b) + c = a + (b + c)
+| a b nat.zero := eq.refl (nat.add a b)
+| a b (succ n) := ap succ (add_assoc₃ a b n)

tests/lean/run/delta_issue1.lean

@@ -0,0 +1,36 @@
+import data.set.basic
+open set
+
+definition preimage {X Y : Type} (f : X → Y) (b : set Y) : set X := λ x, f x ∈ b
+
+example {X Y : Type} {b : set Y} (f : X → Y) (x : X) (H : x ∈ preimage f b) : f x ∈ b :=
+H
+
+theorem preimage_subset {X Y : Type} {a b : set Y} (f : X → Y) (H : a ⊆ b) : preimage f a ⊆ preimage f b :=
+λ (x : X) (H' : x ∈ preimage f a), show x ∈ preimage f b,
+from @H (f x) H'
+
+example {X Y : Type} {a b : set Y} (f : X → Y) (H : a ⊆ b) : preimage f a ⊆ preimage f b :=
+λ (x : X) (H' : x ∈ preimage f a),
+have f x ∈ a, from H',
+have f x ∈ b, from mem_of_subset_of_mem H this,
+this
+
+example {X Y : Type} {a b : set Y} (f : X → Y) (H : a ⊆ b) : preimage f a ⊆ preimage f b :=
+λ (x : X) (H' : x ∈ preimage f a),
+have f x ∈ b, from mem_of_subset_of_mem H H',
+this
+
+example {X Y : Type} {a b : set Y} (f : X → Y) (H : a ⊆ b) : preimage f a ⊆ preimage f b :=
+λ (x : X) (H' : x ∈ preimage f a),
+@H (f x) H'
+
+lemma mem_preimage_of_mem {X Y : Type} {f : X → Y} {s : set Y} {x : X} : f x ∈ s → x ∈ preimage f s :=
+assume H, H
+
+lemma mem_of_mem_preimage {X Y : Type} {f : X → Y} {s : set Y} {x : X} : x ∈ preimage f s → f x ∈ s :=
+assume H, H
+
+example {X Y : Type} {a b : set Y} (f : X → Y) (H : a ⊆ b) : preimage f a ⊆ preimage f b :=
+take x, assume H',
+mem_preimage_of_mem (mem_of_subset_of_mem H (mem_of_mem_preimage H'))