mod Ex01a logic: 'cl'

incl Mtex

loc rem 
  1. CVICENIE Z PREDMETU SPECIFIKACIA A VERIFIKACIA PROGRAMOV

loc rem 
  VASE MENO: ?
  SKUPINA: ?
  VERZIA CL: 5.81.16
  DATUM: stvrtok 17.2.2005
  ******************************************************************************
  SKUSKA (toto je len zakladny ramec, viz. tiez 1. prednaska):
   A = aspon 90 bodov
   B = aspon 80 bodov
   C = aspon 70 bodov
   D = aspon 60 bodov
   E = aspon 50 bodov
  ******************************************************************************
  PMAIL: svp@nw.fmph.uniba.sk
         SUBJECT: prihlasenie sa do skupiny [2i1,2i2,2i3,2i4]
  WWW: http://www.ii.fmph.uniba.sk/cl/view.php/courses/svp

rem 
  \para \bf  Uvodna poznamka.  \end Toto cvicenie je venovane explicitnym 
  definiciam a primitivnej rekurzii. Zadanie sa sklada z tychto suborov: 
  \items 
   \item \para Subor \it  mtex.cl  \end obsahuje makra pre CL-TeX. 
   \item \para Subor(y) \it  maux*.cl  \end obsahuju definicie a vlastnosti 
         pomocnych funkcii a predikatov. 
   \item \para Subor(y) \it  ex01*.cl  \end obsahuju ulohy, ktore mate riesit na 
         tomto cviceni. 
  \end
  \para Tieto subory sa musia skompilovat v spravnom poradi; presny postup je 
  uvedeny v subore \it  readme.txt  \end. 

fun/0 Foo 'Tex_f0_foo'
  Foo = 0

pred/0 Poo 'Tex_p0_poo'
  Poo <-> \f

loc rem 
  ******************************************************************************
  ********************************* EXERCISES **********************************
  ******************************************************************************

rem 
  \para \bf  Literature.  \end 
  \items 
   \item \para \it  [1]  \end J. Komara and P. J. Voda. Metamathematics of 
         Computer Programming. 2001. 
  \end

rem 
  \para \bf  Chapter. Numeric Programs.  \end 

rem 
  \para \bf  Section. Explicit Definitions.  \end 

rem 
  \para \bf  [CL] Monadic case analysis.  \end Syntax: 
  \items 
   \item \para The command \it  case  \end \ft N \end \it  ;  \end 
         \ft Tex0_tau \end invokes monadic case analysis on the term 
         \ft Tex0_tau \end. 
  \end
  \para This means that the current branch of the proof is split in with new 
  assumptions \ft Tex0_tau = 0 \end and \ft Tex0_tau = x+1 \end on the two new 
  branches respectively. The variable \ft x \end is chosen automatically by the 
  system but you can override it by overtyping it with your own variable in the 
  final stage of the prompt for the case command. 
  \para Note that the predicate \ft N \end is defined in the module 
  \ft Standard \end as: 
  \def 
    pred N 
    N(0)
    N(x+1) <- N(x)
  \end
  \para The proof system uses such predicates (you can define your own ones) for 
  the construction of case rules. Try typing just \it  case  \end and the system 
  gives you the full list of case commands available in the current context. We 
  also recommend to use the pseudo-command \it  open  \end to force opening the 
  definitions of defined functions and predicates. 

rem 
  \para \bf  Example of a definition with discrimination on monadic patterns. 
   \end 

fun F_mona 'Tex_f1_f'
  F_mona(0) = 0
  F_mona(x+1) = 1

rem 
  \para \bf  Exercise.  \end Prove 
  \eq Prop_f_mona
    F_mona(x) = 0 \/ F_mona(x) = 1
  \end
  \para \it  Hint.  \end Use monadic case analysis on \ft x \end. 

thm Prop_f_mona
  F_mona(x) = 0 \/ F_mona(x) = 1
proof 
 case N; x @ 0; x1
  proved
  proved..

rem 
  \para \bf  Example of a definition with negation discrimination.  \end 

fun/2 F_neg 'Tex_f2_f'
  F_neg(x,y) = 0 <- x = y
  F_neg(x,y) = 1 <- x != y

rem 
  \para \bf  Exercise.  \end Prove 
  \eq Prop_f_neg
    F_neg(x,y) = 0 \/ F_neg(x,y) = 1
  \end
  \para \it  Hint.  \end Use cut rule with the cut formula \ft x = y \end. 

thm Prop_f_neg
  F_neg(x,y) = 0 \/ F_neg(x,y) = 1
proof 
 cut x = y
  proved
  proved..

rem 
  \para \bf  [CL] Dichotomy case analysis.  \end Syntax: 
  \items 
   \item \para The command \it  case  \end \ft Dich \end \it  ;  \end 
         \ft Tex2_sub(Tex0_tau,1),Tex2_sub(Tex0_tau,2) \end invokes the two way 
         dichotomy case analysis: 
         \ft Tex2_sub(Tex0_tau,1) <= Tex2_sub(Tex0_tau,2) \end versus 
         \ft Tex2_sub(Tex0_tau,1) > Tex2_sub(Tex0_tau,2) \end. 
  \end
  \para The predicate \ft Dich \end is defined in the module \ft Standard \end. 

rem 
  \para \bf  Example of a definition with dichotomy discrimination.  \end 

fun/2 F_dich 'Tex_f2_f'
  F_dich(x,y) = 0 <- x <= y
  F_dich(x,y) = 1 <- x > y

rem 
  \para \bf  Exercise.  \end Prove 
  \eq Prop_f_dich
    F_dich(x,y) = 0 \/ F_dich(x,y) = 1
  \end
  \para \it  Hint.  \end Use dichotomy case analysis. 

thm Prop_f_dich
  F_dich(x,y) = 0 \/ F_dich(x,y) = 1
proof 
 case Dich; x,y @ x1,y1; x1,y1
  proved
  proved..

rem 
  \para \bf  [CL] Trichotomy case analysis.  \end Syntax: 
  \items 
   \item \para The command \it  case  \end \ft Trich \end \it  ;  \end 
         \ft Tex2_sub(Tex0_tau,1),Tex2_sub(Tex0_tau,2) \end invokes the three 
         way trichotomy case analysis: 
         \ft Tex2_sub(Tex0_tau,1) < Tex2_sub(Tex0_tau,2) \end versus 
         \ft Tex2_sub(Tex0_tau,1) = Tex2_sub(Tex0_tau,2) \end versus 
         \ft Tex2_sub(Tex0_tau,1) > Tex2_sub(Tex0_tau,2) \end. 
  \end
  \para The predicate \ft Trich \end is defined in the module \ft Standard \end. 

rem 
  \para \bf  Example of a definition with trichotomy discrimination.  \end 

fun/2 F_trich 'Tex_f2_f'
  F_trich(x,y) = 0 <- x < y
  F_trich(x,y) = 1 <- x = y
  F_trich(x,y) = 2 <- x > y

rem 
  \para \bf  Exercise.  \end Prove 
  \eq Prop_f_trich
    F_trich(x,y) = 0 \/ F_trich(x,y) = 1 \/ F_trich(x,y) = 2
  \end
  \para \it  Hint.  \end Use trichotomy case analysis. 

thm Prop_f_trich
  F_trich(x,y) = 0 \/ F_trich(x,y) = 1 \/ F_trich(x,y) = 2
proof 
 case Trich; x,y @ x1,y1; x1,y1; x1,y1
  proved
  proved
  proved..

rem 
  \para \bf  Minimum.  \end 

fun/2 Min 'Tex_f2_pa_min'
  Min(x,y) = x <- x <= y
  Min(x,y) = y <- x > y

rem 
  \para \bf  Exercise.  \end Prove 
  \eq Spec_min_le1
    Min(x,y) <= x
  \end
  \eq Spec_min_le2
    Min(x,y) <= y
  \end
  \eq Spec_min_eq
    Min(x,y) = x \/ Min(x,y) = y
  \end

thm Spec_min_le1
  Min(x,y) <= x
proof 
 case Dich; x,y @ x1,y1; x1,y1
  proved
  proved..

thm Spec_min_le2
  Min(x,y) <= y
proof 
 case Dich; x,y @ x1,y1; x1,y1
  proved
  proved..

thm Spec_min_eq
  Min(x,y) = x \/ Min(x,y) = y
proof 
 case Dich; x,y @ x1,y1; x1,y1
  proved
  proved..

rem 
  \para \bf  Exercise.  \end \header* fun/2 Max 'Tex_f2_pa_max' \end Find an 
  explicit definition of the maximum function \ft Max(x,y) \end satisfying 
  \eq Spec_max_ge1
    Max(x,y) >= x
  \end
  \eq Spec_max_ge2
    Max(x,y) >= y
  \end
  \eq Spec_max_eq
    Max(x,y) = x \/ Max(x,y) = y
  \end
  \para Prove that the function has the required properties. 

fun/2 Max 'Tex_f2_pa_max'
  Max(x,y) = x <- x >= y
  Max(x,y) = y <- x < y

thm Spec_max_ge1
  Max(x,y) >= x
proof 
 case Dich; y,x @ x1,y1; x1,y1
  proved
  proved..

thm Spec_max_ge2
  Max(x,y) >= y
proof 
 case Dich; y,x @ x1,y1; x1,y1
  proved
  proved..

thm Spec_max_eq
  Max(x,y) = x \/ Max(x,y) = y
proof 
 case Dich; y,x @ x1,y1; x1,y1
  proved
  proved..

rem 
  \para \bf  Exercise.  \end Prove 
  \eq Min_max_le
    Min(x,y) <= Max(x,y)
  \end
  \eq Min_max_eq
    Min(x,y) = Max(x,y) <-> x = y
  \end

thm Min_max_le
  Min(x,y) <= Max(x,y)
proof 
 use Spec_min_le1; x; y
  use Spec_max_ge1; x; y proved...

thm Min_max_eq
  Min(x,y) = Max(x,y) <-> x = y
proof 
 split* Min(x,y) = Max(x,y) <-> x = y.2,0,0
  use Spec_min_le1; x; y
   use Spec_max_ge1; x; y
    use Spec_min_le2; x; y
     use Spec_max_ge2; x; y proved....
  proved..

rem 
  \para \bf  Exercise.  \end \header* fun/3 Median  \end Find an explicit 
  definition of the function \ft Median(x,y,z) \end satisfying 
  \eq Spec_median_le
    x <= y & y <= z -> Median(x,y,z) = y
  \end
  \eq Spec_median_perm213
    Median(x,y,z) = Median(y,x,z)
  \end
  \eq Spec_median_perm132
    Median(x,y,z) = Median(x,z,y)
  \end
  \para Prove that the function has the required properties. 

fun/3 Median 
  Median(x,y,z) = y <- x <= y & y <= z
  Median(x,y,z) = z <- x <= y & y > z & x <= z
  Median(x,y,z) = x <- x <= y & y > z & x > z
  Median(x,y,z) = x <- x > y & y <= z & x <= z
  Median(x,y,z) = z <- x > y & y <= z & x > z
  Median(x,y,z) = y <- x > y & y > z

thm Spec_median_le
  x <= y & y <= z -> Median(x,y,z) = y
proof  proved.

thm Spec_median_perm213
  Median(x,y,z) = Median(y,x,z)
proof 
 case Dich; x,y @ x1,y1; x1,y1
  case Dich; y,z @ x1,y1; x1,y1
   case Dich; y,x @ x1,y1; x1,y1
    proved
    proved.
   case Dich; x,z @ x1,y1; x1,y1
    proved
    case Dich; y,x @ x1,y1; x1,y1
     proved
     proved...
  case Dich; y,z @ x1,y1; x1,y1
   case Dich; x,z @ x1,y1; x1,y1
    proved
    proved.
   proved...

thm Spec_median_perm132
  Median(x,y,z) = Median(x,z,y)
proof 
 case Dich; x,y @ x1,y1; x1,y1
  case Dich; y,z @ x1,y1; x1,y1
   case Dich; z,y @ x1,y1; x1,y1
    proved
    proved.
   case Dich; x,z @ x1,y1; x1,y1
    proved
    proved..
  case Dich; y,z @ x1,y1; x1,y1
   case Dich; x,z @ x1,y1; x1,y1
    proved
    case Dich; z,y @ x1,y1; x1,y1
     proved
     proved..
   proved...