Converting proofs to term-style

Stream: new members

[Sebastian Monnet]

I'm trying to write these proofs without tactics, and the rewrites are giving me a hard time.

import order.filter.basic
open filter set

def cofinite (α : Type) : filter α :=
{ sets := { S : set α | (Sᶜ).finite },
  univ_sets := begin
    change univᶜ.finite,
    rw compl_univ,
    exact finite_empty,
  end,
  sets_of_superset :=
  λ X Y hX hY, finite.subset hX (compl_subset_compl.2 hY),
  inter_sets := begin
    intros X Y hX hY,
    change (X ∩ Y)ᶜ.finite,
    rw compl_inter,
    exact finite.union hX hY,
  end }

Could someone show me how to do either of them? I suspect the other one will use the same tricks.

[Kevin Buzzard]

Rewrites are hard to do in term mode. If you can get eq.subst to work then great, otherwise stick to tactic mode

[Alex J. Best]

You can do the first one as (((@compl_univ α).symm) ▸ finite_empty : (univ : set α)ᶜ.finite),, but there isn't much gain in doing so,

[Alex J. Best]

Its just harder to read and more fiddly to write than using tactic mode when rewrites are involved

[Kevin Buzzard]

univ_sets := by simp,

[Kevin Buzzard]

The little black triangle (\t) is notation for eq.subst, a far less powerful version of rw which needs a lot of help with unification (as Alex demonstrates)

[Sebastian Monnet]

huh, that surprises me

[Sebastian Monnet]

Thanks for explaining!

[Kevin Buzzard]

You can right click on rw and see how it works -- it's written in meta code. rw uses rw_core which uses rw_goal which uses rewrite which uses rewrite_core which is written in C++ so now I get lost.

[Alex J. Best]

You can also use tactic#show_term to print the proof term created by a given tactic, for things like intro and exact this is usually a concise/readable term, but for rewrite there is a lot of id ((id (eq.rec (eq.refl (X ∩ Y)ᶜ.finite) (X.compl_inter Y))).mpr (finite.union hX hY)).
It can be the case that using the little triangle is helpful to avoid nested tactic blocks, and you can certainly find uses of it in mathlib so I'd say its worth knowing how to do, but not always worth doing in every situation.

[Eric Rodriguez]

also, usually when there's eq.rec in a term proof, it will not typecheck if you just copy-paste it into term mode; the elaborator is fickle