The Coq mailing list

[Samuel Gruetter <gruetter AT mit.edu>]

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