From abdc8e5056dfedf403ce0e28adc13228d4c4f9a0 Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Sat, 27 Nov 2021 14:17:09 -0800 Subject: [PATCH] Cleanup DawnEval.v --- code/dawn/DawnEval.v | 148 +++++++++++++++---------------------------- 1 file changed, 51 insertions(+), 97 deletions(-) diff --git a/code/dawn/DawnEval.v b/code/dawn/DawnEval.v index 69f16e1..b9fa7ef 100644 --- a/code/dawn/DawnEval.v +++ b/code/dawn/DawnEval.v @@ -1,6 +1,7 @@ Require Import Coq.Lists.List. Require Import Dawn. Require Import Coq.Program.Equality. +From Ltac2 Require Import Ltac2. Inductive step_result := | err @@ -79,7 +80,7 @@ Lemma eval_chain_split : forall (e1 e2 : expr) (s s'' : list expr), eval_chain s (e_comp e1 e2) s'' -> exists s', (eval_chain s e1 s') /\ (eval_chain s' e2 s''). Proof. intros e1 e2 s ss'' ch. - dependent induction ch. + ltac1:(dependent induction ch). - simpl in P. destruct (eval_step s e1); inversion P. - simpl in P. destruct (eval_step s e1) eqn:Hval; try (inversion P). + injection P as Hinj; subst. specialize (IHch e e2 H0) as [s'0 [ch1 ch2]]. @@ -91,47 +92,6 @@ Proof. * apply ch. Qed. -Theorem eval_step_preservation : forall (e : expr) (vs : value_stack) (s' : list expr), - ((exists e', eval_step (strip_value_list vs) e = middle e' s') -> - exists vs', (strip_value_list vs') = s') /\ - ((eval_step (strip_value_list vs) e = final s') -> - exists vs', (strip_value_list vs') = s'). -Proof. - intros e vs. induction e; split. - - intros [e' Hst]. - destruct i; try (destruct vs as [|v1 [|v2 vs]]; inversion Hst; fail). - * destruct vs as [|v1 [|v2 vs]]; inversion Hst; - destruct (projT1 v1); inversion H0. - destruct (projT1 v2); inversion H1. - * destruct vs as [|v1 vs]; inversion Hst. - destruct (projT1 v1); inversion H0. - eauto. - - intros Hst. - destruct i; try (destruct vs as [|v1 [|v2 vs]]; inversion Hst; fail). - * destruct vs as [|v1 [|v2 vs]]; inversion Hst. exists (v2 :: v1 :: vs). reflexivity. - * destruct vs as [|v1 vs]; inversion Hst. exists (v1 :: v1 :: vs). reflexivity. - * destruct vs as [|v1 vs]; inversion Hst. exists vs. reflexivity. - * destruct vs as [|v1 vs]; inversion Hst. exists (v_quote (projT1 v1) :: vs). reflexivity. - * destruct vs as [|v1 [|v2 vs]]; inversion Hst. - + destruct (projT1 v1); inversion H0. - + destruct (projT1 v1); destruct (projT1 v2); inversion H0. - exists (v_quote (e_comp e0 e) :: vs). reflexivity. - * destruct vs as [|v1 vs]; inversion Hst; - destruct (projT1 v1); inversion H0. - - intros [e' Hst]. inversion Hst. - - intros Hst. inversion Hst. exists (v_quote e :: vs). reflexivity. - - intros [e' Hst]. inversion Hst. - destruct (eval_step (strip_value_list vs) e1) eqn:Hst1. - * inversion H0. - * specialize (IHe1 s') as [IHe1 _]. apply IHe1. exists e. - injection H0 as Hinj; subst; auto. - * specialize (IHe1 s') as [_ IHe1]. apply IHe1. - injection H0 as Hinj; subst; auto. - - intros Hst. - inversion Hst. destruct (eval_step (strip_value_list vs) e1); inversion H0. -Qed. - - Theorem val_step_sem : forall (e : expr) (vs vs' : value_stack), Sem_expr vs e vs' -> eval_chain (strip_value_list vs) e (strip_value_list vs') with eval_step_int : forall (i : intrinsic) (vs vs' : value_stack), @@ -158,67 +118,61 @@ Proof. Qed. Theorem eval_step_sem_back : forall (e : expr) (vs vs' : value_stack), - eval_chain (strip_value_list vs) e (strip_value_list vs') -> Sem_expr vs e vs' -with eval_step_int_back : forall (i : intrinsic) (vs vs' : value_stack), - eval_chain (strip_value_list vs) (e_int i) (strip_value_list vs') -> Sem_int vs i vs'. + eval_chain (strip_value_list vs) e (strip_value_list vs') -> Sem_expr vs e vs'. Proof. - (* Thoughts: prove a "step value stack preservation" property. A step suggested by - eval_step will ensure the stack contains values if it contained values initially. - - Done! eval_step_preservation. - - From there, by induction, a chain preserves value stacks. *) + (* Thoughts: the issue is with the apparent nondeterminism of evalution. *) Admitted. +Ltac2 Type exn ::= [ | Not_intrinsic ]. -Theorem eval_step_sem_not : forall (e : expr) (vs : value_stack), - ~ (exists vs', Sem_expr vs e vs') -> ~(exists vs', eval_chain (strip_value_list vs) e (strip_value_list vs')) -with eval_step_int_not : forall (i : intrinsic) (vs : value_stack), - ~ (exists vs', Sem_int vs i vs') -> ~(exists vs', eval_chain (strip_value_list vs) (e_int i) (strip_value_list vs')). +Ltac2 rec destruct_n (n : int) (vs : constr) : unit := + if Int.le n 0 then () else + let v := Fresh.in_goal @v in + let vs' := Fresh.in_goal @vs in + destruct $vs as [|$v $vs']; Control.enter (fun () => + try (destruct_n (Int.sub n 1) (Control.hyp vs')) + ). + +Ltac2 int_arity (int : constr) : int := + match! int with + | swap => 2 + | clone => 1 + | drop => 1 + | quote => 1 + | compose => 2 + | apply => 1 + | _ => Control.throw Not_intrinsic + end. + +Ltac2 destruct_int_stack (int : constr) (va: constr) := destruct_n (int_arity int) va. + +Ltac2 ensure_valid_value_stack () := Control.enter (fun () => + match! goal with + | [h : eval_step (strip_value_list ?a) (e_int ?b) = ?c |- _] => + let h := Control.hyp h in + destruct_int_stack b a; + try (inversion $h; fail) + | [|- _ ] => () + end). + +Ltac2 ensure_valid_stack () := Control.enter (fun () => + match! goal with + | [h : eval_step ?a (e_int ?b) = ?c |- _] => + let h := Control.hyp h in + destruct_int_stack b a; + try (inversion $h; fail) + | [|- _ ] => () + end). + +Theorem test : forall (s s': list expr), eval_step s (e_int swap) = final s' -> + exists v1 v2 s'', s = v1 :: v2 :: s'' /\ s' = v2 :: v1 :: s''. Proof. -(* - - intros e vs Hnsem [vs' Hev]. - destruct e. - + specialize (eval_step_sem_not _ _ Hnsem). apply eval_step_sem_not. - eexists. apply Hev. - + apply Hnsem. eexists. apply Sem_e_quote. - + inversion Hev. - * simpl in P. destruct (eval_step (strip_value_list vs) e1); inversion P. - * specialize (eval_chain_split e1 e2 (strip_value_list vs) (strip_value_list vs') Hev) as [s' [ch1 ch2]]. - assert (Hnboth : ~ (exists vsi, Sem_expr vs e1 vsi /\ Sem_expr vsi e2 vs')). - { intros [vsi [H1 H2]]. apply Hnsem. exists vs'. eapply Sem_e_comp. apply H1. apply H2. } - - assert (Hncomp : ~ (exists vsi, Sem_expr vs e1 vsi) \/ exists vsi, Sem_expr vs e1 vsi /\ ~(Sem_expr vsi e2 vs')). - { - - intros i vs Hnint [vs' Hev]. destruct i. - + destruct vs as [|v [|v' vs]]; inversion Hev; simpl in P; inversion P. - apply Hnint. eexists. apply Sem_swap. - + destruct vs as [|v vs]; inversion Hev; simpl in P; inversion P. - apply Hnint. eexists. apply Sem_clone. - + destruct vs as [|v vs]; inversion Hev; simpl in P; inversion P. - apply Hnint. eexists. apply Sem_drop. - + destruct vs as [|v vs]; inversion Hev; simpl in P; inversion P. - apply Hnint. eexists. apply Sem_quote. - + destruct vs as [|v [|v' vs]]; - try (destruct v; destruct x); - try (destruct v'; destruct x0); - simpl in Hev; inversion Hev; simpl in P; inversion P; subst. - destruct i; destruct i0. - apply Hnint. eexists. apply Sem_compose. - + destruct vs as [|v vs]. - * simpl in Hev; inversion Hev; simpl in P; inversion P. - * (* Monkey at keyboard mode engaged here. *) - destruct v eqn:Hv. destruct i eqn:Hi. - simpl in Hev; inversion Hev; simpl in P; inversion P. - injection P as Heq. subst. - assert (Hna : ~(exists vs', Sem_expr vs ei vs')). - { intros [vs'0 Hsem]. apply Hnint. eexists. apply Sem_apply. apply Hsem. } - specialize (eval_step_sem_not _ _ Hna). apply eval_step_sem_not. eexists. - apply rest. - *) -Admitted. + intros s s' Heq. + ensure_valid_stack (). + simpl in Heq. injection Heq as Hinj. subst. eauto. +Qed. Require Extraction. Require Import ExtrHaskellBasic. Extraction Language Haskell. -Extraction "UccGen.hs" eval_step true false or. +Extraction "UccGen.hs" expr eval_step true false or.