How to manipulate proofs that involve Sigma types

Stream: new members

[kroton]

Hello,
I got stuck in the middle of a proof when I encountered the following situation.
I tried using grind, which improved things, but is it possible to resolve this manually?

example {I : Type*} {β : I → Type*} {S : (i : I) → Set (β i)}
  (f : (i : I) → Σ i, β i)
  (h1 : ∀ i, (f i).fst = i)
  (h2 : ∀ i, (f i).snd ∈ S (f i).fst)
: ∀ i, (h1 i) ▸ (f i).snd ∈ S i := by
  grind

[Eric Wieser]

intro i; specialize h1 i; specialize h2 i; cases h1; exact h2?

[kroton]

@Eric Wieser
Thanks for your reply.
However, in my environment, it failed with the following error.

dependent elimination failed, failed to solve equation
  i = (f i).fst

[Eric Wieser]

My mental Lean environment has some bugs

[Eric Wieser]

You'll need to generalize h : f i =fi at * first or similar

[suhr]

Played with it a little:

import Mathlib

example {I : Type*} {β : I → Type*} {S : (i : I) → Set (β i)}
  (f : (i : I) → Σ i, β i)
  (h1 : ∀ i, (f i).fst = i)
  (h2 : ∀ i, (f i).snd ∈ S (f i).fst)
: ∀ i, (h1 i) ▸ (f i).snd ∈ S i := by
  intro i
  suffices h: (h3: (f i).fst = i) → (h4: (f i).snd ∈ S (f i).fst) → h3 ▸ (f i).snd ∈ S i
  from (h (h1 i) (h2 i))
  refine (f i).recOn ?_
  dsimp
  intro j h1 h2 h3
  sorry

The Σ type is not a problem, but an ▸ is.

[kroton]

@Eric Wieser
generalize also failed with a different error in my environment .

tactic 'generalize' failed, result is not type correct
  ∀ (fi : (i : I) × β i), ⋯ ▸ fi.snd ∈ S i

[suhr]

By the way, you can just look at the proof generated by grind:

import Mathlib

def foo {I : Type*} {β : I → Type*} {S : (i : I) → Set (β i)}
  (f : (i : I) → Σ i, β i)
  (h1 : ∀ i, (f i).fst = i)
  (h2 : ∀ i, (f i).snd ∈ S (f i).fst)
: ∀ i, (h1 i) ▸ (f i).snd ∈ S i := by grind

#print foo
#print foo._proof_1

It's weird but short, so could be refactored into something readable.

[kroton]

@suhr
Thanks for your reply.
I didn’t know that it was possible to see the result of grind—thank you!

[kroton]

I tried checking what grind does, but just copy-pasting it doesn’t seem to work.
I asked ChatGPT too, but didn’t get anything useful. Hmm...

theorem foo._proof_3.{u_1, u_2} : ∀ {I : Type u_2} {β : I → Type u_1} {S : (i : I) → Set (β i)} (f : I → (i : I) × β i)
  (h1 : ∀ (i : I), (f i).fst = i), (∀ (i : I), (f i).snd ∈ S (f i).fst) → ∀ (i : I), h1 i ▸ (f i).snd ∈ S i :=
fun {I} {β} {S} f h1 h2 i ↦
  Classical.byContradiction fun h ↦
    Eq.mp
      (Eq.trans
        (Eq.trans (Eq.symm (eq_true (Eq.mp (Eq.refl ((f i).snd ∈ S (f i).fst)) (h2 i))))
          (eq_of_heq
            (Membership.mem.hcongr_5 (β (f i).fst) (β i) (congrArg β (h1 i)) (Set (β (f i).fst)) (Set (β i))
              (congrArg (fun x ↦ Set (β x)) (h1 i)) Set.instMembership Set.instMembership
              (Set.instMembership.hcongr_1 (β (f i).fst) (β i) (congrArg β (h1 i))) (S (f i).fst) (S i)
              ((fun i i' e_1 ↦ e_1 ▸ HEq.refl (S i)) (f i).fst i (h1 i)) (f i).snd (‹(f i).fst = i› ▸ (f i).snd)
              (HEq.symm (Lean.Grind.eqRec_heq (f i).snd ‹(f i).fst = i›)))))
        (eq_false h))
      True.intro

[kroton]

The error occurs at the expression e₁ ▸ HEq.refl (S i) in the code above.

[Eric Wieser]

Note that instead of using #print after the proof, you can use show_term grind inside it

[suhr]

import Mathlib

theorem foobar.{u_1, u_2} : ∀ {I : Type u_2} {β : I → Type u_1} {S : (i : I) → Set (β i)} (f : I → (i : I) × β i)
  (h1 : ∀ (i : I), (f i).fst = i), (∀ (i : I), (f i).snd ∈ S (f i).fst) → ∀ (i : I), h1 i ▸ (f i).snd ∈ S i :=
fun {I} {β} {S} f h1 h2 i =>
  Classical.byContradiction fun h =>
    Eq.mp
      (Eq.trans
        (Eq.trans (Eq.symm (eq_true (Eq.mp (Eq.refl ((f i).snd ∈ S (f i).fst)) (h2 i))))
          (eq_of_heq
            (Membership.mem.hcongr_5 (β (f i).fst) (β i) (congrArg β (h1 i)) (Set (β (f i).fst)) (Set (β i))
              (congrArg (fun x => Set (β x)) (h1 i)) Set.instMembership Set.instMembership
              (Set.instMembership.hcongr_1 (β (f i).fst) (β i) (congrArg β (h1 i))) (S (f i).fst) (S i)
              ((fun i i' e_1 => @Eq.ndrec I i (fun i' => S i ≍ S i') (HEq.refl (S i)) i' e_1) (f i).fst i (h1 i)) (f i).snd (@Eq.rec I (f i).fst (fun x h => β x) (f i).snd i (h1 i))
              (HEq.symm (eqRec_heq (h1 i) (f i).snd)))))
        (eq_false h))
      True.intro

[suhr]

Obtained using clicking in the lean infoview and by apply?.

[kroton]

@Eric Wieser @suhr
Thank you for your response. I’ll do a bit more digging.

[Aaron Liu]

It's not that complicated and you can just do it manually

import Mathlib

example {I : Type*} {β : I → Type*} {S : (i : I) → Set (β i)}
    (f : (i : I) → Σ i, β i)
    (h1 : ∀ i, (f i).fst = i)
    (h2 : ∀ i, (f i).snd ∈ S (f i).fst) :
    ∀ i, (h1 i) ▸ (f i).snd ∈ S i :=
  fun i => Eq.rec (motive := fun x h => h ▸ (f i).snd ∈ S x) (h2 i) (h1 i)

[suhr]

Beware of dependent type hell. Heterogeneous equality is famously poorly behaving in Lean. It would be wise to avoid it.

[Aaron Liu]

In general dependent rewriting is hard tedious but this case is simple so you get a relatively simple solution

[suhr]

Yeah. An elegant usage of Eq.rec by the way, you rarely see the second argument being used.

[kroton]

@Aaron Liu Wow, thanks for the simple solution!