Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Fwd: Hiding "Obvious" Hypothesis?

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Fwd: Hiding "Obvious" Hypothesis?


Chronological Thread 
  • From: Pierre Courtieu <Pierre.Courtieu AT cnam.fr>
  • To: Coq Club <coq-club AT inria.fr>
  • Subject: Re: [Coq-Club] Fwd: Hiding "Obvious" Hypothesis?
  • Date: Thu, 2 Apr 2020 10:45:49 +0200
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=Pierre.Courtieu AT cnam.fr; spf=Pass smtp.mailfrom=pierre.courtieu AT gmail.com; spf=None smtp.helo=postmaster AT mail-io1-f68.google.com
  • Ironport-phdr: 9a23:8laikhdS4lhmV/AS6gm67HJ+lGMj4u6mDksu8pMizoh2WeGdxcS8Yx7h7PlgxGXEQZ/co6odzbaP7ua4BSdYvd7B6ClELMUQEUddyI0/pE8JPo2sMQXDNvnkbig3ToxpdWRO2DWFC3VTA9v0fFbIo3e/vnY4ExT7MhdpdKyuQtaBx8u42Pqv9JLNfg5GmCSyYa9oLBWxsA7dqtQajZFtJ6osyhbFuGdEdutZyW90Kl+YghLw6tut8JJ5/Clcpv0s+9RcXanmeqgzUKBVAikhP20p68LnsgXOQxGS7XUGSGUWlRRIAwnB7B7kW5r6rzX3uOlg1iSEJMP6Vb87Vyis4KdtUx/olTwINyUl/2HNi8x/l7xUrRS8rBFi2YHUYYWVNP1jfqPBeN4RWGRMUtpNWyFHH4ixdJUEAfYfMulEron9v1oOogW4BQmwH+Pk1ztEimbr0aEmz+gtFAfL1xEiEd0TqnTZtNr6NKkQXu61wqfGzijNYe1K1jny84XIbgkhrOuQUb5sbcbcy08iHB7FgFWKrozlOiuY2P4Ms2eF9epgT/yggHM5pgF2vziv3NssiojXiYII11vJ8j93wIcrKt2iUk50f8SoHYVXtyGHLYt2XsIiTH91uCsh1rIGv4S0fC0QxJQp3R7ScvqKeJWG7BLkUeaeOzZ4hHR9dbKwhhay7UigyvDnWcWuzFlKqS9Fn9/RvX4Ozxze8taLRud580u72juC1xrf5vxFLE01j6bWKp0sz7gtnZQJq0vDBDX5mEDuga+WaEok/u+o5vziYrr8p5+cM5Z4igD5Mqgzg8C/D+U1PwsUU2iU/uS807Lj/UnnT7lQkvI2lazZvIjbJcQduKG5HxdY3pg/5xu7FTur09QVkWMaIF9EeR+LlYnkNlLWLPD9F/i/glCskDlxx/DBO73sGo3NLnndn7f7Z7Zy9VRQxxY0zdBC/ZJUFrABL+zuWkLqu9zYCwU2Mw2ww+r9FNp90YYeVXqVAqCFKKPSrUOI5uU3LuaQY48VoS/xJOQh5/7zlnA0gkQdfKms3ZsPcn+0BPVmI0ODYXrtmNgNC2kKvhBtBNDt3XaFSHZ4Y2u4F/Y34Sh+A4a7B6/CQJqsifqPxnHoMIdRYzV+C12WC3qgXIKZQesNZT/advdgnyYeWP6KTJI7yRCjqSfxzbNiaOTOrH5L/an/3cR4srWA3So58iZ5WoHEiznUEjNE21gQTjpz55hR5ExwzlDZjPp9iv1cUN1UvrZHDFd8OpnbwOh3Tdv1X1CZJ4bbeBOdWtyjRAoJYJc0yt4KbVx6Hoz73B/G1iuuRbQSku7SXcBmwufnx3H0Yv1F5TPezqBw3VIgS84JO3f03qM=

Nice ltac!
I have something similar in LibHyps without touching the proof term
(thanks to ltac hack from J.Leivant). 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.

Le jeu. 2 avr. 2020 à 04:45, Samuel Gruetter
<gruetter AT mit.edu>
a écrit :
>
> Here's solution which does not exactly hide them, but at least puts
> everything you want to ignore into one place:
>
>
> Require Import Coq.Lists.List. Import ListNotations.
>
>
> Inductive IgnoreAboveThisLine := mkIgnoreAboveThisLine.
>
> Notation "'_______________________'" := IgnoreAboveThisLine.
>
>
> 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.
>
>
> (* 8 lines of hypotheses, variables and hypotheses mixed:
>
> 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
>
> *)
>
>
> repeat match goal with
>
> | x: ?T |- _ =>
>
> match type of T with
>
> | Prop => revert x
>
> end
>
> end.
>
> pose proof mkIgnoreAboveThisLine as __.
>
> repeat match goal with
>
> | x: ?T |- _ =>
>
> repeat match goal with
>
> | y: T |- _ => revert y
>
> end
>
> end.
>
> intros.
>
>
> (* All the hypotheses you're interested in are below the single dashed
> line,
>
> and the variables are sorted by type to save lines:
>
> l1, l2 : list nat
>
> bs1, bs2 : list bool
>
> x, y : nat
>
> __ : _______________________
>
> H0 : l1 = l2 ++ l2
>
> H1 : true :: bs1 = bs2 ++ bs1
>
> H2 : x :: l1 = y :: y :: l2
>
> ============================
>
> l1 ++ l2 ++ l1 = (l1 ++ l2) ++ l1
>
> *)
>
>
>
>
> And since proof general scrolls to the bottom of your goal by default, the
> variables you're not interested in are the first lines which are going to
> be hidden if you run out of space.
>
>
> On Wed, 2020-04-01 at 16:58 -0500, Agnishom Chattopadhyay wrote:
>
>
>
> ---------- Forwarded message ---------
> From: Agnishom Chattopadhyay
> <agnishom AT cmi.ac.in>
> Date: Wed, Apr 1, 2020 at 4:54 PM
> Subject: Hiding "Obvious" Hypothesis?
> To:
> <coq-club AT inria.fr>
>
>
> Hi;
>
> Very often, I end up with a proof environment which looks like this:
>
> buf : list bool
> sc : list bool -> bool
> cnt : nat
> l2, l1 : list A
> H : length l1 > 0
> Hx : length l2 > 0
> b2 : list bool
> m2 : Monitor A
> H0 : eval4 m (l2 ++ l1) = (b2, m2)
> b2' : bool
> m2' : Monitor A
> bs2' : list bool
> H11 : (bs2', m2') = eval4 (monExpandSlider m buf sc cnt) (l2 ++ l1)
> H12 : b2' = hd false bs2'
> H2 : length l1 = cnt
> H1' : eval2 (monExpandSlider m buf sc cnt) (l2 ++ l1) = (b2', m2')
> bs1' : list bool
> m1' : Monitor A
> E : eval4 (monExpandSlider m buf sc cnt) l1 = (bs1', m1')
> bb2' : list bool
> F : eval4 m1' l2 = (bb2', m2')
> H4 : bs2' = bb2' ++ bs1'
> bs1 : list bool
> m1 : Monitor A
> G : eval4 m l1 = (bs1, m1)
> b1 : bool
> mm1 : Monitor A
> E11 : (b1, m1') = eval2 (monExpandSlider m buf sc cnt) l1
> E12 : b1 = hd false bs1'
> buf1 : list bool
> B11 : buf1 = bs1 ++ buf
> B12 : m1' = monSlider m1 buf1 sc
> B13 : b1 = sc buf1
> bb2 : list bool
> I : eval4 m1 l2 = (bb2, m2)
> H5 : b2 = bb2 ++ bs1
> bx2' : bool
> F1 : (bx2', m2') = eval2 (monSlider m1 buf1 sc) l2
> F2 : bx2' = hd false bb2'
> H1 : length buf1 > 0
> buf2 : list bool
> H31 : buf2 = firstn (cnt + length buf) ((bb2 ++ bs1) ++ buf)
> H32 : m2' = monSlider m2 buf2 sc
> H33 : length buf2 = cnt + length buf
> H34 : b2' = sc buf2
> H6 : length buf1 = cnt + length buf
> H7 : bx2' = b2'
> ============================
> exists buf0 : list bool,
> buf0 = firstn (cnt + length buf) ((bb2 ++ bs1) ++ buf) /\
> m2' = monSlider m2 buf0 sc /\ length buf0 = cnt + length buf /\ b2' =
> sc buf0
>
> There is a lot of Hypotheses here, but more than half of these are obvious
> to the Human user. For example, the type of buf, sc, cnt, l2, l1, b2, b2'
> and so on are clear to me. Is there a proof general mode or a plugin or a
> tactic that gives a way to hide these hypotheses?
>
> I suppose one way of classifying such hypotheses would be to look at all
> the hypotheses whose type is not of kind Prop
>
> --Agnishom



Archive powered by MHonArc 2.6.18.

Top of Page