proposition: Theorem find_all_correct: forall s s1, refine s s1 -> (sudoku s1 <-> In s1 (find_all s)).
proof: Proof. intros s s1 Hs; unfold find_all. assert (F0: length s = size * size). case Hs; intuition. match goal with |- context [find_all_aux ?X ?Y ?Z] => case (find_all_aux_sat X Y Z); auto with arith end. apply gen_init_clauses_valid; auto. apply gen_init_clauses_ordered; auto. intros V1 (V2, V3); split; intros V4. case (V3 s1); auto. case (invariant_gen_init_clauses s); auto. intros _ (_, (_, tmp)); case (tmp s1); auto; clear tmp. intros s2 (V5, V6). case (V2 s2); auto. intros V7 V8. case (invariant_gen_init_clauses s); auto. intros _ (_, (_, tmp)); case (tmp s2); auto; clear tmp. intros _ tmp; generalize (tmp V8); clear tmp V8; intros V8. replace s1 with s2; auto. apply sudoku_refine_id; auto. case (V2 s1); auto; intros V5 V6. case (invariant_gen_init_clauses s); auto. intros _ (_, (_, tmp)); case (tmp s1); auto; clear tmp. Qed.
imports: List UList Permutation Div OrderedList ListOp Lia