proposition: Lemma fold_update_rel_correct : forall {A: Type} (F: A -> state -> dresult) (R : state -> dresult -> Prop) (RSucc : forall st d, R st (Success d)) (REFL : forall st : state, R st (Progress st)) (FOUT : forall a st, ~ is_fail (F a st)) (RTrans : forall s1 s2 s3, R s1 (Progress s2) -> R s2 (Progress s3) -> R s1 (Progress s3)) (ROK : forall a st st', F a st = Progress st' -> R st (Progress st')) l st, R st (fold_update F l st).
proof: Proof. induction l; simpl. - auto. - intros. generalize (FOUT a st). destruct (F a st) eqn:EQ; simpl; auto. + tauto. + apply ROK in EQ. specialize (IHl st0). assert (~ is_fail (fold_update F l st0)). { clear - FOUT. revert st0. induction l ; simpl. congruence. intros. specialize (FOUT a st0). destruct (F a st0) ; try congruence. apply IHl. } destruct (fold_update F l st0); try congruence. simpl in H. tauto. intros. apply RSucc. intros. eapply RTrans; eauto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause