diff --git a/lean/Spa/Analysis/Constant.lean b/lean/Spa/Analysis/Constant.lean index 9208753..6d9983b 100644 --- a/lean/Spa/Analysis/Constant.lean +++ b/lean/Spa/Analysis/Constant.lean @@ -77,12 +77,12 @@ theorem eval_mono (e : Expr) : Monotone (eval prog e) := by intro vs₁ vs₂ h simp only [eval] by_cases hk : k ∈ prog.vars - · rw [dif_pos (FiniteMap.memKey_iff.mpr hk), - dif_pos (FiniteMap.memKey_iff.mpr hk)] + · rw [dif_pos (FiniteMap.MemKey_iff.mpr hk), + dif_pos (FiniteMap.MemKey_iff.mpr hk)] exact FiniteMap.le_of_mem_mem prog.vars_nodup h (FiniteMap.locate _).2 (FiniteMap.locate _).2 - · rw [dif_neg (fun hm => hk (FiniteMap.memKey_iff.mp hm)), - dif_neg (fun hm => hk (FiniteMap.memKey_iff.mp hm))] + · rw [dif_neg (fun hm => hk (FiniteMap.MemKey_iff.mp hm)), + dif_neg (fun hm => hk (FiniteMap.MemKey_iff.mp hm))] | num n => intro vs₁ vs₂ _ exact le_refl _ diff --git a/lean/Spa/Analysis/Forward/Lattices.lean b/lean/Spa/Analysis/Forward/Lattices.lean index c1fa27f..54bd62f 100644 --- a/lean/Spa/Analysis/Forward/Lattices.lean +++ b/lean/Spa/Analysis/Forward/Lattices.lean @@ -20,7 +20,7 @@ variable {L prog} omit [Lattice L] in theorem states_memKey (s : prog.State) (sv : StateVariables L prog) : FiniteMap.MemKey s sv := - FiniteMap.memKey_iff.mpr (prog.states_complete s) + FiniteMap.MemKey_iff.mpr (prog.states_complete s) def variablesAt (s : prog.State) (sv : StateVariables L prog) : VariableValues L prog := diff --git a/lean/Spa/Analysis/Sign.lean b/lean/Spa/Analysis/Sign.lean index d5079ef..bf841d3 100644 --- a/lean/Spa/Analysis/Sign.lean +++ b/lean/Spa/Analysis/Sign.lean @@ -137,12 +137,12 @@ theorem eval_mono (e : Expr) : Monotone (eval prog e) := by intro vs₁ vs₂ h simp only [eval] by_cases hk : k ∈ prog.vars - · rw [dif_pos (FiniteMap.memKey_iff.mpr hk), - dif_pos (FiniteMap.memKey_iff.mpr hk)] + · rw [dif_pos (FiniteMap.MemKey_iff.mpr hk), + dif_pos (FiniteMap.MemKey_iff.mpr hk)] exact FiniteMap.le_of_mem_mem prog.vars_nodup h (FiniteMap.locate _).2 (FiniteMap.locate _).2 - · rw [dif_neg (fun hm => hk (FiniteMap.memKey_iff.mp hm)), - dif_neg (fun hm => hk (FiniteMap.memKey_iff.mp hm))] + · rw [dif_neg (fun hm => hk (FiniteMap.MemKey_iff.mp hm)), + dif_neg (fun hm => hk (FiniteMap.MemKey_iff.mp hm))] | num n => intro vs₁ vs₂ _ cases n <;> exact le_refl _ diff --git a/lean/Spa/Lattice/FiniteMap.lean b/lean/Spa/Lattice/FiniteMap.lean index 680e5da..3c476c0 100644 --- a/lean/Spa/Lattice/FiniteMap.lean +++ b/lean/Spa/Lattice/FiniteMap.lean @@ -1,318 +1,111 @@ -import Spa.Lattice.IterProd -import Spa.Isomorphism +import Spa.Lattice.Tuple +import Mathlib.Data.List.Nodup namespace Spa -def FiniteMap (A B : Type*) (ks : List A) : Type _ := - { l : List (A × B) // l.map Prod.fst = ks } +def FiniteMap (A B : Type*) (ks : List A) : Type _ := Fin ks.length → B namespace FiniteMap variable {A B : Type*} {ks : List A} -instance [DecidableEq A] [DecidableEq B] : DecidableEq (FiniteMap A B ks) := - fun a b => decidable_of_iff (a.val = b.val) Subtype.ext_iff.symm +instance [Lattice B] : Lattice (FiniteMap A B ks) := + inferInstanceAs (Lattice (Fin ks.length → B)) -theorem spine_eq (fm₁ fm₂ : FiniteMap A B ks) : - fm₁.val.map Prod.fst = fm₂.val.map Prod.fst := - fm₁.property.trans fm₂.property.symm +instance [Lattice B] [FiniteHeightLattice B] : FiniteHeightLattice (FiniteMap A B ks) := + inferInstanceAs (FiniteHeightLattice (Fin ks.length → B)) -def combine (f : B → B → B) (l₁ l₂ : List (A × B)) : List (A × B) := - List.zipWith (fun p q => (p.1, f p.2 q.2)) l₁ l₂ - -theorem combine_spine (f : B → B → B) : ∀ {l₁ l₂ : List (A × B)}, - l₁.map Prod.fst = l₂.map Prod.fst → - (combine f l₁ l₂).map Prod.fst = l₁.map Prod.fst - | [], [], _ => rfl - | p :: l₁, q :: l₂, h => by - simp only [List.map_cons, List.cons.injEq] at h - simp only [combine, List.zipWith_cons_cons, List.map_cons] - exact congrArg _ (combine_spine f h.2) - | [], _ :: _, h => by simp at h - | _ :: _, [], h => by simp at h - -theorem combine_comm (f : B → B → B) (hf : ∀ a b, f a b = f b a) : - ∀ {l₁ l₂ : List (A × B)}, l₁.map Prod.fst = l₂.map Prod.fst → - combine f l₁ l₂ = combine f l₂ l₁ - | [], [], _ => rfl - | p :: l₁, q :: l₂, h => by - simp only [List.map_cons, List.cons.injEq] at h - simp only [combine, List.zipWith_cons_cons] - rw [h.1, hf] - exact congrArg _ (combine_comm f hf h.2) - | [], _ :: _, h => by simp at h - | _ :: _, [], h => by simp at h - -theorem combine_assoc (f : B → B → B) (hf : ∀ a b c, f (f a b) c = f a (f b c)) : - ∀ {l₁ l₂ l₃ : List (A × B)}, - l₁.map Prod.fst = l₂.map Prod.fst → l₂.map Prod.fst = l₃.map Prod.fst → - combine f (combine f l₁ l₂) l₃ = combine f l₁ (combine f l₂ l₃) - | [], [], [], _, _ => rfl - | p :: l₁, q :: l₂, r :: l₃, h₁₂, h₂₃ => by - simp only [List.map_cons, List.cons.injEq] at h₁₂ h₂₃ - simp only [combine, List.zipWith_cons_cons] - rw [hf] - exact congrArg _ (combine_assoc f hf h₁₂.2 h₂₃.2) - | [], [], _ :: _, _, h => by simp at h - | [], _ :: _, _, h, _ => by simp at h - | _ :: _, [], _, h, _ => by simp at h - | _ :: _, _ :: _, [], _, h => by simp at h - -theorem combine_absorb (f g : B → B → B) (hfg : ∀ a b, f a (g a b) = a) : - ∀ {l₁ l₂ : List (A × B)}, l₁.map Prod.fst = l₂.map Prod.fst → - combine f l₁ (combine g l₁ l₂) = l₁ - | [], [], _ => rfl - | p :: l₁, q :: l₂, h => by - simp only [List.map_cons, List.cons.injEq] at h - simp only [combine, List.zipWith_cons_cons, hfg] - exact congrArg _ (combine_absorb f g hfg h.2) - | [], _ :: _, h => by simp at h - | _ :: _, [], h => by simp at h - -variable [Lattice B] - -instance : Max (FiniteMap A B ks) where - max fm₁ fm₂ := - ⟨combine (· ⊔ ·) fm₁.val fm₂.val, - (combine_spine _ (spine_eq fm₁ fm₂)).trans fm₁.property⟩ - -instance : Min (FiniteMap A B ks) where - min fm₁ fm₂ := - ⟨combine (· ⊓ ·) fm₁.val fm₂.val, - (combine_spine _ (spine_eq fm₁ fm₂)).trans fm₁.property⟩ - -@[simp] theorem sup_val (fm₁ fm₂ : FiniteMap A B ks) : - (fm₁ ⊔ fm₂).val = combine (· ⊔ ·) fm₁.val fm₂.val := rfl - -@[simp] theorem inf_val (fm₁ fm₂ : FiniteMap A B ks) : - (fm₁ ⊓ fm₂).val = combine (· ⊓ ·) fm₁.val fm₂.val := rfl - -instance : Lattice (FiniteMap A B ks) := - Lattice.mk' - (fun a b => Subtype.ext (combine_comm _ sup_comm (spine_eq a b))) - (fun a b c => Subtype.ext (combine_assoc _ sup_assoc (spine_eq a b) (spine_eq b c))) - (fun a b => Subtype.ext (combine_comm _ inf_comm (spine_eq a b))) - (fun a b c => Subtype.ext (combine_assoc _ inf_assoc (spine_eq a b) (spine_eq b c))) - (fun a b => Subtype.ext (combine_absorb _ _ (fun _ _ => sup_inf_self) (spine_eq a b))) - (fun a b => Subtype.ext (combine_absorb _ _ (fun _ _ => inf_sup_self) (spine_eq a b))) +instance [DecidableEq B] : DecidableEq (FiniteMap A B ks) := + inferInstanceAs (DecidableEq (Fin ks.length → B)) instance : Membership (A × B) (FiniteMap A B ks) := - ⟨fun fm p => p ∈ fm.val⟩ + ⟨fun fm p => ∃ i : Fin ks.length, ks.get i = p.1 ∧ fm i = p.2⟩ -omit [Lattice B] in -theorem mem_def {p : A × B} {fm : FiniteMap A B ks} : p ∈ fm ↔ p ∈ fm.val := - Iff.rfl +theorem mem_iff {fm : FiniteMap A B ks} {p : A × B} : + p ∈ fm ↔ ∃ i : Fin ks.length, ks.get i = p.1 ∧ fm i = p.2 := Iff.rfl -def MemKey (k : A) (fm : FiniteMap A B ks) : Prop := - k ∈ fm.val.map Prod.fst +def MemKey (k : A) (_fm : FiniteMap A B ks) : Prop := k ∈ ks -omit [Lattice B] in -theorem memKey_iff {k : A} {fm : FiniteMap A B ks} : MemKey k fm ↔ k ∈ ks := by - rw [MemKey, fm.property] +theorem MemKey_iff {k : A} {fm : FiniteMap A B ks} : MemKey k fm ↔ k ∈ ks := Iff.rfl -instance {k : A} {fm : FiniteMap A B ks} [DecidableEq A] : - Decidable (MemKey k fm) := - decidable_of_iff _ memKey_iff.symm +instance {k : A} {fm : FiniteMap A B ks} [DecidableEq A] : Decidable (MemKey k fm) := + decidable_of_iff _ MemKey_iff.symm -omit [Lattice B] in theorem mem_key_of_mem {k : A} {v : B} {fm : FiniteMap A B ks} - (h : (k, v) ∈ fm) : MemKey k fm := - List.mem_map_of_mem _ h + (h : (k, v) ∈ fm) : MemKey k fm := by + obtain ⟨i, hi, _⟩ := h + have hik : ks.get i = k := hi + exact hik ▸ ks.get_mem i + +def toList (fm : FiniteMap A B ks) : List (A × B) := + (List.finRange ks.length).map fun i => (ks.get i, fm i) + +theorem le_def [Lattice B] {fm₁ fm₂ : FiniteMap A B ks} : + fm₁ ≤ fm₂ ↔ ∀ i, fm₁ i ≤ fm₂ i := Iff.rfl section Locate variable [DecidableEq A] -private def locateList (k : A) : - (l : List (A × B)) → k ∈ l.map Prod.fst → {v : B // (k, v) ∈ l} - | [], h => absurd h (by simp) - | p :: l', h => - if heq : p.1 = k then - ⟨p.2, by rw [← heq]; exact List.mem_cons_self ..⟩ - else - let ⟨v, hv⟩ := locateList k l' (by - rcases List.mem_cons.mp h with h' | h' - · exact absurd h'.symm heq - · exact h') - ⟨v, List.mem_cons_of_mem _ hv⟩ - +/-- Recover the value stored under a present key. -/ def locate {k : A} {fm : FiniteMap A B ks} (h : MemKey k fm) : {v : B // (k, v) ∈ fm} := - locateList k fm.val h + let i : Fin ks.length := ⟨ks.idxOf k, List.idxOf_lt_length_iff.mpr h⟩ + ⟨fm i, i, List.idxOf_get _, rfl⟩ end Locate -theorem combine_eq_right_iff : ∀ {l₁ l₂ : List (A × B)}, - l₁.map Prod.fst = l₂.map Prod.fst → - (combine (· ⊔ ·) l₁ l₂ = l₂ ↔ - List.Forall₂ (fun p q : A × B => p.1 = q.1 ∧ p.2 ≤ q.2) l₁ l₂) - | [], [], _ => by simp [combine] - | p :: l₁, q :: l₂, h => by - simp only [List.map_cons, List.cons.injEq] at h - simp only [combine, List.zipWith_cons_cons, List.cons.injEq, - List.forall₂_cons, Prod.ext_iff] - rw [show List.zipWith (fun p q : A × B => (p.1, p.2 ⊔ q.2)) l₁ l₂ - = combine (· ⊔ ·) l₁ l₂ from rfl, - combine_eq_right_iff h.2] - constructor - · rintro ⟨⟨hk, hv⟩, hrest⟩ - exact ⟨⟨hk, sup_eq_right.mp hv⟩, hrest⟩ - · rintro ⟨⟨hk, hv⟩, hrest⟩ - exact ⟨⟨hk, sup_eq_right.mpr hv⟩, hrest⟩ - | [], _ :: _, h => by simp at h - | _ :: _, [], h => by simp at h - -theorem le_iff {fm₁ fm₂ : FiniteMap A B ks} : - fm₁ ≤ fm₂ ↔ - List.Forall₂ (fun p q : A × B => p.1 = q.1 ∧ p.2 ≤ q.2) fm₁.val fm₂.val := by - rw [← sup_eq_right, ← combine_eq_right_iff (spine_eq fm₁ fm₂), Subtype.ext_iff, - sup_val] - -private theorem forall₂_spine : ∀ {l₁ l₂ : List (A × B)}, - List.Forall₂ (fun p q : A × B => p.1 = q.1 ∧ p.2 ≤ q.2) l₁ l₂ → - l₁.map Prod.fst = l₂.map Prod.fst - | _, _, List.Forall₂.nil => rfl - | _, _, List.Forall₂.cons hpq hrest => by - simp [List.map_cons, hpq.1, forall₂_spine hrest] - -private theorem forall₂_mem_mem {l₁ l₂ : List (A × B)} - (hf : List.Forall₂ (fun p q : A × B => p.1 = q.1 ∧ p.2 ≤ q.2) l₁ l₂) : - (l₁.map Prod.fst).Nodup → - ∀ {k : A} {v₁ v₂ : B}, (k, v₁) ∈ l₁ → (k, v₂) ∈ l₂ → v₁ ≤ v₂ := by - induction hf with - | nil => - intro _ k v₁ v₂ h₁ _ - simp at h₁ - | @cons p q l₁' l₂' hpq hrest ih => - intro hnd k v₁ v₂ h₁ h₂ - simp only [List.map_cons, List.nodup_cons] at hnd - have hspine := forall₂_spine hrest - rcases List.mem_cons.mp h₁ with heq₁ | h₁' - · rcases List.mem_cons.mp h₂ with heq₂ | h₂' - · rw [← heq₁, ← heq₂] at hpq - exact hpq.2 - · exfalso - apply hnd.1 - rw [show p.1 = k from (congrArg Prod.fst heq₁).symm, hspine] - exact List.mem_map_of_mem _ h₂' - · rcases List.mem_cons.mp h₂ with heq₂ | h₂' - · exfalso - apply hnd.1 - rw [hpq.1, show q.1 = k from (congrArg Prod.fst heq₂).symm] - exact List.mem_map_of_mem _ h₁' - · exact ih hnd.2 h₁' h₂' +variable [Lattice B] theorem le_of_mem_mem (hks : ks.Nodup) {fm₁ fm₂ : FiniteMap A B ks} (hle : fm₁ ≤ fm₂) {k : A} {v₁ v₂ : B} - (h₁ : (k, v₁) ∈ fm₁) (h₂ : (k, v₂) ∈ fm₂) : v₁ ≤ v₂ := - forall₂_mem_mem (le_iff.mp hle) (fm₁.property.symm ▸ hks) h₁ h₂ - -omit [Lattice B] in -private theorem mem_combine (f : B → B → B) : ∀ {l₁ l₂ : List (A × B)} {k : A} {v : B}, - l₁.map Prod.fst = l₂.map Prod.fst → - (k, v) ∈ combine f l₁ l₂ → - ∃ v₁ v₂, v = f v₁ v₂ ∧ (k, v₁) ∈ l₁ ∧ (k, v₂) ∈ l₂ - | [], [], _, _, _, h => by simp [combine] at h - | p :: l₁, q :: l₂, k, v, hsp, h => by - simp only [List.map_cons, List.cons.injEq] at hsp - simp only [combine, List.zipWith_cons_cons] at h - rcases List.mem_cons.mp h with heq | h' - · injection heq with hk hv - exact ⟨p.2, q.2, hv, - by rw [hk]; simp, - by rw [hk, hsp.1]; simp⟩ - · obtain ⟨v₁, v₂, hv, h₁, h₂⟩ := mem_combine f hsp.2 h' - exact ⟨v₁, v₂, hv, List.mem_cons_of_mem _ h₁, List.mem_cons_of_mem _ h₂⟩ + (h₁ : (k, v₁) ∈ fm₁) (h₂ : (k, v₂) ∈ fm₂) : v₁ ≤ v₂ := by + obtain ⟨i, hi, rfl⟩ := h₁ + obtain ⟨j, hj, rfl⟩ := h₂ + have hij : i = j := hks.get_inj_iff.mp (hi.trans hj.symm) + subst hij + exact le_def.mp hle i theorem mem_sup {fm₁ fm₂ : FiniteMap A B ks} {k : A} {v : B} (h : (k, v) ∈ fm₁ ⊔ fm₂) : - ∃ v₁ v₂, v = v₁ ⊔ v₂ ∧ (k, v₁) ∈ fm₁ ∧ (k, v₂) ∈ fm₂ := - mem_combine _ (spine_eq fm₁ fm₂) h + ∃ v₁ v₂, v = v₁ ⊔ v₂ ∧ (k, v₁) ∈ fm₁ ∧ (k, v₂) ∈ fm₂ := by + obtain ⟨i, hi, rfl⟩ := h + exact ⟨fm₁ i, fm₂ i, rfl, ⟨i, hi, rfl⟩, ⟨i, hi, rfl⟩⟩ section Updating variable [DecidableEq A] -def updating (fm : FiniteMap A B ks) (ks' : List A) (g : A → B) : - FiniteMap A B ks := - ⟨fm.val.map (fun p => if p.1 ∈ ks' then (p.1, g p.1) else p), by - rw [List.map_map, - show (Prod.fst ∘ fun p : A × B => if p.1 ∈ ks' then (p.1, g p.1) else p) - = Prod.fst from funext fun p => by by_cases h : p.1 ∈ ks' <;> simp [h]] - exact fm.property⟩ - -omit [Lattice B] in -@[simp] theorem updating_val (fm : FiniteMap A B ks) (ks' : List A) (g : A → B) : - (updating fm ks' g).val - = fm.val.map (fun p => if p.1 ∈ ks' then (p.1, g p.1) else p) := rfl - -omit [Lattice B] in -theorem memKey_updating {k : A} {fm : FiniteMap A B ks} {ks' : List A} {g : A → B} : - MemKey k (updating fm ks' g) ↔ MemKey k fm := by - rw [memKey_iff, memKey_iff] +def updating (fm : FiniteMap A B ks) (ks' : List A) (g : A → B) : FiniteMap A B ks := + fun i => if ks.get i ∈ ks' then g (ks.get i) else fm i omit [Lattice B] in theorem eq_of_mem_updating {k : A} {v : B} {fm : FiniteMap A B ks} {ks' : List A} {g : A → B} (hk : k ∈ ks') (h : (k, v) ∈ updating fm ks' g) : v = g k := by - obtain ⟨p, hp, heq⟩ := List.mem_map.mp h - by_cases hmem : p.1 ∈ ks' - · rw [if_pos hmem] at heq - injection heq with h1 h2 - rw [← h2, h1] - · rw [if_neg hmem] at heq - rw [heq] at hmem - exact absurd hk hmem - -omit [Lattice B] in -theorem mem_updating {k : A} {fm : FiniteMap A B ks} {ks' : List A} {g : A → B} - (hk : k ∈ ks') (hmem : MemKey k fm) : (k, g k) ∈ updating fm ks' g := by - obtain ⟨v, hv⟩ := locate hmem - exact List.mem_map.mpr ⟨(k, v), hv, by simp [hk]⟩ - -omit [Lattice B] in -theorem mem_updating_of_not_mem {k : A} {v : B} {fm : FiniteMap A B ks} - {ks' : List A} {g : A → B} (hk : k ∉ ks') (h : (k, v) ∈ fm) : - (k, v) ∈ updating fm ks' g := - List.mem_map.mpr ⟨(k, v), h, by simp [hk]⟩ + obtain ⟨i, hi, rfl⟩ := h + show (if ks.get i ∈ ks' then g (ks.get i) else fm i) = g k + rw [if_pos (by rw [hi]; exact hk), hi] omit [Lattice B] in theorem mem_of_mem_updating {k : A} {v : B} {fm : FiniteMap A B ks} {ks' : List A} {g : A → B} (hk : k ∉ ks') (h : (k, v) ∈ updating fm ks' g) : (k, v) ∈ fm := by - obtain ⟨p, hp, heq⟩ := List.mem_map.mp h - by_cases hmem : p.1 ∈ ks' - · rw [if_pos hmem] at heq - injection heq with h1 _ - rw [← h1] at hk - exact absurd hmem hk - · rw [if_neg hmem] at heq - exact heq ▸ hp - -private theorem updating_mono_list {ks' : List A} {g₁ g₂ : A → B} - (hg : ∀ k, g₁ k ≤ g₂ k) {l₁ l₂ : List (A × B)} - (hl : List.Forall₂ (fun p q : A × B => p.1 = q.1 ∧ p.2 ≤ q.2) l₁ l₂) : - List.Forall₂ (fun p q : A × B => p.1 = q.1 ∧ p.2 ≤ q.2) - (l₁.map fun p => if p.1 ∈ ks' then (p.1, g₁ p.1) else p) - (l₂.map fun p => if p.1 ∈ ks' then (p.1, g₂ p.1) else p) := by - induction hl with - | nil => exact List.Forall₂.nil - | @cons x y l₁' l₂' hpq hrest ih => - simp only [List.map_cons] - refine List.Forall₂.cons ?_ ih - obtain ⟨hk, hv⟩ := hpq - by_cases h : x.1 ∈ ks' - · rw [if_pos h, if_pos (hk ▸ h)] - exact ⟨hk, hk ▸ hg x.1⟩ - · rw [if_neg h, if_neg (fun hy => h (hk.symm ▸ hy))] - exact ⟨hk, hv⟩ + obtain ⟨i, hi, rfl⟩ := h + refine ⟨i, hi, ?_⟩ + show fm i = (if ks.get i ∈ ks' then g (ks.get i) else fm i) + rw [if_neg (by rw [hi]; exact hk)] theorem updating_mono {fm₁ fm₂ : FiniteMap A B ks} {ks' : List A} {g₁ g₂ : A → B} (hfm : fm₁ ≤ fm₂) (hg : ∀ k, g₁ k ≤ g₂ k) : updating fm₁ ks' g₁ ≤ updating fm₂ ks' g₂ := by - rw [le_iff] at hfm ⊢ - simp only [updating_val] - exact updating_mono_list hg hfm + rw [le_def] + intro i + show (if ks.get i ∈ ks' then g₁ (ks.get i) else fm₁ i) + ≤ (if ks.get i ∈ ks' then g₂ (ks.get i) else fm₂ i) + split + · exact hg (ks.get i) + · exact le_def.mp hfm i end Updating @@ -321,7 +114,7 @@ section GeneralizedUpdate variable [DecidableEq A] {L : Type*} [Lattice L] def generalizedUpdate (f : L → FiniteMap A B ks) (g : A → L → B) - (ks' : List A) (l : L) : FiniteMap A B ks := + (ks' : List A) : L → FiniteMap A B ks := fun l => (f l).updating ks' (fun k => g k l) variable {f : L → FiniteMap A B ks} {g : A → L → B} {ks' : List A} @@ -330,35 +123,15 @@ theorem generalizedUpdate_monotone (hf : Monotone f) (hg : ∀ k, Monotone (g k)) : Monotone (generalizedUpdate f g ks') := fun _ _ hl => updating_mono (hf hl) (fun k => hg k hl) -omit [Lattice B] [Lattice L] in -theorem generalizedUpdate_memKey {k : A} {l : L} - (h : MemKey k (f l)) : MemKey k (generalizedUpdate f g ks' l) := by - unfold generalizedUpdate - exact memKey_updating.mpr h - -omit [Lattice B] [Lattice L] in -theorem generalizedUpdate_mem {k : A} {l : L} (hk : k ∈ ks') - (h : MemKey k (f l)) : (k, g k l) ∈ generalizedUpdate f g ks' l := by - unfold generalizedUpdate - exact mem_updating hk h - omit [Lattice B] [Lattice L] in theorem generalizedUpdate_mem_eq {k : A} {v : B} {l : L} (hk : k ∈ ks') - (h : (k, v) ∈ generalizedUpdate f g ks' l) : v = g k l := by - unfold generalizedUpdate at h - exact eq_of_mem_updating (g := fun k => g k l) hk h - -omit [Lattice B] [Lattice L] in -theorem generalizedUpdate_not_mem_forward {k : A} {v : B} {l : L} (hk : k ∉ ks') - (h : (k, v) ∈ f l) : (k, v) ∈ generalizedUpdate f g ks' l := by - unfold generalizedUpdate - exact mem_updating_of_not_mem hk h + (h : (k, v) ∈ generalizedUpdate f g ks' l) : v = g k l := + eq_of_mem_updating (g := fun k => g k l) hk h omit [Lattice B] [Lattice L] in theorem generalizedUpdate_not_mem_backward {k : A} {v : B} {l : L} (hk : k ∉ ks') - (h : (k, v) ∈ generalizedUpdate f g ks' l) : (k, v) ∈ f l := by - unfold generalizedUpdate at h - exact mem_of_mem_updating hk h + (h : (k, v) ∈ generalizedUpdate f g ks' l) : (k, v) ∈ f l := + mem_of_mem_updating hk h end GeneralizedUpdate @@ -366,48 +139,36 @@ section ValuesAt variable [DecidableEq A] -private def lookup? (k : A) : List (A × B) → Option B - | [] => none - | p :: l' => if p.1 = k then some p.2 else lookup? k l' +/-- The value stored under `k`, if `k` is a key. -/ +private def lookup (fm : FiniteMap A B ks) (k : A) : Option B := + if h : k ∈ ks then some (fm ⟨ks.idxOf k, List.idxOf_lt_length_iff.mpr h⟩) else none +/-- The values stored under the keys `ks'` (skipping any that are not keys). -/ def valuesAt (fm : FiniteMap A B ks) (ks' : List A) : List B := - ks'.filterMap (fun k => lookup? k fm.val) - -omit [Lattice B] in -private theorem lookup?_eq_some_of_mem : ∀ {l : List (A × B)}, - (l.map Prod.fst).Nodup → ∀ {k : A} {v : B}, (k, v) ∈ l → - lookup? k l = some v - | [], _, _, _, h => by simp at h - | p :: l', hnd, k, v, h => by - simp only [List.map_cons, List.nodup_cons] at hnd - rcases List.mem_cons.mp h with heq | h' - · rw [← heq] - simp [lookup?] - · rw [lookup?, if_neg ?_] - · exact lookup?_eq_some_of_mem hnd.2 h' - · intro hpk - subst hpk - have := List.mem_map_of_mem Prod.fst h' - exact hnd.1 this + ks'.filterMap fm.lookup omit [Lattice B] in theorem mem_valuesAt (hks : ks.Nodup) {fm : FiniteMap A B ks} {k : A} {v : B} - {ks' : List A} (hk : k ∈ ks') (h : (k, v) ∈ fm) : v ∈ valuesAt fm ks' := - List.mem_filterMap.mpr - ⟨k, hk, lookup?_eq_some_of_mem (fm.property.symm ▸ hks) h⟩ + {ks' : List A} (hk : k ∈ ks') (h : (k, v) ∈ fm) : v ∈ valuesAt fm ks' := by + refine List.mem_filterMap.mpr ⟨k, hk, ?_⟩ + obtain ⟨i, hi, rfl⟩ := h + have hik : ks.get i = k := hi + have hmem : k ∈ ks := hik ▸ ks.get_mem i + show (if h : k ∈ ks then + some (fm ⟨ks.idxOf k, List.idxOf_lt_length_iff.mpr h⟩) else none) = some (fm i) + rw [dif_pos hmem] + have : (⟨ks.idxOf k, List.idxOf_lt_length_iff.mpr hmem⟩ : Fin ks.length) = i := + hks.get_inj_iff.mp (by rw [List.idxOf_get, hi]) + rw [this] -private theorem lookup?_forall₂ {l₁ l₂ : List (A × B)} - (h : List.Forall₂ (fun p q : A × B => p.1 = q.1 ∧ p.2 ≤ q.2) l₁ l₂) (k : A) : - Option.Rel (· ≤ ·) (lookup? k l₁) (lookup? k l₂) := by - induction h with - | nil => exact Option.Rel.none - | @cons p q l₁ l₂ hpq hrest ih => - rw [lookup?, lookup?] - by_cases hc : q.1 = k - · rw [if_pos hc, if_pos (hpq.1.trans hc)] - exact Option.Rel.some hpq.2 - · rw [if_neg hc, if_neg (fun hp => hc (hpq.1 ▸ hp))] - exact ih +private theorem lookup_rel {fm₁ fm₂ : FiniteMap A B ks} (hle : fm₁ ≤ fm₂) (k : A) : + Option.Rel (· ≤ ·) (fm₁.lookup k) (fm₂.lookup k) := by + show Option.Rel _ + (if h : k ∈ ks then some (fm₁ ⟨ks.idxOf k, List.idxOf_lt_length_iff.mpr h⟩) else none) + (if h : k ∈ ks then some (fm₂ ⟨ks.idxOf k, List.idxOf_lt_length_iff.mpr h⟩) else none) + by_cases hk : k ∈ ks + · rw [dif_pos hk, dif_pos hk]; exact Option.Rel.some (le_def.mp hle _) + · rw [dif_neg hk, dif_neg hk]; exact Option.Rel.none theorem valuesAt_le {fm₁ fm₂ : FiniteMap A B ks} (hle : fm₁ ≤ fm₂) (ks' : List A) : @@ -415,11 +176,11 @@ theorem valuesAt_le {fm₁ fm₂ : FiniteMap A B ks} (hle : fm₁ ≤ fm₂) induction ks' with | nil => exact List.Forall₂.nil | cons k ks'' ih => - have hrel := lookup?_forall₂ (le_iff.mp hle) k + have hrel := lookup_rel hle k rw [valuesAt, valuesAt, List.filterMap_cons, List.filterMap_cons] revert hrel - generalize lookup? k fm₁.val = o₁ - generalize lookup? k fm₂.val = o₂ + generalize fm₁.lookup k = o₁ + generalize fm₂.lookup k = o₂ intro hrel cases hrel with | none => simpa [valuesAt] using ih @@ -427,120 +188,6 @@ theorem valuesAt_le {fm₁ fm₂ : FiniteMap A B ks} (hle : fm₁ ≤ fm₂) end ValuesAt -section Iso - -omit [Lattice B] in -theorem val_ne_nil {k : A} {ks' : List A} (fm : FiniteMap A B (k :: ks')) : - fm.val ≠ [] := fun h => by - have hp := fm.property - rw [h] at hp - simp at hp - -def headVal {k : A} {ks' : List A} : FiniteMap A B (k :: ks') → B - | ⟨[], h⟩ => absurd h (by simp) - | ⟨p :: _, _⟩ => p.2 - -def pop {k : A} {ks' : List A} : FiniteMap A B (k :: ks') → FiniteMap A B ks' - | ⟨[], h⟩ => absurd h (by simp) - | ⟨_ :: l, h⟩ => - ⟨l, by simp only [List.map_cons, List.cons.injEq] at h; exact h.2⟩ - -omit [Lattice B] in -theorem val_eq_cons {k : A} {ks' : List A} : - ∀ fm : FiniteMap A B (k :: ks'), fm.val = (k, fm.headVal) :: fm.pop.val - | ⟨[], h⟩ => absurd h (by simp) - | ⟨p :: l, h⟩ => by - simp only [List.map_cons, List.cons.injEq] at h - simp [headVal, pop, ← h.1] - -def toIter : {ks : List A} → FiniteMap A B ks → IterProd B PUnit ks.length - | [], _ => PUnit.unit - | _ :: _, fm => (fm.headVal, toIter fm.pop) - -def ofIter : (ks : List A) → IterProd B PUnit ks.length → FiniteMap A B ks - | [], _ => ⟨[], rfl⟩ - | k :: ks', ip => - ⟨(k, ip.1) :: (ofIter ks' ip.2).val, by - simp [(ofIter ks' ip.2).property]⟩ - -omit [Lattice B] in -theorem ofIter_toIter : ∀ {ks : List A} (fm : FiniteMap A B ks), - ofIter ks (toIter fm) = fm - | [], fm => by - obtain ⟨val, hprop⟩ := fm - cases val with - | nil => rfl - | cons p l => exact absurd hprop (by simp) - | k :: ks', fm => Subtype.ext (by - show (k, fm.headVal) :: (ofIter ks' (toIter fm.pop)).val = fm.val - rw [ofIter_toIter fm.pop, ← val_eq_cons fm]) - -omit [Lattice B] in -theorem toIter_ofIter : ∀ (ks : List A) (ip : IterProd B PUnit ks.length), - toIter (ofIter ks ip) = ip - | [], _ => rfl - | k :: ks', ip => by - show (headVal (ofIter (k :: ks') ip), toIter (pop (ofIter (k :: ks') ip))) = ip - rw [show pop (ofIter (k :: ks') ip) = ofIter ks' ip.2 from rfl, - toIter_ofIter ks' ip.2] - rfl - -theorem headVal_le {k : A} {ks' : List A} {fm₁ fm₂ : FiniteMap A B (k :: ks')} - (h : fm₁ ≤ fm₂) : fm₁.headVal ≤ fm₂.headVal := by - have h' := le_iff.mp h - rw [val_eq_cons fm₁, val_eq_cons fm₂] at h' - exact (List.forall₂_cons.mp h').1.2 - -theorem pop_le {k : A} {ks' : List A} {fm₁ fm₂ : FiniteMap A B (k :: ks')} - (h : fm₁ ≤ fm₂) : fm₁.pop ≤ fm₂.pop := by - rw [le_iff] - have h' := le_iff.mp h - rw [val_eq_cons fm₁, val_eq_cons fm₂] at h' - exact (List.forall₂_cons.mp h').2 - -theorem toIter_monotone : ∀ {ks : List A}, - Monotone (toIter : FiniteMap A B ks → IterProd B PUnit ks.length) - | [] => fun _ _ _ => le_refl _ - | _ :: _ => fun _ _ h => - Prod.mk_le_mk.mpr ⟨headVal_le h, toIter_monotone (pop_le h)⟩ - -theorem ofIter_monotone : ∀ (ks : List A), Monotone (ofIter (A := A) (B := B) ks) - | [] => fun _ _ _ => le_refl _ - | k :: ks' => fun ip₁ ip₂ h => by - rw [le_iff] - show List.Forall₂ _ ((k, ip₁.1) :: (ofIter ks' ip₁.2).val) - ((k, ip₂.1) :: (ofIter ks' ip₂.2).val) - exact List.Forall₂.cons ⟨rfl, h.1⟩ (le_iff.mp (ofIter_monotone ks' h.2)) - -def fixedHeight [FiniteHeightLattice B] (ks : List A) : - FiniteHeightLattice (FiniteMap A B ks) := - FiniteHeightLattice.transport - (ofIter ks) toIter (ofIter_monotone ks) toIter_monotone - (toIter_ofIter ks) ofIter_toIter - -instance [FiniteHeightLattice B] : FiniteHeightLattice (FiniteMap A B ks) := - fixedHeight ks - -omit [Lattice B] in -theorem mem_ofIter_build {b : B} : ∀ {ks : List A} {k : A} {v : B}, - (k, v) ∈ ofIter ks (IterProd.build b PUnit.unit ks.length) → v = b - | [], _, _, h => by simp [ofIter, mem_def] at h - | k' :: ks', k, v, h => by - rcases List.mem_cons.mp h with heq | h' - · exact (Prod.ext_iff.mp heq).2 - · exact mem_ofIter_build h' - -theorem bot_contains_bots [FiniteHeightLattice B] {k : A} {v : B} - (h : (k, v) ∈ (fixedHeight ks).bot) : v = (⊥ : B) := by - have hbot : (fixedHeight ks).bot - = ofIter ks (IterProd.build (⊥ : B) (⊥ : PUnit) ks.length) := by - show ofIter ks (IterProd.fixedHeight (A := B) (B := PUnit) ks.length).bot = _ - rw [IterProd.bot_fixedHeight] - rw [hbot] at h - exact mem_ofIter_build h - -end Iso - end FiniteMap end Spa diff --git a/lean/Spa/Lattice/Tuple.lean b/lean/Spa/Lattice/Tuple.lean new file mode 100644 index 0000000..ba1f964 --- /dev/null +++ b/lean/Spa/Lattice/Tuple.lean @@ -0,0 +1,65 @@ +import Spa.Lattice.IterProd +import Spa.Isomorphism + +namespace Spa + +namespace Tuple + +universe u + +variable {B : Type u} + +private def iterOfFun : {n : ℕ} → (Fin n → B) → IterProd B PUnit n + | 0, _ => PUnit.unit + | _ + 1, f => (f 0, iterOfFun (Fin.tail f)) + +private def funOfIter : {n : ℕ} → IterProd B PUnit n → (Fin n → B) + | 0, _ => Fin.elim0 + | _ + 1, ip => Fin.cons ip.1 (funOfIter ip.2) + +private theorem funOfIter_iterOfFun : ∀ {n : ℕ} (f : Fin n → B), + funOfIter (iterOfFun f) = f + | 0, _ => funext fun i => i.elim0 + | _ + 1, f => by + show Fin.cons (f 0) (funOfIter (iterOfFun (Fin.tail f))) = f + rw [funOfIter_iterOfFun (Fin.tail f), Fin.cons_self_tail] + +private theorem iterOfFun_funOfIter : ∀ {n : ℕ} (ip : IterProd B PUnit n), + iterOfFun (funOfIter ip) = ip + | 0, PUnit.unit => rfl + | _ + 1, ip => by + show (funOfIter ip 0, iterOfFun (Fin.tail (funOfIter ip))) = ip + rw [show funOfIter ip = Fin.cons ip.1 (funOfIter ip.2) from rfl] + simp [Fin.cons_zero, Fin.tail_cons, iterOfFun_funOfIter ip.2] + +variable [Lattice B] + +private theorem funOfIter_mono {n : ℕ} : + Monotone (funOfIter : IterProd B PUnit n → (Fin n → B)) := by + induction n with + | zero => intro _ _ _ i; exact i.elim0 + | succ n ih => + intro ip₁ ip₂ h i + obtain ⟨h1, h2⟩ := Prod.le_def.mp h + rw [show funOfIter ip₁ = Fin.cons ip₁.1 (funOfIter ip₁.2) from rfl, + show funOfIter ip₂ = Fin.cons ip₂.1 (funOfIter ip₂.2) from rfl] + induction i using Fin.cases with + | zero => rw [Fin.cons_zero, Fin.cons_zero]; exact h1 + | succ j => rw [Fin.cons_succ, Fin.cons_succ]; exact ih h2 j + +private theorem iterOfFun_mono {n : ℕ} : + Monotone (iterOfFun : (Fin n → B) → IterProd B PUnit n) := by + induction n with + | zero => intro f g _; exact le_of_eq rfl + | succ n ih => + intro f g h + exact Prod.le_def.mpr ⟨h 0, ih fun i => h i.succ⟩ + +instance instFiniteHeight {n : ℕ} [FiniteHeightLattice B] : + FiniteHeightLattice (Fin n → B) := + FiniteHeightLattice.transport funOfIter iterOfFun + funOfIter_mono iterOfFun_mono iterOfFun_funOfIter funOfIter_iterOfFun + +end Tuple + +end Spa diff --git a/lean/Spa/Showable.lean b/lean/Spa/Showable.lean index b4dd2ca..3990043 100644 --- a/lean/Spa/Showable.lean +++ b/lean/Spa/Showable.lean @@ -30,7 +30,8 @@ instance {α : Type*} [Showable α] : Showable (AboveBelow α) := instance {α β : Type*} {ks : List α} [Showable α] [Showable β] : Showable (FiniteMap α β ks) := ⟨fun fm => - "{" ++ fm.val.foldr (fun p rest => show' p.1 ++ " ↦ " ++ show' p.2 ++ ", " ++ rest) "" + "{" ++ (FiniteMap.toList fm).foldr + (fun p rest => show' p.1 ++ " ↦ " ++ show' p.2 ++ ", " ++ rest) "" ++ "}"⟩ end Spa