Impossible cases for an inductive type constructor

Stream: new members

[Ömer Şakar]

Is it possible to prove that a case for a function is impossible?

Suppose you define a map (or dictionary in Python) as a list of key/value pairs (see the definition below).

inductive map {α β: Type} : Type
| nil : map
| build (a:α) (b:β) (m: map): map

I could define a function that, given a key k, returns me the value v that is associated with that key (see definition below). This function would probably use an option type in case the key is not in the map.

def mget {α β: Type*} [decidable_eq α] (k: α): @map α β → option β
| map.nil             := option.none
| (map.build k1 v1 m) := if k1 = k then option.some v1 else mget m

But if I know that key k is in the keyset of this map (see the function below that returns the keyset), I know it is impossible that mget returns none.

def keys {α β: Type} [has_union (finset α)] [decidable_eq α] : @map α β → finset α
| map.nil := ∅
| (map.build k _ m) := has_insert.insert k (keys m)

The reason I want to define such a function is that, if I have a prove for (mget k m).is_some (where k is a key, m is a map). I can use option.get on that proof to return me something (with the type of the values). But don't think I can reason about that value, which is what I need. Right? For this question I do not know whether this last statement is true or not, but my attempts at proving something using mget almost always return in a goal that looks like

option.get _ \in keys m

(where _ is (mget k m).is_some)

[Mario Carneiro]

Yes it is possible to prove that cases are impossible, and option.get is an example. You should see how it is implemented - it cases on the option and then proves that the none case yields false

[Mario Carneiro]

[has_union (finset α)] <-- you don't want this

[Ömer Şakar]

Aa, the answer was closer than I thought. I will try that, don't know what the none case for option.get exactly says, but I can figure it out.
thakn you!

[Ömer Şakar]

Btw, why wouldn't I want [has_union (finset \a)]? Maybe I am reading it wrong, but this says that you can do somefinset \union otherfinset, which should be fine right?

[Mario Carneiro]

src#option.get

[Mario Carneiro]

There is already a definition of has_union (finset A). By asking for a different one it might not have the right properties, for example it might say that the union of any two finsets is empty, in which case your theorems won't be provable

[Mario Carneiro]

if you just delete that typeclass argument you will still be able to use union on finsets

[Mario Carneiro]

Also map should take its type arguments explicitly, i.e. inductive map (α β: Type) : Type. They can't be inferred from context which is why you are having to write @map α β all the time

[Mario Carneiro]

As for your actual question, could you give a #mwe with the theorem you want to prove? It's a little vague what the problem is

[Ömer Şakar]

Let me first explain the context of the question before giving the mwe. I am taking a course called Logical Verification (Jasmin Blanchette as the teacher). This is part of the project I am working on for that course. He mentioned that i could ask question here. So, I am trying to ask questions about smaller problems I have (I feel like I should at least mention this, just so it does not look suspicious or anything). I will mention your name if I use anything you post here.

[Ömer Şakar]

MWE coming in a bit

[Ömer Şakar]

Again I want to stress that I do not want a the proof (as that would be cheating), but I was allowed to ask questions regarding smaller problems.

So my MWE is here, it is a bit long though

import data.set.finite
import data.finset
open finset multiset
namespace mapfuncs

inductive map {α β: Type} : Type*
| nil : map
| build (a:α) (b:β) (m: map): map

def values {α β: Type} : @map α β → list β
| map.nil := []
| (map.build a b m) := [b] ++ values m

def keys {α β: Type} [has_union (finset α)] [decidable_eq α] : @map α β → finset α
| map.nil := ∅
| (map.build k _ m) := has_insert.insert k (keys m)


def mget {α β: Type*} [decidable_eq α] (k: α): @map α β → option β
| map.nil             := option.none
| (map.build k1 v1 m) := if k1 = k then option.some v1 else mget m

def keygetfromvalue {α β: Type} [decidable_eq β] (v: β) : @map α β → option α
| map.nil := option.none
| (map.build k v1 m) := if v1 = v then option.some k else keygetfromvalue m

def keygetfromvaluesome{α β: Type*} [decidable_eq β] (v: β) (m: @map α β) (h: option.is_some (keygetfromvalue v m)): α
:= option.get h

lemma lemma_to_proof {α β: Type} [decidable_eq α] [decidable_eq β] (v: β) (m: @map α β) :
  v ∈ (values m) → (∃ k: α, k ∈ (keys m) ∧ (mget k m) = (option.some v)) :=
  begin
      intro hvinvalm,
      apply exists.intro (keygetfromvaluesome v m (by sorry)), -- I do have a proof here, but it involves a longer lemma.
      apply and.intro,
      {
        simp[keygetfromvaluesome],
          -- αβ: Type
          -- _inst_1: decidable_eq α
          -- _inst_2: decidable_eq β
          -- v: β
          -- m: map
          -- hvinvalm: v ∈ values m
          -- ⊢ option.get _ ∈ keys m
        sorry -- The problem is the state here. I can't get any info on the key itself.
      },
      {
        simp[keygetfromvaluesome],-- same problem here
        sorry,
      }
  end
end mapfuncs

[Ömer Şakar]

The map inductive type is the same, for completeness sake I have included the definitions of values and keys (but I do not think they matter in this case). I gave a different example here, but the problem is the same.

Now I want to define a function (which I call keygetfromvalue) that, given a value v, gets a key associated with that value. When i use that function in my proof I get the problem that I have a goal that looks like option.get _ \in someset (see the two "sorry"s in the lemma_to_proof). Now I want to define a new function (lets call that valuetokey) that given a value v and a proof that there is a key associated with it, returns me v (so not option.some v).

[Anne Baanen]

Ömer Şakar said:

Let me first explain the context of the question before giving the mwe. I am taking a course called Logical Verification (Jasmin Blanchette as the teacher).

Now where have I heard that name before? :)

[Anne Baanen]

My first instinct is that you might be able to use case distinction on m, like in keygetfromvalue to prove that ↥((keygetfromvalue v m).is_some) implies that option.get this is in the keys.

[Yakov Pechersky]

Yes, but unfortunately the way that map is defined, there is no connection between a and b currently.

[Yakov Pechersky]

No lemma showing that

[Anne Baanen]

Right, it would probably have to be in the form of a new lemma (couple of new lemmas?) proved by pattern matching. Basically what I mean is duplicate keygetfromvalue but return a proof instead of a key.

[Yakov Pechersky]

lemma lemma_to_proof {α β: Type} [decidable_eq α] [decidable_eq β] (v: β) (m: @map α β) :
  v ∈ (values m) → (∃ k: α, k ∈ (keys m) ∧ (mget k m) = (option.some v)) :=
  begin
    induction m with a b m hm generalizing v,
    { simp [values] }, -- false because we would have `v ∈ values map.nil`
    { simp only [values, keys, mem_insert, list.mem_cons_iff, list.singleton_append],
      rintro (rfl | H),
      { use a,
        simp [mget] },
      { obtain ⟨k, hk, hv⟩ := hm _ H,
        use k,
        simp [hk, hv, mget],
        sorry -- you can't prove this because there is no relationship between `b` and `v`
      },
    }
  end

[Yakov Pechersky]

That is because map.build 0 1 (map.build 0 0 map.nil) has values = [0, 1] but keys = {0}!

[Mario Carneiro]

Here's how I suggest you set this up:

import data.set.finite
import data.finset

namespace mapfuncs

inductive map (α β: Type) : Type
| nil : map
| build (a:α) (b:β) (m: map): map

def map.values {α β: Type} : map α β → list β
| map.nil := []
| (map.build a b m) := [b] ++ m.values

def map.keys {α β: Type} [decidable_eq α] : map α β → finset α
| map.nil := ∅
| (map.build k _ m) := insert k m.keys

def map.get {α β: Type*} [decidable_eq α] (k: α): map α β → option β
| map.nil             := none
| (map.build k1 v1 m) := if k1 = k then some v1 else map.get m

def map.by_value {α β: Type} [decidable_eq β] (v: β) : map α β → option α
| map.nil := none
| (map.build k v1 m) := if v1 = v then some k else map.by_value m

/-
def map.get_by_value {α β: Type*} [decidable_eq β]
  (v: β) (m: map α β) (h: option.is_some (map.by_value v m)) : α :=
option.get h
-/

lemma map.mem_by_value {α β: Type} [decidable_eq α] [decidable_eq β] {k v} {m : map α β} :
  k ∈ m.by_value v → v ∈ m.get k :=
by induction m; sorry

lemma map.mem_keys {α β: Type} [decidable_eq α] {k} {m : map α β} :
  k ∈ m.keys ↔ ∃ v, v ∈ m.get k :=
by induction m; sorry

lemma map.mem_values {α β: Type} [decidable_eq α] {v} {m : map α β} :
  v ∈ m.values ↔ ∃ k : α, v ∈ m.get k :=
by induction m; sorry

end mapfuncs

[Mario Carneiro]

I removed the k ∈ (keys m) conjunct from map.mem_values because it's implied by the second conjunct v ∈ m.get k

[Mario Carneiro]

You don't need the keygetfromvaluesome function at all for these proofs, so it's commented out

[Mario Carneiro]

Actually, now that I come to think about it, it's possible to prove map.mem_values directly by induction on m, rather than splitting the forward and reverse directions into two theorems

[Ömer Şakar]

Anne Baanen said:

Right, it would probably have to be in the form of a new lemma (couple of new lemmas?) proved by pattern matching. Basically what I mean is duplicate keygetfromvalue but return a proof instead of a key.

Hi Anne, long time no see:)

[Ömer Şakar]

Yakov Pechersky said:

Yes, but unfortunately the way that map is defined, there is no connection between a and b currently.

Hmm I thought that if they are within the same constructor case, that that would be the association. But I guess not... (I only realize that now).

[Ömer Şakar]

Mario Carneiro said:

Here's how I suggest you set this up:

Interesting. So if I understand it correctly, is the difference with my approach that I rely on a proof (from which you cannot extract any info) and your approach (besides looking more structured) associates the map.by_value and map.get functions?

[Mario Carneiro]

The main point with these lemmas is to have something that can be proven straightforwardly by induction. Once you have them you can use them to prove theorems about the get_by_value function if you want:

lemma map.get_by_value_mem_keys {α β: Type} [decidable_eq α] [decidable_eq β]
  {v} {m : map α β} (h) : m.get_by_value v h ∈ m.keys :=
map.mem_keys.2 ⟨_, map.mem_by_value (option.get_mem _)⟩

[Mario Carneiro]

Also as pointed out by Yakov, some of these theorems aren't true because there is no constraint on m having unique keys. You might find it easier to work with the relation (k, v) ∈ m.entries in place of v ∈ m.get k in the theorems, where

def map.entries {α β: Type} : map α β → list (α × β)
| map.nil := []
| (map.build a b m) := (a, b) :: m.entries

[Ömer Şakar]

The reason I did not constraint m on having unique keys is that I wanted to model a map as a list of entries. The keyset has unique keys (because by definition elements in a set a unique).

[Ömer Şakar]

Mario Carneiro said:

The main point with these lemmas is to have something that can be proven straightforwardly by induction. Once you have them you can use them to prove theorems about the get_by_value function if you want:

lemma map.get_by_value_mem_keys {α β: Type} [decidable_eq α] [decidable_eq β]
  {v} {m : map α β} (h) : m.get_by_value v h ∈ m.keys :=
map.mem_keys.2 ⟨_, map.mem_by_value (option.get_mem _)⟩

Hmmm, i think i get what you mean, I will try it out. Thank you (Anne and Yakov) a lot!

[Yakov Pechersky]

Ömer Şakar said:

The reason I did not constraint m on having unique keys is that I wanted to model a map as a list of entries. The keyset has unique keys (because by definition elements in a set a unique).

The keyset as defined by map.keys is unique, but you're still able to construct that keys = {0}, values = [0, 1] map, where, depending on how you define retrieval function, some of those values might be unreachable

[Mario Carneiro]

One way to express that the map has unique keys using the map.keys finset is m.keys.card = m.values.length, although that's not the most convenient. If map.keys was a list then you could say m.keys.nodup to express that there are no duplicate keys (and hence you can upgrade this list to a finset without losing duplicate elements)