Fix App_Lam rule in bidir

CakeML · Oct 5, 2023 · 05de3cc · 05de3cc
1 parent 09dad92
commit 05de3cc
Show file tree

Hide file tree

Showing 2 changed files with 58 additions and 49 deletions.
diff --git a/compiler/backend/languages/relations/pure_presScript.sml b/compiler/backend/languages/relations/pure_presScript.sml
@@ -16,7 +16,6 @@ open pure_expTheory pure_valueTheory pure_evalTheory pure_eval_lemmasTheory
      pure_tcexpTheory pure_tcexp_lemmasTheory
      pure_typingTheory pure_typingPropsTheory;
 
-
 val exp_of_def = pureLangTheory.exp_of_def;
 val rows_of_def = pureLangTheory.rows_of_def;
 val lets_for_def = pureLangTheory.lets_for_def;
@@ -155,9 +154,11 @@ Inductive bidir:
   (* typing: => direction proved
              <= direction has mismatching free variables *)
 [~App_Lam:]
-  (∀a b c vs x.
-    bidir (App a (Lam b vs x) (MAP (Var c) vs))
-          x) ∧
+  (∀a b c vs x ws.
+    set vs ⊆ set ws ∧ vs ≠ []
+    ⇒
+    bidir (Lam a ws (App b (Lam c vs x) (MAP (Var d) vs)))
+          (Lam a ws x)) ∧
 [~Letrec_Lam:]
   (∀a b c d vs l e.
     EVERY (λ(v,e). DISJOINT (IMAGE explode (set vs)) (freevars (exp_of e)) ∧
@@ -361,7 +362,6 @@ Proof
   >~ [`spec_arg`]
   >- cheat (* TODO specialisation *) >>
   rw[] >> eq_tac >> rw[] >> gvs[EVERY_MEM, FORALL_PROD] >> res_tac
-  >- cheat (* App_Lam - not true due to potentially empty `vs` *)
 QED
 
 Theorem pres_imp_wf_preserved:
@@ -638,6 +638,7 @@ Proof
     \\ irule Letrec_eq_Let_Letrec)
   >-
    (fs [exp_of_def,MAP_MAP_o,o_DEF]
+    \\ irule exp_eq_Lams_cong
     \\ ‘MAP (λx. Var (explode x) : exp) vs = MAP Var (MAP explode vs)’ by
           fs [MAP_MAP_o,o_DEF]
     \\ simp [Apps_Lams_Vars])

diff --git a/compiler/backend/languages/relations/pure_pres_lemmasScript.sml b/compiler/backend/languages/relations/pure_pres_lemmasScript.sml
@@ -15,7 +15,7 @@ open pure_expTheory pure_valueTheory pure_evalTheory pure_eval_lemmasTheory
 val _ = new_theory "pure_pres_lemmas";
 
 Theorem bidir_letrec_eta:
-  MEM (f,Lam a vs x) l ∧ ALL_DISTINCT (MAP FST l) ∧
+  MEM (f,Lam a vs x) l ∧ ALL_DISTINCT (MAP FST l) ∧ vs ≠ [] ∧
   EVERY (λ(v,e).
            DISJOINT (IMAGE explode (set vs)) (freevars (exp_of e)) ∧
            ~MEM v vs) l ∧
@@ -34,7 +34,8 @@ Proof
   \\ conj_tac
   >-
    (irule bidir_Letrec \\ fs [LIST_REL_same]
-    \\ irule bidir_Lam \\ simp [Once bidir_sym,bidir_App_Lam])
+    \\ simp [Once bidir_sym]
+    \\ irule bidir_App_Lam \\ fs [])
   \\ irule_at Any bidir_trans
   \\ irule_at (Pos hd) bidir_Letrec_Lam \\ fs []
   \\ simp [Once bidir_sym]
@@ -55,7 +56,7 @@ Proof
 QED
 
 Theorem bidir_letrec_eta_1:
-  ¬MEM f vs
+  ¬MEM f vs ∧ vs ≠ []
   ⇒
   (Letrec a [(f,Lam a vs x)] (Var a f))
   <-->
@@ -67,7 +68,7 @@ Proof
 QED
 
 Theorem bidir_letrec_expand_1:
-  ¬MEM f vs
+  ¬MEM f vs ∧ vs ≠ []
   ⇒
   (Letrec a [(f,Lam a vs x)] x)
   <-->
@@ -91,7 +92,7 @@ Proof
 QED
 
 Theorem bidir_contract_1:
-  ~MEM f ps ∧ ~MEM f ws ∧ vs ≠ [] ∧ ws ≠ []
+  ~MEM f ps ∧ ~MEM f ws ∧ vs ≠ [] ∧ ws ≠ [] ∧ set ws ⊆ set vs
   ⇒
   (Lam a (vs ++ ps)
      (Letrec a [(f,Lam a (ws ++ ps) x)]
@@ -103,53 +104,60 @@ Theorem bidir_contract_1:
 Proof
   Cases_on ‘ps = []’ >- fs []
   \\ rw []
-  \\ irule bidir_trans
-  \\ irule_at Any bidir_Lam_append \\ fs []
-  \\ irule bidir_Lam
-  \\ irule bidir_trans
-  \\ qabbrev_tac ‘y = Letrec a [(f,Lam a (ws ++ ps) x)] x’
-  \\ qexists_tac ‘Lam a ps
-                   (App a (Lam a (ws ++ ps) y) (MAP (Var a) ws ++ MAP (Var a) ps))’
-  \\ conj_tac >-
-   (irule bidir_Lam
-    \\ irule bidir_trans
-    \\ irule_at Any bidir_Letrec_App_forget
-    \\ irule_at Any bidir_App
-    \\ fs [LIST_REL_same,EVERY_MAP,exp_of_def]
-    \\ gvs [EVERY_MEM]
-    \\ irule bidir_trans
-    \\ irule_at (Pos hd) bidir_Letrec_unroll \\ fs []
-    \\ unabbrev_all_tac
-    \\ irule bidir_Letrec_Lam
-    \\ fs [exp_of_def,IN_DISJOINT,MEM_MAP]
-    \\ metis_tac [])
-  \\ simp [Once bidir_sym]
-  \\ irule bidir_trans
-  \\ qexists_tac ‘App a (Lam a (ws ++ ps) y) (MAP (Var a) ws)’
-  \\ conj_tac >-
+  \\ qabbrev_tac ‘z = Letrec a [(f,Lam a (ws ++ ps) x)] x’
+  \\ ‘Letrec a [(f,Lam a (ws ++ ps) x)] (Var a f) <--> Lam a (ws ++ ps) z’ by
    (irule bidir_trans
-    \\ irule_at Any bidir_Letrec_App_forget
-    \\ irule_at Any bidir_App
-    \\ fs [LIST_REL_same,EVERY_MAP,exp_of_def]
-    \\ gvs [EVERY_MEM]
-    \\ irule bidir_trans
     \\ irule_at (Pos hd) bidir_Letrec_unroll \\ fs []
     \\ unabbrev_all_tac
-    \\ irule bidir_Letrec_Lam
-    \\ fs [exp_of_def,IN_DISJOINT,MEM_MAP]
+    \\ irule_at (Pos hd) bidir_Letrec_Lam \\ gvs []
+    \\ gvs [exp_of_def,IN_DISJOINT,MEM_MAP]
     \\ metis_tac [])
-  \\ irule bidir_trans
-  \\ qexists_tac ‘Lam a ps y’
-  \\ conj_tac >-
-   (irule bidir_trans
+  \\ qsuff_tac ‘
+      Lam a (vs ++ ps)
+        (App a (Lam a (ws ++ ps) z) (MAP (Var a) ws ++ MAP (Var a) ps)) <-->
+      Lam a vs
+        (App a (Lam a (ws ++ ps) z) (MAP (Var a) ws))’
+  >-
+   (strip_tac
+    \\ irule_at (Pos hd) bidir_trans
+    \\ irule_at (Pos last) bidir_trans
+    \\ pop_assum $ irule_at $ Pos hd
+    \\ irule_at Any bidir_Lam
+    \\ irule_at Any bidir_Lam
+    \\ unabbrev_all_tac
+    \\ irule_at (Pos hd) bidir_trans
+    \\ irule_at Any bidir_Letrec_App_forget
+    \\ gvs [EVERY_MAP,exp_of_def] \\ gvs [EVERY_MEM]
+    \\ irule_at (Pos hd) bidir_App
+    \\ gvs [LIST_REL_same]
+    \\ simp [Once bidir_sym]
+    \\ irule_at (Pos hd) bidir_trans
+    \\ irule_at Any bidir_Letrec_App_forget
+    \\ gvs [EVERY_MAP,exp_of_def] \\ gvs [EVERY_MEM]
     \\ irule_at (Pos hd) bidir_App
+    \\ gvs [LIST_REL_same])
+  \\ irule_at Any bidir_trans
+  \\ qexists_tac ‘Lam a (vs ++ ps) z’
+  \\ conj_tac >-
+   (rewrite_tac [GSYM MAP_APPEND]
+    \\ irule bidir_App_Lam \\ fs []
+    \\ gvs [SUBSET_DEF])
+  \\ qsuff_tac ‘
+      Lam a vs (Lam a ps z) <-->
+      Lam a vs (App a (Lam a ws (Lam a ps z)) (MAP (Var a) ws))’
+  >-
+   (strip_tac
+    \\ irule bidir_trans
     \\ irule_at (Pos hd) bidir_Lam_append \\ fs []
-    \\ qexists_tac ‘MAP (Var a) ws’ \\ fs []
+    \\ irule bidir_trans
+    \\ pop_assum $ irule_at $ Pos hd
+    \\ irule bidir_Lam
+    \\ irule bidir_App
     \\ gvs [LIST_REL_same]
-    \\ metis_tac [bidir_App_Lam])
-  \\ irule bidir_Lam
+    \\ simp [Once bidir_sym]
+    \\ irule_at (Pos hd) bidir_Lam_append \\ fs [])
   \\ simp [Once bidir_sym]
-  \\ rewrite_tac [GSYM MAP_APPEND,bidir_App_Lam]
+  \\ irule bidir_App_Lam \\ fs []
 QED
 
 val _ = export_theory ();