deepspec / dsss18 Goto Github PK

I think it should be mentioned somewhere that following QuickChick volume require installing quickchick library. Sorry if I missed them. Installation instructions at https://github.com/QuickChick/QuickChick worked for me.

actully instead of actually

Consider following lemma:

Definition elements_property (t: tree) (cts: total_map V) : Prop :=
   forall k v,
    (In (k,v) (elements t) -> cts (int2Z k) = v) /\
    (cts (int2Z k) <> default -> In (k, cts (int2Z k)) (elements t)).
Theorem elements_relate:
  forall t cts,
  SearchTree t ->
  Abs t cts ->
  elements_property t cts.

This lemma does not seem provable. Specifically, the second conjunction:

 (cts (int2Z k) <> default -> In (k, cts (int2Z k)) (elements t)

is not provable in the case where k is found in the tree. In that time, the premises will look like

t = T _ l (int2Z k0) (cts (int2Z k0)) r
int2Z k0 = int2Z k

while the goal is

In (k, cts (int2Z k)) [(k0, cts(int2Z k0)]

since int is a postulated type, we cannot prove k = k0.

For this reason, I propose to use

cts (int2Z k) <> default -> exists k', int2Z k = int2Z k' /\ In (k', cts (int2Z k)) (elements t)

to be the goal instead. This new goal is weakened, such that any k' in the same fibre as k w.r.t int2Z will work, and I've proved this lemma with this modified goal instead.

Another way to fix it is to postulate int2Z is injective. However, this is quite a strong axiom to introduce (though no inconsistency introduced).

Please confirm if the original goal can be proved and if not, my proposed goal is a good idea or not. I can raise a PR if it's OK.