feat(tactic/ext): add indexing of extensionality lemmas

category_theory/isomorphism.lean

@@ -43,30 +43,30 @@ instance : has_coe (iso.{u v} X Y) (X ⟶ Y) :=
     refl
   end
 
-@[symm] def symm (I : X ≅ Y) : Y ≅ X := 
+@[symm] def symm (I : X ≅ Y) : Y ≅ X :=
 { hom := I.inv,
   inv := I.hom,
   hom_inv_id' := I.inv_hom_id',
   inv_hom_id' := I.hom_inv_id' }
 
 -- These are the restated lemmas for iso.hom_inv_id' and iso.inv_hom_id'
-@[simp] lemma hom_inv_id (α : X ≅ Y) : (α : X ⟶ Y) ≫ (α.symm : Y ⟶ X) = 𝟙 X := 
+@[simp] lemma hom_inv_id (α : X ≅ Y) : (α : X ⟶ Y) ≫ (α.symm : Y ⟶ X) = 𝟙 X :=
 begin unfold_coes, unfold symm, have p := α.hom_inv_id', dsimp at p, rw p end
-@[simp] lemma inv_hom_id (α : X ≅ Y) : (α.symm : Y ⟶ X) ≫ (α : X ⟶ Y) = 𝟙 Y := 
+@[simp] lemma inv_hom_id (α : X ≅ Y) : (α.symm : Y ⟶ X) ≫ (α : X ⟶ Y) = 𝟙 Y :=
 begin unfold_coes, unfold symm, have p := iso.inv_hom_id', dsimp at p, rw p end
 
 -- We rewrite the projections `.hom` and `.inv` into coercions.
 @[simp] lemma hom_eq_coe (α : X ≅ Y) : α.hom = (α : X ⟶ Y) := rfl
 @[simp] lemma inv_eq_coe (α : X ≅ Y) : α.inv = (α.symm : Y ⟶ X) := rfl
 
-@[refl] def refl (X : C) : X ≅ X := 
+@[refl] def refl (X : C) : X ≅ X :=
 { hom := 𝟙 X,
   inv := 𝟙 X }
 
 @[simp] lemma refl_coe (X : C) : ((iso.refl X) : X ⟶ X) = 𝟙 X := rfl
 @[simp] lemma refl_symm_coe  (X : C) : ((iso.refl X).symm : X ⟶ X)  = 𝟙 X := rfl
 
-@[trans] def trans (α : X ≅ Y) (β : Y ≅ Z) : X ≅ Z := 
+@[trans] def trans (α : X ≅ Y) (β : Y ≅ Z) : X ≅ Z :=
 { hom := (α : X ⟶ Y) ≫ (β : Y ⟶ Z),
   inv := (β.symm : Z ⟶ Y) ≫ (α.symm : Y ⟶ X),
   hom_inv_id' := begin /- `obviously'` says: -/ erw [category.assoc], conv { to_lhs, congr, skip, rw ← category.assoc }, rw iso.hom_inv_id, rw category.id_comp, rw iso.hom_inv_id end,
@@ -82,40 +82,40 @@ infixr ` ≪≫ `:80 := iso.trans -- type as `\ll \gg`.
 
 end iso
 
-/-- `is_iso` typeclass expressing that a morphism is invertible. 
+/-- `is_iso` typeclass expressing that a morphism is invertible.
     This contains the data of the inverse, but is a subsingleton type. -/
 class is_iso (f : X ⟶ Y) :=
 (inv : Y ⟶ X)
 (hom_inv_id' : f ≫ inv = 𝟙 X . obviously)
 (inv_hom_id' : inv ≫ f = 𝟙 Y . obviously)
 
-def inv (f : X ⟶ Y) [is_iso f] := is_iso.inv f 
+def inv (f : X ⟶ Y) [is_iso f] := is_iso.inv f
 
 namespace is_iso
 
 instance (f : X ⟶ Y) : subsingleton (is_iso f) :=
-⟨ λ a b, begin 
-          cases a, cases b, 
-          dsimp at *, congr, 
+⟨ λ a b, begin
+          cases a, cases b,
+          dsimp at *, congr,
           rw [← category.id_comp _ a_inv, ← b_inv_hom_id', category.assoc, a_hom_inv_id', category.comp_id]
-         end ⟩ 
+         end ⟩
 
-@[simp] def hom_inv_id (f : X ⟶ Y) [is_iso f] : f ≫ inv f = 𝟙 X := is_iso.hom_inv_id' f 
-@[simp] def inv_hom_id (f : X ⟶ Y) [is_iso f] : inv f ≫ f = 𝟙 Y := is_iso.inv_hom_id' f 
+@[simp] def hom_inv_id (f : X ⟶ Y) [is_iso f] : f ≫ inv f = 𝟙 X := is_iso.hom_inv_id' f
+@[simp] def inv_hom_id (f : X ⟶ Y) [is_iso f] : inv f ≫ f = 𝟙 Y := is_iso.inv_hom_id' f
 
-instance (X : C) : is_iso (𝟙 X) := 
+instance (X : C) : is_iso (𝟙 X) :=
 { inv := 𝟙 X }
 
 instance of_iso         (f : X ≅ Y) : is_iso (f : X ⟶ Y) :=
 { inv := (f.symm : Y ⟶ X) }
-instance of_iso_inverse (f : X ≅ Y) : is_iso (f.symm : Y ⟶ X)  := 
+instance of_iso_inverse (f : X ≅ Y) : is_iso (f.symm : Y ⟶ X)  :=
 { inv := (f : X ⟶ Y) }
 
 end is_iso
 
 namespace functor
 
-universes u₁ v₁ u₂ v₂ 
+universes u₁ v₁ u₂ v₂
 variables {D : Type u₂}
 
 variables [𝒟 : category.{u₂ v₂} D]
@@ -137,15 +137,15 @@ instance (F : C ⥤ D) (f : X ⟶ Y) [is_iso f] : is_iso (F.map f) :=
 
 end functor
 
-instance epi_of_iso  (f : X ⟶ Y) [is_iso f] : epi f  := 
+instance epi_of_iso  (f : X ⟶ Y) [is_iso f] : epi f  :=
 { left_cancellation := begin
                          -- This is an interesting test case for better rewrite automation.
                          intros,
                          rw [←category.id_comp C g, ←category.id_comp C h],
                          rw [← is_iso.inv_hom_id f],
                          erw [category.assoc, w, category.assoc],
                        end }
-instance mono_of_iso (f : X ⟶ Y) [is_iso f] : mono f := 
+instance mono_of_iso (f : X ⟶ Y) [is_iso f] : mono f :=
 { right_cancellation := begin
                          intros,
                          rw [←category.comp_id C g, ←category.comp_id C h],
@@ -173,9 +173,11 @@ end functor
 
 def Aut (X : C) := X ≅ X
 
-instance {X : C} : group (Aut X) := 
-by refine { one := iso.refl X, 
+attribute [extensionality iso Aut] iso.ext
+
+instance {X : C} : group (Aut X) :=
+by refine { one := iso.refl X,
             inv := iso.symm,
             mul := iso.trans, .. } ; obviously
 
-end category_theory
+end category_theory

tactic/basic.lean

@@ -335,29 +335,6 @@ meta def try_intros : list name → tactic (list name)
 | [] := try intros $> []
 | (x::xs) := (intro x >> try_intros xs) <|> pure (x :: xs)
 
-meta def rec_beta : expr → tactic expr
-| (expr.app e₀ e₁) := expr.app <$> rec_beta e₀ <*> rec_beta e₁ >>= head_beta
-| (expr.pi n bi e₀ e₁)  := expr.pi n bi  <$> rec_beta e₀ <*> rec_beta e₁ >>= head_beta
-| (expr.lam n bi e₀ e₁) := expr.lam n bi <$> rec_beta e₀ <*> rec_beta e₁ >>= head_beta
-| e := head_beta e
-
-meta def ext1 (xs : list name) : tactic (list name) :=
-do ls ← attribute.get_instances `extensionality,
-   ls.any_of (λ l, do
-     t ← target,
-     g ← main_goal,
-     applyc l,
-     t  ← instantiate_mvars t >>= rec_beta,
-     t' ← get_assignment g >>= infer_type >>= instantiate_mvars >>= rec_beta,
-     guard $ t =ₐ t' ) <|>
-   ls.any_of applyc <|> fail "no applicable extensionality rule found",
-   try_intros xs
-
-meta def ext : list name → option ℕ → tactic unit
-| _  (some 0) := skip
-| xs n        := focus1 $ do
-  ys ← ext1 xs, try (ext ys (nat.pred <$> n))
-
 meta def var_names : expr → list name
 | (expr.pi n _ _ b) := n :: var_names b
 | _ := []

tactic/ext.lean

@@ -3,6 +3,23 @@ import tactic.basic
 
 universes u₁ u₂
 
+open interactive interactive.types
+open lean.parser nat tactic
+
+meta def get_ext_subject : expr → tactic name
+| (expr.pi n bi d b) :=
+  do v  ← mk_local' n bi d,
+     b' ← whnf $ b.instantiate_var v,
+     get_ext_subject b'
+| (expr.app _ e) :=
+  do t ← infer_type e,
+     pure $ t.get_app_fn.const_name
+| _ := pure name.anonymous
+
+open native
+
+meta def rident := do i ← ident, resolve_constant i
+
 /--
  Tag lemmas of the form:
 
@@ -13,11 +30,22 @@ universes u₁ u₂
  ```
  -/
 @[user_attribute]
-meta def extensional_attribute : user_attribute :=
+meta def extensional_attribute : user_attribute (name_map name) (list name) :=
 { name := `extensionality,
-  descr := "lemmas usable by `ext` tactic" }
-
-attribute [extensionality] _root_.funext array.ext
+  descr := "lemmas usable by `ext` tactic",
+  cache_cfg := { mk_cache := λ ls,
+                          do { attrs ← ls.mmap $ λ l,
+                                     do { ls ← extensional_attribute.get_param l,
+                                          if ls.empty
+                                          then list.ret <$> (prod.mk <$> (mk_const l >>= infer_type >>= get_ext_subject)
+                                                                     <*> pure l)
+                                          else pure $ prod.mk <$> ls <*> pure l },
+                               pure $ rb_map.of_list $ attrs.join },
+                 dependencies := [] },
+  parser := many (name.anonymous <$ tk "*" <|> rident) }
+
+attribute [extensionality] array.ext
+attribute [extensionality * thunk] _root_.funext
 
 namespace ulift
 @[extensionality] lemma ext {α : Type u₁} (X Y : ulift.{u₂} α) (w : X.down = Y.down) : X = Y :=
@@ -27,8 +55,22 @@ end
 end ulift
 
 namespace tactic
-open interactive interactive.types
-open lean.parser nat
+
+meta def ext1 (xs : list name) : tactic (list name) :=
+do subject ← target >>= get_ext_subject,
+   m ← extensional_attribute.get_cache,
+   do { rule ← m.find subject,
+        applyc rule } <|>
+     do { ls ← attribute.get_instances `extensionality,
+          ls.any_of applyc } <|>
+     fail format!"no applicable extensionality rule found for {subject}",
+   try_intros xs
+
+meta def ext : list name → option ℕ → tactic unit
+| _  (some 0) := skip
+| xs n        := focus1 $ do
+  ys ← ext1 xs, try (ext ys (nat.pred <$> n))
+
 
 local postfix `?`:9001 := optional
 local postfix *:9001 := many