Re: [ProofPower] Z Schemas - Help with Initialization and Precondition calculus

```On Tuesday 24 March 2009 05:07:09 Artur Oliveira Gomes wrote:

I'm having hard times to achieve some proofs of preciondition
and initialization using ProofPower.
The file attached contains 3 examples that I still can not prove.
If anyone could help me out with those proofs, I will be thankful.

These are all existential conjectures.

ProofPower is sometimes quite dumb about these things
(sometimes quite smart), it only really knows about
the kinds of existential proofs which are necessary
for proving consistency of things like recursive
definitions (and that stuff only really works for HOL
its not so good in Z).  So usually you will have to
come up with a witness for the existential goal
yourself.

In the case of an existential with a schema as the
signature the witness will usually be a binding
display.  So for each of your proofs you must
come up with the binding display of a witness
for your conjecture, i.e. a binding which satisfies
the body of the existential, and then offer it up
using exists-tac.  Then you have to prove that
your witness does satisfy the predicate.

(I didn't check whether you are trying to prove
the right thing!)

regards,
Roger Jones

___
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

```

Re: [ProofPower] Z Schemas - Help with Initialization and Precondition calculus

```Roger,

In the case of an existential with a schema as the
signature the witness will usually be a binding
display.  So for each of your proofs you must
come up with the binding display of a witness
for your conjecture, i.e. a binding which satisfies
the body of the existential, and then offer it up
using exists-tac.  Then you have to prove that
your witness does satisfy the predicate.

That is exactly what I am doing. Except for those examples,
I can do it fine. I just did not included in the file few steps
until the exist-tac. The problem is: only for those cases,
what I choose as witness does not satisfy the predicate.
I sent the file in order to see if someone could find the right
witness for each of the three goals. ;-)

Regards,

--
Artur Oliveira Gomes
___
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

```

Re: [ProofPower] Z Schemas - Help with Initialization and Precondition calculus

```Artur,

On Tuesday 24 March 2009 10:35:51 Artur Oliveira Gomes wrote:

The problem is: only for those cases,
what I choose as witness does not satisfy the predicate.

Well, any sequence of length 1 (or zero?) does for the
first case. Proof attached.

If you still can't crack the other two send me your
best attempt.

Roger

(*01*)

=SML
open_theory z_library;
delete_theory temp;
new_theory temp;
new_parent z_reals;
=TEX

(*defs*)
�Z
� TYPES ::= AA | BB | CC
�

�ZAX
� TYPE :  � TYPES
���
� TYPE = {AA, BB}
�

�Z
�EXAMPLE � {a:TYPE; b:� � (a,b)}
�

�ZAX
� Example :  EXAMPLE
�

�Z
�S_EXAMPLES � {s:seq EXAMPLE |
�   � i,j: dom s
�   | i � j � � m1,m2: ran s
�   | m1 = s(i) � m2 = s(j)
�   � m1.2 � m2.2}
�

�Z
� S_Example �  �Example�
�

�ZAX
� S_Example2 :  seq EXAMPLE
���
� dom S_Example2 = {1}
�

(*State*)
� AState ���
� a, b, c: S_EXAMPLES
���

(*init of State*)
� InitAState ���
� AState'
���

�Z
� IA_State �  (a' � S_Example2, b' � S_Example2, c' � S_Example2)
�

(*02*)

� Sch ���
� a:�;b,c:�
���

� Sch1 ���
� Sch
���
� a=true
���

� Sch2 ���
� Sch
���
� b=10
���

�Z
� NSch � Sch1 � Sch2
�

(*Schema*)
� BState ���
� var: NSch
���

(*init of State*)
� InitBState ���
� BState'
��
� var' � Sch2
���

� CState ���
� counter: �
���

(*init of State*)
� InitCState ���
� CState'
���

�Z
� State � AState � BState � CState
�

�Z
� St � [StComp : State]
�

(*03*)
� Op1 ��
� �St
���
� � State; State' |
�   StComp = �State � StComp' = �State' �
� counter' = counter + 1 �
�   �(State \�s (counter))'
�   = �(State \�s (counter))

(*Initialization Proofs

Is it this correct? If so, how can
its initialization be proved?*)

push_pc z_library_ext;

(*01*)
set_goal ([], �� AState' � InitAState�);
a (z_�_tac �IA_State�);
a (rewrite_tac [z_get_spec �InitAState�, z_get_spec �AState�,
z_get_spec �S_EXAMPLES�, z_get_spec �IA_State�, z_get_spec
�S_Example2�,
z_get_spec �Example�]);
a (REPEAT z_strip_tac
THEN POP_ASM_T ante_tac
THEN asm_rewrite_tac[]);

(...)

(*02*)  set_goal ([], �� BState' � InitBState�);
(...)

(*Precondition Proofs *)

(*03*)  set_goal ([], �� �St � pre Op1�);
(...)
___
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

```

Re: [ProofPower] Z Schemas - Help with Initialization and Precondition calculus

```Roger,

When I execute:

a (REPEAT z_strip_tac
THEN POP_ASM_T ante_tac
THEN asm_rewrite_tac[]);

ProofPower returns the following message:

:# :# Exception- Fail * the assumption list is empty [POP_ASM_T.9302] *
raised
Exception+ Fail * the assumption list is empty [POP_ASM_T.9302] * raised

Is everything fine?

Artur

2009/3/24 Roger Bishop Jones r...@rbjones.com

Artur,

On Tuesday 24 March 2009 10:35:51 Artur Oliveira Gomes wrote:

The problem is: only for those cases,
what I choose as witness does not satisfy the predicate.

Well, any sequence of length 1 (or zero?) does for the
first case. Proof attached.

If you still can't crack the other two send me your
best attempt.

Roger

___
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

--
Artur Oliveira Gomes
___
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

```