proposition: Theorem invariant_refine: forall n p z c cs s, invariant ((n, L p z :: c) :: cs) s -> (forall s1, refine (update p z s) s1 -> ~ sudoku s1) -> invariant ((n, c) :: cs) s.
proof: Proof. Proof with auto with datatypes. intros n p z c cs s (V1, (V2, (V3, V4))) H0. assert (H: valid_lit (L p z) s)... apply (V2 n (L p z :: c))... assert (F1: ordered_clause (L p z :: c))... apply (V1 n)... assert (F2: valid_clause (L p z :: c) s)... apply (V2 n)... split... intros n2 c2; simpl; intros [HH | HH]; subst. injection HH; intros; subst; clear HH. inversion F1... red; apply olist_nil. apply (V1 n2)... split... intros n2 c2; simpl; intros [HH | HH]; subst. injection HH; intros; subst; clear HH. intros l Hl; apply F2... apply (V2 n2)... split... intros s2 Hs2; split; intros HH1. assert (Heq2: sat ((n, L p z :: c) :: cs) s2). case (V4 s2)... intros n2 c2; simpl; intros [HH | HH]. injection HH; intros; subst n2 c2; clear HH. case (Heq2 n (L p z :: c))... simpl; intros l ([Hl1 | Hl1], Hl2); subst. simpl in Hl2. case (H0 s2)... split... rewrite length_update... split... case HH1... intros p1 Hp1. case (pos_dec p p1); intros Heq; try (subst p1). rewrite update_get... apply valid_pos2n... rewrite update_diff_get... case Hs2; intros _ (_, tmp)... case (F2 (L p z))... intros _ (tmp, _)... exists l... apply (Heq2 n2 c2)... case (V4 s2); auto; intros _ tmp; apply tmp; clear tmp. intros n2 c2; simpl; intros [HH | HH]. injection HH; intros; subst; clear HH. case (HH1 n2 c)... intros l (Hl1, Hl2); exists l... apply (HH1 n2)... Qed.
imports: List UList Permutation Div OrderedList ListOp Lia