Commits

Konstantin Solomatov  committed f5fc320

Working through Rel.v

  • Participants
  • Parent commits 9447c69

Comments (0)

Files changed (1)

 (** Show that the [total_relation] defined in Logic.v is not a partial
     function. *)
 
-(* FILL IN HERE *)
+Theorem total_relation_not_a_partial_function :
+  ~ (partial_function total_relation).
+Proof.
+  unfold not. unfold partial_function. intros H.
+  assert (0 = 1) as Nonsense.
+    apply H with 0.  apply total. apply total.
+  inversion Nonsense.
+Qed.
+
 (** [] *)
 
 (** **** Exercise: 2 stars, optional *)
 (** Show that the [empty_relation] defined in Logic.v is a partial
     function. *)
+Theorem empty_relation_is_a_partial_function : 
+  partial_function empty_relation.
+Proof.
+  unfold partial_function. intros x y1 y2 E1 E2.
+  inversion E1.
+Qed.
 
-(* FILL IN HERE *)
 (** [] *)
 
 (** A _reflexive_ relation on a set [X] is one that holds for every
   unfold lt. unfold transitive.
   intros n m o Hnm Hmo.
   induction Hmo as [| m' Hm'o].
-    (* FILL IN HERE *) Admitted.
+  Case "le_n". apply le_S. apply Hnm.
+  Case "le_S". apply le_S. apply IHHm'o.
+Qed.
 (** [] *)
 
 (** **** Exercise: 2 stars, optional *)
 Proof.
   unfold lt. unfold transitive.
   intros n m o Hnm Hmo.
-  induction o as [| o'].
-  (* FILL IN HERE *) Admitted.
+  induction o as [| o'].                                                                
+  Case "0". inversion Hmo.
+  Case "S n". inversion Hmo.
+    SCase "le_n". rewrite H0 in Hnm. apply le_S. apply Hnm.
+    SCase "le_S". apply le_S. apply IHo'. apply H0.
+Qed.
 (** [] *)
 
 (** The transitivity of [le], in turn, can be used to prove some facts
 Theorem le_S_n : forall n m,
   (S n <= S m) -> (n <= m).
 Proof.
-  (* FILL IN HERE *) Admitted.
+  intros n m H. inversion H.
+  Case "le_n". apply le_n.
+  Case "le_S". apply le_Sn_le. apply H1.
+Qed.
 (** [] *)
 
 (** **** Exercise: 2 stars, optional (le_Sn_n_inf) *)
     the informal proof without doing the formal proof first.
  
     Proof:
-    (* FILL IN HERE *)
-    []
+      induction on n.
+        n = 0: ~ 1 <= 0. => we use le_n here. but it isn't applicable
+        n = S n: ~(S n <= n). Want ~(S (S n) <= S n)
+          assume S (S n) <= S n. by le_S_n we have (S n <= n) and we can get false.
+      Qed.
  *)
 
 (** **** Exercise: 1 star, optional *)
 Theorem le_Sn_n : forall n,
   ~ (S n <= n).
 Proof.
-  (* FILL IN HERE *) Admitted.
+  induction n.
+  Case "0". intros H. inversion H.
+  Case "S n". intros H. apply le_S_n in H. apply IHn in H. apply H.
+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.