diff --git a/Dockerfile b/Dockerfile index 7b69919d2..a3d735f83 100644 --- a/Dockerfile +++ b/Dockerfile @@ -1,8 +1,8 @@ -FROM amazonlinux:2 AS prepare +FROM amazonlinux:2023 AS prepare RUN yum update -y \ && yum install -y \ - curl clang tar zip unzip python3 git xz \ + curl-minimal clang tar zip unzip python3 git xz \ make wget \ && yum clean all @@ -32,7 +32,10 @@ RUN git clone --depth 1 https://github.com/cedar-policy/cedar # Build the Lean formalization and extract to static C libraries WORKDIR $CEDAR_SPEC_ROOT/cedar-lean -RUN source /root/.profile && source ../cedar-drt/set_env_vars.sh && elan default "$(cat lean-toolchain)" && ../cedar-drt/build_lean_lib.sh +RUN source /root/.profile \ + && elan default "$(cat lean-toolchain)" \ + && source ../cedar-drt/set_env_vars.sh \ + && ../cedar-drt/build_lean_lib.sh # Build DRT WORKDIR $CEDAR_SPEC_ROOT/cedar-drt diff --git a/cedar-lean/Cedar/Data/LT.lean b/cedar-lean/Cedar/Data/LT.lean index f064b26f2..b545aafc0 100644 --- a/cedar-lean/Cedar/Data/LT.lean +++ b/cedar-lean/Cedar/Data/LT.lean @@ -45,6 +45,14 @@ theorem StrictLT.if_not_lt_gt_then_eq [LT α] [StrictLT α] (x y : α) : have h₄ := StrictLT.connected x y h₃ simp [h₁, h₂] at h₄ +theorem StrictLT.if_not_lt_eq_then_gt [LT α] [StrictLT α] (x y : α) : + ¬ x < y → ¬ x = y → x > y +:= by + intro h₁ h₂ + by_contra h₃ + have h₄ := StrictLT.connected x y h₂ + simp [h₁, h₃] at h₄ + theorem StrictLT.not_eq [LT α] [StrictLT α] (x y : α) : x < y → ¬ x = y := by @@ -62,69 +70,51 @@ end Cedar.Data open Cedar.Data -theorem List.lt_cons_cases [LT α] {x y : α} {xs ys : List α} : +theorem List.lt_cons_cases [LT α] [Cedar.Data.DecidableLT α] {x y : α} {xs ys : List α} : x :: xs < y :: ys → (x < y ∨ (¬ x < y ∧ ¬ y < x ∧ xs < ys)) := by intro h₁ - cases h₁ - case head _ h₁ => simp [h₁] - case tail _ h₁ h₂ h₃ => simp [h₁, h₂]; assumption + cases h₁ <;> simp_all [lex_lt, Decidable.em] theorem List.cons_lt_cons [LT α] [StrictLT α] (x : α) (xs ys : List α) : xs < ys → x :: xs < x :: ys := by intro h₁ - apply List.lt.tail (StrictLT.irreflexive x) (StrictLT.irreflexive x) h₁ + apply List.Lex.cons + simp only [lex_lt, h₁] -theorem List.slt_irrefl [LT α] [StrictLT α] (xs : List α) : +theorem List.slt_irrefl [LT α] [StrictLT α] [Cedar.Data.DecidableLT α] (xs : List α) : ¬ xs < xs := by induction xs case nil => by_contra; contradiction case cons _ _ hd tl ih => by_contra h₁ - have h₂ := StrictLT.irreflexive hd - cases tl - case nil => - have h₃ := List.lt_cons_cases h₁ - simp [h₂] at h₃ - contradiction - case cons _ _ hd' tl' => - have h₃ := List.lt_cons_cases h₁ - simp [h₂] at h₃ - contradiction + replace h₁ := List.lt_cons_cases h₁ + simp [StrictLT.irreflexive hd] at h₁ + contradiction theorem List.slt_trans [LT α] [StrictLT α] {xs ys zs : List α} : xs < ys → ys < zs → xs < zs := by intro h₁ h₂ cases h₁ - case nil => cases h₂ <;> apply List.lt.nil - case head _ _ xhd xtl yhd ytl h₃ => - cases h₂ - case head _ _ zhd ztl h₄ => - apply List.lt.head - apply StrictLT.transitive _ _ _ h₃ h₄ - case tail _ _ zhd ztl h₄ h₅ h₆ => - have h₇ := StrictLT.if_not_lt_gt_then_eq yhd zhd h₄ h₅ - subst h₇ - apply List.lt.head - exact h₃ - case tail _ _ xhd xtl yhd ytl h₃ h₄ h₅ => + case nil => cases h₂ <;> apply List.Lex.nil + case rel _ _ xhd xtl yhd ytl h₃ => + cases h₂ <;> apply List.Lex.rel + case rel _ _ zhd ztl h₄ => exact StrictLT.transitive _ _ _ h₃ h₄ + case cons _ _ ztl h₄ => exact h₃ + case cons _ _ xhd xtl ytl h₃ => cases h₂ - case head _ _ zhd ztl h₆ => - have h₇ := StrictLT.if_not_lt_gt_then_eq xhd yhd h₃ h₄ - subst h₇ - apply List.lt.head + case rel _ _ zhd ztl h₆ => + apply List.Lex.rel exact h₆ - case tail _ _ zhd ztl h₆ h₇ h₈ => - have h₉ := StrictLT.if_not_lt_gt_then_eq xhd yhd h₃ h₄ - subst h₉ - apply List.lt.tail h₆ h₇ - apply List.slt_trans h₅ h₈ + case cons _ _ ztl h₆ => + apply List.Lex.cons + exact List.slt_trans h₃ h₆ -theorem List.lt_asymm [LT α] [StrictLT α] {xs ys : List α} : +theorem List.slt_asymm [LT α] [StrictLT α] [Cedar.Data.DecidableLT α] {xs ys : List α} : xs < ys → ¬ ys < xs := by intro h₁ @@ -146,38 +136,42 @@ theorem List.lt_conn [LT α] [StrictLT α] {xs ys : List α} : := by intro h₁ by_contra h₂ - simp [not_or] at h₂ - have ⟨h₂, h₃⟩ := h₂ + simp only [not_or] at h₂ + replace ⟨h₂, h₃⟩ := h₂ cases xs <;> cases ys case nil.nil => contradiction - case nil.cons _ _ xhd xtl _ => - have h₄ := List.lt.nil xhd xtl - contradiction - case cons.nil _ _ yhd ytl _ => - have h₄ := List.lt.nil yhd ytl - contradiction - case cons.cons _ _ xhd xtl yhd ytl _ => + case nil.cons xhd xtl => + simp_all only [ne_eq, nil_eq, not_false_eq_true, and_self, nil_lt_cons, not_true_eq_false] + case cons.nil yhd ytl => + simp_all only [ne_eq, not_false_eq_true, and_self, not_lt_nil, nil_lt_cons, not_true_eq_false] + case cons.cons xhd xtl yhd ytl => by_cases (xhd < yhd) case pos h₄ => - have h₅ := List.lt.head xtl ytl h₄ + have h₅ : xhd :: xtl < yhd :: ytl := List.Lex.rel h₄ contradiction case neg h₄ => - by_cases (yhd < xhd) + by_cases (xhd = yhd) case pos h₅ => - have h₆ := List.lt.head ytl xtl h₅ + subst yhd + suffices xtl < ytl ∨ ytl < xtl by + cases this <;> rename_i h₅ + · apply h₂ ; clear h₂ + apply List.Lex.cons ; simp only [lex_lt] + exact h₅ + · apply h₃ ; clear h₃ + apply List.Lex.cons ; simp only [lex_lt] + exact h₅ + apply List.lt_conn (xs := xtl) (ys := ytl) + intro h₅ + subst ytl contradiction case neg h₅ => - have h₆ := StrictLT.if_not_lt_gt_then_eq xhd yhd h₄ h₅ - subst h₆ - simp at h₁ - cases (List.lt_conn h₁) <;> rename_i h₆ - · have h₇ := List.cons_lt_cons xhd xtl ytl h₆ - contradiction - · have h₇ := List.cons_lt_cons xhd ytl xtl h₆ - contradiction - -instance List.strictLT (α) [LT α] [StrictLT α] : StrictLT (List α) where - asymmetric _ _ := List.lt_asymm + apply h₃ ; clear h₃ + apply List.Lex.rel + exact StrictLT.if_not_lt_eq_then_gt xhd yhd h₄ h₅ + +instance List.strictLT (α) [LT α] [StrictLT α] [Cedar.Data.DecidableLT α] : StrictLT (List α) where + asymmetric _ _ := List.slt_asymm transitive _ _ _ := List.slt_trans connected _ _ := List.lt_conn diff --git a/cedar-lean/Cedar/Data/List.lean b/cedar-lean/Cedar/Data/List.lean index 4174c243d..04514fbe2 100644 --- a/cedar-lean/Cedar/Data/List.lean +++ b/cedar-lean/Cedar/Data/List.lean @@ -29,7 +29,7 @@ open Cedar.Data ----- Definitions ----- -def insertCanonical [LT β] [DecidableLT β] (f : α → β) (x : α) (xs : List α) : List α := +def insertCanonical [LT β] [Cedar.Data.DecidableLT β] (f : α → β) (x : α) (xs : List α) : List α := match xs with | [] => [x] | hd :: tl => @@ -46,7 +46,7 @@ If the ordering relation < on β is strict, then `canonicalize` returns a canonical representation of the input list, which is sorted and free of duplicates. -/ -def canonicalize [LT β] [DecidableLT β] (f : α → β) : List α → List α +def canonicalize [LT β] [Cedar.Data.DecidableLT β] (f : α → β) : List α → List α | [] => [] | hd :: tl => insertCanonical f hd (canonicalize f tl) diff --git a/cedar-lean/Cedar/Data/Map.lean b/cedar-lean/Cedar/Data/Map.lean index 120ddda0f..a3ab9be52 100644 --- a/cedar-lean/Cedar/Data/Map.lean +++ b/cedar-lean/Cedar/Data/Map.lean @@ -104,8 +104,8 @@ def mapMOnKeys {α β γ} [LT γ] [DecidableLT γ] [Monad m] (f : α → m γ) ( instance [LT (Prod α β)] : LT (Map α β) where lt a b := a.kvs < b.kvs -instance decLt [LT (Prod α β)] [DecidableRel (α:=(Prod α β)) (·<·)] : (n m : Map α β) → Decidable (n < m) - | .mk nkvs, .mk mkvs => List.hasDecidableLt nkvs mkvs +instance decLt [LT (Prod α β)] [DecidableEq (Prod α β)] [Cedar.Data.DecidableLT (Prod α β)] : (n m : Map α β) → Decidable (n < m) + | .mk nkvs, .mk mkvs => List.decidableLT nkvs mkvs -- enables ∈ notation for map keys instance : Membership α (Map α β) where diff --git a/cedar-lean/Cedar/Data/Set.lean b/cedar-lean/Cedar/Data/Set.lean index 234cfae14..3c19436d0 100644 --- a/cedar-lean/Cedar/Data/Set.lean +++ b/cedar-lean/Cedar/Data/Set.lean @@ -124,8 +124,8 @@ def foldl {α β} (f : α → β → α) (init : α) (s : Set β) : α := instance [LT α] : LT (Set α) where lt a b := a.elts < b.elts -instance decLt [LT α] [DecidableLT α] : (n m : Set α) → Decidable (n < m) - | .mk nelts, .mk melts => List.hasDecidableLt nelts melts +instance decLt [LT α] [DecidableEq α] [Cedar.Data.DecidableLT α] : (n m : Set α) → Decidable (n < m) + | .mk nelts, .mk melts => List.decidableLT nelts melts -- enables ∅ instance : EmptyCollection (Set α) where diff --git a/cedar-lean/Cedar/Data/SizeOf.lean b/cedar-lean/Cedar/Data/SizeOf.lean index 111c1e91f..986928d50 100644 --- a/cedar-lean/Cedar/Data/SizeOf.lean +++ b/cedar-lean/Cedar/Data/SizeOf.lean @@ -40,15 +40,7 @@ theorem sizeOf_lt_of_value [SizeOf α] [SizeOf β] {m : Map α β} {k : α} {v : have m1_lt_m : sizeOf m.1 < sizeOf m := by simp only [sizeOf, Map._sizeOf_1] omega - let a := sizeOf v - let c := sizeOf m.1 - let d := sizeOf m - have v_lt_m1 : a < c := by apply Nat.lt_trans v_lt_kv h - have v_lt_m : a < d := by apply Nat.lt_trans v_lt_m1 m1_lt_m - have ha : a = sizeOf v := by simp - have hd : d = sizeOf m := by simp - rw [ha, hd] at v_lt_m - exact v_lt_m + omega theorem sizeOf_lt_of_kvs [SizeOf α] [SizeOf β] (m : Map α β) : sizeOf m.kvs < sizeOf m @@ -66,9 +58,6 @@ theorem sizeOf_lt_of_tl [SizeOf α] [SizeOf β] {m : Map α β} {tl : List (α simp only unfold kvs at h simp only [h, List.cons.sizeOf_spec, Prod.mk.sizeOf_spec] - generalize sizeOf k = kn - generalize sizeOf v = vn - generalize sizeOf tl = tn omega end Cedar.Data.Map diff --git a/cedar-lean/Cedar/Thm/Authorization/Authorizer.lean b/cedar-lean/Cedar/Thm/Authorization/Authorizer.lean index 7bfa036ba..4a8854d51 100644 --- a/cedar-lean/Cedar/Thm/Authorization/Authorizer.lean +++ b/cedar-lean/Cedar/Thm/Authorization/Authorizer.lean @@ -306,7 +306,7 @@ theorem Except.isOk_iff_exists {x : Except ε α} : := by cases x <;> simp [Except.isOk, Except.toBool] -theorem if_mapM_doesn't_fail_on_list_then_doesn't_fail_on_set [LT α] [DecidableLT α] [StrictLT α] {f : α → Except ε β} {as : List α} : +theorem if_mapM_doesn't_fail_on_list_then_doesn't_fail_on_set [LT α] [Cedar.Data.DecidableLT α] [StrictLT α] {f : α → Except ε β} {as : List α} : Except.isOk (as.mapM f) → Except.isOk ((Set.elts (Set.make as)).mapM f) := by diff --git a/cedar-lean/Cedar/Thm/Data/LT.lean b/cedar-lean/Cedar/Thm/Data/LT.lean index 56d528aae..02b1640cd 100644 --- a/cedar-lean/Cedar/Thm/Data/LT.lean +++ b/cedar-lean/Cedar/Thm/Data/LT.lean @@ -164,13 +164,16 @@ instance Ext.strictLT : StrictLT Ext where instance Name.strictLT : StrictLT Name where asymmetric a b := by - simp [LT.lt, Name.lt] - apply List.lt_asymm + simp only [LT.lt, Bool.not_eq_true] + simp only [Name.lt, decide_eq_true_eq, decide_eq_false_iff_not, List.not_lt] + apply List.slt_asymm transitive a b c := by - simp [LT.lt, Name.lt] + simp only [LT.lt] + simp only [Name.lt, decide_eq_true_eq] apply List.slt_trans connected a b := by - simp [LT.lt, Name.lt] + simp only [ne_eq, LT.lt] + simp only [Name.lt, decide_eq_true_eq] intro h₁ apply List.lt_conn by_contra h₂ @@ -203,24 +206,22 @@ theorem EntityUID.lt_asymm {a b : EntityUID} : theorem EntityUID.lt_trans {a b c : EntityUID} : a < b → b < c → a < c := by - simp [LT.lt, EntityUID.lt] + simp only [LT.lt] + simp only [EntityUID.lt, Bool.decide_or, Bool.decide_and, Bool.or_eq_true, decide_eq_true_eq, + Bool.and_eq_true] intro h₁ h₂ rcases h₁ with h₁ | h₁ <;> rcases h₂ with h₂ | h₂ - · have h₃ := Name.strictLT.transitive a.ty b.ty c.ty h₁ h₂ - simp only [LT.lt] at h₃ - simp [h₃] - · have ⟨h₂, _⟩ := h₂ + · simp [Name.strictLT.transitive a.ty b.ty c.ty h₁ h₂] + · replace ⟨h₂, _⟩ := h₂ simp [h₂] at h₁ simp [h₁] - · have ⟨h₁, _⟩ := h₁ + · replace ⟨h₁, _⟩ := h₁ simp [←h₁] at h₂ simp [h₂] - · have ⟨hl₁, hr₁⟩ := h₁ - have ⟨hl₂, hr₂⟩ := h₂ + · replace ⟨hl₁, hr₁⟩ := h₁ ; clear h₁ + replace ⟨hl₂, hr₂⟩ := h₂ ; clear h₂ simp [hl₁] at * ; simp [hl₂] at * - have h₃ := String.strictLT.transitive a.eid b.eid c.eid hr₁ hr₂ - simp only [LT.lt] at h₃ - simp [h₃] + simp [String.strictLT.transitive a.eid b.eid c.eid hr₁ hr₂] theorem EntityUID.lt_conn {a b : EntityUID} : a ≠ b → (a < b ∨ b < a) @@ -387,7 +388,8 @@ theorem ValueAttrs.lt_asym {vs₁ vs₂: List (Attr × Value)} : have h₂ := String.strictLT.asymmetric a₁ a₂ h₁ have h₃ := StrictLT.not_eq a₁ a₂ h₁ rw [eq_comm] at h₃ - simp [h₂, h₃] + simp only [h₃, false_implies, and_true, ge_iff_le] + simp_all only [String.not_lt] case inr => have ⟨hl₁, h₂⟩ := h₁ subst hl₁ diff --git a/cedar-lean/Cedar/Thm/Data/List/Basic.lean b/cedar-lean/Cedar/Thm/Data/List/Basic.lean index 63ac38924..d94667da2 100644 --- a/cedar-lean/Cedar/Thm/Data/List/Basic.lean +++ b/cedar-lean/Cedar/Thm/Data/List/Basic.lean @@ -294,7 +294,7 @@ theorem sortedBy_cons [LT β] [StrictLT β] {f : α → β} {x : α} {ys : List apply h₂ simp only [mem_cons, true_or] -theorem mem_of_sortedBy_unique {α β} [LT β] [StrictLT β] [DecidableLT β] [DecidableEq β] +theorem mem_of_sortedBy_unique {α β} [LT β] [StrictLT β] [Cedar.Data.DecidableLT β] [DecidableEq β] {f : α → β} {x y : α} {xs : List α} : xs.SortedBy f → x ∈ xs → y ∈ xs → f x = f y → x = y @@ -317,7 +317,7 @@ theorem mem_of_sortedBy_unique {α β} [LT β] [StrictLT β] [DecidableLT β] [D simp only [hf, StrictLT.irreflexive] at hlt · exact ih hx hy -theorem mem_of_sortedBy_implies_find? {α β} [LT β] [StrictLT β] [DecidableLT β] [DecidableEq β] +theorem mem_of_sortedBy_implies_find? {α β} [LT β] [StrictLT β] [Cedar.Data.DecidableLT β] [DecidableEq β] {f : α → β} {x : α} {xs : List α} : x ∈ xs → xs.SortedBy f → xs.find? (fun y => f y == f x) = x @@ -384,7 +384,7 @@ theorem map_eq_implies_sortedBy [LT β] [StrictLT β] {f : α → β} {g : γ apply sortedBy_implies_head_lt_tail h₂ simp only [mem_cons, true_or] -theorem filter_sortedBy [LT β] [StrictLT β] [DecidableLT β] {f : α → β} (p : α → Bool) {xs : List α} : +theorem filter_sortedBy [LT β] [StrictLT β] [Cedar.Data.DecidableLT β] {f : α → β} (p : α → Bool) {xs : List α} : SortedBy f xs → SortedBy f (xs.filter p) := by intro h₁ @@ -401,7 +401,7 @@ theorem filter_sortedBy [LT β] [StrictLT β] [DecidableLT β] {f : α → β} ( exact h₂.left · exact ih -theorem filterMap_sortedBy [LT β] [StrictLT β] [DecidableLT β] {f : α → β} {g : α → Option γ} {f' : γ → β} {xs : List α} : +theorem filterMap_sortedBy [LT β] [StrictLT β] [Cedar.Data.DecidableLT β] {f : α → β} {g : α → Option γ} {f' : γ → β} {xs : List α} : (∀ x y, g x = some y → f x = f' y) → SortedBy f xs → SortedBy f' (xs.filterMap g) diff --git a/cedar-lean/Cedar/Thm/Data/List/Canonical.lean b/cedar-lean/Cedar/Thm/Data/List/Canonical.lean index 4455fcf33..7079e8a27 100644 --- a/cedar-lean/Cedar/Thm/Data/List/Canonical.lean +++ b/cedar-lean/Cedar/Thm/Data/List/Canonical.lean @@ -30,11 +30,11 @@ open Cedar.Data /-! ### insertCanonical -/ -theorem insertCanonical_singleton [LT β] [DecidableLT β] (f : α → β) (x : α) : +theorem insertCanonical_singleton [LT β] [Cedar.Data.DecidableLT β] (f : α → β) (x : α) : insertCanonical f x [] = [x] := by unfold insertCanonical; rfl -theorem insertCanonical_not_nil [DecidableEq β] [LT β] [DecidableLT β] (f : α → β) (x : α) (xs : List α) : +theorem insertCanonical_not_nil [DecidableEq β] [LT β] [Cedar.Data.DecidableLT β] (f : α → β) (x : α) (xs : List α) : insertCanonical f x xs ≠ [] := by unfold insertCanonical @@ -46,7 +46,7 @@ theorem insertCanonical_not_nil [DecidableEq β] [LT β] [DecidableLT β] (f : split at h <;> try trivial split at h <;> trivial -theorem insertCanonical_sortedBy [LT β] [StrictLT β] [DecidableLT β] {f : α → β} {xs : List α} (x : α) : +theorem insertCanonical_sortedBy [LT β] [StrictLT β] [Cedar.Data.DecidableLT β] {f : α → β} {xs : List α} (x : α) : SortedBy f xs → SortedBy f (insertCanonical f x xs) := by @@ -85,7 +85,7 @@ theorem insertCanonical_sortedBy [LT β] [StrictLT β] [DecidableLT β] {f : α case cons_nil => exact SortedBy.cons_nil case cons_cons h₅ h₆ => exact SortedBy.cons_cons (by simp only [h₄, h₆]) h₅ -theorem insertCanonical_cases [LT β] [DecidableLT β] (f : α → β) (x y : α) (ys : List α) : +theorem insertCanonical_cases [LT β] [Cedar.Data.DecidableLT β] (f : α → β) (x y : α) (ys : List α) : (f x < f y ∧ insertCanonical f x (y :: ys) = x :: y :: ys) ∨ (¬ f x < f y ∧ f x > f y ∧ insertCanonical f x (y :: ys) = y :: insertCanonical f x ys) ∨ (¬ f x < f y ∧ ¬ f x > f y ∧ insertCanonical f x (y :: ys) = x :: ys) @@ -102,7 +102,7 @@ theorem insertCanonical_cases [LT β] [DecidableLT β] (f : α → β) (x y : α case pos _ _ h₃ => simp [h₃, h₁] case neg _ _ h₃ => simp [h₃] -theorem insertCanonical_subset [LT β] [DecidableLT β] (f : α → β) (x : α) (xs : List α) : +theorem insertCanonical_subset [LT β] [Cedar.Data.DecidableLT β] (f : α → β) (x : α) (xs : List α) : insertCanonical f x xs ⊆ x :: xs := by induction xs @@ -117,7 +117,7 @@ theorem insertCanonical_subset [LT β] [DecidableLT β] (f : α → β) (x : α) · simp only [h₁, cons_subset, mem_cons, true_or, true_and] exact Subset.trans (List.subset_cons_self hd tl) (List.subset_cons_self x (hd :: tl)) -theorem insertCanonical_equiv [LT α] [StrictLT α] [DecidableLT α] (x : α) (xs : List α) : +theorem insertCanonical_equiv [LT α] [StrictLT α] [Cedar.Data.DecidableLT α] (x : α) (xs : List α) : x :: xs ≡ insertCanonical id x xs := by unfold insertCanonical @@ -173,7 +173,7 @@ theorem insertCanonical_equiv [LT α] [StrictLT α] [DecidableLT α] (x : α) (x apply cons_equiv_cons exact ih -theorem insertCanonical_preserves_forallᵥ {α β γ} [LT α] [StrictLT α] [DecidableLT α] {p : β → γ → Prop} +theorem insertCanonical_preserves_forallᵥ {α β γ} [LT α] [StrictLT α] [Cedar.Data.DecidableLT α] {p : β → γ → Prop} {kv₁ : α × β} {kv₂ : α × γ} {kvs₁ : List (α × β)} {kvs₂ : List (α × γ)} (h₁ : kv₁.fst = kv₂.fst ∧ p kv₁.snd kv₂.snd) (h₂ : Forallᵥ p kvs₁ kvs₂) : @@ -202,7 +202,7 @@ theorem insertCanonical_preserves_forallᵥ {α β γ} [LT α] [StrictLT α] [De · contradiction · exact Forall₂.cons (by exact h₁) (by exact h₄) -theorem insertCanonical_map_fst {α β γ} [LT α] [StrictLT α] [DecidableLT α] (xs : List (α × β)) (f : β → γ) (x : α × β) : +theorem insertCanonical_map_fst {α β γ} [LT α] [StrictLT α] [Cedar.Data.DecidableLT α] (xs : List (α × β)) (f : β → γ) (x : α × β) : insertCanonical Prod.fst (Prod.map id f x) (map (Prod.map id f) xs) = map (Prod.map id f) (insertCanonical Prod.fst x xs) := by @@ -218,23 +218,23 @@ theorem insertCanonical_map_fst {α β γ} [LT α] [StrictLT α] [DecidableLT α simp [ih, Prod.map] · simp [Prod.map] -theorem insertCanonical_map_fst_canonicalize {α β γ} [LT α] [StrictLT α] [DecidableLT α] (xs : List (α × β)) (f : β → γ) (x : α × β) : +theorem insertCanonical_map_fst_canonicalize {α β γ} [LT α] [StrictLT α] [Cedar.Data.DecidableLT α] (xs : List (α × β)) (f : β → γ) (x : α × β) : insertCanonical Prod.fst (Prod.map id f x) (canonicalize Prod.fst (map (Prod.map id f) xs)) = map (Prod.map id f) (insertCanonical Prod.fst x (canonicalize Prod.fst xs)) := by induction xs generalizing x case nil => simp [insertCanonical, canonicalize, Prod.map] case cons hd tl ih => - simp only [canonicalize, ih hd] + simp only [map_cons, canonicalize, ih hd] apply insertCanonical_map_fst (insertCanonical Prod.fst hd (canonicalize Prod.fst tl)) /-! ## canonicalize -/ -theorem canonicalize_nil [LT β] [DecidableLT β] (f : α → β) : +theorem canonicalize_nil [LT β] [Cedar.Data.DecidableLT β] (f : α → β) : canonicalize f [] = [] := by unfold canonicalize; rfl -theorem canonicalize_nil' [DecidableEq β] [LT β] [DecidableLT β] (f : α → β) (xs : List α) : +theorem canonicalize_nil' [DecidableEq β] [LT β] [Cedar.Data.DecidableLT β] (f : α → β) (xs : List α) : xs = [] ↔ (canonicalize f xs) = [] := by constructor @@ -251,7 +251,7 @@ theorem canonicalize_nil' [DecidableEq β] [LT β] [DecidableLT β] (f : α → apply insertCanonical_not_nil f x (canonicalize f xs) exact h₁ -theorem canonicalize_not_nil [DecidableEq β] [LT β] [DecidableLT β] (f : α → β) (xs : List α) : +theorem canonicalize_not_nil [DecidableEq β] [LT β] [Cedar.Data.DecidableLT β] (f : α → β) (xs : List α) : xs ≠ [] ↔ (canonicalize f xs) ≠ [] := by constructor @@ -267,14 +267,14 @@ theorem canonicalize_not_nil [DecidableEq β] [LT β] [DecidableLT β] (f : α intro h₀ cases xs <;> simp only [ne_eq, reduceCtorEq, not_false_eq_true, not_true_eq_false] at * -theorem canonicalize_cons [LT β] [DecidableLT β] (f : α → β) (xs : List α) (a : α) : +theorem canonicalize_cons [LT β] [Cedar.Data.DecidableLT β] (f : α → β) (xs : List α) (a : α) : canonicalize f xs = canonicalize f ys → canonicalize f (a :: xs) = canonicalize f (a :: ys) := by intro h₁ unfold canonicalize simp [h₁] -theorem canonicalize_sortedBy [LT β] [StrictLT β] [DecidableLT β] (f : α → β) (xs : List α) : +theorem canonicalize_sortedBy [LT β] [StrictLT β] [Cedar.Data.DecidableLT β] (f : α → β) (xs : List α) : SortedBy f (canonicalize f xs) := by induction xs @@ -284,7 +284,7 @@ theorem canonicalize_sortedBy [LT β] [StrictLT β] [DecidableLT β] (f : α → apply insertCanonical_sortedBy exact ih -theorem sortedBy_implies_canonicalize_eq [LT β] [StrictLT β] [DecidableLT β] {f : α → β} {xs : List α} : +theorem sortedBy_implies_canonicalize_eq [LT β] [StrictLT β] [Cedar.Data.DecidableLT β] {f : α → β} {xs : List α} : SortedBy f xs → (canonicalize f xs) = xs := by intro h₁ @@ -296,7 +296,7 @@ theorem sortedBy_implies_canonicalize_eq [LT β] [StrictLT β] [DecidableLT β] specialize ih h₁ simp [ih, insertCanonical, h₂] -theorem canonicalize_subseteq [LT β] [StrictLT β] [DecidableLT β] (f : α → β) (xs : List α) : +theorem canonicalize_subseteq [LT β] [StrictLT β] [Cedar.Data.DecidableLT β] (f : α → β) (xs : List α) : xs.canonicalize f ⊆ xs := by induction xs <;> simp only [canonicalize, Subset.refl] @@ -308,7 +308,7 @@ theorem canonicalize_subseteq [LT β] [StrictLT β] [DecidableLT β] (f : α → simp only [subset_cons_self] /-- Corollary of `canonicalize_subseteq` -/ -theorem in_canonicalize_in_list [LT β] [StrictLT β] [DecidableLT β] {f : α → β} {x : α} {xs : List α} : +theorem in_canonicalize_in_list [LT β] [StrictLT β] [Cedar.Data.DecidableLT β] {f : α → β} {x : α} {xs : List α} : x ∈ xs.canonicalize f → x ∈ xs := by intro h₁ @@ -321,7 +321,7 @@ Note that `canonicalize_equiv` does not hold for all functions `f`. To see why, consider xs = [(1, false), (1, true)], f = Prod.fst. Then `canonicalize f xs = [(1, false)] !≡ xs`. -/ -theorem canonicalize_equiv [LT α] [StrictLT α] [DecidableLT α] (xs : List α) : +theorem canonicalize_equiv [LT α] [StrictLT α] [Cedar.Data.DecidableLT α] (xs : List α) : xs ≡ canonicalize id xs := by induction xs @@ -339,7 +339,7 @@ theorem canonicalize_equiv [LT α] [StrictLT α] [DecidableLT α] (xs : List α) Note that `equiv_implies_canonical_eq` does not hold for all functions `f`. To see why, consider the `example` immediately below this. -/ -theorem equiv_implies_canonical_eq [LT α] [StrictLT α] [DecidableLT α] (xs ys : List α) : +theorem equiv_implies_canonical_eq [LT α] [StrictLT α] [Cedar.Data.DecidableLT α] (xs ys : List α) : xs ≡ ys → (canonicalize id xs) = (canonicalize id ys) := by intro h₁ @@ -371,7 +371,7 @@ example : simp [List.Equiv] decide -theorem canonicalize_idempotent {α β} [LT β] [StrictLT β] [DecidableLT β] (f : α → β) (xs : List α) : +theorem canonicalize_idempotent {α β} [LT β] [StrictLT β] [Cedar.Data.DecidableLT β] (f : α → β) (xs : List α) : canonicalize f (canonicalize f xs) = canonicalize f xs := sortedBy_implies_canonicalize_eq (canonicalize_sortedBy f xs) @@ -384,7 +384,7 @@ Then `(canonicalize f xs).filter p = []` but `(xs.filter p).canonicalize f = [(1 #eval (canonicalize Prod.fst [(1, false), (1, true)]).filter Prod.snd #eval ([(1, false), (1, true)].filter Prod.snd).canonicalize Prod.fst -/ -theorem canonicalize_id_filter {α} [LT α] [StrictLT α] [DecidableLT α] (p : α → Bool) (xs : List α) : +theorem canonicalize_id_filter {α} [LT α] [StrictLT α] [Cedar.Data.DecidableLT α] (p : α → Bool) (xs : List α) : (canonicalize id xs).filter p = (xs.filter p).canonicalize id := by have h₁ : (canonicalize id xs).filter p ≡ xs.filter p := by @@ -397,7 +397,7 @@ theorem canonicalize_id_filter {α} [LT α] [StrictLT α] [DecidableLT α] (p : (canonicalize_sortedBy id (filter p xs)) (Equiv.trans h₁ h₂) -theorem canonicalize_preserves_forallᵥ {α β γ} [LT α] [StrictLT α] [DecidableLT α] (p : β → γ → Prop) (kvs₁ : List (α × β)) (kvs₂ : List (α × γ)) : +theorem canonicalize_preserves_forallᵥ {α β γ} [LT α] [StrictLT α] [Cedar.Data.DecidableLT α] (p : β → γ → Prop) (kvs₁ : List (α × β)) (kvs₂ : List (α × γ)) : List.Forallᵥ p kvs₁ kvs₂ → List.Forallᵥ p (List.canonicalize Prod.fst kvs₁) (List.canonicalize Prod.fst kvs₂) := by @@ -410,7 +410,7 @@ theorem canonicalize_preserves_forallᵥ {α β γ} [LT α] [StrictLT α] [Decid have h₄ := canonicalize_preserves_forallᵥ p tl₁ tl₂ h₃ apply insertCanonical_preserves_forallᵥ h₂ h₄ -theorem canonicalize_of_map_fst {α β γ} [LT α] [StrictLT α] [DecidableLT α] (xs : List (α × β)) (f : β → γ) : +theorem canonicalize_of_map_fst {α β γ} [LT α] [StrictLT α] [Cedar.Data.DecidableLT α] (xs : List (α × β)) (f : β → γ) : List.canonicalize Prod.fst (List.map (Prod.map id f) xs) = List.map (Prod.map id f) (List.canonicalize Prod.fst xs) := by diff --git a/cedar-lean/Cedar/Thm/Validation/Typechecker/BinaryApp.lean b/cedar-lean/Cedar/Thm/Validation/Typechecker/BinaryApp.lean index 292de993b..240182a90 100644 --- a/cedar-lean/Cedar/Thm/Validation/Typechecker/BinaryApp.lean +++ b/cedar-lean/Cedar/Thm/Validation/Typechecker/BinaryApp.lean @@ -659,7 +659,6 @@ theorem mapM'_eval_lits_eq_prims {ps : List Prim} {vs : List Value} {request : R subst h₁ simp only [List.map_nil] case cons hd tl => - simp only [List.mapM', bind_pure_comp] at h₁ cases h₂ : evaluate (Expr.lit hd) request entities <;> simp [h₂] at h₁ cases h₃ : List.mapM' (fun x => evaluate x request entities) (List.map Expr.lit tl) <;> simp [h₃] at h₁ rename_i vhd vtl diff --git a/cedar-lean/Cedar/Thm/Validation/Typechecker/Call.lean b/cedar-lean/Cedar/Thm/Validation/Typechecker/Call.lean index 369ee5306..f580023ec 100644 --- a/cedar-lean/Cedar/Thm/Validation/Typechecker/Call.lean +++ b/cedar-lean/Cedar/Thm/Validation/Typechecker/Call.lean @@ -318,22 +318,22 @@ theorem typeOf_of_unary_call_inversion {xs : List Expr} {c : Capabilities} {env simp only [List.mapM₁] at h₁ cases xs case nil => - simp only [List.mapM, List.mapM.loop, pure, Except.pure, List.reverse_nil, Except.ok.injEq, - List.ne_cons_self] at h₁ + simp only [List.mapM, List.attach_nil, List.mapM.loop, pure, Except.pure, List.reverse_nil, + Except.ok.injEq, List.ne_cons_self] at h₁ case cons hd₁ tl₁ => cases tl₁ case nil => - simp only [List.mapM, List.mapM.loop, List.reverse_cons, List.reverse_nil, List.nil_append, - bind_pure_comp] at h₁ - cases h₂ : justType (typeOf hd₁ c env) <;> - simp only [h₂, Except.map_error, reduceCtorEq, - Except.map_ok, Except.ok.injEq, List.cons.injEq, and_true] at h₁ - simp only [justType, Except.map] at h₂ - subst h₁ - split at h₂ <;> simp at h₂ - rename_i res₁ h₃ - exists hd₁, res₁.snd - simp only [ResultType.typeOf, Except.map, h₃, ← h₂, and_self] + simp only [List.attach_cons, List.attach_nil, List.map_nil, List.mapM_cons, List.mapM_nil, + bind_pure_comp, map_pure] at h₁ + cases h₂ : justType (typeOf hd₁ c env) + · simp_all only [justType, List.cons.injEq, and_true, exists_and_left, exists_eq_left', Except.map_error, Except.map_ok, Except.ok.injEq] + simp at h₁ + · simp only [List.cons.injEq, and_true, exists_and_left, exists_eq_left'] at * + simp_all only [Except.map_ok, Except.ok.injEq, List.cons.injEq, and_true] + subst h₁ ; rename_i ty₁ + cases h₁ : typeOf hd₁ c env + <;> simp only [justType, h₁, Except.map, Except.ok.injEq, reduceCtorEq] at h₂ + simp [h₂, ResultType.typeOf, Except.map.eq_2] case cons hd₂ tl₂ => simp only [List.attach_def, List.pmap, List.mapM_cons, List.mapM_pmap_subtype (fun x => justType (typeOf x c env)), bind_assoc, pure_bind] at h₁ diff --git a/cedar-lean/Cedar/Thm/Validation/Typechecker/Record.lean b/cedar-lean/Cedar/Thm/Validation/Typechecker/Record.lean index 8a8f23e45..178a665c9 100644 --- a/cedar-lean/Cedar/Thm/Validation/Typechecker/Record.lean +++ b/cedar-lean/Cedar/Thm/Validation/Typechecker/Record.lean @@ -242,10 +242,11 @@ theorem type_of_record_is_sound_err {axs : List (Attr × Expr)} {c₁ : Capabili simp [List.mapM₂, List.attach₂, pure, Except.pure] at h₄ case cons hd tl => cases h₃ ; rename_i hd' tl' hh₃ ht₃ - simp [List.mapM₂, List.attach₂] at h₄ - cases h₅ : bindAttr hd.fst (evaluate hd.snd request entities) <;> simp [h₅] at h₄ + simp only [List.mapM_cons, List.mapM₂, List.attach₂] at h₄ + cases h₅ : bindAttr hd.fst (evaluate hd.snd request entities) <;> simp only [h₅] at h₄ case error e => - simp [bindAttr] at h₅ + simp only [bindAttr] at h₅ + simp only [bind_pure_comp, Except.bind_err, Except.error.injEq] at h₄ cases h₆ : evaluate hd.snd request entities <;> simp [h₆] at h₅ subst h₄ h₅ specialize ih hd @@ -257,14 +258,13 @@ theorem type_of_record_is_sound_err {axs : List (Attr × Expr)} {c₁ : Capabili simp [EvaluatesTo, h₆] at ih exact ih case ok vhd => - let f := fun (x : Attr × Expr) => bindAttr x.fst (evaluate x.snd request entities) - cases h₅ : tl.mapM f <;> simp [h₅, pure, Except.pure] at h₄ + cases h₅ : tl.mapM λ x => bindAttr x.fst (evaluate x.snd request entities) <;> simp [h₅, pure, Except.pure] at h₄ rw [eq_comm] at h₄ ; subst h₄ - apply @type_of_record_is_sound_err + exact @type_of_record_is_sound_err tl c₁ env request entities tl' err (by intro axᵢ h ; apply ih ; simp [h]) h₁ h₂ ht₃ - (by simp [List.mapM₂, List.attach₂, List.mapM_pmap_subtype f, h₅]) + (by simp [List.mapM₂, List.attach₂, List.mapM_pmap_subtype, h₅]) theorem type_of_record_is_sound {axs : List (Attr × Expr)} {c₁ c₂ : Capabilities} {env : Environment} {ty : TypedExpr} {request : Request} {entities : Entities} @@ -278,11 +278,12 @@ theorem type_of_record_is_sound {axs : List (Attr × Expr)} {c₁ c₂ : Capabil have ⟨h₆, rty, h₅, h₄⟩ := type_of_record_inversion h₃ subst h₆ ; rw [h₅] apply And.intro empty_guarded_capabilities_invariant - simp [EvaluatesTo, evaluate, List.mapM₂, List.attach₂] + simp only [EvaluatesTo, evaluate] + simp only [do_ok, do_error] + simp only [List.mapM₂, List.attach₂] let f := fun (x : Attr × Expr) => bindAttr x.fst (evaluate x.snd request entities) - simp [List.mapM_pmap_subtype f] - cases h₅ : (axs.mapM f) <;> - simp [h₅] + rw [List.mapM_pmap_subtype f] + cases h₅ : (axs.mapM f) <;> simp [h₅] case error err => simp [type_is_inhabited] exact type_of_record_is_sound_err ih h₁ h₂ h₄ h₅ diff --git a/cedar-lean/DiffTest/Parser.lean b/cedar-lean/DiffTest/Parser.lean index 49de940a3..fb060fd5c 100644 --- a/cedar-lean/DiffTest/Parser.lean +++ b/cedar-lean/DiffTest/Parser.lean @@ -419,11 +419,11 @@ formalization standardizes on ancestor information. The definitions and utility functions below are used to convert the descendant representation to the ancestor representation. -/ -def findInMapValues [LT α] [DecidableEq α] [DecidableLT α] (m : Map α (Set α)) (k₁ : α) : Set α := +def findInMapValues [LT α] [DecidableEq α] [Cedar.Data.DecidableLT α] (m : Map α (Set α)) (k₁ : α) : Set α := let setOfSets := List.map (λ (k₂,v) => if v.contains k₁ then Set.singleton k₂ else Set.empty) m.toList setOfSets.foldl (λ acc v => acc.union v) Set.empty -def descendantsToAncestors [LT α] [DecidableEq α] [DecidableLT α] (descendants : Map α (Set α)) : Map α (Set α) := +def descendantsToAncestors [LT α] [DecidableEq α] [Cedar.Data.DecidableLT α] (descendants : Map α (Set α)) : Map α (Set α) := Map.make (List.map (λ (k,_) => (k, findInMapValues descendants k)) descendants.toList) diff --git a/cedar-lean/lakefile.lean b/cedar-lean/lakefile.lean index 44525d3a7..f84cca096 100644 --- a/cedar-lean/lakefile.lean +++ b/cedar-lean/lakefile.lean @@ -18,9 +18,9 @@ import Lake open Lake DSL meta if get_config? env = some "dev" then -- dev is so not everyone has to build it -require "leanprover" / "doc-gen4" @ git "v4.15.0" +require "leanprover" / "doc-gen4" @ git "v4.16.0" -require "leanprover-community" / "batteries" @ git "v4.15.0" +require "leanprover-community" / "batteries" @ git "v4.16.0" package Cedar diff --git a/cedar-lean/lean-toolchain b/cedar-lean/lean-toolchain index d0eb99ff6..2586f8862 100644 --- a/cedar-lean/lean-toolchain +++ b/cedar-lean/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.15.0 +leanprover/lean4:v4.16.0