Lemma `dec_eq_refl : decEq x x = isTrue rfl`?

Stream: Is there code for X?

[Ruifeng Xie]

I am very new to Lean4 (though I have experience in both Coq and Agda). I figured out that I can cases decEq x x; contradiction to do the rewrite I want, but it does not feel quite right. However, I looked into the file Prelude.lean and did not find any lemma for decEq itself, only for decide. This also makes me wonder if using decEq directly is idiomatic at all? Should I use something based on decide instead?

[Eric Wieser]

Can you make a #mwe?

[Aaron Liu]

Can you get rid of the part where you cases decEq x x and just contradiction directly?

[Edward van de Meent]

out of curiosity, let me #xy decEq is showing up in your goal?

[Edward van de Meent]

(also, note that your dec_eq_refl can be proven as Subsingleton.elim (decEq x x) (isTrue rfl) since Decidable p is subsingleton)

[Kenny Lau]

this also feels like #xy to me

[Ruifeng Xie]

It might actually be an X-Y problem, because I do not really know what is the best way to achieve my goal. To answer the questions:

• decEq x x shows up in the goal (after I unfold the recursive function)
• it appears as the scrutinee of a match expression, so I cannot proceed without rewriting it to isTrue _
• using cases decEq x x, the goal splits into two, one of them proceeds with the match simplified, the other is left with a not (x = x) in the premise, which I managed to eliminate with contradiction

I will try to make an MWE right now.

[Aaron Liu]

Why have you set this as your goal

[Aaron Liu]

What recursive function does this show up in

[Ruifeng Xie]

Consider this example, just pretend that 42 and 0 somehow need to access the proofs x_eq_y and x_neq_y:

def test (x y : String) : Nat :=
  match decEq x y with
  | isTrue x_eq_y => 42
  | isFalse x_neq_y => 0

theorem test_x_x : test x x = 42 := by
  unfold test
  cases decEq x x
  · contradiction
  · simp

[Eric Wieser]

The preferred way to spell this is usually

if h : x = y then
  42
else
  0

[Eric Wieser]

Then cases decEq x x becomes split

[Ruifeng Xie]

Oh, thanks. I did not know this syntax for if.

[Ruifeng Xie]

But does this actually simplify the proof? After split I seem to still get two goals, one of which to be eliminated by contradiction.

[Ruifeng Xie]

def test (x y : String) : Nat :=
  match decEq x y with
  | isTrue x_eq_y => 42
  | isFalse x_neq_y => 0

theorem dec_eq_refl [DecidableEq A] (x : A) : decEq x x = isTrue rfl := by
  cases decEq x x
  · contradiction
  · simp

theorem test_x_x : test x x = 42 := by
  unfold test
  rw[dec_eq_refl x]

[Ruifeng Xie]

This version works, so I was wondering if this lemma is present somewhere in the stdlib.

[Kim Morrison]

Probably not, because no one uses decEq. :-)

[Ruifeng Xie]

I see. Should I write in the following way instead?

def test (x y : String) : Nat :=
  if h : x = y
  then 42
  else 0

theorem test_x_x : test x x = 42 := by
  unfold test
  split
  · simp
  · contradiction

[Ruifeng Xie]

I can see that the function definition should probably be written this way, but can the proof also be improved?

[Markus Himmel]

Don't use split if you know which branch of the if is true:

def test (x y : String) : Nat :=
  if h : x = y
  then 42
  else 0

theorem test_x_x : test x x = 42 := by
  simp [test]

theorem test_x_x' : test x x = 42 := by
  unfold test
  simp

theorem test_x_x'' : test x x = 42 := by
  unfold test
  rw [dif_pos rfl]

theorem test_x_x''' : test x x = 42 := by
  unfold test
  rw [dif_pos]
  rfl

[Ruifeng Xie]

Oh, wow.

[Ruifeng Xie]

I did not know simp is this powerful.

[Ruifeng Xie]

Where can I learn about the capabilities of these tactics (ideally with some examples)? I am most familiar with Agda and tactics are not a thing there, so I was learning with trial and error.

[Markus Himmel]

Theorem Proving in Lean has a chapter on tactics that might be a good start: https://lean-lang.org/theorem_proving_in_lean4/Tactics/#Theorem-Proving-in-Lean-4--Tactics

[Ruifeng Xie]

Thanks for all your kind help.

[Ruifeng Xie]

One last question, I guess. With match, I can split on multiple conditions at the same time (copied from my code, please ignore the details):

match is_bound x e, is_bound x f with
| isTrue u, _ => isTrue (.app₁ u)
| isFalse _, isTrue v => isTrue (.app₂ v)
| isFalse u, isFalse v => isFalse fun
  | .app₁ w => absurd w u
  | .app₂ w => absurd w v

Can I also do the same thing with that dependent if?

[Ruifeng Xie]

Also, I noticed that I cannot seem to use dependent if on the Decidable instance being defined. I presume a match is then necessary?

[Kenny Lau]

Ruifeng Xie said:

Can I also do the same thing with that dependent if?

just write two ifs, it isn't like you aren't doing that in the code already

[Kenny Lau]

but no this is another #xy

[Kenny Lau]

from your code i infer that you're trying to prove that something is decidable, and you shouldn't use the isTrue and isFalse things directly, but rather you should use standard lemmas to help you, in this case you should prove an \iff statement in Prop land, and then use decidable_of_decidable_of_iff

[Kenny Lau]

Ruifeng Xie said:

• after I unfold the recursive function

basically this is a common beginner's trap, which is to rely a lot on the underlying definitions, where the better thing to do is to use the standard lemmas to relate definitions to other things

[Kenny Lau]

basically, let's just say this, if you ever have isTrue and isFalse in your code, you're doing something wrong

[Kenny Lau]

see #new members > Decidable instance @ 💬 for an example

[Kenny Lau]

@Markus Himmel this is the second time (as can be seen by the fact that my previous message is a link), is this covered in TPIL somewhere?

[Ruifeng Xie]

Kenny Lau said:

basically, let's just say this, if you ever have isTrue and isFalse in your code, you're doing something wrong

I’m glad to know this before I make even further progress in my proof. It is a habit I carry from Agda, where it does not cause a hassle.

[Ruifeng Xie]

Kenny Lau said:

from your code i infer that you're trying to prove that something is decidable, and you shouldn't use the isTrue and isFalse things directly, but rather you should use standard lemmas to help you, in this case you should prove an \iff statement in Prop land, and then use decidable_of_decidable_of_iff

Thanks for the pointer. I’ll check the documentation and see if I can massage these lemmas into the correct shape for the proof. If there is also an induction lemma for decidables, then I should be able to replace all my proof accordingly.

I have a question, though. What is the benefit of using these lemmas instead of isTrue and isFalse?

[Kenny Lau]

Prop is generally easier to work with than objects

[Kenny Lau]

The predicative hierarchy of Prop

source: https://agda.readthedocs.io/en/v2.6.0/language/prop.html

[Kenny Lau]

Prop in Lean also differs from Prop in Agda in a very significant way: in Lean there is only Prop

[Ruifeng Xie]

Okay, I see. Then I’ll assume that the benefit of Prop is proof irrelevance. Actually, I had the impression that Prop in Agda is not very pleasant to work with, and I have been using Data.Irrelevance instead.

[Ruifeng Xie]

I really wish there is something similar to PLFA for Lean, so that I can work with something familiar and focus on the formalisation and proof techniques.

[Kenny Lau]

what's PLFA?

[Kenny Lau]

Ruifeng Xie said:

Then I’ll assume that the benefit of Prop is proof irrelevance.

I thought Prop in Agda also has proof irrelevance

[Ruifeng Xie]

It does. It is just that Agda also has irrelevance notations for any data type at all (without a separate sort), which is exposed in the Data.Irrelevance module from stdlib.

[Ruifeng Xie]

PLFA is Programming Language Foundations in Agda, a textbook written by Philip Wadler et al.

[Ruifeng Xie]

It is available online at https://plfa.github.io

[Kenny Lau]

does #tpil suffice?

[Ruifeng Xie]

I have not finished reading through it yet, but it has been very helpful. I brought up PLFA mainly because it is driven by examples (formalisation of lambda calculus, modeling semantics, implementing type-checking, etc.), and in each step you learn just enough to accomplish the goal.

[Ruifeng Xie]

I must have missed something. I checked the function decidable_of_decidable_of_iff, but I do not see how it is easier to work with then isTrue and isFalse. Below is part of the proof I was working on:

inductive Expr : Type where
  | const (c : String)
  | var (x : String)
  | app (e f : Expr)
  | abs (x : String) (e : Expr)

open Expr public

inductive Free (x : String) : Expr → Prop where
  | var : Free x (var x)
  | app₁ : Free x e → Free x (app e f)
  | app₂ : Free x f → Free x (app e f)
  | abs : x ≠ y → Free x e → Free x (abs y e)

instance isFree (x : String) : DecidablePred (Free x)
  | const _ => isFalse nofun
  | var y => if h : x = y
    then isTrue (h ▸ .var)
    else isFalse fun .var => absurd rfl h
  | app e f => match isFree x e, isFree x f with
    | isTrue u,  _         => isTrue (.app₁ u)
    | isFalse _, isTrue v  => isTrue (.app₂ v)
    | isFalse u, isFalse v => isFalse fun
      | .app₁ w => absurd w u
      | .app₂ w => absurd w v
  | abs y e => if h : x = y
    then isFalse fun (.abs x_neq_y _) => absurd h x_neq_y
    else match isFree x e with
      | isFalse u => isFalse fun (.abs _ w) => absurd w u
      | isTrue u  => isTrue (.abs h u)

Take the first case (const) of isFree for example, isFalse nofun looks short enough for me, while using decidable_of_decidable_of_iff I only managed to end up with @decidable_of_decidable_of_iff False _ _ ⟨nofun, nofun⟩.

[Kenny Lau]

@Ruifeng Xie that is indeed a little bit tricker. I think in that case I would keep Free, but then below that I would construct freeBool : Expr -> Bool that acts as the "decision program", and then below that prove a theorem freeBool_iff_free, and then finally use decidable...iff

[Kenny Lau]

See (a : α) (as : List α) : Decidable (a ∈ as) for an example

[Kenny Lau]

(the corresponding function to Bool is elem)

[Ruifeng Xie]

I see. I actually tried this approach before switching back to the current version.

This must be a philosophical thing, then. I try very hard to avoid separating the proof and the algorithm, and I learned this style from Wouter Swierstra (his IFL24 talk and his JFP Pearl paper, for example). One of the benefits is that we have a single source of truth, and we do not need to update multiple places when the definition changes. Perhaps it is not a top concern in Lean due to the tactics.

[Chris Henson]

You are correct there is a different design tendency to separate "data" and proofs. As an example, consider docs#Vector, which is a structure with an array and a proof about length as opposed to the standard example you might see in Agda or Rocq.

[Ruifeng Xie]

I see. It makes sense considering that Lean also needs good runtime performance.

[Kenny Lau]

Ruifeng Xie said:

when the definition changes

well, the definition of List.mem actually changed, but that doesn't affect the List -> Bool "decision program", so maybe that's one benefit of separating out the algorithm

[Matt Diamond]

Ruifeng Xie said:

I really wish there is something similar to PLFA for Lean, so that I can work with something familiar and focus on the formalisation and proof techniques.

maybe https://github.com/rami3l/PLFaLean?

[Ruifeng Xie]

Wow, thanks.

[Kenny Lau]

Ruifeng Xie said:

This must be a philosophical thing, then. I try very hard to avoid separating the proof and the algorithm, [...] One of the benefits is that we have a single source of truth, [...]

I've actually been thinking more about this, and in Mathlib we actually separate the definition and the proof a lot; in fact we tend to (and we encourage people to) make definitions be as general as possible and assume as few things as possible, and as a result the function would take on junk values outside the actual domain of interest. One famous example is how we require fields to satisfy the axiom 1/0 = 0, because we want to make division a total function, because we don't want to be supplying proofs in the theorem statements all of the time.

[Ruifeng Xie]

That makes sense. I think the proof is easier to write and maintain if written at the same place as the definition, but the UX of a separate proof might be better in some scenarios.