Zulip Chat Archive

Stream: new members

Topic: how can i prove things inside dos?

lorã (Apr 15 2025 at 03:16):

I mean, do i have i good way to deal with it? I'm trying to prove a thing that... There's my goal:

Goals (3)
case left.h_1
task : Tasks.Task
x : Status
heq : task.status = done
⊢ (do
      let name ←
        ((obj
                  (Id.run
                    (RBNode.insert compare
                      (RBNode.insert compare (RBNode.insert compare RBNode.leaf "name" (str task.name)) "desc"
                        (str task.desc))
                      "status" (str "done")))).getObjValD
              "name").getStr?
      let desc ←
        ((obj
                  (Id.run
                    (RBNode.insert compare
                      (RBNode.insert compare (RBNode.insert compare RBNode.leaf "name" (str task.name)) "desc"
                        (str task.desc))
                      "status" (str "done")))).getObjValD
              "desc").getStr?
      Task.mk name desc <$>
          match
            (obj
                  (Id.run
                    (RBNode.insert compare
                      (RBNode.insert compare (RBNode.insert compare RBNode.leaf "name" (str task.name)) "desc"
                        (str task.desc))
                      "status" (str "done")))).getObjValD
              "status" with
          | str "done" => Except.ok done
          | str "undone" => Except.ok undone
          | str "canceled" => Except.ok canceled
          | str other => Except.error (toString "Invalid format: " ++ toString other ++ toString "")
          | x => Except.error "The received format was not even a string!") =
    Except.ok task

case left.h_2
task : Tasks.Task
x : Status
heq : task.status = undone
⊢ (do
      let name ←
        ((obj
                  (Id.run
                    (RBNode.insert compare
                      (RBNode.insert compare (RBNode.insert compare RBNode.leaf "name" (str task.name)) "desc"
                        (str task.desc))
                      "status" (str "undone")))).getObjValD
              "name").getStr?
      let desc ←
        ((obj
                  (Id.run
                    (RBNode.insert compare
                      (RBNode.insert compare (RBNode.insert compare RBNode.leaf "name" (str task.name)) "desc"
                        (str task.desc))
                      "status" (str "undone")))).getObjValD
              "desc").getStr?
      Task.mk name desc <$>
          match
            (obj
                  (Id.run
                    (RBNode.insert compare
                      (RBNode.insert compare (RBNode.insert compare RBNode.leaf "name" (str task.name)) "desc"
                        (str task.desc))
                      "status" (str "undone")))).getObjValD
              "status" with
          | str "done" => Except.ok done
          | str "undone" => Except.ok undone
          | str "canceled" => Except.ok canceled
          | str other => Except.error (toString "Invalid format: " ++ toString other ++ toString "")
          | x => Except.error "The received format was not even a string!") =
    Except.ok task

case left.h_3
task : Tasks.Task
x : Status
heq : task.status = canceled
⊢ (do
      let name ←
        ((obj
                  (Id.run
                    (RBNode.insert compare
                      (RBNode.insert compare (RBNode.insert compare RBNode.leaf "name" (str task.name)) "desc"
                        (str task.desc))
                      "status" (str "canceled")))).getObjValD
              "name").getStr?
      let desc ←
        ((obj
                  (Id.run
                    (RBNode.insert compare
                      (RBNode.insert compare (RBNode.insert compare RBNode.leaf "name" (str task.name)) "desc"
                        (str task.desc))
                      "status" (str "canceled")))).getObjValD
              "desc").getStr?
      Task.mk name desc <$>
          match
            (obj
                  (Id.run
                    (RBNode.insert compare
                      (RBNode.insert compare (RBNode.insert compare RBNode.leaf "name" (str task.name)) "desc"
                        (str task.desc))
                      "status" (str "canceled")))).getObjValD
              "status" with
          | str "done" => Except.ok done
          | str "undone" => Except.ok undone
          | str "canceled" => Except.ok canceled
          | str other => Except.error (toString "Invalid format: " ++ toString other ++ toString "")
          | x => Except.error "The received format was not even a string!") =
    Except.ok task

Messages here:
174:3:
unsolved goals
case left.h_2
task : Tasks.Task
x : Status
heq : task.status = undone
⊢ (do
      let name ←
        ((obj
                  (Id.run
                    (RBNode.insert compare
                      (RBNode.insert compare (RBNode.insert compare RBNode.leaf "name" (str task.name)) "desc"
                        (str task.desc))
                      "status" (str "undone")))).getObjValD
              "name").getStr?
      let desc ←
        ((obj
                  (Id.run
                    (RBNode.insert compare
                      (RBNode.insert compare (RBNode.insert compare RBNode.leaf "name" (str task.name)) "desc"
                        (str task.desc))
                      "status" (str "undone")))).getObjValD
              "desc").getStr?
      Task.mk name desc <$>
          match
            (obj
                  (Id.run
                    (RBNode.insert compare
                      (RBNode.insert compare (RBNode.insert compare RBNode.leaf "name" (str task.name)) "desc"
                        (str task.desc))
                      "status" (str "undone")))).getObjValD
              "status" with
          | str "done" => Except.ok done
          | str "undone" => Except.ok undone
          | str "canceled" => Except.ok canceled
          | str other => Except.error (toString "Invalid format: " ++ toString other ++ toString "")
          | x => Except.error "The received format was not even a string!") =
    Except.ok task

case left.h_3
task : Tasks.Task
x : Status
heq : task.status = canceled
⊢ (do
      let name ←
        ((obj
                  (Id.run
                    (RBNode.insert compare
                      (RBNode.insert compare (RBNode.insert compare RBNode.leaf "name" (str task.name)) "desc"
                        (str task.desc))
                      "status" (str "canceled")))).getObjValD
              "name").getStr?
      let desc ←
        ((obj
                  (Id.run
                    (RBNode.insert compare
                      (RBNode.insert compare (RBNode.insert compare RBNode.leaf "name" (str task.name)) "desc"
                        (str task.desc))
                      "status" (str "canceled")))).getObjValD
              "desc").getStr?
      Task.mk name desc <$>
          match
            (obj
                  (Id.run
                    (RBNode.insert compare
                      (RBNode.insert compare (RBNode.insert compare RBNode.leaf "name" (str task.name)) "desc"
                        (str task.desc))
                      "status" (str "canceled")))).getObjValD
              "status" with
          | str "done" => Except.ok done
          | str "undone" => Except.ok undone
          | str "canceled" => Except.ok canceled
          | str other => Except.error (toString "Invalid format: " ++ toString other ++ toString "")
          | x => Except.error "The received format was not even a string!") =
    Except.ok task
Messages below:
Messages above:

lorã (Apr 15 2025 at 03:16):

So i'm inside a Except String _ do

lorã (Apr 15 2025 at 03:17):

That was my try: 

theorem parser_task_correctness :
  (∀ (task : Task), (fromJson? ∘ toJson) task = .ok task) ∧
  ∀ (task? : Json),
  (match (fromJson? task? : Except String Task) with
   | .ok task => toJson task
   | .error _   => task?) = task?
   := by {

   constructor
   · intro task
     simp [toJson, fromJson?, mkObj, getObjValAs?, str, parser_task_correctness]
     split

     admit
}

lorã (Apr 15 2025 at 10:46):

theres a link if it can help

Aaron Liu (Apr 15 2025 at 11:19):

do is syntax sugar for >>=

Yaël Dillies (Apr 15 2025 at 11:22):

Aaron, what do you mean? It's a syntax sugar for many things! (a syntax cake, maybe?)

Aaron Liu (Apr 15 2025 at 11:28):

I mean when the pp pprints

do
  let x ← y
  z

then that means you are looking at y >>= fun x => do z

Aaron Liu (Apr 15 2025 at 11:28):

And I think that's the only way to get the pp to output a do

Edward van de Meent (Apr 15 2025 at 11:29):

i wonder if something like an option pp.doNotation might be useful

Edward van de Meent (Apr 15 2025 at 11:31):

i guess you can do pp.notation false, but then you also see bind instead of >>=

Robin Arnez (Apr 18 2025 at 08:39):

From what I can see you are asking something impossible in parser_task_correctness:
Let's say task? : Json is {"status": "done", "name": "Hello, World!", "desc": "ABC"}, then we parse it and convert it back to Json: {"name": "Hello, World!", "desc": "ABC", "status": "done"} (which is different!). It gets worse when the input json contains redundant information: {"status": "done", "name": "Hello, World!", "desc": "ABC", "uhh": "why not"} which gets removed when doing fromJson and toJson.

Last updated: Feb 28 2026 at 14:05 UTC