Various application lemmas

4 files changed, 81 insertions, 8 deletions

diff --git a/src/Reflection/Application.v b/src/Reflection/Application.v
index b49752c99..3ddb25e1f 100644
--- a/src/Reflection/Application.v
+++ b/src/Reflection/Application.v
@@ -160,17 +160,23 @@ Section language.
        | S n' => @ApplyInterped' n' t x
        end.
 
-  Fixpoint ApplyInterpedAll {t}
+  Fixpoint ApplyInterpedAll' {t}
     : forall  (x : interp_type interp_base_type t)
-              (args : interp_all_binders_for t interp_base_type),
+              (args : interp_all_binders_for' t interp_base_type),
       interp_flat_type interp_base_type (remove_all_binders t)
     := match t return (forall (x : interp_type _ t)
-                              (args : interp_all_binders_for t _),
+                              (args : interp_all_binders_for' t _),
                           interp_flat_type _ (remove_all_binders t))
        with
        | Tflat _ => fun x _ => x
-       | Arrow A B => fun f x => @ApplyInterpedAll B (f (fst_binder x)) (snd_binder x)
+       | Arrow A B => fun f x => @ApplyInterpedAll' B (f (fst x)) (snd x)
        end.
+
+  Definition ApplyInterpedAll {t}
+             (x : interp_type interp_base_type t)
+             (args : interp_all_binders_for t interp_base_type)
+    : interp_flat_type interp_base_type (remove_all_binders t)
+    := ApplyInterpedAll' x (interp_all_binders_for_to' _ _ args).
 End language.
 
 Arguments all_binders_for {_} !_ / .
@@ -185,4 +191,5 @@ Arguments Apply {_ _ _ _ _ _} _ _ , {_ _ _} _ {_ _} _ _.
 Arguments Apply _ _ _ !_ _ _ !_ !_ / .
 Arguments ApplyInterped {_ _ !_ !_} _ _ / .
 Arguments ApplyAll {_ _ _ _ !_} !_ _ / .
+Arguments ApplyInterpedAll' {_ _ !_} _ _ / .
 Arguments ApplyInterpedAll {_ _ !_} _ _ / .
diff --git a/src/Reflection/ApplicationLemmas.v b/src/Reflection/ApplicationLemmas.v
index aa589f889..9303ed378 100644
--- a/src/Reflection/ApplicationLemmas.v
+++ b/src/Reflection/ApplicationLemmas.v
@@ -27,12 +27,78 @@ Section language.
     apply interp_apply'.
   Qed.
 
+  Lemma fst_interp_all_binders_for_of' {A B}
+        (args : interp_all_binders_for' (Arrow A B) interp_base_type)
+    : fst_binder (interp_all_binders_for_of' args) = fst args.
+  Proof.
+    destruct B; reflexivity.
+  Qed.
+
+  Lemma snd_interp_all_binders_for_of' {A B}
+        (args : interp_all_binders_for' (Arrow A B) interp_base_type)
+    : snd_binder (interp_all_binders_for_of' args) = interp_all_binders_for_of' (snd args).
+  Proof.
+    destruct B.
+    { edestruct interp_all_binders_for_of'; reflexivity. }
+    { destruct args; reflexivity. }
+  Qed.
+
+  Lemma fst_interp_all_binders_for_to' {A B}
+        (args : interp_all_binders_for (Arrow A B) interp_base_type)
+    : fst (interp_all_binders_for_to' args) = fst_binder args.
+  Proof.
+    destruct B; reflexivity.
+  Qed.
+
+  Lemma snd_interp_all_binders_for_to' {A B}
+        (args : interp_all_binders_for (Arrow A B) interp_base_type)
+    : snd (interp_all_binders_for_to' args) = interp_all_binders_for_to' (snd_binder args).
+  Proof.
+    destruct B; reflexivity.
+  Qed.
+
+  Lemma interp_all_binders_for_to'_of' {t} (args : interp_all_binders_for' t interp_base_type)
+    : interp_all_binders_for_to' (interp_all_binders_for_of' args) = args.
+  Proof.
+    induction t; destruct args; [ reflexivity | ].
+    apply injective_projections;
+      [ rewrite fst_interp_all_binders_for_to', fst_interp_all_binders_for_of'; reflexivity
+      | rewrite snd_interp_all_binders_for_to', snd_interp_all_binders_for_of', IHt; reflexivity ].
+  Qed.
+
+  Lemma interp_all_binders_for_of'_to' {t} (args : interp_all_binders_for t interp_base_type)
+    : interp_all_binders_for_of' (interp_all_binders_for_to' args) = args.
+  Proof.
+    induction t as [|A B IHt].
+    { destruct args; reflexivity. }
+    { destruct B; [ reflexivity | ].
+      destruct args; simpl; rewrite IHt; reflexivity. }
+  Qed.
+
+  Lemma interp_apply_all' {t}
+        (x : @expr base_type interp_base_type op _ t)
+        (args : interp_all_binders_for' t interp_base_type)
+    : interp interp_op (ApplyAll x (interp_all_binders_for_of' args)) = ApplyInterpedAll' (interp interp_op x) args.
+  Proof.
+    induction x as [|?? x IHx]; [ reflexivity | ].
+    simpl; rewrite <- IHx; destruct args.
+    rewrite snd_interp_all_binders_for_of', fst_interp_all_binders_for_of'; reflexivity.
+  Qed.
+
   Lemma interp_apply_all {t}
         (x : @expr base_type interp_base_type op _ t)
         (args : interp_all_binders_for t interp_base_type)
     : interp interp_op (ApplyAll x args) = ApplyInterpedAll (interp interp_op x) args.
   Proof.
-    induction x as [|?? x IHx]; [ reflexivity | ].
-    simpl; rewrite <- IHx; reflexivity.
+    unfold ApplyInterpedAll.
+    rewrite <- interp_apply_all', interp_all_binders_for_of'_to'; reflexivity.
   Qed.
+
+  Lemma interp_apply_all_to' {t}
+         (x : @expr base_type interp_base_type op _ t)
+         (args : interp_all_binders_for t interp_base_type)
+    : interp interp_op (ApplyAll x args) = ApplyInterpedAll' (interp interp_op x) (interp_all_binders_for_to' args).
+   Proof.
+    rewrite <- interp_apply_all', interp_all_binders_for_of'_to'; reflexivity.
+   Qed.
 End language.
diff --git a/src/Reflection/Z/Interpretations128/RelationsCombinations.v b/src/Reflection/Z/Interpretations128/RelationsCombinations.v
index 4fde4d69c..64c0fceb1 100644
--- a/src/Reflection/Z/Interpretations128/RelationsCombinations.v
+++ b/src/Reflection/Z/Interpretations128/RelationsCombinations.v
@@ -37,7 +37,7 @@ Module Relations.
         { reflexivity. }
         { setoid_rewrite IHt; clear IHt.
           split; intro H; intros.
-          { simpl in *; intuition. }
+          { destruct_head_hnf' prod; simpl in *; intuition. }
           { eapply (H (_, _) (_, _)); simpl in *; intuition. } } }
     Qed.
   End lift.
diff --git a/src/Reflection/Z/Interpretations64/RelationsCombinations.v b/src/Reflection/Z/Interpretations64/RelationsCombinations.v
index b1287c7a7..ecb65591b 100644
--- a/src/Reflection/Z/Interpretations64/RelationsCombinations.v
+++ b/src/Reflection/Z/Interpretations64/RelationsCombinations.v
@@ -37,7 +37,7 @@ Module Relations.
         { reflexivity. }
         { setoid_rewrite IHt; clear IHt.
           split; intro H; intros.
-          { simpl in *; intuition. }
+          { destruct_head_hnf' prod; simpl in *; intuition. }
           { eapply (H (_, _) (_, _)); simpl in *; intuition. } } }
     Qed.
   End lift.