test-claude.why 1.48 KB
Newer Older
MARCHE Claude's avatar
MARCHE Claude committed
1 2
theory TestProp

MARCHE Claude's avatar
MARCHE Claude committed
3 4 5 6
  goal Test0 : true

  goal Test0_5 : true -> false

7
  logic a
MARCHE Claude's avatar
MARCHE Claude committed
8

9 10 11
  logic b

  goal Test1: a and b -> a
MARCHE Claude's avatar
MARCHE Claude committed
12 13 14

end

MARCHE Claude's avatar
db  
MARCHE Claude committed
15
theory TestInt
MARCHE Claude's avatar
MARCHE Claude committed
16 17 18

   use import int.Int

MARCHE Claude's avatar
MARCHE Claude committed
19
   goal Test1: 2+2 = 4
MARCHE Claude's avatar
MARCHE Claude committed
20 21 22

   goal Test2: forall x:int. x*x >= 0

MARCHE Claude's avatar
MARCHE Claude committed
23
   goal Test3: 1<>0 
24 25 26 27 28

   goal Test4: 1=2 -> 3=4 

   goal Test5: forall x:int. x <> 0 -> x*x > 0

29 30
   goal Test6: 2+3 = 5 and (forall x:int. x*x >= 0)

MARCHE Claude's avatar
MARCHE Claude committed
31
   goal Test7: 0 = 2 and 2 = 3 and 4 = 5 and 6 = 7
MARCHE Claude's avatar
MARCHE Claude committed
32

MARCHE Claude's avatar
MARCHE Claude committed
33
   goal Test8: 2+2=4 and 3+3=6
34

35 36 37 38
   axiom A : 1 = 2

   goal Test9: 2+2=5 and 3+3=8

MARCHE Claude's avatar
db  
MARCHE Claude committed
39 40
end

41 42 43 44 45 46 47 48 49 50
theory TestSplit

  logic aa int

  logic bb int

  goal G : aa 0 /\ bb 1 -> false

end

MARCHE Claude's avatar
db  
MARCHE Claude committed
51 52 53
theory TestDiv

   use import int.Int
MARCHE Claude's avatar
MARCHE Claude committed
54 55 56 57 58 59 60 61 62 63 64 65
   use int.EuclideanDivision

   goal EDiv1: EuclideanDivision.div 1 2 = 0

   goal EDiv2: EuclideanDivision.div (-1) 2 = -1

   use int.ComputerDivision

   goal CDiv1: ComputerDivision.div 1 2 = 0

   goal CDiv2: ComputerDivision.div (-1) 2 = 0

MARCHE Claude's avatar
db  
MARCHE Claude committed
66 67
end

68 69 70 71 72 73 74 75 76 77
theory TestList

  use import int.Int
  use import list.List

  logic x : list int

(*
  goal Test1: 
     match x with 
MARCHE Claude's avatar
MARCHE Claude committed
78
     | Nil -> 1 = 0 and 2 = 3
79 80 81 82 83 84 85
     | Cons _ Nil -> 4 = 5 and 6 = 7
     | Cons _ _ -> 8 = 9 /\ 10 = 11
     end  
*)

end  

MARCHE Claude's avatar
MARCHE Claude committed
86

MARCHE Claude's avatar
db  
MARCHE Claude committed
87 88
theory TestReal

89
   use import real.Real
MARCHE Claude's avatar
MARCHE Claude committed
90 91 92

   goal Real1: forall x:real. x <> 0.0 -> x*x <> 0.0

93 94
   use import real.Abs

MARCHE Claude's avatar
MARCHE Claude committed
95
   goal RealAbs1: forall x:real. 100.0 >= abs x >= 1.0 -> x*x >= 1.0
96

MARCHE Claude's avatar
db  
MARCHE Claude committed
97 98 99 100
end

theory TestFloat

101 102 103 104 105
   use import floating_point.Rounding
   use floating_point.Single

   lemma Round_single_01: Single.round NearestTiesToEven 0.1 = 0x0.199999Ap0

MARCHE Claude's avatar
MARCHE Claude committed
106 107
end

MARCHE Claude's avatar
MARCHE Claude committed
108

MARCHE Claude's avatar
MARCHE Claude committed
109