Add some documentation to Coq files and simplify ssa proofs

coq/Commands.v

@@ -6,28 +6,16 @@ Require Export Daisy.Infra.ExpressionAbbrevs Daisy.Infra.NatSet.
 
 (**
   Next define what a program is.
-  Currently no loops, only conditionals and assignments
-  Final return statement
+  Currently no loops, or conditionals.
+  Only assignments and return statement
 **)
 Inductive cmd (V:Type) :Type :=
 Let: nat -> exp V -> cmd V -> cmd V
 | Ret: exp V -> cmd V.
-(*| Nop: cmd V. *)
-
-(*
-UNUSED!
-   Small Step semantics for Daisy language
-Inductive sstep : cmd R -> env -> R -> cmd R -> env -> Prop :=
-  let_s x e s E v eps:
-    eval_exp eps E e v ->
-    sstep (Let x e s) E eps s (updEnv x v E)
- |ret_s e E v eps:
-    eval_exp eps E e v ->
-    sstep (Ret e) E eps (Nop R) (updEnv 0 v E).
- *)
 
 (**
-  Analogously define Big Step semantics for the Daisy language
+  Define big step semantics for the Daisy language, terminating on a "returned"
+  result value
  **)
 Inductive bstep : cmd R -> env -> R -> R -> Prop :=
   let_b x e s E v eps res:
@@ -38,12 +26,19 @@ Inductive bstep : cmd R -> env -> R -> R -> Prop :=
     eval_exp eps E e v ->
     bstep (Ret e) E eps v.
 
+(**
+  The free variables of a command are all used variables of expressions
+  without the let bound variables
+**)
 Fixpoint freeVars V (f:cmd V) :NatSet.t :=
   match f with
-  | Let x e1 g => NatSet.remove x (NatSet.union (Expressions.freeVars e1) (freeVars g))
-  | Ret e => Expressions.freeVars e
+  | Let x e g => NatSet.remove x (NatSet.union (usedVars e) (freeVars g))
+  | Ret e => usedVars e
   end.
 
+(**
+  The defined variables of a command are all let bound variables
+**)
 Fixpoint definedVars V (f:cmd V) :NatSet.t :=
   match f with
   | Let x _ g => NatSet.add x (definedVars g)

coq/Expressions.v

@@ -129,8 +129,8 @@ Inductive eval_exp (eps:R) (E:env) :(exp R) -> R -> Prop :=
 Fixpoint usedVars (V:Type) (e:exp V) :NatSet.t :=
   match e with
   | Var _ x => NatSet.singleton x
-  | Unop u e1 => freeVars e1
-  | Binop b e1 e2 => NatSet.union (freeVars e1) (freeVars e2)
+  | Unop u e1 => usedVars e1
+  | Binop b e1 e2 => NatSet.union (usedVars e1) (usedVars e2)
   | _ => NatSet.empty
   end.
 

coq/ssaPrgs.v

+(**
+  We define a pseudo SSA predicate.
+  The formalization is similar to the renamedApart property in the LVC framework by Schneider, Smolka and Hack
+  http://dblp.org/rec/conf/itp/SchneiderSH15
+  Our predicate is not as fully fledged as theirs, but we especially borrow the idea of annotating
+  the program with the predicate with the set of free and defined variables
+**)
 Require Import Coq.QArith.QArith Coq.QArith.Qreals Coq.Reals.Reals.
 Require Import Coq.micromega.Psatz.
 Require Import Daisy.Infra.RealRationalProps Daisy.Infra.Ltacs.
 Require Export Daisy.Commands.
 
-Fixpoint validVars (V:Type) (f:exp V) Vs :bool :=
-  match f with
-  | Const n => true
-  | Var _ v =>  NatSet.mem v Vs
-  | Unop o f1 => validVars f1 Vs
-  | Binop o f1 f2 => validVars f1 Vs && validVars f2 Vs
-  end.
-
-Lemma validVars_subset_freeVars T (e:exp T) V:
-  validVars e V = true->
-  NatSet.Subset (Expressions.freeVars e) V.
-Proof.
-  revert V; induction e; simpl; intros V valid_V; try auto.
-  - rewrite NatSet.mem_spec in valid_V.
-    hnf. intros; rewrite NatSet.singleton_spec in *; subst; auto.
-  - hnf; intros a in_empty; inversion in_empty.
-  - andb_to_prop valid_V.
-    hnf; intros a in_union.
-    rewrite NatSet.union_spec in in_union.
-    destruct in_union as [in_e1 | in_e2].
-    + specialize (IHe1 V L a in_e1); auto.
-    + specialize (IHe2 V R a in_e2); auto.
-Qed.
-
-Lemma validVars_add V (f:exp V) Vs n:
-  validVars f Vs = true ->
-  validVars f (NatSet.add n Vs) = true.
+Lemma validVars_add V (e:exp V) Vs n:
+  NatSet.Subset (usedVars e) Vs ->
+  NatSet.Subset (usedVars e) (NatSet.add n Vs).
 Proof.
-  induction f; try auto.
-  - intros valid_var. unfold validVars in *; simpl in *.
-    rewrite NatSet.mem_spec in *.
+  induction e; try auto.
+  - intros valid_subset.
+    hnf. intros a in_singleton.
+    specialize (valid_subset a in_singleton).
     rewrite NatSet.add_spec; right; auto.
   - intros vars_binop.
     simpl in *.
-    apply Is_true_eq_left in vars_binop.
-    apply Is_true_eq_true.
-    apply andb_prop_intro.
-    apply andb_prop_elim in vars_binop.
-    destruct vars_binop; split; apply Is_true_eq_left.
-    + apply IHf1. apply Is_true_eq_true; auto.
-    + apply IHf2. apply Is_true_eq_true; auto.
-Qed.
-
-Lemma validVars_valid_subset (V:Type) (e:exp V) inVars:
-  validVars e inVars = true ->
-  NatSet.Subset (Expressions.freeVars e) inVars.
-Proof.
-  induction e; intros vars_valid; unfold validVars in *; simpl in *; try auto.
-  - rewrite NatSet.mem_spec in vars_valid.
-    hnf. intros; rewrite NatSet.singleton_spec in *; subst; auto.
-  - hnf; intros a in_empty; inversion in_empty.
-  - hnf; intros a in_union; rewrite NatSet.union_spec in in_union.
-    rewrite andb_true_iff in vars_valid.
-    destruct vars_valid.
-    destruct in_union as [in_e1 | in_e2].
-    + apply IHe1; auto.
-    + apply IHe2; auto.
+    intros a in_empty.
+    inversion in_empty.
+  - simpl; intros in_vars.
+    intros a in_union.
+    rewrite NatSet.union_spec in in_union.
+    destruct in_union.
+    + apply IHe1; try auto.
+      hnf; intros.
+      apply in_vars.
+      rewrite NatSet.union_spec; auto.
+    + apply IHe2; try auto.
+      hnf; intros.
+      apply in_vars.
+      rewrite NatSet.union_spec; auto.
 Qed.
 
 Lemma validVars_non_stuck (e:exp Q) inVars E:
-  validVars e inVars = true ->
-  (forall v, NatSet.In v (Expressions.freeVars e) ->
+ NatSet.Subset (usedVars e) inVars ->
+  (forall v, NatSet.In v (usedVars e) ->
         exists r, E v = Some r)%R ->
   exists vR, eval_exp 0 E (toRExp e) vR.
 Proof.
@@ -84,50 +59,38 @@ Proof.
     + exists (evalUnop Neg ve); constructor; auto.
     + exists (perturb (evalUnop Inv ve) 0); constructor; auto.
       rewrite Rabs_R0; lra.
-  - andb_to_prop vars_valid; simpl in *.
+  - repeat rewrite NatSet.subset_spec in *; simpl in *.
     assert (exists vR1, eval_exp 0 E (toRExp e1) vR1) as eval_e1_def.
     + eapply IHe1; eauto.
-      intros.
-      destruct (fVars_live v) as [vR E_def]; try eauto.
-      apply NatSet.union_spec; auto.
-    + assert (exists vR2, eval_exp 0 E (toRExp e2) vR2) as eval_e2_def.
-      * eapply IHe2; eauto.
-        intros.
+      * hnf; intros.
+        apply vars_valid.
+        rewrite NatSet.union_spec; auto.
+      * intros.
         destruct (fVars_live v) as [vR E_def]; try eauto.
         apply NatSet.union_spec; auto.
+    + assert (exists vR2, eval_exp 0 E (toRExp e2) vR2) as eval_e2_def.
+      * eapply IHe2; eauto.
+        { hnf; intros.
+        apply vars_valid.
+        rewrite NatSet.union_spec; auto. }
+        { intros.
+          destruct (fVars_live v) as [vR E_def]; try eauto.
+          apply NatSet.union_spec; auto. }
       * destruct eval_e1_def as [vR1 eval_e1_def];
           destruct eval_e2_def as [vR2 eval_e2_def].
         exists (perturb (evalBinop b vR1 vR2) 0); constructor; auto.
         rewrite Rabs_R0; lra.
 Qed.
 
-Lemma validVars_equal_set V (e:exp V) vars vars':
-  NatSet.Equal vars vars' ->
-  validVars e vars = true ->
-  validVars e vars' = true.
-Proof.
-  revert vars vars'.
-  induction e; intros vars vars' eq_set valid_vars; simpl in *; auto.
-  - rewrite NatSet.mem_spec in *.
-    rewrite <- eq_set; auto.
-  - eapply IHe; eauto.
-  - apply Is_true_eq_true.
-    apply andb_prop_intro.
-    andb_to_prop valid_vars.
-    split; apply Is_true_eq_left.
-    + eapply IHe1; eauto.
-    + eapply IHe2; eauto.
-Qed.
-
 Inductive ssaPrg (V:Type): (cmd V) -> (NatSet.t) -> (NatSet.t) -> Prop :=
  ssaLet x e s inVars Vterm:
-   validVars e inVars = true->
+   NatSet.Subset (usedVars e) inVars->
    NatSet.mem x inVars = false ->
    ssaPrg s (NatSet.add x inVars) Vterm ->
    ssaPrg (Let x e s) inVars Vterm
 |ssaRet e inVars Vterm:
-   validVars e inVars = true ->
-   NatSet.equal inVars (NatSet.remove 0%nat Vterm) = true->
+   NatSet.Subset (usedVars e) inVars ->
+   NatSet.Equal inVars Vterm ->
    ssaPrg (Ret e) inVars Vterm.
 
 Lemma ssa_subset_freeVars V (f:cmd V) inVars outVars:
@@ -135,8 +98,7 @@ Lemma ssa_subset_freeVars V (f:cmd V) inVars outVars:
   NatSet.Subset (Commands.freeVars f) inVars.
 Proof.
   intros ssa_f; induction ssa_f.
-  - simpl in *. apply validVars_subset_freeVars in H.
-    hnf; intros a in_fVars.
+  - simpl in *. hnf; intros a in_fVars.
     rewrite NatSet.remove_spec, NatSet.union_spec in in_fVars.
     destruct in_fVars as [in_union not_eq].
     destruct in_union; try auto.
@@ -145,7 +107,6 @@ Proof.
     destruct IHssa_f; subst; try auto.
     exfalso; apply not_eq; auto.
   - hnf; intros.
-    apply validVars_subset_freeVars in H.
     simpl in H1.
     apply H; auto.
 Qed.
@@ -159,8 +120,7 @@ Proof.
   revert set_eq; revert inVars'.
   induction ssa_f.
   - constructor.
-    + eapply validVars_equal_set; eauto.
-      symmetry; auto.
+    + rewrite set_eq; auto.
     + case_eq (NatSet.mem x inVars'); intros case_mem; try auto.
       rewrite NatSet.mem_spec in case_mem.
       rewrite set_eq in case_mem.
@@ -169,20 +129,15 @@ Proof.
     + apply IHssa_f; auto.
       apply NatSetProps.Dec.F.add_m; auto.
   - constructor.
-    + eapply validVars_equal_set; eauto.
-      symmetry; auto.
-    + rewrite NatSet.equal_spec in *.
-      hnf. intros a; split.
-      * intros in_primed.
-        rewrite <- H0. rewrite <- set_eq. auto.
-      * intros in_rem. rewrite set_eq. rewrite H0; auto.
+    + rewrite set_eq; auto.
+    + rewrite set_eq; auto.
 Qed.
 
 Fixpoint validSSA (f:cmd Q) (inVars:NatSet.t) :=
   match f with
   |Let x e g =>
-    andb (andb (negb (NatSet.mem x inVars)) (validVars e inVars)) (validSSA g (NatSet.add x inVars))
-  |Ret e => validVars e inVars && (negb (NatSet.mem 0%nat inVars))
+    andb (andb (negb (NatSet.mem x inVars)) (NatSet.subset (usedVars e) inVars)) (validSSA g (NatSet.add x inVars))
+  |Ret e => NatSet.subset (usedVars e) inVars
   end.
 
 Lemma validSSA_sound f inVars:
@@ -197,32 +152,14 @@ Proof.
     destruct IHf as [outVars IHf].
     exists outVars.
     constructor; eauto.
-    rewrite negb_true_iff in L0. auto.
+    + rewrite <- NatSet.subset_spec; auto.
+    + rewrite negb_true_iff in L0. auto.
   - intros inVars validSSA_ret.
     simpl in *.
-    exists (NatSet.add 0%nat inVars).
-    andb_to_prop validSSA_ret.
+    exists inVars.
     constructor; auto.
-    rewrite negb_true_iff in R.
-    hnf in R.
-    rewrite NatSet.equal_spec.
-    hnf.
-    intros a.
-    rewrite NatSet.remove_spec, NatSet.add_spec.
-    split.
-    + intros in_inVars.
-      case_eq (a =? 0%nat).
-      * intros a_zero.
-        rewrite Nat.eqb_eq in a_zero.
-        rewrite a_zero in in_inVars.
-        rewrite <- NatSet.mem_spec in in_inVars.
-        rewrite in_inVars in R.
-        inversion R.
-      * intros a_neq_zero. apply beq_nat_false in a_neq_zero.
-        split; auto.
-    + intros in_add_rem.
-      destruct in_add_rem as [ [a_zero | a_inVars] a_neq_zero]; try auto.
-      exfalso; eauto.
+    + rewrite <- NatSet.subset_spec; auto.
+    + hnf; intros; split; auto.
 Qed.
 
 Lemma ssa_shadowing_free x y v v' e f inVars outVars E:
@@ -301,7 +238,7 @@ Proof.
 Qed.
 
 Lemma dummy_bind_ok e v x v' inVars E:
-  validVars e inVars = true ->
+  NatSet.Subset (usedVars e) inVars ->
   NatSet.mem x inVars = false ->
   eval_exp 0 E (toRExp e) v ->
   eval_exp 0 (updEnv x v' E) (toRExp e) v.
@@ -315,7 +252,13 @@ Proof.
       intros n_eq_x.
       rewrite Nat.eqb_eq in n_eq_x.
       subst; simpl in *.
-      rewrite x_not_free in valid_vars; inversion valid_vars.
+      hnf in valid_vars.
+      assert (NatSet.mem x (NatSet.singleton x) = true)
+        as in_singleton by (rewrite NatSet.mem_spec, NatSet.singleton_spec; auto).
+      rewrite NatSet.mem_spec in *.
+      specialize (valid_vars x in_singleton).
+      rewrite <- NatSet.mem_spec in valid_vars.
+      rewrite valid_vars in *; congruence.
     + econstructor.
       rewrite H; auto.
   - inversion eval_e; subst; constructor; auto.
@@ -323,14 +266,15 @@ Proof.
     + eapply IHe; eauto.
     + eapply IHe; eauto.
   - simpl in valid_vars.
-    apply Is_true_eq_left in valid_vars.
-    apply andb_prop_elim in valid_vars.
-    destruct valid_vars.
     inversion eval_e; subst; constructor; auto.
     + eapply IHe1; eauto.
-      apply Is_true_eq_true; auto.
+      hnf; intros a in_e1.
+      apply valid_vars;
+        rewrite NatSet.union_spec; auto.
     + eapply IHe2; eauto.
-      apply Is_true_eq_true; auto.
+      hnf; intros a in_e2.
+      apply valid_vars;
+        rewrite NatSet.union_spec; auto.
 Qed.
 
 Fixpoint exp_subst (e:exp Q) x e_new :=
@@ -397,7 +341,7 @@ Fixpoint map_subst (f:cmd Q) x e :=
 Lemma stepwise_substitution x e v f E vR inVars outVars:
   ssaPrg f inVars outVars ->
   NatSet.In x inVars ->
-  validVars e inVars = true ->
+  NatSet.Subset (usedVars e) inVars ->
   eval_exp 0%R E (toRExp e) v ->
   bstep (toRCmd f) (updEnv x v E) 0%R vR <->
   bstep (toRCmd (map_subst f x e)) E 0%R vR.