Commits

Konstantin Solomatov committed b3caab4

Working through Imp.v

Comments (0)

Files changed (1)

 
 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  *)