Internalizing congruence lemmas

Stream: general

[Joachim Breitner]

I have been musing this puzzle:

Given a higher order function (like docs#List.map), and a congruence lemma like docs##List.map_congr that says List.map f l = List.map g l if f and g agree on (just) the members of l, can I construct a function that’s equal to List.map, but passes a proof that the element is in the list to its argument (like xs.attach.map f would do).

More generally, can this function be defined:

def internalize_congruence'
  {α β : Sort _}
  {C : α → Sort _}
  (F : (∀ x, C x) → β)
  (P : ((x : α) →  Prop))
  (cong : ∀ (f g : ∀ x, C x), (∀ x, P x → f x = g x) → F f = F g) :
  {F' : (∀ x, P x → C x) → β // ∀ (f : ∀ x, C x), F f = F' (fun x _ => f x) } := sorry

I so far managed to define it if I make some extra non-emptyness-assumptions and use classical choice:

noncomputable
def internalize_congruence'
  {α β : Sort _}
  {C : α → Sort _}
  [ne : ∀ x, Nonempty (C x)]
  (F : (∀ x, C x) → β)
  (P : ((x : α) →  Prop))
  (cong : ∀ (f g : ∀ x, C x), (∀ x, P x → f x = g x) → F f = F g) :
  {F' : (∀ x, P x → C x) → β // ∀ (f : ∀ x, C x), F f = F' (fun x _ => f x) } := by
  refine ⟨fun f => F (fun x => if h : P x then f x h else choice (ne x)), ?x⟩
  intro f
  apply cong
  intro x hx
  simp [hx]

Can I do away with that assumption and/or the use of extra axioms?

[Eric Wieser]

You can lose the axioms with:

def internalize_congruence'
    {α β : Sort _}
    {C : α → Sort _}
    [∀ x, Inhabited (C x)]
    (F : (∀ x, C x) → β)
    (P : α → Prop))
    [DecidablePred P]
    (cong : ∀ (f g : ∀ x, C x), (∀ x, P x → f x = g x) → F f = F g) :
    {F' : (∀ x, P x → C x) → β // ∀ (f : ∀ x, C x), F f = F' (fun x _ => f x) } := by
  refine ⟨fun f => F (fun x => if h : P x then f x h else default), ?x⟩
  intro f
  apply cong
  intro x hx
  simp [hx]

[Joachim Breitner]

Ah, of course. But can I drop the requirement that P needs to be decidable completely (maybe with a different approach than mine)?

[Eric Rodriguez]

Can you clarify what you mean by "passes a proof that the element is in the list to its argument"? Can you formalise the list.map example?

[Joachim Breitner]

Specializing the problem to List.map, what I want is to take an API like

List.map : (α → β) → List α → List β
List.map_congr : (∀ (x : α), x ∈ l → f x = g x) → List.map f l = List.map g l

and get

List.map' : (l : List α) → ((x : α) →  x  ∈  l → β) →  → List β

(without just defining it from scratch, of course).

The motivating context is nested recursion: If you have a trie structure, where each node has a list of subtrees, then often your functions recurse through List.map (or similar functions), and for the termination checker to see that the termination is well-founded, it needs the x ∈ l in the context, so using map' (or l.attach.map) is (as far as I understand) the way to go.

[Eric Wieser]

The other way at looking at this is that we defined map wrongly, and it should provide x ∈ l always

[Eric Wieser]

This is maybe a bit like the observation that docs#Submodule.span_induction was the wrong induction principle, and the helpful one is docs#Submodule.span_induction', even though they're equivalent in some sense

[Joachim Breitner]

Definitely! But in this thread I am more curious about how equivalent these formulations are in Lean.

In Isabelle, you only have the congruence lemma, but it can be used by the termination checker, so you don’t even have to write your functions in this somewhat strange style of having fun x hx => and seemingly not using the hx, and I wonder the same approach could work in Lean.

[Eric Rodriguez]

What do you mean you "only" have the congruence lemma? I see the idea, but also don't see any way to do it straightforwardly without P being decidable; I feel like you need to apply choice "somewhere" to pick things to apply to your function, even though congruence means that those values are irrelevant.

[Joachim Breitner]

Yeah, that's probably the answer. Thanks!

[Eric Rodriguez]

I'm still curious about the isabelle version :)

[Joachim Breitner]

I Isabelle you don't have dependent types, so you can't even write map', but you also don't need it, because map_congr is sufficient to express ”List.map only calls it's argument on members on the list”, e.g. when proving recursive function definitions to be well-defined. It's all extrinsic (?), so no need to worry about converting between intrinsic and extrinsic :-)

[Joachim Breitner]

More concretely: When lean defines a function via well-founded recursion, it uses docs#WellFounded.fix:

WellFounded.fix : (hwf : WellFounded r)
  (F : (x : α) → ((y : α) → r y x → C y) → C x)
  (x : α) : C x

where F is the one step of the function you are trying to define; it can only recurse on smaller arguments (think r = <).

In Isabelle-style, the lemma would probably look like this:

WellFounded.fix_extr : (hwf : WellFounded r)
  (F : (x : α) → ((y : α) → C y) → C x)
  (congr : (x : α) → (f g : (y : α) → C y) → ((y : α) → r y x → f y = g y) → F f x = F f y)
  (x : α) : C x

Not that this means that your function definition F doesn’t have to deal with the recursion argument at all, and you can prove it later separately, by way of a congruence lemma

Congruence lemmas are easy to prove compositionally, so many recursive functions, even if they recurse through other higher-order functions, are accepted without special attention in the definition and without explicit proof in Isabelle.

Since WellFounded definitions in Lean already only give you propositional equalities, and not definitional ones, I wonder if the above fix_extr-approach could work in Lean? Can we define fix_extr?

(Note that it’s more general; it’s straightforward to prove fix from from fix_extr, if I am not mistaken.)