## Stream: general

### Topic: Dealing with heq and Sigma types

#### Patrick Lutz (Nov 11 2020 at 19:49):

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 (Nov 11 2020 at 19:58):

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 }


ohh, nice

#### Patrick Lutz (Nov 11 2020 at 20:03):

what exactly does subst do?

#### Kevin Buzzard (Nov 11 2020 at 20:03):

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

#### Kevin Buzzard (Nov 11 2020 at 20:04):

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 (Nov 11 2020 at 20:04):

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

#### Bryan Gin-ge Chen (Nov 11 2020 at 20:04):

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

#### Kevin Buzzard (Nov 11 2020 at 20:04):

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

oh, I see

#### Patrick Lutz (Nov 11 2020 at 20:05):

Kevin Buzzard said:

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

#### Reid Barton (Nov 11 2020 at 20:07):

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

#### Reid Barton (Nov 11 2020 at 20:08):

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

#### Reid Barton (Nov 11 2020 at 20:08):

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

#### Patrick Lutz (Nov 11 2020 at 20:09):

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

#### Yaël Dillies (Nov 29 2021 at 14:11):

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


#### Reid Barton (Nov 29 2021 at 14:35):

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 (Nov 29 2021 at 14:38):

Maybe docs#sigma.eq can help?

#### Reid Barton (Nov 29 2021 at 14:46):

btw docs#psigma.lex is the same right?

#### Yaël Dillies (Nov 29 2021 at 14:46):

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

#### David Wärn (Nov 29 2021 at 14:47):

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 (Nov 29 2021 at 15:00):

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 (Nov 29 2021 at 15:03):

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 (Nov 29 2021 at 15:20):

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)

Last updated: Aug 03 2023 at 10:10 UTC