rename terms and files

coq-proof/FieldsDefs.v → coq-proof/FieldDefs.v

@@ -8,75 +8,75 @@ Require Import HeapDefs.
 Require Import GammaHeapCorrespondence.
 
 (* ======================================================= *)
-Inductive Field_Declaration : Type :=
-  | FD_Empty : Field_Declaration
-  | FD_Decl : Unit -> ID -> nat -> Field_Declaration -> Field_Declaration.
-Tactic Notation "fd_cases" tactic(first) ident(c) :=
+Inductive Field_Declarations : Type :=
+  | FD_Empty : Field_Declarations
+  | FD_Decl : Unit -> ID -> nat -> Field_Declarations -> Field_Declarations.
+Tactic Notation "fds_cases" tactic(first) ident(c) :=
   first;
   [ Case_aux c "FD_Empty"
   | Case_aux c "FD_Decl"
   ].
-Hint Constructors Field_Declaration.
+Hint Constructors Field_Declarations.
 
 (* ======================================================= *)
-Reserved Notation "'fd:' g1 '|-' fds 'in' g2" (at level 40).
-Inductive fd_has_type : Gamma -> Field_Declaration -> Gamma -> Prop :=
+Reserved Notation "'fds:' g1 '|-' fds 'in' g2" (at level 40).
+Inductive fds_has_type : Gamma -> Field_Declarations -> Gamma -> Prop :=
   | T_FD_Empty : forall (g : Gamma),
-    fd: g |- FD_Empty in g
-  | T_FD : forall (g1 g2 : Gamma) (tail : Field_Declaration) (T : Unit) (f : ID) (z : nat),
+    fds: g |- FD_Empty in g
+  | T_FD : forall (g1 g2 : Gamma) (tail : Field_Declarations) (T : Unit) (f : ID) (z : nat),
     Gamma_Contains g1 f = false ->
     Gamma_Contains g2 f = true ->
     Gamma_Get g2 f = Some T ->
-    fd: Gamma_Extend g1 f T |- tail in g2 ->
-    fd: g1 |- FD_Decl T f z tail in g2
-where "'fd:' g1 '|-' fds 'in' g2" := (fd_has_type g1 fds g2).
-Tactic Notation "fd_has_type_cases" tactic(first) ident(c) :=
+    fds: Gamma_Extend g1 f T |- tail in g2 ->
+    fds: g1 |- FD_Decl T f z tail in g2
+where "'fds:' g1 '|-' fds 'in' g2" := (fds_has_type g1 fds g2).
+Tactic Notation "fds_has_type_cases" tactic(first) ident(c) :=
   first;
   [ Case_aux c "T_FD_Empty"
   | Case_aux c "T_FD"
   ].
-Hint Constructors fd_has_type.
+Hint Constructors fds_has_type.
 
 (* ======================================================= *)
-Reserved Notation " fd1 'fd==>' fd2 " (at level 8).
-Inductive fd_small_step : prod Heap Field_Declaration -> prod Heap Field_Declaration -> Prop :=
-  | ST_FD : forall (h : Heap) (T : Unit) (f : ID) (z : nat) (fds : Field_Declaration),
-    ( h, FD_Decl T f z fds ) fd==> ( (Heap_Update h f T T z), fds )
-where " fd1 'fd==>' fd2 " := (fd_small_step fd1 fd2).
-Tactic Notation "fd_small_step_cases" tactic(first) ident(c) :=
+Reserved Notation " fds1 'fds==>' fds2 " (at level 8).
+Inductive fds_small_step : prod Heap Field_Declarations -> prod Heap Field_Declarations -> Prop :=
+  | ST_FD : forall (h : Heap) (T : Unit) (f : ID) (z : nat) (fds : Field_Declarations),
+    ( h, FD_Decl T f z fds ) fds==> ( (Heap_Update h f T T z), fds )
+where " fds1 'fds==>' fds2 " := (fds_small_step fds1 fds2).
+Tactic Notation "fds_small_step_cases" tactic(first) ident(c) :=
   first;
   [ Case_aux c "ST_FD"
   ].
-Hint Constructors fd_small_step.
+Hint Constructors fds_small_step.
 
 (* ======================================================= *)
 (* step is deterministic *)
-Theorem fd_small_step_deterministic:
-  forall fd fd1 fd2,
-    fd fd==> fd1 ->
-    fd fd==> fd2 ->
-    fd1 = fd2.
+Theorem fds_small_step_deterministic:
+  forall fds fds1 fds2,
+    fds fds==> fds1 ->
+    fds fds==> fds2 ->
+    fds1 = fds2.
 Proof.
-  intros fd fd1 fd2 Hfd1.
-  generalize dependent fd2.
-  fd_small_step_cases (induction Hfd1) Case.
+  intros fds fds1 fds2 Hfds1.
+  generalize dependent fds2.
+  fds_small_step_cases (induction Hfds1) Case.
   Case "ST_FD".
-    intros fd2 Hfd2.
-    inversion Hfd2; subst. reflexivity.
+    intros fds2 Hfds2.
+    inversion Hfds2; subst. reflexivity.
 Qed.
 
 (* ======================================================= *)
-Inductive FD_Normal_Form : Field_Declaration -> Prop :=
+Inductive FD_Normal_Form : Field_Declarations -> Prop :=
   | V_FD_Empty : FD_Normal_Form FD_Empty.
 
 (* ======================================================= *)
-Theorem fd_progress : forall (fd : Field_Declaration) (g1 g2 : Gamma) (h : Heap),
-  fd: g1 |- fd in g2 ->
-  FD_Normal_Form fd \/ exists h' fd', (h, fd) fd==> (h', fd').
+Theorem fds_progress : forall (fds : Field_Declarations) (g1 g2 : Gamma) (h : Heap),
+  fds: g1 |- fds in g2 ->
+  FD_Normal_Form fds \/ exists h' fds', (h, fds) fds==> (h', fds').
 Proof.
-  (* by induction on typing of fd *)
-  intros fd g1 g2 h HT.
-  fd_has_type_cases (induction HT) Case; subst.
+  (* by induction on typing of fds *)
+  intros fds g1 g2 h HT.
+  fds_has_type_cases (induction HT) Case; subst.
   Case "T_FD_Empty".
     left. apply V_FD_Empty.
   Case "T_FD".
@@ -88,25 +88,25 @@ Qed.
 
 (* ======================================================= *)
 
-(* Returns the first field definition in the list of field definitions fd, or None if the list is empty *)
-Definition First_FD (fd : Field_Declaration) : option (prod (prod Unit ID) nat) :=
-  match fd with
-  | FD_Decl T f z fd => Some (T, f, z)
+(* Returns the first field definition in the list of field definitions fds, or None if the list is empty *)
+Definition First_FD (fds : Field_Declarations) : option (prod (prod Unit ID) nat) :=
+  match fds with
+  | FD_Decl T f z fds => Some (T, f, z)
   | FD_Empty => None
   end.
 
 (* ======================================================= *)
 
-Theorem fd_preservation : forall (g1 g2 : Gamma) (h h' : Heap) (fd fd' : Field_Declaration) (T : Unit) (f : ID) (z : nat),
-  fd: g1 |- fd in g2 ->
+Theorem fds_preservation : forall (g1 g2 : Gamma) (h h' : Heap) (fds fds' : Field_Declarations) (T : Unit) (f : ID) (z : nat),
+  fds: g1 |- fds in g2 ->
   gh: g2 |- h OK ->
-  (h, fd) fd==> (h', fd') ->
-  First_FD fd = Some (T, f, z) ->
-  gh: g2 |- h' OK /\ fd: Gamma_Extend g1 f T |- fd' in g2.
+  (h, fds) fds==> (h', fds') ->
+  First_FD fds = Some (T, f, z) ->
+  gh: g2 |- h' OK /\ fds: Gamma_Extend g1 f T |- fds' in g2.
 Proof.
-  intros g1 g2 h h' fd fd' T f z HT HGH HS Hfst.
-  generalize dependent fd'. generalize dependent h'.
-  fd_has_type_cases (induction HT) Case; intros h' fd' HS; subst.
+  intros g1 g2 h h' fds fds' T f z HT HGH HS Hfst.
+  generalize dependent fds'. generalize dependent h'.
+  fds_has_type_cases (induction HT) Case; intros h' fds' HS; subst.
   Case "T_FD_Empty".
     inversion HS.
   Case "T_FD".
@@ -133,6 +133,6 @@ Proof.
         split. apply H4.
         split. rewrite <- H5. apply Heap_Update_FieldType_Neq. apply n.
         split. apply H6. rewrite <- H7. apply Heap_Update_FieldValue_Neq. apply n.
-    (* then prove that fd: Gamma_Extend g1 f T |- fd' in g2 *)
+    (* then prove that fds: Gamma_Extend g1 f T |- fds' in g2 *)
       apply HT.
 Qed.

coq-proof/GammaHeapCorrespondence.v

@@ -7,6 +7,9 @@ Require Import HeapDefs.
 
 (* ======================================================= *)
 
+(* If gamma contains a field f, then there exists Tv and Tf such that Tv <: Tf,
+    and Gamma(f) = FieldType(h, f) = Tf, FieldValue(h, f) = Tv z for some z. *)
+
 Reserved Notation "'gh:' g '|-' h 'OK'" (at level 40).
 Inductive Gamma_Heap_OK : Gamma -> Heap -> Prop :=
   | GH_Correspondence : forall (g : Gamma) (h : Heap),

coq-proof/ProgramDefs.v

@@ -16,28 +16,28 @@ Require Import ValueDefs.
 Require Import GammaDefs.
 Require Import HeapDefs.
 Require Import GammaHeapCorrespondence.
-Require Import FieldsDefs.
-Require Import ExpressionsDefs.
+Require Import FieldDefs.
+Require Import ExpressionDefs.
 Require Import StatementDefs.
 
 (* ======================================================= *)
 Inductive Program : Type :=
-  | program : Field_Declaration -> Statement -> Program.
+  | program : Field_Declarations -> Statements -> Program.
 Tactic Notation "prog_cases" tactic(first) ident(c) :=
   first;
   [ Case_aux c "program"
   ].
 Hint Constructors Program.
 
-Notation "{ fd s }" := (program fd s) (at level 1).
+Notation "{ fds s }" := (program fds s) (at level 1).
 
 (* ======================================================= *)
 Reserved Notation "'prog:' g '|-' p 'in' post_gamma" (at level 40).
 Inductive prog_has_type : Gamma -> Program -> Gamma -> Prop :=
-  | T_Program : forall (g post_gamma : Gamma) (fd : Field_Declaration) (s : Statement),
-    fd: g |- fd in post_gamma ->
+  | T_Program : forall (g post_gamma : Gamma) (fds : Field_Declarations) (s : Statements),
+    fds: g |- fds in post_gamma ->
     stmt: post_gamma |- s ->
-    prog: g |- program fd s in post_gamma
+    prog: g |- program fds s in post_gamma
 where "'prog:' g '|-' p 'in' post_gamma" := (prog_has_type g p post_gamma).
 Tactic Notation "prog_has_type_cases" tactic(first) ident(c) :=
   first;
@@ -48,17 +48,17 @@ Hint Constructors prog_has_type.
 (* ======================================================= *)
 Reserved Notation " p1 'prog==>' p2 " (at level 8).
 Inductive prog_small_step : prod Heap Program -> prod Heap Program -> Prop :=
-  | ST_PROG_FieldDefs_Step : forall h h' fd fd' s,
-    ( h, fd ) fd==> ( h', fd' ) ->
-    ( h, program fd s ) prog==> ( h', program fd' s )
-  | ST_PROG_Statements_Step : forall h h' s s',
+  | ST_PROG_FieldDefs_Step : forall h h' fds fds' s,
+    ( h, fds ) fds==> ( h', fds' ) ->
+    ( h, program fds s ) prog==> ( h', program fds' s )
+  | ST_PROG_Statementss_Step : forall h h' s s',
     ( h, s ) stmt==> ( h', s' ) ->
     ( h, program FD_Empty s ) prog==> ( h', program FD_Empty s' )
 where " p1 'prog==>' p2 " := (prog_small_step p1 p2).
 Tactic Notation "prog_small_step_cases" tactic(first) ident(c) :=
   first;
   [ Case_aux c "ST_PROG_FieldDefs_Step"
-  | Case_aux c "ST_PROG_Statements_Step"
+  | Case_aux c "ST_PROG_Statementss_Step"
   ].
 Hint Constructors prog_small_step.
 
@@ -75,10 +75,10 @@ Proof.
   prog_small_step_cases (induction Hp1) Case.
   Case "ST_PROG_FieldDefs_Step".
     intros p2 Hp2; inversion Hp2; subst.
-      assert ((h', fd') = (h'0, fd'0)) as HfdEQ. eapply fd_small_step_deterministic.
-        apply H. apply H4. inversion HfdEQ; subst. reflexivity.
+      assert ((h', fds') = (h'0, fds'0)) as HfdsEQ. eapply fds_small_step_deterministic.
+        apply H. apply H4. inversion HfdsEQ; subst. reflexivity.
       inversion H.
-  Case "ST_PROG_Statements_Step".
+  Case "ST_PROG_Statementss_Step".
     intros p2 Hp2; inversion Hp2; subst.
       inversion H4.
       assert ((h', s') = (h'0, s'0)) as HsEQ. eapply stmt_small_step_deterministic.
@@ -99,9 +99,9 @@ Proof.
   intros g1 g2 p h HT HGH.
   prog_has_type_cases (induction HT) Case; subst.
   Case "T_Program".
-    assert (FD_Normal_Form fd \/ exists heap' fd', (h, fd) fd==> (heap', fd')).
-      eapply fd_progress. apply H.
-    assert (STMT_Normal_Form s \/ exists (h' : Heap) (s' : Statement), (h, s) stmt==> (h', s')).
+    assert (FD_Normal_Form fds \/ exists heap' fds', (h, fds) fds==> (heap', fds')).
+      eapply fds_progress. apply H.
+    assert (STMT_Normal_Form s \/ exists (h' : Heap) (s' : Statements), (h, s) stmt==> (h', s')).
       eapply stmt_progress. apply H0. apply HGH.
     destruct H1; subst.
     (* Case : FD is normal form *)
@@ -111,18 +111,18 @@ Proof.
       (* Case : STMT can take a step *)
         destruct H1; subst. right. destruct H2 as [h']. destruct H1 as [s'].
         exists h'. exists (program FD_Empty s').
-        apply ST_PROG_Statements_Step. apply H1.
+        apply ST_PROG_Statementss_Step. apply H1.
     (* Case : FD can take a step *)
-      destruct H1 as [h']. destruct H1 as [fd']. right.
-      exists h'. exists (program fd' s).
+      destruct H1 as [h']. destruct H1 as [fds']. right.
+      exists h'. exists (program fds' s).
       apply ST_PROG_FieldDefs_Step. apply H1.
 Qed.
 
 (* ======================================================= *)
 
 Definition Gamma_Extend_Prog (g : Gamma) (p : Program) : Gamma :=
   match p with
-  | program fd s => match First_FD fd with
+  | program fds s => match First_FD fds with
                     | Some (T, f, z) => Gamma_Extend g f T
                     | None => g
                     end
@@ -142,12 +142,12 @@ Proof.
   generalize dependent p'. generalize dependent h'.
   prog_has_type_cases (induction HT) Case; intros h' p' HS; subst.
   Case "T_Program".
-    destruct p' as [fd' s'].
+    destruct p' as [fds' s'].
     prog_small_step_cases (inversion HS) SCase; subst.
     SCase "ST_PROG_FieldDefs_Step".
       inversion H2; subst.
       unfold Gamma_Extend_Prog. simpl.
-      eapply fd_preservation in H.
+      eapply fds_preservation in H.
       destruct H.
         split.
         (* first prove that post_gamma |- h' OK *)
@@ -159,7 +159,7 @@ Proof.
         apply HGH.
         apply H2.
         simpl. reflexivity.
-    SCase "ST_PROG_Statements_Step".
+    SCase "ST_PROG_Statementss_Step".
       simpl. (* in statement step, the input gamma to type p' does not change *)
         eapply stmt_preservation in H0.
         split.

coq-proof/README.md

@@ -34,9 +34,9 @@ run `./cleanup.sh` to remove coq output files
 
 `UnitsArithmetics.v` defines and proves properties for the arithmetic functions add, multiply, and modulo between units; including the subtype consistent lemmas discussed in the paper.
 
-`FieldsDefs.v` contains the definitions and the proof of progress and preservation helper lemmas for field declarations **_fd_** in our language.
+`FieldDefs.v` contains the definitions and the proof of progress and preservation helper lemmas for field declarations **_fd_** in our language.
 
-`ExpressionsDefs.v` contains the definitions and the proof of progress and preservation helper lemmas for expressions **_e_** in our language.
+`ExpressionDefs.v` contains the definitions and the proof of progress and preservation helper lemmas for expressions **_e_** in our language.
 
 `StatementDefs.v` contains the definitions and the proof of progress and preservation helper lemmas for assignment statements **_s_** in our language.