sorted_list.why 1.18 KB
 Jean-Christophe Filliâtre committed May 09, 2011 1 2 ``````theory Order type t `````` Andrei Paskevich committed Jun 29, 2011 3 `````` predicate (<=) t t `````` Jean-Christophe Filliâtre committed May 09, 2011 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 committed Jun 29, 2011 13 `````` predicate mem (x: 'a) (l: list 'a) = match l with `````` Jean-Christophe Filliâtre committed May 09, 2011 14 15 16 `````` | Nil -> false | Cons y r -> x = y \/ mem x r end `````` MARCHE Claude committed Mar 26, 2012 17 `````` `````` Jean-Christophe Filliâtre committed May 09, 2011 18 19 20 21 ``````end theory SortedList use import List `````` Andrei Paskevich committed Jun 14, 2018 22 `````` clone import Order as O with axiom . `````` Jean-Christophe Filliâtre committed May 09, 2011 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 committed Oct 20, 2012 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 committed Sep 20, 2011 36 `````` `````` Andrei Paskevich committed Oct 20, 2012 37 38 39 `````` lemma sorted_mem: forall x: t, l: list t. sorted (Cons x l) -> `````` Jean-Christophe Filliâtre committed May 09, 2011 40 `````` forall y: t. mem y l -> x <= y `````` MARCHE Claude committed Sep 20, 2011 41 42 `````` (* by induction on l *) `````` Jean-Christophe Filliâtre committed May 09, 2011 43 44 45 46 47 ``````end theory SortedIntList use import int.Int use import List `````` Andrei Paskevich committed Mar 19, 2016 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 `````` Jean-Christophe Filliâtre committed May 09, 2011 51 52 53 54 `````` goal sorted123: sorted (Cons 1 (Cons 2 (Cons 3 Nil))) end ``````