Mercurial > cpdt > repo
comparison src/Match.v @ 545:4f6e7bab0d45
Make a theorem name more consistent
| author | Adam Chlipala <adam@chlipala.net> |
|---|---|
| date | Tue, 08 Mar 2016 11:50:53 -0500 |
| parents | ed829eaa91b2 |
| children | 2c8c693ddaba |
comparison
equal
deleted
inserted
replaced
| 544:71b85aaae868 | 545:4f6e7bab0d45 |
|---|---|
| 983 Hypothesis H2 : forall v1 u1 v2 u2, | 983 Hypothesis H2 : forall v1 u1 v2 u2, |
| 984 P v1 u1 | 984 P v1 u1 |
| 985 -> P v2 u2 | 985 -> P v2 u2 |
| 986 -> P (f v1 v2) (g u1 u2). | 986 -> P (f v1 v2) (g u1 u2). |
| 987 | 987 |
| 988 Theorem t6 : forall v1 v2, Q v1 -> Q v2 -> exists u1, exists u2, P (f v1 v2) (g u1 u2). | 988 Theorem t7 : forall v1 v2, Q v1 -> Q v2 -> exists u1, exists u2, P (f v1 v2) (g u1 u2). |
| 989 | 989 |
| 990 (** We can prove the goal by calling [insterKeep] with a tactic that tries to find and apply a [Q] hypothesis over a variable about which we do not yet know any [P] facts. We need to begin this tactic code with [idtac; ] to get around a strange limitation in Coq's proof engine, where a first-class tactic argument may not begin with a [match]. *) | 990 (** We can prove the goal by calling [insterKeep] with a tactic that tries to find and apply a [Q] hypothesis over a variable about which we do not yet know any [P] facts. We need to begin this tactic code with [idtac; ] to get around a strange limitation in Coq's proof engine, where a first-class tactic argument may not begin with a [match]. *) |
| 991 | 991 |
| 992 intros; do 2 insterKeep ltac:(idtac; match goal with | 992 intros; do 2 insterKeep ltac:(idtac; match goal with |
| 993 | [ H : Q ?v |- _ ] => | 993 | [ H : Q ?v |- _ ] => |