coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Agnishom Chattopadhyay <agnishom AT cmi.ac.in>
- To: coq-club AT inria.fr
- Subject: [Coq-Club] Fwd: Hiding "Obvious" Hypothesis?
- Date: Wed, 1 Apr 2020 16:58:22 -0500
- Authentication-results: mail2-smtp-roc.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:mU4RJRATcBD6LJtqyrfXUyQJP3N1i/DPJgcQr6AfoPdwSPvzpMbcNUDSrc9gkEXOFd2Cra4d1qyO6Ou4AiRAuc/H7CleNsQUFlcssoY/oU8JOIa9E0r1LfrnPWQRPf9pcxtbxUy9KlVfA83kZlff8TWY5D8WHQjjZ0IufrymUoHdgN6q2O+s5pbdfxtHhCanYbN1MR66sRjdutMZjId/Kqs90AfFr3VHd+hKy25jOFafkwrh6suq85Nv7itdt+g9+8JcVKnxYrg1Q6FfADk6PG8549HmuwPeRgWV/HscVWsWkhtMAwfb6RzxQ4n8vCjnuOdjwSeWJcL5Q6w6VjSk9KdrVQTniDwbOD4j8WHYkdJ/gaRGqx+8vRN/worUYIaINPpie67WYN0XSXZdUstXSidMBJ63YYkSAOobJetXoIf9qFkOoxWwBgeiGf3hxSNTi3DswaE3yf4sHR3a0AEiGd8FrXTarM/yNKcXSe240KbIzTPCb/NN2Tf9743IeQ0/rPGMR71wbdbRyU43Fwzfk1qQqYzkMCmV1+8QtGWU9eVgVeSui248qwFxpT2vy9wwhYnMh4IZ0ErL+jljzIY0I921UUh2asOnHptIryyWKpZ6T8M4T212tys3yacKtYCmcCQQ1ZgqxALTZ+SZf4SU5h/vTuWcLDdiiH54eb+yhgy+/VWix+D9UMS/zUxEoTBfktbWs3AAzxzT5daDSvt65kqh3CyA1wHX6u1ePU80kKvbJ4Q7zbEsjJYTsELDEjf3mEXwkqCWal0p9vW15+nneLnquJCROoxuhg3gL6gigNGzDOckPgQWWmiU4+W81Lnt/U3jR7VKi+U7nbPWsJDcJMQbva65AwhQ0os49xm/Cjam3M4CknYbNl5FeRSHg5DzO17SOPD4Eeu/g1O0nTh3wPDGJ6TtDYnJLnjei7jsZq196k5ZyAor199T/ZNUCrcbIPLyQED9rtLYDgVqezCzlu3gEZB20p4UcWOJGK6Qdq3I4nGS4ed6CuaKZZQVvzO1APgs++LplXY1mU4UbOH91JQRaWu4GfFOKECYJ3PnxNYHRzRZ9jEiRfDn3QXRGQVYYGy/CvplumMLTbm+BIKGfbiDxaSb1X7iTJZTZyZPARaNFyWwLtTWa7I3cCuXZ/RZvHkBXLmlRZUm0Ej35gT/yvxuJazV/H9B7M+x5J1O/+TW0CoK23l0AsCaij/fSmh1miUDQj5w1as5oEovklo=
---------- 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>
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
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
- [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.