Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Using vm_compute and reflexivity

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Using vm_compute and reflexivity


Chronological Thread 
  • From: Kenneth Roe <kendroe AT hotmail.com>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] Using vm_compute and reflexivity
  • Date: Sat, 22 Apr 2017 18:31:16 -0400
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=kendroe AT hotmail.com; spf=SoftFail smtp.mailfrom=kendroe AT hotmail.com; spf=None smtp.helo=postmaster AT nm8-vm3.bullet.mail.ne1.yahoo.com
  • Ironport-phdr: 9a23:/2Ac1B3mc0cprwYLsmDT+DRfVm0co7zxezQtwd8Zse0eLvad9pjvdHbS+e9qxAeQG96Kt7Qc06L/iOPJYSQ4+5GPsXQPItRndiQuroEopTEmG9OPEkbhLfTnPGQQFcVGU0J5rTngaRAGUMnxaEfPrXKs8DUcBgvwNRZvJuTyB4Xek9m72/q89pDXbAhEniaxba9vJxiqsAvdsdUbj5F/Iagr0BvJpXVIe+VSxWx2IF+Yggjx6MSt8pN96ipco/0u+dJOXqX8ZKQ4UKdXDC86PGAv5c3krgfMQA2S7XYBSGoWkx5IAw/Y7BHmW5r6ryX3uvZh1CScIMb5SrA0WTO+76duUhDoiSMHOycg/G/XhMF9jqFWrAu8qxBh3oXYZI6YOOZ7cq7bYNgUR3dOXtxJWiJBHoyyYIQAAfcPM+ZWsYfypVgAoxylCAmwHePvzyNEhn/q0aA41ekqDAHI3BYnH9ILqHnaqcv6NKEUUe+r0KnIzSjIYe9R2Tjj9YPFdRMhru+KXb1ta8rRzlcgGhjFjlWXtYzlOima1uUJs2SB8+VgUuevhnchpgpsoTav3t8hh43Ki44P11zJ+yZ0zJwxKNGlUkJ3fNCpHZhIuyyeNIZ6WN4uTm9rtSog1LEKp5+2cDIXxJg5xRPSbeGMfZKS7RL5TumRJC91hHJ7d7K7gBa/6U6gyuj/W8WtzlZKqyRInsPXuXAQ0xzT7taISudn8kekwzmP1gTT5vtCIU8qiKbXMZ4gzaQwlpoUtkTPBDP5mELzjKOOd0Uk/Pan6/j/b7jipZKQLZJ4hw/9P6g0nsGzHP40PhUAUmWY4ei80afs/Uz9QLVElP02lazZvYjZJcsFoK62HhVV0oE95BukDzem18gYnXwdI1JEfBKLlZTmO1bLIPzgF/ewn0yskCt3x/DBJrDuHpLNLmHanLj9ebZ99lVTxREozdFf4pJUEqsOLOjyWk/3rtzYDwU2Pxa6w+b9W51B0dYVXnvKCauEOovTt0WJ76QhObqifogQ7RXwLf4o+/6mt3g00QsecK+lx5waQHC/AvFvIkHfan3p1IRSWVwWtxYzGbS5wGaJViReMirqUg==
Below is the actual goal that I am trying to use vm_compute on. I modified
your tactic slightly to:

match goal with |- _ = ?X => let y := eval vm_compute in X in
vm_cast_no_check (refl_equal y).

If you want I can email you my entire source tree. There is one function in
the goal, “propagateExists”. Everything else is a constructor.
PropagateExists is a recursive function that traverses the third parameter
and returns another complex structure.

Executing the above tactic is very slow on the goal. Hopefully, I’ve put up
enough information to figure out what is going on.

- Ken

?P1' = propagateExists 0 nil
(AbsUpdateLoc ([!! (have_var) ==== # 1] **
AbsExistsT
([!! (stack) ==== !! (ssss)] **
AbsExistsT
(AbsMagicWand (AbsUpdateWithLoc (AbsUpdateWithLoc (AbsUpdateWithLoc ([!!
(backtrack) ==== # 0] **
AbsExistsT
([v( 0)] **
[v( 2) ==== # 0] **
AbsExistsT
([# 1] **
AbsExistsT
(AbsExistsT
(AbsExistsT
(AbsExistsT
(AbsExistsT
((((TREE( !! (clauses), v( 0), # 21, # 0 :: nil) **
TREE( !! (assignments_to_do_head), v( 1), # 4, # 0 :: nil)
**
TREE( v( 7), v( 2), # 4, # 0 :: nil) **
ARRAY( !! (assignments), # 4, v( 3)) **
ARRAY( !! (watches), # 4, v( 4))) **
(AbsAll TreeRecords( v( 2)) ([ nth( find( v( 3), v( 0)), #
2) <<<< # 4] **
([ nth( find( v( 3), v( 0)), # 3) ==== # 1] *\/* [ nth(
find( v
( 3), v( 0)), # 3) ==== # 2]) **
[ nth( v( 4), nth( find( v( 3), v( 0)), # 2)) ==== nth(
find( v
( 3), v( 0)), # 3)] **
AbsAll TreeRecords( nth( find( v( 3), v( 0)), # 1)) ([ ~~
nth
( find( v( 4), v( 1)), # 2) ==== nth( find( nth(
find( v
( 4), v( 1)), # 1), v( 0)), # 2)])) **
AbsAll range( # 0, # 4) ([ nth( v( 4), v( 0)) ==== # 0]
*\/*
AbsExists

TreeRecords( v( 3)) ([ nth( find( v( 4), v( 0)), # 2) ====
v( 1) //\\ nth
( find( v( 4), v( 0)), # 3) ==== nth( v( 5), v(
1))]))) **
AbsAll TreeRecords( v( 1)) ([ --( v( 2), v( 0) )---> # 1
==== # 0 //\\ nth
( v( 2), v( 0)) ==== v( 0) \\// --( v( 2), v( 0) )--->
# 1 inTree v
( 0) //\\ --( v( 2), --( v( 2), v( 0) )---> # 1 )---> #
0 ==== v
( 0)]) **

AbsEach

range( # 0, # 4) (AbsExistsT
(Path( nth( v( 4), v( 5)), v( 0), v( 6), # 21, # 13 ++++ v(
5) :: nil) **
AbsAll TreeRecords( v( 6)) ([ --( v( 7), v( 0) )---> (# 17
++++ v
( 3)) ==== # 0 //\\ nth( v( 7), v( 0)) ==== v( 0)
\\// --
( v( 7), v( 0) )---> (# 17 ++++ v( 3)) inTree v( 0)
//\\ --
( v( 7), --( v( 7), v( 0) )---> (# 17 ++++ v( 3))
)--->
(# 13 ++++ v( 3)) ==== v( 0)]) **
AbsAll TreeRecords( v( 0)) (AbsExists

range( # 0, # 4) ([ --( v( 1), v( 6) )---> (# 1 ++++ v(
0)) //\\
(nth( v( 4), v( 0)) ==== # 2 \\// nth( v( 4), v( 0))
==== # 0) \\// --
( v( 1), v( 6) )---> (# 5 ++++ v( 2)) //\\ (nth( v(
4), v
( 0)) ==== # 1 \\// nth( v( 4), v( 0)) ==== #
0)])) **
AbsAll range( # 0, # 4) ([ (--( v( 0), v( 1) )---> (# 9
++++ v
( 0)) ==== # 0 \\// --( v( 0), v( 1) )---> (# 1
++++ v
( 0))) \\// --( v( 0), v( 1) )---> (# 5 ++++ v(
0))]) **
AbsAll range( # 0, # 4) ([ ~~ --( v( 1), v( 6) )---> (# 9
++++ v
( 0)) ==== # 0 //\\ (~~ --( v( 1), v( 6) )---> (# 17
++++ v
( 0)) ==== # 0 \\// nth( v( 0), v( 2)) ==== v( 1))
\\//
(--( v( 1), v( 6) )---> (# 9 ++++ v( 0)) ==== # 0
//\\ --
( v( 1), v( 6) )---> (# 17 ++++ v( 0)) ==== # 0)
//\\ ~~ nth
( v( 4), v( 0)) ==== v( 6)]) **
SUM( range( # 0, # 4), ite( --( v( 0), v( 5) )---> (# 9
++++ v
( 0)), # 1, # 0), # 2) **
(SUM( range( # 0, # 4), (--( v( 5), v( 3) )---> (# 1 ++++
v( 0)) \\// --
( v( 5), v( 3) )---> (# 5 ++++ v( 0))) //\\ (ite(
nth( v
( 3), v( 0)) ==== # 0, # 1, # 0)), # 1) **
AbsAll range( # 0, # 4) ([ # 0 <<<< --( v( 1), v( 6)
)---> (# 9 ++++ v
( 0)) //\\ nth( v( 6), v( 0)) ==== # 0 \\// (# 0
<<<< nth
( v( 6), v( 0)) \\// --( v( 1), v( 6) )---> (# 1
++++ v
( 0)) ==== # 0 //\\ --( v( 1), v( 6) )---> (# 5
++++ v
( 0)) ==== # 0)]) **
AbsAll range( # 0, # 4) (AbsAll range( # 0, # 4) ([
((((--( v
( 2), v( 7) )---> (# 9 ++++ v( 0)) \\// --( v(
2), v
( 7) )---> (# 1 ++++ v( 0)) ==== # 0 //\\ --(
v( 2), v
( 7) )---> (# 5 ++++ v( 0)) ==== # 0) \\// ~~
--( v
( 2), v( 7) )---> (# 9 ++++ v( 1))) \\// nth(
v( 5), v
( 1)) ==== # 0) \\// nth( v( 5), v( 1)) ==== #
0) \\// v
( 0) ==== v( 1)] *\/* AbsExists
TreeRecords( v( 4)) ([ nth( find( v( 5), v( 0)), # 2)
==== v
( 2)] **
AbsExists
TreeRecords( find( v( 5), v( 0))) ([ nth( find( v( 6),
v( 0)), # 2) ==== v
( 1)])))) *\/* AbsExists

range( # 0, # 4) ([ --( v( 1), v( 6) )---> (# 1 ++++ v(
0)) //\\ nth
( v( 4), v( 0)) ==== # 2 \\// --( v( 1), v( 6) )--->
(# 5 ++++ v
( 0)) //\\ nth( v( 1), v( 6)) ==== # 1]) **
AbsAll range( # 0, # 4) ([ # 0 ==== nth( v( 4), v( 0))]
*\/* [ --
( v( 1), v( 6) )---> (# 9 ++++ v( 0)) ==== # 0] **
[ # 0 <<<< nth( v( 4), v( 0))] *\/* AbsExists
TreeRecords( v( 3)) ([ nth( find( v( 4), v( 0)), # 2)
==== v
( 1)]) **
AbsExists
TreeRecords( find( v( 0), v( 0))) ([ # 0 <<<< --( v( 2),
v( 7) )--->
(# 1 ++++ nth( find( v( 4), v( 0)), # 2)) //\\ nth(
find
( v( 4), v( 0)), # 3) ==== # 2 \\// # 0 <<<< --(
v( 2), v
( 7) )---> (# 5 ++++ nth( find( v( 4), v( 0)), #
2)) //\\ nth
( find( v( 4), v( 0)), # 3) ==== # 1])) *\/* AbsAll
range
( # 0, # 4) ([ --( v( 1), v( 6) )---> (# 9 ++++ v(
0)) ==== # 0 \\// nth
( v( 4), v( 0)) ==== # 0]))))) **
[!! (assignments_to_do_head) inTree v( 1)] **
[nth( find( !! (assignments_to_do_head), v( 1)), # 1) ==== #
0]) **
([# 0 <<<< v( 7)] *\/* [v( 6) ==== # 0]))))))))) varx v( 0)
++++ # 1) valuex v
( 0) ++++ # 2) ssss v( 0) ++++ # 0) (AbsExistsT
(AbsExistsT
(AbsExistsT
(AbsExistsT
(AbsExistsT
(v( 0) ++++ # 3 |-> v( 4) **
v( 0) ++++ # 2 |-> v( 3) **
v( 0) ++++ # 1 |-> v( 2) **
v( 0) ++++ # 0 |-> v( 1) **
[v( 5) ==== v( 0)]))))))))) !! (assignments) ++++ !! (varx) # 0)


> On Apr 22, 2017, at 5:39 PM, Laurent Thery
> <Laurent.Thery AT inria.fr>
> wrote:
>
>
>
> On 04/22/2017 11:35 PM, Kenneth Roe wrote:
>> This solution does not quite work. This does indeed apply vm_compute to
>> the ?X term. However, this code will substitute the result or the
>> existential variable. The “reflexivity” tactic will then apply “simpl" to
>> the original “3+4” term. The “3+4” term needs to be evaluated exclusively
>> by vm_compute and nothing else.
>
> That's the point of the vm_cast, the reflexivity will be checked by
> vm_compute.
>
> --
> Laurent


Archive powered by MHonArc 2.6.18.

Top of Page