Commit 747f405e authored by Simon Spies's avatar Simon Spies
Browse files

existential invariants

parent f76f223b
......@@ -46,6 +46,7 @@ theories/systemf/church_encodings.v
theories/systemf/parallel_subst.v
theories/systemf/logrel.v
theories/systemf/free_theorems.v
theories/systemf/binary_logrel.v
theories/systemf/existential_invariants.v
......
From stdpp Require Import gmap base relations.
From iris Require Import prelude.
From semantics.lib Require Export debruijn.
From semantics.systemf Require Import lang notation parallel_subst types bigstep tactics logrel.
From semantics.systemf Require Import lang notation parallel_subst types bigstep tactics.
From semantics.systemf Require logrel binary_logrel.
From Equations Require Import Equations.
(** * Existential types and invariants *)
......@@ -44,7 +45,7 @@ Notation "e1 '&&' e2" := (And e1 e2) : expr_scope.
(* ∃ α, { bit : α, flip : α → α, get : α → bool } *)
Definition BIT : type := ∃: (#0 × (#0 #0)) × (#0 Bool).
Definition MyBit : expr :=
Definition MyBit : val :=
pack (#0, (* bit *)
λ: "x", #1 - "x", (* flip *)
λ: "x", #0 < "x"). (* get *)
......@@ -58,33 +59,82 @@ Definition MyBit_instrumented : val :=
λ: "x", assert (("x" = #0) || ("x" = #1));; #1 - "x", (* flip *)
λ: "x", assert (("x" = #0) || ("x" = #1));; #0 < "x"). (* get *)
Lemma MyBit_instrumented_sem_typed δ :
𝒱 BIT δ MyBit_instrumented.
Definition MyBoolBit : val :=
pack (#false, (* bit *)
λ: "x", UnOp NegOp "x", (* flip *)
λ: "x", "x"). (* get *)
Lemma MyBoolBit_typed n Γ :
TY n; Γ MyBoolBit : BIT.
Proof.
unfold BIT. simp type_interp.
eexists. split; first done.
pose_sem_type (λ x, x = #0 x = #1) as τ.
{ intros v [-> | ->]; done. }
exists τ.
simp type_interp.
eexists _, _. split; first done.
split.
- simp type_interp. eexists _, _. split; first done. split.
+ simp type_interp. simpl. by left.
+ simp type_interp. eexists _, _. split; first done. split; first done.
intros v'. simp type_interp; simpl.
(* Note: this part of the proof is a bit different from the paper version, as we directly do a case split. *)
intros [-> | ->].
* exists #1. split; last simp type_interp; simpl; eauto.
bs_steps_det. eapply bs_if_true; bs_steps_det.
eapply bs_if_true; bs_steps_det.
* exists #0. split; last simp type_interp; simpl; eauto.
bs_steps_det. eapply bs_if_true; bs_steps_det.
eapply bs_if_false; bs_steps_det.
- simp type_interp. eexists _, _. split; first done. split; first done.
intros v'. simp type_interp; simpl. intros [-> | ->].
* exists #false. split; last simp type_interp; simpl; eauto.
bs_steps_det. eapply bs_if_true; bs_steps_det. eapply bs_if_true; bs_steps_det.
* exists #true. split; last simp type_interp; simpl; eauto.
bs_steps_det. eapply bs_if_true; bs_steps_det. eapply bs_if_false; bs_steps_det.
eapply (typed_pack _ _ _ Bool); solve_typing.
simpl. econstructor.
Qed.
Section unary_mybit.
Import logrel.
Lemma MyBit_instrumented_sem_typed δ :
𝒱 BIT δ MyBit_instrumented.
Proof.
unfold BIT. simp type_interp.
eexists. split; first done.
pose_sem_type (λ x, x = #0 x = #1) as τ.
{ intros v [-> | ->]; done. }
exists τ.
simp type_interp.
eexists _, _. split; first done.
split.
- simp type_interp. eexists _, _. split; first done. split.
+ simp type_interp. simpl. by left.
+ simp type_interp. eexists _, _. split; first done. split; first done.
intros v'. simp type_interp; simpl.
(* Note: this part of the proof is a bit different from the paper version, as we directly do a case split. *)
intros [-> | ->].
* exists #1. split; last simp type_interp; simpl; eauto.
bs_steps_det. eapply bs_if_true; bs_steps_det.
eapply bs_if_true; bs_steps_det.
* exists #0. split; last simp type_interp; simpl; eauto.
bs_steps_det. eapply bs_if_true; bs_steps_det.
eapply bs_if_false; bs_steps_det.
- simp type_interp. eexists _, _. split; first done. split; first done.
intros v'. simp type_interp; simpl. intros [-> | ->].
* exists #false. split; last simp type_interp; simpl; eauto.
bs_steps_det. eapply bs_if_true; bs_steps_det. eapply bs_if_true; bs_steps_det.
* exists #true. split; last simp type_interp; simpl; eauto.
bs_steps_det. eapply bs_if_true; bs_steps_det. eapply bs_if_false; bs_steps_det.
Qed.
End unary_mybit.
Section binary_mybit.
Import binary_logrel.
Lemma MyBit_MyBoolBit_sem_typed δ :
𝒱 BIT δ MyBit MyBoolBit.
Proof.
unfold BIT. simp type_interp.
eexists _, _. split_and!; try done.
pose_sem_type (λ v w, (v = #0 w = #false) (v = #1 w = #true)) as τ.
{ intros v w [[-> ->] | [-> ->]]; done. }
exists τ.
simp type_interp.
eexists _, _, _, _. split_and!; try done.
simp type_interp.
eexists _, _, _, _. split_and!; try done.
- simp type_interp. simpl. naive_solver.
- simp type_interp. eexists _, _, _, _. split_and!; try done.
intros v w. simp type_interp. simpl.
intros [[-> ->]|[-> ->]]; simpl; eexists _, _; split_and!; eauto; simpl.
all: simp type_interp; simpl; naive_solver.
- simp type_interp. eexists _, _, _, _. split_and!; try done.
intros v w. simp type_interp. simpl.
intros [[-> ->]|[-> ->]]; simpl.
all: eexists _, _; split_and!; eauto; simpl.
all: simp type_interp; eauto.
Qed.
End binary_mybit.
\ No newline at end of file
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