And.rec

Stream: Type theory

[Riccardo Brasca]

This can be a stupid question, I apologize in advance. Is the following sorry provable?

theorem foo (P Q : Prop) (A : Type) (f : P → Q → A) (x : P ∧ Q) :
    And.rec f x = f (And.left x) (And.right x) := sorry

I was expecting rfl to prove it, but it doesn't, and I don't see what else one can do. Note that

theorem bar (P Q : Prop) (A : Type) (f : P → Q → A) (p : P) (q : Q) :
    And.rec f (And.intro p q) = f p q := rfl

works. In particular it seems to me that, in proving foo, one can replace the first x by the (definitionally) equal term And.intro (And.left x) (And.right x) and then use bar, but

example (P Q : Prop) (A : Type) (f : P → Q → A) (x : P ∧ Q) :
    And.rec f x = f (And.left x) (And.right x) := by
  show And.rec f (And.intro (And.left x) (And.right x)) = f (And.left x) (And.right x)

gives a "type mismatch" error. Am I misunderstanding something obvious?

[Eric Wieser]

theorem foo (P Q : Prop) (A : Type) (f : P → Q → A) (x : P ∧ Q) :
    And.rec f x = f (And.left x) (And.right x) := by cases x; rfl

[Riccardo Brasca]

Ahahah yes, of course...

[Riccardo Brasca]

Still, I am I was expecting the to terms to be definitionally equal. Are they?

[Eric Wieser]

Here's a weird case:

import Mathlib

theorem bar (P Q : Prop) (A : Type) (f : P → Q → A) (x : P ∧ Q) :
    (And.rec f x : A) = And.rec f ⟨x.left, x.right⟩ :=
  congr_arg _ (show x = ⟨x.left, x.right⟩ from rfl)  -- rfl doesn't work by itself

[Eric Wieser]

And.rec has arguments that are equal by rfl, but the application is not equal by rfl!

[Riccardo Brasca]

In my (very limited) understanding of type theory the two terms should be definitionally equal. Maybe this is one of the rare cases where rfl doesn't prove the "true" definitional equality?

[Eric Wieser]

This might just be a corner case of eta-expansion that wasn't implemented

[Eric Wieser]

Indeed, it works fine for Prod:

theorem bar (P Q : Type) (A : Type) (f : P → Q → A) (x : P × Q) :
    (Prod.rec f x : A) = Prod.rec f ⟨x.1, x.2⟩ := rfl

[Alex J. Best]

Also interesting

import Mathlib

theorem bar (P Q : Prop) (A : Type) (f : P → Q → A) (x : P ∧ Q) :
    (And.rec f x : A) = And.rec f ⟨x.left, x.right⟩ := by
  have : x = And.intro x.left x.right := rfl
  conv_lhs =>
    whnf
  conv_rhs =>
    whnf

[Eric Wieser]

So I think either this is just a bug where something is checking for Type when Sort would do, or there is a reason that checking for Sort is a bad idea

[Riccardo Brasca]

I don't know if it is relevant, but the fact that And can eliminate into Type is because of subsingleton elimination, so it's understandable that it works slightly differently from the elimination for Prod.

[Mario Carneiro]

eta for structures only works for structures

[Eric Wieser]

structure And (a b : Prop) : Prop where
  /-- `And.intro : a → b → a ∧ b` is the constructor for the And operation. -/
  intro ::
  /-- Extract the left conjunct from a conjunction. `h : a ∧ b` then
  `h.left`, also notated as `h.1`, is a proof of `a`. -/
  left : a
  /-- Extract the right conjunct from a conjunction. `h : a ∧ b` then
  `h.right`, also notated as `h.2`, is a proof of `b`. -/
  right : b

[Eric Wieser]

So does the "structure" in "eta for structures" refer to something that isn't structure?

[Mario Carneiro]

actually it works for structure-like inductives, but And should be included

[Mario Carneiro]

and Alex's example shows that it does actually work

[Mario Carneiro]

oh wait, alex's example is true by proof irrelevance not eta for structures

[Arthur Adjedj]

Both the elaborator and the kernel avoid doing eta-expansion for Prop-structures, which blocks the iota-reduction of And.rechere.

[Arthur Adjedj]

Mario Carneiro said:

oh wait, alex's example is true by proof irrelevance not eta for structures

Despite the presence of proof-irrelevance, I don't think the reduction of And.rec should trigger in the absence of eta, unless the reduction rules for structure-like inductives was adapted to reduce using projections instead of matching (it would also possibly make sense from a performance perspective to do so).

[Mario Carneiro]

I think the implementation is incorrect (or at least incomplete) to not trigger eta for prop-structures. It is definitely a "provable definitional equality", since it's just congrArg _ rfl

[Mario Carneiro]

but on the other hand reducing recursors for large eliminating props applied to variables is exactly what leads to the undecidability of the typing judgment, so it's not unreasonable to be incomplete here

[Arthur Adjedj]

This also breaks congruence of definitional equality:

variable (P Q : Prop) (A : Type) (f : P → Q → A) (x : P ∧ Q)

example : And.rec f ⟨x.1,x.2⟩ = f (And.left x) (And.right x) := rfl
example : (And.rec f ⟨x.1,x.2⟩ : A) = And.rec f x  := rfl --fails

[Arthur Adjedj]

The right-hand side of the definitional equality is reduced too eagerly, leading to this error. However, even if this type-checked, it would still lead to yet another case of non-transitivity of definitional equality due to eta-for-structures.

[Arthur Adjedj]

Mario Carneiro said:

but on the other hand reducing recursors for large eliminating props applied to variables is exactly what leads to the undecidability of the typing judgment, so it's not unreasonable to be incomplete here

The only possibly dangerous recursors for that would be recursors over recursive large eliminating Props such as Acc, eta-expanding structure-like (thus, non-recursive) Prop-inductives for reduction would certainly not lead to a leakage of infinite reduction in Prop.

[Riccardo Brasca]

Arthur Adjedj said:

This also breaks congruence of definitional equality:

variable (P Q : Prop) (A : Type) (f : P → Q → A) (x : P ∧ Q)

example : And.rec f ⟨x.1,x.2⟩ = f (And.left x) (And.right x) := rfl
example : (And.rec f ⟨x.1,x.2⟩ : A) = And.rec f x  := rfl --fails

To check I am at least understanding what is going on: this is an example that shows that definitional equality (in the sense that rfl proves the equality) does not respect the congruence rules for substitution (or whatever is called the fact that if we replace a by a definitionally equal term b in an expression we get a new expression that is definitionally equal to the previous one)?

[Riccardo Brasca]

In particular, it is not an example of definitional equality not being transitive.

[Arthur Adjedj]

Yes, what I'm saying is that the following rule of conversion fails in this example:

$$\frac{\Gamma \vdash f \equiv g \;\;\;\; \Gamma \vdash x \equiv y}{\Gamma \vdash f\; x \equiv g \; y }$$

This is not an example of non-transitive defeq. However, if And.rec f ⟨x.1,x.2⟩ and And.rec f x were definitionally equal (and they should be), this would still break transitivity, because And.rec f ⟨x.1,x.2⟩ is defeq to f x.1 x.2, but And.rec f x isn't.

[Mario Carneiro]

it's not hard to get lean to agree that the application compatibility rule exists:

example :
  id (And.rec (motive := fun _ => A) f) ⟨x.1,x.2⟩ =
  id (And.rec (motive := fun _ => A) f) x := rfl
example :
  id (And.rec (motive := fun _ => A) f) ⟨x.1,x.2⟩ =
  And.rec (motive := fun _ => A) f ⟨x.1,x.2⟩ := rfl
example :
  id (And.rec (motive := fun _ => A) f) x =
  And.rec (motive := fun _ => A) f x := rfl

[Arthur Adjedj]

Should an issue/RFC/PR be opened on that regard ? The fix (eta-expanding Prop-structures during iota-reduction) seems straightforward and innocuous.

[Chris Hughes]

Note that this isn't necessarily to do with just Prop

Here's another related non-transitivity

example (x y : Unit × Unit) : x = y := rfl -- fails
example (x y : Unit × Unit) : x = y :=
  calc x = ((), ()) := rfl
       _ = y := rfl

[Chris Hughes]

How can I check if the kernel accepts it without going through the elaborator first? Is there a way?

[Arthur Adjedj]

This transitivity failure comes from another issue, and has already been documented here. This come from the fact that the criteria for triggering eta-for-unit during defEq doesn't accept types it should accept. The issue mentioned in this thread is due to the fact that eta-expansion isn't triggered during iota-reduction for Prop-structures.

[Eric Wieser]

Arthur Adjedj said:

Should an issue/RFC/PR be opened on that regard ? The fix (eta-expanding Prop-structures during iota-reduction) seems straightforward and innocuous.

This came up again in this thread; if nothing else a canonical issue to reference would be helpful.