# Commits

committed 1d40523

Finished Rel.v

• Participants
• Parent commits f5fc320

# Rel.v

` Qed.`
` (** [] *)`
` `
`-(** Kostik **)`
`-`
` (** Reflexivity and transitivity are the main concepts we'll need for`
`     later chapters, but, for a bit of additional practice working with`
`     relations in Coq, here are a few more common ones.`
` Theorem le_not_symmetric :`
`   ~ (symmetric le).`
` Proof.`
`-  (* FILL IN HERE *) Admitted.`
`+  unfold symmetric. intros H.`
`+  assert (A1 : 0 <= S 0). apply le_S. apply le_n.`
`+  apply H in A1. `
`+  assert (A2 : ~(S 0 <= 0)). apply le_Sn_n.`
`+  apply A2 in A1. apply A1.`
`+Qed.`
` (** [] *)`
` `
` (** A relation [R] is _antisymmetric_ if [R a b] and [R b a] together`
` Definition antisymmetric {X: Type} (R: relation X) :=`
`   forall a b : X, (R a b) -> (R b a) -> a = b.`
` `
`+(** Kostik **)`
`+`
` (** **** Exercise: 2 stars, optional *)`
` Theorem le_antisymmetric :`
`   antisymmetric le.`
` Proof.`
`-  (* FILL IN HERE *) Admitted.`
`+  unfold antisymmetric. intros a b. generalize dependent b. induction b.`
`+  Case "0". intros H1 H2. inversion H1. reflexivity.`
`+  Case "S b". intros H1 H2. destruct H1. `
`+    SCase "le_n". reflexivity.`
`+    SCase "le_S". apply n_le_m__Sn_le_Sm in H1.    `
`+      assert (A1 : S a <= a). apply le_trans with (S m). apply H1. apply H2.`
`+      assert (A2 : ~(S a <= a)). apply le_Sn_n. `
`+      contradiction.`
`+Qed.`
` (** [] *)`
` `
` (** **** Exercise: 2 stars, optional *)`
`   n < m ->`
`   m <= S p ->`
`   n <= p.`
`-Proof. `
`-  (* FILL IN HERE *) Admitted.`
`+Proof.`
`+  unfold lt. intros n m p H1 H2. `
`+  assert (A1 : S n <= S p). apply le_trans with m. apply H1. apply H2.`
`+  apply Sn_le_Sm__n_le_m in A1. apply A1.`
`+Qed.`
` (** [] *)`
` `
` (** A relation is an _equivalence_ if it's reflexive, symmetric, and`
`   intros X R x y r.`
`   apply rsc_step with y. apply r. apply rsc_refl.   Qed.`
` `
`+(** Kostik **)`
`+`
` (** **** Exercise: 2 stars, optional (rsc_trans) *)`
` Theorem rsc_trans :`
`   forall (X:Type) (R: relation X) (x y z : X),`
`       refl_step_closure R y z ->`
`       refl_step_closure R x z.`
` Proof.`
`-  (* FILL IN HERE *) Admitted.`
`+  intros X R x y z H1 H2. induction H1.`
`+  Case "rsc_refl". assumption.`
`+  Case "rsc_step". apply IHrefl_step_closure in H2. apply rsc_step with y. apply H. apply H2.`
`+Qed.`
` (** [] *)`
` `
` (** Then we use these facts to prove that the two definitions of`
`          forall (X:Type) (R: relation X) (x y : X),`
`   clos_refl_trans R x y <-> refl_step_closure R x y.`
` Proof.`
`-  (* FILL IN HERE *) Admitted.`
`-(** [] *)`
`-`
`+  intros X R x y. split.`
`+  Case "->".`
`+    intros H. induction H.`
`+    SCase "rt_step". apply rsc_R. assumption.`
`+    SCase "rt_refl". apply rsc_refl.`
`+    SCase "rt_trans". apply rsc_trans with y. assumption. assumption.`
`+  Case "<-".`
`+    intros H. induction H.`
`+    SCase "rsc_refl". apply rt_refl.`
`+    SCase "rsc_step". apply rt_trans with y. apply rt_step. apply H. assumption.`
`+Qed.`