The Coq mailing list

[Vadim Zaliva <vzaliva AT cmu.edu>]

On Thu, Sep 1, 2016 at 4:38 PM, Jonathan Leivent <jonikelee AT gmail.com> wrote:

Is this sufficient?:

Class A (n:nat) : Prop.
Definition f (n:nat)`{A n} := n.
Definition g (n:nat) := n.

Lemma Foo:  exists w, forall x, @f (g x) (w x) = x.
unshelve eexists.

Neat trick! Thanks.

If I want to use Foo for rewriting, I guess I have to do something like this:

Lemma Foo_Test:

  exists w, 5 + @f (g 1) (w 1) = 5 + 1.

Proof.

  elim Foo.

  intros A_g H.

  exists A_g.

  rewrite H.

  reflexivity.

Qed.

In more complex cases, where one have several type class instance evars, dependent on each other I suspect using this approach could become unwieldy.

P.S. I have just seen your message with an alternative way, swapping exists and forall. I will play with it now to see if it works any better for rewriting.

Thanks!

--

CMU ECE PhD candidate

Mobile: +1(510)220-1060