softwareFoundations

committed f5fc320

Working through Rel.v

Rel.v

` (** 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.`
Tip: Filter by directory path e.g. /media app.js to search for public/media/app.js.
Tip: Use camelCasing e.g. ProjME to search for ProjectModifiedEvent.java.
Tip: Filter by extension type e.g. /repo .js to search for all .js files in the /repo directory.
Tip: Separate your search with spaces e.g. /ssh pom.xml to search for src/ssh/pom.xml.
Tip: Use ↑ and ↓ arrow keys to navigate and return to view the file.
Tip: You can also navigate files with Ctrl+j (next) and Ctrl+k (previous) and view the file with Ctrl+o.
Tip: You can also navigate files with Alt+j (next) and Alt+k (previous) and view the file with Alt+o.