2

While reading this answer on quotient types, I stumbled upon the construct "case _ of _ ⇒ _". Upon checking the manual, there's no such definition, but there are separate definitions for "case _" (§6.5.1) and "of _" (§6.4.3). Nonetheless, reading these definitions only confused me more about the meaning of this construct.

Consequently, I decided to come up with a simpler version of the lemma that I might be able to prove, which was this one:

lemma test: "(case n of (0::nat,0::nat) ⇒ (a,b) = n) ⟹ a = 0 ∧ b = 0"

In my head, after analyzing the context of the mentioned question, this statement should be equivalent to "(a,b) = (0,0) ⟹ a = 0 ∧ b = 0", which should be trivial to prove. Well, sledgehammer begs to differ:

"cvc4": Timed out 
"z3": Timed out 
"e": Timed out 
"spass": Timed out 
"remote_vampire": The prover gave up

So it seems like I'm misunderstanding what this construct is meant to represent.

In light of that, what is the meaning of the statement "case _ of _ ⇒ _" in Isabelle?

Luiz Martins
  • 1,644
  • 10
  • 24
  • After some study, I realize the statement above does not mean what I first thought. For those interested, this is the correctly written version of my example statement: `lemma test_correct: "(case n of (a,b) ⇒ (a,b) = (0,0)) ⟹ n = (0,0)" by blast` – Luiz Martins Apr 26 '21 at 14:41

2 Answers2

2

In Isabelle, a statement of the type case _ of _ ⇒ _ | _ ⇒ _ | _ ⇒ _ | ... is a form of pattern matching.

You might want to take a look at §2.5.4 of Isabelle's tutorial (§2.5.5 and §2.5.6 are also useful). This question on pattern matching and the Wikipedia article may provide more information about pattern matching in general.

What you are missing is that there not guarantee that the patterns are exhaustive. If no pattern matches, the result is undefined.

Nitpick actually finds a counter-example automatically on your lemma:

Nitpicking formula... 
Kodkod warning: Interrupt 
Nitpick found a counterexample:
  Free variables:
    a = 1
    b = 0
    n = (0, 1)

Let's plugin back the value of n:

lemma ‹(case (0,1) of (0::nat,0::nat) ⇒ (a,b) = n)⟹ a = 0 ∧ b = 0›
  apply simp
(*
proof (prove)
goal (1 subgoal):
 1. undefined ⟹ a = 0 ∧ b = 0
*)

EDIT, to answer the question below: (case (0,1) of (0::nat,0::nat) ⇒ (a,b) = n) means roughly [1]:

(case_prod (0,1) of 
   (0::nat,0::nat) ⇒ (a,b) = n
 | _               ⇒ undefined)

where case_prod is the destructor for pairs. Hence, if you don't match any of the patterns, the result is undefined.

[1] full output:

ML ‹@{term ‹(case (0,1) of (0::nat,0::nat) ⇒ (a,b) = n)›}›
Luiz Martins
  • 1,644
  • 10
  • 24
Mathias Fleury
  • 2,221
  • 5
  • 12
  • Although you found the problem in my example, I'd appreciate a high level description of what the statement "`case _ of _`" actually means, as "`case (0,1) of (0::nat,0::nat)`" doesn't even make sense to me (maybe you can use it as an example in the explanation). I'm actually slightly more confused than before. – Luiz Martins Apr 24 '21 at 19:55
  • I thought that `If no pattern matches, the result is undefined.` would answer your question. I will extend my answer. – Mathias Fleury Apr 25 '21 at 04:47
  • I wasn't aware that `case _ of _` was used for pattern matching in Isabelle. I've suggested an edit to clarify and to add some further resources for future readers about Isabelle's case expressions and pattern-matching in general. – Luiz Martins Apr 25 '21 at 10:25
  • I am curious now: what did you expect that case was doing that is not pattern matching? – Mathias Fleury Apr 25 '21 at 13:23
  • I had no expectations. When I saw pattern matching, in both *Coq* and *Isabelle*, I only saw it with the syntax `fun _ where _` or `match _ with _`, but never `case _ of _`, so I just didn't know what it meant. – Luiz Martins Apr 25 '21 at 14:17
1

As mentioned, nitpick is helpful here. Luckily the fix is simple.

lemma test: "(case n of (0::nat,0::nat) ⇒ (a,b) = n | _ ⇒ False) ⟹ a = 0 ∧ b = 0"

Because you don't bind any variables, rewriting your hypothesis into a conditional statement is trivial. Finally, you might want to look into the concept of pattern matching, specifically in the context of functional programming.

lemma test': "(case n of (0::nat,0::nat) ⇒ (a,b) = n | _ ⇒ (a,b) = (0,0)) = ((a,b) = (0,0))"

lemma test'': "(case n of (0::nat,0::nat) ⇒ (a,b) = n) = (if n = (0,0) then (a,b) = n else undefined)"
user14704889
  • 116
  • 2