X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskProofToStrong.v;h=299a83be3703e2cded3a29e49bbeafc697dca2d4;hp=6ba094e9fe98e7e3c373a86d1cf281b18e0ca532;hb=1a2754d2e135ef3c5fd7ef817e1129af93b533a5;hpb=b83e779e742413ca84df565263dafbdf9f79920a

diff --git a/src/HaskProofToStrong.v b/src/HaskProofToStrong.v
index 6ba094e..299a83b 100644
--- a/src/HaskProofToStrong.v
+++ b/src/HaskProofToStrong.v
@@ -6,6 +6,7 @@ Generalizable All Variables.
 Require Import Preamble.
 Require Import General.
 Require Import NaturalDeduction.
+Require Import NaturalDeductionContext.
 Require Import Coq.Strings.String.
 Require Import Coq.Lists.List.
 Require Import Coq.Init.Specif.
@@ -27,11 +28,11 @@ Section HaskProofToStrong.
 
   Definition judg2exprType (j:Judg) : Type :=
     match j with
-      (Γ > Δ > Σ |- τ) => forall (ξ:ExprVarResolver Γ) vars, Σ = mapOptionTree ξ vars ->
-        FreshM (ITree _ (fun t => Expr Γ Δ ξ t) τ)
+      (Γ > Δ > Σ |- τ @ l) => forall (ξ:ExprVarResolver Γ) vars, Σ = mapOptionTree ξ vars ->
+        FreshM (ITree _ (fun t => Expr Γ Δ ξ t l) τ)
       end.
 
-  Definition justOne Γ Δ ξ τ : ITree _ (fun t => Expr Γ Δ ξ t) [τ] -> Expr Γ Δ ξ τ.
+  Definition justOne Γ Δ ξ τ l : ITree _ (fun t => Expr Γ Δ ξ t l) [τ] -> Expr Γ Δ ξ τ l.
     intros.
     inversion X; auto.
     Defined.
@@ -42,7 +43,7 @@ Section HaskProofToStrong.
     Defined.
 
   Lemma update_branches : forall Γ (ξ:VV -> LeveledHaskType Γ ★) lev l1 l2 q,
-    update_ξ ξ lev (app l1 l2) q = update_ξ (update_ξ ξ lev l2) lev l1 q.
+    update_xi ξ lev (app l1 l2) q = update_xi (update_xi ξ lev l2) lev l1 q.
     intros.
     induction l1.
       reflexivity.
@@ -122,7 +123,7 @@ Section HaskProofToStrong.
   Lemma fresh_lemma'' Γ 
     : forall types ξ lev, 
     FreshM { varstypes : _
-      |  mapOptionTree (update_ξ(Γ:=Γ)   ξ lev (leaves varstypes)) (mapOptionTree (@fst _ _) varstypes) = (types @@@ lev)
+      |  mapOptionTree (update_xi(Γ:=Γ)   ξ lev (leaves varstypes)) (mapOptionTree (@fst _ _) varstypes) = (types @@@ lev)
       /\ distinct (leaves (mapOptionTree (@fst _ _) varstypes)) }.
   admit.
   Defined.
@@ -130,8 +131,8 @@ Section HaskProofToStrong.
   Lemma fresh_lemma' Γ 
     : forall types vars Σ ξ lev, Σ = mapOptionTree ξ vars ->
     FreshM { varstypes : _
-      |  mapOptionTree (update_ξ(Γ:=Γ) ξ lev (leaves varstypes)) vars = Σ
-      /\ mapOptionTree (update_ξ       ξ lev (leaves varstypes)) (mapOptionTree (@fst _ _) varstypes) = (types @@@ lev)
+      |  mapOptionTree (update_xi(Γ:=Γ) ξ lev (leaves varstypes)) vars = Σ
+      /\ mapOptionTree (update_xi       ξ lev (leaves varstypes)) (mapOptionTree (@fst _ _) varstypes) = (types @@@ lev)
       /\ distinct (leaves (mapOptionTree (@fst _ _) varstypes)) }.
     induction types.
       intros; destruct a.
@@ -164,7 +165,7 @@ Section HaskProofToStrong.
         intros vars Σ ξ lev pf; refine (bind x2 = IHtypes2 vars Σ ξ lev pf; _).
           apply FreshMon.
           destruct x2 as [vt2 [pf21 [pf22 pfdist]]].
-          refine (bind x1 = IHtypes1 (vars,,(mapOptionTree (@fst _ _) vt2)) (Σ,,(types2@@@lev)) (update_ξ ξ lev
+          refine (bind x1 = IHtypes1 (vars,,(mapOptionTree (@fst _ _) vt2)) (Σ,,(types2@@@lev)) (update_xi ξ lev
             (leaves vt2)) _ _; return _).
           apply FreshMon.
           simpl.
@@ -204,8 +205,8 @@ Section HaskProofToStrong.
   Lemma fresh_lemma Γ ξ vars Σ Σ' lev
     : Σ = mapOptionTree ξ vars ->
     FreshM { vars' : _
-      |  mapOptionTree (update_ξ(Γ:=Γ) ξ lev ((vars',Σ')::nil)) vars = Σ
-      /\ mapOptionTree (update_ξ ξ lev ((vars',Σ')::nil)) [vars'] = [Σ' @@ lev] }.
+      |  mapOptionTree (update_xi(Γ:=Γ) ξ lev ((vars',Σ')::nil)) vars = Σ
+      /\ mapOptionTree (update_xi ξ lev ((vars',Σ')::nil)) [vars'] = [Σ' @@ lev] }.
     intros.
     set (fresh_lemma' Γ [Σ'] vars Σ ξ lev H) as q.
     refine (q >>>= fun q' => return _).
@@ -222,64 +223,64 @@ Section HaskProofToStrong.
       inversion pf2.
     Defined.
 
-  Definition ujudg2exprType Γ (ξ:ExprVarResolver Γ)(Δ:CoercionEnv Γ) Σ τ : Type :=
-    forall vars, Σ = mapOptionTree ξ vars -> FreshM (ITree _ (fun t => Expr Γ Δ ξ t) τ).
+  Definition ujudg2exprType Γ (ξ:ExprVarResolver Γ)(Δ:CoercionEnv Γ) Σ τ l : Type :=
+    forall vars, Σ = mapOptionTree ξ vars -> FreshM (ITree _ (fun t => Expr Γ Δ ξ t l) τ).
 
-  Definition urule2expr  : forall Γ Δ h j t (r:@Arrange _ h j) (ξ:VV -> LeveledHaskType Γ ★),
-    ujudg2exprType Γ ξ Δ h t ->
-    ujudg2exprType Γ ξ Δ j t
+  Definition urule2expr  : forall Γ Δ h j t l (r:@Arrange _ h j) (ξ:VV -> LeveledHaskType Γ ★),
+    ujudg2exprType Γ ξ Δ h t l ->
+    ujudg2exprType Γ ξ Δ j t l
     .
     intros Γ Δ.
-      refine (fix urule2expr h j t (r:@Arrange _ h j) ξ {struct r} : 
-    ujudg2exprType Γ ξ Δ h t ->
-    ujudg2exprType Γ ξ Δ j t :=
+      refine (fix urule2expr h j t l (r:@Arrange _ h j) ξ {struct r} : 
+    ujudg2exprType Γ ξ Δ h t l ->
+    ujudg2exprType Γ ξ Δ j t l :=
         match r as R in Arrange H C return
-    ujudg2exprType Γ ξ Δ H t ->
-    ujudg2exprType Γ ξ Δ C t
+    ujudg2exprType Γ ξ Δ H t l ->
+    ujudg2exprType Γ ξ Δ C t l
  with
-          | RLeft   h c ctx r => let case_RLeft  := tt in (fun e => _) (urule2expr _ _ _ r)
-          | RRight  h c ctx r => let case_RRight := tt in (fun e => _) (urule2expr _ _ _ r)
-          | RId     a       => let case_RId    := tt in _
-          | RCanL   a       => let case_RCanL  := tt in _
-          | RCanR   a       => let case_RCanR  := tt in _
-          | RuCanL  a       => let case_RuCanL := tt in _
-          | RuCanR  a       => let case_RuCanR := tt in _
-          | RAssoc  a b c   => let case_RAssoc := tt in _
-          | RCossa  a b c   => let case_RCossa := tt in _
-          | RExch   a b     => let case_RExch  := tt in _
-          | RWeak   a       => let case_RWeak  := tt in _
-          | RCont   a       => let case_RCont  := tt in _
-          | RComp   a b c f g => let case_RComp  := tt in (fun e1 e2 => _) (urule2expr _ _ _ f) (urule2expr _ _ _ g)
+          | ALeft   h c ctx r => let case_ALeft  := tt in (fun e => _) (urule2expr _ _ _ _ r)
+          | ARight  h c ctx r => let case_ARight := tt in (fun e => _) (urule2expr _ _ _ _ r)
+          | AId     a       => let case_AId    := tt in _
+          | ACanL   a       => let case_ACanL  := tt in _
+          | ACanR   a       => let case_ACanR  := tt in _
+          | AuCanL  a       => let case_AuCanL := tt in _
+          | AuCanR  a       => let case_AuCanR := tt in _
+          | AAssoc  a b c   => let case_AAssoc := tt in _
+          | AuAssoc  a b c   => let case_AuAssoc := tt in _
+          | AExch   a b     => let case_AExch  := tt in _
+          | AWeak   a       => let case_AWeak  := tt in _
+          | ACont   a       => let case_ACont  := tt in _
+          | AComp   a b c f g => let case_AComp  := tt in (fun e1 e2 => _) (urule2expr _ _ _ _ f) (urule2expr _ _ _ _ g)
           end); clear urule2expr; intros.
 
-      destruct case_RId.
+      destruct case_AId.
         apply X.
 
-      destruct case_RCanL.
+      destruct case_ACanL.
         simpl; unfold ujudg2exprType; intros.
         simpl in X.
         apply (X ([],,vars)).
         simpl; rewrite <- H; auto.
 
-      destruct case_RCanR.
+      destruct case_ACanR.
         simpl; unfold ujudg2exprType; intros.
         simpl in X.
         apply (X (vars,,[])).
         simpl; rewrite <- H; auto.
 
-      destruct case_RuCanL.
+      destruct case_AuCanL.
         simpl; unfold ujudg2exprType; intros.
         destruct vars; try destruct o; inversion H.
         simpl in X.
         apply (X vars2); auto.
 
-      destruct case_RuCanR.
+      destruct case_AuCanR.
         simpl; unfold ujudg2exprType; intros.
         destruct vars; try destruct o; inversion H.
         simpl in X.
         apply (X vars1); auto.
 
-      destruct case_RAssoc.
+      destruct case_AAssoc.
         simpl; unfold ujudg2exprType; intros.
         simpl in X.
         destruct vars; try destruct o; inversion H.
@@ -287,7 +288,7 @@ Section HaskProofToStrong.
         apply (X (vars1_1,,(vars1_2,,vars2))).
         subst; auto.
 
-      destruct case_RCossa.
+      destruct case_AuAssoc.
         simpl; unfold ujudg2exprType; intros.
         simpl in X.
         destruct vars; try destruct o; inversion H.
@@ -295,20 +296,20 @@ Section HaskProofToStrong.
         apply (X ((vars1,,vars2_1),,vars2_2)).
         subst; auto.
 
-      destruct case_RExch.
+      destruct case_AExch.
         simpl; unfold ujudg2exprType ; intros.
         simpl in X.
         destruct vars; try destruct o; inversion H.
         apply (X (vars2,,vars1)).
         inversion H; subst; auto.
         
-      destruct case_RWeak.
+      destruct case_AWeak.
         simpl; unfold ujudg2exprType; intros.
         simpl in X.
         apply (X []).
         auto.
         
-      destruct case_RCont.
+      destruct case_ACont.
         simpl; unfold ujudg2exprType ; intros.
         simpl in X.
         apply (X (vars,,vars)).
@@ -316,7 +317,7 @@ Section HaskProofToStrong.
         rewrite <- H.
         auto.
 
-      destruct case_RLeft.
+      destruct case_ALeft.
         intro vars; unfold ujudg2exprType; intro H.
         destruct vars; try destruct o; inversion H.
         apply (fun q => e ξ q vars2 H2).
@@ -331,7 +332,7 @@ Section HaskProofToStrong.
           simpl.
           reflexivity.
 
-      destruct case_RRight.
+      destruct case_ARight.
         intro vars; unfold ujudg2exprType; intro H.
         destruct vars; try destruct o; inversion H.
         apply (fun q => e ξ q vars1 H1).
@@ -346,16 +347,16 @@ Section HaskProofToStrong.
           simpl.
           reflexivity.
 
-      destruct case_RComp.
+      destruct case_AComp.
         apply e2.
         apply e1.
         apply X.
         Defined.
 
   Definition letrec_helper Γ Δ l (varstypes:Tree ??(VV * HaskType Γ ★)) ξ' :
-    ITree (LeveledHaskType Γ ★)
-         (fun t : LeveledHaskType Γ ★ => Expr Γ Δ ξ' t)
-         (mapOptionTree (ξ' ○ (@fst _ _)) varstypes)
+    ITree (HaskType Γ ★)
+         (fun t : HaskType Γ ★ => Expr Γ Δ ξ' t l)
+         (mapOptionTree (unlev ○ ξ' ○ (@fst _ _)) varstypes)
          -> ELetRecBindings Γ Δ ξ' l varstypes.
     intros.
     induction varstypes.
@@ -371,6 +372,8 @@ Section HaskProofToStrong.
       simpl.
       destruct (eqd_dec h0 l).
         rewrite <- e0.
+        simpl in X.
+        subst.
         apply X.
       apply (Prelude_error "level mismatch; should never happen").
       apply (Prelude_error "letrec type mismatch; should never happen").
@@ -419,7 +422,8 @@ Section HaskProofToStrong.
      prod (judg2exprType (pcb_judg (projT2 pcb))) {vars' : Tree ??VV & pcb_freevars (projT2 pcb) = mapOptionTree ξ vars'} ->
      ((fun sac => FreshM
        { scb : StrongCaseBranchWithVVs VV eqdec_vv tc avars sac
-         & Expr (sac_Γ sac Γ) (sac_Δ sac Γ avars (weakCK'' Δ)) (scbwv_ξ scb ξ lev) (weakLT' (tbranches @@  lev)) }) (projT1 pcb)).
+         & Expr (sac_gamma sac Γ) (sac_delta sac Γ avars (weakCK'' Δ)) (scbwv_xi scb ξ lev)
+         (weakT' tbranches) (weakL' lev) }) (projT1 pcb)).
     intro pcb.
     intro X.
     simpl in X.
@@ -445,10 +449,10 @@ Section HaskProofToStrong.
     cut (distinct (vec2list localvars'')). intro H'''.
     set (@Build_StrongCaseBranchWithVVs _ _ _ _ avars sac localvars'' H''') as scb.
 
-    refine (bind q = (f (scbwv_ξ scb ξ lev) (vars,,(unleaves (vec2list (scbwv_exprvars scb)))) _) ; return _).
+    refine (bind q = (f (scbwv_xi scb ξ lev) (vars,,(unleaves (vec2list (scbwv_exprvars scb)))) _) ; return _).
       apply FreshMon.
       simpl.
-      unfold scbwv_ξ.
+      unfold scbwv_xi.
       rewrite vars_pf.
       rewrite <- mapOptionTree_compose.
       clear localvars_pf1.
@@ -511,7 +515,7 @@ Section HaskProofToStrong.
     intros h j r.
 
       refine (match r as R in Rule H C return ITree _ judg2exprType H -> ITree _ judg2exprType C with
-      | RArrange a b c d e  r         => let case_RURule := tt        in _
+      | RArrange a b c d e l r        => let case_RURule := tt        in _
       | RNote   Γ Δ Σ τ l n           => let case_RNote := tt         in _
       | RLit    Γ Δ l     _           => let case_RLit := tt          in _
       | RVar    Γ Δ σ         p       => let case_RVar := tt          in _
@@ -525,8 +529,8 @@ Section HaskProofToStrong.
       | RApp    Γ Δ Σ₁ Σ₂ tx te p     => let case_RApp := tt          in _
       | RLet    Γ Δ Σ₁ Σ₂ σ₁ σ₂ p     => let case_RLet := tt          in _
       | RWhere  Γ Δ Σ₁ Σ₂ Σ₃ σ₁ σ₂ p  => let case_RWhere := tt          in _
-      | RJoin   Γ p lri m x q         => let case_RJoin := tt in _
-      | RVoid   _ _                   => let case_RVoid := tt   in _
+      | RJoin   Γ p lri m x q l       => let case_RJoin := tt in _
+      | RVoid   _ _ l                 => let case_RVoid := tt   in _
       | RBrak   Σ a b c n m           => let case_RBrak := tt         in _
       | REsc    Σ a b c n m           => let case_REsc := tt          in _
       | RCase   Γ Δ lev tc Σ avars tbranches alts => let case_RCase := tt         in _
@@ -535,12 +539,10 @@ Section HaskProofToStrong.
 
     destruct case_RURule.
       apply ILeaf. simpl. intros.
-      set (@urule2expr a b _ _ e r0 ξ) as q.
-      set (fun z => q z) as q'.
-      simpl in q'.
-      apply q' with (vars:=vars).
-      clear q' q.
+      set (@urule2expr a b _ _ e l r0 ξ) as q.
       unfold ujudg2exprType.
+      unfold ujudg2exprType in q.
+      apply q with (vars:=vars).
       intros.
       apply X_ with (vars:=vars0).
       auto.
@@ -567,8 +569,11 @@ Section HaskProofToStrong.
 
   destruct case_RVar.
     apply ILeaf; simpl; intros; refine (return ILeaf _ _).
-    destruct vars; simpl in H; inversion H; destruct o. inversion H1. rewrite H2.
-    apply EVar.
+    destruct vars; simpl in H; inversion H; destruct o. inversion H1.
+    set (@EVar _ _ _ Δ ξ v) as q.
+    rewrite <- H2 in q.
+    simpl in q.
+    apply q.
     inversion H.
 
   destruct case_RGlobal.
@@ -581,7 +586,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_xi ξ x (((vnew, tx  )) :: nil)) as ξ' in *.
     refine (X_ ξ' (vars,,[vnew]) _ >>>= _).
     apply FreshMon.
     simpl.
@@ -648,7 +653,7 @@ Section HaskProofToStrong.
     apply FreshMon.
 
     destruct pf as [ vnew [ pf1 pf2 ]].
-    set (update_ξ ξ p (((vnew, σ₁ )) :: nil)) as ξ' in *.
+    set (update_xi ξ p (((vnew, σ₁ )) :: nil)) as ξ' in *.
     inversion X_.
     apply ileaf in X.
     apply ileaf in X0.
@@ -687,7 +692,7 @@ Section HaskProofToStrong.
     apply FreshMon.
 
     destruct pf as [ vnew [ pf1 pf2 ]].
-    set (update_ξ ξ p (((vnew, σ₁ )) :: nil)) as ξ' in *.
+    set (update_xi ξ p (((vnew, σ₁ )) :: nil)) as ξ' in *.
     inversion X_.
     apply ileaf in X.
     apply ileaf in X0.
@@ -751,7 +756,7 @@ Section HaskProofToStrong.
     apply ILeaf; simpl; intros.
     refine (bind ξvars = fresh_lemma' _ y _ _ _ t H; _). apply FreshMon.
     destruct ξvars as [ varstypes [ pf1[ pf2 pfdist]]].
-    refine (X_ ((update_ξ ξ t (leaves varstypes)))
+    refine (X_ ((update_xi ξ t (leaves varstypes)))
       (vars,,(mapOptionTree (@fst _ _) varstypes)) _ >>>= fun X => return _); clear X_.  apply FreshMon.
     simpl.
     rewrite pf2.
@@ -763,10 +768,18 @@ Section HaskProofToStrong.
     apply (@ELetRec _ _ _ _ _ _ _ varstypes).
     auto.
     apply (@letrec_helper Γ Δ t varstypes).
-    rewrite <- pf2 in X0.
     rewrite mapOptionTree_compose.
-    apply X0.
+    rewrite mapOptionTree_compose.
+    rewrite pf2.
+    replace ((mapOptionTree unlev (y @@@ t))) with y.
+      apply X0.
+      clear pf1 X0 X1 pfdist pf2 vars varstypes.
+      induction y; try destruct a; auto.
+      rewrite IHy1 at 1.
+      rewrite IHy2 at 1.
+      reflexivity.
     apply ileaf in X1.
+    simpl in X1.
     apply X1.
 
   destruct case_RCase.
@@ -824,7 +837,7 @@ Section HaskProofToStrong.
     clear q.
     destruct q' as [varstypes [pf1 [pf2 distpf]]].
     exists (mapOptionTree (@fst _ _) varstypes).
-    exists (update_ξ ξ l (leaves varstypes)).
+    exists (update_xi ξ l (leaves varstypes)).
     symmetry; auto.
     refine (return _).
     exists [].
@@ -844,9 +857,9 @@ Section HaskProofToStrong.
     admit.
     Defined.
 
-  Definition proof2expr Γ Δ τ Σ (ξ0: VV -> LeveledHaskType Γ ★)
-    {zz:ToString VV} : ND Rule [] [Γ > Δ > Σ |- [τ]] ->
-    FreshM (???{ ξ : _ & Expr Γ Δ ξ τ}).
+  Definition proof2expr Γ Δ τ l Σ (ξ0: VV -> LeveledHaskType Γ ★)
+    {zz:ToString VV} : ND Rule [] [Γ > Δ > Σ |- [τ] @ l] ->
+    FreshM (???{ ξ : _ & Expr Γ Δ ξ τ l}).
     intro pf.
     set (mkSIND systemfc_all_rules_one_conclusion _ _ _ pf (scnd_weak [])) as cnd.
     apply closed2expr in cnd.
@@ -862,7 +875,9 @@ Section HaskProofToStrong.
     auto.
     refine (return OK _).
     exists ξ.
-    apply (ileaf it).
+    apply ileaf in it.
+    simpl in it.
+    apply it.
     apply INone.
     Defined.