From 72663e8a06ffc53864a49ea9028c5f32a06e1f7e Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 8 May 2015 11:32:31 -0700
Subject: [PATCH] feat(library/tactic/rewrite_tactic): take hypotheses into
 account when checking rewrite step

---
 src/library/tactic/rewrite_tactic.cpp         |  2 +-
 tests/lean/550.lean.expected.out              | 10 +--
 tests/lean/finset_induction_bug.lean          | 30 +++++++
 .../finset_induction_bug.lean.expected.out    | 82 +++++++++++++++++++
 4 files changed, 118 insertions(+), 6 deletions(-)
 create mode 100644 tests/lean/finset_induction_bug.lean
 create mode 100644 tests/lean/finset_induction_bug.lean.expected.out

diff --git a/src/library/tactic/rewrite_tactic.cpp b/src/library/tactic/rewrite_tactic.cpp
index 95765baa4..807195314 100644
--- a/src/library/tactic/rewrite_tactic.cpp
+++ b/src/library/tactic/rewrite_tactic.cpp
@@ -1209,7 +1209,7 @@ class rewrite_fn {
     }
 
     void check_term(expr const & H) {
-        lean::check_term(m_env, H);
+        lean::check_term(m_env, m_g.abstract(H));
     }
 
     bool process_rewrite_hypothesis(expr const & hyp, expr const & orig_elem, expr const & pattern, occurrence const & occ) {
diff --git a/tests/lean/550.lean.expected.out b/tests/lean/550.lean.expected.out
index c07a78000..fb5d33b39 100644
--- a/tests/lean/550.lean.expected.out
+++ b/tests/lean/550.lean.expected.out
@@ -1,13 +1,13 @@
 550.lean:44:72: error:invalid 'rewrite' tactic, step produced type incorrect term, details: type mismatch at application
-  eq.rec (eq.rec (eq.refl function.id) (eq.symm linv))
+  eq.symm linv
 term
-  eq.rec (eq.refl function.id) (eq.symm linv)
+  linv
 has type
-  x = function.id
-but is expected to have type
   finv ∘ func = function.id
+but is expected to have type
+  x = function.id
 rewrite step failed using pattern
-  finv ∘ func
+  finv_1 ∘ func_1
 proof state:
 A : Type,
 f : bijection A,
diff --git a/tests/lean/finset_induction_bug.lean b/tests/lean/finset_induction_bug.lean
new file mode 100644
index 000000000..aa0e7c3e2
--- /dev/null
+++ b/tests/lean/finset_induction_bug.lean
@@ -0,0 +1,30 @@
+import data.finset
+open list
+
+namespace finset
+variable {A : Type}
+variable [h : decidable_eq A]
+include h
+
+set_option pp.implicit true
+set_option pp.notation false
+
+protected theorem induction₂ {P : finset A → Prop}
+    (H1 : P empty)
+    (H2 : ∀⦃s : finset A⦄, ∀{a : A}, a ∉ s → P s → P (insert a s)) :
+  ∀s, P s :=
+take s,
+quot.induction_on s
+  take u,
+  subtype.destruct u
+    take l,
+    list.induction_on l
+      (assume nodup_l, H1)
+      (take a l',
+        assume IH nodup_al',
+        assert anl' : a ∉ l', from not_mem_of_nodup_cons nodup_al',
+        assert H3 : list.insert a l' = a :: l', from insert_eq_of_not_mem anl',
+        assert nodup_l' : nodup l', from nodup_of_nodup_cons nodup_al',
+        assert P_l' : P (quot.mk (subtype.tag l' nodup_l')), from IH nodup_l',
+        assert H4 : P (insert a (quot.mk (subtype.tag l' nodup_l'))), from H2 anl' P_l',
+        begin rewrite [eq.symm H3], apply H4 end)
diff --git a/tests/lean/finset_induction_bug.lean.expected.out b/tests/lean/finset_induction_bug.lean.expected.out
new file mode 100644
index 000000000..e352f339c
--- /dev/null
+++ b/tests/lean/finset_induction_bug.lean.expected.out
@@ -0,0 +1,82 @@
+finset_induction_bug.lean:30:23: error:invalid 'rewrite' tactic, step produced type incorrect term, details: type mismatch at application
+  @subtype.tag (list A) (λ (l : list A), @nodup A l) x nodup_al'
+term
+  nodup_al'
+has type
+  @nodup A (@cons A a l')
+but is expected to have type
+  @nodup A x
+rewrite step failed using pattern
+  @cons A_1 a_1 l'_1
+proof state:
+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),
+s : finset A,
+u : nodup_list A,
+l : list A,
+a : A,
+l' : list A,
+IH :
+  ∀ (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 (@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)
+          (@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) (λ (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),
+s : finset A,
+u : nodup_list A,
+l : list A,
+a : A,
+l' : list A,
+IH :
+  ∀ (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 (@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)
+          (@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) (λ (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
+      (λ (u : …),
+         @subtype.destruct … … … u
+           (λ (l : …),
+              @list.induction_on A … l …
+                (λ (a : A) (l' : …) (IH : …) (nodup_al' : …),
+                   assert anl' : …, from …,
+                   assert H3 : …, from …,
+                   assert nodup_l' : …, from …,
+                   assert P_l' : …, from …,
+                   assert H4 : …, from …,
+                   ?M_1)))
+finset_induction_bug.lean:30:49: error: invalid end of module, expecting 'end'