list_solve problems with sorted lists

[andrew-appel]

The zlist solver list_solve has some trouble with sorted lists. In the examples below:

• example1 demonstrates a successful (but a bit slow) solve
• example2 is successful but a bit slow
• example3 has an issue: list_solve fails, list_simplify succeeds leaving an easy rep_lia goal; perhaps list_solve should have solved this (or list_simplify should not have left this easy subgoal).
• example4 has a definite bug: list_solve should not leave those subgoals.
• example5 demonstrates that in the presence of a complex sorted hypothesis such as sorted Z.le (0 :: (r :: row_ptr) ++ [m])), the solver fails. On the other hand, when we split up the hypothesis by means of my new tactic split_sorted, the solver can succeed in some cases, and faster. This example demonstrates other problems as well, if you look at all the Fail commands.

Require Import VST.floyd.proofauto.
Import ListNotations.

Lemma example1: 
 forall
  (mval : list (list byte))
  (cols : Z)
  (vals : list byte)
  (col_ind : list Z)
  (r : Z)
  (row_ptr : list Z)
  (L : Zlength row_ptr + 1 = 1 + (Zlength mval + 1))
  (L0 : Zlength vals = Znth (Zlength mval) row_ptr)
  (L1 : Zlength col_ind = Znth (Zlength mval) row_ptr)
  (COL : Forall (fun j : Z => 0 <= j < cols) col_ind)
  (SORT : sorted Z.le (0 :: (r :: row_ptr) ++ [Int.max_unsigned]))
  (H0 : 0 <= r),
Zlength (sublist r (Zlength vals) vals) = 
Znth (Zlength mval) row_ptr - r.
Proof.
Time list_solve. (* 5.337 sec *)
Qed.

Lemma example2: forall
 (mval : list (list byte))
 (cols : Z)
 (col_ind : list Z)
 (r : Z)
 (row_ptr : list Z)
 (L : Zlength row_ptr + 1 = 1 + (Zlength mval + 1))
 (L1 : Zlength col_ind = Znth (Zlength mval) row_ptr)
 (COL : Forall (fun j : Z => 0 <= j < cols) col_ind)
 (SORT : sorted Z.le (0 :: (r :: row_ptr) ++ [Int.max_unsigned]))
 (H0 : 0 <= r),
Zlength (sublist r (Zlength col_ind) col_ind) = 
Znth (Zlength mval) row_ptr - r.
Proof.
Time list_solve.  (* 9.3 sec *)
Time Qed.   (* 1.255 sec *)

Lemma example3: forall
 (r : Z)
 (row_ptr : list Z)
 (SORT : sorted Z.le (0 :: (r :: row_ptr) ++ [Int.max_unsigned]))
 ( H0 : 0 <= r)
 (i j : Z)
 (H1 : 0 <= i <= j)
 (H2 : j < Z.succ (Zlength row_ptr + 1)),
Znth i
  (0 :: map (fun i0 : Z => i0 - r) row_ptr ++ [Int.max_unsigned]) <=
Znth j
  (0 :: map (fun i0 : Z => i0 - r) row_ptr ++ [Int.max_unsigned]).
Proof.
Fail Time list_solve.
Time list_simplify. (* 19 seconds *)
     (* BUG! in list_solve / list_simplify: one of the tactics is leaving
         this trivial subgoal.  Please report. *) 
rep_lia.
Time Qed. (* 2 seconds*)

Lemma example4: forall 
 (mval : list (list byte))
 (cols : Z)
 (col_ind : list Z)
 (r : Z)
 (row_ptr : list Z)
 (L : Zlength row_ptr + 1 = 1 + (Zlength mval + 1))
 (L1 : Zlength col_ind = Znth (Zlength mval) row_ptr) 
( COL : Forall (fun j : Z => 0 <= j < cols) col_ind)
 (SORT : sorted Z.le (0 :: (r :: row_ptr) ++ [Int.max_unsigned])) 
 (j : Z) 
 (H0 : 0 <= r) 
 (H1 : 0 <= j < Zlength mval),
sublist (Znth j row_ptr) (Znth (j + 1) row_ptr) col_ind = 
sublist (Znth j (map (fun i : Z => i - r) row_ptr))
  (Znth (j + 1) (map (fun i : Z => i - r) row_ptr))
  (sublist r (Zlength col_ind) col_ind).
Proof.
intros.
Time list_solve. (* 17.5 seconds *)
(* Bug: there should not be subgoals *)
Time list_solve.  (* 2.23 seconds *)
Time list_solve.  (* 1.95 seconds *)
Time Qed. (*  2.8 sec *)

Lemma sorted_cons_e:
 forall {T: Type} {INH: Inhabitant T} (le: T -> T -> Prop) (a: T) (bl: list T),
  0 < Zlength bl  -> 
 sorted le (a::bl) -> 
  le a (Znth 0 bl) /\ sorted le bl.
Proof.
intros.
split.
apply (H0 0 1).
split. lia. rewrite Zlength_cons by lia. lia.
intros i j [? ?]. specialize (H0 (i+1) (j+1)).
rewrite !Znth_pos_cons in H0 by lia.
rewrite !Z.add_simpl_r in H0.
rewrite Zlength_cons in H0.
apply H0; split; lia.
Qed.

Lemma sorted_app_e:
 forall {T: Type} {INH: Inhabitant T} (le: T -> T -> Prop) (al bl: list T),
  0 < Zlength al  -> 
  0 < Zlength bl  -> 
 sorted le (al++bl) -> 
  le (Znth (Zlength al - 1) al) (Znth 0 bl) /\ sorted le al /\ sorted le bl.
Proof.
intros.
split3.
specialize (H1 (Zlength al - 1) (Zlength al)).
autorewrite with sublist in H1.
apply H1. Zlength_solve.
intros i j [? ?]. specialize (H1 i j). autorewrite with sublist in H1. apply H1; lia.
intros i j [? ?]. specialize (H1 (Zlength al + i) (Zlength al + j)).
   autorewrite with sublist in H1. apply H1; lia.
Qed.

Ltac split_sorted SORT := 
repeat (
try change ((?a::?bl)++?cl) with (a::(bl++cl)) in SORT;
first [let H := fresh in 
         apply sorted_cons_e in SORT; [ |  Zlength_solve];
         destruct SORT as [H SORT];
         autorewrite with sublist in H
        | let H := fresh in let H' := fresh in 
          apply sorted_app_e in SORT; [ |  Zlength_solve ..];
          destruct SORT as [H [H' SORT]];
          autorewrite with sublist in H, H'
        | match type of SORT with sorted _ [_] => clear SORT end]).

Lemma example5: forall 
 (N cols r j : Z)
 (col_ind row_ptr : list Z)
 (L : Zlength row_ptr = N + 1)
 (L1 : Zlength col_ind = Znth N row_ptr) 
 (COL : Forall (fun j : Z => 0 <= j < cols) col_ind)
 (SORT : sorted Z.le (0 :: (r :: row_ptr) ++ [Int.max_unsigned])) 
 (H1 : 0 <= j < N),
  sublist (Znth j row_ptr) (Znth (j + 1) row_ptr) col_ind = 
  sublist (Znth j row_ptr - r) (Znth (j + 1) row_ptr - r)
                      (sublist r (Zlength col_ind) col_ind).
Proof.
intros.
Time Fail rewrite sublist_sublist by list_solve. (* 6 to 8 seconds: Proof search failed *)
Time Fail list_solve.  (*  7.6 seconds: "Proof search failed" *)
Time split_sorted SORT. (* 0.1 second s*)
Fail Time list_solve. (* 6.6 seconds: "Stack overflow" *)
Time rewrite sublist_sublist by list_solve. (* 4 seconds *)
Time list_solve. (* 0.16 seconds *)
Time Qed.  (* 0.16 seconds *)

[QinshiWang]

example1 and example2 are performance issues. The performance is not so bad, so it is not a high priority.

example3 is about whether to include rep_lia in list_solve. Our design choice is that list_solve should not depend on other parts of VST, which include rep_lia. Another consideration is performance: if rep_lia is not much slower than lia, then it is like calling lia twice. This overhead might be okay. Then we can add it to list_solve in floyd/functional_base.v using a hook in list_solve.

[QinshiWang]

example4 is a bug in list_solve's internal mechanism. apply_list_ext is an internal tactic to apply extensionality to lists. It used to fail when the array length goals in extensionality are not directly provable. I have updated the tactic and will push it so the array length goals will go through the same proof procedure as the main goal.

[QinshiWang]

example5 is about instantiation choice. The completeness of list_solve requires instantiating with the bound set. For example, if we have forall_range 0 n a P, we always need to instantiate to P (a[0]) and P (a[n-1]). This is costly and not often useful, so this instantiation is disabled by Ltac instantiate_bound_set := false by default. I tested as follows. It solves but takes a long time.

Lemma example5: forall 
 (N cols r j : Z)
 (col_ind row_ptr : list Z)
 (L : Zlength row_ptr = N + 1)
 (L1 : Zlength col_ind = Znth N row_ptr) 
 (COL : Forall (fun j : Z => 0 <= j < cols) col_ind)
 (SORT : sorted Z.le (0 :: (r :: row_ptr) ++ [Int.max_unsigned]))
 (H1 : 0 <= j < N),
  sublist (Znth j row_ptr) (Znth (j + 1) row_ptr) col_ind =
  sublist (Znth j row_ptr - r) (Znth (j + 1) row_ptr - r)
                      (sublist r (Zlength col_ind) col_ind).
Proof.
intros.
rewrite sublist_sublist.
- admit.
Ltac instantiate_bound_set ::= true.
- Time list_simplify. (* 56.665 secs *)
Abort.

Therefore, it is good to tune for sortedness. Your tactic is a plan.