# Zulip Chat Archive

## 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 `heq`

s 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 }
```

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

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.

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

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.

why is this bad?

#### 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