## 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):

Adding `apply (subst index_update)` leads to this proof state:

`````` 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 ⇒ 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_int`can 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