Skip to content

Instantly share code, notes, and snippets.

@fetburner

fetburner/lecture.v

Created May 24, 2016 03:23
Show Gist options

  • Select an option

    Learn more about clone URLs
  • Save fetburner/84125bf4aa3fc5c49b80e02e131db4bb to your computer and use it in GitHub Desktop.

Select an option

Learn more about clone URLs
Save fetburner/84125bf4aa3fc5c49b80e02e131db4bb to your computer and use it in GitHub Desktop.
Download ZIP
Raw
lecture.v
Require Import Relations.
Section Lecture.
Variable A : Set.
Variable R : relation A.
Hypothesis Hrefl : reflexive _ R.
Hypothesis H : forall x y z, R x y -> R x z -> R y z.
Hint Unfold reflexive symmetric transitive.
Lemma Hsym : symmetric _ R.
Proof. eauto. Qed.
Hint Resolve Hsym.
Lemma Htrans : transitive _ R.
Proof. eauto. Qed.
End Lecture.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment