# Commits

committed 25c544a

Working through Imp.v

• Participants
• Parent commits f0604bb

# File Imp.v

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