LambdaSemantics.v 44 KB
Newer Older
charguer's avatar
charguer committed
1 2 3 4 5 6 7 8 9 10 11
(*
Inductive test : nat -> Prop :=
  | test_intro : forall m,
      let n := 3 in
      test (m + n) ->
      test m.

Lemma test_inv : test 5 -> True.
intros M. inversion M.
*)

Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
12
(**
charguer's avatar
charguer committed
13

Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
14 15 16
This file describes the syntax and semantics of a lambda calculus
with mutable heap. The language includes recursive functions, and a
couple of primitive functions. Records and arrays operations are
charguer's avatar
charguer committed
17 18
encoded using pointer arithmetics, and using the [alloc] operation
which allocates at once a requested number of consecutive memory cells.
charguer's avatar
charguer committed
19 20 21 22 23 24

Author: Arthur Charguéraud.
License: MIT.

*)

charguer's avatar
charguer committed
25
Set Implicit Arguments.
charguer's avatar
charguer committed
26
From TLC Require Export LibString LibList LibCore.
charguer's avatar
charguer committed
27
From Sep Require Export Fmap TLCbuffer.
charguer's avatar
charguer committed
28
Open Scope string_scope.
charguer's avatar
charguer committed
29

charguer's avatar
charguer committed
30

charguer's avatar
charguer committed
31
(* ********************************************************************** *)
charguer's avatar
charguer committed
32 33
(* * Source language syntax *)

charguer's avatar
charguer committed
34
(* ---------------------------------------------------------------------- *)
charguer's avatar
charguer committed
35 36
(** Representation of variables and locations *)

charguer's avatar
charguer committed
37 38 39 40 41 42
Definition name := string.

Inductive var := 
  | var_name : name -> var
  | var_special : name -> var.

charguer's avatar
charguer committed
43
Definition loc := nat.
charguer's avatar
charguer committed
44
Definition null : loc := 0%nat.
charguer's avatar
charguer committed
45 46
Definition field := nat.

charguer's avatar
charguer committed
47
Global Opaque field name loc.
charguer's avatar
charguer committed
48

charguer's avatar
charguer committed
49 50

(* ---------------------------------------------------------------------- *)
charguer's avatar
charguer committed
51 52
(** Syntax of the source language *)

charguer's avatar
charguer committed
53
Inductive prim : Type :=
charguer's avatar
charguer committed
54 55 56 57
  | val_ref : prim
  | val_get : prim
  | val_set : prim
  | val_alloc : prim
charguer's avatar
charguer committed
58
  | val_eq : prim
charguer's avatar
charguer committed
59
  | val_sub : prim
charguer's avatar
charguer committed
60
  | val_add : prim
charguer's avatar
charguer committed
61
  | val_ptr_add : prim.
charguer's avatar
charguer committed
62

Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
63
Inductive val : Type :=
charguer's avatar
charguer committed
64
  | val_unit : val
charguer's avatar
charguer committed
65
  | val_bool : bool -> val
charguer's avatar
charguer committed
66 67
  | val_int : int -> val
  | val_loc : loc -> val
charguer's avatar
charguer committed
68
  | val_prim : prim -> val
charguer's avatar
charguer committed
69
  (*| val_fun : var -> trm -> val*)
charguer's avatar
charguer committed
70
  | val_fix : var -> var -> trm -> val
charguer's avatar
charguer committed
71 72 73

with trm : Type :=
  | trm_val : val -> trm
charguer's avatar
charguer committed
74
  | trm_var : var -> trm
charguer's avatar
charguer committed
75 76
  | trm_fun : var -> trm -> trm
  | trm_fix : var -> var -> trm -> trm
charguer's avatar
charguer committed
77
  | trm_if : trm -> trm -> trm -> trm
charguer's avatar
charguer committed
78
  | trm_seq : trm -> trm -> trm
charguer's avatar
charguer committed
79
  | trm_let : var -> trm -> trm -> trm
charguer's avatar
charguer committed
80
  | trm_app : trm -> trm -> trm
charguer's avatar
charguer committed
81
  | trm_while : trm -> trm -> trm
charguer's avatar
charguer committed
82
  | trm_for : var -> trm -> trm -> trm -> trm
charguer's avatar
charguer committed
83
  | trm_unbind : var -> trm -> trm.
charguer's avatar
charguer committed
84

charguer's avatar
charguer committed
85
(** The type of values is inhabited *)
charguer's avatar
charguer committed
86 87

Global Instance Inhab_val : Inhab val.
charguer's avatar
charguer committed
88
Proof using. apply (Inhab_of_val val_unit). Qed.
charguer's avatar
charguer committed
89 90 91 92 93 94


(* ---------------------------------------------------------------------- *)
(** Coercions *)

Coercion val_prim : prim >-> val.
charguer's avatar
charguer committed
95
Coercion val_bool : bool >-> val.
charguer's avatar
charguer committed
96 97 98 99 100
Coercion val_int : Z >-> val.
Coercion val_loc : loc >-> val.
Coercion trm_val : val >-> trm.
Coercion trm_var : var >-> trm.
Coercion trm_app : trm >-> Funclass.
charguer's avatar
charguer committed
101
Coercion var_name : name >-> var.
charguer's avatar
charguer committed
102 103


charguer's avatar
charguer committed
104 105 106
(* ---------------------------------------------------------------------- *)
(** Encoded constructs *)

charguer's avatar
charguer committed
107
(*
charguer's avatar
charguer committed
108
Definition var_special (x:var) : bool :=
charguer's avatar
charguer committed
109 110 111 112
  match x with
  | String h _ => if Ascii.ascii_dec h "$" then true else false
  | _ => false
  end.
charguer's avatar
charguer committed
113 114 115
*)

Definition eq_name_dec := String.string_dec.
charguer's avatar
charguer committed
116

charguer's avatar
charguer committed
117 118
Definition name_eq (x y:name) :=
  if eq_name_dec x y then true else false.
charguer's avatar
charguer committed
119

charguer's avatar
charguer committed
120 121
Lemma var_neq_of_name_dec : forall x y,
  name_eq x y = false ->
charguer's avatar
charguer committed
122
  x <> y.
charguer's avatar
charguer committed
123
Proof using. unfolds name_eq. introv M. case_if~. Qed.
charguer's avatar
charguer committed
124

charguer's avatar
charguer committed
125 126 127 128 129 130
Definition var_eq (x y:var) :=
  match x, y with
  | var_name a, var_name b => name_eq a b
  | var_special a, var_special b => name_eq a b
  | _, _ => false
  end.
charguer's avatar
charguer committed
131

charguer's avatar
charguer committed
132 133
Lemma var_neq_of_var_eq : forall x y,
  var_eq x y = false ->
charguer's avatar
charguer committed
134
  x <> y.
charguer's avatar
charguer committed
135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158
Proof using.
  introv M N. unfolds var_eq.
  destruct x as [a|a]; destruct y as [b|b]; inverts N;
    try applys* var_neq_of_name_dec.
Qed.

(* todo: use decide *)

Lemma name_eq_spec : forall (x y:name),
  name_eq x y = isTrue (x = y).
Proof using.
  intros. unfold name_eq. case_if; rew_bool_eq~.
Qed.

Lemma var_eq_spec : forall (x y:var),
  var_eq x y = isTrue (x = y).
Proof using.
  intros. unfold var_eq. destruct x as [a|a]; destruct y as [b|b];
   try rewrite name_eq_spec; rew_bool_eq.
  { iff M; inverts* M. }
  { introv M; inverts* M. }
  { introv M; inverts* M. }
  { iff M; inverts* M. }
Qed.
charguer's avatar
charguer committed
159

charguer's avatar
charguer committed
160

charguer's avatar
charguer committed
161 162 163 164 165 166 167
(* ********************************************************************** *)
(* * Source language semantics *)

(* ---------------------------------------------------------------------- *)
(** Definition of capture-avoiding substitution *)

Fixpoint subst (y:var) (w:val) (t:trm) : trm :=
charguer's avatar
charguer committed
168
  let aux t := subst y w t in
charguer's avatar
charguer committed
169
  let aux_unbind x t := if var_eq x y then t else aux t in
charguer's avatar
charguer committed
170 171
  match t with
  | trm_val v => trm_val v
charguer's avatar
charguer committed
172
  | trm_var x => if var_eq x y then trm_val w else t
charguer's avatar
charguer committed
173
  | trm_fun x t1 => trm_fun x (aux_unbind x t1)
charguer's avatar
charguer committed
174
  | trm_fix f x t1 => trm_fix f x (if var_eq f y then t1 else
charguer's avatar
charguer committed
175
                                   aux_unbind x t1)
charguer's avatar
charguer committed
176
  | trm_if t0 t1 t2 => trm_if (aux t0) (aux t1) (aux t2)
charguer's avatar
charguer committed
177 178
  | trm_seq t1 t2 => trm_seq (aux t1) (aux t2)
  | trm_let x t1 t2 => trm_let x (aux t1) (aux_unbind x t2)
charguer's avatar
charguer committed
179
  | trm_app t1 t2 => trm_app (aux t1) (aux t2)
charguer's avatar
charguer committed
180 181
  | trm_while t1 t2 => trm_while (aux t1) (aux t2)
  | trm_for x t1 t2 t3 => trm_for x (aux t1) (aux t2) (aux_unbind x t3)
charguer's avatar
charguer committed
182
  | trm_unbind x t1 => if var_eq x y then t else trm_unbind x (aux t1)
charguer's avatar
charguer committed
183 184 185 186 187 188 189 190 191 192 193 194 195 196
  end.


(* ---------------------------------------------------------------------- *)
(** Properties of substitution *)

(** Substitutions for two distinct variables commute. *)

Lemma subst_subst_neq : forall x1 x2 v1 v2 t,
  x1 <> x2 ->
  subst x2 v2 (subst x1 v1 t) = subst x1 v1 (subst x2 v2 t).
Proof using.
  introv N. induction t; simpl; try solve [ fequals;
  repeat case_if; simpl; repeat case_if; auto ].
charguer's avatar
charguer committed
197 198
  { repeat case_if; simpl; repeat case_if~.
    rewrite var_eq_spec in *. rew_bool_eq in *. subst*. }
charguer's avatar
charguer committed
199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216
  { repeat case_if; simpl; repeat case_if~. fequals. }
Qed. (* LATER: simplify *)

(** Substituting for a variable that has just been substituted
    does not further modify the term. *)

Lemma subst_subst_same : forall x v1 v2 t,
  subst x v2 (subst x v1 t) = subst x v1 t.
Proof using.
  intros. induction t; simpl; try solve [ fequals;
  repeat case_if; simpl; repeat case_if; auto; fequals ].
Qed.

(** Substitution commutes with [unbind] for a distinct name. *)

Lemma subst_unbind_neq : forall x y v t,
  x <> y ->
  subst x v (trm_unbind y t) = trm_unbind y (subst x v t).
charguer's avatar
charguer committed
217 218 219 220
Proof using.
  intros. simpl. case_if~.
  rewrite var_eq_spec in *. rew_bool_eq in *. subst*.
Qed.
charguer's avatar
charguer committed
221 222 223 224 225

(** Substitution cancels out on [unbind] for a same name. *)

Lemma subst_unbind_same : forall x v t,
  subst x v (trm_unbind x t) = trm_unbind x t.
charguer's avatar
charguer committed
226 227 228 229
Proof using.
  intros. simpl. case_if~. 
  rewrite var_eq_spec in *. rew_bool_eq in *. subst*.
Qed.
charguer's avatar
charguer committed
230 231 232 233 234 235 236 237 238


(* ---------------------------------------------------------------------- *)
(** Characterization of values *)

Definition trm_is_val (t:trm) : Prop :=
  match t with
  | trm_val v => True
  | _ => False
charguer's avatar
charguer committed
239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254
  end.


(* ---------------------------------------------------------------------- *)
(** Big-step evaluation *)

Section Red.

Definition state := fmap loc val.

Local Open Scope fmap_scope.

Implicit Types t : trm.
Implicit Types v : val.
Implicit Types l : loc.
Implicit Types i : field.
charguer's avatar
charguer committed
255
Implicit Types b : bool.
charguer's avatar
charguer committed
256
Implicit Types n : int.
charguer's avatar
charguer committed
257 258

Inductive red : state -> trm -> state -> val -> Prop :=
charguer's avatar
charguer committed
259
  | red_unbind : forall x t1 m1 m2 v,
charguer's avatar
charguer committed
260
      red m1 t1 m2 v ->
charguer's avatar
charguer committed
261
      red m1 (trm_unbind x t1) m2 v
charguer's avatar
charguer committed
262 263
  | red_val : forall m v,
      red m v m v
charguer's avatar
charguer committed
264
  | red_fun_encoded : forall m1 m2 x t1 r,
charguer's avatar
charguer committed
265
      let f : var := var_special "_" in
charguer's avatar
charguer committed
266 267 268 269
      red m1 (trm_fix f x (trm_unbind f t1)) m2 r ->
      red m1 (trm_fun x t1) m2 r
  (*| red_fun : forall m x t1,
      red m (trm_fun x t1) m (val_fun x t1)*)
charguer's avatar
charguer committed
270 271
  | red_fix : forall m f x t1,
      red m (trm_fix f x t1) m (val_fix f x t1)
charguer's avatar
charguer committed
272 273 274
  | red_if : forall m1 m2 m3 b r t0 t1 t2,
      red m1 t0 m2 (val_bool b) ->
      red m2 (if b then t1 else t2) m3 r ->
charguer's avatar
charguer committed
275
      red m1 (trm_if t0 t1 t2) m3 r
charguer's avatar
charguer committed
276 277 278 279
  | red_let_encoded : forall m1 m2 x t1 t2 r,
      red m1 (trm_app (trm_fun x t2) t1) m2 r ->
      red m1 (trm_let x t1 t2) m2 r
  | red_seq_encoded : forall t1 t2 m1 m2 r,
charguer's avatar
charguer committed
280
      let x : var := var_special "u" in
charguer's avatar
charguer committed
281 282
      red m1 (trm_let x t1 (trm_unbind x t2)) m2 r ->
      red m1 (trm_seq t1 t2) m2 r
charguer's avatar
charguer committed
283
  | red_app_arg : forall m1 m2 m3 m4 t1 t2 v1 v2 r,
charguer's avatar
charguer committed
284
      (~ trm_is_val t1 \/ ~ trm_is_val t2) ->
charguer's avatar
charguer committed
285 286 287 288
      red m1 t1 m2 v1 ->
      red m2 t2 m3 v2 ->
      red m3 (trm_app v1 v2) m4 r ->
      red m1 (trm_app t1 t2) m4 r
charguer's avatar
charguer committed
289
  (*| red_app_fun : forall m1 m2 v1 v2 x t r,
charguer's avatar
charguer committed
290 291
      v1 = val_fun x t ->
      red m1 (subst x v2 t) m2 r ->
charguer's avatar
charguer committed
292
      red m1 (trm_app v1 v2) m2 r*)
charguer's avatar
charguer committed
293
  | red_app_fix : forall m1 m2 v1 v2 f x t r,
charguer's avatar
charguer committed
294 295
      v1 = val_fix f x t ->
      red m1 (subst f v1 (subst x v2 t)) m2 r ->
charguer's avatar
charguer committed
296
      (* red m1 (subst x v2 (subst f v1 t)) m2 r -> todo: remove *)
charguer's avatar
charguer committed
297
      red m1 (trm_app v1 v2) m2 r
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
298
  | red_ref : forall ma mb v l,
charguer's avatar
charguer committed
299 300 301 302 303 304 305 306 307 308 309 310
      mb = (fmap_single l v) ->
      l <> null ->
      \# ma mb ->
      red ma (val_ref v) (mb \+ ma) (val_loc l)
  | red_get : forall m l v,
      fmap_data m l = Some v ->
      red m (val_get (val_loc l)) m v
  | red_set : forall m m' l v,
      m' = fmap_update m l v ->
      red m (val_set (val_loc l) v) m' val_unit
  | red_alloc : forall k n ma mb l,
      mb = fmap_conseq l k val_unit ->
charguer's avatar
charguer committed
311
      n = nat_to_Z k ->
charguer's avatar
charguer committed
312 313 314
      l <> null ->
      \# ma mb ->
      red ma (val_alloc (val_int n)) (mb \+ ma) (val_loc l)
charguer's avatar
charguer committed
315
  | red_add : forall m n1 n2 n',
charguer's avatar
charguer committed
316 317
      n' = n1 + n2 ->
      red m (val_add (val_int n1) (val_int n2)) m (val_int n')
charguer's avatar
charguer committed
318 319 320
  | red_sub : forall m n1 n2 n',
      n' = n1 - n2 ->
      red m (val_sub (val_int n1) (val_int n2)) m (val_int n')
charguer's avatar
charguer committed
321
  | red_ptr_add : forall l' m l n,
charguer's avatar
charguer committed
322
      (l':nat) = (l:nat) + n :> int ->
charguer's avatar
charguer committed
323
      red m (val_ptr_add (val_loc l) (val_int n)) m (val_loc l')
charguer's avatar
charguer committed
324
  | red_eq : forall m v1 v2,
charguer's avatar
charguer committed
325
      red m (val_eq v1 v2) m (val_bool (isTrue (v1 = v2)))
charguer's avatar
charguer committed
326
  | red_while_encoded : forall t1 t2 m1 m2 r,
charguer's avatar
charguer committed
327 328
      let F : var := var_special "f" in
      let U : var := var_special "i" in
charguer's avatar
charguer committed
329 330 331
      let P t := trm_unbind F (trm_unbind U t) in
      red m1 ((val_fix F U (trm_if (P t1) (trm_seq (P t2) (F val_unit)) val_unit)) val_unit) m2 r ->
      red m1 (trm_while t1 t2) m2 r
charguer's avatar
charguer committed
332
  | red_for_arg : forall m1 m2 m3 m4 v1 v2 x t1 t2 t3 r,
charguer's avatar
charguer committed
333
      (* LATER: add [not_is_val t1 \/ not_is_val t2] *)
charguer's avatar
charguer committed
334 335 336
      red m1 t1 m2 v1 ->
      red m2 t2 m3 v2 ->
      red m3 (trm_for x v1 v2 t3) m4 r ->
charguer's avatar
charguer committed
337
      red m1 (trm_for x t1 t2 t3) m4 r
charguer's avatar
charguer committed
338 339
  | red_for : forall m1 m2 x n1 n2 t3 r,
      red m1 (
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
340
        If (n1 <= n2)
charguer's avatar
charguer committed
341 342 343
          then (trm_seq (subst x n1 t3) (trm_for x (n1+1) n2 t3))
          else val_unit) m2 r ->
      red m1 (trm_for x n1 n2 t3) m2 r.
charguer's avatar
charguer committed
344

charguer's avatar
charguer committed
345
  (* Remark: alternative for red_for rules.
charguer's avatar
charguer committed
346 347
    | red_for : forall m1 m2 m3 m4 v1 v2 x t1 t2 t3 r,
        red m1 (
charguer's avatar
charguer committed
348 349 350 351
          (trm_seq (trm_let x n1 t3) (trm_for x (n1+1) n2 t3))
          val_unit) m2 r ->
        red m1 (trm_for x n1 n2 t3) m2 r
  *)
charguer's avatar
charguer committed
352 353 354 355

(* ---------------------------------------------------------------------- *)
(* ** Derived rules *)

charguer's avatar
charguer committed
356
(*
charguer's avatar
charguer committed
357
Hint Resolve var_neq_of_special var_neq_of_string_dec.
charguer's avatar
charguer committed
358 359 360 361 362 363
*)

Section Derived.
Hint Resolve var_neq_of_var_eq.

Notation "'$' x" := (var_special x) (at level 6, format "'$' x"). 
charguer's avatar
charguer committed
364 365

Definition val_fun x t :=
charguer's avatar
charguer committed
366
  val_fix (var_special "_") x (trm_unbind (var_special "_") t).
charguer's avatar
charguer committed
367

charguer's avatar
charguer committed
368 369 370 371
Lemma red_fun : forall m x t1,
  red m (trm_fun x t1) m (val_fun x t1).
Proof using. intros. applys red_fun_encoded. applys red_fix. Qed.

charguer's avatar
charguer committed
372 373
Lemma red_app_fun : forall m1 m2 v1 v2 x t r,
  v1 = val_fun x t ->
charguer's avatar
charguer committed
374
  x <> var_special "_" ->
charguer's avatar
charguer committed
375 376
  red m1 (subst x v2 t) m2 r ->
  red m1 (trm_app v1 v2) m2 r.
charguer's avatar
charguer committed
377
Proof using.
charguer's avatar
charguer committed
378
  introv E N M1. applys red_app_fix E.
charguer's avatar
charguer committed
379 380 381 382
  rewrite~ subst_subst_neq. rewrite subst_unbind_same.
  rewrite~ subst_unbind_neq. applys~ red_unbind.
Qed.

charguer's avatar
charguer committed
383 384 385 386 387 388
Lemma red_app_fun' : forall m1 m2 v1 v2 (x:name) t r,
  v1 = val_fun x t ->
  red m1 (subst x v2 t) m2 r ->
  red m1 (trm_app v1 v2) m2 r.
Proof using. introv E M1. applys* red_app_fun. Qed. 

charguer's avatar
charguer committed
389
Lemma red_let : forall m1 m2 m3 x t1 t2 v1 r,
charguer's avatar
charguer committed
390
  x <> var_special "_" ->
charguer's avatar
charguer committed
391 392 393 394 395 396 397
  red m1 t1 m2 v1 ->
  red m2 (subst x v1 t2) m3 r ->
  red m1 (trm_let x t1 t2) m3 r.
Proof using.
  introv N M1 M2. applys red_let_encoded. applys* red_app_arg.
  { applys* red_fun_encoded. applys red_fix. }
  { applys* red_app_fun. }
charguer's avatar
charguer committed
398 399
Qed.

charguer's avatar
charguer committed
400 401 402 403 404 405
Lemma red_let' : forall m1 m2 m3 (x:name) t1 t2 v1 r,
  red m1 t1 m2 v1 ->
  red m2 (subst x v1 t2) m3 r ->
  red m1 (trm_let x t1 t2) m3 r.
Proof using. introv M1 M2. applys* red_let. Qed.

charguer's avatar
charguer committed
406 407 408 409 410
Lemma red_seq : forall m1 m2 m3 t1 t2 r1 r,
  red m1 t1 m2 r1 ->
  red m2 t2 m3 r ->
  red m1 (trm_seq t1 t2) m3 r.
Proof using.
charguer's avatar
charguer committed
411 412 413 414 415
  introv M1 M2. applys red_seq_encoded. applys* red_let.
  simpl. applys* red_unbind.
Qed.

Lemma red_let_inv : forall m1 m3 x t1 t2 r,
charguer's avatar
charguer committed
416
  x <> var_special "_" ->
charguer's avatar
charguer committed
417 418 419 420 421 422 423
  red m1 (trm_let x t1 t2) m3 r ->
  exists m2 v1, red m1 t1 m2 v1 /\ red m2 (subst x v1 t2) m3 r.
Proof using.
  introv N1 M. inverts M as. introv M. inverts M as. introv N2 M1 M2 M3.
  inversions M1. rename H4 into M1. inverts M1.
  exists___. split. applys M2. 
  inverts M3 as. { introv N3. false. destruct* N3. } introv E M4.
charguer's avatar
charguer committed
424 425
  subst f. inverts E. rewrite~ subst_unbind_neq in M4.
  simpls. inverts M4. auto.
charguer's avatar
charguer committed
426 427
Qed.

charguer's avatar
charguer committed
428 429 430 431 432 433 434 435 436 437 438 439 440 441

(** Note: assuming the semantics of [seq], one can show that [seq] 
(*     has the same semantics has its [let]-based encoding. *)  *)
Lemma red_seq' : forall m1 m2 t1 t2 r,
  let x : var := var_special "u" in
  red m1 (trm_let x t1 (trm_unbind x t2)) m2 r ->
  red m1 (trm_seq t1 t2) m2 r.
Proof using.
  introv M. lets~ (m3&r1&M1&M2): red_let_inv M.
  inverts M2 as. intros M3. applys* red_seq.
Qed.



charguer's avatar
charguer committed
442 443 444 445
Lemma red_seq_inv : forall m1 m3 t1 t2 r,
  red m1 (trm_seq t1 t2) m3 r ->
  exists m2 r1, red m1 t1 m2 r1 /\ red m2 t2 m3 r.
Proof using.
charguer's avatar
charguer committed
446 447
  introv M. inversions M. rename H4 into M. subst x.
  forwards~ (m2&v1&M1&M2): red_let_inv M. simpls. inverts* M2.
charguer's avatar
charguer committed
448 449 450 451 452 453
Qed.

Lemma red_while : forall m1 m2 t1 t2 r,
  red m1 (trm_if t1 (trm_seq t2 (trm_while t1 t2)) val_unit) m2 r ->
  red m1 (trm_while t1 t2) m2 r.
Proof using.
charguer's avatar
charguer committed
454
  introv M1. applys red_while_encoded. applys* red_app_fix.
charguer's avatar
charguer committed
455
  match goal with |- context [val_fix ?f ?x ?t] => set (F:=val_fix f x t) end.
charguer's avatar
charguer committed
456
  simpl. inverts M1 as. introv M1 M2. applys red_if.
charguer's avatar
charguer committed
457
  { do 2 applys* red_unbind. }
charguer's avatar
charguer committed
458 459
  { case_if. 
    { lets (m'&r'&M2'&M3'): red_seq_inv (rm M2). applys red_seq.
charguer's avatar
charguer committed
460 461
      { do 2 applys* red_unbind. }
      { inversion M3'; subst. rename H4 into M4. applys M4. } }
charguer's avatar
charguer committed
462 463 464
    { auto. } }
Qed.

charguer's avatar
charguer committed
465

charguer's avatar
charguer committed
466 467 468 469 470





charguer's avatar
charguer committed
471 472 473
Lemma red_ptr_add_nat : forall m l (f : nat),
  red m (val_ptr_add (val_loc l) (val_int f)) m (val_loc (l+f)%nat).
Proof using. intros. applys* red_ptr_add. math. Qed.
charguer's avatar
charguer committed
474

charguer's avatar
charguer committed
475 476 477
Lemma red_if_bool : forall m1 m2 b r t1 t2,
  red m1 (if b then t1 else t2) m2 r ->
  red m1 (trm_if b t1 t2) m2 r.
charguer's avatar
charguer committed
478
Proof using. introv M1. applys* red_if. applys red_val. Qed.
charguer's avatar
charguer committed
479

charguer's avatar
charguer committed
480 481 482 483 484 485 486 487 488 489 490 491 492 493 494 495 496 497 498 499
Lemma red_for_le : forall m1 m2 m3 x n1 n2 t3 r,
  n1 <= n2 ->
  red m1 (subst x n1 t3) m2 val_unit ->
  red m2 (trm_for x (n1+1) n2 t3) m3 r ->
  red m1 (trm_for x n1 n2 t3) m3 r.
Proof using.
  introv N M1 M2. applys red_for. case_if.
  { applys red_seq. applys M1. applys M2. }
  { false; math. }
Qed.

Lemma red_for_gt : forall m x n1 n2 t3,
  n1 > n2 ->
  red m (trm_for x n1 n2 t3) m val_unit.
Proof using.
  introv N. applys red_for. case_if.
  { false; math. }
  { applys red_val. }
Qed.

charguer's avatar
charguer committed
500
End Derived.
charguer's avatar
charguer committed
501
End Red.
charguer's avatar
charguer committed
502 503 504 505 506


(* ********************************************************************** *)
(* * Notation for terms *)

charguer's avatar
charguer committed
507 508 509 510 511 512 513 514 515 516 517 518 519 520 521 522 523 524 525 526 527 528 529 530 531 532 533 534 535 536
(* ---------------------------------------------------------------------- *)
(** Notation for program variables *)

Notation "''a'" := ("a":var) : var_scope.
Notation "''b'" := ("b":var) : var_scope.
Notation "''c'" := ("c":var) : var_scope.
Notation "''d'" := ("d":var) : var_scope.
Notation "''e'" := ("e":var) : var_scope.
Notation "''f'" := ("f":var) : var_scope.
Notation "''g'" := ("g":var) : var_scope.
Notation "''h'" := ("h":var) : var_scope.
Notation "''i'" := ("i":var) : var_scope.
Notation "''j'" := ("j":var) : var_scope.
Notation "''k'" := ("k":var) : var_scope.
Notation "''l'" := ("l":var) : var_scope.
Notation "''m'" := ("m":var) : var_scope.
Notation "''n'" := ("n":var) : var_scope.
Notation "''o'" := ("o":var) : var_scope.
Notation "''p'" := ("p":var) : var_scope.
Notation "''q'" := ("q":var) : var_scope.
Notation "''r'" := ("r":var) : var_scope.
Notation "''s'" := ("s":var) : var_scope.
Notation "''t'" := ("t":var) : var_scope.
Notation "''u'" := ("u":var) : var_scope.
Notation "''v'" := ("v":var) : var_scope.
Notation "''w'" := ("w":var) : var_scope.
Notation "''x'" := ("x":var) : var_scope.
Notation "''y'" := ("y":var) : var_scope.
Notation "''z'" := ("z":var) : var_scope.

charguer's avatar
charguer committed
537 538 539 540 541 542 543 544 545 546 547 548 549 550 551 552 553 554 555 556 557 558 559 560 561 562 563 564 565 566 567 568 569 570 571 572 573 574 575 576 577 578 579 580 581 582 583 584 585 586 587 588 589 590 591 592 593 594 595 596 597 598 599 600 601 602 603 604 605 606 607 608 609 610 611 612 613 614 615 616
Notation "''a1'" := ("a1":var) : var_scope.
Notation "''b1'" := ("b1":var) : var_scope.
Notation "''c1'" := ("c1":var) : var_scope.
Notation "''d1'" := ("d1":var) : var_scope.
Notation "''e1'" := ("e1":var) : var_scope.
Notation "''f1'" := ("f1":var) : var_scope.
Notation "''g1'" := ("g1":var) : var_scope.
Notation "''h1'" := ("h1":var) : var_scope.
Notation "''i1'" := ("i1":var) : var_scope.
Notation "''j1'" := ("j1":var) : var_scope.
Notation "''k1'" := ("k1":var) : var_scope.
Notation "''l1'" := ("l1":var) : var_scope.
Notation "''m1'" := ("m1":var) : var_scope.
Notation "''n1'" := ("n1":var) : var_scope.
Notation "''o1'" := ("o1":var) : var_scope.
Notation "''p1'" := ("p1":var) : var_scope.
Notation "''q1'" := ("q1":var) : var_scope.
Notation "''r1'" := ("r1":var) : var_scope.
Notation "''s1'" := ("s1":var) : var_scope.
Notation "''t1'" := ("t1":var) : var_scope.
Notation "''u1'" := ("u1":var) : var_scope.
Notation "''v1'" := ("v1":var) : var_scope.
Notation "''w1'" := ("w1":var) : var_scope.
Notation "''x1'" := ("x1":var) : var_scope.
Notation "''y1'" := ("y1":var) : var_scope.
Notation "''z1'" := ("z1":var) : var_scope.

Notation "''a2'" := ("a2":var) : var_scope.
Notation "''b2'" := ("b2":var) : var_scope.
Notation "''c2'" := ("c2":var) : var_scope.
Notation "''d2'" := ("d2":var) : var_scope.
Notation "''e2'" := ("e2":var) : var_scope.
Notation "''f2'" := ("f2":var) : var_scope.
Notation "''g2'" := ("g2":var) : var_scope.
Notation "''h2'" := ("h2":var) : var_scope.
Notation "''i2'" := ("i2":var) : var_scope.
Notation "''j2'" := ("j2":var) : var_scope.
Notation "''k2'" := ("k2":var) : var_scope.
Notation "''l2'" := ("l2":var) : var_scope.
Notation "''m2'" := ("m2":var) : var_scope.
Notation "''n2'" := ("n2":var) : var_scope.
Notation "''o2'" := ("o2":var) : var_scope.
Notation "''p2'" := ("p2":var) : var_scope.
Notation "''q2'" := ("q2":var) : var_scope.
Notation "''r2'" := ("r2":var) : var_scope.
Notation "''s2'" := ("s2":var) : var_scope.
Notation "''t2'" := ("t2":var) : var_scope.
Notation "''u2'" := ("u2":var) : var_scope.
Notation "''v2'" := ("v2":var) : var_scope.
Notation "''w2'" := ("w2":var) : var_scope.
Notation "''x2'" := ("x2":var) : var_scope.
Notation "''y2'" := ("y2":var) : var_scope.
Notation "''z2'" := ("z2":var) : var_scope.

Notation "''a3'" := ("a3":var) : var_scope.
Notation "''b3'" := ("b3":var) : var_scope.
Notation "''c3'" := ("c3":var) : var_scope.
Notation "''d3'" := ("d3":var) : var_scope.
Notation "''e3'" := ("e3":var) : var_scope.
Notation "''f3'" := ("f3":var) : var_scope.
Notation "''g3'" := ("g3":var) : var_scope.
Notation "''h3'" := ("h3":var) : var_scope.
Notation "''i3'" := ("i3":var) : var_scope.
Notation "''j3'" := ("j3":var) : var_scope.
Notation "''k3'" := ("k3":var) : var_scope.
Notation "''l3'" := ("l3":var) : var_scope.
Notation "''m3'" := ("m3":var) : var_scope.
Notation "''n3'" := ("n3":var) : var_scope.
Notation "''o3'" := ("o3":var) : var_scope.
Notation "''p3'" := ("p3":var) : var_scope.
Notation "''q3'" := ("q3":var) : var_scope.
Notation "''r3'" := ("r3":var) : var_scope.
Notation "''s3'" := ("s3":var) : var_scope.
Notation "''t3'" := ("t3":var) : var_scope.
Notation "''u3'" := ("u3":var) : var_scope.
Notation "''v3'" := ("v3":var) : var_scope.
Notation "''w3'" := ("w3":var) : var_scope.
Notation "''x3'" := ("x3":var) : var_scope.
Notation "''y3'" := ("y3":var) : var_scope.
Notation "''z3'" := ("z3":var) : var_scope.
charguer's avatar
charguer committed
617 618 619 620 621 622

Open Scope var_scope.

(* Note: for variable names with several letters, add your own definition *)


charguer's avatar
charguer committed
623
(* ---------------------------------------------------------------------- *)
charguer's avatar
charguer committed
624
(** Notation for concrete programs *)
charguer's avatar
charguer committed
625

charguer's avatar
charguer committed
626 627
Notation "'()" := val_unit : trm_scope.

charguer's avatar
charguer committed
628 629 630
Notation "'If_' t0 'Then' t1 'Else' t2" :=
  (trm_if t0 t1 t2)
  (at level 69, t0 at level 0) : trm_scope.
charguer's avatar
charguer committed
631

charguer's avatar
charguer committed
632 633 634 635
Notation "'If_' t0 'Then' t1 'End'" :=
  (trm_if t0 t1 val_unit)
  (at level 69, t0 at level 0) : trm_scope.

charguer's avatar
charguer committed
636 637
Notation "'Let' x ':=' t1 'in' t2" :=
  (trm_let x t1 t2)
charguer's avatar
charguer committed
638
  (at level 69, x at level 0, right associativity,
charguer's avatar
charguer committed
639 640
  format "'[v' '[' 'Let'  x  ':='  t1  'in' ']'  '/'  '[' t2 ']' ']'") : trm_scope.

charguer's avatar
charguer committed
641
Notation "'Let' 'Rec' f x ':=' t1 'in' t2" :=
charguer's avatar
charguer committed
642
  (trm_let f (trm_fix f x t1) t2)
charguer's avatar
charguer committed
643
  (at level 69, f at level 0, x at level 0, right associativity,
charguer's avatar
charguer committed
644 645
  format "'[v' '[' 'Let'  'Rec'  f  x  ':='  t1  'in' ']'  '/'  '[' t2 ']' ']'") : trm_scope.

646
Notation "t1 ;;; t2" :=
charguer's avatar
charguer committed
647 648
  (trm_seq t1 t2)
  (at level 68, right associativity, only parsing,
649
   format "'[v' '[' t1 ']'  ;;;  '/'  '[' t2 ']' ']'") : trm_scope.
charguer's avatar
charguer committed
650 651

Notation "'Fix' f x ':=' t" :=
charguer's avatar
charguer committed
652
  (trm_fix f x t)
charguer's avatar
charguer committed
653
  (at level 69, f at level 0, x at level 0) : trm_scope.
charguer's avatar
charguer committed
654

charguer's avatar
charguer committed
655 656
Notation "'Fix' f x1 x2 ':=' t" :=
  (trm_fix f x1 (trm_fun x2 t))
charguer's avatar
charguer committed
657
  (at level 69, f at level 0, x1 at level 0, x2 at level 0) : trm_scope.
charguer's avatar
charguer committed
658 659 660

Notation "'Fix' f x1 x2 x3 ':=' t" :=
  (trm_fix f x1 (trm_fun x2 (trm_fun x3 t)))
charguer's avatar
charguer committed
661
  (at level 69, f at level 0, x1 at level 0, x2 at level 0, x3 at level 0) : trm_scope.
charguer's avatar
charguer committed
662

charguer's avatar
charguer committed
663 664
Notation "'ValFix' f x ':=' t" :=
  (val_fix f x t)
charguer's avatar
charguer committed
665
  (at level 69, f at level 0, x at level 0) : trm_scope.
charguer's avatar
charguer committed
666

charguer's avatar
charguer committed
667 668
Notation "'ValFix' f x1 x2 ':=' t" :=
  (val_fix f x1 (trm_fun x2 t))
charguer's avatar
charguer committed
669
  (at level 69, f at level 0, x1 at level 0, x2 at level 0) : trm_scope.
charguer's avatar
charguer committed
670 671 672

Notation "'ValFix' f x1 x2 x3 ':=' t" :=
  (val_fix f x1 (trm_fun x2 (trm_fun x3 t)))
charguer's avatar
charguer committed
673
  (at level 69, f at level 0, x1 at level 0, x2 at level 0, x3 at level 0) : trm_scope.
charguer's avatar
charguer committed
674

charguer's avatar
charguer committed
675 676
Notation "'Fun' x1 ':=' t" :=
  (trm_fun x1 t)
charguer's avatar
charguer committed
677
  (at level 69, x1 at level 0) : trm_scope.
charguer's avatar
charguer committed
678 679 680

Notation "'Fun' x1 x2 ':=' t" :=
  (trm_fun x1 (trm_fun x2 t))
charguer's avatar
charguer committed
681
  (at level 69, x1 at level 0, x2 at level 0) : trm_scope.
charguer's avatar
charguer committed
682

charguer's avatar
charguer committed
683 684
Notation "'Fun' x1 x2 x3 ':=' t" :=
  (trm_fun x1 (trm_fun x2 (trm_fun x3 t)))
charguer's avatar
charguer committed
685
  (at level 69, x1 at level 0, x2 at level 0, x3 at level 0) : trm_scope.
charguer's avatar
charguer committed
686 687 688

Notation "'ValFun' x1 ':=' t" :=
  (val_fun x1 t)
charguer's avatar
charguer committed
689
  (at level 69, x1 at level 0) : trm_scope.
charguer's avatar
charguer committed
690

charguer's avatar
charguer committed
691 692
Notation "'ValFun' x1 x2 ':=' t" :=
  (val_fun x1 (trm_fun x2 t))
charguer's avatar
charguer committed
693
  (at level 69, x1 at level 0, x2 at level 0) : trm_scope.
charguer's avatar
charguer committed
694

charguer's avatar
charguer committed
695 696
Notation "'ValFun' x1 x2 x3 ':=' t" :=
  (val_fun x1 (trm_fun x2 (trm_fun x3 t)))
charguer's avatar
charguer committed
697
  (at level 69, x1 at level 0, x2 at level 0, x3 at level 0) : trm_scope.
charguer's avatar
charguer committed
698

charguer's avatar
charguer committed
699 700
Notation "'LetFun' f x1 ':=' t1 'in' t2" :=
  (trm_let f (trm_fun x1 t1) t2)
charguer's avatar
charguer committed
701
  (at level 69, f at level 0, x1 at level 0) : trm_scope.
charguer's avatar
charguer committed
702 703 704

Notation "'LetFun' f x1 x2 ':=' t1 'in' t2" :=
  (trm_let f (trm_fun x1 (trm_fun x2 t1)) t2)
charguer's avatar
charguer committed
705
  (at level 69, f at level 0, x1 at level 0, x2 at level 0) : trm_scope.
charguer's avatar
charguer committed
706

charguer's avatar
charguer committed
707 708
Notation "'LetFun' f x1 x2 x3 ':=' t1 'in' t2" :=
  (trm_let f (trm_fun x1 (trm_fun x2 (trm_fun x3 t1))) t2)
charguer's avatar
charguer committed
709
  (at level 69, f at level 0, x1 at level 0, x2 at level 0, x3 at level 0) : trm_scope.
charguer's avatar
charguer committed
710

charguer's avatar
charguer committed
711 712
Notation "'LetFix' f x1 ':=' t1 'in' t2" :=
  (trm_let f (trm_fix f x1 t1) t2)
charguer's avatar
charguer committed
713
  (at level 69, f at level 0, x1 at level 0) : trm_scope.
charguer's avatar
charguer committed
714 715 716

Notation "'LetFix' f x1 x2 ':=' t1 'in' t2" :=
  (trm_let f (trm_fix f x1 (trm_fun x2 t1)) t2)
charguer's avatar
charguer committed
717
  (at level 69, f at level 0, x1 at level 0, x2 at level 0) : trm_scope.
charguer's avatar
charguer committed
718 719 720

Notation "'LetFix' f x1 x2 x3 ':=' t1 'in' t2" :=
  (trm_let f (trm_fix f x1 (trm_fun x2 (trm_fun x3 t1))) t2)
charguer's avatar
charguer committed
721
  (at level 69, f at level 0, x1 at level 0, x2 at level 0, x3 at level 0) : trm_scope.
charguer's avatar
charguer committed
722

charguer's avatar
charguer committed
723
Notation "'While' t1 'Do' t2 'Done'" :=
charguer's avatar
charguer committed
724 725
  (trm_while t1 t2)
  (at level 69, t2 at level 68,
charguer's avatar
charguer committed
726
   format "'[v' 'While'  t1  'Do'  '/' '[' t2 ']' '/'  'Done' ']'")
charguer's avatar
charguer committed
727
   : trm_scope.
charguer's avatar
charguer committed
728

charguer's avatar
charguer committed
729
Notation "'For' x ':=' t1 'To' t2 'Do' t3 'Done'" :=
charguer's avatar
charguer committed
730
  (trm_for x t1 t2 t3)
charguer's avatar
charguer committed
731
  (at level 69, x at level 0, (* t1 at level 0, t2 at level 0, *)
charguer's avatar
charguer committed
732
   format "'[v' 'For'  x  ':='  t1  'To'  t2  'Do'  '/' '[' t3 ']' '/'  'Done' ']'")
charguer's avatar
charguer committed
733
  : trm_scope.
charguer's avatar
charguer committed
734

charguer's avatar
charguer committed
735 736 737 738 739 740 741 742 743 744 745 746 747 748 749 750 751 752 753 754 755 756 757
Notation "'ref t" :=
  (val_ref t)
  (at level 67) : trm_scope.

Notation "'! t" :=
  (val_get t)
  (at level 67) : trm_scope.

Notation "t1 ':= t2" :=
  (val_set t1 t2)
  (at level 67) : trm_scope.

Notation "t1 '+ t2" :=
  (val_add t1 t2)
  (at level 69) : trm_scope.

Notation "t1 '- t2" :=
  (val_sub t1 t2)
  (at level 69) : trm_scope.

Notation "t1 '= t2" :=
  (val_eq t1 t2)
  (at level 69) : trm_scope.
charguer's avatar
charguer committed
758

charguer's avatar
charguer committed
759

charguer's avatar
charguer committed
760 761 762 763 764 765
(* ********************************************************************** *)
(* * Size of a term *)

(* ---------------------------------------------------------------------- *)
(** Size of a term, where all values counting for one unit. *)

charguer's avatar
charguer committed
766 767
(* TODO: will be deprecated soon *)

charguer's avatar
charguer committed
768 769 770 771 772 773 774
Fixpoint trm_size (t:trm) : nat :=
  match t with
  | trm_var x => 1
  | trm_val v => 1
  | trm_fun x t1 => 1 + trm_size t1
  | trm_fix f x t1 => 1 + trm_size t1
  | trm_if t0 t1 t2 => 1 + trm_size t0 + trm_size t1 + trm_size t2
charguer's avatar
charguer committed
775
  | trm_seq t1 t2 => 1 + trm_size t1 + trm_size t2
charguer's avatar
charguer committed
776 777
  | trm_let x t1 t2 => 1 + trm_size t1 + trm_size t2
  | trm_app t1 t2 => 1 + trm_size t1 + trm_size t2
charguer's avatar
charguer committed
778
  | trm_while t1 t2 => 1 + trm_size t1 + trm_size t2
charguer's avatar
charguer committed
779
  | trm_for x t1 t2 t3 => 1 + trm_size t1 + trm_size t2 + trm_size t3
charguer's avatar
charguer committed
780
  | trm_unbind x t1 => 1 + trm_size t1
charguer's avatar
charguer committed
781 782 783 784 785
  end.

Lemma trm_size_subst : forall t x v,
  trm_size (subst x v t) = trm_size t.
Proof using.
charguer's avatar
charguer committed
786
  intros. induction t; simpl; repeat case_if; auto. { simpl. math. }
charguer's avatar
charguer committed
787 788 789 790
Qed.

(** Hint for induction on size. Proves subgoals of the form
    [measure trm_size t1 t2], when [t1] and [t2] may have some
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
791
    structure or involve substitutions. *)
charguer's avatar
charguer committed
792

charguer's avatar
charguer committed
793
Ltac solve_measure_trm_size tt :=
charguer's avatar
charguer committed
794 795
  unfold measure in *; simpls; repeat rewrite trm_size_subst; math.

charguer's avatar
charguer committed
796
Hint Extern 1 (measure trm_size _ _) => solve_measure_trm_size tt.
charguer's avatar
charguer committed
797 798


charguer's avatar
charguer committed
799

charguer's avatar
charguer committed
800

charguer's avatar
charguer committed
801
(* ********************************************************************** *)
charguer's avatar
charguer committed
802
(* * Iterated substitutions *)
charguer's avatar
charguer committed
803

charguer's avatar
charguer committed
804
(* ---------------------------------------------------------------------- *)
charguer's avatar
charguer committed
805 806 807
(** Distinct variables *)

(** [vars] is the type of a list of variables *)
charguer's avatar
charguer committed
808 809

Definition vars : Type := list var.
charguer's avatar
charguer committed
810 811 812 813 814 815

(** [var_fresh y xs] asserts that [y] does not belong to the list [xs] *)

Fixpoint var_fresh (y:var) (xs:vars) : bool :=
  match xs with
  | nil => true
charguer's avatar
charguer committed
816
  | x::xs' => if var_eq x y then false else var_fresh y xs'
charguer's avatar
charguer committed
817 818 819 820 821 822 823 824 825
  end.

(** [var_distinct xs] asserts that [xs] consists of a list of distinct variables. *)

Fixpoint var_distinct (xs:vars) : bool :=
  match xs with
  | nil => true
  | x::xs' => var_fresh x xs' && var_distinct xs'
  end.
charguer's avatar
charguer committed
826 827


charguer's avatar
charguer committed
828
(* ---------------------------------------------------------------------- *)
charguer's avatar
charguer committed
829
(** Iterated substitution *)
charguer's avatar
charguer committed
830

charguer's avatar
charguer committed
831
(** [ctx] describes a list of bindings *)
charguer's avatar
charguer committed
832

charguer's avatar
charguer committed
833
Definition ctx := list (var*val).
charguer's avatar
charguer committed
834

charguer's avatar
charguer committed
835
(** [ctx_empty] describes the empty context *)
charguer's avatar
charguer committed
836

charguer's avatar
charguer committed
837 838
Definition ctx_empty : ctx :=
  nil.
charguer's avatar
charguer committed
839

charguer's avatar
charguer committed
840
(** [ctx_add x v E] extends [E] with a binding from [x] to [v] *)
charguer's avatar
charguer committed
841

charguer's avatar
charguer committed
842 843
Definition ctx_add (x:var) (v:val) (E:ctx) :=
  (x,v)::E.
charguer's avatar
charguer committed
844

charguer's avatar
charguer committed
845
(** [ctx_rem x E] removes all bindings on [x] stored in [E] *)
charguer's avatar
charguer committed
846

charguer's avatar
charguer committed
847 848 849 850 851
Fixpoint ctx_rem (x:var) (E:ctx) : ctx :=
  match E with
  | nil => nil
  | (y,v)::E' =>
    let E'' := ctx_rem x E' in
charguer's avatar
charguer committed
852
    if var_eq x y then E'' else (y,v)::E''
charguer's avatar
charguer committed
853
  end.
charguer's avatar
charguer committed
854

charguer's avatar
charguer committed
855 856 857
(** [ctx_lookup x E] returns
    - [None] if [x] is not bound in [E]
    - [Some v] if [x] is bound to [v] in [E]. *)
charguer's avatar
charguer committed
858

charguer's avatar
charguer committed
859 860 861
Fixpoint ctx_lookup (x:var) (E:ctx) : option val :=
  match E with
  | nil => None
charguer's avatar
charguer committed
862
  | (y,v)::E' => if var_eq x y
charguer's avatar
charguer committed
863 864
                   then Some v
                   else ctx_lookup x E'
charguer's avatar
charguer committed
865 866
  end.

charguer's avatar
charguer committed
867 868 869 870 871 872 873 874 875 876 877
(** [ctx_fresh x E] asserts that [x] is not bound in [E] *)

Definition ctx_fresh (x:var) (E:ctx) : Prop :=
  ctx_lookup x E = None.

(** [substs E t] substitutes all the bindings from [E] inside [t] *)

Fixpoint substs (E:ctx) (t:trm) :=
  match E with
  | nil => t
  | (x,v)::E' => substs E' (subst x v t)
charguer's avatar
charguer committed
878
  end.
charguer's avatar
charguer committed
879 880


charguer's avatar
charguer committed
881 882 883 884 885 886 887 888 889 890 891 892 893 894 895 896 897 898 899 900 901 902 903
(* ---------------------------------------------------------------------- *)
(** Properties of iterated substitution *)

(** Auxiliary results *)

Lemma ctx_rem_fresh : forall x E,
  ctx_fresh x E ->
  ctx_rem x E = E.
Proof using.
  introv M. unfolds ctx_fresh. induction E as [|(y,v) E'].
  { auto. } { simpls. case_if. fequals. rewrite~ IHE'. }
Qed.

(** Substituting for [E] without [x] then substituting for [x]
    is equivalent to substituting for [x] then for [E]
    (even if [x] is bound in [E]). *)

Lemma subst_substs_ctx_rem_same : forall E x v t,
    subst x v (substs (ctx_rem x E) t)
  = substs E (subst x v t).
Proof using.
  intros E. induction E as [|(y,w) E']; simpl; intros.
  { auto. }
charguer's avatar
charguer committed
904
  { rewrite var_eq_spec. case_if.
charguer's avatar
charguer committed
905 906 907 908 909 910 911 912 913 914 915 916 917 918 919 920 921 922 923 924 925 926
    { subst. rewrite IHE'. rewrite~ subst_subst_same. }
    { simpl. rewrite IHE'. rewrite~ subst_subst_neq. } }
Qed.

Lemma subst_substs : forall x v E t,
  ctx_fresh x E ->
  subst x v (substs E t) = substs E (subst x v t).
Proof using.
  introv M. forwards N: subst_substs_ctx_rem_same E x v t.
  rewrite~ ctx_rem_fresh in N.
Qed.

(** The following lemmas describe how iterated substitution
    distributes over the construction of the language *)

Ltac substs_simpl_proof :=
  let x := fresh "x" in let w := fresh "w" in
  let E := fresh "E" in let E' := fresh "E'" in
  let IH := fresh "IH" in
  intros E; induction E as [|(x,w) E' IH]; intros; simpl;
  [ | try rewrite IH ]; auto.

charguer's avatar
charguer committed
927 928 929
Lemma substs_unbind : forall E x t1,
   substs E (trm_unbind x t1)
 = trm_unbind x (substs (ctx_rem x E) t1).
charguer's avatar
charguer committed
930 931
Proof using. substs_simpl_proof. case_if; rewrite~ IH. Qed.

charguer's avatar
charguer committed
932 933 934 935 936 937 938 939 940 941 942 943 944 945 946 947 948 949 950 951 952 953 954 955 956 957 958 959 960 961
Lemma substs_val : forall E v,
  substs E (trm_val v) = v.
Proof using. substs_simpl_proof. Qed.

Lemma substs_var : forall E x,
    substs E (trm_var x)
  = match ctx_lookup x E with
    | None => trm_var x
    | Some v => v end.
Proof using.
  substs_simpl_proof.
  { case_if. { rewrite~ substs_val. } { auto. } }
Qed.

Lemma substs_if : forall E t1 t2 t3,
   substs E (trm_if t1 t2 t3)
 = trm_if (substs E t1) (substs E t2) (substs E t3).
Proof using. substs_simpl_proof. Qed.

Lemma substs_app : forall E t1 t2,
   substs E (trm_app t1 t2)
 = trm_app (substs E t1) (substs E t2).
Proof using. substs_simpl_proof. Qed.

Lemma substs_let : forall E x t1 t2,
   substs E (trm_let x t1 t2)
 = trm_let x (substs E t1) (substs (ctx_rem x E) t2).
Proof using. substs_simpl_proof. { fequals. case_if~. } Qed.


charguer's avatar
charguer committed
962
(* ---------------------------------------------------------------------- *)
charguer's avatar
charguer committed
963
(** N-ary substitution *)
charguer's avatar
charguer committed
964

charguer's avatar
charguer committed
965
(** Shorthand [vals] and [trms] for lists of values and terms *)
charguer's avatar
charguer committed
966

charguer's avatar
charguer committed
967 968 969 970 971 972 973 974 975 976 977 978 979 980 981 982 983 984 985 986 987 988 989 990 991 992
Definition vals : Type := list val.
Definition trms : Type := list trm.

(** [substn xs vs t] is a shorthand for [substs (List.combine xs vs) t].
    It substitutes the values [vs] for the corresponding variables in [xs].
    This operation is only specified when [length xs = length vs]. *)

Definition substn (xs:vars) (vs:vals) (t:trm) : trm :=
  substs (LibList.combine xs vs) t.

(** Distribution of [substn] on [nil] and [cons] lists *)

Lemma substn_nil : forall t,
  substn nil nil t = t.
Proof using. auto. Qed.

Lemma substn_cons : forall x xs v vs t,
  substn (x::xs) (v::vs) t = substn xs vs (subst x v t).
Proof using. auto. Qed.

(** Auxiliary results for freshness of bindings w.r.t. combine *)

Lemma ctx_fresh_combine : forall x ys vs,
  var_fresh x ys ->
  length ys = length vs ->
  ctx_fresh x (LibList.combine ys vs).
charguer's avatar
charguer committed
993
Proof using.
charguer's avatar
charguer committed
994
  intros x ys. unfold ctx_fresh.
charguer's avatar
charguer committed
995
  induction ys as [|y ys']; simpl; intros [|v vs] M L;
charguer's avatar
charguer committed
996 997
   rew_list in *; try solve [ false; math ].
  { auto. }
charguer's avatar
charguer committed
998
  { simpl. rewrite var_eq_spec in *. do 2 case_if. rewrite~ IHys'. }
charguer's avatar
charguer committed
999
Qed.
charguer's avatar
charguer committed
1000

charguer's avatar
charguer committed
1001 1002 1003
(* Permutation lemma for substitution and n-ary substitution *)

Lemma subst_substn : forall x v ys ws t,
charguer's avatar
charguer committed
1004 1005
  var_fresh x ys ->
  length ys = length ws ->
charguer's avatar
charguer committed
1006
  subst x v (substn ys ws t) = substn ys ws (subst x v t).
charguer's avatar
charguer committed
1007
Proof using.
charguer's avatar
charguer committed
1008 1009
  introv M L. unfold substn. rewrite~ subst_substs.
  applys~ ctx_fresh_combine.
charguer's avatar
charguer committed
1010 1011
Qed.

charguer's avatar
charguer committed
1012

charguer's avatar
charguer committed
1013 1014 1015 1016 1017 1018 1019 1020 1021 1022 1023 1024 1025 1026 1027 1028 1029 1030 1031 1032 1033 1034 1035 1036 1037 1038 1039 1040 1041 1042 1043 1044 1045 1046 1047 1048 1049 1050 1051 1052 1053 1054 1055
(* ********************************************************************** *)
(* * N-ary functions and applications *)

(** [trm_apps t ts] denotes a n-ary application of [t] to the
    arguments from the list [ts].

    [trm_funs xs t] denotes a n-ary function with arguments [xs]
    and body [t].

    [trm_fixs f xs t] denotes a n-ary recursive function [f]
    with arguments [xs] and body [t].

  The tactic [rew_nary] can be used to convert terms in the goal
  to using the nary constructs wherever possible.

  The operation [substn xs vs t] substitutes the variables [xs]
  with the values [vs] inside the term [t].
*)


(* ---------------------------------------------------------------------- *)
(** Coercions from values to terms *)

Coercion vals_to_trms (vs:vals) : trms :=
  List.map trm_val vs.

(** Tactic [rew_vals_to_trms] to fold the coercion where possible *)

Lemma vals_to_trms_fold_start : forall v,
  (trm_val v)::nil = vals_to_trms (v::nil).
Proof using. auto. Qed.

Lemma vals_to_trms_fold_next : forall v vs,
  (trm_val v)::(vals_to_trms vs) = vals_to_trms (v::vs).
Proof using. auto. Qed.

Hint Rewrite vals_to_trms_fold_start vals_to_trms_fold_next
  : rew_vals_to_trms.

Tactic Notation "rew_vals_to_trms" :=
  autorewrite with rew_vals_to_trms.


charguer's avatar
charguer committed
1056
(* ---------------------------------------------------------------------- *)
charguer's avatar
charguer committed
1057
(** N-ary applications and N-ary functions *)
charguer's avatar
charguer committed
1058

charguer's avatar
charguer committed
1059 1060 1061 1062
Fixpoint trm_apps (tf:trm) (ts:trms) : trm :=
  match ts with
  | nil => tf
  | t::ts' => trm_apps (trm_app tf t) ts'
charguer's avatar
charguer committed
1063
  end.
charguer's avatar
charguer committed
1064

charguer's avatar
charguer committed
1065 1066 1067 1068 1069
Fixpoint trm_funs (xs:vars) (t:trm) : trm :=
  match xs with
  | nil => t
  | x::xs' => trm_fun x (trm_funs xs' t)
  end.
charguer's avatar
charguer committed
1070

charguer's avatar
charguer committed
1071 1072 1073 1074 1075 1076
Definition val_funs (xs:vars) (t:trm) : val :=
  match xs with
  | nil => arbitrary
  | x::xs' => val_fun x (trm_funs xs' t)
  end.

charguer's avatar
charguer committed
1077 1078 1079 1080 1081 1082 1083 1084 1085 1086 1087 1088 1089
Definition trm_fixs (f:var) (xs:vars) (t:trm) : trm :=
  match xs with
  | nil => t
  | x::xs' => trm_fix f x (trm_funs xs' t)
  end.

Definition val_fixs (f:var) (xs:vars) (t:trm) : val :=
  match xs with
  | nil => arbitrary
  | x::xs' => val_fix f x (trm_funs xs' t)
  end.


charguer's avatar
charguer committed
1090 1091 1092 1093 1094 1095 1096 1097
(* ---------------------------------------------------------------------- *)
(** Nonempty list of distinct variables *)

Definition var_funs (n:nat) (xs:vars) : Prop :=
     var_distinct xs
  /\ length xs = n
  /\ xs <> nil.

charguer's avatar
charguer committed
1098
(** Computable version of the above definition
charguer's avatar
charguer committed
1099
    LATER use TLC exec *)
charguer's avatar
charguer committed
1100

charguer's avatar
charguer committed
1101
Definition var_funs_exec (n:nat) (xs:vars) : bool :=
charguer's avatar
charguer committed
1102
     nat_compare n (List.length xs)
charguer's avatar
charguer committed
1103
  && is_not_nil xs
charguer's avatar
charguer committed
1104 1105 1106 1107 1108 1109 1110 1111 1112 1113 1114 1115 1116 1117 1118 1119 1120
  && var_distinct xs.

Lemma var_funs_exec_eq : forall n xs,
  var_funs_exec n xs = isTrue (var_funs n xs).
Proof using.
  intros. unfold var_funs_exec, var_funs.
  rewrite nat_compare_eq.
  rewrite is_not_nil_eq.
  rewrite List_length_eq.
  extens. rew_istrue. iff*.
Qed.

Definition var_fixs (f:var) (n:nat) (xs:vars) : Prop :=
     var_distinct (f::xs)
  /\ length xs = n
  /\ xs <> nil.

charguer's avatar
charguer committed
1121
Definition var_fixs_exec (f:var) (n:nat) (xs:vars) : bool :=
charguer's avatar
charguer committed
1122
     nat_compare n (List.length xs)
charguer's avatar
charguer committed
1123
  && is_not_nil xs
charguer's avatar
charguer committed
1124 1125 1126 1127 1128 1129 1130 1131 1132 1133 1134 1135 1136
  && var_distinct (f::xs).

Lemma var_fixs_exec_eq : forall f n xs,
  var_fixs_exec f n xs = isTrue (var_fixs f n xs).
Proof using.
  intros. unfold var_fixs_exec, var_fixs.
  rewrite nat_compare_eq.
  rewrite is_not_nil_eq.
  rewrite List_length_eq.
  extens. rew_istrue. iff*.
Qed.


charguer's avatar
charguer committed
1137 1138 1139
(* ---------------------------------------------------------------------- *)
(** Properties of n-ary functions *)

charguer's avatar
charguer committed
1140 1141 1142 1143
Lemma red_funs : forall m xs t,
  xs <> nil ->
  red m (trm_funs xs t) m (val_funs xs t).
Proof using.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
1144
  introv N. destruct xs as [|x xs']. { false. }
charguer's avatar
charguer committed
1145
  simpl. applys red_fun.
charguer's avatar
charguer committed
1146
Qed.
charguer's avatar
charguer committed
1147

charguer's avatar
charguer committed
1148 1149 1150 1151 1152 1153 1154
Lemma subst_trm_funs : forall y w xs t,
  var_fresh y xs ->
  subst y w (trm_funs xs t) = trm_funs xs (subst y w t).
Proof using.
  introv N. induction xs as [|x xs']; simpls; fequals.
  { case_if. rewrite~ IHxs'. }
Qed.
charguer's avatar
charguer committed
1155

charguer's avatar
charguer committed
1156 1157 1158 1159 1160 1161 1162 1163 1164 1165 1166 1167 1168 1169 1170 1171 1172 1173 1174
Lemma red_app_arg_l : forall m1 tf (v:val) x t m2 r, 
  red m1 tf m1 (val_fun x t) ->
  red m1 ((val_fun x t) v) m2 r ->
  red m1 (tf v) m2 r.
Proof using.
  introv M1 M2. tests C: (trm_is_val tf).
  { destruct tf; tryfalse. inverts M1. applys M2. }
  { applys* red_app_arg M1. applys red_val. } 
Qed.

(* todo move *)

Definition names := list name.

Coercion names_to_vars (xs:names) := 
  List.map var_name xs.

Hint Resolve var_neq_of_var_eq.

charguer's avatar
charguer committed
1175 1176
Lemma red_app_funs_val_ind : forall xs vs m1 m2 tf t r,
  red m1 tf m1 (val_funs xs t) ->
charguer's avatar
charguer committed
1177
  red m1 (substn xs vs t) m2 r ->
charguer's avatar
charguer committed
1178
  var_funs (length vs) xs ->
charguer's avatar
charguer committed
1179
  LibList.Forall (<> var_special "_") xs -> (* todo: executable version *)
charguer's avatar
charguer committed
1180 1181 1182
  red m1 (trm_apps tf vs) m2 r.
Proof using.
  hint red_val.
charguer's avatar
charguer committed
1183 1184
  intros xs. induction xs as [|x xs']; introv R M (N&L&P) S.
  { false*. } clear P.
charguer's avatar
charguer committed
1185 1186
  { destruct vs as [|v vs']; rew_list in *. { false; math. }
    simpls. tests C: (xs' = nil).
charguer's avatar
charguer committed
1187
    { rew_list in *. inverts S as S1 _. asserts: (vs' = nil).
charguer's avatar
charguer committed
1188
      { applys length_zero_inv. math. } subst vs'. clear L.
charguer's avatar
charguer committed
1189 1190 1191 1192
      simpls. applys~ red_app_arg_l R. applys~ red_app_fun. }
    { rew_istrue in N. inverts S as S1 SN.
      destruct N as [F N']. applys~ IHxs' M.
      applys~ red_app_arg_l R. applys~ red_app_fun.
charguer's avatar
charguer committed
1193
      rewrite~ subst_trm_funs. applys~ red_funs. splits~. } }
charguer's avatar
charguer committed
1194
Qed.
charguer's avatar
charguer committed
1195

charguer's avatar
charguer committed
1196
Lemma red_app_funs_val : forall xs vs m1 m2 vf t r,
charguer's avatar
charguer committed
1197
  vf = val_funs xs t ->
charguer's avatar
charguer committed
1198
  red m1 (substn xs vs t) m2 r ->
charguer's avatar
charguer committed
1199
  var_funs (length vs) xs ->
charguer's avatar
charguer committed
1200
  LibList.Forall (<> var_special "_") xs -> (* todo: executable version *)
charguer's avatar
charguer committed
1201 1202
  red m1 (trm_apps vf vs) m2 r.
Proof using.
charguer's avatar
charguer committed
1203
  introv R M N S. applys* red_app_funs_val_ind.
charguer's avatar
charguer committed
1204
  { subst. apply~ red_val. }
charguer's avatar
charguer committed
1205 1206 1207
Qed.


charguer's avatar
charguer committed
1208
(* ---------------------------------------------------------------------- *)
charguer's avatar
charguer committed
1209
(** Properties of n-ary recursive functions *)
charguer's avatar
charguer committed
1210 1211 1212 1213

Lemma red_fixs : forall m f xs t,
  xs <> nil ->
  red m (trm_fixs f xs t) m (val_fixs f xs t).
charguer's avatar
charguer committed
1214
Proof using.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
1215
  introv N. destruct xs as [|x xs']. { false. }
charguer's avatar
charguer committed
1216 1217
  simpl. applys red_fix.
Qed.
charguer's avatar
charguer committed
1218

charguer's avatar
charguer committed
1219 1220 1221
Lemma subst_trm_fixs : forall y w f xs t,
  var_fresh y (f::xs) ->
  subst y w (trm_fixs f xs t) = trm_fixs f xs (subst y w t).
charguer's avatar
charguer committed
1222
Proof using.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
1223
  introv N. unfold trm_fixs. destruct xs as [|x xs'].
charguer's avatar
charguer committed
1224
  { auto. }
charguer's avatar
charguer committed
1225
  { simpls. do 2 case_if in N. rewrite~ subst_trm_funs. }
charguer's avatar
charguer committed
1226 1227
Qed.

charguer's avatar
charguer committed
1228 1229
Lemma red_app_fixs_val : forall xs vs m1 m2 vf f t r,
  vf = val_fixs f xs t ->
charguer's avatar
charguer committed
1230
  red m1 (subst f vf (substn xs vs t)) m2 r ->
charguer's avatar
charguer committed
1231
  var_fixs f (length vs) xs ->
charguer's avatar
charguer committed
1232
  LibList.Forall (fun x => x <> f /\ x <> var_special "_") xs -> (* todo: executable version *)
charguer's avatar
charguer committed
1233 1234
  red m1 (trm_apps vf vs) m2 r.
Proof using.
charguer's avatar
charguer committed
1235
  introv E M (N&L&P) S. destruct xs as [|x xs']. { false. }
charguer's avatar
charguer committed
1236
  { destruct vs as [|v vs']; rew_list in *. { false; math. } clear P.
charguer's avatar
charguer committed
1237
    simpls. case_if*. rew_istrue in *. destruct N as (N1&N2&N3).
charguer's avatar
charguer committed
1238
    tests C':(xs' = nil).
charguer's avatar
charguer committed
1239 1240
    { rew_list in *. asserts: (vs' = nil).
      { applys length_zero_inv. math. } subst vs'. clear L.
charguer's avatar
charguer committed
1241
      simpls. applys* red_app_fix. }
charguer's avatar
charguer committed
1242
    { inverts S as (S1&S1') SN. applys~ red_app_funs_val_ind.
charguer's avatar
charguer committed
1243 1244 1245
      { applys* red_app_fix. do 2 rewrite~ subst_trm_funs. applys~ red_funs. }
      { rewrite~ subst_substn in M. { rewrite~ substn_cons in M.
        rewrite~ subst_subst_neq. } { simpl. case_if~. } }
charguer's avatar
charguer committed
1246 1247
      { splits*. } 
      { applys Forall_pred_incl SN. hnfs*. } } } 
charguer's avatar
charguer committed
1248 1249
Qed.

charguer's avatar
charguer committed
1250

charguer's avatar
charguer committed
1251
(* ---------------------------------------------------------------------- *)
charguer's avatar
charguer committed
1252
(** Folding of n-ary functions *)
charguer's avatar
charguer committed
1253

charguer's avatar
charguer committed
1254 1255
Lemma trm_apps_fold_start : forall t1 t2,
  trm_app t1 t2 = trm_apps t1 (t2::nil).
charguer's avatar
charguer committed
1256 1257
Proof using. auto. Qed.

charguer's avatar
charguer committed
1258 1259
Lemma trm_apps_fold_next : forall t1 t2 t3s,
  trm_apps (trm_app t1 t2) t3s = trm_apps t1 (t2::t3s).
charguer's avatar
charguer committed
1260 1261
Proof using. auto. Qed.

charguer's avatar
charguer committed
1262 1263 1264 1265 1266 1267
Lemma trm_apps_fold_concat : forall t1 t2s t3s,
  trm_apps (trm_apps t1 t2s) t3s = trm_apps t1 (List.app t2s t3s).
Proof using.
  intros. gen t1; induction t2s; intros. { auto. }
  { rewrite <- trm_apps_fold_next. simpl. congruence. }
Qed.
charguer's avatar
charguer committed
1268

charguer's avatar
charguer committed
1269
Lemma trm_funs_fold_start : forall x t,
charguer's avatar
charguer committed
1270 1271 1272
  trm_fun x t = trm_funs (x::nil) t.
Proof using. auto. Qed.

charguer's avatar
charguer committed
1273
Lemma trm_funs_fold_next : forall x xs t,
charguer's avatar
charguer committed
1274
  trm_funs (x::nil) (trm_funs xs t) = trm_funs (x::xs) t.
charguer's avatar
charguer committed
1275 1276
Proof using. auto. Qed.

charguer's avatar
charguer committed
1277 1278
Lemma trm_fixs_fold_start : forall f x t,
  trm_fix f x t = trm_fixs f (x::nil) t.
charguer's avatar
charguer committed
1279 1280
Proof using. auto. Qed.

charguer's avatar
charguer committed
1281
(* subsumed by iteration of trm_funs_fold_next *)
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
1282
Lemma trm_funs_fold_app : forall xs ys t,
charguer's avatar
charguer committed
1283
  trm_funs xs (trm_funs ys t) = trm_funs (List.app xs ys) t.
charguer's avatar