Complete CallElimCorrect proof

Strata/DL/Util/ListUtils.lean

@@ -191,13 +191,22 @@ theorem List.Disjoint.symm_app (d : Disjoint l (l₁ ++ l₂))
   : Disjoint l (l₂ ++ l₁) := fun _ Hin1 Hin2 => d Hin1
         (mem_append.mpr $ Or.symm (mem_append.mp Hin2))
 
-theorem List.Disjoint_Subset : Disjoint vs ks → ks'.Subset ks → vs.Disjoint ks' := by
+theorem List.Disjoint_Subset_right : Disjoint vs ks → ks'.Subset ks → vs.Disjoint ks' := by
   intros Hdis Hsub
   simp [Disjoint, List.Subset] at *
   intros a Hin1 Hin2
   specialize Hdis Hin1
   simp_all
 
+theorem List.Disjoint_Subset_left : Disjoint vs ks → List.Subset vs' vs → vs'.Disjoint ks := by
+  intros Hdis Hsub
+  apply List.Disjoint.symm
+  apply Disjoint_Subset_right (Disjoint.symm Hdis) Hsub
+
+theorem List.Disjoint_Subsets : Disjoint vs ks → List.Subset vs' vs → List.Subset ks' ks → vs'.Disjoint ks' := by
+  intros Hdis Hsub1 Hsub2
+  exact List.Disjoint_Subset_left (Disjoint_Subset_right Hdis Hsub2) Hsub1
+
 theorem List.DisjointAppLeft' :
   Disjoint vs (ks ++ ks') → Disjoint vs ks' := by
   intros Hdist h
@@ -212,6 +221,26 @@ theorem List.DisjointAppRight' :
   have Hdist' := List.Disjoint.symm_app Hdist
   exact List.DisjointAppLeft' Hdist'
 
+theorem List.Subset.subset_app_of_or_2 {l: List α}: l ⊆ l1 ∨ l ⊆ l2 → l ⊆ l1 ++ l2  := by
+  simp [Subset, List.Subset]
+  intro H a Ha
+  cases H <;> simp_all
+
+theorem List.Subset.subset_app_of_or_3 {l: List α}: l ⊆ l1 ∨ l ⊆ l2 ∨ l ⊆ l3 → l ⊆ l1 ++ l2 ++ l3  := by
+  simp [Subset, List.Subset]
+  intro H a Ha
+  cases H <;> try (rename_i H; cases H)
+  any_goals simp_all
+
+theorem List.Subset.subset_app_of_or_4 {l: List α}: l ⊆ l1 ∨ l ⊆ l2 ∨ l ⊆ l3 ∨ l ⊆ l4 → l ⊆ l1 ++ l2 ++ l3 ++ l4 := by
+  simp [Subset, List.Subset]
+  intro H a Ha
+  cases H <;> try (rename_i H; cases H <;> try (rename_i H; cases H))
+  any_goals simp_all
+
+theorem List.Subset.assoc {l: List α}: l ⊆ l1 ++ l2 ++ l3 ↔ l ⊆ l1 ++ (l2 ++ l3) := by
+  simp [Subset, List.Subset]
+
 theorem List.replaceAll_app {α : Type} [DecidableEq α] {h h' : α} {as bs : List α}:
   List.replaceAll as h h' ++ List.replaceAll bs h h' = List.replaceAll (as ++ bs) h h' := by
   induction as generalizing bs

Strata/DL/Util/Map.lean

@@ -202,4 +202,10 @@ theorem Map.insert_values [DecidableEq α] (m : Map α β) :
       grind
   done
 
+theorem Map.findNone_eq_notmem_mapfst {m: Map α β} [DecidableEq α]: ¬ a ∈ List.map Prod.fst m ↔ Map.find? m a = none := by
+  induction m <;> simp [Map.find?]
+  constructor <;> intro H
+  split <;> simp_all
+  split at H <;> simp_all
+  rw [Eq.comm]; assumption
 -------------------------------------------------------------------------------

Strata/Languages/Boogie/OldExpressions.lean

@@ -255,6 +255,18 @@ with `val`.
 def substsOldExprs (sm : Map Expression.Ident Expression.Expr) (es : List Expression.Expr) :=
   es.map $ substsOldExpr sm
 
+theorem substsOldExpr_singleton: substsOldExpr [(var,s)] e = substOld var s e := by
+  induction e <;> simp [substsOldExpr, substOld, Map.isEmpty, *]
+  split <;> simp_all;
+  simp [Map.find?]
+  split <;> simp_all
+  intro h; rw [Eq.comm] at h
+  contradiction
+
+theorem substOldExpr_nil: OldExpressions.substsOldExpr [] e = e := by
+  unfold OldExpressions.substsOldExpr
+  simp [Map.isEmpty]
+
 /--
 For each `(var, expr)` pair in `sm`, substitute `old(var)` with `expr` in
 `conds`.

Strata/Languages/Boogie/StatementSemanticsProps.lean

@@ -1954,7 +1954,7 @@ theorem InvStoresExceptUpdatedMem :
   simp [invStoresExcept] at *
   intros Hsub vs Hdisj
   refine InvStoresUpdatedStatesDisjLeftMono ?_ ?_ Hlen
-  exact List.Disjoint_Subset Hdisj Hsub
+  exact List.Disjoint_Subset_right Hdisj Hsub
   exact Hinv _ Hdisj
 
 theorem InvStoresExceptUpdateStates :