Wishlist for congruence lemmas

[gebner]

As discussed yesterday, let me summarize the important changes related to congruence lemmas in Lean 3 as well as some features that we wanted to add but would have required larger refactorings.

The first two items are about automatically generated congruence lemmas for simp. The other two are about user congruence lemmas marked with @[congr]. Automatically generated congruence lemmas for congruence closure haven't really changed (these are also used for the congr and convert tactics).

Rewriting under subsingleton arguments

If f : α → β, then the congruence lemma should be ∀ x y, x = y → f x = f y even if α is subsingleton.

The rationale is that we want to rewrite e.g. zero-length vectors (see corresponding PR leanprover-community/lean#134):

instance {α : Type u} : HAppend (Fin m → α) (Fin n → α) (Fin (m + n) → α) where
  hAppend a b i := if h : i < m then a ⟨i, h⟩ else b ⟨i - m, sorry⟩

def empty : Fin 0 → Nat := (nomatch ·)

theorem append_empty (x : Fin i → Nat) : x ++ empty = x :=
  funext fun i => dif_pos _

constant f : (Fin 0 → Nat) → Prop
example : f (empty ++ empty) = f empty := by simp only [append_empty] -- should work

Dependent subsingleton instances

This is about functions like the following, where Decidable/Fintype are classes that are also subsingletons but not in Prop:

decide : (p : Prop) → [Decidable p] → Bool
Fintype.card : (α : Type u) → [Fintype α] → Nat

The congruence lemma for decide should be ∀ p q, p = q → [Decidable p] → [Decidable q] → decide p = decide q.

Rationale: generating the instance for Decidable q as ‹p = q› ▸ ‹Decidable p› introduces a diamond, since ‹p = q› ▸ ‹Decidable p› and ‹Decidable q› are typically not defeq. One consequence of using ▸ instead of synthesizing the instance is that simp cannot solve the following example (because decide p = decide p would not be true by reflexivity):

example [Decidable p] : decide (p ∧ True) = decide p := by simp -- should work

Relevant PR: leanprover-community/lean#665 Note: we had to disable the subsingleton check completely in Lean 3 because of massive performance issues with TC synthesis. Now it only checks if the type is of the form ∀ ..., decidable ....

Partially applied user congruence lemmas

This is an actual wishlist item and not implemented in Lean 3 either yet. But it fits the theme, so let me mention it here.

User congruence lemmas should also work if they only match a prefix of the application. That is, a congruence lemma Array.get as i = Array.get bs j should also apply to a subterm Array.get xs j y.

@[congr]
theorem Array.get_congr (as bs : Array α) (h : as = bs) (i : Fin as.size) (j : Nat) (hi : i = j) :
    as.get i = bs.get ⟨j, h ▸ hi ▸ i.2⟩ := by
  subst bs; subst j; rfl

example (as : Array Nat) (h : 0 + x < as.size) :
    as.get ⟨0 + x, h⟩ = as.get ⟨x, Nat.zero_add x ▸ h⟩ := by
  simp -- should work

example (as : Array (Nat → Nat)) (h : 0 + x < as.size) :
    as.get ⟨0 + x, h⟩ i = as.get ⟨x, Nat.zero_add x ▸ h⟩ i := by
  simp -- should also work

Type-specific congruence lemmas

Another actual wishlist item, it would be useful to lift the restriction that all function arguments on the lhs must be free variables. With polymorphic functions, you often want to declare a more specific congruence lemma for some types (e.g. if some arguments become subtypes---see congruence lemma for the Fin argument of Array.get above.)

def Pi.single [DecidableEq ι] {f : ι → Type u} [∀ i, Inhabited (f i)] (i : ι) (x : f i) : ∀ i, f i :=
  fun j => if h : j = i then h ▸ x else default

structure Set (α : Type u) where of :: mem : α → Prop

instance : CoeSort (Set α) (Type u) where coe s := Subtype s.mem

@[congr]
theorem dep_congr [DecidableEq ι] {p : ι → Set α} [∀ i, Inhabited (p i)] :
    ∀ {i j} (h : i = j) (x : p i) (y : α) (hx : x = y), Pi.single (f := (p ·)) i x = Pi.single (f := (p ·)) j ⟨y, hx ▸ h ▸ x.2⟩
  | _, _, rfl, _, _, rfl => rfl

Requested on Zulip: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/simp.20simp/near/263872040

[leodemoura]

@gebner Thanks!

The current TODO list is:

1. Automatically generate lemmas such as

@[congr] theorem decide_congr (p q : Prop) (h : p = q) [s₁ : Decidable p] [s₂ : Decidable q] : decide p = decide q := by
  subst h
  have : s₁ = s₂ := Subsingleton.elim s₁ s₂
  subst this
  rfl

2. Lift the restriction that all function arguments on the lhs must be free variables.

[leodemoura]

@gebner Do you have an example that needs dep_congr?

[gebner]

Do you have an example that needs dep_congr?

Here you go:

def Submodule (α : Type u) [OfNat α 0] := { s : Set α // s.mem 0 }
instance [OfNat α 0] : CoeSort (Submodule α) (Type u) where coe s := s.1
instance [OfNat α 0] (p : Submodule α) : Inhabited p where default := ⟨0, p.2⟩

example (p : Nat → Submodule Nat) :
    Pi.single (f := (p ·)) (x - x) ⟨0, (p ..).2⟩ = Pi.single 0 ⟨0, (p ..).2⟩ := by
  simp only [Nat.sub_self] -- should work

[leodemoura]

@gebner The new test 988.lean contains all examples from the wishlist above. If there are missing features, please create a new issue.