heq again

Stream: general

[Reid Barton]

Hmm, I wasn't expecting this to work.

lemma types_eq_of_heq : Π {α : Type} (a : α) {β : Type} (b : β) (h : a == b), α = β
| α a _ _ (heq.refl _) := rfl

[Kenny Lau]

why not?

[Kenny Lau]

casing on h makes sure that the types are equal and the arguments are equal

[Reid Barton]

Mostly because I haven't seen this fact in core or mathlib, so I guess I assumed it was not provable.

[Reid Barton]

Now I have a followup question about congr.

[Reid Barton]

import data.set

section
parameters {F : Type → Type} {α β α' β' : Type} (hα : F α = F α') (hβ : F β = F β')
parameters (f : F α → F β) (f' : F α' → F β') (h : f == f')
include hα hβ h

def fns := Σ' X Y : set.range F, X.1 → Y.1
def g : fns := ⟨⟨F α, α, rfl⟩, ⟨F β, β, rfl⟩, f⟩
def g' : fns := ⟨⟨F α', α', rfl⟩, ⟨F β', β', rfl⟩, f'⟩

def e : g = g' :=
begin
  dsimp [g, g'],
  /- ⊢ ⟨⟨F α, _⟩, ⟨⟨F β, _⟩, f⟩⟩ = ⟨⟨F α', _⟩, ⟨⟨F β', _⟩, f'⟩⟩ -/
  /- How to proceed? My solution: -/
  congr' 1, { simp [hα] },
  congr' 1, { rw hα }, { simp [hβ] },
  simp [h],
end

end

[Kenny Lau]

are you going to livestream?

[Mario Carneiro]

type_eq_of_heq

[Reid Barton]

I'm annoyed about this { rw hα } thing. The goal there is

⊢ (λ (Y : {x // x ∈ set.range F}), F α → Y.val) = λ (Y : {x // x ∈ set.range F}), F α' → Y.val

which I think is trying to say that when I do the second congr', the types of the two sides are equal.

[Reid Barton]

Wow, my grep skills failed

[Reid Barton]

If I put { admit } there, the rest of the proof seems to go through fine. So couldn't congr' deduce that the types are equal after the fact, using type_eq_of_heq?

[Reid Barton]

Here's a dumber example.

example {α β : Type} (a : α) (b : β) : (a, a) == (b, b) :=
begin
  congr,
end

There are four goals, ⊢ α = β twice and ⊢ a == b twice. But I can get the former from the latter.

[Reid Barton]

Or a nicer presentation

example {α α' β β' : Type} (a : α) (b : β) (a' : α') (b' : β') : (a, b) == (a', b') :=

[Kenny Lau]

import data.set

section
parameters {F : Type → Type} {α β α' β' : Type} (hα : F α = F α') (hβ : F β = F β')
parameters (f : F α → F β) (f' : F α' → F β') (h : f == f')
include hα hβ h

def fns := Σ' X Y : set.range F, X.1 → Y.1
def g : fns := ⟨⟨F α, α, rfl⟩, ⟨F β, β, rfl⟩, f⟩
def g' : fns := ⟨⟨F α', α', rfl⟩, ⟨F β', β', rfl⟩, f'⟩

def e : g = g' :=
begin
  dsimp only [g, g'],
  congr; try {assumption},
  ext Y, rw hα
end

end

[Reid Barton]

The ext Y, rw hα part is still there, though. That's the only part I care about because it seems unnecessary.
In my real use case, I have three of them and they are bigger

[Reid Barton]

Does set_option trace.congr_lemma true do anything?

[Reid Barton]

Kenny, I was thinking I would try this evening US eastern time today, maybe a bit late for you

[Mario Carneiro]

That's a pretty messy goal. I would clean it up by hand as follows:

begin
  let G := λ A B (f : A → B) h h', (⟨⟨A, h⟩, ⟨B, h'⟩, f⟩ : fns),
  suffices : ∀ {f f' h₁ h₂ h₃ h₄}, f == f' →
    G (F α) (F β) f h₁ h₂ = G (F α') (F β') f' h₃ h₄, exact this h,
  rw [hα, hβ], intros, congr', apply eq_of_heq a
end

[Mario Carneiro]

I would avoid having type equalities and heqs in the hypotheses to begin with

[Mario Carneiro]

congr is clearly dropping the ball here. There are lots of superfluous goals being generated

[Mario Carneiro]

But usually you don't want to deduce a type equality from a heq; rather you want to assume the type equality and prove a regular equality dependent on it

[Kenny Lau]

is there any way to prove this goal?

[Kenny Lau]

import data.set

section
parameters {F : Type → Type} {α β α' β' : Type} (hα : F α = F α') (hβ : F β = F β')
parameters (f : F α → F β) (f' : F α' → F β') (h : f == f')
include hα hβ h

def fns := Σ' X Y : set.range F, X.1 → Y.1
def g : fns := ⟨⟨F α, α, rfl⟩, ⟨F β, β, rfl⟩, f⟩
def g' : fns := ⟨⟨F α', α', rfl⟩, ⟨F β', β', rfl⟩, f'⟩

set_option pp.proofs true
theorem e : g = g' :=
begin
  fapply psigma.eq,
  { exact subtype.eq hα },
  fapply psigma.eq,
  { /- (eq.rec_on (subtype.eq hα) (g.snd)).fst = (g'.snd).fst -/ }
end

end

[Reid Barton]

Well how about the following modification to congr. After each single layer of congr, try filling each of the new goals by applying exact type_eq_of_heq ?m_i where ?m_i is the metavariable of each other goal.

[Mario Carneiro]

That's not what you want though. You will have to deduce those type equalities anyway in order to prove the heq

[Reid Barton]

But I didn't!

[Reid Barton]

I happen to have the heq lying around, and where I proved it, the type equalities were obvious

[Mario Carneiro]

You satisfied the type equality proof by assumption

[Reid Barton]

Which type equality proof?

[Mario Carneiro]

hα

[Mario Carneiro]

and hβ later in the proof

[Reid Barton]

Right, but then there is an inner proof obligation I have to take care of, the one I solve using { rw hα }

[Reid Barton]

Let me put up my real code

[Mario Carneiro]

you have to solve that anyway

[Reid Barton]

No, it follows from being able to solve the rest of the goals

[Mario Carneiro]

how?

[Reid Barton]

By type_eq_of_heq. Right?

[Mario Carneiro]

applied to what?

[Reid Barton]

Isn't it the same thing as this?

example {α α' β β' : Type} (a : α) (b : β) (a' : α') (b' : β') (ha : a == a') (hb : b == b') :
  (a, b) == (a', b') :=
begin
  congr, { exact type_eq_of_heq ha }, { exact type_eq_of_heq hb }, { exact ha }, { exact hb }
end

[Mario Carneiro]

sure, but this is an unrealistic goal. Where are you going to get those heqs without a type equality?

[Reid Barton]

so in my real code it happens here https://gist.github.com/rwbarton/dfb90b2552f09b51798bb52af9948d48#file-filtered-lean-L249

[Reid Barton]

S is the image of a functor F : I -> C considered as a subgraph, defined here https://gist.github.com/rwbarton/dfb90b2552f09b51798bb52af9948d48#file-filtered-lean-L87

[Mario Carneiro]

can you MWE the state just before the rintro?

[Mario Carneiro]

or maybe just after

[Reid Barton]

It should be more or less what I pasted originally.
Note hg : functor.map F ((⟨i', ⟨j', g⟩⟩.snd).snd) == f, which came from the definition of S

[Reid Barton]

Corresponding to my original (h : f == f')

[Mario Carneiro]

I want to catch the state before the type equalities enter the context

[Reid Barton]

Ah, so you mean hi', hj'

[Mario Carneiro]

ideally you should be able to match on hi', hj', hg and save all the mess

[Mario Carneiro]

don't match on ⟨X, i, rfl⟩, ⟨Y, j, rfl⟩, just do ⟨X, _⟩, ⟨Y, _⟩

[Reid Barton]

Hmm, I will try that

[Reid Barton]

Meanwhile I updated the gist with a version which is not M, but should be a WE

[Reid Barton]

Oh, there is a trick in F ijg.1 = X ∧ F ijg.2.1 = Y ∧ .... That is not just X, but X.val

[Reid Barton]

because of my representation of a subgraph, which I now infinitely regret

[Reid Barton]

I have a subgraph as (1) a subset of the vertices, (2) for each pair of vertices in that set (as a subtype), a subset of the edges between them

[Mario Carneiro]

works for me:

    rintro ⟨⟨X, _⟩, ⟨Y, _⟩, ⟨f, ⟨i, j, g⟩, ⟨⟩, ⟨⟩, ⟨⟩⟩⟩,
    exact ⟨⟨i, j, g⟩, rfl⟩,

[Mario Carneiro]

using rfl instead of ⟨⟩ calls subst instead of cases, and subst is not sufficiently aggressive wrt definitionally unfolding one side to a variable

[Reid Barton]

Ahh

[Mario Carneiro]

I would suggest, if you are okay with the added verbosity, that you use an inductive type to define your hom sets instead of ands of eqs and heqs

[Reid Barton]

I see

rfl : ⇑F (⟨i', ⟨j', g⟩⟩.fst) = ↑⟨X, b_fst_property⟩,

[Mario Carneiro]

it names the variable rfl before substing, I think

[Reid Barton]

Looks that way.

[Reid Barton]

that's a whole lot better, thanks!

[Reid Barton]

You mean, in the definition of S?

[Mario Carneiro]

yes

[Mario Carneiro]

it's up to you, you can use tricks like this to match on it either way

[Reid Barton]

oh, I could replace the whole λ X Y, {f | ∃ (ijg : Σ (i j : I), i ⟶ j), F ijg.1 = X ∧ F ijg.2.1 = Y ∧ F.map ijg.2.2 == f} with an inductive type I guess

[Mario Carneiro]

right

[Mario Carneiro]

it would give nicer equations, but if this is a one-off it's probably not worth it

[Reid Barton]

and elsewhere I have similar constructions, like the union of a family of subgraphs

[Reid Barton]

Yeah, I'm not sure I will need any of these constructions more than once, inside the associated proof

[Reid Barton]

But a good technique to keep in mind

[Mario Carneiro]

oh, looks like you don't even need to match on ijg in that proof

[Reid Barton]

Yep

[Reid Barton]

I think I know what happened here

[Reid Barton]

I started without the F ijg.1 = X ∧ F ijg.2.1 = Y ∧ part

[Reid Barton]

in the definition of S. And then I realized that wasn't going to work

[Reid Barton]

but I think I had already written the ⟨X, i, rfl⟩, ⟨Y, j, rfl⟩ patterns

[Mario Carneiro]

yeah, of course you can't deduce X = X' and Y = Y' from X ⟶ Y = X' ⟶ Y'

[Mario Carneiro]

not for function types and definitely not for homsets

[Reid Barton]

Although it curiously would not even matter for the cardinality estimate I need to do here, because it would blow things up by a factor of less than $\kappa$

[Reid Barton]

But anyways, that's when I started to wonder: would it be better to just define the edges as (mors : set (Σ X Y, X ⟶ Y))

[Mario Carneiro]

I'm inclined to say no, although possibly you might want homs to be defined on all objects, not just those in the subset

[Mario Carneiro]

and just require that it be empty outside the subset

[Mario Carneiro]

structure subgraph (C : Type u) [small_category C] : Type u :=
(objs : set C)
(homs : Π X Y : C, set (X ⟶ Y))
(dom_mem : Π X Y f, f ∈ homs X Y → X ∈ objs)
(cod_mem : Π X Y f, f ∈ homs X Y → Y ∈ objs)

[Reid Barton]

Right, I would need those last two fields anyways. Just a difference between set (Σ X Y, X ⟶ Y) and Π X Y : C, set (X ⟶ Y)

[Mario Carneiro]

having a big sigma will make things more complicated with heqs and stuff as you've seen

[Reid Barton]

Given that some of the things I do are look at the cardinality of the set of edges, and form the union of subgraphs

[Reid Barton]

but I guess those are not significantly harder with the Pi approach

[Mario Carneiro]

I think arrows := Σ X Y, X ⟶ Y is a useful definition in a category though