ϵ">]> Clausal Language (ver. 5.81.20, by P.J. Voda, J. Komara, J. Kluka)
...
Clausal Language (ver. 5.81.20, by P.J. Voda, J. Komara, J. Kluka)
Module  Ex08 in logic: Peano arithmetic
Included module  Standard
Included module  Mtex
Included module  Mtexg
Included module  Mtexln
Included module  Maux
Remark 

Literature.

  • [1] J. Komara. Specification and Verification of Programs. Downloadable lecture notes available through the web page of the course.

  • [2] J. Komara and P. J. Voda. Metamathematics of Computer Programming. 2001.

Remark 

[CL] Catalan pairing function and its projections. See the module Maux*.

Remark 

Chapter. Programs Operating on Lists.

Remark 

Section. Lists.

Remark 

[CL] Structural case analysis on lists. Syntax:

case Ln ; <term>

Example(s):

  • caseLn;t

      t=0 ∣ t=v,w

    where v and w are new variables (eigen-variables).

The predicate Ln is defined in the module Standard.

Remark 

[CL] Structural induction on lists. Syntax:

ind Ln ; <variable> [; <variable(s)>]

where the induction formula is formed from the current sequent.

Example(s):

  • indLn;x

    φ [x] ∗ φ [0] ∗ ∣ φ [w] →φ [v,w] ∗

  • indLn;x;a

    φ [x] ∗ φ [0] ∗ ∣ ∀aφ [w] →φ [v,w] ∗

The predicate Ln is defined in the module Standard.

Remark 

List length.

Function  L
L (0) =0 L ( v , w ) =L (w) +1
Remark 

Exercise. Prove

L (x) =0↔x=0 ∃ x L ( x ) =n 
##
Theorem  L_is_zero
L (x) =0↔x=0 
##
Theorem  L_surjective
∃ x L ( x ) =n
Remark 

Exercise. Show that

Function  L
L ( x ) = μ n [ π2 n ( x ) =0]

by proving

π2 L (x) (x) =0 n<L (x) → π2n (x) ≠0 
##
Theorem  L_by_minimalization1
π2 L (x) (x) =0 
##
Theorem  L_by_minimalization2
n<L (x) → π2n (x) ≠0
Remark 

List indexing.

Function  Sub  / 2 displayed by Tex_f2_ln_sub as  #1 [ #2 ]
x [0] =v← x= v , w x [ i +1] =w [i] ← x= v , w
Remark 

Remark. Note that by default

0 [i] =0
Theorem  Sub_default
0 [i] =0
Remark 

Exercise. Prove

x [0] = π1 (x) x [i+1] = π2 (x) [i]

Hint. By structural case analysis on the list x . 

##
Theorem  Sub_zero
x [0] = π1 (x) 
##
Theorem  Sub_succ
x [i+1] = π2 (x) [i]
Remark 

Exercise. Prove

x [i] = π1 π2i (x) 
##
Theorem  Sub_expl
x [i] = π1 π2i (x)
Remark 

List concatenation.

Function  Conc  / 2 displayed by Tex_f2_ln_conc as  #1 ⊕ #2
0⊕ y =y ( v , w ) ⊕ y =v,w⊕y
Remark 

Remark. We write x⊕y⊕z as an abbreviation for (x⊕y) ⊕z .

Remark 

Exercise. Prove

x⊕y=0↔x=0∧y=0 x⊕0=x x⊕ (y⊕z) =x⊕y⊕z x⊕y=x⊕z→y=z x⊕ (a,0) =y⊕ (b,0) →x=y∧a=b x⊕z=y⊕z→x=y 
##
Theorem  Conc_is_zero
x⊕y=0↔x=0∧y=0 
##
Theorem  Conc_zero_right
x⊕0=x 
##
Theorem  Conc_assoc
x⊕ (y⊕z) =x⊕y⊕z 
##
Theorem  Conc_cancel_left
x⊕y=x⊕z→y=z 
##
Theorem  Conc_cancel_last
x⊕ (a,0) =y⊕ (b,0) →x=y∧a=b 
##
Theorem  Conc_cancel_right
x⊕z=y⊕z→x=y
Remark 

[CL] Remark. The list concatenation function x⊕y , written as x++y, is defined in the module Standard and the following properties are built in into the CL theorem prover:

0⊕y=y (v,w) ⊕y=v,w⊕y x⊕y=0↔x=0∧y=0 x⊕0=x x⊕ (y⊕z) =x⊕y⊕z x⊕y=x⊕z↔y=z x⊕ (a,0) =y⊕ (b,0) ↔x=y∧a=b x⊕z=y⊕z↔x=y x⊕y=a,0→x=a,0∧y=0∨x=0∧y=a,0 x⊕ (a,y) =a,0↔x=0∧y=0 x⊕a⊕y=a,0↔a=0∧x⊕y=0,0

From now on we will be using the built-in version of the list concatenation function.

Remark 

Exercise.

L (x⊕y) =L (x) +L (y) i<L (x) → (x⊕y) [i] =x [i] i<L (y) → (x⊕y) [L (x) +i] =y [i] x≠0↔ ∃ y ∃ a x= y ⊕ ( a ,0) 
##
Theorem  Conc_l
L (x⊕y) =L (x) +L (y) 
##
Theorem  Conc_sub_left
i<L (x) → (x⊕y) [i] =x [i] 
##
Theorem  Conc_sub_right
i<L (y) → (x⊕y) [L (x) +i] =y [i] 
##
Theorem  Conc_nzero
x≠0↔ ∃ y ∃ a x= y ⊕ ( a ,0)
Remark 

List membership.

Predicate  In1  / 2 displayed by Tex_p2_ln_in as  #1 ϵ #2
x ϵ v , w ← x=v x ϵ v , w ← x≠v ∧ xϵw
Remark 

Exercise. Prove

xϵv,w↔x=v∨xϵw xϵy⊕z↔xϵy∨xϵz 
##
Theorem  In_pair
xϵv,w↔x=v∨xϵw 
##
Theorem  In_conc
xϵy⊕z↔xϵy∨xϵz
Remark 

[CL] Remark. The list membership predicate x&CLin;y written as x in y, is defined in the module Standard . The following properties are built in into the CL theorem prover:

x&CLin;0↔⊥ x&CLin;v,w↔x=v∨x&CLin;w x&CLin;y⊕z↔x&CLin;y∨x&CLin;z

From now on we will be using the built-in version of the list membership predicate.

Note that the negation x∉y is written as x !in y.

Remark 

List reversal.

Function  Rev
Rev (0) =0 Rev ( v , w ) =Rev (w) ⊕ (v,0)
Remark 

Exercise. Prove

Rev (x) =0↔x=0 Rev (x⊕y) =Rev (y) ⊕Rev (x) RevRev (x) =x Rev (x) =Rev (y) →x=y ∃ y Rev ( y ) =x x&CLin;Rev (y) ↔x&CLin;y LRev (x) =L (x) 
##
Theorem  Rev_is_zero
Rev (x) =0↔x=0 
##
Theorem  Rev_conc
Rev (x⊕y) =Rev (y) ⊕Rev (x) 
##
Theorem  Rev_rev
RevRev (x) =x 
##
Theorem  Rev_injective
Rev (x) =Rev (y) →x=y 
##
Theorem  Rev_surjective
∃ y Rev ( y ) =x 
##
Theorem  Rev_in
x&CLin;Rev (y) ↔x&CLin;y 
##
Theorem  Rev_l
LRev (x) =L (x)
Remark 

Fast list reversal.

Function  Reva  / 2 displayed by Tex_f2_f as  f ( #1 , #2 )
f (0, a ) =a f ( ( v , w ) , a ) =f (w,v,a)
Remark 

Prove

Rev (x) =f (x,0) 
##
Theorem  Rev_by_reva
Rev (x) =f (x,0)
Query:

Results:
Heap used: 439428 free: 133776960
Time used: 0:0:0:39