Dealing with heq and Sigma types

Stream: general

[Patrick Lutz]

When proving that some type is equivalent to a Sigma type, how do you deal with heqs that pop up? Here's an example

import tactic

variables (A B : Type) (S : set A)

example : (A → B) ≃ Σ (f : S → B), {φ : A → B // ∀ (s : A) (h : s ∈ S), φ s = f ⟨s, h⟩ } :=
{ to_fun := λ g, ⟨λ s, g s.1, ⟨g, λ _ _, rfl⟩⟩,
  inv_fun := λ ⟨f, φ⟩, φ.1,
  left_inv := λ _, rfl,
  right_inv := begin
    rintros ⟨f, φ, h⟩,
    ext,
    { cases x, dsimp only, tauto },
    { -- heq occurs here
      sorry, }
  end }

How should the final sorry be proved? By the way, this example is by Kevin Buzzard. The actual, more complicated, situation that inspired this is here if you're curious.

[Reid Barton]

Turn back and go another way

example : (A → B) ≃ Σ (f : S → B), {φ : A → B // ∀ (s : A) (h : s ∈ S), φ s = f ⟨s, h⟩ } :=
{ to_fun := λ g, ⟨λ s, g s.1, ⟨g, λ _ _, rfl⟩⟩,
  inv_fun := λ p, p.2.1,
  left_inv := λ _, rfl,
  right_inv := begin
    rintros ⟨f, φ, h⟩,
    have : f = λ s, φ s.1, sorry,
    subst this,
  end }

[Patrick Lutz]

ohh, nice

[Patrick Lutz]

what exactly does subst do?

[Kevin Buzzard]

(note that Reid changed inv_fun -- λ ⟨f, φ⟩ is not good style when defining data, as you are here.

[Kevin Buzzard]

subst takes a proof of A = B and replaces all the A's everywhere by B's, or possibly the other way around

[Reid Barton]

oh yeah, I did that just in case it would help and then forgot to mention it

[Bryan Gin-ge Chen]

(Reid's sorry can be filled with simp [h].)

[Kevin Buzzard]

it's like rw h at * except that it's more powerful because it rewrites under binders. It literally removes A from the picture.

[Patrick Lutz]

oh, I see

[Patrick Lutz]

Kevin Buzzard said:

(note that Reid changed inv_fun -- λ ⟨f, φ⟩ is not good style when defining data, as you are here.

why is this bad?

[Reid Barton]

If you look at the goal in the original right_inv it's got some _match_1 or whatever junk in it

[Reid Barton]

more importantly, the version which matches in the lambda is less likely to reduce when applied to something

[Reid Barton]

though maybe in a case as simple as this one it doesn't really matter, not sure

[Patrick Lutz]

by the way, even though the example was originally by Kevin, I was the one who introduced the angle brackets

[Yaël Dillies]

A very similar question. I'm trying to construct the decidability instance of the lexicographical order on a sigma type:

variables {ι : Type*} {α : ι → Type*}

inductive sigma.lex [has_lt ι] [Π i, has_le (α i)] : Π a b : Σ i, α i, Prop
| fiber (i : ι) (a b : α i) : a ≤ b → sigma.lex ⟨i, a⟩ ⟨i, b⟩
| base (i j: ι) (a : α i) (b : α j) : i < j → sigma.lex ⟨i, a⟩ ⟨j, b⟩

def sigma.lex.decidable_le [has_lt ι] [Π i, has_le (α i)] [hι : decidable_eq ι]
  [hι' : decidable_rel ((<) : ι → ι → Prop)]
  [hα : Π i, decidable_rel ((≤) : α i → α i → Prop)] :
  decidable_rel (sigma.lex : (Σ i, α i) → (Σ i, α i) → Prop) :=
λ a b, match hι a.1 b.1 with
  | is_true hij := begin
    refine match hα _ a.2 b.2 with
    | is_true hab := is_true begin
      convert sigma.lex.fiber j a b hab, -- Heeelp
      sorry-- refine rec_heq_of_heq _ _,
    end
    | is_false hab := is_false sorry
  end
  end
  | is_false h := sorry
end

Also see https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there.20code.20for.20X.3F/topic/Order.20on.20.CE.B1.20.E2.8A.95.20.CE.B2

[Reid Barton]

Doing cases on a and b would certainly help but you still need to subst hij as well and I don't know how to do it in term mode. Probably easier to write a careful tactic-mode definition...

[Yaël Dillies]

Maybe docs#sigma.eq can help?

[Reid Barton]

btw docs#psigma.lex is the same right?

[Yaël Dillies]

Not quite, because it's taking arbitrary relations in.

[David Wärn]

I think we're just missing an iff lemma for the lexicographic order

import tactic.basic

variables {ι : Type*} {α : ι → Type*} [has_lt ι] [Π i, has_le (α i)]

inductive sigma.lex : Π a b : Σ i, α i, Prop
| fiber (i : ι) (a b : α i) : a ≤ b → sigma.lex ⟨i, a⟩ ⟨i, b⟩
| base (i j: ι) (a : α i) (b : α j) : i < j → sigma.lex ⟨i, a⟩ ⟨j, b⟩

lemma le_iff (p q : Σ i, α i) :
  sigma.lex p q ↔ p.1 < q.1 ∨ ∃ h : p.1 = q.1, h.rec p.2 ≤ q.2 :=
⟨ λ h, by { cases h with i a b ab i j a b ij, exact or.inr ⟨rfl, ab⟩, exact or.inl ij },
  by { cases p, cases q, dsimp only, rintro (h | ⟨rfl, h⟩),
    exact sigma.lex.base _ _ _ _ h, exact sigma.lex.fiber _ _ _ h } ⟩

def sigma.lex.decidable_le [hι : decidable_eq ι] [hι' : decidable_rel ((<) : ι → ι → Prop)]
  [hα : Π i, decidable_rel ((≤) : α i → α i → Prop)] :
  decidable_rel (sigma.lex : (Σ i, α i) → (Σ i, α i) → Prop) :=
λ p q, decidable_of_decidable_of_iff infer_instance (le_iff p q).symm

[Reid Barton]

Yaël Dillies said:

Not quite, because it's taking arbitrary relations in.

This is irrelevant, but on the other hand sigma and psigma are not the same.

[Reid Barton]

There's something a bit funny about this decidability instance (which I was realizing was also going to be an issue with using subst), namely that decidable_le for sigma.lex might not reduce to a constructor even if the inputs hι' and hα always do. I think this is intrinsic to the question though.

[David Wärn]

I think what happens is that if you try to decide (a, b) <= (x, y) where h : a = x holds propositionally but not judgementally, then this decidability instance will get stuck trying to compute h.rec b. Indeed this should be intrinsic to the question. You can get around it in the non-dependent case, but it would require another decidability instance (since docs#eq_rec_constant isn't proved by rfl)