## Stream: General

### Topic: Assumption about finite set cardinality not being considered

#### Alex Weisberger (Dec 30 2021 at 22:14):

I have the following lemma that I was expecting to be used to simplify a proof goal:

lemma index_update[simp]:
"n < CARD('b::finite) ⟹ index (update (f::'a['b]) n x) n = x"

This lemma is a part of the C-to-Isabelle parser, and as you can see is marked as a simplification rule by default. I have the following proof goal that is not considering this rule, and I'm wondering why:

1. ⋀s. 0 ≤ i ⟹
i < 10 ⟹
client_orders_'' s.[unat (word_of_int i)] = NOT_CACHED ⟹
server_orders.[unat (word_of_int i)] =
Arrays.update (client_orders_'' s) (unat (word_of_int i))
(server_orders.[unat (word_of_int i)]).[unat (word_of_int i)]

This is a translation of some C code where client_orders and server_orders are both arrays of size 10. The index being used to read values out of these arrays is i, and the assumptions here show that i is between 0 and 10, i.e. i < 10. Intuitively I would expect this rule to apply here, since this proof goal is just showing that the client_orders array is being updated to contain the value at i in server_orders.

Of course, I see that the proof goal is not in the exact same shape as the lemma - there is an additional assumption here, namely:

client_orders_'' s.[unat (word_of_int i)] = NOT_CACHED

Is this what's preventing the simplification rule from being considered? Some background, this assumption is coming from an if statement in the C code that I've parsed. There are actual 2 proof goals here, the other one being the else case of the code. Can that be used to aid in the proof?

I also am thinking that because i is an int, it is not finite, so that may also be causing the lemma to not be used.

#### Manuel Eberl (Jan 02 2022 at 17:00):

What happens if you do apply (subst index_update)? If it doesn't work, try putting a using [[show_sorts, unify_trace_failure]] before it and check the output.

#### Alex Weisberger (Jan 02 2022 at 20:05):

1. s::lifted_globals.
(0::int)  i
i < (10::int)
client_orders_'' s.[unat (word_of_int i)] = NOT_CACHED
unat (word_of_int i) < CARD(10)
2. s::lifted_globals.
(0::int)  i
i < (10::int)
client_orders_'' s.[unat (word_of_int i)] = NOT_CACHED
server_orders.[unat (word_of_int i)] =
server_orders.[unat (word_of_int i)]
3. s::lifted_globals.
(0::int)  i
i < (10::int)
client_orders_'' s.[unat (word_of_int i)]  NOT_CACHED
server_orders.[unat (word_of_int i)] =
client_orders_'' s.[unat (word_of_int i)]

It looks like it introduces a new goal, #1, but makes #2 trivial (apply(auto) afterwards discharges that goal).

I think adding using [[show_sorts, unify_trace_failure]] is showing that there's a type mismatch somewhere, here's part of the output:

The following types do not unify:
32 word[10] ⇒ nat ⇒ 32 word
(nat ⇒ 32 word)[?'b::finite] ⇒ nat ⇒ nat ⇒ 32 word

There are other similar errors, but there's quite a bit of output - I won't post it all unless you think it's helpful.

I'm assuming there's a type issue with subgoal 1: unat (word_of_int i) < CARD(10). CARD is defined in the Cardinality theory as:

translations "CARD('t)" => "CONST card (CONST UNIV :: 't set)"

I've honestly never seen a definition like this so I don't know how to interpret it.

#### Manuel Eberl (Jan 02 2022 at 20:17):

Hm, depending on where you got that goal from, one possibility might be that the polymorphism of word_of_int is the problem here. word_of_int probably has a type something like int ⇒ 'a :: finite word, so if you just write unat (word_of_int n) in two different places, Isabelle will infer the most general situation, which is that the two occurances of word_of_intcan have different bit-width.

Type annotations to fix the bit width here would help with that.

Last updated: Aug 15 2022 at 02:13 UTC