Dependent congruence theorem?

Stream: general

[Rish Vaishnav]

Can this theorem be proven?

theorem congrDep
  (A : Type) (T : A → Type) (f g : (a : A) → T a) (x y : A)
  (hfg : f = g) (hxy : x = y) (hT : T x = T y) : f x = Eq.mpr hT (g y) := by
  sorry

(we don't need hT actually, I just included it for brevity). The closest thing I could find in the stdlib was congrFun, but that seems to imply that we need definitional equality between x and y. At first glance the cast on the RHS seems to get in the way of proving anything here, as you can't apply the (non-dependent) congr theorem since the application functions have different types.

If it's not possible to prove, would it be problematic (i.e. inconsistent) to add it as an axiom?

[Edward van de Meent]

apparently yes

import Init.Tactics
theorem congrDep
  (A : Type) (T : A → Type) (f g : (a : A) → T a) (x y : A)
  (hfg : f = g) (hxy : x = y) (hT : T x = T y) : f x = Eq.mpr hT (g y) := by
  subst hxy
  subst hfg
  rfl

[Edward van de Meent]

i.e. yes, it can be proven

[Edward van de Meent]

it's a trick i learnt in the last few weeks... when you'd like to rewrite in not only the goal but also the type of the goal, the subst tactic is your friend

[Rish Vaishnav]

Oh sweet, thanks a lot! I admit I kind of assumed it wasn't provable since it was a simple generalization of congrand couldn't find it in the stdlib, but thank you for showing me otherwise. I guess it's probably just something that is not actually needed very often.

[Edward van de Meent]

actually, i think it might be the case that the goal is typically written different? maybe you meant something like HEq (f x) (f y)? because in that case i think there might be better api... i'm not very familiar with this corner of lean, however, so my suggestions might not be the most helpful

[Damiano Testa]

Rish Vaishnav said:

If it's not possible to prove, would it be problematic (i.e. inconsistent) to add it as an axiom?

As a small generic advice, there is this little known axiom:

axiom: if you are not completely certain that adding an axiom is consistent, then adding the axiom will create inconsistencies.

[Rish Vaishnav]

I have another small related question, is it simple to prove this theorem, or do I need to use some injectivity principle?

universe u v
example {A : Type u} {U V : A → Type v}
  (hAUBV : ((a : A) → U a) = ((a : A) → V a))
  : U = V := by
  sorry

[Damiano Testa]

Is this true if U is List and V is Array?

[Damiano Testa]

It seems that hAUBV only asserts that U and V either both have or both do not have terms.

[Yaël Dillies]

This is independent of Lean's logic

[Rish Vaishnav]

Hmm, in that case wouldn't it be true because the hypothesis hAUBV is false? Like, you can't prove ((a : A) -> List a) = ((a : A) -> Array a)

[Yaël Dillies]

...but conversely hAUBV doesn't bring you any information

[Yaël Dillies]

It's not because something can't be proved that it is false

[Rish Vaishnav]

Yaël Dillies said:

This is independent of Lean's logic

Hmm okay, by that do you mean I can't expect to prove it? For context, I was trying to prove the theorem congrDepEq below:

universe u v
theorem congrDepEqAux {A : Type u} {U V : A → Type v}
  (hAUBV : ((a : A) → U a) = ((a : A) → V a))
  : U = V := by
  sorry

theorem congrDepEq {A B : Type u} {U : A → Type v} {V : B → Type v}
  (f : (a : A) → U a) (g : (b : B) → (V b)) (a : A) (b : B)
  (hAB : A = B) (hAUBV : ((a : A) → U a) = ((b : B) → V b)) (hUaVb : U a = V b)
  (hfg : f = Eq.mpr hAUBV g) (hab : a = Eq.mpr hAB b) : f a = Eq.mpr hUaVb (g b) := by
  subst hAB
  have this : U = V := congrDepEqAux hAUBV
  subst this
  subst hab
  subst hfg
  rfl

I guess I could include the hypothesis (hUV : U = Eq.mpr (congrArg (· → Type v) hAB) V), but would like to avoid doing so if possible.

[Yaël Dillies]

In Lean's logic, all you can deduce from hAUBV : (∀ a, U a) = (∀ b, V b) is that ∀ a, U a and ∀ b, V b have the same cardinality. That's it.

[Yaël Dillies]

In particular, f = Eq.mpr hAUBV g doesn't let you deduce anything

[Yaël Dillies]

Maybe A := Bool, B := Bool, U := fun _ ↦ Nat, V := fun _ ↦ Nat and Eq.mpr hAUBV is the permutation (Bool → Nat) ≃ (Bool → Nat) which sends f : Bool → Nat to fun b ↦ f (!b)

[Yaël Dillies]

Replacing Bool → Nat with Nat × Nat is possibly clearer: For all you know, Eq.mpr hAUBV could be the map fun (a, b) ↦ (b, a), which is not the identity

[Kyle Miller]

I simplified the theorem to congrDepEq', and I was only able to prove it by adding a Subsingleton assumption. When the theorem is in this form, you can see that it's a statement about whether casting commutes with application, which I'm not sure is provable without additional assumptions (and what Yael says suggests "no").

theorem congrDepEq' {A : Type u} {U V : A → Type v} (g : (b : A) → V b) (b : A)
    [Subsingleton (U b)] -- True if this is a subsingleton
    (hAUBV : ((a : A) → U a) = ((b : A) → V b))
    (hUaVb : U b = V b) :
    HEq ((cast hAUBV.symm g) b) (g b) := by
  congr!

theorem congrDepEq {A B : Type u} {U : A → Type v} {V : B → Type v}
  (f : (a : A) → U a) (g : (b : B) → (V b)) (a : A) (b : B)
  (hAB : A = B) (hAUBV : ((a : A) → U a) = ((b : B) → V b)) (hUaVb : U a = V b)
  [inst : Subsingleton (U (cast hAB.symm b))]
  (hfg : f = Eq.mpr hAUBV g) (hab : a = Eq.mpr hAB b) : f a = Eq.mpr hUaVb (g b) := by
  cases hAB
  cases hab
  cases hfg
  dsimp only [eq_mpr_eq_cast, cast_eq] at hUaVb ⊢
  rw [eq_comm, cast_eq_iff_heq]
  symm
  dsimp at inst
  apply congrDepEq' <;> assumption

[Rish Vaishnav]

Yaël Dillies said:

Replacing Bool → Nat with Nat × Nat is possibly clearer: For all you know, Eq.mpr hAUBV could be the map fun (a, b) ↦ (b, a), which is not the identity

I may not be understanding completely, but wouldn't this only be the case if I had used some arbitrary F : ((b : B) -> V b) -> (b : B) -> V b instead of Eq.mpr hAUBV, which is a particular defined function? I ask because it seems that the theorem is provable after adding the hUV hypothesis:

universe u v
theorem congrDepEq {A B : Type u} {U : A → Type v} {V : B → Type v}
  (f : (a : A) → U a) (g : (b : B) → (V b)) (a : A) (b : B)
  (hAB : A = B) (hUV : U = Eq.mpr (congrArg (· → Type v) hAB) V)
  (hAUBV : ((a : A) → U a) = ((b : B) → V b)) (hUaVb : U a = V b)
  (hfg : f = Eq.mpr hAUBV g) (hab : a = Eq.mpr hAB b)
  : f a = Eq.mpr hUaVb (g b) := by
  subst hAB
  subst hab
  subst hUV
  subst hfg
  rfl

I can't prove it without hfg, which would imply that this hypothesis does bring some useful information, right?

[Mario Carneiro]

Yaël Dillies said:

Replacing Bool → Nat with Nat × Nat is possibly clearer: For all you know, Eq.mpr hAUBV could be the map fun (a, b) ↦ (b, a), which is not the identity

No, this is not true. If it's possible to prove the equality using reflexivity, then Eq.mpr must be the identity map

[Yaël Dillies]

Yes, which is what adding hUV does. In the absence of if, my claim holds.

[Mario Carneiro]

your example here involves an equality (Nat × Nat) = (Nat × Nat) or (Bool → Nat) = (Bool → Nat). Lean can prove that this equality is rfl, and the cast equivalent to id, because of proof irrelevance

[Mario Carneiro]

I actually don't know whether ((x : A) -> T x) = ((x : A) -> U x) -> T = U is provable or not. The cardinality model doesn't give a counterexample

[Mario Carneiro]

If you allow both the domain and codomain to be different then it's independent

[Mario Carneiro]

Actually I take it back, there is a cardinality model counterexample, where A = Fin 2, T = ![Bool, Unit] and U = ![Unit, Bool] since in this case the two function types each have cardinality 1* 2 = 2 * 1 but T 0 is not equal to U 0

[Yaël Dillies]

Yeah indeed that's what I was alluding to but I overminimised to the point where rfl worked

[Rish Vaishnav]

Okay. So, I guess I'm stuck with hUV in that case, though I may eventually try to reformulate this theorem using HEq. On the bright side, thanks to funext I can reframe it as (hUV : ∀ a : A, U a = V (Eq.mp hAB a)), which I think makes it a bit easier to work with for my purposes:

theorem congrDepEq {A B : Type u} {U : A → Type v} {V : B → Type v}
  (f : (a : A) → U a) (g : (b : B) → (V b)) (a : A) (b : B)
  (hAB : A = B) (hUV : ∀ a : A, U a = V (Eq.mp hAB a))
  (hAUBV : ((a : A) → U a) = ((b : B) → V b)) (hUaVb : U a = V b)
  (hfg : f = Eq.mpr hAUBV g) (hab : a = Eq.mpr hAB b)
  : f a = Eq.mpr hUaVb (g b) := by
  subst hAB
  have this : U = V := funext hUV
  subst this
  subst hab
  subst hfg
  rfl