The Coq mailing list

[Agnishom Chattopadhyay <agnishom AT cmi.ac.in>]

---------- 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