boolean true = true is Prop True?

Stream: lean4

[Hannah Santos]

I've been trying to prove some things for this ListNat type, to practice, and I've been having this problem with having to prove (true = true) = True, and also with ¬(false = true) = True every time I want to use an if-then-else. It would be most helpful if one could point me in the right direction here. :sweat_smile:

inductive ListNat where
  | nil
  | cons : Nat → ListNat → ListNat
  deriving Repr

open ListNat
open Nat

def filter : (Nat → Bool) → ListNat → ListNat
  | _, nil => nil
  | function, cons n l => if function n = True then cons n (filter function l) else filter function l

def append : Nat → ListNat → ListNat
  | n, nil => cons n nil
  | n, cons m l => cons m (append n l)

def reverse : ListNat → ListNat
  | nil => nil
  | cons n l => append n (reverse l)

theorem false_not_true :
  false ≠ true :=
by
  intro H
  cases H

theorem filter_reverse (n : Nat) (ns : ListNat) (p : Nat → Bool):
  filter p (append n (reverse ns)) = (if p n then append n (filter p (reverse ns)) else (filter p (reverse ns))) :=
by
  induction ns with
  | nil =>
    rw [reverse, filter, append, filter, filter]
    cases p n
    rw [if_neg, if_neg false_not_true]
    intro H
    exact false_not_true H

/-case nil.true
  l: ListNat
  n: Nat
  p: Nat → Bool
  ⊢ (if (true = true) = True then cons n nil else nil) = if true = true then cons n nil else nil
  Expected type
  Messages (1)

lean:413:25
  application type mismatch
    false_not_true H
  argument
    H
  has type
    (false = true) = True : Prop
  but is expected to have type
    false = true : Prop
  -/

[Alex Keizer]

The simp tactic should be able to prove that for you.

example : (true = true) = True := by
  simp only

[Hannah Santos]

But what is it doing behind the scenes?

[Timo Carlin-Burns]

It looks like the main thing it's using is docs#eq_true_of_decide

import Mathlib.Tactic

example : (true = true) = True := by
  show_term simp only
  -- Try this: exact of_eq_true (eq_true_of_decide (Eq.refl true))

[Timo Carlin-Burns]

The decide tactic also works

example : (true = true) = True := by decide

[Hannah Santos]

And what would work for the other case ¬(false = true) = True?

[Timo Carlin-Burns]

example : ¬(false = true) = True := by
  decide

[Timo Carlin-Burns]

(simp/simp only would work as well. By default simp uses decide automatically, so anything decide can prove simp can prove too.)

[Kevin Buzzard]

If you're trying to prove things rather than compute things, then why not use Prop instead of bool? It's far more proof-friendly. It's quite rare to see bool in mathlib, for example.

[Hannah Santos]

(I like to avoid simp because I like to write every part of the proof myself, when I put simp I feel like I have no clue as to what solved it)

[Hannah Santos]

It's a part of a homework I got, so it was supposed to be in bool. (Even though making it on Lean is a part of my desire to suffer, it seems)

[Ruben Van de Velde]

I think (part of) the cause may be the if function n = True in your filter, where function n returns a Bool but True is a Prop. Try replacing that by = true, perhaps

[Hannah Santos]

Oh!

[Hannah Santos]

I did that again!

[Hannah Santos]

Thanks.

[Thomas Murrills]

By the way, there are other ways to show this equality! One is by decide, but you can turn decide off in simp and it still works:

theorem foo : (true = true) = True := by
  simp (config := {decide := false}) only

#print foo

The main ingredient in this method (which imo is more "sensible") is propext, turning a ↔︎ b into a = b; and we can prove a ↔︎ b directly when a and b are true (in the sense that h1 : a and h2 : b) by just providing those proofs for each direction. So this bottoms out to rfl : true = true and trivial : True; see eq_self and eq_true (which perform this proof) for details. (Actually this particular simp does some unnecessary stuff as well, so it's not the best example, but you can still find sensible things by digging through the term and command-clicking.)

You might be aware of these already, but just in case it's helpful for discovery: simp?, is useful in seeing what lemmas simp uses behind the scenes (I think you might need to import Std?), and if you don't have access to that, there's always set_option trace.Meta.Tactic.simp true. (And, ofc, #print <theoremName> after the fact to see what the term is! :) )

[Kevin Buzzard]

Classically Prop and bool are the same thing. I'm a bit unclear about the homework claim. If the homework wasn't "do this in lean" then you could argue that Prop = {True, False} just like bool = {true, false} and surely it's very difficult to tell them apart