Skip to content

Instantly share code, notes, and snippets.

Show Gist options
  • Save skaslev/c21c33f7d1c7723a1a9b4547edd42dc9 to your computer and use it in GitHub Desktop.
Save skaslev/c21c33f7d1c7723a1a9b4547edd42dc9 to your computer and use it in GitHub Desktop.
meta def blast : tactic unit := using_smt $ return ()
structure Category :=
(Obj : Type)
(Hom : Obj → Obj → Type)
structure Functor (C : Category) (D : Category) :=
(onObjects : C^.Obj → D^.Obj)
(onMorphisms : Π { X Y : C^.Obj },
C^.Hom X Y → D^.Hom (onObjects X) (onObjects Y))
namespace workaround1
/-
Declare notation for applying "type casts" using objectWitness.
Cons: it is verbose.
-/
def transportHom
{C D : Category} {F G : Functor C D}
(objectWitness : ∀ X : C^.Obj, F^.onObjects X = G^.onObjects X )
{X Y : C^.Obj}
(h : D^.Hom (F^.onObjects X) (F^.onObjects Y)) : D^.Hom (G^.onObjects X) (G^.onObjects Y) :=
eq.rec_on (objectWitness X) (eq.rec_on (objectWitness Y) h)
infix `►`:60 := transportHom
lemma Functors_pointwise_equal
{ C D : Category }
{ F G : Functor C D }
( objectWitness : ∀ X : C^.Obj, F^.onObjects X = G^.onObjects X )
( morphismWitness : ∀ X Y : C^.Obj, ∀ f : C^.Hom X Y, objectWitness ► F^.onMorphisms f = G^.onMorphisms f ) : F = G :=
begin
induction F with F_onObjects F_onMorphisms,
induction G with G_onObjects G_onMorphisms,
assert h_objects : F_onObjects = G_onObjects, exact funext objectWitness,
/-
(rewrite h_objects at F_onMorphisms) creates a copy of F_onMorphisms because
other hypotheses depend on F_onMorphisms. One possible workaround is to revert the dependencies,
rewrite, and then reintroduce them. For equalities (h : a = b), where the lhs/rhs
is a variable, the tactic subst is much more effective. It reverts and reintroduces things automatically
for us.
-/
subst h_objects,
/- Note that F_onMorphisms and G_onMorphisms have implicit arguments, and they cannot be inferred
if we don't provide f. We can workaround this by using '@'. -/
assert h_morphisms : @F_onMorphisms = @G_onMorphisms,
apply funext, intro X, apply funext, intro Y, apply funext, intro f,
exact morphismWitness X Y f,
subst h_morphisms
end
end workaround1
namespace workaround2
/-
Use heterogeneous equality.
We can convert a heterogeneous equality back into a homogeneous one, if we can prove the types are equal.
Cons: it is easy to make mistakes. For example, given (a : nat) (s : string) (h : a == s), the hypothesis
h is probably a mistake, but Lean will not complain.
-/
lemma Functors_pointwise_equal
{ C D : Category }
{ F G : Functor C D }
( objectWitness : ∀ X : C^.Obj, F^.onObjects X = G^.onObjects X )
( morphismWitness : ∀ X Y : C^.Obj, ∀ f : C^.Hom X Y, F^.onMorphisms f == G^.onMorphisms f ) : F = G :=
begin
induction F with F_onObjects F_onMorphisms,
induction G with G_onObjects G_onMorphisms,
assert h_objects : F_onObjects = G_onObjects, exact funext objectWitness,
subst h_objects,
assert h_morphisms : @F_onMorphisms = @G_onMorphisms,
apply funext, intro X, apply funext, intro Y, apply funext, intro f,
/- We need to use eq_of_heq to convert the heterogeneous equality into a homogeneous one -/
exact (eq_of_heq (morphismWitness X Y f)),
subst h_morphisms
end
end workaround2
namespace workaround3
/-
Write a tactic for automatically generating the type casts, and notation for invoking it.
Cons: the tactic may create "ugly" proofs, and these proofs will be nested in the
statement of your theorem.
-/
open smt_tactic
/- Very simple tactic that uses hypotheses from the local context for performing 3
rounds of heuristic instantiation, and congruence closure. -/
meta def simple_tac : tactic unit :=
using_smt $ intros >> add_lemmas_from_facts >> repeat_at_most 3 ematch
/- Version of cast operator that "hides" the "ugly" proof -/
def {u} auto_cast {α β : Type u} {h : α = β} (a : α) :=
cast h a
notation `⟦` p `⟧` := @auto_cast _ _ (by simple_tac) p
lemma Functors_pointwise_equal
{ C D : Category }
{ F G : Functor C D }
( objectWitness : ∀ X : C^.Obj, F^.onObjects X = G^.onObjects X )
( morphismWitness : ∀ X Y : C^.Obj, ∀ f : C^.Hom X Y, ⟦ F^.onMorphisms f ⟧ = G^.onMorphisms f ) : F = G :=
begin
induction F with F_onObjects F_onMorphisms,
induction G with G_onObjects G_onMorphisms,
assert h_objects : F_onObjects = G_onObjects, exact funext objectWitness,
subst h_objects,
assert h_morphisms : @F_onMorphisms = @G_onMorphisms,
apply funext, intro X, apply funext, intro Y, apply funext, intro f,
exact morphismWitness X Y f,
subst h_morphisms
end
print Functors_pointwise_equal
end workaround3
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment