Error on induction tactic: failed to infer implicit target

Stream: new members

[Dylan Lapeyre]

Hi, I'm building set theory using the ZF axioms, and have built the Von Neumann natural numbers (ω₀ : MySet). I would like to be able to use the induction tactic with this, but am running into an issue. A MWE is below:

import Mathlib

suppress_compilation
namespace MWE

axiom MySet : Type

axiom Mem (x y : MySet) : Prop

instance : Membership MySet MySet where
  mem := Mem

-- empty set
axiom empty : MySet

instance : EmptyCollection MySet where
  emptyCollection := empty


-- ZF3: changed to iff
axiom pairing_axiom (x y: MySet) : ∃ z : MySet, ∀ w : MySet, w ∈ z ↔ (w = x) ∨ (w = y)

def pairing (x y : MySet) : MySet := (pairing_axiom x y).choose

instance : Singleton MySet MySet where
  singleton x := pairing x x

-- ZF4 union: for any set A, there is a set B = ⋃ A (= ⋃ {z : z ∈ A})
axiom union_axiom (A : MySet) : ∃ B : MySet, ∀ x : MySet, x ∈ B ↔ (∃ z : MySet, z ∈ A ∧ x ∈ z)

def union (A : MySet) : MySet := (union_axiom A).choose

instance : Union MySet where
  union := λ x y => union (pairing x y)

axiom specification_axiom_scheme (A : MySet) (P : MySet → Prop) : ∃ B : MySet, ∀ x : MySet, x ∈ B ↔ (x ∈ A ∧ P x)

def specification (A : MySet) (P : MySet → Prop) : MySet := (specification_axiom_scheme A P).choose

def successor (x : MySet) : MySet := x ∪ {x}
postfix:max "†" => successor

def inductive_set (A : MySet) : Prop := (∅ : MySet) ∈ A ∧ (∀ x ∈ A, x† ∈ A)

axiom infinity_axiom : ∃  A : MySet, inductive_set A

-- equivalent to {x ∈ A | ∀ B : MySet, inductive_set B → x ∈ B}, where A is an inductive set
def naturals : MySet :=
  specification infinity_axiom.choose (λ x => ∀ B : MySet, inductive_set B → x ∈ B)

notation "ω₀" => naturals

theorem induction_on_naturals {P : MySet → Prop} (hempty : P ∅)
    (hsucc : ∀ k ∈ ω₀, P k → P k†) {n : MySet} (hn : n ∈ ω₀) : P n := sorry  -- not yet translated into lean, check it works first

example {n : MySet} (h : n ∈ ω₀) : n = n := by
  induction n using induction_on_naturals -- error here: failed to infer implicit target, it contains unresolved metavariables ?m.4905 (metavariable of type MySet)
  sorry

How can I resolve this issue? Thank you

[Joachim Breitner]

Try using induction_on_naturals (hn := h).

Hmm, although this might fix n…

Maybe use refine instead of induction.

[Dylan Lapeyre]

refine works, thank you!
But is there a way to be able to use the induction tactic? If not this solution is fine

[Eric Wieser]

This works:

@[elab_as_elim]
theorem induction_on_naturals {P : (s : MySet) → s ∈ ω₀ → Prop}
    (hempty : P ∅ sorry) (hsucc : ∀ k, ∀ h : k ∈ ω₀, P k h → P k† sorry)
    {n : MySet} (hn : n ∈ ω₀) : P n hn := sorry

example {n : MySet} (h : n ∈ ω₀) : n = n := by
  induction h using induction_on_naturals
  sorry

[Eric Wieser]

Note you now have two more sorries to fill in the statement.

[Dylan Lapeyre]

In the inductive step, I don't have access to the inductive hypotheses (they don't have names), is there a way of adding those in?

[Dylan Lapeyre]

Using refine with the new definition works (giving me the correct terms to prove and I can do intro to get the inductive hypotheses)

[Kevin Buzzard]

Dylan Lapeyre said:

In the inductive step, I don't have access to the inductive hypotheses (they don't have names), is there a way of adding those in?

For natural induction you can name the hypotheses like this:

import Mathlib

example (n : ℕ) : n = n := by
  induction n with
  | zero => sorry
  | succ n ih => sorry

so hopefully something like that works in your case too.

[Paul Rowe]

In fact, if you use induction_on_naturals defined above, I think you would use hempty and hsucc in place of zero and succ. If they need arguments you can name them as Kevin did above.