coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: "jonikelee AT gmail.com" <jonikelee AT gmail.com>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] Fwd: Hiding "Obvious" Hypothesis?
- Date: Thu, 2 Apr 2020 13:13:23 -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-f180.google.com
- Ironport-phdr: 9a23:7iwEbhYRm2Y7UV3fVrOPuQv/LSx+4OfEezUN459isYplN5qZrs64bnLW6fgltlLVR4KTs6sC17OL9fi8EjVYu97B6ClELMUQEUddyI0/pE8JPo2sMQXDNvnkbig3ToxpdWRO2DWFC3VTA9v0fFbIo3e/vnY4ExT7MhdpdKyuQtaBx8u42Pqv9JLNfg5GmCSyYa9oLBWxsA7dqtQajZFtJ6osyhbFuGdEdutZyW91OV6fgQv36sOs8JJ+6ShdtO8t+sFaXanmY6g0SKFTASg7PWwy+MDkuh7PQBeV6HABSGsWiB1IAwbE7BH+QJj8tzbxu/R+1ieHI8D4VKg4Vju+4ahlTh/okzoHOCUi8G7LkMxwjblUrwynqhdi3oPbeoCVNP55fqPAYdMXQHdKU8hNWyBdBI63co0CBPcDM+lFtYnwv1UAoxugCwexB+3gyDFIiHj50qIm3OosCh3G0Q46Et4SqnnYsMv5OaEPWu611qnIyjDDYutY1Tf/74jIdBEhofKSUrJ0b8Xe11IiFwzAjlqKqIzlOymZ2fgKs2ie4eZrSOWii2wgqwF3ozivxdkjio3XiY0L0V3E+iB5z5w0Jd28UkJ0fdmkEJ5JuiycKoB4TMQiQ2RytyY7zL0LoZq7czYLyJQ53RHfbeCHf5KI4h39TuaePy90hH1keLKjhxay7FOvxvfgWcmz1VZHqDdOnNrUtn0VyRDf9syKRuF+80qhwzqDyR7f5v9eLUwplqfXN4YtzqAxm5YPrEjOGzL6lUHqg6KTeUgp+/Sk5/jib7n7qJKTKop5hwH9P6s0gMOyBPk0PhYAX2iV/Om82qPs8lfkT7hPivA6j6vUvZPcKM8GvKC2GRVV3Zwm6xunDzepztAYnX4fIVJAYh2HjozpN0jXIPD7EPuzmlqsnCpoyvzaJLHhDZLNLn/MkLflY7lx8VJTyA02zdxH5pJUDK8OIO7rV0PvqNDVCgU1Pg+0zur9FtlxyJ0SVXiSDqKaLK/eqVqI6fguI+mIao8VojH9K/096v7sin85n14dfaq30psTdn+3AO9rI0qcYXX2g9cBFX0GsRY5TOzvkFGCSyJcZ26uX6Ig4TE2EJ6pDYDaRoy0nLOB2Dq7EYZNa2BdClGMFG/oeJ+eV/cNbiKSOM5hnSYeWbivUY9ynS2p4QT90v9sKvfe0iwer5PqktZvtMPJkhRnvz5zCcWe3mWAQkl7m2oJQ3k926U16Rh/zVGC0qV8jvFwGtla5vcPWQA/Y82Ph9dmAsz/D1qSNuyCT0yrF43/XGMBC+kpytpLWH5TXtWviheZgXivCr4R0qWIXdk6q/KEmXf2IMl5xjDN06xz1wB3EPsKDnWvg+tEzyaWAofIl0uDkKPzLPYT2SfM8CGIym/c5RgEAj41ar3MWDUkXmWTtc7wvxqQQLqnCLBhOQxEm5aP
On Thu, 2 Apr 2020 11:55:51 -0400
"jonikelee AT gmail.com"
<jonikelee AT gmail.com>
wrote:
> On Thu, 2 Apr 2020 11:23:31 -0400
> "jonikelee AT gmail.com"
>
> <jonikelee AT gmail.com>
> wrote:
>
> > 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
> >
>
> Somewhere, I had a version of this hack that grouped like-typed
> hypotheses together to take full advantage of ProofGeneral's ability
> to list adjacent like-typed hypotheses on the same line. I'll look
> for it...
This 'minlines' tactic is it, from:
https://github.com/jonleivent/mindless-coding-phase2/blob/master/utils.v
Ltac revert_all :=
repeat lazymatch goal with H:_ |- _ => revert H end.
Ltac get_value H := eval cbv delta [H] in H.
Ltac has_value H := let X:=get_value H in idtac.
Ltac minlines :=
idtac; (*prevent early eval*)
let stop:=fresh "stop" in
generalize I as stop;
revert_all;
let rec f :=
try (intro;
lazymatch goal with H:?T |- _ =>
first[constr_eq H stop; clear stop
|let v := get_value H in
try match goal with H' := v : T |- _ =>
first[constr_eq H H'; fail 1
|move H before H'] end; f
|try match goal with H':T |- _ =>
first[constr_eq H H'; fail 1
|has_value H'; fail 1
|move H before H'] end; f
|f]
end)
in f.
What this does to the goal in Pierre's example in ProofGeneral: After
the 'onAllHyps move_up_types' tactic, the goal is:
1 subgoal (ID 63)
y : nat
bs2 : list bool
x : nat
bs1 : list bool
l2, l1 : list nat
H0 : l1 = l2 ++ l2
H1 : true :: bs1 = bs2 ++ bs1
H2 : x :: l1 = y :: y :: l2
============================
l1 ++ l2 ++ l1 = (l1 ++ l2) ++ l1
If you then execute 'minlines', the goal becomes:
1 subgoal (ID 96)
y, x : nat
bs2, bs1 : list bool
l2, l1 : list nat
H0 : l1 = l2 ++ l2
H1 : true :: bs1 = bs2 ++ bs1
H2 : x :: l1 = y :: y :: l2
============================
l1 ++ l2 ++ l1 = (l1 ++ l2) ++ l1
They are usable separately or together. I think minlines is idempotent.
I have found minlines particularly useful in goals which have many
hypotheses of simple types (consider a goal with 20 nats scattered
about) and only a few with complex types important to furthering the
proof.
-- Jonathan
- [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.