The Coq mailing list

[Paolo Giarrusso <p.giarrusso AT gmail.com>]

On Fri, 10 Apr 2020 at 17:00, Agnishom Chattopadhyay <agnishom AT cmi.ac.in> wrote:

Everyone on this thread has contributed some interesting ideas. I am going to try to see which one works best for me. Thanks.

I am aware of subst, but I do not know how exactly it works. When I try subst, it appears that it removes some hypotheses substituting some quantity for some other and I am often unsure if this is what I want.

I wasn’t sure how much exactly you knew; it does pretty much what I just explained*.

I think that’s almost always safe — in particular, it never makes the goal unprovable. There are limited cases where using subst can complicate a proof, and the “subst x” variant becomes useful — say, after using `remember` to introduce a variable, maybe because you must generalize the induction hypothesis or for other reasons.

But that goal doesn’t _look like_ one of those.

Overall, your call of course, but from my experience I would recommend using it more.

* More precisely, subst finds hypotheses H of form variable = _expression_ (or _expression_ = variable), where _expression_ does not contain variable, substitutes variable by _expression_ everywhere in context, and clears both variable and _expression_. Even more precisely, see the manual:

https://coq.inria.fr/refman/proof-engine/tactics.html#coq:tacn.subst

On Thu, Apr 9, 2020 at 2:13 PM Paolo Giarrusso <p.giarrusso AT gmail.com> wrote:

While this is not what you were asking, there are also tactics to collapse or simplify hypotheses. For instance, the "subst" tactic would get rid of hypotheses like H12 : b2' = hd false bs2'
and of b2' itself by replacing it with its value throughout the context, removing 2 entries from the context for each such hypothesis. "subst x" would only do this for variable x.

I think that would remove 12 such hypotheses (and 12 variables). That's a bit of a sledgehammer, and sometimes you don't want to substitute _everything, but I usually use subst when new variables are introduced.

Cheers,
Paolo

On Thu, 9 Apr 2020 at 21:05, Agnishom Chattopadhyay <agnishom AT cmi.ac.in> 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

--

Paolo G. Giarrusso

--

Paolo G. Giarrusso