Tactics for Los's theorem -- can't synthesise placeholder

Stream: general

[Abhimanyu Pallavi Sudhir]

I'm trying to use tactics to do Los's theorem for the hyperreals -- e.g. you would have a goal (¬ Q x ↔ {n : ℕ | ¬ Q ((quotient.out' x) n)} ∈ (@hyperfilter ℕ).sets), and a tactic called transfer_not would reduce it to the goal (Q3 x ↔ {n : ℕ | Q3 ((quotient.out' x) n)} ∈ (@hyperfilter ℕ).sets) -- similarly transfer_and, transfer_exists, so you can recursively reduce your goal to transfer for atomic formulae, and finally another tactic to sort that out. This doesn't work for any proposition Q, which is why we need tactics, rather than theorems. So I figured something like this should work:

import data.real.hyperreal
meta def trans_not (x : ℝ*) {P : ∀ {α : Type} [discrete_linear_ordered_field α], α → Prop} :
  tactic unit := do
`[have HImp : (P x ↔ {n : ℕ | P ((quotient.out' x) n)} ∈ (@hyperfilter ℕ).sets)
    → (¬ P x ↔ {n : ℕ | ¬ P ((quotient.out' x) n)} ∈ (@hyperfilter ℕ).sets) :=
  λ Hψ, ⟨ λ HnQ, (ultrafilter_iff_compl_mem_iff_not_mem.mp U _).mpr (not_imp_not.mpr Hψ.2 HnQ),
  λ HnSQ, not_imp_not.mpr Hψ.1 ((ultrafilter_iff_compl_mem_iff_not_mem.mp U _).mp HnSQ) ⟩],
`[apply HImp]

But if I write:

def Q3 {α : Type} [discrete_linear_ordered_field α]: α → Prop :=
λ x, x = x + 1

example (x : ℝ*) :
  (Q3 x ↔ {n : ℕ | Q3 ((quotient.out' x) n)} ∈ (@hyperfilter ℕ).sets) →
  (¬ Q3 x ↔ {n : ℕ | ¬ Q3 ((quotient.out' x) n)} ∈ (@hyperfilter ℕ).sets) :=
begin
intro,
@trans_not x Q3,
end

It tells me at the second-last line it can't synthesise the placeholder Type ? -- what placeholder does it need to synthesise? trans_not just needs a real number and a proposition, not a type.

[Kenny Lau]

looks like you're reaching another level of enlightenment! :P

[Kenny Lau]

what happens if you do it manually, i.e. substitute the content of your tactic?

[Chris Hughes]

It won't be an argument to trans_not, it will be something wrong inside trans_not

[Abhimanyu Pallavi Sudhir]

what happens if you do it manually, i.e. substitute the content of your tactic?

It works when I do that:

example (x : ℝ*) :
  (Q3 x ↔ {n : ℕ | Q3 ((quotient.out' x) n)} ∈ (@hyperfilter ℕ).sets) →
  (¬ Q3 x ↔ {n : ℕ | ¬ Q3 ((quotient.out' x) n)} ∈ (@hyperfilter ℕ).sets) :=
begin
intro,
have HImp : (Q3 x ↔ {n : ℕ | Q3 ((quotient.out' x) n)} ∈ (@hyperfilter ℕ).sets)
    → (¬ Q3 x ↔ {n : ℕ | ¬ Q3 ((quotient.out' x) n)} ∈ (@hyperfilter ℕ).sets) :=
  λ Hψ, ⟨ λ HnQ, (ultrafilter_iff_compl_mem_iff_not_mem.mp U _).mpr (not_imp_not.mpr Hψ.2 HnQ),
  λ HnSQ, not_imp_not.mpr Hψ.1 ((ultrafilter_iff_compl_mem_iff_not_mem.mp U _).mp HnSQ) ⟩,
  apply HImp,
  exact a,
end

no goals

[Abhimanyu Pallavi Sudhir]

Perhaps there's an issue with the type of P?

[Mario Carneiro]

The type of trans_not does not make any sense

[Mario Carneiro]

it's mixing meta levels

[Mario Carneiro]

I think it might work if you just take x and P out