diff --git a/category_theory/isomorphism.lean b/category_theory/isomorphism.lean index 4d065474a514b..44c4217ff29a7 100644 --- a/category_theory/isomorphism.lean +++ b/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,7 +137,7 @@ 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, @@ -145,7 +145,7 @@ instance epi_of_iso (f : X ⟶ Y) [is_iso f] : epi f := 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 \ No newline at end of file +end category_theory diff --git a/tactic/basic.lean b/tactic/basic.lean index 1d6d314929bd2..50d62af32954c 100644 --- a/tactic/basic.lean +++ b/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 | _ := [] diff --git a/tactic/ext.lean b/tactic/ext.lean index f99d4f37ad033..cfc1f6b682ceb 100644 --- a/tactic/ext.lean +++ 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