Skip to content

Instantly share code, notes, and snippets.

@uenoku

uenoku/coq_practice_01.v

Last active April 28, 2017 11:14
Show Gist options
  • Save uenoku/eefb7295feb9fb347419e99576c5848a to your computer and use it in GitHub Desktop.
Save uenoku/eefb7295feb9fb347419e99576c5848a to your computer and use it in GitHub Desktop.
Download ZIP
Raw
coq_practice_01.v
Section hoge.
Variable P Q R S T : Prop.
Lemma id_p : P -> P.
Proof.
intro a.
assumption.
Qed.
Lemma id_pp : (P-> P) -> (P-> P).
Proof.
intro a.
assumption.
Qed.
Lemma imp_trans : (P->Q)->(Q->R)->P->R.
Proof.
intro a.
intro b.
intro c.
apply b.
apply a.
assumption.
Qed.
Lemma imp_perm : (P->Q->R)->(Q->P->R).
Proof.
intro a.
intro b.
intro c.
apply a.
assumption.
assumption.
Qed.
Lemma diamond : (P->Q)->(P->R)->(Q->R->T)->P->T.
Proof.
intro a.
intro b.
intro c.
intro d.
apply c.
apply a.
assumption.
apply b.
assumption.
Qed.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment