Skip to content

Instantly share code, notes, and snippets.

@MikeMKH

MikeMKH/bySimpl.v

Created April 11, 2017 11:42
Show Gist options

  • Select an option

    Learn more about clone URLs
  • Save MikeMKH/b44fa4dce13cd2790c2873ae480c6945 to your computer and use it in GitHub Desktop.

Select an option

Learn more about clone URLs
Save MikeMKH/b44fa4dce13cd2790c2873ae480c6945 to your computer and use it in GitHub Desktop.
Download ZIP
Simple proofs using Simplification in Coq, taken from Proof by Simplification section of https://www.seas.upenn.edu/~cis500/current/sf/Basics.html
Raw
bySimpl.v
(* taken from https://www.seas.upenn.edu/~cis500/current/sf/Basics.html *)
Theorem plus_0_l : forall n : nat, 0 + n = n.
Proof.
intros.
simpl.
reflexivity.
Qed.
Theorem plus_1_l : forall n : nat, 1 + n = S n.
Proof.
intros.
simpl.
reflexivity.
Qed.
Theorem mult_0_l : forall n : nat, 0 * n = 0.
Proof.
intros.
simpl.
reflexivity.
Qed.
@MikeMKH

MikeMKH commented Apr 11, 2017

Copy link
Copy Markdown
Author

Note reflexivity in Coq is powerful enough that simplification is not needed.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment