proposition: Theorem SharpenedGuard : FullySharpened GuardSpec.
proof: Proof. start sharpening ADT. match goal with |- context [@BuildADT (QueryStructure ?Rep) _ _ _ _ _ _] => hone representation using (@DropQSConstraints_AbsR Rep) end. - apply Constructor_DropQSConstraints. - etransitivity; [ eapply refine_If_Opt_Then_Else_Bind | ]. etransitivity; [ eapply refine_If_Opt_Then_Else | ]; swap 1 3. + higher_order_reflexivity. + simplify with monad laws. refine pick val _; [ | reflexivity ]. simplify with monad laws; simpl. match goal with | [ H: DropQSConstraints_AbsR _ _ |- _ ] => red in H; rewrite !H end; higher_order_reflexivity. + intro. etransitivity; [ eapply refine_If_Opt_Then_Else_Bind | ]. etransitivity; [ eapply refine_If_Opt_Then_Else | ]; swap 1 3. * higher_order_reflexivity. * simplify with monad laws. refine pick val _; [ | reflexivity ]. simplify with monad laws; simpl. match goal with | [ H: DropQSConstraints_AbsR _ _ |- _ ] => red in H; rewrite !H end; higher_order_reflexivity. * intro. simplify with monad laws. etransitivity. -- setoid_rewrite DropQSConstraintsQuery_In. try simplify with monad laws; cbv beta; simpl; repeat match goal with H : DropQSConstraints_AbsR _ _ |- _ => unfold DropQSConstraints_AbsR in H; rewrite H end. finish honing. -- etransitivity; [ eapply refine_bind | ]; cycle -1. ++ higher_order_reflexivity. ++ higher_order_reflexivity. ++ intro. etransitivity; [ eapply refine_If_Then_Else_Bind | ]. etransitivity; [ eapply refine_If_Then_Else | ]; swap 1 3. ** higher_order_reflexivity. ** etransitivity; [ eapply refine_If_Then_Else_Bind | ]. etransitivity; [ eapply refine_If_Then_Else | ]; swap 1 3. --- higher_order_reflexivity. --- simplify with monad laws. refine pick val _; [ | reflexivity ]. simplify with monad laws; simpl. match goal with | [ H: DropQSConstraints_AbsR _ _ |- _ ] => red in H; rewrite !H end; higher_order_reflexivity. --- etransitivity; [ eapply refine_If_Then_Else_Bind | ]. etransitivity; [ eapply refine_If_Then_Else | ]; swap 1 3. +++ higher_order_reflexivity. +++ simplify with monad laws. refine pick val _; [ | reflexivity ]. simplify with monad laws; simpl. match goal with | [ H: DropQSConstraints_AbsR _ _ |- _ ] => red in H; rewrite !H end; higher_order_reflexivity. +++ unfold Bind2; simplify with monad laws. simpl. Lemma refine_bind_bind_dep X X' Y Z (f : X -> Comp Y) (g : Y -> Comp Z) (k: X -> X') x : refine (Bind x (fun x0 => Bind (f x0) (fun u => g u))) (Bind (Bind x (fun x0 => Bind (f x0) (fun u => ret (u, (k x0))))) (fun x0u => g (fst x0u))). Proof. red; intros. computes_to_inv; subst. eauto using @BindComputes. Qed.
imports: Fiat.QueryStructure.Automation.MasterPlan Fiat.Narcissus.Examples.NetworkStack.IPv4Header Fiat.Narcissus.Examples.NetworkStack.TCP_Packet Fiat.Narcissus.Formats.ByteBuffer Bedrock.Word Fiat.Narcissus.BinLib.Core