Merge pull request #8 from harp-project/concurrency

Code cleanup, comments

src/Basics.v

@@ -1,3 +1,12 @@
+(**
+
+  This file is a part of a formalisation of a subset of Core Erlang.
+
+  In this file, we define a number of theorems to extend Coq's
+  standard library to aid our formalisation.
+
+*)
+
 Require Export Coq.micromega.Lia
                Coq.Lists.List
                Coq.Arith.PeanoNat.
@@ -42,6 +51,8 @@ Proof.
       exists (a::x), x0. apply app_comm_cons. Unshelve. simpl. lia.
 Qed.
 
+(** Similar Forall, but this checks a property that is satisfied pairwise
+    by the elements of two lists. *)
 Inductive list_biforall {T1 T2 : Type} (P : T1 -> T2 -> Prop) : list T1 -> list T2 -> Prop :=
 | biforall_nil : list_biforall P [] []
 | biforall_cons hd hd' tl tl' : P hd hd' -> list_biforall P tl tl' -> list_biforall P (hd::tl) (hd'::tl').

src/Bisimulations.v

@@ -1,3 +1,10 @@
+(**
+  This file is a part of a formalisation of a subset of Core Erlang.
+
+  In this file, we show bisimulation-based equivalence concepts for
+  concurrent Core Erlang.
+*)
+
 Require Export ConcurrentProperties.
 Import ListNotations.
 

src/CIU.v

@@ -1,3 +1,10 @@
+(**
+  This file is a part of a formalisation of a subset of Core Erlang.
+
+  In this file, we define CIU equivalence for sequential Core Erlang.
+  We prove that CIU equivalence coicides with logical relations.
+*)
+
 Require Export Compatibility.
 
 Import ListNotations.

src/CTX.v

@@ -1,3 +1,13 @@
+(**
+  This file is a part of a formalisation of a subset of Core Erlang.
+
+  In this file, we define contextual equivalence for sequential Core Erlang.
+  We prove the contextual equivalence coincides with CIU equivalence and
+  lofical relations.
+
+  At the bottom of the file, we define a notion of behavioural equivalence too,
+  which also proved to be coincide with CIU equivalence.
+*)
 Require Export CIU.
 
 Import ListNotations.

src/Compatibility.v

@@ -1,3 +1,9 @@
+(**
+  This file is a part of a formalisation of a subset of Core Erlang.
+
+  We prove the reflexivity and compatibility of the logical relations.
+*)
+
 Require Export LogRel.
 Import ListNotations.
 

src/ConcurrentFunSemantics.v

@@ -1,4 +1,11 @@
-(* This part of the work is based on https://dl.acm.org/doi/10.1145/3123569.3123576 *)
+(**
+  This file is a part of a formalisation of a subset of Core Erlang.
+
+  In this file, we describe the frame stack semantics for concurrent
+  Core Erlang.
+
+  This part of the work is based on https://dl.acm.org/doi/10.1145/3123569.3123576
+*)
 Require Export SubstSemantics.
 Require Export Coq.Sorting.Permutation.
 Require Export Coq.Classes.EquivDec.

src/ConcurrentProperties.v

@@ -1,3 +1,8 @@
+(**
+  This file is a part of a formalisation of a subset of Core Erlang.
+
+  In this file, we prove properties about concurrent Core Erlang.
+*)
 Require Export ConcurrentFunSemantics.
 Import ListNotations.
 

src/Equivs.v

@@ -1,3 +1,8 @@
+(**
+  This file is a part of a formalisation of a subset of Core Erlang.
+
+  In this file, we show example program equivalences in sequential Core Erlang.
+*)
 Require Import CTX.
 Import ListNotations.
 
@@ -252,3 +257,105 @@ Proof.
     simpl in H0. break_match_hyp. inversion H0.
     eapply IHxs. 2: exact Heqo. rewrite map_length. auto.
 Qed.
+
+Theorem CIU_evaluates :
+  forall e1 e2 v, EXPCLOSED e1 -> EXPCLOSED e2 ->
+  ⟨[], e1⟩ -->* v -> ⟨[], e2⟩ -->* v ->
+  CIU e1 e2.
+Proof.
+  intros.
+  split. 2: split. 1-2: auto.
+  intros.
+  destruct H1 as [CL1 [k1 H1]], H2 as [CL2 [k2 H2]].
+  apply frame_indep_nil with (Fs' := F) in H2. simpl in H2.
+  apply frame_indep_nil with (Fs' := F) in H1. simpl in H1.
+  destruct H4 as [k1' H4].
+  eapply terminates_step_any_2 in H1. 2: exact H4.
+  eapply term_step_term_plus in H2. 2: exact H1.
+  now exists (k2 + (k1' - k1)).
+Qed.
+
+Theorem map_foldr_equiv :
+  forall l' l x y z e f
+  (VsCL : VALCLOSED l) (SCE : EXP 2 ⊢ e),
+  computes x e f -> cons_to_list l = Some l' ->
+  CIU (obj_map (EFun [x] e) l) (obj_foldr (EFun [y;z] (ECons (EApp (EFun [x] e) [EVar 1]) (EVar 2))) l ENil).
+Proof.
+  intros.
+  pose proof (obj_foldr_on_meta_level l' l x y z e f VsCL SCE H H0).
+  pose proof (obj_map_on_meta_level l' l x e f VsCL SCE H H0).
+  eapply CIU_evaluates; eauto.
+  {
+    unfold obj_map. do 3 constructor; auto; simpl.
+    - constructor. simpl. constructor; auto.
+      cbn. constructor; auto.
+      destruct i. 2: destruct i.
+      all: constructor. lia.
+    - do 2 constructor; auto. simpl in H3.
+      destruct i. 2: destruct i. 3: destruct i. all: constructor. all: lia.
+    - simpl in *. destruct i. 2: destruct i.
+      constructor; simpl. now apply (proj2 (scope_ext_app 3 2 ltac:(lia))).
+      now apply (proj1 (scope_ext_app 1 0 ltac:(lia))).
+      lia.
+  }
+  {
+    unfold obj_map. do 3 constructor; auto; simpl.
+    - do 2 constructor; auto.
+    - intros. destruct i. 2: destruct i. 3: destruct i.
+      constructor. constructor. lia.
+      all: auto.
+      constructor. do 2 constructor. lia. simpl.
+      intros. destruct i. 2: destruct i. 3: destruct i.
+      1-3: do 2 constructor. all: lia.
+    - do 2 constructor; auto.
+    - simpl in *. destruct i. 2: destruct i. 3: destruct i.
+      do 3 constructor; simpl. all: auto.
+      + do 2 constructor. simpl. now apply (proj2 (scope_ext_app 6 2 ltac:(lia))).
+      + intros. destruct i. do 2 constructor. all: lia.
+      + now apply (proj1 (scope_ext_app 1 0 ltac:(lia))).
+      + lia.
+  }
+Qed.
+
+Theorem map_foldr_equiv_rev :
+  forall l' l x y z e f
+  (VsCL : VALCLOSED l) (SCE : EXP 2 ⊢ e),
+  computes x e f -> cons_to_list l = Some l' ->
+  CIU (obj_foldr (EFun [y;z] (ECons (EApp (EFun [x] e) [EVar 1]) (EVar 2))) l ENil) (obj_map (EFun [x] e) l).
+Proof.
+  intros.
+  pose proof (obj_foldr_on_meta_level l' l x y z e f VsCL SCE H H0).
+  pose proof (obj_map_on_meta_level l' l x e f VsCL SCE H H0).
+  eapply CIU_evaluates; eauto.
+  2: {
+    unfold obj_map. do 3 constructor; auto; simpl.
+    - constructor. simpl. constructor; auto.
+      cbn. constructor; auto.
+      destruct i. 2: destruct i.
+      all: constructor. lia.
+    - do 2 constructor; auto. simpl in H3.
+      destruct i. 2: destruct i. 3: destruct i. all: constructor. all: lia.
+    - simpl in *. destruct i. 2: destruct i.
+      constructor; simpl. now apply (proj2 (scope_ext_app 3 2 ltac:(lia))).
+      now apply (proj1 (scope_ext_app 1 0 ltac:(lia))).
+      lia.
+  }
+  {
+    unfold obj_map. do 3 constructor; auto; simpl.
+    - do 2 constructor; auto.
+    - intros. destruct i. 2: destruct i. 3: destruct i.
+      constructor. constructor. lia.
+      all: auto.
+      constructor. do 2 constructor. lia. simpl.
+      intros. destruct i. 2: destruct i. 3: destruct i.
+      1-3: do 2 constructor. all: lia.
+    - do 2 constructor; auto.
+    - simpl in *. destruct i. 2: destruct i. 3: destruct i.
+      do 3 constructor; simpl. all: auto.
+      + do 2 constructor. simpl. now apply (proj2 (scope_ext_app 6 2 ltac:(lia))).
+      + intros. destruct i. do 2 constructor. all: lia.
+      + now apply (proj1 (scope_ext_app 1 0 ltac:(lia))).
+      + lia.
+  }
+Qed.
+

src/Examples.v

@@ -1,3 +1,9 @@
+(**
+  This file is a part of a formalisation of a subset of Core Erlang.
+
+  In this file, we show example program evaluation in concurrent Core Erlang.
+*)
+
 Require Import ConcurrentFunSemantics.
 Import ListNotations.
 Import PeanoNat.

src/ExpManipulation.v

@@ -1,3 +1,16 @@
+(**
+
+  This file is a part of a formalisation of a subset of Core Erlang.
+
+  In this file, we describe the capture-avoiding
+  renaming and substitution for Core
+  Erlang expressions. This work is based on the techniques of the Autosubst
+  library [1] and Wand et al. [2].
+
+  1: https://github.com/coq-community/autosubst
+  2: https://dl.acm.org/doi/10.1145/3236782
+*)
+
 Require Export ExpSyntax
                Coq.Structures.OrderedType.
 
@@ -45,9 +58,11 @@ match e with
  | EReceive l => EReceive (map (fun '(p, v) => (p, rename (uprenn (pat_vars p) ρ) v)) l)
 end.
 
-Definition Substitution := nat -> Exp + nat. (** We need to have the names for the
-                                                  identity elements explicitly, because 
-                                                  of the shiftings (up, upn) *)
+Definition Substitution := nat -> Exp + nat.
+(** We need to have the names for the
+    identity elements explicitly, because of the shiftings (up, upn) *)
+
+
 Definition idsubst : Substitution := fun x => inr x.
 
 Definition shift (ξ : Substitution) : Substitution :=