StackOverflow2013

Note that there are some explanatory texts on larger screens.

plurals

PO
primarykey
Id
11603848
data
AcceptedAnswerId
0
AnswerCount
0
ClosedDate
CommentCount
2
CommunityOwnedDate
CreationDate
2012-07-22T20:45:05.403
FavoriteCount
0
LastActivityDate
2012-07-22T20:45:05.403
LastEditDate
LastEditorUserId
0
OwnerUserId
805875
ParentId
11600336
PostTypeId
2
Score
1
ViewCount
0
LastEditorDisplayName
text
Body
I think I can't correctly infer the general problem that you have, given your description and example. If you already know <code>H : f = g</code>, you can use that to <code>rewrite H</code> wherever you want to show something about <code>f</code> and <code>g</code>, or just <code>elim H</code> to rewrite everything at once. You don't need to <code>assert</code> a helper theorem and if you do, you'll obviously need something like <code>assert</code> or <code>pose proof</code>. If that equality is hidden underneath some eta-expansion, like in your example, remove that layer and then proceed as above. Here are two (out of many) possible ways of doing that: <pre><code>intros A B P Q a H. assert (P = Q) as H0 by apply H. rewrite H0; reflexivity. </code></pre> This solves your example proof by <code>assert</code>ing the equality, then rewriting. Another possibility is to define eta reduction helpers (haven't found predefined ones) and using these. That will be more verbose, but might work in more complex cases. If you define <pre><code>Lemma eta_reduce : forall (A B : Type) (f : A -> B), (fun x => f x) = f. intros. reflexivity. Defined. Tactic Notation "eta" constr(f) "in" ident(H) := pattern (fun x => f x) in H; rewrite -> eta_reduce in H. </code></pre> you can do the following: <pre><code>intros A B P Q a H. eta P in H. eta Q in H. rewrite H; reflexivity. </code></pre> (That notation is a bit of a loose cannon and might rewrite in the wrong places. Don't rely on it and in case of anomalies do the <code>pattern</code> and <code>rewrite</code> manually.)
Tags
Title
singulars
PostAcceptedAnswerId
1. This table or related slice is empty.
PostParentId
1. POapply argument to equal functions in Coq
 singulars
 PostTypePostTypeId
 PTQuestion
PostTypePostTypeId
1. PTAnswer
UserLastEditorUserId
1. This table or related slice is empty.
UserOwnerUserId
1. USnobody
plurals
PostLinksPostIdRelatedPostId
1. This table or related slice is empty.
PostLinksRelatedPostIdPostId
1. This table or related slice is empty.
PostsAcceptedAnswerId
1. POapply argument to equal functions in Coq
 singulars
 PostTypePostTypeId
 PTQuestion
PostsParentIdCreationDate
1. This table or related slice is empty.
VotesPostIdCreationDate
1. VO
 singulars
 PostPostId
 PO
 UserUserId
 This table or related slice is empty.
 VoteTypeVoteTypeId
 VTUpMod
2. VO
 singulars
 PostPostId
 PO
 UserUserId
 This table or related slice is empty.
 VoteTypeVoteTypeId
 VTAcceptedByOriginator
CommentsPostId
1. COIf you want the (AFAIK) exact opposite of `f_equal`, there's `equal_f`. If you `Require Import Coq.Logic.FunctionalExtensionality.`, you can solve your example by `intros A B P Q a H. apply equal_f with a in H. exact H.`. Note that this module adds the axiom of functional extensionality, which may or may not be compatible with your choice of axioms. ;-)
 singulars
 PostPostId
 PO
 UserUserId
 USnobody
2. COThanks. I think this is what I was looking for :)
 singulars
 PostPostId
 PO
 UserUserId
 USAlex

Querying!

Guidance

A row detail

Detail views are divided into sections. All the information in the data section comes from columns in the selected row. The other sections display data from other, related rows.

Related data can be related in a to-one or a to-many fashion. Captions of data related in a to-many fashion link to a list view showing a filtered view of the table.

Try moving around until you find a non-empty to-many entry and click on the label to get to one. You can move back to the root by clicking on the database name in the header.