add an identity production for Arrange

diff --git a/src/HaskProof.v b/src/HaskProof.v
index ee536b0..d9c6a7e 100644 (file)
--- a/src/HaskProof.v
+++ b/src/HaskProof.v
@@ -45,6 +45,7 @@ Implicit Arguments ProofCaseBranch [ ].
 
 (* Figure 3, production $\vdash_E$, Uniform rules *)
 Inductive Arrange {T} : Tree ??T -> Tree ??T -> Type :=
 
 (* Figure 3, production $\vdash_E$, Uniform rules *)
 Inductive Arrange {T} : Tree ??T -> Tree ??T -> Type :=

+| RId     : forall a        ,                Arrange           a                  a

 | RCanL   : forall a        ,                Arrange  (    [],,a   )      (       a   )
 | RCanR   : forall a        ,                Arrange  (    a,,[]   )      (       a   )
 | RuCanL  : forall a        ,                Arrange  (       a    )      (  [],,a    )
 | RCanL   : forall a        ,                Arrange  (    [],,a   )      (       a   )
 | RCanR   : forall a        ,                Arrange  (    a,,[]   )      (       a   )
 | RuCanL  : forall a        ,                Arrange  (       a    )      (  [],,a    )

@@ -176,6 +177,7 @@ Definition arrangeMap :
     Arrange (mapOptionTree f Σ₁) (mapOptionTree f Σ₂).
   intros.
   induction X; simpl.
     Arrange (mapOptionTree f Σ₁) (mapOptionTree f Σ₂).
   intros.
   induction X; simpl.

+  apply RId.

   apply RCanL.
   apply RCanR.
   apply RuCanL.
   apply RCanL.
   apply RCanR.
   apply RuCanL.

diff --git a/src/HaskProofToLatex.v b/src/HaskProofToLatex.v
index d35a870..61b358f 100644 (file)
--- a/src/HaskProofToLatex.v
+++ b/src/HaskProofToLatex.v
@@ -161,6 +161,7 @@ Fixpoint nd_uruleToRawLatexMath {T}{h}{c}(r:@Arrange T h c) : string :=
   match r with
     | RLeft   _ _ _ r => nd_uruleToRawLatexMath r
     | RRight  _ _ _ r => nd_uruleToRawLatexMath r
   match r with
     | RLeft   _ _ _ r => nd_uruleToRawLatexMath r
     | RRight  _ _ _ r => nd_uruleToRawLatexMath r

+    | RId     _     => "Id"

     | RCanL   _     => "CanL"
     | RCanR   _     => "CanR"
     | RuCanL  _     => "uCanL"
     | RCanL   _     => "CanL"
     | RCanR   _     => "CanR"
     | RuCanL  _     => "uCanL"

diff --git a/src/HaskProofToStrong.v b/src/HaskProofToStrong.v
index 19f2f62..b6e8efe 100644 (file)
--- a/src/HaskProofToStrong.v
+++ b/src/HaskProofToStrong.v
@@ -239,6 +239,7 @@ Section HaskProofToStrong.
  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)
  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 _
           | RCanL   a       => let case_RCanL  := tt in _
           | RCanR   a       => let case_RCanR  := tt in _
           | RuCanL  a       => let case_RuCanL := tt in _

@@ -251,6 +252,9 @@ Section HaskProofToStrong.
           | RComp   a b c f g => let case_RComp  := tt in (fun e1 e2 => _) (urule2expr _ _ _ f) (urule2expr _ _ _ g)
           end); clear urule2expr; intros.
 
           | RComp   a b c f g => let case_RComp  := tt in (fun e1 e2 => _) (urule2expr _ _ _ f) (urule2expr _ _ _ g)
           end); clear urule2expr; intros.
 

+      destruct case_RId.
+        apply X.
+

       destruct case_RCanL.
         simpl; unfold ujudg2exprType; intros.
         simpl in X.
       destruct case_RCanL.
         simpl; unfold ujudg2exprType; intros.
         simpl in X.