test-jcf.why 1.19 KB
Newer Older
1

2 3 4 5 6 7 8 9 10 11 12
theory Test

  use import bool.Bool

  type t 'a = {| a: 'a; b: bool; c: 'a |}

  goal G: forall x: t bool.
    {| x with a = 0 |}.a = 0

end

13 14 15
theory Order
  type t
  logic (<=) t t
16

17 18 19 20
  axiom le_refl : forall x : t. x <= x
  axiom le_asym : forall x y : t. x <= y -> y <= x -> x = y
  axiom le_trans: forall x y z : t. x <= y -> y <= z -> x <= z
end
21

22 23
theory List
  type list 'a = Nil | Cons 'a (list 'a)
24

25 26 27
  logic mem (x: 'a) (l: list 'a) = match l with
    | Nil -> false
    | Cons y r -> x = y \/ mem x r
28 29 30
  end
end

31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46
theory SortedList
  use import List
  clone import Order as O

  inductive sorted (l : list t) =
    | sorted_nil :
        sorted Nil
    | sorted_one :
        forall x:t. sorted (Cons x Nil)
    | sorted_two :
        forall x y : t, l : list t.
        x <= y -> sorted (Cons y l) -> sorted (Cons x (Cons y l))

  lemma sorted_Cons: 
    forall x: t, l: list t. sorted (Cons x l) -> 
    forall y: t. mem y l -> x <= y
47
end
48

49
theory SortedIntList
50
  use import int.Int
51 52
  use import List
  clone import SortedList with type O.t = int, logic O.(<=) = (<=)
53

54
  goal sorted123: sorted (Cons 1 (Cons 2 (Cons 3 Nil)))
55
end
56

Jean-Christophe Filliâtre's avatar
prelude  
Jean-Christophe Filliâtre committed
57 58
(*
Local Variables: 
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
59
compile-command: "make -C .. tests/test-jcf.gui"
Jean-Christophe Filliâtre's avatar
prelude  
Jean-Christophe Filliâtre committed
60 61
End: 
*)
62