Skip to content

GitLab

Commit bc7e855e authored by Joachim Bard's avatar Joachim Bard
Browse files
Options

remove unnecassary admits

parent 58137a95
Hide whitespace changes
Inline Side-by-side
Showing with 5 additions and 5 deletions
coq/ssaPrgs.v
View file @ bc7e855e
......@@ -581,7 +581,7 @@ Fixpoint expr_subst (e:expr Q) x e_new :=
(* simpl in *. *)
(* rewrite <- expr_subst_correct in H0; eauto. *)
(* econstructor; eauto. *)
(* Admitted. *)
(* Abort. *)
(* Fixpoint let_subst (f:cmd Q) := *)
(* match f with *)
......@@ -627,7 +627,7 @@ Fixpoint expr_subst (e:expr Q) x e_new :=
(* destruct x_live as [x_used | x_live]. *)
(* + exists E. eapply eval_subst_subexpr; eauto. *)
(* + eapply IHf; eauto. *)
(* Admitted. *)
(* Abort. *)
(* - simpl in *. *)
(* inversion eval_f; subst. *)
(* exists E. eapply eval_subst_subexpr; eauto. *)
......@@ -677,7 +677,7 @@ Fixpoint expr_subst (e:expr Q) x e_new :=
(* destruct x_live as [x_used | x_live]. *)
(* + eapply eval_subst_subexpr; eauto. *)
(* + edestruct IHg as [v0 eval_v0]; eauto. *)
(* Admitted. *)
(* Abort. *)
(* Theorem let_free_agree f E vR inVars outVars e defVars: *)
(* ssa f inVars outVars -> *)
......@@ -695,7 +695,7 @@ Fixpoint expr_subst (e:expr Q) x e_new :=
(* (* Let Case, prove that the value of the let binding must be used somewhere *) *)
(* - case_eq (let_subst s). *)
(* + intros e0 subst_s; rewrite subst_s in *. *)
(* Admitted. *)
(* Abort. *)
(* (*inversion subst_step; subst. *)
(* clear subst_s subst_step. *)
(* inversion bstep_e; subst. *)
......@@ -726,7 +726,7 @@ Fixpoint expr_subst (e:expr Q) x e_new :=
(* - simpl. *)
(* inversion bstep_f; subst. *)
(* inversion ssa_f; subst. *)
(* Admitted. *)
(* Abort. *)
(* (* case_eq (let_subst f). *)
(* + intros f_subst subst_f_eq. *)
(* specialize (IHf (updEnv n REAL v E) vR (NatSet.add n inVars) outVars f_subst H9 H7 subst_f_eq). *)
......
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