coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Agnishom Chattopadhyay <agnishom AT cmi.ac.in>
- To: Paolo Giarrusso <p.giarrusso AT gmail.com>
- Cc: coq-club AT inria.fr
- Subject: Re: [Coq-Club] Fwd: Hiding "Obvious" Hypothesis?
- Date: Fri, 10 Apr 2020 09:59:52 -0500
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=agnishom AT cmi.ac.in; spf=Pass smtp.mailfrom=agnishom AT cmi.ac.in; spf=None smtp.helo=postmaster AT mail.cmi.ac.in
- Ironport-phdr: 9a23:eoGBVxSeZH8nkDqcARuQsHM9XNpsv+yvbD5Q0YIujvd0So/mwa64ZByN2/xhgRfzUJnB7Loc0qyN7PCmBDRIyK3CmU5BWaQEbwUCh8QSkl5oK+++Imq/EsTXaTcnFt9JTl5v8iLzG0FUHMHjew+a+SXqvnY6Uy/yPgttJ+nzBpWaz4Huj7jzqNXvZFBwjT25ZvtdLRystxjKrc5e1ZMkJac40AHUuWBPU+tTzGJsY1mUmkCvyN23+ctK/CJRoPIm8oZrUazmY6MgRLBYHT03ezQ868vqrhnESCOE43paW25QkxweUFuN1w3zQpqk6niyjeF6wiTPeJSuFellCwTn1L9iTVrTsAlCMjc49G/Njckp1fBQpRPnrhc5woiGOdjJZso7RbvUeJYhfUQERtxYDnUTCYa9KYIESesHb74B8tvN4mAWpB77PjGCQePizjgR2C3z1Kw+le8kEEfP10ohGYBWvQ==
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.
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,
PaoloOn 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 buf0There 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
- [Coq-Club] Fwd: Hiding "Obvious" Hypothesis?, Agnishom Chattopadhyay, 04/01/2020
- Re: [Coq-Club] Fwd: Hiding "Obvious" Hypothesis?, Samuel Gruetter, 04/02/2020
- Re: [Coq-Club] Fwd: Hiding "Obvious" Hypothesis?, Pierre Courtieu, 04/02/2020
- Re: [Coq-Club] Fwd: Hiding "Obvious" Hypothesis?, jonikelee AT gmail.com, 04/02/2020
- Re: [Coq-Club] Fwd: Hiding "Obvious" Hypothesis?, jonikelee AT gmail.com, 04/02/2020
- Re: [Coq-Club] Fwd: Hiding "Obvious" Hypothesis?, jonikelee AT gmail.com, 04/02/2020
- Re: [Coq-Club] Fwd: Hiding "Obvious" Hypothesis?, Pierre Courtieu, 04/02/2020
- Re: [Coq-Club] Fwd: Hiding "Obvious" Hypothesis?, jonikelee AT gmail.com, 04/03/2020
- Re: [Coq-Club] Fwd: Hiding "Obvious" Hypothesis?, Pierre Courtieu, 04/02/2020
- Re: [Coq-Club] Fwd: Hiding "Obvious" Hypothesis?, jonikelee AT gmail.com, 04/02/2020
- Re: [Coq-Club] Fwd: Hiding "Obvious" Hypothesis?, jonikelee AT gmail.com, 04/02/2020
- Re: [Coq-Club] Fwd: Hiding "Obvious" Hypothesis?, jonikelee AT gmail.com, 04/02/2020
- Re: [Coq-Club] Fwd: Hiding "Obvious" Hypothesis?, Pierre Courtieu, 04/02/2020
- Re: [Coq-Club] Fwd: Hiding "Obvious" Hypothesis?, Paolo Giarrusso, 04/09/2020
- Re: [Coq-Club] Fwd: Hiding "Obvious" Hypothesis?, Agnishom Chattopadhyay, 04/10/2020
- Re: [Coq-Club] Fwd: Hiding "Obvious" Hypothesis?, Paolo Giarrusso, 04/10/2020
- Re: [Coq-Club] Fwd: Hiding "Obvious" Hypothesis?, Agnishom Chattopadhyay, 04/10/2020
- Re: [Coq-Club] Fwd: Hiding "Obvious" Hypothesis?, Samuel Gruetter, 04/02/2020
Archive powered by MHonArc 2.6.18.