feat(tactic/elim_cast): remove cast expressions from goal

Author: cipher1024

data/prod.lean

@@ -6,6 +6,8 @@ Authors: Johannes Hölzl
 Extends theory on products
 -/
 
+import tactic.ext
+
 universes u v
 variables {α : Type u} {β : Type v}
 
@@ -23,6 +25,7 @@ namespace prod
 lemma ext_iff {p q : α × β} : p = q ↔ p.1 = q.1 ∧ p.2 = q.2 :=
 by rw [← @mk.eta _ _ p, ← @mk.eta _ _ q, mk.inj_iff]
 
+@[extensionality]
 lemma ext {α β} {p q : α × β} : p.1 = q.1 → p.2 = q.2 → p = q :=
 by rw [ext_iff] ; intros ; split ; assumption
 
@@ -60,4 +63,3 @@ theorem lex_def (r : α → α → Prop) (s : β → β → Prop)
  end⟩
 
 end prod
-

logic/basic.lean

@@ -631,3 +631,15 @@ lemma classical.nonempty_pi {α : Sort u} {β : α → Sort v} :
 iff.intro (assume ⟨f⟩ a, ⟨f a⟩) (assume f, ⟨assume a, classical.choice $ f a⟩)
 
 end nonempty
+
+lemma cast_eq_of_heq  {α : Sort*} {β : Sort*} {x : α} {y : β}
+  (h : α = β)
+  (h' : x == y) :
+  cast h x = y :=
+by cc
+
+lemma heq_of_cast_eq {α β} {x : α} {y : β}
+  (h : α = β)
+  (h' : cast h x = y) :
+  x == y :=
+by cc

tactic/cache.lean

@@ -1,14 +1,15 @@
 
 import tactic.basic
 
+open lean
 open lean.parser
 
 local postfix `?`:9001 := optional
 local postfix *:9001 := many
 
 namespace tactic
 namespace interactive
-open interactive interactive.types
+open interactive interactive.types expr
 
 /-- Unfreeze local instances, which allows us to revert
   instances in the context. -/

tactic/ext.lean

@@ -0,0 +1,15 @@
+/--
+ Tag lemmas of the form:
+
+ ```
+ lemma my_collection.ext (a b : my_collection)
+   (h : ∀ x, a.lookup x = b.lookup y) :
+   a = b := ...
+ ```
+ -/
+@[user_attribute]
+meta def extensional_attribute : user_attribute :=
+{ name := `extensionality,
+  descr := "lemmas usable by `ext` tactic" }
+
+attribute [extensionality] _root_.funext array.ext

tactic/interactive.lean

@@ -5,7 +5,8 @@ Authors: Mario Carneiro
 -/
 import data.dlist data.dlist.basic data.prod category.basic
   tactic.basic tactic.rcases tactic.generalize_proofs
-  tactic.split_ifs meta.expr logic.basic
+  tactic.split_ifs meta.expr tactic.ext
+  logic.basic
 
 open lean
 open lean.parser
@@ -197,7 +198,6 @@ do let h := h.get_or_else `this,
 
 meta def symm_apply (e : expr) (cfg : apply_cfg := {}) : tactic (list (name × expr)) :=
 tactic.apply e cfg <|> (symmetry >> tactic.apply e cfg)
-
 /--
   `apply_assumption` looks for an assumption of the form `... → ∀ _, ... → head`
   where `head` matches the current goal.
@@ -280,7 +280,7 @@ repeat (do
   try (refine ``( or_iff_not_imp_left.mpr _)),
   try (refine ``( or_iff_not_imp_right.mpr _)),
   gs' ← get_goals,
-  guard (gs ≠ gs') ) ;
+  guard (gs ≠ gs') );
 repeat
 (reflexivity <|> solve_by_elim <|>
  constructor_matching none [``(_ ∧ _),``(_ ↔ _),``(Exists _)] ) ;
@@ -289,22 +289,6 @@ done
 /-- Shorter name for the tactic `tautology`. -/
 meta def tauto := tautology
 
-/--
- Tag lemmas of the form:
-
- ```
- lemma my_collection.ext (a b : my_collection)
-   (h : ∀ x, a.lookup x = b.lookup y) :
-   a = b := ...
- ```
- -/
-@[user_attribute]
-meta def extensional_attribute : user_attribute :=
-{ name := `extensionality,
-  descr := "lemmas usable by `ext` tactic" }
-
-attribute [extensionality] _root_.funext array.ext prod.ext
-
 /--
   `ext1 id` selects and apply one extensionality lemma (with attribute
   `extensionality`), using `id`, if provided, to name a local constant
@@ -537,5 +521,18 @@ meta def apply_field : tactic unit :=
 propagate_tags $
 get_current_field >>= applyc
 
+/-- `elim_cast e with x` matches on `cast _ e` in the goal and replaces it with
+    `x`. It also adds `Hx : e == x` as an assumption.
+
+    `elim_cast! e with x` acts similarly but reverts `Hx`.
+-/
+meta def elim_cast (rev : parse (tk "!")?) (e : parse texpr) (n : parse (tk "with" *> ident)) : tactic unit :=
+do h ← get_unused_name ("H" ++ n.to_string : string),
+   interactive.generalize h () (``(cast _ %%e), n),
+   asm ← get_local h,
+   to_expr ``(heq_of_cast_eq _ %%asm) >>= note h none,
+   tactic.clear asm,
+   when rev.is_some (interactive.revert [n])
+
 end interactive
 end tactic