Maj terminée. Pour consulter la release notes associée voici le lien :
 Jean-Christophe Filliâtre committed Apr 11, 2012 1 2 3 4 5 6 7 8 9 10 11 `````` (* The 2nd Verified Software Competition (VSTTE 2012) https://sites.google.com/site/vstte2012/compet Problem 2: Combinators S and K *) module Combinators type term = S | K | App term term `````` Guillaume Melquiond committed Mar 17, 2016 12 13 14 15 16 17 18 19 20 `````` let rec predicate eq (x y : term) ensures { result <-> x = y } = match x, y with | S, S -> True | K, K -> True | App x1 x2, App y1 y2 -> eq x1 y1 && eq x2 y2 | _, _ -> False end `````` Jean-Christophe Filliâtre committed Apr 11, 2012 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 `````` (* specification of the CBV reduction *) predicate is_value (t: term) = match t with | K | S -> true | App K v | App S v -> is_value v | App (App S v1) v2 -> is_value v1 /\ is_value v2 | _ -> false end (* contexts *) type context = Hole | Left context term | Right term context predicate is_context (c: context) = match c with | Hole -> true | Left c _ -> is_context c | Right v c -> is_value v && is_context c end function subst (c: context) (t: term) : term = match c with | Hole -> t | Left c1 t2 -> App (subst c1 t) t2 | Right v1 c2 -> App v1 (subst c2 t) end (* one step reduction (the notion of context is inlined in the following definition) *) inductive (-->) (t1 t2: term) = | red_K: forall c: context. is_context c -> forall v1 v2: term. is_value v1 -> is_value v2 -> subst c (App (App K v1) v2) --> subst c v1 | red_S: forall c: context. is_context c -> forall v1 v2 v3: term. is_value v1 -> is_value v2 -> is_value v3 -> subst c (App (App (App S v1) v2) v3) --> subst c (App (App v1 v3) (App v2 v3)) clone import relations.ReflTransClosure with type t = term, predicate rel = (-->) predicate (-->*) (t1 t2: term) = relTR t1 t2 `````` Martin Clochard committed Apr 05, 2018 64 65 66 67 68 69 70 71 72 `````` type zipper = ZHole | ZLeft context term | ZRight term context let rec function subst_c (c ct:context) : context ensures { is_context c /\ is_context ct -> is_context result } = match c with | Hole -> ct | Left c1 t2 -> Left (subst_c c1 ct) t2 | Right v1 c2 -> Right v1 (subst_c c2 ct) end `````` Jean-Christophe Filliâtre committed Apr 11, 2012 73 `````` `````` Martin Clochard committed Apr 05, 2018 74 75 `````` lemma subst_c_commute : forall c [@induction] ct t. subst c (subst ct t) = subst (subst_c c ct) t `````` Jean-Christophe Filliâtre committed Apr 11, 2012 76 77 78 `````` (* task 1: implement CBV reduction *) `````` Martin Clochard committed Apr 05, 2018 79 `````` let rec reduction (ghost c:context) (t: term) : term `````` MARCHE Claude committed Feb 03, 2014 80 `````` diverges (* there are non-normalizable terms... *) `````` Martin Clochard committed Apr 05, 2018 81 82 83 `````` requires { is_context c } ensures { subst c t -->* subst c result } ensures { is_value result } `````` Andrei Paskevich committed Oct 13, 2012 84 `````` = match t with `````` Jean-Christophe Filliâtre committed Apr 11, 2012 85 86 `````` | S -> S | K -> K `````` Martin Clochard committed Apr 05, 2018 87 88 89 90 91 92 93 `````` | App t1 t2 -> let v1 = reduction (subst_c c (Left Hole t2)) t1 in let v2 = reduction (subst_c c (Right v1 Hole)) t2 in match v1 with | K | S | App S _ -> App v1 v2 | App K v3 -> v3 | App (App S v3) v4 -> reduction c (App (App v3 v2) (App v4 v2)) `````` Jean-Christophe Filliâtre committed Apr 11, 2012 94 95 96 97 `````` | _ -> absurd end end `````` MARCHE Claude committed Jan 15, 2014 98 99 `````` exception BenchFailure `````` Guillaume Melquiond committed Mar 17, 2016 100 `````` let constant i = App (App S K) K `````` MARCHE Claude committed Jan 15, 2014 101 `````` `````` MARCHE Claude committed Feb 03, 2014 102 `````` let test_SKK () `````` MARCHE Claude committed Feb 03, 2014 103 `````` diverges (* would be hard to prove terminating *) `````` MARCHE Claude committed Feb 03, 2014 104 `````` raises { BenchFailure -> true } `````` Martin Clochard committed Apr 05, 2018 105 `````` = let t1 = reduction Hole (App i i) in `````` Guillaume Melquiond committed Mar 17, 2016 106 `````` if not (eq t1 i) then raise BenchFailure; `````` Martin Clochard committed Apr 05, 2018 107 `````` let t2 = reduction Hole (App (App (App (App K K) K) K) K) in `````` Guillaume Melquiond committed Mar 17, 2016 108 `````` if not (eq t2 K) then raise BenchFailure; `````` Andrei Paskevich committed Jun 11, 2017 109 `````` t1, t2 `````` MARCHE Claude committed Jan 15, 2014 110 `````` `````` Jean-Christophe Filliâtre committed Apr 11, 2012 111 `````` (* an irreducible term is a value *) `````` Martin Clochard committed Apr 05, 2018 112 `````` predicate irreducible (t: term) = forall t': term. not (t-->t') `````` Jean-Christophe Filliâtre committed Apr 11, 2012 113 `````` `````` Martin Clochard committed Apr 05, 2018 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 `````` exception Fail let rec ghost reduce_step (c:context) (t:term) : term requires { is_context c } ensures { subst c t --> subst c result } raises { Fail -> is_value t } variant { t } = match t with | App t1 t2 -> try App (reduce_step (subst_c c (Left Hole t2)) t1) t2 with Fail -> try App t1 (reduce_step (subst_c c (Right t1 Hole)) t2) with Fail -> match t1 with | App K v -> v | App (App S v1) v2 -> App (App v1 t2) (App v2 t2) | _ -> raise Fail end end end | _ -> raise Fail end `````` Jean-Christophe Filliâtre committed Apr 11, 2012 131 `````` `````` Martin Clochard committed Apr 05, 2018 132 133 134 135 136 137 138 139 140 `````` let rec lemma value_in_context (c:context) (t:term) : unit requires { is_value (subst c t) } ensures { is_value t } variant { c } = match c with | Hole -> () | Left cl _ -> value_in_context cl t | Right _ cr -> value_in_context cr t end `````` Jean-Christophe Filliâtre committed Apr 11, 2012 141 `````` `````` Martin Clochard committed Apr 05, 2018 142 143 144 `````` let lemma irreducible_is_value (t:term) : unit ensures { irreducible t <-> is_value t } = try let _ = reduce_step Hole t in () with Fail -> () end `````` Jean-Christophe Filliâtre committed Apr 11, 2012 145 146 147 148 149 150 151 152 153 154 155 `````` (* task 2 *) use import int.Int inductive only_K (t: term) = | only_K_K: only_K K | only_K_App: forall t1 t2: term. only_K t1 -> only_K t2 -> only_K (App t1 t2) `````` Martin Clochard committed Apr 05, 2018 156 157 `````` let rec reduction2 (ghost c:context) (t: term) : term requires { only_K t /\ is_context c } `````` Andrei Paskevich committed Oct 13, 2012 158 `````` ensures { only_K result /\ is_value result } `````` Martin Clochard committed Apr 05, 2018 159 160 `````` ensures { subst c t -->* subst c result } variant { t } `````` Andrei Paskevich committed Oct 13, 2012 161 `````` = match t with `````` Jean-Christophe Filliâtre committed Apr 11, 2012 162 `````` | K -> K `````` Martin Clochard committed Apr 05, 2018 163 164 165 166 167 168 `````` | App t1 t2 -> let v1 = reduction2 (subst_c c (Left Hole t2)) t1 in let v2 = reduction2 (subst_c c (Right v1 Hole)) t2 in match v1 with | K -> App v1 v2 | App K v3 -> v3 `````` Jean-Christophe Filliâtre committed Apr 11, 2012 169 170 `````` | _ -> absurd end `````` Martin Clochard committed Apr 05, 2018 171 `````` | _ -> absurd `````` Jean-Christophe Filliâtre committed Apr 11, 2012 172 173 174 175 `````` end (* task 3 *) `````` MARCHE Claude committed Jun 11, 2017 176 177 `````` let rec function ks (n: int) : term requires { n >= 0 } `````` Martin Clochard committed Apr 05, 2018 178 `````` ensures { only_K result } `````` MARCHE Claude committed Jun 11, 2017 179 180 `````` variant { n } = if n = 0 then K else App (ks (n-1)) K `````` Jean-Christophe Filliâtre committed Apr 11, 2012 181 `````` `````` MARCHE Claude committed Jun 11, 2017 182 `````` use import number.Parity `````` Jean-Christophe Filliâtre committed Apr 11, 2012 183 `````` `````` Martin Clochard committed Apr 05, 2018 184 185 `````` let rec reduction3 (ghost c:context) (ghost n:int) (t: term) : term requires { n >= 0 /\ t = ks n /\ is_context c } `````` MARCHE Claude committed Jun 11, 2017 186 `````` variant { n } `````` Martin Clochard committed Apr 05, 2018 187 `````` ensures { subst c t -->* subst c result } `````` MARCHE Claude committed Jun 11, 2017 188 189 190 `````` ensures { is_value result } ensures { even n -> result = K } ensures { odd n -> result = App K K } `````` Andrei Paskevich committed Oct 13, 2012 191 `````` = match t with `````` Jean-Christophe Filliâtre committed Apr 11, 2012 192 `````` | K -> K `````` Martin Clochard committed Apr 05, 2018 193 194 195 196 197 198 `````` | App t1 t2 -> let v1 = reduction3 (subst_c c (Left Hole t2)) (n-1) t1 in let v2 = reduction3 (subst_c c (Right v1 Hole)) 0 t2 in match v1 with | K -> App v1 v2 | App K v3 -> v3 `````` Jean-Christophe Filliâtre committed Apr 11, 2012 199 200 `````` | _ -> absurd end `````` Martin Clochard committed Apr 05, 2018 201 `````` | _ -> absurd `````` Jean-Christophe Filliâtre committed Apr 11, 2012 202 203 `````` end `````` Martin Clochard committed Apr 05, 2018 204 205 206 207 208 209 210 `````` let lemma ks_even_odd (n:int) : unit requires { n >= 0 } ensures { ks (2*n) -->* K } ensures { ks (2*n+1) -->* App K K } = let _ = reduction3 Hole (2*n) (ks (2*n)) in let _ = reduction3 Hole (2*n+1) (ks (2*n+1)) in () `````` Jean-Christophe Filliâtre committed Apr 11, 2012 211 212 `````` end``````