Stream: new members

Topic: Impossible cases for an inductive type constructor

Ömer Şakar (Jan 21 2021 at 18:53):

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 (Jan 21 2021 at 18:58):

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 (Jan 21 2021 at 18:59):

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

Ömer Şakar (Jan 21 2021 at 19:25):

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 (Jan 21 2021 at 19:36):

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?

src#option.get

Mario Carneiro (Jan 21 2021 at 19:48):

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 (Jan 21 2021 at 19:49):

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

Mario Carneiro (Jan 21 2021 at 19:50):

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 (Jan 21 2021 at 19:50):

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 (Jan 27 2021 at 19:44):

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 (Jan 27 2021 at 19:44):

MWE coming in a bit

Ömer Şakar (Jan 27 2021 at 19:55):

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 (Jan 27 2021 at 20:00):

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 (Jan 27 2021 at 20:16):

Ö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 (Jan 27 2021 at 20:19):

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 (Jan 27 2021 at 20:25):

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

Yakov Pechersky (Jan 27 2021 at 20:25):

No lemma showing that

Anne Baanen (Jan 27 2021 at 20:29):

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 (Jan 27 2021 at 20:31):

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 (Jan 27 2021 at 20:33):

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

Mario Carneiro (Jan 27 2021 at 20:36):

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 (Jan 27 2021 at 20:37):

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 (Jan 27 2021 at 20:38):

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

Mario Carneiro (Jan 27 2021 at 20:41):

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 (Jan 27 2021 at 20:53):

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 (Jan 27 2021 at 20:54):

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 (Jan 27 2021 at 21:01):

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 (Jan 27 2021 at 21:39):

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 (Jan 27 2021 at 21:49):

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 (Jan 27 2021 at 22:00):

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 (Jan 27 2021 at 22:00):

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 (Jan 27 2021 at 22:07):

Ö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 (Jan 27 2021 at 22:13):

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)

Last updated: May 13 2021 at 04:21 UTC