coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Using vm_compute and reflexivity

From: Kenneth Roe <kendroe AT hotmail.com>
To: coq-club AT inria.fr
Subject: [Coq-Club] Using vm_compute and reflexivity
Date: Sat, 22 Apr 2017 08:55:04 -0400
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=kendroe AT hotmail.com; spf=SoftFail smtp.mailfrom=kendroe AT hotmail.com; spf=None smtp.helo=postmaster AT nm25-vm6.bullet.mail.ne1.yahoo.com
Ironport-phdr: 9a23:litTuhS8SFVESKcuYpIsjw2E5dpsv+yvbD5Q0YIujvd0So/mwa69bBSN2/xhgRfzUJnB7Loc0qyN4vymATRIyK3CmUhKSIZLWR4BhJdetC0bK+nBN3fGKuX3ZTcxBsVIWQwt1Xi6NU9IBJS2PAWK8TW94jEIBxrwKxd+KPjrFY7OlcS30P2594HObwlSijewZbx/IA+qoQnNq8IbnZZsJqEtxxXTv3BGYf5WxWRmJVKSmxbz+MK994N9/ipTpvws6ddOXb31cKokQ7NYCi8mM30u683wqRbDVwqP6WACXWgQjxFFHhLK7BD+Xpf2ryv6qu9w0zSUMMHqUbw5Xymp4KBrSB/vlCcHMiQ28GDTisBpla5VoBysqh58zoLNfY2ZKud1cqfScN8GQGZMWNtaWS5cDYOmd4YBD/YOM+lXoIfgpFUAowWwCw63CePz0z9Ig2P63a0m3+kjFwzNwQwuH8gJsHTRtNj7MbkdUeazzKbW0TXDb+5d1yv66IfWbxsspvKMUqx2ccXM00kvEB3Kg06QqYziIzOV0/4Cs2mf7+Z6Se2vjGsnphh3rzOyxckskpHEi4YWx1ze6Cl0zoU4Kce8RUJme9KoDYZcuiKCO4ZyQc4uWXxktSg5x7Ecp5K3YikHxI4nyhPebfGMbpKG7Qj5VOmLJDd1nHJld6y7hxa16UWgzOj8Wte03VpTsCpFl9jBumoW2BzO7siHTuVy/lu71TaKzQ/T6+VELVoylaXFNpIt2L4xmYATsUTEGS/6gln5jKiTdkk8++io7froYqn+q5KYNIJ4kBzyP6otl8ClBek0LxICU3WG9em/zLHj+Ff2QLROjv04iKnZt5XaKNwYpqGnBQ9az5wj6xGhADq90NQYmmUHLFdfdxKGi4jlIU3BIPf9DfunmVSjjC9rx+zaPr3mGpjCMn/DkK74cblh705c1RE8wMtE55NUD7EBOOj8VlXwtNzeFB85Mha7z/zpCNVnhcsiXjeEBbbcO6fPu3eJ4PguKq+Cftw7ojH4ftso4fjjkX9xo1gQNf2q0J0bcne1NvRhP0CQYH6qidAERzRZ9jEiRfDn3QXRGQVYYGy/Cv5k6w==

Here is a simple proof:

Theorem refl: exists x, x=3+4.
Proof.
apply ex_intro.
(* vm_compute. *)
compute.
reflexivity.
Qed.

I would like to use vm_compute in place of compute. However, when I change
the command, I get the following error:
“Error: vm_compute does not support existential variables.” How can I
reformulate this proof to use vm_compute?

- Ken

[Coq-Club] Using vm_compute and reflexivity, Kenneth Roe, 04/22/2017
- Re: [Coq-Club] Using vm_compute and reflexivity, Laurent Thery, 04/22/2017
  - Re: [Coq-Club] Using vm_compute and reflexivity, Laurent Thery, 04/22/2017
    - Re: [Coq-Club] Using vm_compute and reflexivity, Kenneth Roe, 04/22/2017
      - Re: [Coq-Club] Using vm_compute and reflexivity, Laurent Thery, 04/22/2017
        
        Re: [Coq-Club] Using vm_compute and reflexivity, Kenneth Roe, 04/23/2017
        
        Re: [Coq-Club] Using vm_compute and reflexivity, Laurent Thery, 04/23/2017
        
        Re: [Coq-Club] Using vm_compute and reflexivity, Kenneth Roe, 04/23/2017
        
        Re: [Coq-Club] Using vm_compute and reflexivity, Kenneth Roe, 04/23/2017
    - Re: [Coq-Club] Using vm_compute and reflexivity, Kenneth Roe, 04/22/2017