Make .lt strict. (#167)

Co-authored-by: Emina Torlak <[email protected]>

cedar-lean/Cedar/Data/Int64.lean

@@ -15,6 +15,7 @@
 -/
 
 import Std
+import Cedar.Data.LT
 
 /-!
 This file defines a signed 64-bit integer datatype similar to Rust's `i64`.
@@ -75,6 +76,23 @@ if h : Int64.le i₁ i₂ then isTrue h else isFalse h
 
 deriving instance Repr, DecidableEq for Int64
 
+instance strictLT : StrictLT Int64 where
+  asymmetric a b   := by
+    cases a ; cases b
+    simp [LT.lt, Int64.lt, Int.lt]
+    apply Int.strictLT.asymmetric
+  transitive a b c := by
+    simp [LT.lt, Int64.lt, Int.lt]
+    exact Int.strictLT.transitive a b c
+  connected  a b   := by
+    simp [LT.lt, Int64.lt, Int.lt]
+    intro h₁
+    apply Int.strictLT.connected a b
+    simp [h₁]
+    by_contra h₂
+    rcases (Subtype.eq h₂) with h₃
+    contradiction
+
 end Int64
 
 

cedar-lean/Cedar/Data/LT.lean

@@ -43,6 +43,15 @@ theorem StrictLT.if_not_lt_gt_then_eq [LT α] [StrictLT α] (x y : α) :
   rcases (StrictLT.connected x y h₃) with h₄
   simp [h₁, h₂] at h₄
 
+theorem StrictLT.not_eq [LT α] [StrictLT α] (x y : α) :
+  x < y → ¬ x = y
+:= by
+  intro h₁
+  by_contra h₂
+  subst h₂
+  rcases (StrictLT.irreflexive x) with h₃
+  contradiction
+
 abbrev DecidableLT (α) [LT α] := DecidableRel (α := α) (· < ·)
 
 end Cedar.Data
@@ -173,6 +182,29 @@ instance List.strictLT (α) [LT α] [StrictLT α] : StrictLT (List α) where
   transitive _ _ _ := List.lt_trans
   connected  _ _   := List.lt_conn
 
+def Bool.lt (a b : Bool) : Bool := match a,b with
+| false, true => true
+| _, _ => false
+
+instance : LT Bool where
+  lt a b := Bool.lt a b
+
+instance Bool.decLt (a b : Bool) : Decidable (a < b) :=
+  if h : Bool.lt a b then isTrue h else isFalse h
+
+instance Bool.strictLT : StrictLT Bool where
+  asymmetric a b   := by
+    simp [LT.lt, Bool.lt]
+    split <;> simp
+  transitive a b c := by
+    simp [LT.lt, Bool.lt]
+    split <;> simp
+  connected  a b   := by
+    simp [LT.lt, Bool.lt]
+    split <;> simp
+    split <;> simp
+    cases a <;> cases b <;> simp at *
+
 instance Nat.strictLT : StrictLT Nat where
   asymmetric a b   := Nat.lt_asymm
   transitive a b c := Nat.lt_trans
@@ -182,6 +214,19 @@ instance Nat.strictLT : StrictLT Nat where
     simp [h₁] at h₂
     exact h₂
 
+instance Int.strictLT : StrictLT Int where
+  asymmetric a b   := by
+    intro h₁
+    rw [Int.not_lt]
+    rw [Int.lt_iff_le_not_le] at h₁
+    simp [h₁]
+  transitive a b c := Int.lt_trans
+  connected  a b   := by
+    intro h₁
+    rcases (Int.lt_trichotomy a b) with h₂
+    simp [h₁] at h₂
+    exact h₂
+
 instance UInt32.strictLT : StrictLT UInt32 where
   asymmetric a b   := by apply Nat.strictLT.asymmetric
   transitive a b c := by apply Nat.strictLT.transitive
@@ -216,4 +261,3 @@ instance String.strictLT : StrictLT String where
     simp [String.lt_iff, String.ext_iff]
     have h : StrictLT (List Char) := by apply List.strictLT
     apply h.connected
-

cedar-lean/Cedar/Data/List.lean

@@ -91,6 +91,26 @@ def mapM₂ {m : Type u → Type v} [Monad m] {γ : Type u} [SizeOf α] [SizeOf
 
 ----- Theorems -----
 
+theorem mapM_pmap_subtype [Monad m] [LawfulMonad m]
+  {p : α → Prop}
+  (f : α → m β)
+  (as : List α)
+  (h : ∀ a, a ∈ as → p a)
+  : List.mapM (fun x : { a : α // p a } => f x.val) (List.pmap Subtype.mk as h)
+    =
+    List.mapM f as
+:= by
+  rw [←List.mapM'_eq_mapM]
+  induction as <;> simp [*]
+
+theorem mapM₁_eq_mapM [Monad m] [LawfulMonad m]
+  (f : α → m β)
+  (as : List α) :
+  List.mapM₁ as (fun x : { x // x ∈ as } => f x.val) =
+  List.mapM f as
+:= by
+  simp [mapM₁, attach, mapM_pmap_subtype]
+
 theorem Equiv.refl {a : List α} :
   a ≡ a
 := by unfold List.Equiv; simp
@@ -446,4 +466,4 @@ theorem if_equiv_strictLT_then_canonical [LT α] [StrictLT α] [DecidableLT α]
   apply Equiv.symm
   exact h₁
 
-end List
+end List

cedar-lean/Cedar/Data/Map.lean

@@ -33,7 +33,7 @@ deriving Repr, DecidableEq, Repr, Inhabited
 
 namespace Map
 
-private def kvs {α : Type u} {β : Type v} : Map α β -> List (Prod α β)
+def kvs {α : Type u} {β : Type v} : Map α β → List (Prod α β)
 | .mk kvs => kvs
 
 
@@ -58,16 +58,16 @@ def keys {α β} (m : Map α β) : Set α :=
 def values {α β} (m : Map α β) : Set β :=
   Set.mk (m.kvs.map Prod.snd)
 
-/-- Returns true if `m` contains a mapping for the key `k`. -/
-def contains {α β} [BEq α] (m : Map α β) (k : α) : Bool :=
-  (m.kvs.find? (fun ⟨k', _⟩ => k' == k)).isSome
-
 /-- Returns the binding for `k` in `m`, if any. -/
 def find? {α β} [BEq α] (m : Map α β) (k : α) : Option β :=
   match m.kvs.find? (fun ⟨k', _⟩ => k' == k) with
   | some (_, v) => some v
   | _           => none
 
+/-- Returns true if `m` contains a mapping for the key `k`. -/
+def contains {α β} [BEq α] (m : Map α β) (k : α) : Bool :=
+  (m.find? k).isSome
+
 /-- Returns the binding for `k` in `m` or `err` if none is found. -/
 def findOrErr {α β ε} [BEq α] (m : Map α β) (k : α) (err: ε) : Except ε β :=
   match m.find? k with
@@ -88,17 +88,17 @@ def size {α β} (m : Map α β) : Nat :=
   m.kvs.length
 
 def mapOnValues {α β γ} [LT α] [DecidableLT α] (f : β → γ) (m : Map α β) : Map α γ :=
-  Map.make (m.kvs.map (λ (k,v) => (k, f v )))
+  Map.mk (m.kvs.map (λ (k,v) => (k, f v)))
 
 def mapOnKeys {α β γ} [LT γ] [DecidableLT γ] (f : α → γ) (m : Map α β) : Map γ β :=
-  Map.make (m.kvs.map (λ (k,v) => (f k, v) ))
+  Map.make (m.kvs.map (λ (k,v) => (f k, v)))
 
 ----- Props and Theorems -----
 
 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)
+instance decLt [LT (Prod α β)] [DecidableRel (α:=(Prod α β)) (·<·)] : (n m : Map α β) → Decidable (n < m)
   | .mk nkvs, .mk mkvs => List.hasDecidableLt nkvs mkvs
 
 instance : Membership α (Map α β) where
@@ -114,6 +114,14 @@ theorem in_list_in_map {α : Type u} (k : α) (v : β) (m : Map α β) :
     simp [h0]
   apply h1
 
+theorem contains_iff_some_find? {α β} [BEq α] {m : Map α β} {k : α} :
+  m.contains k ↔ ∃ v, m.find? k = .some v
+:= by simp [contains, Option.isSome_iff_exists]
+
+theorem not_contains_of_empty {α β} [BEq α] (k : α) :
+  ¬ (Map.empty : Map α β).contains k
+:= by simp [contains, empty, find?, List.find?]
+
 end Map
 
 end Cedar.Data

cedar-lean/Cedar/Data/Set.lean

@@ -34,7 +34,7 @@ deriving Repr, DecidableEq, Inhabited, Lean.ToJson
 
 namespace Set
 
-private def elts {α : Type u} : (Set α) -> (List α)
+def elts {α : Type u} : (Set α) -> (List α)
 | .mk elts => elts
 
 open Except
@@ -155,6 +155,17 @@ theorem make_eq_if_eqv [LT α] [DecidableLT α] [StrictLT α] (xs ys : List α)
   intro h; unfold make; simp
   apply List.if_equiv_strictLT_then_canonical _ _ h
 
+theorem make_mem [LT α] [DecidableLT α] [StrictLT α] (x : α) (xs : List α) :
+  x ∈ xs ↔ x ∈ Set.make xs
+:= by
+  simp [make, Membership.mem, elts]
+  rcases (List.canonicalize_equiv xs) with h₁
+  simp [List.Equiv, List.subset_def] at h₁
+  rcases h₁ with ⟨h₁, h₂⟩
+  constructor <;> intro h₃
+  case mp => apply h₁ h₃
+  case mpr => apply h₂ h₃
+
 end Set
 
 end Cedar.Data

cedar-lean/Cedar/Spec/Ext/IPAddr.lean

@@ -251,8 +251,8 @@ def ip (str : String) : Option IPNet := parse str
 def IPNet.lt : IPNet → IPNet → Bool
   | .V4 _ _, .V6 _ _ => true
   | .V6 _ _, .V4 _ _ => false
-  | .V4 v₁ p₁, .V4 v₂ p₂ => v₁ < v₂ || (v₁ = v₂ && p₁ < p₂)
-  | .V6 v₁ p₁, .V6 v₂ p₂ => v₁ < v₂ || (v₁ = v₂ && p₁ < p₂)
+  | .V4 v₁ p₁, .V4 v₂ p₂ => v₁.val < v₂.val || (v₁.val = v₂.val && p₁.val < p₂.val)
+  | .V6 v₁ p₁, .V6 v₂ p₂ => v₁.val < v₂.val || (v₁.val = v₂.val && p₁.val < p₂.val)
 
 ----- IPNet deriviations -----
 

cedar-lean/Cedar/Spec/ExtFun.lean

@@ -39,7 +39,7 @@ inductive ExtFun where
   | isMulticast
   | isInRange
 
-private def res {α} [Coe α Ext] : Option α → Result Value
+def res {α} [Coe α Ext] : Option α → Result Value
   | some v => ok v
   | none   => error .extensionError
 

cedar-lean/Cedar/Spec/Value.lean

@@ -171,15 +171,15 @@ def decValueList (as bs : List Value) : Decidable (as = bs) :=
       | isFalse _ => isFalse (by intro h; injection h; contradiction)
     | isFalse _ => isFalse (by intro h; injection h; contradiction)
 
-def decProdAttrValue (as bs : Prod Attr Value) : Decidable (as = bs) :=
+def decProdAttrValue (as bs : Attr × Value) : Decidable (as = bs) :=
   match as, bs with
   | (a1, a2), (b1, b2) => match decEq a1 b1 with
     | isTrue h₀ => match decValue a2 b2 with
       | isTrue h₁ => isTrue (by rw [h₀, h₁])
       | isFalse _ => isFalse (by intro h; injection h; contradiction)
     | isFalse _ => isFalse (by intro h; injection h; contradiction)
 
-def decProdAttrValueList (as bs : List (Prod Attr Value)) : Decidable (as = bs) :=
+def decProdAttrValueList (as bs : List (Attr × Value)) : Decidable (as = bs) :=
   match as, bs with
   | [], [] => isTrue rfl
   | _::_, [] => isFalse (by intro; contradiction)
@@ -209,86 +209,76 @@ instance : DecidableEq Value :=
   decValue
 
 def Name.lt (a b : Name) : Bool :=
-  (a.id < b.id) ∨ (a.id = b.id ∧ a.path < b.path)
+  (a.id :: a.path) < (b.id :: b.path)
 
 instance : LT Name where
   lt a b := Name.lt a b
 
-instance Name.decLt (n m : Name) : Decidable (n < m) :=
-  if h : Name.lt n m then isTrue h else isFalse h
-
+instance Name.decLt (a b : Name) : Decidable (a < b) :=
+  if h : Name.lt a b then isTrue h else isFalse h
 
 def EntityUID.lt (a b : EntityUID) : Bool :=
   (a.ty < b.ty) ∨ (a.ty = b.ty ∧ a.eid < b.eid)
 
 instance : LT EntityUID where
   lt a b := EntityUID.lt a b
 
-instance EntityUID.decLt (n m : EntityUID) : Decidable (n < m) :=
-  if h : EntityUID.lt n m then isTrue h else isFalse h
-
-instance : Ord EntityUID where
-  compare a b := compareOfLessAndEq a b
-
-def Bool.lt (a b : Bool) : Bool := match a,b with
-| false, true => true
-| _, _ => false
-
-instance : LT Bool where
-  lt a b := Bool.lt a b
-
-instance Bool.decLt (n m : Bool) : Decidable (n < m) :=
-  if h : Bool.lt n m then isTrue h else isFalse h
+instance EntityUID.decLt (a b : EntityUID) : Decidable (a < b) :=
+  if h : EntityUID.lt a b then isTrue h else isFalse h
 
-def Prim.lt (n m : Prim) : Bool := match n,m with
+def Prim.lt : Prim → Prim → Bool
   | .bool nb, .bool mb => nb < mb
   | .int ni, .int mi => ni < mi
   | .string ns, .string ms => ns < ms
   | .entityUID nuid, .entityUID muid => nuid < muid
-  | .bool _, .int _ => True
-  | .bool _, .string _ => True
-  | .bool _, .entityUID _ => True
-  | .int _, .string _ => True
-  | .int _, .entityUID _ => True
-  | .string _, .entityUID _ => True
-  | _,_ => False
+  | .bool _, .int _ => true
+  | .bool _, .string _ => true
+  | .bool _, .entityUID _ => true
+  | .int _, .string _ => true
+  | .int _, .entityUID _ => true
+  | .string _, .entityUID _ => true
+  | _,_ => false
 
 instance : LT Prim where
 lt := fun x y => Prim.lt x y
 
-instance Prim.decLt (n m : Prim) : Decidable (n < m) :=
-if  h : Prim.lt n m then isTrue h else isFalse h
+instance Prim.decLt (a b : Prim) : Decidable (a < b) :=
+if  h : Prim.lt a b then isTrue h else isFalse h
 
 mutual
-def Value.lt (n m : Value) : Bool := match n,m with
+def Value.lt : Value → Value → Bool
   | .prim x, .prim y => x < y
   | .set (.mk lx), .set (.mk ly) => Values.lt lx ly lx.length
   | .record (.mk lx), .record (.mk ly) => ValueAttrs.lt lx ly lx.length
   | .ext x, .ext y => x < y
-  | .prim _, .set _ => True
-  | .prim _, .record _ => True
-  | .prim _, .ext _ => True
-  | .set _, .record _ => True
-  | .set _, .ext _ => True
-  | .set _, .prim _ => False
-  | .record _, .ext _ => True
-  | .record _, .prim _ => False
-  | .record _, .set _ => False
-  | .ext _, .prim _ => False
-  | .ext _, .set _ => False
-  | .ext _, .record _ => False
-
-def Values.lt (n m : List Value) (i : Nat): Bool := match n, m with
-  | [], [] => False
-  | [], _ => True
-  | _, [] => False
-  | n::ns, m::ms => Value.lt n m && Values.lt ns ms (i-1)
-
-def ValueAttrs.lt (n m : List (Prod String Value)) (i : Nat) : _root_.Bool := match n, m with
-  | [], [] => False
-  | [], _ => True
-  | _, [] => False
-  | (na, nv)::ns, (ma, mv)::ms => Value.lt nv mv && na < ma && ValueAttrs.lt ns ms (i-1)
+  | .prim _, .set _ => true
+  | .prim _, .record _ => true
+  | .prim _, .ext _ => true
+  | .set _, .record _ => true
+  | .set _, .ext _ => true
+  | .set _, .prim _ => false
+  | .record _, .ext _ => true
+  | .record _, .prim _ => false
+  | .record _, .set _ => false
+  | .ext _, .prim _ => false
+  | .ext _, .set _ => false
+  | .ext _, .record _ => false
+
+def Values.lt (n m : List Value) (i : Nat): Bool :=
+  match n, m with
+  | [], [] => false
+  | [], _ => true
+  | _, [] => false
+  | n::ns, m::ms => Value.lt n m || (n = m && Values.lt ns ms (i-1))
+
+def ValueAttrs.lt (n m : List (Attr × Value)) (i : Nat) : Bool :=
+  match n, m with
+  | [], [] => false
+  | [], _ => true
+  | _, [] => false
+  | (na, nv)::ns, (ma, mv)::ms =>
+    na < ma || (na = ma && Value.lt nv mv) ||
+    (na = ma && nv = mv && ValueAttrs.lt ns ms (i-1))
 end
 termination_by
 Value.lt as₁ as₂ => (sizeOf as₁, 0)