Commit 3895a2ef by Lennard Gäher

### Merge branch 'main' of gitlab.mpi-sws.org:FP/semantics-course

parents 2d8e3248 747f405e
 ... ... @@ -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 ... ...
This diff is collapsed.
 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!