X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskStrongToProof.v;h=c1e54aa9499a323352376f3c7753d1deb97532ba;hp=b0c5b11180c4e2775354ec25704507d839f4bc01;hb=9e7ea73d3a6f4bbfba279164a806490cf95efec4;hpb=fd337b235014f43000773eb0d95168d89e93a893

diff --git a/src/HaskStrongToProof.v b/src/HaskStrongToProof.v
index b0c5b11..c1e54aa 100644
--- a/src/HaskStrongToProof.v
+++ b/src/HaskStrongToProof.v
@@ -142,7 +142,7 @@ Lemma strip_twice_lemma x y t : stripOutVars x (stripOutVars y t) = stripOutVars
   rewrite app_comm_cons.
   reflexivity.
 *)
-admit.
+  admit.
   Qed.
 
 Lemma strip_distinct a y : (not (In a (leaves y))) -> stripOutVars (a :: nil) y = y.
@@ -363,21 +363,6 @@ Fixpoint eLetRecTypes {Γ}{Δ}{ξ}{lev}{τ}(elrb:ELetRecBindings Γ Δ ξ lev τ
   | ELR_leaf   Γ Δ ξ  lev  v t e => [t]
   | ELR_branch Γ Δ ξ lev t1 t2 b1 b2 => (eLetRecTypes b1),,(eLetRecTypes b2)
   end.
-(*
-Fixpoint eLetRecVars {Γ}{Δ}{ξ}{lev}{τ}(elrb:ELetRecBindings Γ Δ ξ lev τ) : Tree ??VV :=
-  match elrb with
-  | ELR_nil    Γ Δ ξ lev  => []
-  | ELR_leaf   Γ Δ ξ  lev  v _ _ e => [v]
-  | ELR_branch Γ Δ ξ lev t1 t2 b1 b2 => (eLetRecVars b1),,(eLetRecVars b2)
-  end.
-
-Fixpoint eLetRecTypesVars {Γ}{Δ}{ξ}{lev}{τ}(elrb:ELetRecBindings Γ Δ ξ lev τ) : Tree ??(VV * HaskType Γ ★):=
-  match elrb with
-  | ELR_nil    Γ Δ ξ lev  => []
-  | ELR_leaf   Γ Δ ξ  lev  v t _ e => [(v, t)]
-  | ELR_branch Γ Δ ξ lev t1 t2 b1 b2 => (eLetRecTypesVars b1),,(eLetRecTypesVars b2)
-  end.
-*)
 
 Lemma stripping_nothing_is_inert
   {Γ:TypeEnv}
@@ -579,7 +564,7 @@ Lemma updating_stripped_tree_is_inert {Γ} (ξ:VV -> LeveledHaskType Γ ★) v t
   reflexivity.
   Qed.
 
-(* IDEA: use multi-conclusion proofs instead *)
+(* TODO: use multi-conclusion proofs instead *)
 Inductive LetRecSubproofs Γ Δ ξ lev : forall tree, ELetRecBindings Γ Δ ξ lev tree -> Type := 
   | lrsp_nil  : LetRecSubproofs Γ Δ ξ lev [] (ELR_nil _ _ _ _)
   | lrsp_leaf : forall v t e ,
@@ -596,12 +581,12 @@ Lemma letRecSubproofsToND Γ Δ ξ lev tree branches :
       |- (mapOptionTree (@snd _ _) tree) @@@ lev ].
   intro X; induction X; intros; simpl in *.
     apply nd_rule.
-      apply REmptyGroup.
+      apply RVoid.
     set (ξ v) as q in *.
       destruct q.
       simpl in *.
       apply n.
-    eapply nd_comp; [ idtac | eapply nd_rule; apply RBindingGroup ].
+    eapply nd_comp; [ idtac | eapply nd_rule; apply RJoin ].
     eapply nd_comp; [ apply nd_llecnac | idtac ].
     apply nd_prod; auto.
   Defined.
@@ -654,7 +639,7 @@ Lemma letRecSubproofsToND' Γ Δ ξ lev τ tree  :
   simpl.
 
   set (letRecSubproofsToND _ _ _ _ _ branches lrsp) as q.
-    eapply nd_comp; [ idtac | eapply nd_rule; apply RBindingGroup ].
+    eapply nd_comp; [ idtac | eapply nd_rule; apply RJoin ].
     eapply nd_comp; [ apply nd_llecnac | idtac ].
     apply nd_prod; auto.
     rewrite ξlemma.
@@ -826,10 +811,11 @@ Definition expr2proof  :
     destruct case_ELet; intros; simpl in *.
       eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
       eapply nd_comp; [ apply nd_llecnac | idtac ].
-      apply nd_prod; [ idtac | apply pf_let].
-      clear pf_let.
-      eapply nd_comp; [ apply pf_body | idtac ].
-      clear pf_body.
+      apply nd_prod.
+        apply pf_let.
+        clear pf_let.
+        eapply nd_comp; [ apply pf_body | idtac ].
+        clear pf_body.
       fold (@mapOptionTree VV).
       fold (mapOptionTree ξ).
       set (update_ξ ξ v ((lev,tv)::nil)) as ξ'.