coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Making COq do more of the search work

From: Clément Pit-Claudel <cpitclaudel AT gmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Making COq do more of the search work
Date: Tue, 13 Mar 2018 10:43:40 -0400
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=cpitclaudel AT gmail.com; spf=Pass smtp.mailfrom=cpitclaudel AT gmail.com; spf=None smtp.helo=postmaster AT mail-qt0-f182.google.com
Ironport-phdr: 9a23:nSr0+xaW6ttCXsqtucmgTIL/LSx+4OfEezUN459isYplN5qZr8m5bnLW6fgltlLVR4KTs6sC17KN9fi4EUU7or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6arXK99yMdFQviPgRpOOv1BpTSj8Oq3Oyu5pHfeQpFiCazbL9oMBm6sRjau9ULj4dlNqs/0AbCrGFSe+RRy2NoJFaTkAj568yt4pNt8Dletuw4+cJYXqr0Y6o3TbpDDDQ7KG81/9HktQPCTQSU+HQRVHgdnwdSDAjE6BH6WYrxsjf/u+Fg1iSWIdH6QLYpUjmk8qxlSgLniD0fOjAk7m/XhMx+gqFVrh2vqBNwwZLbbo6OOfpifa7QZ88WSXZPU8tTUSFKH4Oyb5EID+oEJetVsY39oEELrRSgAwmsGPvgxCVJhn/qxKE3zeAhHhvb3AM9Ad0OtGnfodLpO6cKUOC10LXHzTHZYPNLxDjy9ozIfwsuofGJR71wcM7RxVMzGAPCi1WdsIroNC6b2OQKtmiU9etgVeS3hm4/qgFxviGjydsoiobTm4Ia107L9SFjzIY7P921TlNwb928EJZIqS2WK497TtkhTmxooio21KAKtJ+hcCQXy5kr2QbTZ+KGfoSU/x7uUfudLDR3iX9gd7+zmhW//VSlx+D9V8S7zlRHoy9Gn9XRqHwA2Bne5tabRvRj8Ees3DiP2gPO5uxEJE07ibDUJII8zrM2i5Edq17MHjXsl0XzlKKWdlsr+uyv6+n/Z7XpvJ6cN4tthgHnLqQihtWzAeolPgUNQWSX4+u81Lrk/U32RLVFkOc6nbXesJDfPcgbp6i5DBFJ0os79RqzEzOr3M4bkHQHNl5JZg+LgonzN13TI/30E++zg1G2nzdqw/DGMKfhApLILnXbjLjhZbd961JAxwo3199f+o9bBa8FIP/oVU/xscbXDh49MwCu3+nnD9B92psEWW2TGq+ZLL/SsViQ6+0zJOmMfZYZtyr5K/g4/PHjlmQ5mF8Yfamxx5QbcnG4HvJ8I0WYe3XgmNkBEX1Z9jY5GeftkRiJVSNZT3e0RaM1oD8hW6y8CoKWbYQshbGHwBCDH4ETTWRPF1yBFT+8fJ2FR/wIYT+eL8tJnTkNVLznQIgkg0L9/DTmwqZqe7KHshYTsojugYAstr/j0Coq/DkxNPyzlmSETmV6hGQNHmZk06V2oEg7wVCGg/Eh365oUOdL7vYMaT8UcIbGxrUjWd/3UwPFONyOTQT+G4j0MXQKVts0huQ2TQN9FtGl1E6R2iOrB/oMi+TOCsVkqOTT2H/+I8s7wHHDhvEs

On 2018-03-13 08:02, Matthieu Sozeau wrote:
> without doing expensive “did I do this already?” checks, ie an
> explicit state manipulation.

I've been using that style in some of my proofs, and didn't find so costly as
to be unusable. I wrote a bit about it at
http://pit-claudel.fr/clement/MSc/#text-5-2-1

Clément.

[Coq-Club] Making COq do more of the search work, Jim Fehrle, 03/12/2018
- RE: [Coq-Club] Making COq do more of the search work, Soegtrop, Michael, 03/12/2018
  - Re: [Coq-Club] Making COq do more of the search work, Abhishek Anand, 03/12/2018
    - Re: [Coq-Club] Making COq do more of the search work, Matthieu Sozeau, 03/12/2018
      - RE: [Coq-Club] Making COq do more of the search work, Soegtrop, Michael, 03/12/2018
        
        Re: [Coq-Club] Making COq do more of the search work, Théo Zimmermann, 03/12/2018
        
        Re: [Coq-Club] Making COq do more of the search work, Armaël Guéneau, 03/13/2018
        
        Re: [Coq-Club] Making COq do more of the search work, Matthieu Sozeau, 03/13/2018
        Re: [Coq-Club] Making COq do more of the search work, Clément Pit-Claudel, 03/13/2018
        
        RE: [Coq-Club] Making COq do more of the search work, Soegtrop, Michael, 03/14/2018
      - Re: [Coq-Club] Making COq do more of the search work, R. Pollack, 03/12/2018