interface for dite

Stream: general

[Kenny Lau]

noncomputable def succ (C : set (set α)) : set (set α) :=
if H : ∃ A, A ∈ (hat S C) \ C then insert (classical.some H) C else C

@[elab_as_eliminator] noncomputable def succ.rec {C : set (set α) → set (set α) → Sort*}
  (H1 : ∀ t, ∀ A ∈ (hat S t) \ t, C t (insert (classical.some (⟨A, H⟩ : ∃ A, A ∈ (hat S t) \ t)) t))
  (H2 : ∀ t, (∀ A ∈ (hat S t) \ t, false) → C t t)
  (t : set (set α)) : C t (succ S t) :=
if H : ∃ A, A ∈ (hat S t) \ t then
  have succ S t = insert (classical.some H) t, from dif_pos H,
  eq.drec_on this.symm $ H1 _ (classical.some H) (classical.some_spec H)
else
  have succ S t = t, from dif_neg H,
  eq.drec_on this.symm $ H2 t $ λ A h, H ⟨A, h⟩

@[elab_as_eliminator] noncomputable def succ.rec_on {C : set (set α) → set (set α) → Sort*}
  (t : set (set α))
  (H1 : ∀ t, ∀ A ∈ (hat S t) \ t, C t (insert (classical.some (⟨A, H⟩ : ∃ A, A ∈ (hat S t) \ t)) t))
  (H2 : ∀ t, (∀ A ∈ (hat S t) \ t, false) → C t t) :
  C t (succ S t) :=
succ.rec S H1 H2 t

theorem succ.subset (C : set (set α)) : C ⊆ succ S C :=
succ.rec_on S C
  (λ t A H, show t ⊆ insert (classical.some _) t, from λ z, or.inr)
  (λ t H z, id)

[Kenny Lau]

noncomputable def succ (C : set (set α)) : set (set α) :=
if H : ∃ A, A ∈ (hat S C) \ C then insert (classical.some H) C else C

@[elab_as_eliminator] noncomputable def succ.rec {C : set (set α) → set (set α) → Sort*}
  (H1 : ∀ t, ∀ A ∈ (hat S t) \ t, C t (insert A t))
  (H2 : ∀ t, (∀ A ∈ (hat S t) \ t, false) → C t t)
  (t : set (set α)) : C t (succ S t) :=
if H : ∃ A, A ∈ (hat S t) \ t then
  have succ S t = insert (classical.some H) t, from dif_pos H,
  eq.drec_on this.symm $ H1 _ (classical.some H) (classical.some_spec H)
else
  have succ S t = t, from dif_neg H,
  eq.drec_on this.symm $ H2 t $ λ A h, H ⟨A, h⟩

@[elab_as_eliminator] noncomputable def succ.rec_on {C : set (set α) → set (set α) → Sort*}
  (t : set (set α))
  (H1 : ∀ t, ∀ A ∈ (hat S t) \ t, C t (insert A t))
  (H2 : ∀ t, (∀ A ∈ (hat S t) \ t, false) → C t t) :
  C t (succ S t) :=
succ.rec S H1 H2 t

theorem succ.subset (C : set (set α)) : C ⊆ succ S C :=
succ.rec_on S C
  (λ t A H, show t ⊆ insert A t, from λ z, or.inr)
  (λ t H z, id)

[Kenny Lau]

which one is better?

[Kenny Lau]

why does elaborator fail for this one?

type mismatch, term
  succ.rec_on S C ?m_2 ?m_3
has type
  ?m_1 C (succ S C) : Sort ?
but is expected to have type
  is_chain C → is_chain (succ S C) : Prop

[Kevin Buzzard]

dite stinks and I would strongly encourage you to work on this until it stinks less.

[Kevin Buzzard]

dite is such a normal thing coming from procedural languages

[Kevin Buzzard]

and it's so hard to eliminate

[Kenny Lau]

I did write an interface

[Kevin Buzzard]

I know

[Kenny Lau]

but the elaborator fails lol