naming existentials

Using Coq
#1

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

#2

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*)
1 Like
#3

Hi Li-yao - thanks for that,
Cheers, Jeremy