Commit f67b5116 authored by charguer's avatar charguer

record_metaprog

parent 0062010f
......@@ -495,12 +495,12 @@ Qed.
Definition val_new_record (n:nat) :=
let fs := nat_seq 0%nat n in
let xs := var_seq 0%nat n in
let P : var := nat_to_var n in
let P : var := nat_to_var n in
val_funs xs (
Let P := val_alloc n in
LibList.fold_right (fun f t => val_set_field (f:field) P (nat_to_var f);; t) (trm_var P) fs).
Lemma Subst_new_record_aux : forall fs xs Vs (i n n':nat) (p:loc),
Lemma Subst_new_record_aux : forall (n':nat) fs xs Vs (i n:nat) (p:loc),
n' = length Vs ->
fs = nat_seq i n' ->
xs = var_seq i n' ->
......@@ -509,45 +509,49 @@ Lemma Subst_new_record_aux : forall fs xs Vs (i n n':nat) (p:loc),
(Subst N (Dyn p) (Substs xs Vs (fold_right (fun f t => trm_seq (val_set_field (f:field) (trm_var N) (nat_to_var f)) t) (trm_var N) fs)))
= fold_right (fun fV t => let '(f,V) := fV in trm_seq (val_set_field (f:field) p (enc V)) t) p (LibList.combine fs Vs).
Proof using.
(*
intros xs. induction xs as [|x xs']; introv LVs Exs Ein.
{ simpl combine. rew_list. unfold Subst. simpl. case_if~. }
{ forwards Lin: length_var_seq i n'.
rewrite <- Exs in Lin. rew_list in Lin.
destruct Vs as [|V Vs']. { false. rew_list in LVs. math. }
rew_list in LVs. asserts EL: (length xs' = length Vs'). { math. }
destruct n' as [|n'']. { inverts Exs. } simpl in Exs.
invert Exs. intros Ei Exs'. subst i. rewrite <- Exs'.
asserts N: (x <> n). { math. }
rewrite Substs_cons. rewrite combine_cons. rew_listx.
rewrite Subst_seq.
asserts_rewrite (Subst x V (val_set_field x (trm_var n) (trm_var x))
= val_set_field x (trm_var n) (enc V)).
{ unfold Subst. simpl. case_if. case_if~. }
intros n'. induction n' as [|n'']; introv LVs Efs Exs Ein; intros N.
{ destruct xs; [|rew_list in *; false; math].
destruct fs; [|rew_list in *; false; math].
destruct Vs; [|rew_list in *; false; math].
rew_listx. unfold Subst. simpl. case_if~. }
{ hide IHn''. destruct xs as [|x xs']; [rew_list in *; false; math|].
destruct fs as [|f fs']; [rew_list in *; false; math|].
destruct Vs as [|V Vs']; [rew_list in *; false; math|].
invert Efs. intros Ef Efs'. subst i. invert Exs. intros Ex Exs'.
rew_list in *.
asserts EL: (length xs' = length Vs').
{ subst. rewrite length_var_seq. math. }
asserts Nxn: (x <> N).
{ intros E. subst x. lets: injective_nat_to_var E. math. }
rewrite <- Ex. rewrite <-Exs'. rew_listx.
rewrite Substs_cons. rewrite Subst_seq. rewrite <- Ex.
asserts_rewrite (Subst x V (val_set_field f N (trm_var x))
= val_set_field f N (enc V)).
{ unfold Subst. simpl. case_if. case_if~. }
rewrite~ Substs_seq.
asserts_rewrite (Substs xs' Vs' (val_set_field x (trm_var n) `V)
= (val_set_field x (trm_var n) `V)).
asserts_rewrite (Substs xs' Vs' (val_set_field f N `V)
= (val_set_field f N `V)).
{ do 2 rewrite~ Substs_app. do 2 rewrite~ Substs_val. rewrite~ Substs_var_neq.
{ rewrite Exs'. applys var_fresh_var_seq_ge. math. } }
rewrite~ Subst_seq.
asserts_rewrite (Subst n (Dyn p) (val_set_field x (trm_var n) `V) = val_set_field x p `V).
asserts_rewrite (Subst N (Dyn p) (val_set_field f N `V) = val_set_field f p `V).
{ unfold Subst; simpl. case_if~. } (* todo: lemma Subst_var *)
fequals.
match goal with |- context [Subst x V ?t'] => set (t:=t') end.
asserts_rewrite (Subst x V t = t).
{ subst xs'. cuts K: (forall n' i,
(x < i)%nat ->
let t := @fold_right nat trm (fun f t => trm_seq (val_set_field f (trm_var n) (trm_var f)) t) (trm_var n) (var_seq i n') in
Subst x V t = t).
{ subst x. cuts K: (forall n' i,
(f < i)%nat ->
let t := @fold_right nat trm (fun f' t =>
trm_seq (val_set_field f' N (nat_to_var f')) t) N (nat_seq i n') in
Subst (nat_to_var f) V t = t).
{ applys K. math. }
intros n'. gen N. clears_all. induction n'; introv L; intros; subst t.
intros n'. gen Nxn. clears_all. induction n'; introv L; intros; subst t.
{ simpl. unfold Subst. simpl. case_if~. } (*todo: Subst_var_neq.*)
{ simpl. rewrite Subst_seq. fequals.
{ unfold Subst. simpl. case_if. case_if. { false; math. } { auto. } }
{ unfold Subst. simpl. case_if as C. case_if as C'.
{ lets: injective_nat_to_var C'. false; math. } { auto. } }
{ rewrite~ IHn'. } } }
applys IHxs' Exs'; math. }
*)
admit.
applys~ IHn'' Exs'; try math. }
Qed.
Lemma Rule_new_record : forall (n:nat) (Vs:dyns),
......@@ -578,7 +582,7 @@ Proof using.
[ xlocal | | hsimpl; intros; subst~]. (* todo: weaken_post with swapped order *)
gen n Vs Ws. set (start := O). intros n. gen start.
induction n as [|n']; intros.
{ destruct xs; [|rew_list in *; false; math].
{ destruct xs; [|rew_list in *; false; math]. (* todo: lemma/tactic for this *)
destruct Vs; [|rew_list in *; false; math].
destruct Ws; [|rew_list in *; false; math].
rew_list in *. subst. simpls.
......
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