The Coq mailing list

[Pierre Courtieu <Pierre.Courtieu AT cnam.fr>]

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