propext docstring contains invalid code

Stream: lean4

[Snir Broshi]

propext (propositional extensionality) is in Init/Core.lean, documented here
Its docstring contains the following example:

set_option pp.proofs true

def foo : Nat := by
  have : (True → True) ↔ True := ⟨λ _ => trivial, λ _ _ => trivial⟩
  have := propext this ▸ (2 : Nat)
  exact this

#reduce foo
-- propext { mp := fun x x => True.intro, mpr := fun x => True.intro } ▸ 2

#eval foo -- 2

This code fails, as you can see on Lean 4 Web, with the following error:

invalid `▸` notation, the equality
  propext this
has type
  (True → True) = True
but neither side of the equality is mentioned in the type
  Nat

What goes wrong in this example? Is it something that broke in the Lean 4 transition?

[Robin Arnez]

My guess is that it previously did not complain about this exact problem and just did:

set_option pp.proofs true

def foo : Nat := by
  have : (True → True) ↔ True := ⟨λ _ => trivial, λ _ _ => trivial⟩
  have := Eq.rec (motive := fun _ _ => Nat) (2 : Nat) (propext this)
  exact this

#reduce foo
-- foo._proof_2 foo._proof_1 ▸ 2

#eval foo -- 2

[Snir Broshi]

So should we fix it to use your solution in a PR?

[François G. Dorais]

What is this example supposed to illustrate?

[Robin Arnez]

Reduction getting stuck in the presence of this axiom

[François G. Dorais]

Doesn't reduction get stuck on any axiom? Anyway, it's an unusual thing to put in a docstring.

[Snir Broshi]

François G. Dorais said:

Doesn't reduction get stuck on any axiom?

Other than propext, the only axioms in Lean & Mathlib are Classical.choice and Quot stuff.
Here's an example with choice:

def foo : Set Nat := { x | x = 0 }
theorem foo_ne : Nonempty foo := Nonempty.intro ⟨0, rfl⟩

#reduce (Classical.choice foo_ne).val
-- (Classical.choice foo_ne).1

But can Quot.sound do this as well? Not sure

[Robin Arnez]

Quot.sound example:

structure TestType (x : Quot fun _ _ : Nat => True) where
  value : Nat

def test : Nat :=
  let a : TestType (Quot.mk _ 0) := ⟨3⟩
  have h : Quot.mk (fun _ _ : Nat => True) 0 = Quot.mk _ 1 := Quot.sound trivial
  (h ▸ a).value

#eval test
#reduce test

My guess is that propext is here in particular because it's commonly found when using rw. Maybe a better example is:

def myProp := ¬False

instance : Decidable myProp := by
  simp [myProp]
  infer_instance

#reduce decide myProp -- gets stuck

[François G. Dorais]

Snir said:

Other than propext, the only axioms in Lean & Mathlib are Classical.choice and Quot stuff.

And sorryAx, ofReduceBool, ofReduceNat, maybe a couple more? Also, opaque defs should break reduction in the same way. It seems to be there isn't anything special to propext here.

[François G. Dorais]

IMHO the bottom line is that this kind of reduction issue should be documented somewhere but the docstring for propext is not the right place since it gives little guidance on how to use propext other than the fact that it is an axiom.

[Snir Broshi]

So PR to delete it then?

[François G. Dorais]

That's probably the best.

[Kyle Miller]

I think the motivation of this part of the docstring is to point out that you can't use iffs to do rewrites and expect the result to still reduce. This is a reason for the overly general advice "don't use tactics to make definitions".

@Mario Carneiro wrote this — maybe he wants to iterate on it? Or maybe @David Thrane Christiansen is planning on incorporating it into the language reference?

[Mario Carneiro]

I'm not sure I understand the issue

[Mario Carneiro]

the docstring does mention that the same thing is true for any axiom

[Mario Carneiro]

the way to use propext is to prove that two propositions are equal given that they are iff, this seems self-explanatory and is also the first paragraph

[Kyle Miller]

The issue is that the example doesn't work right now. Mainly, I figured I'd ping you before someone makes a PR to delete anything, and if someone's wanting to modify things, best to ping the original author.

[Mario Carneiro]

this code was definitely tested at one point, so it must be a regression

[Kyle Miller]

I'm sure you tested it. I think what happened is the triangle operator was improved. It notices that neither True nor True -> True appears in Nat and fails intentionally.

[Mario Carneiro]

here's a fixed version, but it has significantly degraded as a demonstration:

set_option pp.proofs true

def foo : Nat := by
  have : (True → True) ↔ True := ⟨λ _ => trivial, λ _ _ => trivial⟩
  have : Nat := (propext this).recOn (motive := λ _ _ => Nat) 2
  exact this

#reduce foo
-- foo._proof_2 foo._proof_1 ▸ 2

#eval foo -- 2

[Mario Carneiro]

maybe there is a way to disable the proof extraction

[David Thrane Christiansen]

I think the docstring should just link to the section on reduction and axioms if this is something that needs to be explicitly called out here, and this example can be deleted.

[David Thrane Christiansen]

I can do it in the next couple of days

[Robin Arnez]

There's some stuff in that section that's wrong/misleading, specifically the "Axioms and Compilation" section:

The function is marked partial to avoid further error messages from termination checking.

That's not true, there are no further error messages.

The by_cases tactic uses the Law of the Excluded Middle, which is proved in the standard library using the Axiom of Choice. Indeed, this definition uses three axioms:

This is misleading, the actual source of Classical.choice turns out to be Nat.left_eq_add! In fact, this variant doesn't use choice:

def nextOdd (k : Nat) :
    { n : Nat // n % 2 = 1 ∧ (n = k ∨ n = k + 1) } where
  val := if k % 2 = 1 then k else k + 1
  property := by
    by_cases k % 2 = 1 <;>
    simp only [↓reduceIte, Nat.succ_ne_self, Nat.ne_add_one, or_false, or_true, and_true, *] <;> omega

[Mario Carneiro]

Man, this thing about stupid uses of choice bums me out so much. Lean FRO has changed a lot in the past few years, I'd really like us to allow some PRs through to fix the low hanging fruit here

[David Thrane Christiansen]

Thanks @Robin Arnez, I've fixed the inaccuracies.