Commit 0169d014 authored by charguer's avatar charguer

specialvars

parent b915f56d
......@@ -4195,4 +4195,70 @@ Ltac xwhile_core xwhile_tactic ::=
*)
*)
\ No newline at end of file
*)
(** Encoding of sequences *)
Definition trm_seq (t1:trm) (t2:trm) : trm :=
trm_tag tag_seq (trm_let "$_" t1 (trm_unbind "$_" t2)).
(** Encoding of while loops *)
Definition trm_while (t1:trm) (t2:trm) : trm :=
let F : var := "$f" in
let U : var := "$_" in
let P t := trm_unbind F (trm_unbind U t) in
let X : val := val_fix F U (trm_if (P t1) (trm_seq (P t2) (F val_unit)) val_unit) in
trm_tag tag_while (X val_unit).
(*
Lemma red_app_fun : forall m1 m2 v1 v2 x t r,
var_special x = false ->
v1 = val_fun x t ->
red m1 (subst x v2 t) m2 r ->
red m1 (trm_app v1 v2) m2 r.
Proof using. intros. applys* red_app_fun_precise. Qed.
*)
(* todo: deprecated
Lemma red_seq_unit : forall m1 m2 m3 t1 t2 r,
red m1 t1 m2 val_unit ->
red m2 t2 m3 r ->
red m1 (trm_seq t1 t2) m3 r.
Proof using.
introv M1 M2. applys* red_let.
simpl. applys* red_unbind.
Qed.
*)
(* todo: deprecated
Lemma red_seq' : forall m1 m2 t1 t2 r,
let x : var := "$_" 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. inverts M as. intros m3 r1 M1 M2.
inverts M2 as. intros M3. applys* red_seq.
Qed.
*)
(* todo: deprecated
Lemma red_while' : forall t1 t2 m1 m2 r,
let F : var := "$f" in
let U : var := "$_" in
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.
Proof using.
introv M1. applys red_while. ...
Qed.
*)
This diff is collapsed.
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment