coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] LibHyps 1.0: tactics for manipulation of (groups of) hypothesis

From: Pierre Courtieu <pierre.courtieu AT gmail.com>
To: Coq Club <coq-club AT inria.fr>
Subject: [Coq-Club] LibHyps 1.0: tactics for manipulation of (groups of) hypothesis
Date: Sat, 6 Jul 2019 16:41:33 +0200
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=pierre.courtieu AT gmail.com; spf=Pass smtp.mailfrom=pierre.courtieu AT gmail.com; spf=None smtp.helo=postmaster AT mail-io1-f52.google.com
Ironport-phdr: 9a23:I40TkhIZRvnTEt+hRNmcpTZWNBhigK39O0sv0rFitYgeKP7xwZ3uMQTl6Ol3ixeRBMOHsqgC0LSd7P+ocFdDyK7JiGoFfp1IWk1NouQttCtkPvS4D1bmJuXhdS0wEZcKflZk+3amLRodQ56mNBXdrXKo8DEdBAj0OxZrKeTpAI7SiNm82/yv95HJbAhEmSSxbal8IRi3ognctMsbipZ+J6gszRfEvmFGcPlMy2NyIlKTkRf85sOu85Nm7i9dpfEv+dNeXKvjZ6g3QqBWAzogM2Au+c3krgLDQheV5nsdSWoZjBxFCBXY4R7gX5fxtiz6tvdh2CSfIMb7Q6w4VSik4qx2UxLjljsJOCAl/2HWksxwjbxUoBS9pxxk3oXYZJiZOOdicq/BeN8XQ3dKUMRMWCxbGo6zYIsBAeQCM+hFsYfyu0ADrQeiCQS2GO/j1iNEi33w0KYn0+ohCwbG3Ak4EtwUsXTbss/1NL0MXuuo0qTIyijDb+lK2Tf89ofIbw0qrPaUXbJxb8XR01MvGB3fglqMrozlIimV1vgMs2eF8uptTu2vi2s9pAFwpjij3Nsjio7Mho8MzF3P6Ct3wIEwJdKiSU57Z8apEJRRtyGGN4t2X9gtT3t0tyY9z70Lv4OwcisSyJk/2RLTd/iKf5KL7x/jTuqdPDZ1iXN/dL+/mRq/91WrxPfmWcmuyllKqzJIktnSuXAJ0Bze8s2HReF8/kelwDqP1gfT5vxdLUA6lafXNYQtwrE3lpoUvkTDGjH5lF/qg6+Rc0Uo4umo6+L5bbX6vpKQKZN4hwXkPqktmsGzG/k0PwkPUmSB+emwyqXv/UjjT7VLiv02nLPZsJffJckDvq65AhFa0pw56xmhFTupzNMYnWQdLFJZeRKIkZXpNkrBIPD9F/i/glCsnC13yPDBO73tGo/NIWTbkLf9YbZ97FZRxxY0zdBG/p5bFrUBIO/oVULqr9zZDho5MxSuzOr9CdV90JkeWWOVDaODPqPSqwzA2uV6CO6VLKQRpTy1f/Mi/rvliWIzsV4bZ6igm5UNPiOWBPNjdn2YbGD2j58qFnoQogszUaS+kFyPSyReIX21Qrgg5zwmII2jBIbHAIuqherSj2+AApRKazUeWRi3GnDyetDBAq9UMXPAEopaijUBEIOZZcok3BCquhX9zuM+fOXR8ywc85nk0YosvrGBpVQJ7TVxSv+l/SSVVWgtxzEHQjY32OZ0pkkvkg7eg5g9uORREJlo390MUgo+MsSBnelzCtS3WwWYO9nUEhCpRdKpBTx3RdU0kYcD

Hi,

This Library provides several coq tactics and tacticals to deal with
hypothesis during a proof.

Main page and documentation: https://github.com/Matafou/LibHyps

SHORT DESCRIPTION:

Among manipulations on hypothesis we provide:

- Automatically give better names to hypothesis. The name is computed
from the type of the hypothesis so that it resists lots of script
changes.
- specialize the nth premis of a hypothesis (forward reasoning without
copy-paste).
- move up non-prop hypothesis, to focus on properties
- apply subst, revert.
- ...

These manipulations can be applied:
- to one hyp
- to all hyps
- to "new" hyps after some tactics.

QUICK INSTALL USING OPAM

opam install coq-libhyps

QUICK TEST:

Require Import LibHyps.LibHyps.

Demo file https://github.com/Matafou/LibHyps/blob/master/LibHyps/LibHypsDemo.v

Best regards,
Pierre Courtieu

[Coq-Club] LibHyps 1.0: tactics for manipulation of (groups of) hypothesis, Pierre Courtieu, 07/06/2019