Commit 37f38437 authored by charguer's avatar charguer
Browse files

tour_functional_queue

parent b4f27557
......@@ -42,11 +42,12 @@ Proof.
(* Detailed proof *)
{ xmatch.
{ xret. xsimpl. rewrite I1. rewrite I2. auto. auto. }
{ xret. xsimpl. rewrite I1. applys app_not_empty_l. intros E. false* C. } }
{ xret. xsimpl. rewrite I1. applys app_not_empty_l.
intros E. subst. false* C. } }
(* Shorter proof *)
{ xmatch; xrets.
{ rewrite* I2 in I1. }
{ intros E. subst L. applys* app_not_empty_l. } }
{ subst L. applys* app_not_empty_l. intros ->. false* C . } }
Qed.
Hint Extern 1 (RegisterSpec is_empty) => Provide is_empty_spec.
......
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