sorted_list.why 1.18 KB
Newer Older
1
2
theory Order
  type t
Andrei Paskevich's avatar
Andrei Paskevich committed
3
  predicate (<=) t t
4
5
6
7
8
9
10
11
12

  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

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

Andrei Paskevich's avatar
Andrei Paskevich committed
13
  predicate mem (x: 'a) (l: list 'a) = match l with
14
15
16
    | Nil -> false
    | Cons y r -> x = y \/ mem x r
  end
MARCHE Claude's avatar
MARCHE Claude committed
17

18
19
20
21
end

theory SortedList
  use import List
22
  clone import Order as O with axiom .
23
24
25
26
27
28
29
30
31
32

  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))

Andrei Paskevich's avatar
Andrei Paskevich committed
33
34
35
  lemma sorted_inf:
    forall x y: t, l: list t. x <= y -> sorted (Cons y l) ->
      sorted (Cons x l)
MARCHE Claude's avatar
MARCHE Claude committed
36

Andrei Paskevich's avatar
Andrei Paskevich committed
37
38
39

  lemma sorted_mem:
    forall x: t, l: list t. sorted (Cons x l) ->
40
    forall y: t. mem y l -> x <= y
MARCHE Claude's avatar
MARCHE Claude committed
41
42
    (* by induction on l *)

43
44
45
46
47
end

theory SortedIntList
  use import int.Int
  use import List
48
49
50
  clone import SortedList with
    type O.t = int, predicate O.(<=) = (<=),
    lemma O.le_refl, lemma O.le_asym, lemma O.le_trans
51
52
53
54

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