switch to higher-level functions in a few places (#901)

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

Author: cdisselkoen

cedar-lean/Cedar/Data/Set.lean

@@ -157,6 +157,14 @@ public instance [DecidableEq α] : Inter (Set α) := ⟨Set.intersect⟩
 -- enables ∪
 public instance [LT α] [DecidableLT α] : Union (Set α) := ⟨Set.union⟩
 
+----- Termination-friendly iterators -----
+
+public def all₁ {α} (s : Set α) (f : {a : α // a ∈ s} → Bool) : Bool :=
+  s.elts.attach.all f
+
+public def any₁ {α} (s : Set α) (f : {a : α // a ∈ s} → Bool) : Bool :=
+  s.elts.attach.any f
+
 end Set
 
 end Cedar.Data

cedar-lean/Cedar/Data/SizeOf.lean

@@ -90,6 +90,14 @@ public theorem sizeOf_lt_of_toList [SizeOf α] [SizeOf β] (m : Map α β) :
   generalize sizeOf m.1 = s
   omega
 
+public theorem sizeOf_lt_of_values [SizeOf α] [SizeOf β] {m : Map α β}
+  (h : b ∈ m.values) :
+  sizeOf b < sizeOf m
+:= by
+  simp only [values, List.mem_map, Prod.exists, exists_eq_right] at h
+  replace ⟨a, h⟩ := h
+  exact List.sizeOf_snd_lt_sizeOf_list h
+
 public theorem sizeOf_lt_of_tl [SizeOf α] [SizeOf β] {m : Map α β} {tl : List (α × β)}
   (h : m.toList = (k, v) :: tl) :
   1 + sizeOf tl < sizeOf m
@@ -117,7 +125,7 @@ public theorem sizeOf_lt_of_mem [SizeOf α] {s : Set α}
     omega
   omega
 
-public theorem sizeOf_lt_of_elts [SizeOf α] {s : Set α} :
+public theorem sizeOf_lt_of_elts [SizeOf α] (s : Set α) :
   sizeOf s.elts < sizeOf s
 := by
   simp only [elts]

cedar-lean/Cedar/SymCC/Decoder.lean

@@ -357,14 +357,10 @@ def defaultPrim (eidOf : EntityType → String) : TermPrimType → TermPrim
   | .ext xty    => defaultExt xty
 
 def defaultLit (eidOf : EntityType → String) : TermType → Term
-  | .prim pty            => .prim (defaultPrim eidOf pty)
-  | .option ty           => .none ty
-  | .set ty              => .set Set.empty ty
-  | .record (Map.mk tys) =>
-    let ts := tys.map₂ λ ⟨(a, ty), _⟩ => (a, defaultLit eidOf ty)
-    .record (Map.mk ts)
-termination_by ty => sizeOf ty
-decreasing_by simp_wf ; simp at * ; omega
+  | .prim pty   => .prim (defaultPrim eidOf pty)
+  | .option ty  => .none ty
+  | .set ty     => .set Set.empty ty
+  | .record tys => .record (tys.mapOnValues₂ λ ⟨ty, _⟩ => defaultLit eidOf ty)
 
 def defaultUDF (eidOf : EntityType → String) (f : UUF) : UDF :=
   ⟨f.arg, f.out, Map.empty, defaultLit eidOf f.out⟩

cedar-lean/Cedar/SymCC/Factory.lean

@@ -256,11 +256,10 @@ public def set.inter (ts₁ ts₂ : Term) : Term :=
     | _, _ => .app Op.set.inter [ts₁, ts₂] ts₁.typeOf
 
 public def set.isEmpty : Term → Term
-  | .set (Set.mk []) _     => true
-  | .set (Set.mk (_::_)) _ => false
+  | .set s _ => s.isEmpty
   | ts =>
     match ts.typeOf with
-    | .set ty => eq ts (.set (Set.mk []) ty)
+    | .set ty => eq ts (.set Set.empty ty)
     | _       => false
 
 public def set.intersects (ts₁ ts₂ : Term) : Term :=

cedar-lean/Cedar/SymCC/Term.lean

@@ -16,6 +16,7 @@
 
 module
 
+import Cedar.Data.SizeOf
 import Cedar.Spec
 public import Cedar.SymCC.Data
 public import Cedar.SymCC.Op
@@ -89,11 +90,21 @@ public def Term.typeOf : Term → TermType
 
 public def Term.isLiteral : Term → Bool
   | .prim _
-  | .none _               => true
-  | .some t               => t.isLiteral
-  | .set (Set.mk ts) _    => ts.attach.all (λ ⟨t, _⟩ => t.isLiteral)
-  | .record (Map.mk atrs) => atrs.attach₃.all (λ ⟨(_, t), _⟩ => t.isLiteral)
-  | _                     => false
+  | .none _      => true
+  | .some t      => t.isLiteral
+  | .set ts _    => ts.all₁ λ ⟨t, _⟩ => t.isLiteral
+  | .record atrs => atrs.toList.attach₂.all λ ⟨(_, t), _⟩ => t.isLiteral
+  | _            => false
+decreasing_by
+  all_goals simp_wf
+  · rename_i h
+    have := Set.sizeOf_lt_of_elts ts
+    have := List.sizeOf_lt_of_mem h
+    omega
+  · rename_i h
+    have := Map.sizeOf_lt_of_toList atrs
+    simp only at *
+    omega
 
 public instance : Coe Bool Term where
   coe b := .prim (.bool b)

cedar-lean/Cedar/Thm/Data/List/Lemmas.lean

@@ -64,7 +64,7 @@ public theorem all_pmap_subtype
 := by
   induction as <;> simp [*]
 
-/-! ### map and map₁ -/
+/-! ### map, map₁, map₂, map₃, and `attach` variants -/
 
 /--
   Copied from Mathlib. We can delete this if it gets added to Batteries.
@@ -128,6 +128,28 @@ public theorem attach_def {as : List α} :
 := by
   simp [attach, attachWith]
 
+public theorem mem_attach₂ [SizeOf α] [SizeOf β] {as : List (α × β)} {pair : {x : α × β // sizeOf x.snd < 1 + sizeOf as}} :
+  pair ∈ as.attach₂ → (pair.val.fst, pair.val.snd) ∈ as
+:= by
+  simp only [attach₂, mem_pmap, Prod.exists]
+  intro h
+  replace ⟨a, b, h, _⟩ := h ; subst pair
+  simp [h]
+
+@[simp]
+public theorem all_attach₂ [SizeOf α] [SizeOf β] {as : List (α × β)} {f : (α × β) → Bool} :
+  as.attach₂.all (λ ⟨pair, _⟩ => f pair) = as.all f
+:= by
+  unfold attach₂
+  rw [all_pmap_subtype]
+
+@[simp]
+public theorem all_attach₂_snd [SizeOf α] [SizeOf β] {as : List (α × β)} {f : β → Bool} :
+  as.attach₂.all (λ ⟨(_, b), _⟩ => f b) = as.all λ (_, b) => f b
+:= by
+  unfold attach₂
+  simp [all_pmap_subtype λ ((_, b) : α × β) => f b]
+
 public theorem map₁_eq_map (f : α → β) (as : List α) :
   as.map₁ (λ x : {x // x ∈ as} => f x.val) =
   as.map f

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

@@ -847,6 +847,23 @@ public theorem values_mapOnValues [LT α] [StrictLT α] [DecidableLT α] [Decida
   unfold mapOnValues values
   induction m.1 <;> simp
 
+@[simp]
+public theorem mapOnValues_mapOnValues [LT α] [StrictLT α] [DecidableLT α] [DecidableEq α] {f : β → γ} {g : γ → φ} {m : Map α β} :
+  (m.mapOnValues f).mapOnValues g = m.mapOnValues (g ∘ f)
+:= by simp [mapOnValues]
+
+public theorem mapOnValues_restricted_id  {f : β → β} {m : Map α β} :
+  (∀ b ∈ m.values, f b = b) →
+  m.mapOnValues f = m
+:= by
+  simp only [mapOnValues]
+  cases m ; simp only [toList_mk_id, mk.injEq]
+  intro h
+  apply List.map_restricted_id
+  intro pair hpair
+  simp [h pair.snd (Map.in_list_in_values hpair)]
+
+@[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
 := by
@@ -988,40 +1005,31 @@ public theorem find?_none_iff_findorErr_errors [LT α] [DecidableLT α] [Decidab
   exact findOrErr_err_iff_find?_none.symm
 
 /--
-  Converse of `in_toList_in_mapOnValues`; requires the extra preconditions that `m`
-  is `WellFormed` and `f` is injective
+  Converse of `in_toList_in_mapOnValues`; requires the extra precondition that `f` is injective
 -/
-public theorem in_mapOnValues_in_toList [LT α] [DecidableLT α] [StrictLT α] [DecidableEq α] {f : β → γ} {m : Map α β} {k : α} {v : β}
-  (wf : m.WellFormed) :
+public theorem in_mapOnValues_in_toList [LT α] [DecidableLT α] [StrictLT α] [DecidableEq α] {f : β → γ} {m : Map α β} {k : α} {v : β} :
   (k, f v) ∈ (m.mapOnValues f).toList →
   (∀ v', f v = f v' → v = v') → -- require f to be injective
   (k, v) ∈ m.toList
 := by
-  rw [mapOnValues_eq_make_map f wf]
-  unfold toList
-  intro h₁ h_inj
-  replace h₁ := make_mem_list_mem h₁
-  replace ⟨(k', v'), h₁, h₂⟩ := List.mem_map.mp h₁
-  simp only [Prod.mk.injEq] at h₂ ; replace ⟨h₂', h₂⟩ := h₂ ; subst k'
-  specialize h_inj v' h₂.symm
+  simp only [toList, mapOnValues, List.mem_map, Prod.mk.injEq, Prod.exists, forall_exists_index,
+    and_imp]
+  intro a b h₁ _ h₂ h_inj ; subst a
+  specialize h_inj b h₂.symm
   subst h_inj
   exact h₁
 
 /--
   Slightly different formulation of `in_mapOnValues_in_toList`
 -/
-public theorem in_mapOnValues_in_toList' [LT α] [DecidableLT α] [StrictLT α] [DecidableEq α] {f : β → γ} {m : Map α β} {k : α} {v' : γ}
-  (wf : m.WellFormed) :
+public theorem in_mapOnValues_in_toList' [LT α] [DecidableLT α] [StrictLT α] [DecidableEq α] {f : β → γ} {m : Map α β} {k : α} {v' : γ} :
   (k, v') ∈ (m.mapOnValues f).toList →
   ∃ v, f v = v' ∧ (k, v) ∈ m.toList
 := by
-  rw [mapOnValues_eq_make_map f wf]
-  unfold toList
-  intro h₁
-  replace h₁ := make_mem_list_mem h₁
-  replace ⟨(k', v'), h₁, h₂⟩ := List.mem_map.mp h₁
-  simp only [Prod.mk.injEq] at h₂ ; replace ⟨h₂', h₂⟩ := h₂ ; subst k' h₂
-  exists v'
+  simp only [mapOnValues, toList, List.mem_map, Prod.mk.injEq, Prod.exists,
+    forall_exists_index, and_imp]
+  intro a b h₁ _ _ ; subst a v'
+  exists b
 
 /-! ### mapMOnValues -/
 

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

@@ -156,6 +156,16 @@ public theorem map_empty [LT β] [DecidableLT β] (f : α → β) :
 := by
   simp [Set.map, empty_eq_mk_nil, Set.elts, Set.make, List.canonicalize_nil]
 
+@[simp]
+public theorem all_empty (f : α → Bool) :
+  Set.empty.all f = true
+:= by simp [all]
+
+@[simp]
+public theorem any_empty (f : α → Bool) :
+  Set.empty.any f = false
+:= by simp [any]
+
 /-! ### isEmpty -/
 
 @[simp]
@@ -757,4 +767,16 @@ public theorem difference_subset [LT α] [DecidableLT α] [StrictLT α] [Decidab
   rw [mem_difference]
   exact And.left
 
+/-! ### all₁ and any₁ -/
+
+@[simp]
+public theorem all₁_eq_all {s : Set α} {f : α → Bool} :
+  (s.all₁ λ ⟨elt, _⟩ => f elt) = s.all f
+:= by simp [all₁, all]
+
+@[simp]
+public theorem any₁_eq_any {s : Set α} {f : α → Bool} :
+  (s.any₁ λ ⟨elt, _⟩ => f elt) = s.any f
+:= by simp [any₁, any]
+
 end Cedar.Data.Set

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

@@ -631,7 +631,6 @@ theorem compile_well_typed_unaryApp
     ]
     split
     · simp [typeOf_bool]
-    · simp [typeOf_bool]
     · simp [hty_get_comp_expr]
       apply (wf_eq ?_ ?_ ?_).right
       any_goals assumption

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

@@ -112,8 +112,6 @@ theorem wf_δ_implies_wf_app_tags_keys {uid : EntityUID} {δ : SymEntityData} {
 theorem lit_tagOf (uid : EntityUID) (tag : Tag) :
   (tagOf (Term.entity uid) (Term.string tag)).isLiteral
 := by
-  simp only [tagOf, Term.isLiteral, List.cons.sizeOf_spec, Prod.mk.sizeOf_spec,
-    Term.prim.sizeOf_spec, TermPrim.entity.sizeOf_spec, TermPrim.string.sizeOf_spec,
-    List.nil.sizeOf_spec, List.attach₃, List.pmap, List.all_cons, List.all_nil, Bool.and_self]
+  simp [tagOf, Term.isLiteral]
 
 end Cedar.Thm