demo-itp.mlw 2.68 KB
Newer Older
1

2 3 4 5 6 7 8 9

module M
  use import int.Int

  function (++) (x:int) (y:int) : int  = x * y

end

10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30
module TestTaskPrinting

  use import int.Int

  function averyveryveryveryveryverylongname int : int

  goal g1: averyveryveryveryveryverylongname 1 + averyveryveryveryveryverylongname 2 +
           averyveryveryveryveryverylongname 3 + averyveryveryveryveryverylongname 4 >= 0

  goal g2: let x = 1 in x + 1 >= 0

  goal g3: let x = 1 in averyveryveryveryveryverylongname x + averyveryveryveryveryverylongname 1 >= 0

  goal g4: let x = averyveryveryveryveryverylongname 1 in averyveryveryveryveryverylongname x + 1 >= 0

  goal g5: let x = averyveryveryveryveryverylongname 1 + averyveryveryveryveryverylongname 2
           in averyveryveryveryveryverylongname x + 1 >= 0

  goal g6: let x = averyveryveryveryveryverylongname 1 + averyveryveryveryveryverylongname 2
           in averyveryveryveryveryverylongname x + averyveryveryveryveryverylongname 1 >= 0

31 32 33 34 35 36 37 38 39 40
  function (+) (x:int) (y:int) : int  = x * y

  goal g7: 2 + 3 = Int.(+) 3 3

  use import M

  function (++) (x:int) (y:int) : int  = x * y

  goal g8: 2 ++ 3 = M.(++) 3 3

41
end
42

43 44 45 46 47 48 49 50 51
module TestAutomaticIntro


  use import int.Int

  goal g : forall x:int. x > 0 -> forall y z:int. y = z -> x=y

end

52 53 54 55 56 57 58 59 60
module TestInduction

  use import int.Int
  
  predicate p int
  
  goal g : forall n. p n
  
end
61 62 63 64 65 66 67 68 69

module TestInfixSymbols

function (+) int int : int

goal g : false

end

70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89
module TestAutoFocus

  use import int.Int


  goal g0: 0=0 /\ 1=1
  (* "split" should mode you to the first subgoal
     "compute" should then move you to the second goal
     "compute" should then move you to the next goal
   *)

  goal g1: 2+2 = 4
  (* "compute" should move you to the next goal *)

  goal g2: 2+3 = 4
  (* "compute" should move you to the subgoal 5=4 *)


end

90 91 92 93 94 95 96 97 98 99
module TestRewritePoly

  use import int.Int
  use import list.List
  use import list.Append
  
  goal g : (Cons 1 Nil) ++ ((Cons 2 Nil) ++ Nil) = Cons 1 (Cons 2 Nil)
  
end

100

101 102 103 104 105 106 107 108 109 110 111 112 113
module Power

  use import int.Int

  function power int int : int
  axiom power_0 : forall x:int. power x 0 = 1
  axiom power_s : forall x n:int. n >= 0 ->
    power x (n+1) = x * power x n

  lemma power_1 : forall x:int. power x 1 = x

  lemma sqrt4_256 : exists x:int. power x 4 = 256

MARCHE Claude's avatar
MARCHE Claude committed
114
  lemma power_sum : forall x n m: int.
115 116 117 118 119 120 121
    0 <= n /\ 0 <= m ->
    power x (n+m) = power x n * power x m

(* Fermat's little theorem for n = 3 *)

  lemma power_0_left : forall n. n >= 1 -> power 0 n = 0

MARCHE Claude's avatar
MARCHE Claude committed
122
(*
123 124
  lemma power_3 : forall x. x >= 1 ->
    power (x-1) 3 = power x 3 - 3 * x * x + 3 * x - 1
MARCHE Claude's avatar
MARCHE Claude committed
125
*)
126

MARCHE Claude's avatar
MARCHE Claude committed
127 128
  lemma little_fermat_3 :
    forall x : int. x >= 0 -> exists y : int. power x 3 - x = 3 * y
129 130 131 132 133 134

end


(*
Local Variables:
MARCHE Claude's avatar
MARCHE Claude committed
135
compile-command: "why3 ide demo-itp.mlw"
136 137
End:
*)