proposition: Theorem all_cell_sat: forall s, sat all_cell s <-> forall p, valid_pos p -> In (get p s) ref_list.
proof: Proof. unfold all_cell, sat; intros s; split. intros H (x, y) (H1, H2). case (H (length (gen_cell (Pos x y))) (gen_cell (Pos x y))). apply fold_clause_insert3; auto. case (cross2_correct (Pos x y)); intros _ tmp; apply tmp; clear tmp; auto. split; auto. intros l (Hl1, Hl2). case (gen_cell_correct l x y); auto. intros tmp _; case tmp; auto; clear tmp Hl1. intros z (Hz1, Hz2); subst; simpl in Hl2. rewrite Hl2; auto. intros H n c H1. case fold_clause_insert1 with (1 := H1); clear H1. intros ((x, y), (n1, (H2, H3))); injection H3; intros Eq1 E2; clear H3. subst. case (cross2_correct (Pos x y)); intros tmp _; case (tmp H2); clear tmp H2; intros H3 H4. exists (L (Pos x y) (get (Pos x y) s)); split. case (gen_cell_correct (L (Pos x y) (get (Pos x y) s)) x y); auto. intros H1 H2; apply H2; clear H1 H2; simpl; auto. exists (get (Pos x y) s); split; auto. apply H; split; auto. simpl; auto. simpl; intros H1; case H1. Qed.
imports: List UList Permutation Div OrderedList ListOp Lia