swap order of hypotheses in RApp to match RLet

diff --git a/src/ExtractionMain.v b/src/ExtractionMain.v
index 3cd8ff6..e4281d7 100644 (file)
--- a/src/ExtractionMain.v
+++ b/src/ExtractionMain.v
@@ -236,12 +236,13 @@ Section core2proof.
     ND Rule 
        [ Γ > Δ > Σ             |- [a ---> s @@ lev ] ]
        [ Γ > Δ > Σ,,[a @@ lev] |-       [ s @@ lev ] ].
     ND Rule 
        [ Γ > Δ > Σ             |- [a ---> s @@ lev ] ]
        [ Γ > Δ > Σ,,[a @@ lev] |-       [ s @@ lev ] ].

-    eapply nd_comp; [ idtac | eapply nd_rule; apply (@RApp Γ Δ Σ [a@@lev] a s lev) ].
-    eapply nd_comp; [ apply nd_rlecnac | idtac ].
-    apply nd_prod.    
-    apply nd_id.
+    eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RExch ].
+    eapply nd_comp; [ idtac | eapply nd_rule; apply (@RApp Γ Δ [a@@lev] Σ a s lev) ].
+    eapply nd_comp; [ apply nd_llecnac | idtac ].
+    apply nd_prod.

     apply nd_rule.
     apply RVar.
     apply nd_rule.
     apply RVar.

+    apply nd_id.

     Defined.
 
   Definition fToC1 {Γ}{Δ}{a}{s}{lev} :
     Defined.
 
   Definition fToC1 {Γ}{Δ}{a}{s}{lev} :

diff --git a/src/HaskProof.v b/src/HaskProof.v
index d28db62..ee536b0 100644 (file)
--- a/src/HaskProof.v
+++ b/src/HaskProof.v
@@ -81,7 +81,7 @@ Inductive Rule : Tree ??Judg -> Tree ??Judg -> Type :=
 
 | RJoin  : ∀ Γ Δ Σ₁ Σ₂ τ₁ τ₂ ,   Rule ([Γ > Δ > Σ₁ |- τ₁ ],,[Γ > Δ > Σ₂ |- τ₂ ])         [Γ>Δ>  Σ₁,,Σ₂  |- τ₁,,τ₂          ]
 
 
 | RJoin  : ∀ Γ Δ Σ₁ Σ₂ τ₁ τ₂ ,   Rule ([Γ > Δ > Σ₁ |- τ₁ ],,[Γ > Δ > Σ₂ |- τ₂ ])         [Γ>Δ>  Σ₁,,Σ₂  |- τ₁,,τ₂          ]
 

-| RApp           : ∀ Γ Δ Σ₁ Σ₂ tx te l,  Rule ([Γ>Δ> Σ₁       |- [tx--->te @@l]],,[Γ>Δ> Σ₂ |- [tx@@l]])  [Γ>Δ> Σ₁,,Σ₂ |- [te   @@l]]
+| RApp           : ∀ Γ Δ Σ₁ Σ₂ tx te l,  Rule ([Γ>Δ> Σ₁ |- [tx@@l]],,[Γ>Δ> Σ₂       |- [tx--->te @@l]])  [Γ>Δ> Σ₁,,Σ₂ |- [te   @@l]]

 
 | RLet           : ∀ Γ Δ Σ₁ Σ₂ σ₁ σ₂ l,  Rule ([Γ>Δ> Σ₂ |- [σ₂@@l]],,[Γ>Δ> Σ₁,,[σ₂@@l] |- [σ₁@@l] ])     [Γ>Δ> Σ₁,,Σ₂ |- [σ₁   @@l]]
 
 
 | RLet           : ∀ Γ Δ Σ₁ Σ₂ σ₁ σ₂ l,  Rule ([Γ>Δ> Σ₂ |- [σ₂@@l]],,[Γ>Δ> Σ₁,,[σ₂@@l] |- [σ₁@@l] ])     [Γ>Δ> Σ₁,,Σ₂ |- [σ₁   @@l]]
 

diff --git a/src/HaskProofToStrong.v b/src/HaskProofToStrong.v
index b14a53e..19f2f62 100644 (file)
--- a/src/HaskProofToStrong.v
+++ b/src/HaskProofToStrong.v
@@ -632,7 +632,7 @@ Section HaskProofToStrong.
     apply ileaf in q1'.
     apply ileaf in q2'.
     simpl in *.
     apply ileaf in q1'.
     apply ileaf in q2'.
     simpl in *.

-    apply (EApp _ _ _ _ _ _ q1' q2').
+    apply (EApp _ _ _ _ _ _ q2' q1').

 
   destruct case_RLet.
     apply ILeaf.
 
   destruct case_RLet.
     apply ILeaf.

diff --git a/src/HaskStrongToProof.v b/src/HaskStrongToProof.v
index 8cd5688..9c3b041 100644 (file)
--- a/src/HaskStrongToProof.v
+++ b/src/HaskStrongToProof.v
@@ -522,7 +522,7 @@ Fixpoint expr2antecedent {Γ'}{Δ'}{ξ'}{τ'}(exp:Expr Γ' Δ' ξ' τ') : Tree ?
   | EGlobal  Γ Δ ξ _ _ _                          => []
   | EVar     Γ Δ ξ ev                             => [ev]
   | ELit     Γ Δ ξ lit lev                        => []
   | EGlobal  Γ Δ ξ _ _ _                          => []
   | EVar     Γ Δ ξ ev                             => [ev]
   | ELit     Γ Δ ξ lit lev                        => []

-  | EApp     Γ Δ ξ t1 t2 lev e1 e2                => (expr2antecedent e1),,(expr2antecedent e2)
+  | EApp     Γ Δ ξ t1 t2 lev e1 e2                => (expr2antecedent e2),,(expr2antecedent e1)

   | ELam     Γ Δ ξ t1 t2 lev v    e               => stripOutVars (v::nil) (expr2antecedent e)
   | ELet     Γ Δ ξ tv t  lev v ev ebody           => ((stripOutVars (v::nil) (expr2antecedent ebody)),,(expr2antecedent ev))
   | EEsc     Γ Δ ξ ec t lev e                     => expr2antecedent e
   | ELam     Γ Δ ξ t1 t2 lev v    e               => stripOutVars (v::nil) (expr2antecedent e)
   | ELet     Γ Δ ξ tv t  lev v ev ebody           => ((stripOutVars (v::nil) (expr2antecedent ebody)),,(expr2antecedent ev))
   | EEsc     Γ Δ ξ ec t lev e                     => expr2antecedent e

@@ -997,11 +997,11 @@ Definition expr2proof  :
 
     destruct case_EApp.
       unfold mapOptionTree; simpl; fold (mapOptionTree ξ).
 
     destruct case_EApp.
       unfold mapOptionTree; simpl; fold (mapOptionTree ξ).

-      eapply nd_comp; [ idtac | eapply nd_rule; apply RApp ].
+      eapply nd_comp; [ idtac
+        | eapply nd_rule;
+          apply (@RApp _ _ _ _ t2 t1) ].

       eapply nd_comp; [ apply nd_llecnac | idtac ].
       apply nd_prod; auto.
       eapply nd_comp; [ apply nd_llecnac | idtac ].
       apply nd_prod; auto.

-      apply e1'.
-      apply e2'.

 
     destruct case_ELam; intros.
       unfold mapOptionTree; simpl; fold (mapOptionTree ξ).
 
     destruct case_ELam; intros.
       unfold mapOptionTree; simpl; fold (mapOptionTree ξ).