Assumption about finite set cardinality not being considered · General

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"
  by (simp add: update_def)

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.

Stream: General

Topic: Assumption about finite set cardinality not being considered

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

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

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

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