Commits

Konstantin Solomatov committed 1d40523

Finished Rel.v

  • Participants
  • Parent commits f5fc320

Comments (0)

Files changed (1)

 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.