Beginner question on rfl

Stream: lean4

[Shreyas Srinivas]

I apologise if this is too basic as a mistake. I am trying to model some timing properties of certain systems in lean. For this I have the following struct:

structure Event (α : Type) where
      value : α
      time : Nat

I now want to name predicates on this type. It is useful to be able to show that the name of the predicate applied to an event is actually equal to the corresponding proposition. This is because I often have two different names say p : Event Bool -> Prop and q : Event Bool -> Prop for the same predicate which have the exact same definition say λ (e : Event Bool) => e.time ≥ 5, and I can then use Eq.trans to show that the two predicates are equal. I use this, because I have already written a theorem that says

theorem Prop_eq_implies {p q : Prop} (heq : p = q) : p → q :=
  λ (hp : p) => @Eq.subst Prop (λ p => p) p q heq hp

so I can then get a proof of q e from a proof of p e

When doing this at the top level with def and example, this is trivial as shown below:

def ip (e : Event Bool) : Prop := e.time ≥ 5
example (e : Event Bool) : (e.time ≥ 5) = ip e := rfl

This neatly typechecks and everything is fine. But the exact same thing fails when I put this code in a have statement

...
have ip (e₁ : Event Bool) : Prop := e₁.time ≥ 5
have pr_ip_eq (e : Event Bool) : (e.time ≥ 5) = ip e  := rfl
...

This somehow fails to typecheck. I am not sure why this happens. What I seem to have trouble with is that according to the book, when applying rfl, lean reduces both terms according to their definition and checks for equality. Why does it appear to not work inside a have statement?

Lean version : Lean (version 4.0.0-nightly-2021-12-20, commit 068ea1beb475, Release)

[Kevin Buzzard]

I can't read your code right now because of the `` backtick error (should be three) but perhaps the issue is this:have ip ... : Prop := ... is wrong -- you want let ip ... : Prop := .... The problem with have is that it immediately forgets the term and just remembers its type (you use it to supply proofs, not data, and ip is data).

[Shreyas Srinivas]

Hi Kevin, my apologies, I fixed it now

[Kevin Buzzard]

Does changing the have to let fix your problem? With have you'll find that ip doesn't actually know what proposition it is, just that it is some proposition or other.

[Shreyas Srinivas]

Indeed this fixes it

[Shreyas Srinivas]

Thanks a lot