Referential transparency and proofs

Stream: lean4

[cognivore]

Consider the following code:

private def isInr (x : α ⊕ β) := match x with
  | .inr _ => true
  | .inl _ => false

private def extractNat' -- (x : String)
                   (pr : String ⊕ Nat)-- := parse (parseRadixNat'Do $ hod x) x)
                   (doesParse : isInr pr)
                   : Nat :=
  match pr with
  | .inr y => y
  | .inl _ => by
    unfold isInr at doesParse
    simp at doesParse

private def parseRadixNat'Do' (_radix : Nat) (input : String) : String ⊕ Nat :=
  if input == "23" then
    .inr 100
  else
    .inl "Menzoberranzan"

private def demoParse (φ : String → String ⊕ Nat) (x : String) : String ⊕ Nat :=
  φ x

structure Nat' (x : String) :=
  radix := 10
  valE := demoParse (parseRadixNat'Do' radix) x
  doesParse : isInr $ demoParse (parseRadixNat'Do' radix) x
  val : Nat := extractNat' (demoParse (parseRadixNat'Do' radix) x) doesParse

structure Nat'Buggy (x : String) :=
  -- radix := hod x
  radix := 10
  valE := demoParse (parseRadixNat'Do' radix) x
  doesParse : isInr valE
  val : Nat := extractNat' valE doesParse

theorem high_five : isInr $ demoParse (parseRadixNat'Do' 3555) "23" := by
  simp

def bug : Nat'Buggy "228" :=
  { doesParse := high_five }
#check bug
#eval bug.val

Instead of complaining that the proof is attached to a wrong String, it binds valE to the value we supply via the theorem.

Nat', however, behaves well.

Is there a way to optimise Nat' such that we parse stuff only once and have lean check that "valE" from the theorem is the same as the default valE?

[cognivore]

To rephrase it shortly:

If a structure depends on $x$, how to make it also depend on $f \ x$ without having the user call $f \ x$ themselves?

[James Gallicchio]

Oh, I see what you mean -- I use a Cached type for this, lemme send a link

[James Gallicchio]

https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Computed.20.20Fields.20feature/near/290148231

[cognivore]

Wow, will check it out, thank you, James! cc @Ilona Prikule