symcc: refactor a couple more places to rely on higher level primitives (#909)

Signed-off-by: Craig Disselkoen <cdiss@amazon.com>

Author: cdisselkoen

cedar-lean/Cedar/Data/Set.lean

@@ -159,6 +159,9 @@ public instance [LT α] [DecidableLT α] : Union (Set α) := ⟨Set.union⟩
 
 ----- Termination-friendly iterators -----
 
+public def map₁ {α} [LT β] [DecidableLT β] (s : Set α) (f : {a : α // a ∈ s} → β) : Set β :=
+  Set.make (s.elts.attach.map f)
+
 public def all₁ {α} (s : Set α) (f : {a : α // a ∈ s} → Bool) : Bool :=
   s.elts.attach.all f
 

cedar-lean/Cedar/Data/SizeOf.lean

@@ -132,4 +132,8 @@ public theorem sizeOf_lt_of_elts [SizeOf α] (s : Set α) :
   conv => rhs ; unfold sizeOf _sizeOf_inst _sizeOf_1 ; simp
   omega
 
+public theorem sizeOf_mk [SizeOf α] (xs : List α) :
+  sizeOf (Set.mk xs) = 1 + sizeOf xs
+:= by simp
+
 end Cedar.Data.Set

cedar-lean/Cedar/SymCC/Concretizer.lean

@@ -122,23 +122,23 @@ def TermPrim.value? : TermPrim → Option Value
 
 def Term.value? : Term → Option Value
   | .prim p => p.value?
-  | .set (.mk ts) _ => do
-    let vs ← ts.mapM₁ λ ⟨tᵢ, _⟩ => tᵢ.value?
+  | .set s _ => do
+    let vs ← s.elts.mapM₁ λ ⟨tᵢ, _⟩ => tᵢ.value?
     .some (.set (Set.make vs))
-  | .record (.mk ats) => do
-    let avs? ← ats.mapM₂ λ ⟨(aᵢ, tᵢ), _⟩ => attrValue? aᵢ tᵢ
+  | .record ats => do
+    let avs? ← ats.toList.mapM₂ λ ⟨(aᵢ, tᵢ), _⟩ => attrValue? aᵢ tᵢ
     let avs := avs?.filterMap λ (aᵢ, vᵢ?) => vᵢ?.map (Prod.mk aᵢ)
     .some (.record (Map.mk avs))
   | _ => .none
 termination_by t => sizeOf t
 decreasing_by
-  all_goals {
-    simp_wf
-    rename_i h
-    try replace h := List.sizeOf_lt_of_mem h
-    simp only at h
+  all_goals simp_wf ; rename_i h
+  · have := List.sizeOf_lt_of_mem h
+    have := Set.sizeOf_lt_of_elts s
+    omega
+  · have := Map.sizeOf_lt_of_toList ats
+    simp only at *
     omega
-  }
 where
   attrValue? (a : Attr) : Term → Option (Attr × Option Value)
     | .some t => do .some (a, .some (← t.value?))
@@ -158,12 +158,24 @@ def TermPrim.entityUIDs : TermPrim → Set EntityUID
 
 def Term.entityUIDs : Term → Set EntityUID
   | .var _
-  | .none _              => Set.empty
-  | .prim p              => p.entityUIDs
-  | .some t              => t.entityUIDs
-  | .set (Set.mk ts) _   => ts.mapUnion₁ (λ ⟨t, _⟩ => t.entityUIDs)
-  | .record (Map.mk ats) => ats.mapUnion₃ (λ ⟨(_, t), _⟩ => t.entityUIDs)
-  | .app _ ts _          => ts.mapUnion₁ (λ ⟨t, _⟩ => t.entityUIDs)
+  | .none _      => Set.empty
+  | .prim p      => p.entityUIDs
+  | .some t      => t.entityUIDs
+  | .set ts _    => ts.elts.mapUnion₁ (λ ⟨t, _⟩ => t.entityUIDs)
+  | .record ats  => ats.toList.mapUnion₃ (λ ⟨(_, t), _⟩ => t.entityUIDs)
+  | .app _ ts _  => ts.mapUnion₁ (λ ⟨t, _⟩ => t.entityUIDs)
+decreasing_by
+  all_goals simp_wf
+  · rename t ∈ ts.elts => h
+    have := Set.sizeOf_lt_of_mem h
+    have := Set.sizeOf_lt_of_elts ts
+    omega
+  · have := Map.sizeOf_lt_of_toList ats
+    simp only at *
+    omega
+  · rename t ∈ ts => h
+    have := List.sizeOf_lt_of_mem h
+    omega
 
 def Term.entityUID? : Term → Option EntityUID
   | .prim (.entity uid) => .some uid

cedar-lean/Cedar/SymCC/Interpretation.lean

@@ -16,6 +16,7 @@
 
 module
 
+import Cedar.Data.SizeOf
 import Cedar.Spec
 public import Cedar.SymCC.Env
 import Cedar.SymCC.Factory
@@ -141,19 +142,27 @@ def Op.interpret (I : Interpretation) (op : Op) (ts : List Term) (ty : TermType)
   | _, _                  => .app op ts ty
 
 public def Term.interpret (I : Interpretation) : Term → Term
-  | .prim p             => .prim p
-  | .var v              => I.vars v
-  | .none ty            => noneOf ty
-  | .some t             => someOf (t.interpret I)
-  | .set (Set.mk ts) ty =>
+  | .prim p       => .prim p
+  | .var v        => I.vars v
+  | .none ty      => noneOf ty
+  | .some t       => someOf (t.interpret I)
+  | .set ts ty    =>
     let ts' := ts.map₁ (λ ⟨t, _⟩ => t.interpret I)
-    setOf ts' ty
-  | .app op ts ty       =>
+    .set ts' ty
+  | .app op ts ty =>
     let ts' := ts.map₁ (λ ⟨t, _⟩ => t.interpret I)
     op.interpret I ts' ty
-  | .record (.mk ats)   =>
-    let ats' := ats.map₃ (λ ⟨(aᵢ, tᵢ), _⟩ => (aᵢ, tᵢ.interpret I))
-    recordOf ats'
+  | .record ats   =>
+    .record $ ats.mapOnValues₂ (λ ⟨t, _⟩ => t.interpret I)
+decreasing_by
+  all_goals simp_wf
+  · rename t ∈ ts => h
+    have := Set.sizeOf_lt_of_mem h
+    omega
+  · rename t ∈ ts => h
+    have := List.sizeOf_lt_of_mem h
+    omega
+  · omega
 
 public def SymRequest.interpret (I : Interpretation) (req : SymRequest)  : SymRequest :=
   {

cedar-lean/Cedar/Thm/Data/Map.lean

@@ -460,6 +460,26 @@ public theorem find?_notmem_keys [LT α] [DecidableLT α] [StrictLT α] [Decidab
       replace h₂ := List.mem_of_find?_eq_some h₂
       exact in_list_in_keys h₂
 
+/--
+  Two well-formed maps are equal if they have the same `find?` for every key.
+-/
+public theorem find?_ext [LT α] [DecidableLT α] [StrictLT α] [DecidableEq α] {m₁ m₂ : Map α β}
+  (wf₁ : m₁.WellFormed)
+  (wf₂ : m₂.WellFormed)
+  (h : ∀ k, m₁.find? k = m₂.find? k) :
+  m₁ = m₂
+:= by
+  apply eq_iff_toList_equiv wf₁ wf₂ |>.mp
+  constructor
+  · intro ⟨k, v⟩ h₁
+    have h₂ := (in_list_iff_find?_some wf₁).mp h₁
+    rw [h] at h₂
+    exact (in_list_iff_find?_some wf₂).mpr h₂
+  · intro ⟨k, v⟩ h₁
+    have h₂ := (in_list_iff_find?_some wf₂).mp h₁
+    rw [← h] at h₂
+    exact (in_list_iff_find?_some wf₁).mpr h₂
+
 public theorem find?_none_all_absent [LT α] [DecidableLT α] [StrictLT α] [DecidableEq α] {m : Map α β} {k : α} :
   m.find? k = none → ∀ v, ¬ (k, v) ∈ m.toList
 := by
@@ -765,8 +785,9 @@ public theorem mapOnValues_doubleton {f : β → γ} {s₁ s₂ : String} (b₁
   Map.mapOnValues f (Map.mk [(s₁, b₁), (s₂, b₂)]) = Map.mk [(s₁, f b₁), (s₂, f b₂)]
 := by simp [mapOnValues]
 
+@[simp]
 public theorem find?_mapOnValues {α β γ} [LT α] [DecidableLT α] [DecidableEq α] (f : β → γ) (m : Map α β) (k : α)  :
-  (m.find? k).map f = (m.mapOnValues f).find? k
+  (m.mapOnValues f).find? k = (m.find? k).map f
 := by
   simp only [find?, toList, mapOnValues, ← List.find?_pair_map]
   cases m.1.find? (λ x => x.fst == k) <;> simp only [Option.map_none, Option.map_some]
@@ -776,7 +797,7 @@ public theorem find?_mapOnValues_some {α β γ} [LT α] [DecidableLT α] [Decid
   (m.mapOnValues f).find? k = .some (f v)
 := by
   intro h₁
-  rw [← find?_mapOnValues]
+  rw [find?_mapOnValues]
   simp [Option.map, h₁]
 
 public theorem find?_mapOnValues_some' {α β γ} [LT α] [DecidableLT α] [DecidableEq α] (f : β → γ) {m : Map α β} {k : α} {v : γ} :
@@ -805,7 +826,7 @@ public theorem find?_mapOnValues_some' {α β γ} [LT α] [DecidableLT α] [Deci
 public theorem find?_mapOnValues_none {α β γ} [LT α] [DecidableLT α] [DecidableEq α] (f : β → γ) {m : Map α β} {k : α} :
   (m.mapOnValues f).find? k = .none ↔
   m.find? k = .none
-:= by simp [← find?_mapOnValues]
+:= by simp [find?_mapOnValues]
 
 public theorem mapOnValues_eq_make_map {α β γ} [LT α] [StrictLT α] [DecidableLT α] (f : β → γ) {m : Map α β}
   (wf : m.WellFormed) :
@@ -834,13 +855,14 @@ public theorem mem_toList_find? {α β} [LT α] [DecidableLT α] [StrictLT α] [
   simp only at h
   simp [find?, h]
 
-public theorem mapOnValues_contains {α β γ} [LT α] [DecidableLT α] [DecidableEq α] (f : β → γ) {m : Map α β} {k : α} :
-  Map.contains m k = Map.contains (Map.mapOnValues f m) k
+@[simp]
+public theorem contains_mapOnValues {α β γ} [LT α] [DecidableLT α] [DecidableEq α] (f : β → γ) {m : Map α β} {k : α} :
+  Map.contains (Map.mapOnValues f m) k = Map.contains m k
 := by
   simp only [contains, Option.isSome]
-  split <;> rename_i h
-  · simp [find?_mapOnValues_some f h]
+  cases h : m.find? k
   · simp [(find?_mapOnValues_none f).mpr h]
+  · simp [find?_mapOnValues_some f h]
 
 @[simp]
 public theorem keys_mapOnValues [LT α] [StrictLT α] [DecidableLT α] [DecidableEq α] (f : β → γ) (m : Map α β) :
@@ -879,6 +901,12 @@ public theorem mapOnValues_restricted_id  {f : β → β} {m : Map α β} :
   intro pair hpair
   simp [h pair.snd (Map.in_list_in_values hpair)]
 
+@[simp]
+public theorem mapOnValues_make [LT α] [DecidableLT α] [StrictLT α] {f : β → γ} {kvs : List (α × β)} :
+  (Map.make kvs).mapOnValues f = Map.make (kvs.map (Prod.map id f))
+:= by
+  simp [make, mapOnValues, List.canonicalize_of_map_fst]
+
 @[simp]
 public theorem mapOnValues₂_eq_mapOnValues {α β γ} [SizeOf α] [SizeOf β] (m : Map α β) (f : β → γ) :
   m.mapOnValues₂ (λ x : { x : β // sizeOf x < sizeOf m } => f x.1) = m.mapOnValues f
@@ -898,7 +926,7 @@ public theorem findOrErr_mapOnValues [LT α] [DecidableLT α] [DecidableEq α] {
   (m.mapOnValues f).findOrErr k e = (m.findOrErr k e).map f
 := by
   unfold findOrErr
-  rw [← find?_mapOnValues]
+  rw [find?_mapOnValues]
   cases m.find? k <;> simp [Except.map]
 
 @[simp]
@@ -1001,10 +1029,10 @@ public theorem findOrErr_err_iff_not_in_keys [LT α] [DecidableLT α] [StrictLT
   exact find?_notmem_keys wf
 
 /--
-  The converse requires two extra preconditions (`m` is `WellFormed` and `f` is
-  injective) and is available as `in_mapOnValues_in_toList`
+  The converse requires the extra precondition that `f` is injective, and is
+  available as `in_mapOnValues_in_toList`
 -/
-public theorem in_toList_in_mapOnValues [LT α] [DecidableLT α] [DecidableEq α] {f : β → γ} {m : Map α β} {k : α} {v : β} :
+public theorem in_toList_in_mapOnValues [LT α] [DecidableLT α] [DecidableEq α] (f : β → γ) {m : Map α β} {k : α} {v : β} :
   (k, v) ∈ m.toList → (k, f v) ∈ (m.mapOnValues f).toList
 := by
   unfold mapOnValues

cedar-lean/Cedar/Thm/Data/Set.lean

@@ -263,6 +263,10 @@ public theorem make_wf [LT α] [DecidableLT α] [StrictLT α] (xs : List α) :
 := by
   simp only [WellFormed, make, toList, elts, List.canonicalize_idempotent]
 
+public theorem make_elts [LT α] [DecidableLT α] {s : Set α} :
+  WellFormed s → Set.make s.elts = s
+:= by grind [WellFormed, toList]
+
 public theorem make_sorted {α} [LT α] [DecidableLT α] [StrictLT α] {xs : List α} :
   xs.Sorted → Set.make xs = Set.mk xs
 := by
@@ -730,13 +734,60 @@ public theorem wellFormed_correct {α} [LT α] [StrictLT α] [DecidableLT α] {s
 
 /-! ### map -/
 
+public theorem map_wf [LT β] [DecidableLT β] [StrictLT β] (f : α → β) (s : Set α) :
+  (s.map f).WellFormed
+:= by simp [map, make_wf]
+
+public theorem map_id [LT α] [DecidableLT α] (s : Set α) :
+  s.WellFormed → s.map id = s
+:= by
+  intro hwf
+  simp [map, make_elts hwf]
+
 /-- Analogue of `List.mem_map` but for sets -/
 @[simp]
-public theorem mem_map [LT α] [DecidableLT α] [StrictLT α] [LT β] [DecidableLT β] [StrictLT β] (b : β) (f : α → β) (s : Set α) :
+public theorem mem_map [LT α] [DecidableLT α] [StrictLT α] [LT β] [DecidableLT β] [StrictLT β] {b : β} {f : α → β} {s : Set α} :
   b ∈ s.map f ↔ ∃ a ∈ s, f a = b
 := by
   simp [Set.map, Set.mem_make, Set.mem_elts_iff_mem_set]
 
+/-- Analogue of `List.map_congr`, but for sets -/
+public theorem map_congr [LT β] [DecidableLT β] {f g : α → β} {s : Set α} :
+  (∀ a ∈ s, f a = g a) → s.map f = s.map g
+:= by
+  simp only [map]
+  intro h
+  congr 1
+  apply List.map_congr
+  intro x hx
+  exact h x hx
+
+@[simp]
+public theorem isEmpty_map [DecidableEq α] [LT β] [DecidableLT β] [DecidableEq β] {f : α → β} {s : Set α} :
+  (s.map f).isEmpty = s.isEmpty
+:= by
+  cases h : s.isEmpty
+  case true =>
+    simp only [isEmpty, empty, beq_iff_eq] at h
+    simp [map, h]
+  case false =>
+    simp only [isEmpty, empty, beq_eq_false_iff_ne, ne_eq] at h
+    simp only [map, elts, isEmpty_make_eq_false, ne_eq, List.map_eq_nil_iff]
+    cases s ; simp_all
+
+@[simp]
+public theorem map_make [LT α] [DecidableLT α] [StrictLT α] [LT β] [DecidableLT β] [StrictLT β] {f : α → β} {xs : List α} :
+  (Set.make xs).map f = Set.make (xs.map f)
+:= by
+  simp only [map]
+  rw [make_make_eqv]
+  exact List.map_equiv f (Set.elts (Set.make xs)) xs elts_make_eqv
+
+-- TODO: perhaps we could avoid needing to have this a public theorem, if we had enough other lemmas about `Set.map` that avoided callers having to reason about `make` or `elts`
+public theorem map_def [LT β] [DecidableLT β] (f : α → β) (s : Set α) :
+  s.map f = Set.make (s.elts.map f)
+:= by simp [Set.map]
+
 /-! ### filter and differences -/
 
 public theorem filter_wf [LT α] [DecidableLT α] [StrictLT α] (p : α → Bool) (s : Set α) :
@@ -802,7 +853,12 @@ public theorem any_eq_false {f : α → Bool} {s : Set α} :
 := by
   simp only [Set.any, List.any_eq_false, Set.mem_elts_iff_mem_set]
 
-/-! ### all₁ and any₁ -/
+/-! ### map₁, all₁, and any₁ -/
+
+@[simp]
+public theorem map₁_eq_map [LT α] [DecidableLT α] [LT β] [DecidableLT β] (f : α → β) (s : Set α) :
+  (s.map₁ λ ⟨elt, _⟩ => f elt) = s.map f
+:= by simp [map₁, map]
 
 @[simp]
 public theorem all₁_eq_all {s : Set α} {f : α → Bool} :

cedar-lean/Cedar/Thm/SymCC/Compiler/Record.lean

@@ -262,17 +262,17 @@ private theorem same_forall₂_implies_same_record {ats : List (Attr × Term)} {
   generalize h₂ : (List.canonicalize Prod.fst avs) = vs
   rw [h₁, h₂] at hs
   clear h₁ h₂
-  have ⟨avs', hts⟩ : ∃ avs', List.mapM' (λ x => Term.value?.attrValue? x.fst x.snd) ts = some avs' := by
+  have ⟨avs', hts⟩ : ∃ avs', List.mapM (λ x => Term.value?.attrValue? x.fst x.snd) ts = some avs' := by
     induction hs
     case nil =>
       exists []
     case cons thd vhd ttl _ h₁ _ ih =>
       replace ⟨vtl', ih⟩ := ih
       exists ((vhd.fst, some vhd.snd) :: vtl')
-      simp only [List.mapM'_cons, value?_some_implies_attrValue?_some h₁.right, ih, Option.pure_def,
+      simp only [List.mapM_cons, value?_some_implies_attrValue?_some h₁.right, ih, Option.pure_def,
         Option.bind_some_fun, ← h₁.left]
   apply record_value?_some_implied_by hts
-  replace hts := List.mapM'_some_eq_filterMap hts
+  replace hts := List.mapM_some_eq_filterMap hts
   subst hts
   simp only [List.filterMap_filterMap]
   induction hs

cedar-lean/Cedar/Thm/SymCC/Concretizer/Lit.lean

@@ -168,7 +168,6 @@ theorem wf_term_implies_valid_uids {t : Term} {εs : SymEntities} :
     replace hwf := wf_term_set_implies_wf_elt hwf hin'
     exact wf_term_implies_valid_uids hwf uid hin
   case record ats =>
-    cases ats ; rename_i ats
     simp only [List.mapUnion₃_eq_mapUnion λ x : Attr × Term => x.snd.entityUIDs] at hin
     rw [List.mem_mapUnion_iff_mem_exists] at hin
     replace ⟨at', hin', hin⟩ := hin
@@ -187,20 +186,22 @@ decreasing_by
   · rename_i h _ ; subst h
     simp only [Term.some.sizeOf_spec]
     omega
-  · rename_i h _ _ _ _ _ ; subst h
-    rename_i h _ _ _ _ _ _ ; subst h
+  · subst_vars
     have hs := List.sizeOf_lt_of_mem hin'
     simp only [Term.set.sizeOf_spec, Set.mk.sizeOf_spec, gt_iff_lt]
+    rename List Term => ts
+    have := Set.sizeOf_lt_of_elts (Set.mk ts)
+    have := Set.sizeOf_mk ts
     omega
-  · rename_i h _ _ _ _ _ ; subst h
-    rename_i h _ _ _ _ _ _ ; subst h
-    have hs := List.sizeOf_lt_of_mem hin'
-    have hp : at' = (at'.fst, at'.snd) := by simp only
-    rw [hp] at hs
-    simp only [Prod.mk.sizeOf_spec] at hs
-    simp only [Term.record.sizeOf_spec, Map.mk.sizeOf_spec, gt_iff_lt]
+  · subst_vars
+    simp only [Term.record.sizeOf_spec]
+    rename Map Attr Term => m
+    calc sizeOf at'.snd
+      _ < sizeOf at' := by cases at' ; simp only [Prod.mk.sizeOf_spec, Nat.lt_add_left_iff_pos] ; omega
+      _ < sizeOf m.toList := List.sizeOf_lt_of_mem hin'
+      _ < sizeOf m := Map.sizeOf_lt_of_toList m
     omega
-  · rename_i h _ _ _ _ _ _ _ _ _ _ _ _ _ _ ; subst h
+  · subst_vars
     have hs := List.sizeOf_lt_of_mem hin'
     simp only [Term.app.sizeOf_spec]
     omega