Commits

Konstantin Solomatov committed 25c544a

Working through Imp.v

  • Participants
  • Parent commits f0604bb

Comments (0)

Files changed (1)

     evaluation are greatly preferable to functional ones, as we'll see
     shortly. *)
 
-(** Kostik **)
-
 (* ####################################################### *)
 (** ** Inference Rule Notation *)
 
 Theorem beq_id_eq : forall i1 i2,
   true = beq_id i1 i2 -> i1 = i2.
 Proof.
-  (* FILL IN HERE *) Admitted.
+  intros i1 i2 H. unfold beq_id in H. destruct i1. destruct i2. symmetry in H. 
+  apply beq_nat_true in H. subst. reflexivity.
+Qed.
 (** [] *)
 
 (** **** Exercise: 1 star, optional (beq_id_false_not_eq) *)
 Theorem beq_id_false_not_eq : forall i1 i2,
   beq_id i1 i2 = false -> i1 <> i2.
 Proof.
-  (* FILL IN HERE *) Admitted.
+  intros i1 i2. unfold beq_id. destruct i1. destruct i2. intros H. intros PC.
+  inversion PC. subst. rewrite <- beq_nat_refl in H. inversion H.
+Qed.
 (** [] *)
 
 (** **** Exercise: 1 star, optional (not_eq_beq_id_false) *)
 Theorem not_eq_beq_id_false : forall i1 i2,
   i1 <> i2 -> beq_id i1 i2 = false.
 Proof.
-  (* FILL IN HERE *) Admitted.
-(** [] *)
+  intros i1 i2. destruct i1. destruct i2. intros H. unfold beq_id. 
+  apply beq_nat_false_iff. intros H1. subst. apply H. reflexivity.
+Qed.
 
 (** **** Exercise: 1 star, optional (beq_id_sym) *)
 Theorem beq_id_sym: forall i1 i2,
   beq_id i1 i2 = beq_id i2 i1.
 Proof.
-  (* FILL IN HERE *) Admitted.
+  intros i1 i2. destruct i1. destruct i2. unfold beq_id. rewrite beq_nat_sym. reflexivity.
+Qed.
 (** [] *)
 
 End Id.
 
+(** Kostik **)
+
 (* ####################################################### *) 
 (** ** States *)