some progress with Map.Equals

kth-step · Mar 15, 2024 · 13fbef9 · 13fbef9
1 parent 8055c81
commit 13fbef9
Showing 1 changed file with 67 additions and 22 deletions.
diff --git a/theories/abs_functional_metatheory.v b/theories/abs_functional_metatheory.v
@@ -428,6 +428,46 @@ Proof.
   }
 Qed.
 
+Lemma typ_e_G_Equal_equiv_imp : 
+ forall G1 G2 e T, Map.Equal G1 G2 -> typ_e G1 e T -> typ_e G2 e T.
+Proof.
+intros G1 G2 e0 T0 Heq.
+intros Ht.
+induction Ht.
+- apply typ_bool.
+- apply typ_int.
+- apply typ_var.
+  symmetry in Heq.
+  rewrite <- H.
+  apply Heq.
+- apply typ_func_expr.
+  * intros.
+    apply H0; auto.
+  * rewrite <- H1.
+    symmetry in Heq.
+    apply Heq.
+Qed.
+
+Lemma typ_e_G_Equal_equiv : 
+ forall G1 G2 e T, Map.Equal G1 G2 -> (typ_e G1 e T <-> typ_e G2 e T).
+Proof.
+intros G1 G2 e0 T0 Heq; split; apply typ_e_G_Equal_equiv_imp; auto.
+symmetry; assumption.
+Qed.
+
+
+
+Lemma fold_map5 {A X Y Z W: Type}: forall (f : _ -> _ -> A -> A) (l: list (X*Y*Z*W)) a0,
+    fold_right (fun '(z, _, _, w) a => f z w a) a0 l =
+      fold_right (fun '(z, w) a => f z w a) a0
+        (map (fun '(z, _, _, w) => (z, w)) l).
+Proof.
+  induction l; intros; eauto.
+  destruct a as [[[? ?] ?] ?].
+  simpl.
+  now rewrite IHl.
+Qed.
+
 Lemma subst_lemma: forall (T_x_t_y_list:list (T*x*t*x)) G0 e0 A,
   typ_e (fold_right (fun '(Ai, x_, _, _) (G0 : G) => Map.add x_ (ctxv_T Ai) G0) G0 T_x_t_y_list) e0 A ->
   NoDup (map (fun '(_, _, _, y) => y) T_x_t_y_list) ->
@@ -463,13 +503,34 @@ Proof.
         now intros (((?, ?), ?), ?).
       - now left.
     }
-    replace (Map.add x_ (ctxv_T T_) (fold_right (fun '(Ai, x_, _, _) (G0 : G) => Map.add x_ (ctxv_T Ai) G0) G0 T_x_t_y_list))
-      with (fold_right (fun '(Ai, x_, _, _) (G0 : G) => Map.add x_ (ctxv_T Ai) G0) (Map.add x_ (ctxv_T T_) G0) T_x_t_y_list)
-      in H.
+    assert (Map.Equal
+     (Map.add x_ (ctxv_T T_) (fold_right (fun '(Ai, x_0, _, _) (G0 : G) => Map.add x_0 (ctxv_T Ai) G0) G0 T_x_t_y_list))
+     (fold_right (fun '(Ai, x_, _, _) (G0 : G) => Map.add x_ (ctxv_T Ai) G0) (Map.add x_ (ctxv_T T_) G0) T_x_t_y_list))
+      as HMEqualx.
+    {
+      (*
+      epose proof fold_add_comm G0 x_ T_ (map (fun '(Ai, x1, _, _) => (Ai, x1)) T_x_t_y_list).
+      rewrite 2 fold_map5.
+      assumption.
+      *)
+      admit.
+    }
+    assert (Map.Equal
+     (fold_right (fun '(Ai, _, _, y) (G0 : G) => Map.add y (ctxv_T Ai) G0) (Map.add x_ (ctxv_T T_) G0) T_x_t_y_list)
+     (Map.add x_ (ctxv_T T_) (fold_right (fun '(Ai, _, _, y) (G0 : G) => Map.add y (ctxv_T Ai) G0) G0 T_x_t_y_list)))
+      as HMEqualy.
+    {
+      epose proof fold_add_comm G0 x_ T_ (map (fun '(Ai, _, _, y1) => (Ai, y1)) T_x_t_y_list) H9.
+      rewrite fold_map5.
+      set (fd := fold_right _ _ _).
+      rewrite fold_map5.
+      unfold fd; clear fd.
+      symmetry.
+      assumption.
+    }
+    apply (typ_e_G_Equal_equiv _ _ _ _ HMEqualx) in H.
     pose proof IHT_x_t_y_list H7 H8 H4 _ H1 _ H as IH.
-    replace (fold_right (fun '(Ai, _, _, y) (G0 : G) => Map.add y (ctxv_T Ai) G0) (Map.add x_ (ctxv_T T_) G0) T_x_t_y_list)
-      with (Map.add x_ (ctxv_T T_) (fold_right (fun '(Ai, _, _, y) (G0 : G) => Map.add y (ctxv_T Ai) G0) G0 T_x_t_y_list))
-      in IH.
+    apply (typ_e_G_Equal_equiv _ _ _ _ HMEqualy) in IH.
     assert (fresh_vars_e [y] (e_var_subst e0 (map (fun '(_, x_, _, y_) => (x_, y_)) T_x_t_y_list))).
     {
       assert (map snd (map (fun '(_, x_0, _, y_) => (x_0, y_)) T_x_t_y_list) = map (fun '(_, _, _, y) => y) T_x_t_y_list).
@@ -481,22 +542,6 @@ Proof.
       apply fresh_var_subst; try rewrite H10; auto.
     }
     now apply (subst_lemma_one _ _ _ _ _ _ IH H10).
-
-    (* resolving those replaces from earlier *)
-    {
-      epose proof fold_add_comm G0 x_ T_ (map (fun '(Ai, _, _, y1) => (Ai, y1)) T_x_t_y_list) H9.
-      rewrite 2 fold_map1.
-      Fail apply H10.
-      (* why? *)
-      admit.
-    }
-    {
-      epose proof fold_add_comm G0 x_ T_ (map (fun '(Ai, _, _, y1) => (Ai, y1)) T_x_t_y_list) H9.
-      rewrite 2 fold_map2.
-      Fail rewrite <- H10.
-      (* why? *)
-      admit.
-    }
 Admitted.
 
 Lemma type_preservation : forall (Flist : list F) (G5 : G) (s5 : s),