Light sorry cleaning

imbrem · Sep 3, 2024 · 0559ce9 · 0559ce9
1 parent e59b211
commit 0559ce9
Show file tree

Hide file tree

Showing 3 changed files with 58 additions and 20 deletions.
diff --git a/DeBruijnSSA/BinSyntax/Syntax/Fv/Basic.lean b/DeBruijnSSA/BinSyntax/Syntax/Fv/Basic.lean
@@ -569,11 +569,10 @@ theorem Region.fvs_fvi {r : Region φ} : r.fvs ⊆ Set.Iio r.fvi := by
     apply Term.fvs_fvi
     apply Set.liftnFv_subset_Iio_of_subset_Iio
     assumption
-  | cfg β _ f =>
-    simp only [fvs, fvi, Set.Iio_max]
-    apply Set.union_subset_union
-    assumption
-    sorry
+  | cfg β _ f Iβ I =>
+    simp only [fvs, fvi, Set.Iio_max, Set.Iio_finset_univ_sup]
+    apply Set.union_subset_union Iβ
+    exact Set.iUnion_mono λi => Set.liftnFv_subset_Iio_of_subset_Iio (I i)
 
 -- theorem Region.vwk_eqOn_fvi {r : Region φ} (h : (Set.Iio r.fvi).EqOn ρ ρ')
 --   : r.vwk ρ = r.vwk ρ' := r.vwk_eqOn_fvs (h.mono r.fvs_fvi)
@@ -649,10 +648,17 @@ theorem Region.lwk_eqOn_fls (r : Region φ) (ρ ρ' : ℕ → ℕ) (h : r.fls.Eq
   | cfg β n G Iβ IG =>
     simp only [lwk]
     congr 1
-    exact Iβ _ _ sorry
+    apply Iβ _ _ _
+    rw [Nat.liftnWk_eqOn_iff]
+    apply h.mono
+    simp [fls]
     funext i
     apply IG
-    sorry
+    rw [Nat.liftnWk_eqOn_iff]
+    apply h.mono
+    apply Set.subset_union_of_subset_right
+    apply Set.subset_iUnion_of_subset
+    rfl
 
 -- theorem Region.fls_fli {r : Region φ} : r.fls ⊆ Set.Iio r.fli := by sorry
 

diff --git a/DeBruijnSSA/BinSyntax/Syntax/Fv/Subst.lean b/DeBruijnSSA/BinSyntax/Syntax/Fv/Subst.lean
@@ -33,12 +33,37 @@ theorem Region.fl_vsubst (σ : Term.Subst φ) (r : Region φ) : (r.vsubst σ).fl
 
 def Term.Subst.fvs (σ : Term.Subst φ) (i : ℕ) : Set ℕ := (σ i).fvs
 
+theorem Term.Subst.fvs_lift_def {σ : Term.Subst φ} {i}
+  : σ.lift.fvs i = σ.lift.fvs i := rfl
+
+theorem Term.Subst.fvs_liftn_def {σ : Term.Subst φ} {i n}
+  : (σ.liftn n).fvs i = (σ.liftn n i).fvs := rfl
+
+theorem Term.Subst.biUnion_fvs_lift {σ : Term.Subst φ} {s : Set ℕ}
+  : ⋃i ∈ s, (σ.lift.fvs i).liftFv = ⋃i ∈ s.liftFv, σ.fvs i := by
+  sorry
+
+theorem Term.Subst.biUnion_fvs_liftn {σ : Term.Subst φ} {s : Set ℕ}
+  : ⋃i ∈ s, ((σ.liftn n).fvs i).liftnFv n = ⋃i ∈ s.liftnFv n, σ.fvs i := by
+  induction n generalizing σ s with
+  | zero => simp
+  | succ n I =>
+    rw [Set.liftnFv_succ', <-biUnion_fvs_lift]
+    simp only [<-Set.liftFv_biUnion]
+    rw [<-I]
+    simp only [Set.liftFv_biUnion, <-Set.liftnFv_succ', Subst.liftn_succ']
+
 theorem Term.fvs_subst (σ : Term.Subst φ) (t : Term φ) : (t.subst σ).fvs = ⋃ x ∈ t.fvs, σ.fvs x
   := by induction t generalizing σ with
   | pair a b Ia Ib => simp only [fvs, Set.biUnion_union, *]
-  | let1 => sorry
-  | let2 => sorry
-  | case => sorry
+  | let1 =>
+    simp only [fvs, Set.biUnion_union, Set.liftnFv_iUnion, Subst.biUnion_fvs_lift, *]
+  | let2 =>
+    simp only [fvs, Set.biUnion_union, Set.liftnFv_iUnion, Subst.biUnion_fvs_liftn, *]
+  | case =>
+    simp only [
+      fvs, Set.biUnion_union, Set.liftnFv_iUnion, Subst.biUnion_fvs_lift, Set.union_assoc, *
+    ]
   | _ => simp [Subst.fvs, *]
 
 open Classical in
@@ -65,14 +90,21 @@ theorem Region.fvs_vsubst (σ : Term.Subst φ) (r : Region φ)
   := by induction r generalizing σ with
   | br => simp [Term.fvs_subst]
   | let1 =>
-    simp only [fvs, Term.fvs_subst, Set.biUnion_union, Set.liftnFv_iUnion, *]
-    apply congrArg
-    ext k
-    simp only [Set.mem_iUnion, exists_prop]
-    sorry
-  | let2 => sorry
-  | case => sorry
-  | cfg => sorry
+    simp only [
+      fvs, Term.fvs_subst, Set.biUnion_union, Set.liftnFv_iUnion, Term.Subst.biUnion_fvs_lift, *
+    ]
+  | let2 =>
+    simp only [
+      fvs, Term.fvs_subst, Set.biUnion_union, Set.liftnFv_iUnion, Term.Subst.biUnion_fvs_liftn, *
+    ]
+  | case =>
+    simp only [
+      fvs, Term.fvs_subst, Set.biUnion_union, Set.liftnFv_iUnion, Term.Subst.biUnion_fvs_lift, *
+    ]
+  | cfg =>
+    simp only [
+      fvs, Set.biUnion_union, Set.biUnion_iUnion, Set.liftFv_biUnion, Term.Subst.biUnion_fvs_lift, *
+    ]
 
 open Classical in
 theorem Region.fvs_vsubst0 (t : Region φ) (s : Term φ)

diff --git a/lake-manifest.json b/lake-manifest.json
@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "ba7dc41500c8e6b10775da7e2c62f172776926c9",
+   "rev": "3a97fe99a8c8180b83efac3be780aa9342a2529c",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,
@@ -75,7 +75,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "bd2aae74446bd3cfce55255dfb5aed18ab927def",
+   "rev": "3c270bec05c94350f961c5fae7399fa815527418",
    "name": "discretion",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",