# Commits

committed b3caab4

Working through Imp.v

# Imp.v

` `
` End Id.`
` `
`-(** Kostik **)`
`-`
` (* ####################################################### *) `
` (** ** States *)`
` `
` Theorem update_eq : forall n X st,`
`   (update st X n) X = n.`
` Proof.`
`-  (* FILL IN HERE *) Admitted.`
`+  intros n X st. unfold update. rewrite <- beq_id_refl. reflexivity.`
`+Qed.`
` (** [] *)`
` `
` (** **** Exercise: 2 stars, optional (update_neq) *)`
`   beq_id V2 V1 = false ->`
`   (update st V2 n) V1 = (st V1).`
` Proof.`
`-  (* FILL IN HERE *) Admitted.`
`-(** [] *)`
`+  intros V2 V1 n st H. unfold update. rewrite H. reflexivity.`
`+Qed.`
` `
` (** **** Exercise: 2 stars, optional (update_example) *)`
` (** Before starting to play with tactics, make sure you understand`
` Theorem update_example : forall (n:nat), `
`   (update empty_state (Id 2) n) (Id 3) = 0.`
` Proof.`
`-  (* FILL IN HERE *) Admitted.`
`+  intros n. unfold update. simpl. unfold empty_state. reflexivity.`
`+Qed.`
` (** [] *)`
` `
` (** **** Exercise: 2 stars (update_shadow) *)`
` Theorem update_shadow : forall x1 x2 k1 k2 (f : state),`
`    (update  (update f k2 x1) k2 x2) k1 = (update f k2 x2) k1.`
` Proof.`
`-  (* FILL IN HERE *) Admitted.`
`+  intros x1 x2 k1 k2 f. unfold update. destruct (beq_id k2 k1). reflexivity. reflexivity.`
`+Qed.`
` (** [] *)`
` `
` (** **** Exercise: 2 stars, optional (update_same) *)`
`   f k1 = x1 ->`
`   (update f k1 x1) k2 = f k2.`
` Proof.`
`-  (* FILL IN HERE *) Admitted.`
`+  intros x1 k1 k2 f H. unfold update. remember (beq_id k1 k2) as eq. destruct eq.`
`+  Case "true". apply beq_id_eq in Heqeq. subst. reflexivity.`
`+  Case "false". reflexivity.`
`+Qed.`
` (** [] *)`
` `
` (** **** Exercise: 2 stars, optional (update_permute) *)`
`   beq_id k2 k1 = false -> `
`   (update (update f k2 x1) k1 x2) k3 = (update (update f k1 x2) k2 x1) k3.`
` Proof.`
`-  (* FILL IN HERE *) Admitted.`
`+  intros x1 x2 k1 k2 k3 f H. unfold update.`
`+  remember (beq_id k1 k3) as eq13. remember (beq_id k2 k3) as eq23. `
`+  destruct eq13; destruct eq23; try (reflexivity).`
`+  destruct k1; destruct k2; destruct k3. unfold beq_id in H.`
`+  unfold beq_id in Heqeq13. unfold beq_id in Heqeq23. `
`+  symmetry in Heqeq13.  symmetry in Heqeq23. `
`+  apply beq_nat_true_iff in Heqeq13. apply beq_nat_true_iff in Heqeq23. subst.`
`+  apply beq_nat_false in H. `
`+  assert (A1 : n1 = n1). reflexivity. apply H in A1. inversion A1.`
`+Qed.`
` (** [] *)`
` `
`+(** Kostik **)`
`+`
` (* ################################################### *)`
` (** ** Syntax  *)`
` `