proposition: Lemma put_method_R: forall n s1 s2 k v1 v2, RState _ _ R s1 s2 -> R v1 v2 -> let (s1', u1) := put_method _ n s1 k v1 in let (s2', u2) := put_method _ n s2 k v2 in RState _ _ R s1' s2' /\ RUpdate _ _ R u1 u2.
proof: Proof. Proof using. intros. unfold put_method. unfold RState in H. open_conjs. split. unfold RState. simpl. split_all. intros. destruct (eq_nat_dec k k0). subst k. simpl_override. simpl_override. split_all. assumption. reflexivity. rewrite H2. reflexivity. simpl_override. simpl_override. specialize (H k0). open_conjs. split_all; assumption. apply functional_extensionality. intro n'. destruct (eq_nat_dec n n'). simpl_override. simpl_override. rewrite H2. reflexivity. simpl_override. simpl_override. rewrite H1. reflexivity. rewrite H2. reflexivity. rewrite H2. reflexivity. unfold RUpdate. rewrite H2. rewrite H3. split_all; reflexivity. Qed.
imports: Coq(FunctionalExtensionality List Bool) Coq(Arith Arith.Peano_dec Arith.Compare_dec) Coq(Program.Basics) Chapar(Predefs extralib KVStore)