Created
April 27, 2017 10:57
-
-
Save MikeMKH/98f04ab550bbcdf7688c06c6e1d05335 to your computer and use it in GitHub Desktop.
Look at inference rules in Coq from Coq Art
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| (* exercise 4.3 from Coq Art *) | |
| Lemma all_perm : | |
| forall (A : Type) (P : A -> A -> Prop), | |
| (forall x y : A, P x y) -> | |
| forall x y : A, P y x. | |
| Proof. | |
| intros A P H x y. | |
| apply H. | |
| Qed. | |
| Lemma resolution : | |
| forall (A : Type) (P Q R S : A -> Prop), | |
| (forall a : A, Q a -> R a -> S a) -> | |
| (forall b : A, P b -> Q b) -> | |
| forall c : A, P c -> R c -> S c. | |
| Proof. | |
| intros A P Q R S H H0 c H1 H2. | |
| apply H; try assumption. | |
| apply H0; assumption. | |
| Qed. |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Note try assumption will not be able to applied to Q c but can be applied to R c, so try will fail on Q c and give that as the next goal.