X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskProofToStrong.v;h=b14a53e8f23ca3e84921e9a1d126b599c52b70eb;hp=d38286d549af7a4b1623672181b186619e606fa3;hb=dac68fdf6d495ed60d3e4c5738c27ca7fffc1399;hpb=6ef9f270b138fc7aab48013d55a8192ff022c0f1

diff --git a/src/HaskProofToStrong.v b/src/HaskProofToStrong.v
index d38286d..b14a53e 100644
--- a/src/HaskProofToStrong.v
+++ b/src/HaskProofToStrong.v
@@ -569,7 +569,6 @@ Section HaskProofToStrong.
   destruct case_RGlobal.
     apply ILeaf; simpl; intros; refine (return ILeaf _ _).
     apply EGlobal.
-    apply wev.
 
   destruct case_RLam.
     apply ILeaf.
@@ -577,7 +576,7 @@ Section HaskProofToStrong.
     refine (fresh_lemma _ ξ vars _ tx x H >>>= (fun pf => _)).
     apply FreshMon.
     destruct pf as [ vnew [ pf1 pf2 ]].
-    set (update_ξ ξ x ((⟨vnew, tx  ⟩) :: nil)) as ξ' in *.
+    set (update_ξ ξ x (((vnew, tx  )) :: nil)) as ξ' in *.
     refine (X_ ξ' (vars,,[vnew]) _ >>>= _).
     apply FreshMon.
     simpl.
@@ -642,7 +641,7 @@ Section HaskProofToStrong.
     refine (fresh_lemma _ ξ vars1 _ σ₂ p H1 >>>= (fun pf => _)).
     apply FreshMon.
     destruct pf as [ vnew [ pf1 pf2 ]].
-    set (update_ξ ξ p ((⟨vnew, σ₂  ⟩) :: nil)) as ξ' in *.
+    set (update_ξ ξ p (((vnew, σ₂ )) :: nil)) as ξ' in *.
     inversion X_.
     apply ileaf in X.
     apply ileaf in X0.
@@ -715,6 +714,7 @@ Section HaskProofToStrong.
     inversion X; subst; clear X.
 
     apply (@ELetRec _ _ _ _ _ _ _ varstypes).
+    auto.
     apply (@letrec_helper Γ Δ t varstypes).
     rewrite <- pf2 in X1.
     rewrite mapOptionTree_compose.
@@ -758,15 +758,12 @@ Section HaskProofToStrong.
       apply H2.
     Defined.
 
-  Definition closed2expr : forall c (pn:@ClosedSIND _ Rule c), ITree _ judg2exprType c.
-    refine ((
-      fix closed2expr' j (pn:@ClosedSIND _ Rule j) {struct pn} : ITree _ judg2exprType j :=
-      match pn in @ClosedSIND _ _ J return ITree _ judg2exprType J with
-      | cnd_weak             => let case_nil    := tt in INone _ _
-      | cnd_rule h c cnd' r  => let case_rule   := tt in rule2expr _ _ r (closed2expr' _ cnd')
-      | cnd_branch _ _ c1 c2 => let case_branch := tt in IBranch _ _ (closed2expr' _ c1) (closed2expr' _ c2)
-      end)); clear closed2expr'; intros; subst.
-        Defined.
+  Fixpoint closed2expr h j (pn:@SIND _ Rule h j) {struct pn} : ITree _ judg2exprType h -> ITree _ judg2exprType j :=
+    match pn in @SIND _ _ H J return ITree _ judg2exprType H -> ITree _ judg2exprType J with
+    | scnd_weak   _             => let case_nil    := tt in fun _ => INone _ _
+    | scnd_comp   x h c cnd' r  => let case_rule   := tt in fun q => rule2expr _ _ r (closed2expr _ _ cnd' q)
+    | scnd_branch _ _ _ c1 c2   => let case_branch := tt in fun q => IBranch _ _ (closed2expr _ _ c1 q) (closed2expr _ _ c2 q)
+    end.
 
   Lemma manyFresh : forall Γ Σ (ξ0:VV -> LeveledHaskType Γ ★),
     FreshM { vars : _ & { ξ : VV -> LeveledHaskType Γ ★ & Σ = mapOptionTree ξ vars } }.
@@ -804,7 +801,7 @@ Section HaskProofToStrong.
     {zz:ToString VV} : ND Rule [] [Γ > Δ > Σ |- [τ]] ->
     FreshM (???{ ξ : _ & Expr Γ Δ ξ τ}).
     intro pf.
-    set (closedFromSIND _ _ (mkSIND systemfc_all_rules_one_conclusion _ _ _ pf (scnd_weak [])) cnd_weak) as cnd.
+    set (mkSIND systemfc_all_rules_one_conclusion _ _ _ pf (scnd_weak [])) as cnd.
     apply closed2expr in cnd.
     apply ileaf in cnd.
     simpl in *.
@@ -819,6 +816,7 @@ Section HaskProofToStrong.
     refine (return OK _).
     exists ξ.
     apply (ileaf it).
+    apply INone.
     Defined.
 
 End HaskProofToStrong.