logic.equiv.basic

Stream: mathlib4

[Scott Morrison]

77tigers (sorry, I don't know their zulip usernames --- @Kevin Buzzard?) started the port of Logic.Equiv.Basic in mathlib4#631.

I feel this one is on the critical path to porting many other things, so I hope it is okay with the OP if others join in to get it done asap.

[Scott Morrison]

I've just gone ahead and finished renaming and aligning the file.

[Scott Morrison]

However there are many broken proofs still, for mostly independent reasons, so it should be fine if anyone wants to jump in and just fix as many as they have inclination to do.

[Scott Morrison]

Probably best not to sit on changes, however: if you fix a few proofs, push your commit. :-)

[Scott Morrison]

In that logic.equiv.basic we have the slightly esoteric (and only used in Chevalley-Warning)

/-- The type of all functions `X → Y` with prescribed values for all `x' ≠ x`
is equivalent to the codomain `Y`. -/
def subtypeEquivCodomain (f : { x' // x' ≠ x } → Y) : { g : X → Y // g ∘ coe = f } ≃ Y := ...

but of course coe doesn't mean anything now. I'm guessing the closest replacement for this theorem will be:

def subtypeEquivCodomain (f : { x' // x' ≠ x } → Y) : { g : X → Y // (fun x : { x' // x' ≠ x }  => g x) = f } ≃ Y :=

Any other suggestions?

[Mario Carneiro]

For specific types where we can find a Coe instance, you should replace occurrences of coe with (↑) (defined in Mathlib.Tactic.Coe) or (·)

[Scott Morrison]

I can't get (↑) or (·) to work here, as without a type annotation on the left-hand-side (i.e. g ∘ (·)) they just seem to default to the identity, and then we get a type error on the f.

[Scott Morrison]

Hence writing (fun x : { x' // x' ≠ x } => g x) = f.

[Mario Carneiro]

I'm getting a bad error:

instance (p : α → Prop) : Coe (Subtype p) α := ⟨Subtype.val⟩

def subtypeEquivCodomain {X : Type u} {Y : Type v} (x : X) (f : { x' // x' ≠ x } → Y) :
  { g : X → Y // (g ∘ (·)) = f } ≃ Y := sorry

-- failed to synthesize
--   CoeHTCT ({ x' // x' ≠ x } → Y) (X → Y)
-- (deterministic) timeout at 'typeclass', maximum number of heartbeats (20000) has been reached (use 'set_option synthInstance.maxHeartbeats <num>' to set the limit)

[Mario Carneiro]

which indicates that there is a bad instance somewhere causing a loop

[Mario Carneiro]

oh, actually it's probably the subtype coe I had to add to make this compile

[Mario Carneiro]

Using Subtype.val works, of course

[Mario Carneiro]

also by exact (·)

[Scott Morrison]

So is it better to have Subtype.val in the statement, or what I wrote?

[Mario Carneiro]

I think this is a bug report

[Gabriel Ebner]

That (↑) doesn't work here is a bug. Give me a sec.

[Scott Morrison]

A separate logic.equiv.basic question, I seem to be encountering a failure of beta reduction in the following:

structure Equiv (α : Sort _) (β : Sort _) where
  toFun : α → β
  invFun : β → α
  left_inv : ∀ x, invFun (toFun x) = x

infixl:25 " ≃ " => Equiv

/-- A product of types can be split as the binary product of one of the types and the product
  of all the remaining types. -/
def piSplitAt {α : Type _} [DecidableEq α] (i : α) (β : α → Type _) :
    (∀ j, β j) ≃ β i × ∀ j : { j // j ≠ i }, β j where
  toFun f := ⟨f i, fun j => f j⟩
  invFun f j := if h : j = i then h.symm.rec f.1 else f.2 ⟨j, h⟩
  left_inv f := by
    apply funext
    intro x
    /- Goal is now:
    ```
    (fun f j => if h : j = i then (_ : i = j) ▸ f.fst else Prod.snd f { val := j, property := h })
      ((fun f => (f i, fun j => f j.val)) f) x =
      f x
    ```
    -/
    dsimp only -- Does nothing
    -- Expected the goal to start with `if h : j = i ...`

Am I missing something, or is this a bug?

[Mario Carneiro]

I'm inclined to use Subtype.val (or something that expands to it, once we work that out) to ensure it is still written in first-order style with explicit composition

[Mario Carneiro]

that also looks like a bug

[Gabriel Ebner]

https://github.com/leanprover-community/mathlib4/pull/652

[Scott Morrison]

Reported the beta reduction issue as lean4#1856.

[Scott Morrison]

In logic.equiv.basic we have the somewhat tricky statement pi_congr_left', which translates to:

import Mathlib.Logic.Equiv.Defs

namespace Equiv

def piCongrLeft' (P : α → Sort _) (e : α ≃ β) : (∀ a, P a) ≃ ∀ b, P (e.symm b) where
  toFun f x := f (e.symm x)
  invFun f x := by
    rw [← e.symm_apply_apply x]
    exact f (e x)
  left_inv f :=
    funext fun x =>
      eq_of_heq
        ((eq_rec_heq _ _).trans
          (by
            dsimp
            rw [e.symm_apply_apply]))    -- fails, but the goal was already bad: `HEq ?m.205 ?m.206`
  right_inv f := funext fun x => eq_of_heq ((eq_rec_heq _ _).trans (by rw [e.apply_symm_apply]))    -- fails similarly
#align equiv.Pi_congr_left' Equiv.piCongrLeft'

However this proof isn't working. When I try to do it step by step I can't get the eq_rec_heqs to unify. Can anyone work out a new proof here?

[Scott Morrison]

Ah, got it. I found the old thread form 2020 when we first put this in mathlib, where Mario offered some alternative proofs, and one of those translates just fine.

[Matthew Ballard]

I've run into another situation where dsimp doesn't beta-reduce. Let me do a sanity check and report back.