coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: "jonikelee AT gmail.com" <jonikelee AT gmail.com>
- To: Pierre Courtieu <Pierre.Courtieu AT cnam.fr>
- Cc: coq-club AT inria.fr
- Subject: Re: [Coq-Club] Fwd: Hiding "Obvious" Hypothesis?
- Date: Thu, 2 Apr 2020 11:23:31 -0400
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=jonikelee AT gmail.com; spf=Pass smtp.mailfrom=jonikelee AT gmail.com; spf=None smtp.helo=postmaster AT mail-qk1-f194.google.com
- Ironport-phdr: 9a23:HSQ/RRDg+TGt9J2XdPWTUyQJP3N1i/DPJgcQr6AfoPdwSPXzo8bcNUDSrc9gkEXOFd2Cra4d1qyO7+u/CCRAuc/H7CleNsQUFlcssoY/oU8JOIa9E0r1LfrnPWQRPf9pcxtbxUy9KlVfA83kZlff8TWY5D8WHQjjZ0IufrymUoHdgN6q2O+s5pbdfxtHhCanYbN1MR66sRjdutMZjId/Kqs90AfFr3RHd+lUwW5jOFafkwrh6suq85Nv7itdt+g9+8JcVKnxYrg1Q6FfADk6PG8549HmuwPeRgWV/HscVWsWkhtMAwfb6RzxQ4n8vCjnuOdjwSeWJcL5Q6w6VjSk9KdrVQTniDwbOD4j8WHYkdJ/gaRGqx+8vRN/worUYIaINPpie67WYN0XSXZdUstXSidMGZ23YZcRAOUdPOZYt4j9qEUIrRuiHgmnGefjxiZVinPqwaE21uIsGhzE0gM9BdIDqHraotXrOqkPUu66zqfIwzLMYPxK1jnw85TIfxI7rP2QR798bdTdxE8yHA3FlFWQronlMiub2uQPtGib6etgVeGxhG4jtQ5+vCOixsgpiobTh4IVzkrI+jl+wIYwK9GzVUl2YdyjEJtWtiGaNJV5Qsc8TG52oys6xbgGtoS6fCgO0pgo2xnfa/mefoWO/xntWuGRITJii3JkfrKynxKy/lahyu3iTMa01kpKojBFktbSrHACyQTf6seGSvth/kehxC2A2xrP5eFDJEA5k7fQJZ05wrMoiJYfrUDOEjX1lUj2lqOaaFso9vay5+j6ZrjrqYeQO5F1hw3iL6gjn9GzDOAkPQULUGWW+Piw2KHm8EHkTrhFk/g7n6navZ/AP8sWo7O1DxFb0oYt7hu/ASmp384FknQCKF9JZRCKgovvNlrTOv73F+2/jE6pkDpzx/DJILnhApLVI3jGirjhfLJ951dFyAow0NxT/pxUBqwFLf/8QEPxu9vYDhg2Mwyw3enrEsly1oQbWW6XA6+ZNr3dsUOQ6+4xP+WBYJUZtTX9JvQ/+fLik2E1lUUAcaSt0pYbcHW4Ee5nI0Wdb3rsmNABEWISswo8S+zqjlyCUT1NaHa2Qa0z+Co2CI2jDYjZR4CthKaN0zu8Hp1TfmxGEEyDEW/0d4WYXPcBcD6dIsh4kjAdSbehT5Ih2gq1uQ/hy7tnK/LU9TcCuZLi0th1/ezTmgso+Tx6FcTOm12KGll1k3kSSncd271lvU1w1x/X6al1meZVU/dU+ulVUwonHZXaxuk8BcqkCSzbedLcAlShRNSlDDU8Q/o+xtYPZwB2HNDoxkTB2CyrALIRmrGjC5k986aa1H/0cZUug03a3bUs2gF1CvBEMner0+smr1CKVtz51n6BnqPvTpwymSvE9WON122L5RgKXwt5UKGDVncaNBKP8IbJo3jaRrrrMowJdwtMzcnYdPlPY9ztyExFHbLtYYWCJW22nGi0CFCDwbbeNNO2KVVY5z3UDQ0/qy5W5WyPbFFsCSKoomaYBztrRwri
On Thu, 2 Apr 2020 10:45:49 +0200
Pierre Courtieu
<Pierre.Courtieu AT cnam.fr>
wrote:
> Nice ltac!
> I have something similar in LibHyps without touching the proof term
> (thanks to ltac hack from J.Leivant).
Here's the source for that hypothesis harvesting and iteration hack:
https://github.com/jonleivent/mindless-coding-phase2/blob/master/hypiter.v
> There is no "ignore line"
> though. And I must say it has a better effect with the "Set Compact
> Context" which is only available for proofgeneral I think.
>
>
> Just do "onAllHyps move_up_types." once you have imported the library.
> Here is a minimal header (you don't need it if you import LibHyps) to
> see what the "onAllHyps move_up_types." does at the end.
>
> Hope this helps
> P.
> PS LibHyps: https://github.com/Matafou/LibHyps, available as opam
> package, coq-8.11 supported but not yet declared as such in opam
> (should happen quickly).
> --------------------------8X----------------------------
>
> Require Import List.
> Import ListNotations.
>
> (* Credit for the harvesting of hypothesis: Jonathan Leivant *)
> Ltac harvest_hyps harvester := constr:(ltac:(harvester; constructor)
> : True).
>
> Ltac revert_clearbody_all :=
> repeat lazymatch goal with H:_ |- _ => try clearbody H; revert H
> end.
>
> Ltac all_hyps := harvest_hyps revert_clearbody_all.
>
> Ltac next_hyp hs step last :=
> lazymatch hs with
> | (?hs' ?H) => step H hs'
> | _ => last
> end.
>
> Ltac map_hyps tac hs :=
> idtac;
> let rec step H hs := next_hyp hs step idtac; tac H in
> next_hyp hs step idtac.
>
> Ltac map_all_hyps tac := map_hyps tac all_hyps.
>
> (* For less parenthesis: OnAllHyp tacA;tac2. *)
> Tactic Notation (at level 3) "onAllHyps" tactic(Tac) := (map_all_hyps
> Tac).
>
>
> Ltac revertHyp H := revert H. (* revert is a tactic notation *)
> Ltac move_up_types H := match type of H with
> | ?T => match type of T with
> | Set => move H at top
> | Type => move H at top
> | _ => idtac
> end
> end.
>
> Goal forall
> (l1 l2: list nat)
> (H0: l1 = l2 ++ l2)
> (bs1: list bool)
> (x: nat)
> (bs2: list bool)
> (H1: true :: bs1 = bs2 ++ bs1)
> (y: nat)
> (H2: x :: l1 = y :: y :: l2),
> l1 ++ l2 ++ l1 = (l1 ++ l2) ++ l1.
> Proof.
> intros.
> onAllHyps move_up_types.
>
- [Coq-Club] Fwd: Hiding "Obvious" Hypothesis?, Agnishom Chattopadhyay, 04/01/2020
- Re: [Coq-Club] Fwd: Hiding "Obvious" Hypothesis?, Samuel Gruetter, 04/02/2020
- Re: [Coq-Club] Fwd: Hiding "Obvious" Hypothesis?, Pierre Courtieu, 04/02/2020
- Re: [Coq-Club] Fwd: Hiding "Obvious" Hypothesis?, jonikelee AT gmail.com, 04/02/2020
- Re: [Coq-Club] Fwd: Hiding "Obvious" Hypothesis?, jonikelee AT gmail.com, 04/02/2020
- Re: [Coq-Club] Fwd: Hiding "Obvious" Hypothesis?, jonikelee AT gmail.com, 04/02/2020
- Re: [Coq-Club] Fwd: Hiding "Obvious" Hypothesis?, Pierre Courtieu, 04/02/2020
- Re: [Coq-Club] Fwd: Hiding "Obvious" Hypothesis?, jonikelee AT gmail.com, 04/03/2020
- Re: [Coq-Club] Fwd: Hiding "Obvious" Hypothesis?, Pierre Courtieu, 04/02/2020
- Re: [Coq-Club] Fwd: Hiding "Obvious" Hypothesis?, jonikelee AT gmail.com, 04/02/2020
- Re: [Coq-Club] Fwd: Hiding "Obvious" Hypothesis?, jonikelee AT gmail.com, 04/02/2020
- Re: [Coq-Club] Fwd: Hiding "Obvious" Hypothesis?, jonikelee AT gmail.com, 04/02/2020
- Re: [Coq-Club] Fwd: Hiding "Obvious" Hypothesis?, Pierre Courtieu, 04/02/2020
- Re: [Coq-Club] Fwd: Hiding "Obvious" Hypothesis?, Paolo Giarrusso, 04/09/2020
- Re: [Coq-Club] Fwd: Hiding "Obvious" Hypothesis?, Agnishom Chattopadhyay, 04/10/2020
- Re: [Coq-Club] Fwd: Hiding "Obvious" Hypothesis?, Paolo Giarrusso, 04/10/2020
- Re: [Coq-Club] Fwd: Hiding "Obvious" Hypothesis?, Agnishom Chattopadhyay, 04/10/2020
- Re: [Coq-Club] Fwd: Hiding "Obvious" Hypothesis?, Samuel Gruetter, 04/02/2020
Archive powered by MHonArc 2.6.18.