## § Inductive Predicate as Least Fixed Point, directly

inductive IsEven : Nat → Prop
| zero : IsEven 0
| succ : ∀ n, IsEven n → IsEven (n + 2)

def IsEvenProp (p : Nat → Prop) : Prop :=
p 0 ∧ (∀ n, p n → p (n + 2))

theorem IsEvenPropOfIsEven : IsEvenProp IsEven := by
unfold IsEvenProp
constructor
· exact IsEven.zero
· intro n h
exact IsEven.succ n h

/--
least fixed point of IsEvenProp.
See that this uses impredicativity.
It is quantifying over all (p : Nat → Prop).
In doing so, it is quantifying over *itself* (IsEven' : Nat → Prop).
-/
def IsEven' : Nat → Prop := fun n =>
∀ (p : Nat → Prop) (hp : IsEvenProp p), p n

theorem IsEven'_zero : IsEven' 0 := by
intro p hp
unfold IsEvenProp at hp
obtain ⟨h0, _hsucc⟩ := hp
exact h0

theorem IsEven'_ind (h : IsEven' n) : IsEven' (n + 2) := by
intro p hp
unfold IsEvenProp at hp
obtain ⟨h0, hsucc⟩ := hp
apply hsucc
unfold IsEven' at h
apply h
unfold IsEvenProp
simp only
constructor <;> assumption

theorem IsEvenOfIsEven' : ∀ n, IsEven' n → IsEven n := by
unfold IsEven'
intros n
intros h
specialize h IsEven IsEvenPropOfIsEven
exact h

theorem IsEven'OfIsEven : ∀ n, IsEven n → IsEven' n := by
intro n
intros h
induction h
case zero => exact IsEven'_zero
case succ m heven heven' =>
exact IsEven'_ind heven'

theorem IsEven_eq_IsEven' : ∀ n, IsEven n ↔ IsEven' n := by
intro n
apply Iff.intro
· apply IsEven'OfIsEven
· apply IsEvenOfIsEven'