Hi,
The documentation says
Existential variables can be named by the user upon creation using the syntax ?[ident].
What does this mean? Specifically, where the existential is created by
eapply nrs_rule_indep in n.
I've tried
eapply nrs_rule_indep in n as ?[xxx].
eapply nrs_rule_indep in n ?[xxx].
neither works. How do I name the existential that is created?
Thanks,
Jeremy
There’s some room for improvement in the docs. You can directly apply a lemma to an existential variable (eapply (nrs_rule_indep ?[xxx])) or use the eapply _ with syntax (eapply nrs_rule_indep with (x := ?[xxx]), if nrs_rule_indep is a function with first argument named x, ie., nrs_rule_indep : forall (x : _), ...).
Here are some more example usages with eapply and eexists:
Parameter prop : forall n : nat, True -> n = n.
Goal True -> exists n : nat, n = S n.
Proof.
intros H.
eapply prop with (n := ?[x] + ?x) in H.
(* H : ?x + ?x = ?x + ?x *)
eexists ?[y].
(* Goal : ?y = S ?y*)
Hi Li-yao - thanks for that,
Cheers, Jeremy