diff --git a/SSA/Experimental/Bits/AutoStructs/Basic.lean b/SSA/Experimental/Bits/AutoStructs/Basic.lean index b6339ebb6..29b3a6e1c 100644 --- a/SSA/Experimental/Bits/AutoStructs/Basic.lean +++ b/SSA/Experimental/Bits/AutoStructs/Basic.lean @@ -5,13 +5,17 @@ Released under Apache 2.0 license as described in the file LICENSE. import Std.Data.HashSet import Std.Data.HashMap import Std.Data.HashMap.Lemmas +import Batteries.Data.Fin.Basic +import Mathlib.Computability.NFA import Mathlib.Data.Finset.Basic import Mathlib.Data.Finset.Card import Mathlib.Data.List.Perm.Basic import Mathlib.Data.List.Perm.Lattice import Mathlib.Data.List.Perm.Subperm import SSA.Experimental.Bits.AutoStructs.ForLean +import SSA.Experimental.Bits.AutoStructs.ForMathlib import SSA.Experimental.Bits.AutoStructs.FinEnum +import SSA.Experimental.Bits.AutoStructs.GoodNFA abbrev State := Nat @@ -20,73 +24,233 @@ abbrev State := Nat The definition of a computational automaton. It is meant to be more efficient than the definition in Mathlib. -/ -structure NFA (A : Type 0) [BEq A] [Hashable A] [DecidableEq A] [FinEnum A] where +structure CNFA (A : Type 0) [BEq A] [Hashable A] [DecidableEq A] [FinEnum A] where stateMax : State initials : Std.HashSet State finals : Std.HashSet State trans : Std.HashMap (State × A) (Std.HashSet State) deriving Repr +section sim + +variable {A : Type} [BEq A] [Hashable A] [DecidableEq A] [FinEnum A] + +noncomputable def CNFA.states (m : CNFA A) : Finset State := Finset.range m.stateMax + +instance CNFA.statesFinset (m : CNFA A) : Fintype m.states := (Finset.range m.stateMax).fintypeCoeSort + +@[simp] +lemma CNFA.states_lt (m : CNFA A) s : s ∈ m.states → s < m.stateMax := by simp [CNFA.states] + +/-- +A simulation between a concrete NFA and an abstract NFA consists in a map from +concrete to abstract states which satisfies some properties. +-/ +structure CNFA.SimUnpacked (m : CNFA A) (M : NFA A Q) (R : Set Q) (T : Set (Q × A × Q)) (f : m.states → Q) where + injective : Function.Injective f + reduced : M.Reachable = ⊤ -- all the states are reachable + accept s : s.val ∈ m.finals ↔ f s ∈ M.accept + initial s : s.val ∈ m.initials ↔ f s ∈ M.start + initial_all q : q ∈ M.start → ∃ s, f s = q ∧ s.val ∈ m.initials + trans_match₁ s a q' : q' ∈ M.step (f s) a → f s ∈ R → (f s, a, q') ∉ T → ∃ s', f s' = q' ∧ s'.val ∈ m.trans.getD (s.val, a) ∅ + trans_match₂ s a s' : s' ∈ m.trans.getD (s.val, a) ∅ → ∃ hin : s' ∈ m.states, f ⟨s', hin⟩ ∈ M.step (f s) a + +attribute [aesop 50% unsafe] + CNFA.SimUnpacked.initial_all + CNFA.SimUnpacked.trans_match₁ + CNFA.SimUnpacked.trans_match₂ + +def CNFA.Sim (m : CNFA A) (A : NFA A S) := ∃ f, CNFA.SimUnpacked m A ⊤ ∅ f + +def sim_closed_set (m : CNFA A) (M : NFA A S) (R : Set S) (T : Set (S × A × S)) f (hcl: M.closed_set R) : + T = ∅ → + m.SimUnpacked M R T f → m.Sim M := by + rintro rfl ⟨_, hr, _, _, _, h, _⟩; use f + constructor <;> try assumption + rintro s a q' hq' hreach _ + apply h <;> try assumption + rw [←hr] at hreach + apply NFA.reachable_sub_closed_set at hreach <;> assumption + +end sim + section basics variable {A : Type} [BEq A] [Hashable A] [DecidableEq A] [FinEnum A] -def NFA.empty : NFA A := { +def CNFA.empty : CNFA A := { stateMax := 0 initials := ∅ finals := ∅ trans := ∅ } -def NFA.newState (m : NFA A) : State × NFA A := +def CNFA.newState (m : CNFA A) : State × CNFA A := let old := m.stateMax let m := { m with stateMax := old + 1 } (old, m) -def NFA.addTrans (m : NFA A) (a : A) (s s' : State) : NFA A := +def CNFA.addTrans (m : CNFA A) (a : A) (s s' : State) : CNFA A := let ns := m.trans.getD (s, a) ∅ let ns := ns.insert s' { m with trans := m.trans.insert (s, a) ns } -def NFA.addManyTrans (m : NFA A) (a : List A) (s s' : State) : NFA A := +def CNFA.addManyTrans (m : CNFA A) (a : List A) (s s' : State) : CNFA A := a.foldl (init := m) fun m a => m.addTrans a s s' -def NFA.addInitial (m : NFA A) (s : State) : NFA A := +def CNFA.addInitial (m : CNFA A) (s : State) : CNFA A := { m with initials := m.initials.insert s } -def NFA.addFinal (m : NFA A) (s : State) : NFA A := +def CNFA.addFinal (m : CNFA A) (s : State) : CNFA A := { m with finals := m.finals.insert s } -def NFA.transSet (m : NFA A) (ss : Std.HashSet State) (a : A) : Std.HashSet State := +def CNFA.createSink (m : CNFA A) : State × CNFA A := + let (s, m) := m.newState + let m := m.addInitial s + let m := FinEnum.toList (α := A).foldl (init := m) fun m a => + m.addTrans a s s + (s, m) + +def CNFA.transSet (m : CNFA A) (ss : Std.HashSet State) (a : A) : Std.HashSet State := ss.fold (init := ∅) fun ss' s => ss'.insertMany $ m.trans.getD (s, a) ∅ -instance NFA_Inhabited : Inhabited (NFA A) where - default := NFA.empty +def CNFA.transBV (m : CNFA A) (s : m.states) (a : A) : BitVec m.stateMax := + let ts := m.trans.getD (s, a) ∅ + BitVec.ofFn (fun n => n ∈ ts) + +def CNFA.transSetBV (m : CNFA A) (ss : BitVec m.stateMax) (a : A) : BitVec m.stateMax := + (List.finRange m.stateMax).foldl (init := BitVec.zero m.stateMax) fun res n => + if ss[n] then res ||| m.transBV ⟨n.val, by simp [CNFA.states]⟩ a else res + +/- +Computes the set of states of the automaton. This is only meant to be used in proofs +and is quite horrible. The alternative is to have a dependent type asserting that +all the states involved are `< stateMax` which may be a better idea... +-/ +structure CNFA.WF (m : CNFA A) where + initials_lt : ∀ s ∈ m.initials, s < m.stateMax + finals_lt : ∀ s ∈ m.finals, s < m.stateMax + trans_src_lt : ∀ s_a ∈ m.trans, s_a.1 < m.stateMax + trans_tgt_lt : ∀ (s_a : State × A) ss' s', m.trans[s_a]? = some ss' → s' ∈ ss' → s' < m.stateMax + +structure GoodCNFA (n : Nat) where + m : CNFA (BitVec n) + wf : m.WF + -- etc? + +def GoodCNFA.Sim (m : GoodCNFA n) (M : GoodNFA n) := + m.m.Sim M.M + +attribute [simp] CNFA.WF.initials_lt CNFA.WF.trans_src_lt CNFA.WF.trans_tgt_lt CNFA.WF.finals_lt +attribute [aesop 50% unsafe] CNFA.WF.initials_lt CNFA.WF.trans_src_lt CNFA.WF.trans_tgt_lt CNFA.WF.finals_lt + +@[simp, aesop 50% unsafe] +lemma CNFA.WF.trans_src_lt' {m : CNFA A} (hwf : m.WF) : + ∀ s a, (s, a) ∈ m.trans → s < m.stateMax := by + intros s a hin; simp [hwf.trans_src_lt _ hin] + +@[simp, aesop 50% unsafe] +lemma CNFA.WF.trans_tgt_lt' [LawfulBEq A] {m : CNFA A} (hwf : m.WF) : + ∀ s a s', s' ∈ m.trans.getD (s, a) ∅ → s' ∈ m.states := by + intros s a s' hin + rw [Std.HashMap.getD_eq_getD_getElem?] at hin + rcases htrans : m.trans[(s, a)]? with ⟨⟩ | ⟨ts⟩ + · simp_all + · simp [CNFA.states]; apply hwf.trans_tgt_lt (s, a) ts <;> simp_all + +@[simp, aesop 50% unsafe] +lemma wf_newState (m : CNFA A) (hwf : m.WF) : + m.newState.2.WF := by + constructor <;> intros <;> apply Nat.lt_add_one_of_lt <;> simp_all [CNFA.newState, CNFA.WF] + apply hwf.trans_tgt_lt <;> assumption + +@[simp, aesop 50% unsafe] +lemma wf_addInitial (m : CNFA A) (hwf : m.WF) (hin : s ∈ m.states) : + (m.addInitial s).WF := by + constructor <;> intros <;> simp_all [CNFA.addInitial, CNFA.WF] + { casesm* _ ∨ _ <;> subst_eqs <;> simp_all } + { apply hwf.trans_tgt_lt <;> assumption } + +@[simp, aesop 50% unsafe] +lemma wf_addFinal (m : CNFA A) (hwf : m.WF) (hin : s ∈ m.states) : + (m.addFinal s).WF := by + constructor <;> intros <;> simp_all [CNFA.addFinal, CNFA.WF] <;> aesop + +@[simp, aesop 50% unsafe] +lemma states_addInitial (m : CNFA A) (s' : State) : + (m.addInitial s').states = m.states := by + simp_all [CNFA.addInitial, CNFA.states] + +@[simp, aesop 50% unsafe] +lemma states_addFinal (m : CNFA A) (s' : State) : + (m.addFinal s').states = m.states := by + simp_all [CNFA.addFinal, CNFA.states] + +@[simp, aesop 50% unsafe] +lemma states_addTrans (m : CNFA A) (a : A) (s1 s2 : State) : + (m.addTrans a s1 s2).states = m.states := by + simp_all [CNFA.addTrans, CNFA.states] + +@[simp, aesop 50% unsafe] +lemma mem_states_newState (m : CNFA A) (s : State) (hin : s ∈ m.states) : + s ∈ m.newState.2.states := by + simp_all [CNFA.newState, CNFA.states]; omega + +@[simp, aesop 50% unsafe] +lemma states_newState (m : CNFA A) : + m.newState.2.states = m.states ∪ { m.stateMax } := by + simp_all [CNFA.newState, CNFA.states, Finset.range_add] + +@[simp, aesop 50% unsafe] +lemma newState_eq (m : CNFA A) : + m.newState.1 = m.stateMax := by + simp_all [CNFA.newState, CNFA.states, Finset.range_add] + +@[simp, aesop 50% unsafe] +lemma mem_states_newState_self (m : CNFA A) : + m.newState.1 ∈ m.newState.2.states := by + simp_all [CNFA.newState, CNFA.states] + +@[simp, aesop 50% unsafe] +lemma wf_addTrans [LawfulBEq A] (m : CNFA A) (hwf : m.WF) s a s' (hin : s ∈ m.states) (hin' : s' ∈ m.states) : + (m.addTrans a s s').WF := by + constructor <;> simp_all [CNFA.addTrans, CNFA.WF] + { intros s a htin; casesm* _ ∨ _ <;> aesop } + { rintro s1 b ss'1 s'1 hsome hmem + rw [Std.HashMap.getElem?_insert] at hsome; split at hsome; simp_all + { casesm* _ ∧ _; subst_eqs; simp_all; cases_type Or; simp_all + by_cases hmem : (s, a) ∈ m.trans + { apply Std.HashMap.getElem?_eq_some_getD (fallback := ∅) at hmem + apply hwf.trans_tgt_lt _ _ _ hmem; assumption } + { have : m.trans.getD (s, a) ∅ = ∅ := by apply Std.HashMap.getD_eq_fallback; assumption + simp_all } + } + { apply hwf.trans_tgt_lt _ _ _ hsome; assumption }} + +instance CNFA_Inhabited : Inhabited (CNFA A) where + default := CNFA.empty end basics -- A generic function to define automata constructions using worklist algorithms section worklist -variable (A : Type) [BEq A] [Hashable A] [DecidableEq A] [FinEnum A] -variable {S : Type} [BEq S] [LawfulBEq S] [Hashable S] [DecidableEq S] -variable (stateSpace : Finset S) - -abbrev inSS : Type := { sa : S // sa ∈ stateSpace } +variable (A : Type) [BEq A] [LawfulBEq A] [Hashable A] [DecidableEq A] [FinEnum A] +variable (S : Type) [Fintype S] [BEq S] [LawfulBEq S] [Hashable S] [DecidableEq S] -private structure worklist.St where - m : NFA A - map : Std.HashMap (inSS stateSpace) State := ∅ - worklist : Array (inSS stateSpace) := ∅ +structure worklist.St where + m : CNFA A + map : Std.HashMap S State := ∅ + worklist : Array S := ∅ worklist_nodup : worklist.toList.Nodup worklist_incl : ∀ sa ∈ worklist, sa ∈ map attribute [aesop 10% unsafe] worklist.St.worklist_nodup worklist.St.worklist_incl attribute [simp] worklist.St.worklist_nodup worklist.St.worklist_incl -private def worklist.St.meas (st : worklist.St A stateSpace) : ℕ := - Finset.card $ stateSpace.attach.filter fun x => x ∉ st.map.keys ∨ x ∈ st.worklist.toList +def worklist.St.meas (st : worklist.St A S) : ℕ := + Finset.card $ Finset.univ |>.filter fun x => x ∉ st.map.keys ∨ x ∈ st.worklist.toList theorem List.perm_subset_iff_right {l1 l2 : List α} (hperm : l1.Perm l2) (l : List α) : @@ -96,7 +260,7 @@ theorem List.perm_subset_iff_right {l1 l2 : List α} (hperm : l1.Perm l2) (l : L { intros hincl x hin; apply List.Perm.mem_iff (a := x) at hperm ; apply hperm.mpr; apply hincl; assumption } open List in -private theorem list_perm_trick (x y a b c : List α) : +theorem list_perm_trick (x y a b c : List α) : y ~ b ++ x → x ~ a ++ c → y ~ a ++ b ++ c := by intros h1 h2 have hi : b ++ x ~ b ++ (a ++ c) := by apply Perm.append_left; assumption @@ -104,7 +268,7 @@ private theorem list_perm_trick (x y a b c : List α) : have := h1.trans (hi.trans this) aesop -private def worklist.St.addOrCreateState (st : worklist.St A stateSpace) (final? : Bool) (sa : inSS stateSpace) : State × worklist.St A stateSpace := +def worklist.St.addOrCreateState (st : worklist.St A S) (final? : Bool) (sa : S) : State × worklist.St A S := match heq : st.map[sa]? with | some s => (s, st) | none => @@ -116,14 +280,35 @@ private def worklist.St.addOrCreateState (st : worklist.St A stateSpace) (final? simp [worklist]; apply List.nodup_middle.mpr; simp intros hc; apply Array.Mem.mk at hc; apply st.worklist_incl at hc; simp at hc; apply Std.HashMap.get?_none_not_mem at heq; contradiction have worklist_incl : ∀ sa ∈ worklist, sa ∈ map := by - simp [worklist, map]; intros sa' hsa' hin; apply Array.mem_push at hin; rcases hin with hin | heq + simp [worklist, map]; intros sa' hin; apply Array.mem_push at hin; rcases hin with hin | heq { apply st.worklist_incl at hin; aesop } { aesop } let st' := { st with m, map, worklist, worklist_nodup, worklist_incl } (s, st') -omit [BEq S] [LawfulBEq S] in -theorem addOrCreateState_grow (st : worklist.St A stateSpace) (b : Bool) (sa : inSS stateSpace) : +omit [Fintype S] [LawfulBEq A] in +lemma addOrCreate_preserves_map (st : worklist.St A S) (final? : Bool) (sa sa' : S) : + let (_, st') := st.addOrCreateState _ _ final? sa' + st.map[sa]? = some s → + st'.map[sa]? = some s := by + simp_all [worklist.St.addOrCreateState]; intros hmap + split; simp_all + dsimp only + simp_all [Std.HashMap.getElem?_insert] + rintro rfl; simp_all + +omit [Fintype S] [DecidableEq S] [LawfulBEq A] in +lemma addOrCreate_preserves_mem (st : worklist.St A S) (final? : Bool) (sa sa' : S) : + let (_, st') := st.addOrCreateState _ _ final? sa' + sa ∈ st.map → + sa ∈ st'.map := by + simp_all [worklist.St.addOrCreateState]; intros hmap + split; simp_all + dsimp only + simp_all [Std.HashMap.getElem?_insert] + +omit [Fintype S] [DecidableEq S] [LawfulBEq A] in +theorem addOrCreateState_grow (st : worklist.St A S) (b : Bool) (sa : S) : let (_, st') := st.addOrCreateState _ _ b sa ∃ sas, List.Perm st'.map.keys (sas ++ st.map.keys) ∧ st'.worklist.toList = st.worklist.toList ++ sas := by unfold worklist.St.addOrCreateState @@ -135,35 +320,65 @@ theorem addOrCreateState_grow (st : worklist.St A stateSpace) (b : Bool) (sa : i apply Std.HashMap.insert_keys_perm_new apply Std.HashMap.get?_none_not_mem; assumption -private def processOneElem (final : S → Bool) (s : State) (st : worklist.St A stateSpace) : A × inSS stateSpace → worklist.St A stateSpace := +def processOneElem (final : S → Bool) (s : State) (st : worklist.St A S) : A × S → worklist.St A S := fun (a', sa') => let (s', st') := st.addOrCreateState _ _ (final sa') sa' let m := st'.m.addTrans a' s s' { st' with m } -omit [BEq S] [LawfulBEq S] in -theorem processOneElem_grow (st : worklist.St A stateSpace) (final : S → Bool) (a : A) (sa' : inSS stateSpace) (s : State) : +omit [Fintype S] [LawfulBEq A] in +lemma processOneElem_preserves_map (st : worklist.St A S) (final : S → Bool) (a : A) (sa sa' : S) (s s' : State) : + let st' := processOneElem _ _ final s st (a, sa') + st.map[sa]? = some s' → + st'.map[sa]? = some s' := by + simp_all [processOneElem, addOrCreate_preserves_map] + +omit [Fintype S] [DecidableEq S] [LawfulBEq A] in +lemma processOneElem_preserves_mem (st : worklist.St A S) (final : S → Bool) (a : A) (sa sa' : S) (s : State) : + let st' := processOneElem _ _ final s st (a, sa') + sa ∈ st.map → + sa ∈ st'.map := by + simp_all [processOneElem, addOrCreate_preserves_mem] + +omit [Fintype S] [DecidableEq S] [LawfulBEq A] in +theorem processOneElem_grow (st : worklist.St A S) (final : S → Bool) (a : A) (sa' : S) (s : State) : let st' := processOneElem _ _ final s st (a, sa') ∃ sas, List.Perm st'.map.keys (sas ++ st.map.keys) ∧ st'.worklist.toList = st.worklist.toList ++ sas := by simp [processOneElem] have h := addOrCreateState_grow _ _ st (final sa') sa' - rcases heq : (worklist.St.addOrCreateState A stateSpace st (final ↑sa') sa') with ⟨x, st'⟩ + rcases heq : (worklist.St.addOrCreateState A S st (final ↑sa') sa') with ⟨x, st'⟩ simp [heq] at h rcases h with ⟨sas, h1, h2⟩ use sas -def worklist.initState (init : inSS stateSpace) : worklist.St A stateSpace := - let m := NFA.empty - let (s, m) := m.newState - let m := m.addInitial s - let map : Std.HashMap _ _ := {(init, s)} - let worklist := Array.singleton init - { m, map, worklist, worklist_nodup := by simp [worklist], worklist_incl := by simp [map, worklist] } +def worklist.initState (inits : Array S) (hinits : inits.toList.Nodup) (final? : S → Bool) : worklist.St A S := + let m := CNFA.empty (A := A) + let mapm := inits.foldl (init := (Std.HashMap.empty, m)) fun (map, m) sa => + let (s, m) := m.newState + let m := m.addInitial s + let m := if final? sa then m.addFinal s else m + (map.insert sa s, m) + let map := mapm.1 + let m := mapm.2 + let worklist_incl : ∀ sa ∈ inits, sa ∈ map := by + let mot (n : ℕ) (mapm : Std.HashMap S State × CNFA A) : Prop := + ∀ sa, ∀ k < n, inits[k]? = some sa → sa ∈ mapm.1 + suffices hccl : mot inits.size mapm by + simp_all [mot]; intros sa hin + apply Array.getElem_of_mem at hin; rcases hin with ⟨k, hk, heq⟩ + apply hccl _ _ hk (by simp_all [Array.getElem?_eq_getElem]) + apply Array.foldl_induction; simp [mot] + intros i map ih; simp [mot] at ih ⊢ + intros sa k hk hsome + apply Nat.lt_add_one_iff_lt_or_eq.mp at hk; rcases hk with hk | rfl + { right; apply ih _ _ hk hsome } + { left; simp_all [Array.getElem?_eq_getElem] } + { m, map, worklist := inits, worklist_nodup := hinits, worklist_incl } -def worklistRunAux (final : S → Bool) (f : S → Array (A × inSS stateSpace)) (init : inSS stateSpace) : NFA A := - let st0 := worklist.initState _ _ init +def worklistRun' (final : S → Bool) (inits : Array S) (hinits : inits.toList.Nodup) (f : S → Array (A × S)) : CNFA A := + let st0 := worklist.initState _ _ inits hinits final go st0 -where go (st0 : worklist.St A stateSpace) : NFA A := +where go (st0 : worklist.St A S) : CNFA A := if hemp : st0.worklist.isEmpty then st0.m else let sa? := st0.worklist.back? match heq : sa? with @@ -185,46 +400,46 @@ where go (st0 : worklist.St A stateSpace) : NFA A := | nil => simp | cons asa al ih => simp; simp at ih; intros st - let wl' := processOneElem A stateSpace final s st asa + let wl' := processOneElem A S final s st asa rcases ih wl' with ⟨sas', h1', h2'⟩; clear ih rcases processOneElem_grow _ _ st final asa.1 asa.2 s with ⟨sas, h1, h2⟩ use (sas ++ sas') constructor - { simp [wl'] at h1'; apply list_perm_trick <;> assumption } - { simp [wl'] at h2'; rw [h2] at h2'; aesop } + { simp [wl'] at h1'; apply list_perm_trick; exact h1'; exact h1 } + { simp [wl', h2] at h2'; aesop } have hincl : ∀ k, k ∈ st1.map → k ∈ st2.map := by intros k; rcases hgrow with ⟨sas, hkeys, -⟩; have := @(List.perm_subset_iff_right hkeys st1.map.keys).mpr (by aesop) k; aesop have : st1.meas < st0.meas := by - rcases heq' : sa? with ⟨⟩ | ⟨sa, hsa⟩ + rcases heq' : sa? with ⟨⟩ | ⟨sa⟩ { aesop } apply Finset.card_lt_card simp [worklist.St.meas, Finset.ssubset_iff, Finset.subset_iff] - use sa, hsa + use sa simp [sa?] at heq' constructor { constructor { apply Array.back?_mem at heq'; apply st0.worklist_incl; assumption } - { apply Array.not_elem_back_pop at heq'; simp [Array.pop] at heq'; assumption; exact st0.worklist_nodup } } + { apply Array.not_elem_back_pop at heq' <;> simp_all [Array.pop, wl] } } constructor { right; apply Array.back?_mem at heq'; apply Array.Mem.val; assumption} - rintro sa hsa hh; rcases hh with hnin | hin + rintro sa hh; rcases hh with hnin | hin { simp [hnin] } right apply List.mem_of_mem_dropLast; assumption have : st2.meas ≤ st1.meas := by apply Finset.card_le_card simp [worklist.St.meas, Finset.subset_iff] - intros sa' hsa' h + intros sa' h rcases h with hnin | hin { left; simp [st1] at hincl; intros hc; apply hnin; apply hincl; assumption } - by_cases hnew : ⟨sa', hsa'⟩ ∈ st0.map + by_cases hnew : sa' ∈ st0.map all_goals try (left; trivial) right simp [st1] at hgrow rcases hgrow with ⟨sas, hkeys2, hwl2⟩ simp [hwl2] at hin - have hnin : ⟨sa', hsa'⟩ ∉ sas := by + have hnin : sa'∉ sas := by intros hc have hdisj : st0.map.keys.Disjoint sas := by have : (sas ++ st0.map.keys).Nodup := by @@ -232,7 +447,9 @@ where go (st0 : worklist.St A stateSpace) : NFA A := assumption apply st2.map.keys_nodup simp [List.nodup_append_comm, List.disjoint_of_nodup_append, this] - aesop + apply hdisj + { simp_all [Std.HashMap.mem_keys_iff_mem]; apply hnew } + { apply hc } rcases hin <;> trivial have : st2.meas < st0.meas := by omega go st2 @@ -241,8 +458,643 @@ where go (st0 : worklist.St A stateSpace) : NFA A := | none => st0.m -- never happens termination_by st0.meas +def worklistRun (final : S → Bool) (inits : Array S) + (hinits : inits.toList.Nodup) (f : S → Array (BitVec n × S)) : GoodCNFA n := + ⟨worklistRun' _ S final inits hinits f, by sorry⟩ + +-- Correctness of the algorithm +variable (final : S → Bool) (f : S → Array (A × S)) (inits : Array S) +variable (M : NFA A σ) +variable (corr : S → σ) +variable (corr_inj : Function.Injective corr) +variable (final_corr : ∀ (s : S), final s ↔ corr s ∈ M.accept) +variable (hinit₁ : ∀ sa ∈ inits, corr sa ∈ M.start) +variable (hinit₂ : ∀ q ∈ M.start, ∃ sa, corr sa = q ∧ sa ∈ inits) +variable (hf₁: ∀ sa q' a, q' ∈ M.step (corr sa) a → ∃ sa', corr sa' = q' ∧ (a, sa') ∈ f sa) +variable (hf₂: ∀ sa a sa', (a, sa') ∈ f sa → corr sa' ∈ M.step (corr sa) a) + +def worklist.St.visited (st : worklist.St A S) : Set S := { s : S | s ∈ st.map ∧ s ∉ st.worklist } + +omit [LawfulBEq A] [Fintype S] [DecidableEq S] in +lemma addOrCreateElem_visited final? (st : worklist.St A S) sa : + st.addOrCreateState _ _ final? sa |>.2.visited = st.visited := by + simp [worklist.St.visited, worklist.St.addOrCreateState] + ext sa' + split; simp + simp; constructor <;> simp + · rintro ⟨rfl | h⟩ hnin + · exfalso; apply hnin; apply Array.mem_push_self + · constructor; assumption; intros hin; apply hnin; apply Array.push_incl sa hin + · rintro hin hnin; constructor + · right; assumption + · intros hc; apply Array.mem_push at hc + rcases hc + · simp_all + · subst_eqs + suffices _ : sa ∉ st.map by simp_all + apply Std.HashMap.get?_none_not_mem; assumption + +omit [LawfulBEq A] [Fintype S] [DecidableEq S] in +lemma processOneElem_visited (st : worklist.St A S) : + let st' := processOneElem _ _ final s st (a, sa') + st'.visited = st.visited := by + intros st' + rw [←addOrCreateElem_visited _ _ (final sa') st sa'] + simp [st', processOneElem, worklist.St.visited] + +def worklist.St.R (st : worklist.St A S) : Set σ := { q : σ | ∃ sa ∈ st.visited, corr sa = q } + +structure StInv (T : Set (S × A × S)) (st : worklist.St A S) where + wf : st.m.WF + map_states : ∀ (sa : S) s, st.map[sa]? = some s → s ∈ st.m.states + map_surj : ∀ s : st.m.states, ∃ (sa : S), st.map[sa]? = some s.val + map_inj : ∀ (s : st.m.states) (sa sa' : S), st.map[sa]? = some s.val → st.map[sa']? = some s.val → sa = sa' + frontier : ∀ sa a q', sa ∈ st.visited → q' ∈ M.step (corr sa) a → + ∃ sa', corr sa' = q' ∧ (sa' ∈ st.map ∨ (sa, a, sa') ∈ T) + +attribute [simp] StInv.wf StInv.map_states StInv.map_surj StInv.frontier + +-- is there a better way? +local notation "StInv'" => StInv A S M corr + +-- We make a map from the (nat) states of the automaton to the +-- abstract states using the axiom of choice applied to the +-- property `StInv.map_surj` +noncomputable def StInv.mFun (inv : StInv A S M corr T st) : st.m.states → S := + Classical.choose $ Classical.axiomOfChoice inv.map_surj + +omit [Fintype S] [LawfulBEq S] [DecidableEq S] [LawfulBEq A] in +lemma StInv.mFun_spec (inv : StInv' T st) (s : st.m.states) : st.map[inv.mFun _ _ _ _ s]? = some s := by + simp [StInv.mFun] + apply Classical.choose_spec (Classical.axiomOfChoice inv.map_surj) + +omit [Fintype S] [LawfulBEq S] [DecidableEq S] [LawfulBEq A] in +lemma StInv.mFun_eq (inv : StInv' T st) (s : st.m.states) (sa : S) : + st.map[sa]? = some s → sa = inv.mFun _ _ _ _ s := by + intros heq; apply inv.map_inj + · exact heq + · apply inv.mFun_spec + +omit [Fintype S] [LawfulBEq S] [DecidableEq S] [LawfulBEq A] in +lemma StInv.mFun_inj (inv : StInv' T st) (s s' : st.m.states) : + inv.mFun _ _ _ _ s = inv.mFun _ _ _ _ s' → s.val = s'.val := by + intros heq + have h1 := inv.mFun_spec _ _ _ _ s + have h2 := inv.mFun_spec _ _ _ _ s' + rcases s; rcases s' + simp_all + +omit [Fintype S] [LawfulBEq S] [DecidableEq S] [LawfulBEq A] in +lemma StInv.mFun_inj' (inv : StInv' T st) : Function.Injective (inv.mFun _ _ _ _) := by + rintro ⟨s1, hs1⟩ ⟨s2, hs2⟩ heq; simp + apply inv.mFun_inj _ _ _ _ ⟨s1, hs1⟩ ⟨s2, hs2⟩ heq + +omit [Fintype S] [DecidableEq S] [LawfulBEq A] in +lemma mFun_mem (inv : StInv' T st) (s : st.m.states) : inv.mFun _ _ _ _ s ∈ st.map := + Std.HashMap.mem_of_get? (inv.mFun_spec _ _ _ _ s) + +omit [LawfulBEq A] [Fintype S] [DecidableEq S] in +lemma processOneElem_states (st : worklist.St A S) (final : S → Bool) (a : A) (sa : S) (s : State) : + (processOneElem A S final s st (a, sa)).m.states = + if sa ∉ st.map then st.m.newState.2.states else st.m.states := by + simp [processOneElem, worklist.St.addOrCreateState] + split + next s' heq => + dsimp + have _ := Std.HashMap.mem_of_get? heq + split_ifs; simp_all + next heq => + dsimp + have _ := Std.HashMap.get?_none_not_mem heq + split <;> simp_all + +omit [LawfulBEq A] [Fintype S] [DecidableEq S] in +lemma processOneElem_mem_states (st : worklist.St A S) (final : S → Bool) (a : A) (sa : S) (s : State) : + s ∈ (processOneElem A S final s st (a, sa)).m.states → + s ∈ st.m.states ∨ s = st.m.stateMax := by + simp [processOneElem_states]; split <;> simp_all + +omit [LawfulBEq A] [Fintype S] in +lemma processOneElem_map (st : worklist.St A S) (final : S → Bool) (a : A) (sa sa' : S) (s : State) : + (processOneElem A S final s st (a, sa)).map[sa']? = + match st.map[sa']? with + | some s => some s + | none => if sa = sa' then some st.m.stateMax else none := by + simp [processOneElem, worklist.St.addOrCreateState] + split + next s' heq => + dsimp + split <;> simp_all + split <;> simp_all + next heq => + dsimp; split <;> (rw [Std.HashMap.getElem?_insert]; split <;> simp_all) + +omit [LawfulBEq A] [Fintype S] in +lemma processOneElem_new_map (st : worklist.St A S) (final : S → Bool) (a : A) (sa : S) (s : State) : + (processOneElem A S final s st (a, sa)).map[sa]? = + match st.map[sa]? with + | some s => some s + | none => some st.m.stateMax := by + simp [processOneElem_map] + +omit [LawfulBEq A] [Fintype S] [DecidableEq S] in +lemma processOneElem_initials (st : worklist.St A S) (final : S → Bool) (a : A) (sa : S) (s : State) : + (processOneElem A S final s st (a, sa)).m.initials = st.m.initials := by + simp [processOneElem, worklist.St.addOrCreateState, CNFA.addTrans, CNFA.newState, CNFA.addFinal] + split + · dsimp + · split <;> dsimp + +omit [LawfulBEq A] [Fintype S] [DecidableEq S] in +lemma processOneElem_finals (st : worklist.St A S) (final : S → Bool) (a : A) (sa : S) (s : State) : + (processOneElem A S final s st (a, sa)).m.finals = + if sa ∉ st.map ∧ final sa then st.m.finals.insert st.m.stateMax else st.m.finals := by + simp [processOneElem, worklist.St.addOrCreateState] + split + next s' heq => + dsimp + have _ := Std.HashMap.mem_of_get? heq + split_ifs <;> simp_all + simp [CNFA.addTrans] + next heq => + dsimp + have _ := Std.HashMap.get?_none_not_mem heq + split + { simp_all [CNFA.newState, CNFA.addTrans, CNFA.addFinal] } + { simp_all [CNFA.newState, CNFA.addTrans] } + +omit [Fintype S] [DecidableEq S] in +lemma processOneElem_trans (st : worklist.St A S) (final : S → Bool) (a b : A) (sa : S) (s s' : State) : + if a = b ∧ s = s' then + ∃ ssa, (processOneElem A S final s st (a, sa)).map[sa]? = some ssa ∧ + (processOneElem A S final s st (a, sa)).m.trans.getD (s', b) ∅ = + (st.m.trans.getD (s, a) ∅ |>.insert ssa) + else + (processOneElem A S final s st (a, sa)).m.trans.getD (s', b) ∅ = + st.m.trans.getD (s', b) ∅ := by + simp [processOneElem, worklist.St.addOrCreateState] + split + next _ => + casesm _ ∧ _; subst_eqs + dsimp + split + next s'' heq => + use s''; constructor; assumption + have _ := Std.HashMap.mem_of_get? heq + simp [CNFA.addTrans] + next heq => + use st.m.stateMax + simp + split_ifs <;> simp_all [CNFA.addFinal, CNFA.addTrans, CNFA.newState] + next heq => + dsimp + split + { simp_all [CNFA.newState, CNFA.addTrans, CNFA.addFinal, Std.HashMap.getD_insert]; aesop } + { simp_all [CNFA.newState, CNFA.addTrans, CNFA.addFinal, Std.HashMap.getD_insert] + split; simp_all; split <;> simp } + +omit [Fintype S] [DecidableEq S] in +lemma processOneElem_trans_preserved (st : worklist.St A S) (final : S → Bool) (a b : A) (sa : S) (s s1 s2 : State) : + s2 ∈ st.m.trans.getD (s1, b) ∅ → + s2 ∈ (processOneElem A S final s st (a, sa)).m.trans.getD (s1, b) ∅ := by + have h := processOneElem_trans _ _ st final a b sa s s1 + split_ifs at h + · obtain ⟨_, _, h2⟩ := h + simp_all + · simp_all + +noncomputable def StInv.fun (inv : StInv' T st) : st.m.states → σ := corr ∘ inv.mFun + +-- why is it needed? +include corr_inj in +omit [LawfulBEq A] [Fintype S] [LawfulBEq S] [DecidableEq S] in +lemma StInv.fun_inj (inv : StInv' T st) : + Function.Injective (inv.fun _ _ _ _) := by + simp [StInv.fun] + rw [Function.Injective.of_comp_iff] + · apply mFun_inj' + · exact corr_inj + + + +abbrev StInv.sim {st : worklist.St A S} (inv : StInv' T st) := + st.m.SimUnpacked M (st.R A S corr) {(q, a, q') | ∃ sa sa', (sa, a, sa') ∈ T ∧ corr sa = q ∧ corr sa' = q' } (inv.fun A S M corr) + +def processOneElem_mot (s : State) (sa : S) (n : ℕ) (st : worklist.St A S) : Prop := + st.map[sa]? = some s ∧ + sa ∈ st.visited ∧ + ∃ (inv : StInv A S M corr st (T := {(sa1, a, sa') | sa1 = sa ∧ ∃ k ≥ n, (f sa)[k]? = some (a, sa') })), + inv.sim A S M corr + +def processOneElem_inv {st : worklist.St A S} (s : State) (sa : S) (k : ℕ) : + ∀ a sa', (f sa)[k]? = some (a, sa') → + processOneElem_mot A S f M corr s sa k st → + StInv' {(sa1, a, sa') | sa1 = sa ∧ ∃ k' ≥ k + 1, (f sa)[k']? = some (a, sa')} (processOneElem A S final s st (a, sa')) := by + rintro a sa' hf ⟨hmap, hvisited, inv, hsim⟩ + have hmem : ∀ s (sa : S), st.map[sa]? = some s → s ∈ st.m.states := by intros; apply inv.map_states; assumption + have _ : st.m.WF := by apply inv.wf + constructor + { simp_all only [processOneElem, worklist.St.addOrCreateState]; aesop } + { simp_all only [processOneElem, worklist.St.addOrCreateState]; split + { aesop } + { dsimp only; intros sa s hin + by_cases hnew? : sa' = sa + { subst_eqs; simp at hin; subst_eqs; aesop } + { have _ : s ∈ st.m.states := by rw [Std.HashMap.getElem?_insert] at hin; aesop + aesop } } } + { simp_all only [processOneElem, worklist.St.addOrCreateState]; split + { simp; intros s hs; apply inv.map_surj ⟨s, hs⟩ } + { simp; intros s' hs' + have hs' : s' ∈ st.m.newState.2.states := by aesop + simp at hs' + rcases hs' with hold | rfl + { obtain ⟨sa, hsa⟩ := inv.map_surj ⟨_, hold⟩; use sa + rw [Std.HashMap.getElem?_insert] + simp_all; rintro rfl; simp_all } + { use sa'; simp_all } } } + { rintro ⟨s', hs'⟩ sa1 sa2 + rw [processOneElem_map] + rw [processOneElem_map] + split <;> split + · rintro heq1 heq2; subst_eqs + have hs'' : s' ∈ st.m.states := by apply hmem s' sa1 (by assumption) + apply inv.map_inj ⟨s', hs''⟩ <;> simp_all + · rintro heq1; split <;> rintro heq2 <;> subst_eqs + exfalso + suffices hccl : st.m.stateMax < st.m.stateMax by aesop + apply st.m.states_lt + exact hmem st.m.stateMax sa1 (by assumption) + · rintro heq1; split <;> rintro heq2 <;> try split at heq2 <;> subst_eqs <;> try rfl + exfalso; subst_eqs + suffices hccl : st.m.stateMax < st.m.stateMax by aesop + apply st.m.states_lt + exact hmem st.m.stateMax sa2 (by assumption) + · simp } + { intros sa' a q' hsa' hq' + rw [processOneElem_visited] at hsa' + obtain ⟨sa', h1, h2⟩ := inv.frontier sa' a q' (by simp_all [worklist.St.visited]) hq' + use sa'; constructor; assumption + rcases h2 with h2 | ⟨rfl, k', hk', h2⟩ + { left; apply processOneElem_preserves_mem; assumption } + by_cases hkeq : k' = k + on_goal 2 => right; dsimp; constructor; rfl; use k'; constructor; omega; assumption + subst_eqs; left + simp only [processOneElem, worklist.St.addOrCreateState] + split; on_goal 2 => simp_all + next _ _ heq => simp_all; rw [h2] at *; casesm* _ ∧ _ ; injections; subst_eqs; aesop } + +set_option debug.skipKernelTC true in -- typechecking gets stuck :( +set_option maxHeartbeats 1000000 in +def processOneElem_spec {st : worklist.St A S} (s : State) (sa : S) (k : ℕ) : + ∀ a sa', (f sa)[k]? = some (a, sa') → + processOneElem_mot A S f M corr s sa k st → + processOneElem_mot A S f M corr s sa (k+1) (processOneElem A S final s st (a, sa')) := by + intro a sa' hf ⟨hmap, hvisited, inv, hsim⟩ + have hmem : ∀ s (sa : S), st.map[sa]? = some s → s ∈ st.m.states := by intros; apply inv.map_states; assumption + -- have hs : s ∈ st.m.states := by apply inv.map_states; assumption + have _ : st.m.WF := by apply inv.wf + have inv' := processOneElem_inv A S final f M corr s sa k a sa' hf ⟨hmap, hvisited, inv, hsim⟩ + have hmfun s' hs hs' : inv.mFun _ _ _ _ ⟨s', hs⟩ = inv'.mFun _ _ _ _ ⟨s', hs'⟩ := by + have h1 := inv.mFun_spec _ _ _ _ ⟨s', hs⟩ + have h2 := inv'.mFun_spec _ _ _ _ ⟨s', hs'⟩ + apply inv'.map_inj ⟨s', hs'⟩ + · apply processOneElem_preserves_map + exact h1 + · apply h2 + have hfun s' hs hs' : inv.fun _ _ _ _ ⟨s', hs⟩ = inv'.fun _ _ _ _ ⟨s', hs'⟩:= by + simp [StInv.fun]; rw [hmfun] + unfold processOneElem_mot + constructor + (rw [processOneElem_preserves_map]; assumption) + constructor + (rw [processOneElem_visited]; exact hvisited) + use inv'; constructor + { exact StInv.fun_inj A S M corr corr_inj inv' } + { exact hsim.reduced } + { rw [processOneElem_finals] + rintro ⟨sa1, hsa1⟩ + rw [processOneElem_states] at hsa1 + split_ifs with hcond + { split_ifs at hsa1; simp_all + simp at hsa1; rcases hsa1 with hsa1 | rfl + · have hneq : sa1 ≠ st.m.stateMax := by rintro rfl; simp_all [CNFA.states] + rw [Std.HashSet.mem_insert]; constructor + · rintro (hc | hfin) + dsimp at hc; exfalso; simp at hneq hc; rw [hc] at hneq; simp at hneq + apply hsim.accept ⟨_, hsa1⟩ |>.mp at hfin + rw [←hfun]; exact hfin + · intros hin; rw [←hfun _ hsa1] at hin; apply hsim.accept _ |>.mpr at hin + right; trivial + · constructor + · intros; rcases hcond with ⟨_, hfinal⟩ + apply final_corr _ |>.mp at hfinal + unfold StInv.fun + convert hfinal + dsimp; congr; symm; apply inv'.mFun_eq; dsimp + have hn : st.map[sa']? = none := by apply Std.HashMap.getElem?_eq_none; assumption + rw [processOneElem_new_map, hn] + · intros _; exact Std.HashSet.mem_insert_self } + { simp at hcond + split_ifs at hsa1 + { rw [hsim.accept ⟨_, hsa1⟩, ←hfun] } + { simp at hsa1; rcases hsa1 with hsa1 | rfl + · rw [hsim.accept ⟨_, hsa1⟩, ←hfun] + · constructor + · simp; intros hc; exfalso; apply inv.wf.finals_lt at hc; simp at hc + · intros hacc; apply final_corr _ |>.mpr at hacc + suffices hc' : final sa' = true by + simp_all + convert hacc + apply inv'.mFun_eq + have hn : st.map[sa']? = none := by apply Std.HashMap.getElem?_eq_none; assumption + rw [processOneElem_new_map, hn]; simp } } } + { rintro ⟨s', hs'⟩; rw [processOneElem_initials]; + rw [processOneElem_states] at hs' + have hin : s' ∈ st.m.newState.2.states := by + split at hs'; exact hs'; simp; left; exact hs' + simp at hin; rcases hin with hin | rfl + · rw [←hfun _ hin]; rw [hsim.initial ⟨s', hin⟩] + · constructor + · intros h; apply inv.wf.initials_lt at h; simp at h + · intros h; obtain ⟨s', hs', hinit⟩ := hsim.initial_all _ h + rw [hfun _ _ (by rw [processOneElem_states]; split <;> simp)] at hs' + apply corr_inj at hs' + convert hinit using 1 + symm; apply inv'.mFun_inj _ _ _ _ _ _ hs' } + { intros q hq; obtain ⟨s', hs', hin⟩ := hsim.initial_all q hq + use ⟨s', by simp [processOneElem_states]; split <;> simp⟩ + rcases s' with ⟨s', hs''⟩ + rw [←hfun _ hs'', processOneElem_initials]; dsimp; simp_all only [ge_iff_le, and_self] } + { + rintro ⟨s', hs'⟩ b q' hq' hR hT + apply processOneElem_mem_states _ _ _ _ a at hs' + rcases hs' with hs' | rfl + on_goal 2 => { + obtain ⟨sa', hvis, hcorr⟩ := hR + simp [processOneElem_visited] at hvis + apply corr_inj at hcorr; subst hcorr + rcases hvis with ⟨hmap, hwl⟩ + obtain hmap' := inv'.mFun_spec _ _ _ _ ⟨_, hs'⟩; dsimp at hmap' + obtain ⟨s'', hs''⟩ := Std.HashMap.mem_iff_getElem?.mp hmap + obtain rfl : s'' = st.m.stateMax := by + apply processOneElem_preserves_map at hs'' + rw [hs''] at hmap' + injection hmap' + apply inv.map_states at hs'' + simp [hs'', CNFA.states] at hs'' + } + obtain hT' | hsame : + (StInv.fun A S M corr inv' ⟨s', _⟩, b, q') ∉ {(q, a, q') | ∃ sa_1 sa', + (sa_1, a, sa') ∈ {(sa1, a, sa') | sa1 = sa ∧ ∃ k_1 ≥ k, (f sa)[k_1]? = some (a, sa')} ∧ corr sa_1 = q ∧ corr sa' = q'} ∨ + (StInv.fun A S M corr inv' ⟨s', _⟩ = corr sa ∧ b = a ∧ corr sa' = q') := by + simp at hT + by_cases hh : StInv.fun A S M corr inv' ⟨s', by assumption⟩ = corr sa ∧ b = a ∧ corr sa' = q' + · right; assumption + · left; simp; rintro s1 s2 rfl k1 hk1 hfk1 hcorr rfl + simp at hh + specialize hh (by symm; apply hcorr) + by_cases heq : k = k1 + · subst heq; apply hh; simp_all; simp_all + · apply hT s1 _ (by simp_all) k1 (by omega) hfk1 hcorr rfl + · -- old + have hR' : StInv.fun A S M corr inv ⟨s', hs'⟩ ∈ worklist.St.R A S corr st := by + obtain ⟨sa', hvis, hcorr⟩ := hR + simp [processOneElem_visited] at hvis + -- apply corr_inj at hcorr; subst hcorr + dsimp [worklist.St.R] + use sa'; constructor; assumption + rw [hcorr]; symm; apply hfun + rw [←hfun] at hT' + obtain ⟨⟨s1, hs1⟩, hcorr', htrans⟩ := hsim.trans_match₁ ⟨_, hs'⟩ b q' (by simp_all) hR' hT' + use ⟨s1, by rw [processOneElem_states]; split <;> simp_all⟩ + constructor + · rw [←hfun]; assumption + · apply processOneElem_trans_preserved; assumption + · -- new + obtain ⟨h1, h2, h3⟩ := hsame + subst_eqs + by_cases heq? : s' = s + · obtain ⟨sa1, hvis, hcorr⟩ := hR + apply corr_inj at hcorr + subst hcorr heq? + rw [h1] at hq' + obtain ⟨sa2, hcorr, hnew?⟩ := inv'.frontier sa a (corr sa') (by rw [processOneElem_visited]; assumption) hq' + apply corr_inj at hcorr; subst hcorr + simp at hT + rcases hnew? with hnew | habs + · obtain ⟨s'', hs''⟩ := Std.HashMap.mem_iff_getElem?.mp hnew + use ⟨s'', by apply inv'.map_states; assumption ⟩ + constructor + · unfold StInv.fun; simp; congr; symm; apply inv'.mFun_eq; exact hs'' + · have h := processOneElem_trans _ _ st final a a sa2 s' s' + simp at h + rcases h with ⟨ssa, h1, h2⟩ + rw [h2] + obtain rfl : ssa = s'' := by simp_all + exact Std.HashSet.mem_insert_self + · simp at habs; obtain ⟨k', hk', hfk'⟩ := habs + exfalso; apply hT sa sa2 rfl k' hk' hfk' (by symm; apply h1) rfl + · have hR' : StInv.fun A S M corr inv ⟨s', hs'⟩ ∈ worklist.St.R A S corr st := by + obtain ⟨sa', hvis, hcorr⟩ := hR + simp [processOneElem_visited] at hvis + -- apply corr_inj at hcorr; subst hcorr + dsimp [worklist.St.R] + use sa'; constructor; assumption + rw [hcorr]; symm; apply hfun + obtain ⟨⟨s1, hs1⟩, hcorr', htrans⟩ := hsim.trans_match₁ ⟨_, hs'⟩ a (corr sa') (by simp_all) hR' (by + rintro hc; simp at hc; obtain ⟨sa1, sa2, ⟨rfl, h1⟩, h2, h3⟩ := hc + apply corr_inj at h3; subst h3 + apply heq? + suffices hccl : st.map[sa1]? = some s' by simp_all + apply corr_inj at h1 + rw [←h1, ←hmfun s' (by assumption), inv.mFun_spec]; rfl + ) + use ⟨s1, by rw [processOneElem_states]; split <;> simp_all⟩ + constructor + · rw [←hfun _ hs1, hcorr'] + · apply processOneElem_trans_preserved; assumption } + { rintro ⟨s', hs'⟩ b s'' hs'' + have h := processOneElem_trans _ _ st final a b sa' s s' + have hs : s ∈ st.m.states := by apply inv.map_states at hmap; assumption + have hin := by apply inv'.wf.trans_tgt_lt'; assumption + use hin + split at h + next heqs => + rcases heqs; subst_eqs + rcases h with ⟨ssa, hmap, htrans⟩ + rw [htrans] at hs'' + simp at hs''; rcases hs'' with rfl | hs'' + · apply hf₂ + have h1 : StInv.mFun A S M corr inv' ⟨ssa, hin⟩ = sa' := by + symm; apply inv'.mFun_eq; simp; exact hmap + have h2 : StInv.mFun A S M corr inv' ⟨s, hs'⟩ = sa := by + symm; apply inv'.mFun_eq; simp; apply processOneElem_preserves_map; assumption + rw [h1, h2] + apply Array.mem_iff_getElem?.mpr; use k + · have hin' := by apply inv.wf.trans_tgt_lt'; assumption + have h := hsim.trans_match₂ ⟨s, hs⟩ a s'' hs'' + simp_all only [ge_iff_le, Prod.mk.eta, exists_const] + next hneq => + + rw [h] at hs'' + have hin' := by apply inv.wf.trans_tgt_lt'; assumption + have hs' : s' ∈ st.m.states := by + simp [CNFA.states]; apply inv.wf.trans_src_lt' _ b + apply Std.HashMap.mem_iff_getElem?.mpr + rw [Std.HashMap.getD_eq_getD_getElem?] at hs'' + by_contra hc + simp at hc + rcases heq : st.m.trans[(s', b)]? + · rw [heq] at hs''; simp at hs'' + · apply hc at heq; contradiction + have h := hsim.trans_match₂ ⟨s', hs'⟩ b s'' hs'' + simp_all } + +-- TODO: improve this proof, make it faster +def worklistGo_spec {st : worklist.St A S} (inv : StInv' ∅ st) : + inv.sim A S M corr → + (worklistRun'.go A S final f st |>.Sim M) := by + induction st using worklistRun'.go.induct _ _ final f with + | case4 st hnemp sa? hsa? => -- trivial case that's impossible + simp [sa?, Array.back?] at hsa? + have : st.worklist.size = 0 := by omega + simp_all only [Array.isEmpty, decide_true, not_true_eq_false] + | case3 st hnemp sa? sa hsa? wl' st' hc => + have h : sa ∈ st.map := by + apply st.worklist_incl + simp_all [sa?, Array.back?_mem] + apply Std.HashMap.getElem?_eq_some_getD (fallback := 0) at h + simp [st'] at hc + exfalso; apply (hc _); exact h + | case1 st hemp => -- exit case, prove that the invariant + empty worklist implies the postcondition + have : st.worklist = #[] := by + simp only [Array.isEmpty] at hemp; apply Array.eq_empty_of_size_eq_zero; simp_all only [decide_eq_true_eq] + intros hsim; unfold worklistRun'.go; simp_all; apply sim_closed_set _ _ _ _ _ _ (by simp_all) hsim + simp [NFA.closed_set]; constructor + { intros q hq; simp [worklist.St.R] + obtain ⟨s, hmap, _⟩ := hsim.initial_all q hq + use (inv.mFun _ _ _ _ s); constructor + · simp [worklist.St.visited]; constructor + { apply mFun_mem } + { simp_all } + · exact hmap } + intros a q' hq' + simp [NFA.mem_stepSet] at hq'; obtain ⟨q, ⟨sa, ⟨hin, -⟩, rfl⟩, hstep⟩ := hq' + apply inv.frontier at hstep; rcases hstep with ⟨sa, rfl, hsa⟩ + simp_all [worklist.St.R, worklist.St.visited]; use sa + simp_all [worklist.St.visited] + | case2 st hnemp sa? sa heq wl' st1 s hs as st2 _ _ _ _ _ ih => -- inductive case, prove the invariant is maintained + intros hsim; unfold worklistRun'.go; simp_all [sa?] + split + next sa' hsome => + have _ : sa' = sa := by simp_all + subst_eqs + split + next _ s' hmap => + have _ : s' = s := by simp_all + subst_eqs + rw [heq] at hsome; subst_eqs + suffices hccl : processOneElem_mot A S f M corr s sa (f sa).size (Array.foldl (processOneElem A S final s) st1 (f sa)) by + obtain ⟨_, _, inv', hsim'⟩ := hccl + simp at inv' + have hemp : {(sa1, a, sa') | sa1 = sa ∧ ∃ k, (f sa).size ≤ k ∧ (f sa)[k]? = some (a, sa')} = ∅ := by + ext sa'; simp_all; rintro rfl k hge hsome + suffices hccl : (f sa'.1)[k]? = none by simp_all + apply Array.getElem?_size_le; assumption + simp_all only [ge_iff_le, st2] + apply Array.foldl_induction + simp only [st1, wl'] + { unfold processOneElem_mot + have inv' : StInv' {(sa1, a, sa') | sa1 = sa ∧ ∃ k ≥ 0, (f sa)[k]? = some (a, sa')} st1 := by + constructor + { simp [st1]; exact inv.wf } + { simp [st1]; apply inv.map_states } + { simp only [st1]; intros a; obtain ⟨sa, hsa⟩ := inv.map_surj a; use sa } + { simp only [st1]; exact inv.map_inj } + { simp only [st1, wl', worklist.St.visited]; intros sa' a q' hsa' hq' + by_cases h : sa' = sa + { subst h; obtain ⟨sa'', h1, h2⟩ := hf₁ _ _ _ hq' + use sa''; constructor; assumption; right + simp; exact Array.getElem?_of_mem h2 } + { obtain ⟨sa', h1, h2 | himp⟩ := inv.frontier sa' a q' (by + simp [worklist.St.visited]; simp_all + intros hc; apply hsa'.2; rw [Array.mem_pop_iff] at hc; simp_all) hq' + on_goal 2 => simp_all + use sa'; simp_all } } + constructor; on_goal 1 => assumption + have hmfun : inv.mFun _ _ _ _ = inv'.mFun _ _ _ _ := by simp [StInv.mFun] + have hfun : inv.fun _ _ _ _ = inv'.fun _ _ _ _ := by simp [StInv.fun, hmfun] + constructor + { simp [worklist.St.visited]; simp_all; exact Std.HashMap.mem_of_get? hmap } + use inv'; constructor + { exact hsim.injective } + { apply hsim.reduced } + { apply hsim.accept } + { apply hsim.initial } + { apply hsim.initial_all } + { rintro ⟨s1, hs1⟩ a q' hq' hin hnin + let sa1 := inv'.mFun _ _ _ _ ⟨s1, hs1⟩ + by_cases hnew? : sa1 = sa + { exfalso; apply hnin + apply hf₁ at hq'; obtain ⟨sa', hcorr, hf⟩ := hq' + use sa, sa' + split_ands + · rfl + · obtain ⟨k, hk⟩ := Array.getElem?_of_mem hf + use k + rw [←hnew?] + simp [hnew?, sa1] at hk ⊢; assumption + · congr; nth_rw 1 [←hnew?] + · assumption } + { rw [←hfun] at *; apply hsim.trans_match₁ <;> try (simp_all; done) + simp_all only [worklist.St.R, worklist.St.visited] + obtain ⟨sa2, ⟨h2, h3⟩, h4⟩ := hin + have heq : sa1 = sa2 := by apply corr_inj; rw [h4]; unfold sa1; rw [←hmfun]; unfold StInv.fun; simp -- TODO + use sa1; simp_all; intros hc + have heq : sa1 = sa := by apply Array.mem_pop_iff _ _ |>.mp at hc; simp_all + simp_all}} + { apply hsim.trans_match₂ } } + { intros k st; apply processOneElem_spec A S final f M corr (st := st) corr_inj final_corr hf₂ s sa k + simp; exact Array.getElem?_lt (f sa) k.isLt } + next hnone => + have hnin : sa ∉ st.map := by + intros hin + suffices ex : ∃ s, st.map[sa]? = some s by simp_all + simp_all + exfalso; apply hnin; apply st.worklist_incl; exact Array.back_mem st.worklist sa hsome + next hnone => + simp [Array.back?] at * + have : st.worklist.size = 0 := by omega + simp_all + +def worklistRun'_spec : (worklistRun' A S final inits hinits f |>.Sim M) := by + unfold worklistRun' + simp + have hh : StInv' ∅ (worklist.initState A S inits hinits final) := by + sorry + apply worklistGo_spec <;> try assumption + sorry + end worklist +section worklist_good + +variable (S : Type) [Fintype S] [BEq S] [LawfulBEq S] [Hashable S] [DecidableEq S] +variable (final : S → Bool) (f : S → Array (BitVec n × S)) (inits : Array S) +variable (M : GoodNFA n) +variable (corr : S → M.σ) +variable (corr_inj : Function.Injective corr) +variable (final_corr : ∀ (s : S), final s ↔ corr s ∈ M.M.accept) +variable (hinit₁ : ∀ sa ∈ inits, corr sa ∈ M.M.start) +variable (hinit₂ : ∀ q ∈ M.M.start, ∃ sa, corr sa = q ∧ sa ∈ inits) +variable (hf₁: ∀ sa q' a, q' ∈ M.M.step (corr sa) a → ∃ sa', corr sa' = q' ∧ (a, sa') ∈ f sa) +variable (hf₂: ∀ sa a sa', (a, sa') ∈ f sa → corr sa' ∈ M.M.step (corr sa) a) + +def worklistRun_spec : (worklistRun S final inits hinits f |>.Sim M) := + worklistRun'_spec (BitVec n) S final f inits M.M corr corr_inj final_corr hf₁ hf₂ + +end worklist_good + /- TODOs and NOTES TODOs: diff --git a/SSA/Experimental/Bits/AutoStructs/Constructions.lean b/SSA/Experimental/Bits/AutoStructs/Constructions.lean index 9c09f44d2..8518e3708 100644 --- a/SSA/Experimental/Bits/AutoStructs/Constructions.lean +++ b/SSA/Experimental/Bits/AutoStructs/Constructions.lean @@ -1,100 +1,137 @@ import Std.Data.HashSet import Std.Data.HashMap import Mathlib.Data.FinEnum +import Mathlib.Data.Fintype.Prod +import Mathlib.Data.Finset.Powerset import SSA.Experimental.Bits.AutoStructs.Basic import SSA.Experimental.Bits.AutoStructs.ForLean import SSA.Experimental.Bits.AutoStructs.FinEnum -import Batteries.Data.Fin.Basic +import SSA.Experimental.Bits.AutoStructs.GoodNFA section sink variable {A : Type} [BEq A] [Hashable A] [DecidableEq A] [FinEnum A] -def NFA.addSink (m : NFA A) : NFA A := - let (sink, m) := m.newState - -- let m := m.addInitial sink -- TODO(leo) is that right? - (List.range m.stateMax).foldl (init := m) fun m s => - (FinEnum.toList (α := A)).foldl (init := m) fun m a => - let stuck := if let some trans := m.trans.get? (s, a) then trans.isEmpty else true - if stuck then m.addTrans a s sink else m -def NFA.flipFinals (m : NFA A) : NFA A := +def CNFA.addSink (m : CNFA A) : CNFA A := m.createSink.2 +-- def CNFA.addSink (m : CNFA A) : CNFA A := + -- let res := (List.range m.stateMax).foldl (init := (none, m)) fun (sink?, m) s => + -- (FinEnum.toList (α := A)).foldl (init := (sink?, m)) fun (sink?, m) a => + -- let stuck := if let some trans := m.trans.get? (s, a) then trans.isEmpty else true + -- if !stuck then (sink?, m) else + -- let (sink, m) := match sink? with + -- | some s => (s, m) + -- | none => m.createSink + -- (some sink, m.addTrans a s sink) + -- res.2 + +def GoodCNFA.addSink (m : GoodCNFA n) : GoodCNFA n := ⟨m.m.addSink, sorry⟩ + +lemma addSink_spec (m : GoodCNFA n) (M : GoodNFA n) : + m.Sim M → + m.addSink.Sim M.complete := + sorry + +def CNFA.flipFinals (m : CNFA A) : CNFA A := let oldFinals := m.finals let newFinals := (List.range m.stateMax).foldl (init := ∅) fun fins s => if oldFinals.contains s then fins else fins.insert s { m with finals := newFinals } +def GoodCNFA.flipFinals (m : GoodCNFA n) : GoodCNFA n := ⟨m.m.flipFinals, by sorry⟩ + end sink section product -variable {A : Type} [BEq A] [Hashable A] [DecidableEq A] [FinEnum A] - -private structure product.State where - m : NFA A - map : Std.HashMap (_root_.State × _root_.State) _root_.State := ∅ - worklist : Array (_root_.State × _root_.State) := ∅ - -private def product.State.measure (st : product.State (A := A)) (m1 m2 : NFA A) := - ((Multiset.range m1.stateMax).product (Multiset.range m2.stateMax)).sub - ((Multiset.ofList st.map.keys).sub (Multiset.ofList st.worklist.toList)) - -def product (final? : Bool → Bool → Bool) (m1 m2 : NFA A) : NFA A := - let map : Std.HashMap (State × State) State := ∅ - let worklist : Array (State × State) := ∅ - let st : product.State (A := A) := { m := NFA.empty } - let st := init st - go st -where init (st : product.State (A := A)) : product.State (A := A) := - m1.initials.fold (init := st) fun st s1 => - m2.initials.fold (init := st) fun st s2 => - let (s, m) := st.m.newState - let m := m.addInitial s - let map := st.map.insert (s1, s2) s - let worklist := st.worklist.push (s1, s2) - {m, map, worklist} - go (st0 : product.State (A := A)) : NFA A := Id.run do - if hne : st0.worklist.size == 0 then - return st0.m - else - let some (s1, s2) := st0.worklist.get? (st0.worklist.size - 1) | return st0.m - let st := { st0 with worklist := st0.worklist.pop } - let some s := st.map.get? (s1, s2) | return NFA.empty - let st := if final? (m1.finals.contains s1) (m2.finals.contains s2) then - { st with m := st.m.addFinal s } - else - st - let st := (FinEnum.toList (α := A)).foldl (init := st) fun st a => - if let some s1trans := m1.trans.get? (s1, a) then - if let some s2trans := m2.trans.get? (s2, a) then - s1trans.fold (init := st) fun st s1' => - s2trans.fold (init := st) fun st s2' => - if let some s' := st.map.get? (s1', s2') then - let m := st.m.addTrans a s s' - { st with m } - else - let (s', m) := st.m.newState - let worklist := st.worklist.push (s1', s2') - let map := st.map.insert (s1', s2') s' - let m := m.addTrans a s s' - { m, map, worklist } - else - st - else - st - go st - termination_by st0.measure m1 m2 - decreasing_by { - sorry - } - - - -def NFA.inter (m1 m2 : NFA A) : NFA A := product (fun b1 b2 => b1 && b2) m1 m2 -def NFA.union (m1 m2 : NFA A) : NFA A := +variable {A : Type} [BEq A] [LawfulBEq A] [Hashable A] [DecidableEq A] [FinEnum A] + +omit [LawfulBEq A] in +lemma CNFA.WF.intitials_states (m : CNFA A) (hwf : m.WF) : ∀ s ∈ m.initials, s ∈ m.states := by + simp_all [CNFA.states, hwf] + +def product (final? : Bool → Bool → Bool) (m1 m2 : GoodCNFA n) : GoodCNFA n := + worklistRun (m1.m.states × m2.m.states) final inits (by sorry /- looks annoying -/) f +where final (ss : m1.m.states × m2.m.states) := final? (m1.m.finals.contains ss.1) (m2.m.finals.contains ss.2) + inits := + let a := Array.mkEmpty <| m1.m.initials.size * m2.m.initials.size + m1.m.initials.attachWith _ m1.wf.intitials_states |>.fold (init := a) fun is s1 => + m2.m.initials.attachWith _ m2.wf.intitials_states |>.fold (init := is) fun is s2 => + is.push (s1, s2) + f (ss : m1.m.states × m2.m.states) := + let (s1, s2) := ss + (FinEnum.toList (α := BitVec n)).foldl (init := Array.empty) fun as a => + let s1trans := m1.m.trans.getD (s1, a) ∅ + let s2trans := m2.m.trans.getD (s2, a) ∅ + s1trans.attachWith _ (m1.wf.trans_tgt_lt' s1 a) |>.fold (init := as) fun as s1' => + s2trans.attachWith _ (m2.wf.trans_tgt_lt' s2 a) |>.fold (init := as) fun as s2' => + as.push (a, (s1', s2')) + + +def GoodCNFA.inter (m1 m2 : GoodCNFA n) : GoodCNFA n := product (fun b1 b2 => b1 && b2) m1 m2 +def GoodCNFA.union (m1 m2 : GoodCNFA n) : GoodCNFA n := -- FIXME add a sink state to each automata, or modify product product (fun b1 b2 => b1 || b2) m1.addSink m2.addSink +noncomputable def to_prop (f : Bool → Bool → Bool) (p1 p2 : Prop) : Prop := + f (@Decidable.decide p1 (Classical.propDecidable _)) (@Decidable.decide p2 (Classical.propDecidable _)) + +def GoodCNFA.product_spec (final? : Bool → Bool → Bool) (m1 m2 : GoodCNFA n) + {M1 : GoodNFA n} {M2 : GoodNFA n} : + m1.Sim M1 → + m2.Sim M2 → + (product final? m1 m2).Sim (GoodNFA.product (to_prop final?) M1 M2) := by + rintro ⟨f1, hsim1⟩ ⟨f2, hsim2⟩ + apply worklistRun_spec (m1.m.states × m2.m.states) + (corr := fun (s1, s2) => (f1 s1, f2 s2)) + · rintro ⟨s1, s2⟩ ⟨s1', s2'⟩; simp; rintro heqs + injection heqs with h1 h2 + apply hsim1.injective at h1; apply hsim2.injective at h2; simp_all + · rintro ⟨s1, s2⟩ + simp [product.final, GoodNFA.product, NFA.product, to_prop, Set.instMembership, Set.Mem]; congr + · rw [←Bool.coe_iff_coe, ←Std.HashSet.mem_iff_contains]; simp; apply hsim1.accept + · rw [←Bool.coe_iff_coe, ←Std.HashSet.mem_iff_contains]; simp; apply hsim2.accept + · rintro ⟨s1, s2⟩ ⟨q1, q2⟩ a hin + simp [NFA.product] at hin + obtain ⟨hst1, hst2⟩ := hin + obtain ⟨s1', hf1, htr1⟩ := hsim1.trans_match₁ s1 a q1 hst1 (by simp) (by simp) + obtain ⟨s2', hf2, htr2⟩ := hsim2.trans_match₁ s2 a q2 hst2 (by simp) (by simp) + use ⟨s1', s2'⟩; simp_all [product.f] + sorry + · rintro ⟨s1, s2⟩ a ⟨s1', s2'⟩ hinf + dsimp only [GoodNFA.product, NFA.product] + simp [to_prop, Set.instMembership, Set.Mem] + suffices h : s1'.val ∈ m1.m.trans.getD (s1, a) ∅ ∧ s2'.val ∈ m2.m.trans.getD (s2, a) ∅ by + rcases h with ⟨h1, h2⟩ + obtain ⟨h1, hin1⟩ := hsim1.trans_match₂ _ _ _ h1 + obtain ⟨h2, hin2⟩ := hsim2.trans_match₂ _ _ _ h2 + aesop + sorry + +def GoodCNFA.inter_spec (m1 m2 : GoodCNFA n) + {M1 : GoodNFA n} {M2 : GoodNFA n} : + m1.Sim M1 → + m2.Sim M2 → + (m1.inter m2).Sim (M1.inter M2) := by + intros h1 h2 + simp [GoodNFA.inter_eq, GoodCNFA.inter] + have heq : And = to_prop (fun x y => x && y) := by + ext x y; simp [to_prop] + simp [heq] + apply product_spec <;> assumption + +def GoodCNFA.union_spec (m1 m2 : GoodCNFA n) + {M1 : GoodNFA n} {M2 : GoodNFA n} : + m1.Sim M1 → + m2.Sim M2 → + (m1.union m2).Sim (M1.union M2) := by + intros h1 h2 + simp [GoodNFA.union_eq, GoodCNFA.union] + have heq : Or = to_prop (fun x y => x || y) := by + ext x y; simp [to_prop] + simp [heq] + apply product_spec <;> apply addSink_spec <;> assumption + end product def HashSet.inter [BEq A] [Hashable A] (m1 m2 : Std.HashSet A) : Std.HashSet A := @@ -108,161 +145,181 @@ def HashSet.areIncluded [BEq A] [Hashable A] (m1 m2 : Std.HashSet A) : Bool := section determinization -variable {A : Type} [BEq A] [Hashable A] [DecidableEq A] [FinEnum A] - -instance hashableHashSet [Hashable A] : Hashable (Std.HashSet A) where - hash s := s.fold (init := 0) fun h x => mixHash h (hash x) - -private structure NFA.determinize.St where - map : Std.HashMap (Std.HashSet State) State - worklist : List (Std.HashSet State) - m : NFA A - -open NFA.determinize in -def NFA.determinize (mi : NFA A) : NFA A := - let m : NFA A := NFA.empty - let (si, m) := m.newState - let m := m.addInitial si - let map : Std.HashMap _ _ := { (mi.initials, si) } - let st : St := { map, worklist := [mi.initials], m} - go st -where go (st : St) : NFA A := Id.run do - if let some (ss, worklist) := st.worklist.next? then - let st := { st with worklist } - let some s := st.map[ss]? | return NFA.empty - let m := if !ss.isDisjoint mi.finals then st.m.addFinal s else st.m - let st := (FinEnum.toList A).foldl (init := { st with m }) fun st a => - let ss' := mi.transSet ss a - let (s', st) := if let some s' := st.map[ss']? then (s', st) else - let (s', m) := st.m.newState - let map := st.map.insert ss' s' - let worklist := ss' :: st.worklist - (s', { map, worklist, m }) - { st with m := st.m.addTrans a s s'} - go st - else - st.m - decreasing_by sorry - -def NFA.neg (m : NFA A) : NFA A := m.determinize.flipFinals +variable {A : Type} [BEq A] [LawfulBEq A] [Hashable A] [DecidableEq A] [FinEnum A] + +-- TODO: I'd rather use hashsets, but I don't think the following holds +-- `Fintype α → Fintype (HashSet α)` + +def BitVec.any (b : BitVec w) (f : Fin w → Bool → Bool) := + List.finRange w |>.any fun n => f n (b[n]) + +def GoodCNFA.determinize (m : GoodCNFA n) : GoodCNFA n := + worklistRun (BitVec m.m.stateMax) + (fun ss => ss.any fun n b => b == true && n ∈ m.m.finals) + #[BitVec.ofFn (fun n => n ∈ m.m.initials)] + (by apply List.nodup_singleton) + fun (ss : BitVec m.m.stateMax) => + (FinEnum.toList (BitVec n)).foldl (init := Array.empty) fun ts a => + let ss' := m.m.transSetBV ss a + ts.push (a, ss') + +def GoodNFA.determinize_spec_nonemp (m : GoodCNFA n) [Nonempty m.m.states] + {M : GoodNFA n} (hsim : m.Sim M) : + m.determinize.Sim M.determinize := by + rcases hsim with ⟨fsim, hsim⟩ + unfold GoodCNFA.determinize + apply worklistRun_spec (BitVec m.m.stateMax) + (corr := λ ss q => let i := Function.invFun fsim q; ss[i.val] == true) + (M := M.determinize) + · intros ss1 ss2; simp; intros heq; ext i + rw [funext_iff] at heq + specialize heq (fsim ⟨i.val, by simp [CNFA.states]⟩) + rw [Function.leftInverse_invFun hsim.injective] at heq + simp at heq; exact heq + · sorry + · sorry + · sorry + +def GoodNFA.determinize_spec_emp (m : GoodCNFA n) (hemp : m.m.stateMax = 0) + {M : GoodNFA n} (hsim : m.Sim M) : + m.determinize.Sim M.determinize := by + rcases hsim with ⟨fsim, hsim⟩ + unfold GoodCNFA.determinize + apply worklistRun_spec (BitVec m.m.stateMax) + (corr := λ ss _ => True) + (M := M.determinize) + · rw [hemp]; intros ss1 ss2 _; apply BitVec.eq_of_getMsbD_eq; simp + · rw [hemp]; rintro ⟨⟨x⟩⟩ + obtain rfl : x = 0 := by omega + simp [BitVec.any, GoodNFA.determinize, NFA.toDFA] + intros q _ ha + sorry -- need to prove that f is surjective? + · sorry + · sorry + +def GoodNFA.determinize_spec (m : GoodCNFA n) + {M : GoodNFA n} (hsim : m.Sim M) : + m.determinize.Sim M.determinize := by + rcases heq : m.m.stateMax + · apply GoodNFA.determinize_spec_emp <;> simp_all + · have _ : Nonempty m.m.states := by use 0; simp_all [CNFA.states] + apply GoodNFA.determinize_spec_nonemp; simp_all + +def GoodCNFA.neg (m : GoodCNFA n) : GoodCNFA n := m.determinize.flipFinals + +def GoodCNFA.neg_spec (m : GoodCNFA n) {M : GoodNFA n} (hsim : m.Sim M) : + m.neg.Sim M.neg := by + sorry end determinization section equality -variable {A : Type} [BEq A] [Hashable A] [DecidableEq A] [FinEnum A] +-- variable {A : Type} [BEq A] [Hashable A] [DecidableEq A] [FinEnum A] + +-- private structure isIncluded.State where +-- visited : List (_root_.State × Std.HashSet _root_.State) := ∅ -- TODO: slow +-- worklist : List (_root_.State × Std.HashSet _root_.State) := ∅ + +-- TODO: this function is not correct yet... it should be a more optimized +-- procedure to check that the languages of two automata are included. +/- Returns true when `L(m1) ⊆ L(m2)` -/ +-- def CNFA.isIncluded (m1 m2 : CNFA A) : Bool := +-- let st := { visited := [], worklist := m1.initials.fold (init := []) fun res s1 => (s1, m2.initials) :: res } +-- go st +-- where go (st : isIncluded.State) : Bool := +-- if let some ((s1, ss1), worklist) := st.worklist.next? then +-- let st := { st with worklist } +-- if m1.initials.contains s1 ∧ ss1.isDisjoint m2.finals then +-- false +-- else +-- let st := { st with visited := (s1, ss1) :: st.visited } +-- let st := (FinEnum.toList (α := A)).foldl (init := st) fun st a => +-- let ss2 := m2.transSet ss1 a +-- (m1.trans.getD (s1, a) ∅).fold (init := st) fun st s2 => +-- if st.worklist.any (fun (s'', ss'') => s'' = s2 && HashSet.areIncluded ss'' ss2) || +-- st.visited.any (fun (s'', ss'') => s'' = s2 && HashSet.areIncluded ss'' ss2) then +-- st +-- else +-- { st with worklist := (s2, ss2)::st.worklist } +-- go st +-- else +-- true +-- decreasing_by sorry + +-- end equality + +section emptiness + +variable {A : Type} [BEq A] [LawfulBEq A] [Hashable A] [DecidableEq A] [FinEnum A] -private structure isIncluded.State where - visited : List (_root_.State × Std.HashSet _root_.State) := ∅ -- TODO: slow - worklist : List (_root_.State × Std.HashSet _root_.State) := ∅ - --- TODO: this function is not correct yet... -/-- Returns true when `L(m1) ⊆ L(m2)` -/ -def NFA.isIncluded (m1 m2 : NFA A) : Bool := - let st := { visited := [], worklist := m1.initials.fold (init := []) fun res s1 => (s1, m2.initials) :: res } - go st -where go (st : isIncluded.State) : Bool := - if let some ((s1, ss1), worklist) := st.worklist.next? then - let st := { st with worklist } - if m1.initials.contains s1 ∧ ss1.isDisjoint m2.finals then - false - else - let st := { st with visited := (s1, ss1) :: st.visited } - let st := (FinEnum.toList (α := A)).foldl (init := st) fun st a => - let ss2 := m2.transSet ss1 a - (m1.trans.getD (s1, a) ∅).fold (init := st) fun st s2 => - if st.worklist.any (fun (s'', ss'') => s'' = s2 && HashSet.areIncluded ss'' ss2) || - st.visited.any (fun (s'', ss'') => s'' = s2 && HashSet.areIncluded ss'' ss2) then - st - else - { st with worklist := (s2, ss2)::st.worklist } - go st - else - true - decreasing_by sorry - -end equality - -section universality +-- TODO: this relies on the fact that all states are reachable! +-- We should add this to the simulation predicate I think +def GoodCNFA.isEmpty (m : GoodCNFA n) : Bool := m.m.finals.isEmpty -variable {A : Type} [BEq A] [Hashable A] [DecidableEq A] [FinEnum A] +def GoodCNFA.isUniversal (m : GoodCNFA n) : Bool := m.neg.isEmpty -private structure isUniversal.State where - visited : Std.HashSet (Std.HashSet _root_.State) := ∅ - worklist : Array (Std.HashSet _root_.State) := ∅ - -/-- Returns true when `L(m) = A*` -/ -def NFA.isUniversal (m : NFA A) : Bool := - let st := { visited := ∅, worklist := Array.singleton m.initials} - go st -where go (st : isUniversal.State) : Bool := - match heq : st.worklist.back? with - | none => true - | some ss => - let worklist := st.worklist.pop - let st := { st with worklist } - if ss.isDisjoint m.finals then - false - else - let st := { st with visited := st.visited.insert ss } - let st := (FinEnum.toList (α := A)).foldl (init := st) fun st a => - let ss' := m.transSet ss a - if st.worklist.any (fun ss'' => HashSet.areIncluded ss'' ss') || - st.visited.any (fun ss'' => HashSet.areIncluded ss'' ss') then - st - else - { st with worklist := st.worklist.push ss' } - go st - decreasing_by sorry +theorem GoodCNFA.isUniversal_spec {m : GoodCNFA n} {M : GoodNFA n} : + m.Sim M → m.isUniversal → M.accepts = ⊤ := by + sorry /-- Recognizes the empty word -/ -def NFA.emptyWord : NFA A := - let m := NFA.empty +def CNFA.emptyWord : CNFA A := + let m := CNFA.empty let (s, m) := m.newState let m := m.addInitial s let m := m.addFinal s m +def GoodCNFA.emptyWord : GoodCNFA n := ⟨CNFA.emptyWord, by sorry⟩ + /-- Returns true when `L(m) ∪ {ε} = A*`. This is useful because the bitvector of with width zero has strange properties. -/ -def NFA.isUniversal' (m : NFA A) : Bool := - m.union NFA.emptyWord |> NFA.isUniversal +def GoodCNFA.isUniversal' (m : GoodCNFA n) : Bool := + m.union GoodCNFA.emptyWord |> GoodCNFA.isUniversal -- TODO: this relies on the fact that all states are reachable! -def NFA.isEmpty (m : NFA A) : Bool := m.finals.isEmpty -def NFA.isNotEmpty (m : NFA A) : Bool := !m.finals.isEmpty +-- should derive from the fact that all states of M are reachable. +def CNFA.isNotEmpty (m : CNFA A) : Bool := !m.finals.isEmpty -end universality - -instance: Hashable (BitVec n) where - hash x := Hashable.hash x.toFin +end emptiness section lift_proj --- Defined as bv'[i] = bv[f i] -def transport (f : Fin n2 → Fin n1) (bv : BitVec n1) : BitVec n2 := - (Fin.list n2).foldl (init := BitVec.zero n2) fun bv' (i : Fin _) => bv' ||| (BitVec.twoPow n2 i * bv[f i].toNat) - variable {n : Nat} -- Morally, n2 >= n1 -def NFA.lift (m1: NFA (BitVec n1)) (f : Fin n1 → Fin n2) : NFA (BitVec n2) := - let m2 : NFA (BitVec n2) := { m1 with trans := Std.HashMap.empty } +def CNFA.lift (m1: CNFA (BitVec n1)) (f : Fin n1 → Fin n2) : CNFA (BitVec n2) := + let m2 : CNFA (BitVec n2) := { m1 with trans := Std.HashMap.empty } (List.range m2.stateMax).foldl (init := m2) fun m2 s => (FinEnum.toList (BitVec n2)).foldl (init := m2) fun m2 (bv : BitVec n2) => - let newtrans := m1.trans.getD (s, transport f bv) ∅ + let newtrans := m1.trans.getD (s, bv.transport f) ∅ let oldtrans := m2.trans.getD (s, bv) ∅ let trans := newtrans.union oldtrans if trans.isEmpty then m2 else { m2 with trans := m2.trans.insert (s, bv) trans } +def GoodCNFA.lift (m: GoodCNFA n1) (f : Fin n1 → Fin n2) : GoodCNFA n2 := + ⟨m.m.lift f, by sorry⟩ + +def GoodCNFA.lift_spec (m : GoodCNFA n1) (f : Fin n1 → Fin n2) {M : GoodNFA n1} : + m.Sim M → (m.lift f |>.Sim (M.lift f)) := by + sorry + -- Morally, n1 >= n2 -def NFA.proj (m1: NFA (BitVec n1)) (f : Fin n2 → Fin n1) : NFA (BitVec n2) := - let m2 : NFA (BitVec n2) := { m1 with trans := Std.HashMap.empty } +def CNFA.proj (m1: CNFA (BitVec n1)) (f : Fin n2 → Fin n1) : CNFA (BitVec n2) := + let m2 : CNFA (BitVec n2) := { m1 with trans := Std.HashMap.empty } m1.trans.keys.foldl (init := m2) fun m2 (s, bv) => let trans := m1.trans.getD (s, bv) ∅ - let bv' := transport f bv + let bv' := bv.transport f let oldtrans := m2.trans.getD (s, bv') ∅ { m2 with trans := m2.trans.insert (s, bv') (trans.union oldtrans) } +def GoodCNFA.proj (m: GoodCNFA n2) (f : Fin n1 → Fin n2) : GoodCNFA n1 := + ⟨m.m.proj f, by sorry⟩ + +def GoodCNFA.proj_spec (m : GoodCNFA n2) (f : Fin n1 → Fin n2) {M : GoodNFA n2} : + m.Sim M → (m.proj f |>.Sim (M.proj f)) := by + sorry + end lift_proj diff --git a/SSA/Experimental/Bits/AutoStructs/Defs.lean b/SSA/Experimental/Bits/AutoStructs/Defs.lean index d98c1cc0f..a295f1b03 100644 --- a/SSA/Experimental/Bits/AutoStructs/Defs.lean +++ b/SSA/Experimental/Bits/AutoStructs/Defs.lean @@ -3,11 +3,29 @@ Released under Apache 2.0 license as described in the file LICENSE. -/ import Mathlib.Data.Bool.Basic import Mathlib.Data.Fin.Basic +import Mathlib.Tactic import SSA.Projects.InstCombine.ForLean import SSA.Experimental.Bits.Fast.BitStream +import SSA.Experimental.Bits.AutoStructs.ForMathlib namespace AutoStructs +-- A bunch of maps from `Fin n` to `Fin m` that we use to +-- lift and project variables when we interpret formulas +def liftMaxSucc1 (n m : Nat) : Fin (n + 1) → Fin (max n m + 2) := + fun k => if _ : k = n then Fin.last (max n m) else k.castLE (by omega) +def liftMaxSucc2 (n m : Nat) : Fin (m + 1) → Fin (max n m + 2) := + fun k => if _ : k = m then Fin.last (max n m + 1) else k.castLE (by omega) +def liftLast2 n : Fin 2 → Fin (n + 2) +| 0 => n +| 1 => Fin.last (n + 1) +def liftExcept2 n : Fin n → Fin (n + 2) := + fun k => Fin.castLE (by omega) k +def liftMax1 (n m : Nat) : Fin n → Fin (max n m) := + fun k => k.castLE (by omega) +def liftMax2 (n m : Nat) : Fin m → Fin (max n m) := + fun k => k.castLE (by omega) + /-! # Term Language This file defines the term language the decision procedure operates on, @@ -39,10 +57,6 @@ inductive Term : Type | sub : Term → Term → Term /-- Negation -/ | neg : Term → Term -/-- Increment (i.e., add one) -/ -| incr : Term → Term -/-- Decrement (i.e., subtract one) -/ -| decr : Term → Term deriving Repr -- /-- `repeatBit` is an operation that will repeat the infinitely repeat the -- least significant `true` bit of the input. @@ -81,8 +95,6 @@ a term like `var 10` only has a single free variable, but its arity will be `11` | add t₁ t₂ => max (arity t₁) (arity t₂) | sub t₁ t₂ => max (arity t₁) (arity t₂) | neg t => arity t -| incr t => arity t -| decr t => arity t -- | repeatBit t => arity t @@ -122,13 +134,19 @@ and only require that many bitstream values to be given in `vars`. let x₂ := t₂.evalFin (fun i => vars (Fin.castLE (by simp [arity]) i)) x₁ - x₂ | neg t => -(Term.evalFin t vars) - | incr t => Term.evalFin t vars + 1 - | decr t => Term.evalFin t vars - 1 -- | repeatBit t => BitStream.repeatBit (Term.evalFin t vars) +lemma evalFin_eq {t : Term} {vars1 : Fin t.arity → BitVec w1} {vars2 : Fin t.arity → BitVec w2} : + ∀ (heq : w1 = w2), + (∀ n, vars1 n = heq ▸ vars2 n) → + t.evalFin vars1 = heq ▸ t.evalFin vars2 := by + rintro rfl heqs + simp only + congr; ext1; simp_all + @[simp] def Term.evalNat (t : Term) (vars : Nat → BitVec w) : BitVec w := match t with - | var n => vars (Fin.last n) + | var n => vars n | zero => BitVec.zero w | one => 1 | negOne => -1 @@ -155,8 +173,6 @@ and only require that many bitstream values to be given in `vars`. let x₂ := t₂.evalNat vars x₁ - x₂ | neg t => -(Term.evalNat t vars) - | incr t => Term.evalNat t vars + 1 - | decr t => Term.evalNat t vars - 1 -- | repeatBit t => BitStream.repeatBit (Term.evalFin t vars) @[simp] def Term.evalFinStream (t : Term) (vars : Fin (arity t) → BitStream) : BitStream := match t with @@ -186,8 +202,9 @@ and only require that many bitstream values to be given in `vars`. let x₂ := t₂.evalFinStream (fun i => vars (Fin.castLE (by simp [arity]) i)) x₁ - x₂ | neg t => -(Term.evalFinStream t vars) - | incr t => BitStream.incr (Term.evalFinStream t vars) - | decr t => BitStream.decr (Term.evalFinStream t vars) + +def Term.language (t : Term) : Set (BitVecs (t.arity + 1)) := + { bvs : BitVecs (t.arity + 1) | t.evalFin (fun n => bvs.bvs.get n) = bvs.bvs.get t.arity } inductive RelationOrdering | lt | le | gt | ge @@ -199,8 +216,7 @@ inductive Relation | unsigned (ord : RelationOrdering) deriving Repr -@[simp] -def evalRelation {w} (rel : Relation) (bv1 bv2 : BitVec w) : Bool := +def evalRelation (rel : Relation) {w} (bv1 bv2 : BitVec w) : Bool := match rel with | .eq => bv1 = bv2 | .signed .lt => bv1 <ₛ bv2 @@ -212,11 +228,19 @@ def evalRelation {w} (rel : Relation) (bv1 bv2 : BitVec w) : Bool := | .unsigned .gt => bv1 >ᵤ bv2 | .unsigned .ge => bv1 ≥ᵤ bv2 +@[simp] +lemma evalRelation_coe (rel : Relation) (bv1 bv2 : BitVec w1) (heq : w1 = w2) : + evalRelation rel (heq ▸ bv1) (heq ▸ bv2) = evalRelation rel bv1 bv2 := by + rcases heq; simp + +@[simp] +def Relation.language (rel : Relation) : Set (BitVecs 2) := + { bvs | evalRelation rel (bvs.bvs.get 0) (bvs.bvs.get 1) } + inductive Binop | and | or | impl | equiv deriving Repr -@[simp] def evalBinop (op : Binop) (b1 b2 : Bool) : Bool := match op with | .and => b1 && b2 @@ -231,6 +255,14 @@ def evalBinop' (op : Binop) (b1 b2 : Prop) : Prop := | .or => b1 ∨ b2 | .impl => b1 → b2 | .equiv => b1 ↔ b2 + +def langBinop (op : Binop) (l1 l2 : Set (BitVecs n)) : Set (BitVecs n) := + match op with + | .and => l1 ∩ l2 + | .or => l1 ∪ l2 + | .impl => l1ᶜ ∪ l2 + | .equiv => (l1ᶜ ∪ l2) ∩ (l2ᶜ ∪ l1) + inductive Unop | neg deriving Repr @@ -265,6 +297,206 @@ def Formula.sat {w : Nat} (φ : Formula) (ρ : Fin φ.arity → BitVec w) : Bool evalBinop op b1 b2 | .msbSet t => (t.evalFin ρ).msb +@[simp] +def _root_.Set.lift (f : Fin n → Fin m) (bvs : Set (BitVecs n)) : Set (BitVecs m) := + BitVecs.transport f ⁻¹' bvs + +@[simp] +def _root_.Set.proj (f : Fin n → Fin m) (bvs : Set (BitVecs m)) : Set (BitVecs n) := + BitVecs.transport f '' bvs + +@[simp] +def langMsb : Set (BitVecs 1) := { bvs | bvs.bvs.get 0 |>.msb } + +@[simp] +def Formula.language (φ : Formula) : Set (BitVecs φ.arity) := + match φ with + | .atom rel t1 t2 => + let l1 := t1.language.lift (liftMaxSucc1 (FinEnum.card $ Fin t1.arity) (FinEnum.card $ Fin t2.arity)) + let l2 := t2.language.lift (liftMaxSucc2 (FinEnum.card $ Fin t1.arity) (FinEnum.card $ Fin t2.arity)) + let lrel := rel.language.lift $ liftLast2 (max (FinEnum.card (Fin t1.arity)) (FinEnum.card (Fin t2.arity))) + let l := lrel ∩ l1 ∩ l2 + l.proj (liftExcept2 _) + | .unop .neg φ => φ.languageᶜ + | .binop op φ1 φ2 => + let l1 := φ1.language.lift $ liftMax1 φ1.arity φ2.arity + let l2 := φ2.language.lift $ liftMax2 φ1.arity φ2.arity + langBinop op l1 l2 + | .msbSet t => + let lmsb := langMsb.lift $ fun _ => Fin.last t.arity + let l' := t.language ∩ lmsb + l'.proj fun n => n.castLE (by simp [Formula.arity, FinEnum.card]) + +lemma helper1 : (k = 0) → (x ::ᵥ vs).get k = x := by rintro rfl; simp +lemma helper2 : (k = 1) → (x ::ᵥ y ::ᵥ vs).get k = y := by rintro rfl; simp [Mathlib.Vector.get] +lemma msb_coe {x : BitVec w1} (heq : w1 = w2) : x.msb = (heq ▸ x).msb := by rcases heq; simp + +lemma formula_language_case_atom : + let φ := Formula.atom rel t1 t2 + φ.language = λ (bvs : BitVecs φ.arity) => (φ.sat (fun k => bvs.bvs.get k) = true) := by + unfold Formula.language + rintro φ + let n := φ.arity + unfold φ + dsimp (config := { zeta := false }) + lift_lets + intros l1 l2 lrel l + ext bvs + constructor + · intros h; simp at h + obtain ⟨bvsb, h, heqb⟩ := h + unfold l at h + simp at h + unfold lrel l1 l2 at h + obtain ⟨⟨hrel, h1⟩, h2⟩ := h + have _ : n+1 < bvsb.bvs.length := by simp_all [n] + have _ : n < bvsb.bvs.length := by simp_all [n] + have hrel : evalRelation rel (bvsb.bvs.get n) (bvsb.bvs.get (Fin.last (n + 1))) := by + simp at hrel + apply hrel + have ht1 : bvsb.bvs.get n = t1.evalFin fun n => bvsb.bvs.get n := by + unfold Term.language at h1 + simp [Mathlib.Vector.transport, liftMaxSucc1] at h1 + unfold n; simp; rw [←h1] + congr; ext1 k + split_ifs with h + · exfalso + have _ : k < t1.arity := by simp + have _ : k = t1.arity := by rcases k with ⟨k, hk⟩; simp_all [Fin.last] + omega + · congr; ext; simp; rw [Nat.mod_eq_of_lt]; omega + have ht2 : bvsb.bvs.get (Fin.last (n+1)) = t2.evalFin fun n => bvsb.bvs.get n := by + unfold Term.language at h2 + simp [Mathlib.Vector.transport, liftMaxSucc2] at h2 + unfold n; simp only [Formula.arity, Fin.natCast_self]; rw [←h2] + congr; ext1 k + split_ifs with h + · exfalso + have _ : k < t2.arity := by simp + have _ : k = t2.arity := by rcases k with ⟨k, hk⟩; simp_all [Fin.last] + omega + · congr; ext; simp; rw [Nat.mod_eq_of_lt]; omega + have hw : bvsb.w = bvs.w := by rw [←heqb]; simp + have heq1 : (t1.evalFin fun n => bvsb.bvs.get n) = + hw ▸ t1.evalFin fun n => bvs.bvs.get $ n.castLE (by simp) := by + apply evalFin_eq hw; intros k + rcases bvs with ⟨w, bvs⟩; rcases hw + injection heqb with _ heqb; rw [←heqb] + simp [Mathlib.Vector.transport, liftExcept2] + congr; ext; simp; omega + have heq2 : (t2.evalFin fun n => bvsb.bvs.get n) = + hw ▸ t2.evalFin fun n => bvs.bvs.get $ n.castLE (by simp) := by + apply evalFin_eq hw; intros k + rcases bvs with ⟨w, bvs⟩; rcases hw + injection heqb with _ heqb; rw [←heqb] + simp [Mathlib.Vector.transport, liftExcept2] + congr; ext; simp; omega + rw [ht1, ht2, heq1, heq2, evalRelation_coe] at hrel + dsimp only [Set.instMembership, Set.Mem] + simp_all + · intros h + simp + let bv1 := t1.evalFin fun k => bvs.bvs.get $ k.castLE (by simp) + let bv2 := t2.evalFin fun k => bvs.bvs.get $ k.castLE (by simp) + use ⟨bvs.w, bvs.bvs.append $ bv1 ::ᵥ bv2 ::ᵥ Mathlib.Vector.nil⟩ + rcases bvs with ⟨w, bvs⟩ + simp + constructor + · unfold l; simp; split_ands + · unfold lrel; simp only [Fin.isValue, BitVecs.transport_getElem, + liftLast2, Set.mem_setOf_eq, Fin.val_last, le_add_iff_nonneg_right, zero_le, + Mathlib.Vector.append_get_ge] + rw [Mathlib.Vector.append_get_ge (by dsimp; rw [Nat.mod_eq_of_lt]; omega)] + simp [Set.instMembership, Set.Mem] at h + convert h using 2 + · apply helper1; ext; simp; rw [Nat.mod_eq_of_lt] <;> omega + · apply helper2; ext; simp + · unfold l1 Term.language; simp [Mathlib.Vector.transport, liftMaxSucc1] + rw [Mathlib.Vector.append_get_ge (by dsimp; rw [Nat.mod_eq_of_lt]; omega)] + rw [helper1 (by ext; simp; rw [Nat.mod_eq_of_lt] <;> omega)] + unfold bv1 + congr; ext1 k; split_ifs + · exfalso + have _ : k < t1.arity := by simp + have _ : k = t1.arity := by rcases k with ⟨k, hk⟩; simp_all [Fin.last] + omega + · simp; congr 1 + · unfold l2 Term.language; simp [Mathlib.Vector.transport, liftMaxSucc2] + rw [helper2 (by ext; simp)] + unfold bv2 + congr; ext1 k; split_ifs + · exfalso + have _ : k < t2.arity := by simp + have _ : k = t2.arity := by rcases k with ⟨k, hk⟩; simp_all [Fin.last] + omega + · simp; congr 1 + · ext1; simp + next i => + simp [Mathlib.Vector.transport, liftExcept2] + rw [Mathlib.Vector.append_get_lt i.isLt] + congr 1 + +theorem formula_language (φ : Formula) : + φ.language = { (bvs : BitVecs φ.arity) | φ.sat (fun k => bvs.bvs.get k) = true } := by + let n : Nat := φ.arity + induction φ + case atom rel t1 t2 => + apply formula_language_case_atom + case unop op φ ih => + rcases op; simp [ih, Set.compl_def] + case binop op φ1 φ2 ih1 ih2 => + unfold Formula.language + ext1 bvs + simp [ih1, ih2] + have heq1 : (φ1.sat fun k => bvs.bvs.get (liftMax1 φ1.arity φ2.arity k)) = true ↔ + (φ1.sat fun n => bvs.bvs.get (Fin.castLE (by simp) n)) = true := by + simp; congr + have heq2 : (φ2.sat fun k => bvs.bvs.get (liftMax2 φ1.arity φ2.arity k)) = true ↔ + (φ2.sat fun n => bvs.bvs.get (Fin.castLE (by simp) n)) = true := by + simp; congr + rcases op <;> + simp [evalBinop, langBinop, Set.compl, Set.instMembership, + Set.Mem, Mathlib.Vector.transport] <;> aesop + case msbSet t => + ext1 bvs; simp only [Formula.arity, Formula.language, Set.proj, Set.lift, langMsb, Fin.isValue, + Set.preimage_setOf_eq, Set.mem_image, Set.mem_inter_iff, + Set.mem_setOf_eq, Formula.sat] + rcases bvs with ⟨w, bvs⟩ + constructor + · rintro ⟨bvsb, ⟨ht, hmsb⟩, heq⟩ + simp only [Fin.isValue, Formula.arity] at ht hmsb ⊢ + unfold Term.language at ht + simp only [BitVecs.transport, Mathlib.Vector.transport] at hmsb + simp at ht; rw [←ht] at hmsb; rw [←hmsb] + simp [BitVecs.transport] at heq + obtain ⟨hw, hbvs⟩ := heq + simp [hw]; congr 1; simp [hw] + rcases hw; simp + congr 1; ext1 k + simp at hbvs; simp [←hbvs, Mathlib.Vector.transport]; congr + · intros heq + use ⟨w, + bvs.append ((t.evalFin fun k => bvs.get $ k.castLE (by simp)) ::ᵥ Mathlib.Vector.nil)⟩ + unfold Term.language + simp [BitVecs.transport, Mathlib.Vector.transport] at heq ⊢ + constructor; assumption + ext1 k; simp; congr 1 + +/-- +The formula `φ` is true for evey valuation. +-/ +@[simp] +def Formula.Tautology (φ : Formula) := φ.language = ⊤ + +/-- +The formula `φ` is true for evey valuation made up of non-empty bitvectors. +-/ +@[simp] +def Formula.Tautology' (φ : Formula) := φ.language ∪ BitVecs0 = ⊤ + +/-- +Same as `Formula.sat` but the environment is indexed by unbounded natural number. +-/ @[simp] def Formula.sat' {w : Nat} (φ : Formula) (ρ : Nat → BitVec w) : Prop := match φ with @@ -279,6 +511,29 @@ def Formula.sat' {w : Nat} (φ : Formula) (ρ : Nat → BitVec w) : Prop := evalBinop' op b1 b2 | .msbSet t => (t.evalNat ρ).msb +lemma evalFin_evalNat (t : Term): + t.evalFin (fun k => ρ k.val) = t.evalNat ρ := by + induction t <;> simp_all + +lemma sat_impl_sat' {φ : Formula} : + (φ.sat fun k => ρ k.val) ↔ φ.sat' ρ := by + induction φ + case atom rel t1 t2 => + simp [←evalFin_evalNat] + case binop op φ1 φ2 ih1 ih2 => + simp [evalBinop, ←ih1, ←ih2] + rcases op <;> simp + rw [←Bool.eq_false_eq_not_eq_true] + tauto + case unop op φ ih => rcases op; simp [←ih] + case msbSet t => + simp [←evalFin_evalNat] + +lemma env_to_bvs (φ : Formula) (ρ : Fin φ.arity → BitVec w) : + let bvs : BitVecs φ.arity := ⟨w, Mathlib.Vector.ofFn fun k => ρ k⟩ + ρ = fun k => bvs.bvs.get k := by + simp + @[simp] abbrev envOfArray {w} (a : Array (BitVec w)) : Nat → BitVec w := fun n => a.getD n 0 diff --git a/SSA/Experimental/Bits/AutoStructs/FiniteStateMachine.lean b/SSA/Experimental/Bits/AutoStructs/FiniteStateMachine.lean index f5892d4f7..39b9883a8 100644 --- a/SSA/Experimental/Bits/AutoStructs/FiniteStateMachine.lean +++ b/SSA/Experimental/Bits/AutoStructs/FiniteStateMachine.lean @@ -46,7 +46,7 @@ attribute [instance] FSM.i FSM.dec_eq namespace FSM -variable {arity : Type} (p : FSM arity) +variable {ar : Type} (p : FSM ar) /-- The state of FSM `p` is given by a function from `p.α` to `Bool`. @@ -56,7 +56,7 @@ abbrev State : Type := p.α → Bool /-- `p.nextBit state in` computes both the next state bits and the output bit, where `state` are the *current* state bits, and `in` are the current input bits. -/ -def nextBit : p.State → (arity → Bool) → p.State × Bool := +def nextBit : p.State → (ar → Bool) → p.State × Bool := fun carry inputBits => let input := Sum.elim carry inputBits let newState : p.State := fun (a : p.α) => (p.nextBitCirc (some a)).eval input @@ -64,16 +64,41 @@ def nextBit : p.State → (arity → Bool) → p.State × Bool := (newState, outBit) /-- `p.carry in i` computes the internal carry state at step `i`, given input *streams* `in` -/ -def carry (x : arity → BitStream) : ℕ → p.State +def carry (x : ar → BitStream) : ℕ → p.State | 0 => p.initCarry | n+1 => (p.nextBit (carry x n) (fun i => x i n)).1 +lemma carry_eq_up_to : + (∀ ar k, k < n → x ar k = y ar k) → + p.carry x n = p.carry y n := by + induction n generalizing x y + case zero => intros; rfl + case succ n ih => + rintro heq + simp [carry, @ih x y (by tauto)] + congr; simp_all only [lt_add_iff_pos_right, zero_lt_one] + +def carryBV (x : ar → BitVec w) : p.State := + p.carry (fun ar => BitStream.ofBitVec (x ar)) w + /-- `eval p` morally gives the function `BitStream → ... → BitStream` represented by FSM `p` -/ -def eval (x : arity → BitStream) : BitStream := +def eval (x : ar → BitStream) : BitStream := fun n => (p.nextBit (p.carry x n) (fun i => x i n)).2 +lemma eval_eq_up_to : + (∀ ar k, k ≤ n → x ar k = y ar k) → + p.eval x n = p.eval y n := by + rintro h + simp [eval] + congr + apply carry_eq_up_to p (by rintro ar k hlt; apply h; omega) + ext; apply h; rfl + +def evalBV {w} (x : ar → BitVec w) : BitVec w := + BitVec.ofFn fun k => p.eval (fun ar => BitStream.ofBitVec (x ar)) k + /-- `eval'` is an alternative definition of `eval` -/ -def eval' (x : arity → BitStream) : BitStream := +def eval' (x : ar → BitStream) : BitStream := BitStream.corec (fun ⟨x, (carry : p.State)⟩ => let x_head := (x · |>.head) let next := p.nextBit carry x_head @@ -82,11 +107,11 @@ def eval' (x : arity → BitStream) : BitStream := ) (x, p.initCarry) /-- `p.changeInitCarry c` yields an FSM with `c` as the initial state -/ -def changeInitCarry (p : FSM arity) (c : p.α → Bool) : FSM arity := +def changeInitCarry (p : FSM ar) (c : p.α → Bool) : FSM ar := { p with initCarry := c } theorem carry_changeInitCarry_succ - (p : FSM arity) (c : p.α → Bool) (x : arity → BitStream) : ∀ n, + (p : FSM ar) (c : p.α → Bool) (x : ar → BitStream) : ∀ n, (p.changeInitCarry c).carry x (n+1) = (p.changeInitCarry (p.nextBit c (fun a => x a 0)).1).carry (fun a i => x a (i+1)) n @@ -96,7 +121,7 @@ theorem carry_changeInitCarry_succ simp [nextBit, carry, changeInitCarry] theorem eval_changeInitCarry_succ - (p : FSM arity) (c : p.α → Bool) (x : arity → BitStream) (n : ℕ) : + (p : FSM ar) (c : p.α → Bool) (x : ar → BitStream) (n : ℕ) : (p.changeInitCarry c).eval x (n+1) = (p.changeInitCarry (p.nextBit c (fun a => x a 0)).1).eval (fun a i => x a (i+1)) n := by @@ -104,22 +129,13 @@ theorem eval_changeInitCarry_succ simp [eval, changeInitCarry, nextBit] /-- unfolds the definition of `eval` -/ -theorem eval_eq_carry (x : arity → BitStream) (n : ℕ) : +theorem eval_eq_carry (x : ar → BitStream) (n : ℕ) : p.eval x n = (p.nextBit (p.carry x n) (fun i => x i n)).2 := rfl -theorem eval_eq_eval' : - p.eval x = p.eval' x := by - funext i - simp only [eval, eval'] - induction i generalizing p x - case zero => rfl - case succ i ih => - sorry - /-- `p.changeVars f` changes the arity of an `FSM`. The function `f` determines how the new input bits map to the input expected by `p` -/ -def changeVars {arity2 : Type} (changeVars : arity → arity2) : FSM arity2 := +def changeVars {arity2 : Type} (changeVars : ar → arity2) : FSM arity2 := { p with nextBitCirc := fun a => (p.nextBitCirc a).map (Sum.map id changeVars) } /-- @@ -128,13 +144,13 @@ a family of `n` FSMs `qᵢ` of posibly different arities `mᵢ`, and given yet another arity `m` such that `mᵢ ≤ m` for all `i`, we can compose `p` with `qᵢ` yielding a single FSM of arity `m`, such that each FSM `qᵢ` computes the `i`th bit that is fed to the FSM `p`. -/ -def compose [FinEnum arity] [DecidableEq arity] +def compose [FinEnum ar] [DecidableEq ar] (new_arity : Type) -- `new_arity` is the resulting arity - (q_arity : arity → Type) -- `q_arityₐ` is the arity of FSM `qₐ` - (vars : ∀ (a : arity), q_arity a → new_arity) + (q_arity : ar → Type) -- `q_arityₐ` is the arity of FSM `qₐ` + (vars : ∀ (a : ar), q_arity a → new_arity) -- ^^ `vars` is the function that tells us, for each FSM `qₐ`, -- which bits of the final `new_arity` corresponds to the `q_arityₐ` bits expected by `qₐ` - (q : ∀ (a : arity), FSM (q_arity a)) : -- `q` gives the FSMs to be composed with `p` + (q : ∀ (a : ar), FSM (q_arity a)) : -- `q` gives the FSMs to be composed with `p` FSM new_arity := { α := p.α ⊕ (Σ a, (q a).α), i := by letI := p.i; infer_instance, @@ -162,11 +178,11 @@ def compose [FinEnum arity] [DecidableEq arity] (fun a => inl (inr ⟨_, a⟩)) (fun a => inr (vars x a))) } -lemma carry_compose [FinEnum arity] [DecidableEq arity] +lemma carry_compose [FinEnum ar] [DecidableEq ar] (new_arity : Type) - (q_arity : arity → Type) - (vars : ∀ (a : arity), q_arity a → new_arity) - (q : ∀ (a : arity), FSM (q_arity a)) + (q_arity : ar → Type) + (vars : ∀ (a : ar), q_arity a → new_arity) + (q : ∀ (a : ar), FSM (q_arity a)) (x : new_arity → BitStream) : ∀ (n : ℕ), (p.compose new_arity q_arity vars q).carry x n = let z := p.carry (λ a => (q a).eval (fun i => x (vars _ i))) n @@ -195,11 +211,11 @@ lemma carry_compose [FinEnum arity] [DecidableEq arity] · simp /-- Evaluating a composed fsm is equivalent to composing the evaluations of the constituent FSMs -/ -lemma eval_compose [FinEnum arity] [DecidableEq arity] +lemma eval_compose [FinEnum ar] [DecidableEq ar] (new_arity : Type) - (q_arity : arity → Type) - (vars : ∀ (a : arity), q_arity a → new_arity) - (q : ∀ (a : arity), FSM (q_arity a)) + (q_arity : ar → Type) + (vars : ∀ (a : ar), q_arity a → new_arity) + (q : ∀ (a : ar), FSM (q_arity a)) (x : new_arity → BitStream) : (p.compose new_arity q_arity vars q).eval x = p.eval (λ a => (q a).eval (fun i => x (vars _ i))) := by @@ -276,7 +292,7 @@ theorem carry_add_succ (x : Bool → BitStream) (n : ℕ) : unfold carry simp [nextBit, ih, Circuit.eval, BitStream.addAux, BitVec.adcb] -@[simp] theorem carry_zero (x : arity → BitStream) : carry p x 0 = p.initCarry := rfl +@[simp] theorem carry_zero (x : ar → BitStream) : carry p x 0 = p.initCarry := rfl @[simp] theorem initCarry_add : add.initCarry = (fun _ => false) := rfl @[simp] lemma eval_add (x : Bool → BitStream) : add.eval x = (x true) + (x false) := by @@ -495,17 +511,6 @@ def repeatBit : FSM Unit where nextBitCirc := fun _ => .or (.var true <| .inl ()) (.var true <| .inr ()) -@[simp] theorem eval_repeatBit : - repeatBit.eval x = BitStream.repeatBit (x ()) := by - unfold BitStream.repeatBit - rw [eval_eq_eval', eval'] - apply BitStream.corec_eq_corec - (R := fun a b => a.1 () = b.2 ∧ (a.2 ()) = b.1) - · simp [repeatBit] - · intro ⟨y, a⟩ ⟨b, x⟩ h - simp at h - simp [h, nextBit, BitStream.head] - end FSM structure FSMSolution (t : Term) extends FSM (Fin t.arity) where @@ -621,174 +626,7 @@ def termEvalEqFSM : ∀ (t : Term), FSMSolution t let q := termEvalEqFSM t { toFSM := by dsimp [arity]; exact composeUnary FSM.neg q, good := by ext; simp } - | incr t => - let q := termEvalEqFSM t - { toFSM := by dsimp [arity]; exact composeUnary FSM.incr q, - good := by ext; simp } - | decr t => - let q := termEvalEqFSM t - { toFSM := by dsimp [arity]; exact composeUnary FSM.decr q, - good := by ext; simp } -/-! -FSM that implement bitwise-and. Since we use `0` as the good state, -we keep the invariant that if both inputs are good and our state is `0`, then we produce a `0`. -If not, we produce an infinite sequence of `1`. --/ -def and : FSM Bool := - { α := Unit, - initCarry := fun _ => false, - nextBitCirc := fun a => - match a with - | some () => - -- Only if both are `0` we produce a `0`. - (Circuit.var true (inr false) ||| - ((Circuit.var false (inr true) ||| - -- But if we have failed and have value `1`, then we produce a `1` from our state. - (Circuit.var true (inl ()))))) - | none => -- must succeed in both arguments, so we are `0` if both are `0`. - Circuit.var true (inr true) ||| - Circuit.var true (inr false) - } - -/-! -FSM that implement bitwise-or. Since we use `0` as the good state, -we keep the invariant that if either inputs is `0` then our state is `0`. -If not, we produce a `1`. --/ -def or : FSM Bool := - { α := Unit, - initCarry := fun _ => false, - nextBitCirc := fun a => - match a with - | some () => - -- If either succeeds, then the full thing succeeds - ((Circuit.var true (inr false) &&& - ((Circuit.var false (inr true)) ||| - -- On the other hand, if we have failed, then propagate failure. - (Circuit.var true (inl ()))))) - | none => -- can succeed in either argument, so we are `0` if either is `0`. - Circuit.var true (inr true) &&& - Circuit.var true (inr false) - } - -/-! -FSM that implement logical not. -we keep the invariant that if the input ever fails and becomes a `1`, then we produce a `0`. -IF not, we produce an infinite sequence of `1`. - -EDIT: Aha, this doesn't work! -We need NFA to DFA here (as the presburger book does), -where we must produce an infinite sequence of`0` iff the input can *ever* become a `1`. -But here, since we phrase things directly in terms of producing sequences, it's a bit less clear -what we should do :) - -- Alternatively, we need to be able to decide `eventually always zero`. -- Alternatively, we push negations inside, and decide `⬝ ≠ ⬝` and `⬝ ≰ ⬝`. --/ - -inductive Result : Type - | falseAfter (n : ℕ) : Result - | trueFor (n : ℕ) : Result - | trueForall : Result -deriving Repr, DecidableEq - -def card_compl [Fintype α] [DecidableEq α] (c : Circuit α) : ℕ := - Finset.card $ (@Finset.univ (α → Bool) _).filter (fun a => c.eval a = false) - -theorem decideIfZeroAux_wf {α : Type _} [Fintype α] [DecidableEq α] - {c c' : Circuit α} (h : ¬c' ≤ c) : card_compl (c' ||| c) < card_compl c := by - apply Finset.card_lt_card - simp [Finset.ssubset_iff, Finset.subset_iff] - simp only [Circuit.le_def, not_forall, Bool.not_eq_true] at h - rcases h with ⟨x, hx, h⟩ - use x - simp [hx, h] - -def decideIfZerosAux {arity : Type _} [DecidableEq arity] - (p : FSM arity) (c : Circuit p.α) : Bool := - if c.eval p.initCarry - then false - else - have c' := (c.bind (p.nextBitCirc ∘ some)).fst - if h : c' ≤ c then true - else - have _wf : card_compl (c' ||| c) < card_compl c := - decideIfZeroAux_wf h - decideIfZerosAux p (c' ||| c) - termination_by card_compl c - -def decideIfZeros {arity : Type _} [DecidableEq arity] - (p : FSM arity) : Bool := - decideIfZerosAux p (p.nextBitCirc none).fst - -theorem decideIfZerosAux_correct {arity : Type _} [DecidableEq arity] - (p : FSM arity) (c : Circuit p.α) - (hc : ∀ s, c.eval s = true → - ∃ m y, (p.changeInitCarry s).eval y m = true) - (hc₂ : ∀ (x : arity → Bool) (s : p.α → Bool), - (FSM.nextBit p s x).snd = true → Circuit.eval c s = true) : - decideIfZerosAux p c = true ↔ ∀ n x, p.eval x n = false := by - rw [decideIfZerosAux] - split_ifs with h - · simp - exact hc p.initCarry h - · dsimp - split_ifs with h' - · simp only [true_iff] - intro n x - rw [p.eval_eq_zero_of_set {x | c.eval x = true}] - · intro y s - simp [Circuit.le_def, Circuit.eval_fst, Circuit.eval_bind] at h' - simp [Circuit.eval_fst, FSM.nextBit] - apply h' - · assumption - · exact hc₂ - · let c' := (c.bind (p.nextBitCirc ∘ some)).fst - have _wf : card_compl (c' ||| c) < card_compl c := - decideIfZeroAux_wf h' - apply decideIfZerosAux_correct p (c' ||| c) - simp [c', Circuit.eval_fst, Circuit.eval_bind] - intro s hs - rcases hs with ⟨x, hx⟩ | h - · rcases hc _ hx with ⟨m, y, hmy⟩ - use (m+1) - use fun a i => Nat.casesOn i x (fun i a => y a i) a - rw [FSM.eval_changeInitCarry_succ] - rw [← hmy] - simp only [FSM.nextBit, Nat.rec_zero, Nat.rec_add_one] - · exact hc _ h - · intro x s h - have := hc₂ _ _ h - simp only [Circuit.eval_bind, Bool.or_eq_true, Circuit.eval_fst, - Circuit.eval_or, this, or_true] -termination_by card_compl c - -theorem decideIfZeros_correct {arity : Type _} [DecidableEq arity] - (p : FSM arity) : decideIfZeros p = true ↔ ∀ n x, p.eval x n = false := by - apply decideIfZerosAux_correct - · simp only [Circuit.eval_fst, forall_exists_index] - intro s x h - use 0 - use (fun a _ => x a) - simpa [FSM.eval, FSM.changeInitCarry, FSM.nextBit, FSM.carry] - · simp only [Circuit.eval_fst] - intro x s h - use x - exact h +abbrev FSM.ofTerm (t : Term) : FSM (Fin t.arity) := termEvalEqFSM t |>.toFSM end FSM - -/-- -The fragment of predicate logic that we support in `bv_automata`. -Currently, we support equality, conjunction, disjunction, and negation. -This can be expanded to also support arithmetic constraints such as unsigned-less-than. --/ -inductive Predicate : Nat → Type _ where -| eq (t1 t2 : Term) : Predicate ((max t1.arity t2.arity)) -| and (p : Predicate n) (q : Predicate m) : Predicate (max n m) -| or (p : Predicate n) (q : Predicate m) : Predicate (max n m) --- For now, we can't prove `not`, because it needs NFA → DFA conversion --- the way Sid knows how to build it, or negation normal form, --- both of which is machinery we lack. --- | not (p : Predicate n) : Predicate n diff --git a/SSA/Experimental/Bits/AutoStructs/ForLean.lean b/SSA/Experimental/Bits/AutoStructs/ForLean.lean index 3c54fc02f..cc2408e7c 100644 --- a/SSA/Experimental/Bits/AutoStructs/ForLean.lean +++ b/SSA/Experimental/Bits/AutoStructs/ForLean.lean @@ -9,6 +9,7 @@ import Aesop /- Question: why does `Decidable (s ∈ l)` require `LawfulBEq` if `l` is a list but `DecidableEq` if `l` is an array? -/ +-- Practical ways to relate Finsets and HashSets @[simp] theorem ofBool_1_iff_true : BitVec.ofBool b = 1#1 ↔ b := by @@ -37,6 +38,22 @@ theorem Array.mem_of_mem_pop (a : Array α) (x : α) : x ∈ a.pop → x ∈ a : theorem Array.mem_push (a : Array α) (x y : α) : x ∈ a.push y → x ∈ a ∨ x = y := by sorry +theorem Array.mem_pop_iff (a : Array α) (x : α) : x ∈ a ↔ x ∈ a.pop ∨ a.back? = some x := by sorry + +theorem Array.mem_push_self (a : Array α) (x : α) : x ∈ a.push x := by + simp [Array.push] + +theorem Array.push_incl {a : Array α} {x : α} (y : α) : x ∈ a → x ∈ a.push y := by + simp [Array.push] + intros h + left + exact h.val + +@[aesop 50% unsafe] +theorem Array.mem_iff_getElem? {a : Array α} {x : α} : + x ∈ a ↔ ∃ (k : Nat), a[k]? = some x := by + sorry + theorem Std.HashMap.keys_nodup [BEq K] [Hashable K] (m : Std.HashMap K V) : m.keys.Nodup := by sorry @[simp] @@ -51,10 +68,68 @@ theorem Std.HashMap.mem_keys_insert_old [BEq K] [LawfulBEq K] [Hashable K] [Lawf intros _; apply mem_insert.mpr; simp_all only [beq_iff_eq, or_true] @[aesop 50% unsafe] -theorem Std.HashMap.get?_none_not_mem [BEq K] [LawfulBEq K] [Hashable K] [LawfulHashable K] (m : Std.HashMap K V) (k : K) : m.get? k = none → k ∉ m := by +theorem Std.HashMap.mem_iff_getElem? [BEq K] [LawfulBEq K] [Hashable K] [LawfulHashable K] {m : Std.HashMap K V} {k : K} : + k ∈ m ↔ ∃ v, m[k]? = some v := by + sorry + +@[aesop 50% unsafe] +theorem Std.HashMap.get?_none_not_mem [BEq K] [LawfulBEq K] [Hashable K] [LawfulHashable K] {m : Std.HashMap K V} {k : K} : m.get? k = none → k ∉ m := by + sorry + +@[aesop 50% unsafe] +theorem Std.HashMap.mem_of_get? [BEq K] [LawfulBEq K] [Hashable K] [LawfulHashable K] {m : Std.HashMap K V} {k : K} : + m.get? k = some v → k ∈ m := by sorry @[aesop 50% unsafe] theorem Std.HashMap.insert_keys_perm_new [BEq K] [LawfulBEq K] [Hashable K] [LawfulHashable K] (m : Std.HashMap K V) (k : K) (v : V) : k ∉ m → (m.insert k v).keys.Perm (k :: m.keys) := by sorry + +instance subtypeBEq [BEq α] (P : α → Prop) : BEq { x // P x } := { beq := fun x y => x.val == y.val } +instance [BEq α] [LawfulBEq α] (P : α → Prop) : LawfulBEq { x // P x } := by constructor <;> simp [subtypeBEq] + +-- is it sound? maybe we somehow need to know which instance for BEq was used to prevent some +-- weird stuff... +@[inline] private unsafe def Std.HashSet.attachWithImpl [BEq α] [LawfulBEq α] [Hashable α] [LawfulHashable α] + (xs : Std.HashSet α) (P : α → Prop) (_ : ∀ x ∈ xs, P x) : Std.HashSet {x // P x} := unsafeCast xs + +/-- `O(1)`. "Attach" a proof `P x` that holds for all the elements of `xs` to produce a new hash set + with the same elements but in the type `{x // P x}`. -/ +@[implemented_by attachWithImpl] def Std.HashSet.attachWith [BEq α] [LawfulBEq α] [Hashable α] [LawfulHashable α] + (xs : Std.HashSet α) (P : α → Prop) (H : ∀ x ∈ xs, P x) : Std.HashSet {x // P x} := + Std.HashSet.ofList <| xs.toList.attachWith P fun x h => H x (by sorry /- need lemmas about toList -/) + +theorem List.mem_attachWith_mem (l : List α) {P H}(x : α) h : ⟨x, h⟩ ∈ l.attachWith P H → x ∈ l := by + induction l + case nil => simp + case cons x l ih => simp only [attachWith_cons, mem_cons, Subtype.mk.injEq]; intros h; rcases h <;> simp_all + +theorem List.attachWith_nodup (l : List α) (hnd : l.Nodup) P H : (l.attachWith P H).Nodup := by + induction l + case nil => simp + case cons x l ih => + simp; constructor + · intros h; simp only [nodup_cons] at hnd; rcases hnd; have := l.mem_attachWith_mem x _ h; contradiction + · apply ih; simp_all + +def BitVec.ofFn {w : Nat} (f : Fin w → Bool) : BitVec w := + BitVec.iunfoldr (fun i _ => ((), f i)) () |>.2 + +-- TODO: is there a way to only have one of these three lemmas? + +@[simp] +theorem BitVec.ofFn_getLsbD {w : Nat} (f : Fin w → Bool) (i : Fin w) : + (BitVec.ofFn f).getLsbD i = f i := by + simp [BitVec.ofFn, BitVec.iunfoldr_getLsbD (fun _ => ())] + +@[simp] +theorem BitVec.ofFn_getLsbD' {w : Nat} (f : Fin w → Bool) (i : Nat) (hi : i < w) : + (BitVec.ofFn f).getLsbD i = f ⟨i, hi⟩ := ofFn_getLsbD f ⟨i, hi⟩ + +@[simp] +theorem BitVec.ofFn_getElem {w : Nat} (f : Fin w → Bool) (i : Fin w) : + (BitVec.ofFn f)[i.val] = f i := by + rw [←BitVec.ofFn_getLsbD f i] + rw [BitVec.getLsbD_eq_getElem?_getD] + simp diff --git a/SSA/Experimental/Bits/AutoStructs/ForMathlib.lean b/SSA/Experimental/Bits/AutoStructs/ForMathlib.lean new file mode 100644 index 000000000..50448c850 --- /dev/null +++ b/SSA/Experimental/Bits/AutoStructs/ForMathlib.lean @@ -0,0 +1,639 @@ +import Batteries.Data.Fin.Basic +import Mathlib.Computability.NFA +import Mathlib.Data.FinEnum +import Mathlib.Data.Vector.Basic +import Mathlib.Data.Vector.Defs +import SSA.Experimental.Bits.AutoStructs.ForLean + +open Set +open Mathlib + +@[simp] +lemma Mathlib.Vector.append_get_lt {x : Mathlib.Vector α n} {y : Mathlib.Vector α m} {i : Fin (n+m)} (hlt: i < n) : + (x.append y).get i = x.get (i.castLT hlt) := by + rcases x with ⟨x, hx⟩; rcases y with ⟨y, hy⟩ + dsimp [Mathlib.Vector.append, Mathlib.Vector.get] + apply List.getElem_append_left + +@[simp] +lemma Mathlib.Vector.append_get_ge {x : Mathlib.Vector α n} {y : Mathlib.Vector α m} {i : Fin (n+m)} (hlt: n ≤ i) : + (x.append y).get i = y.get ((i.cast (Nat.add_comm n m) |>.subNat n hlt)) := by + rcases x with ⟨x, hx⟩; rcases y with ⟨y, hy⟩ + dsimp [Mathlib.Vector.append, Mathlib.Vector.get] + rcases hx + apply List.getElem_append_right hlt + +@[simp] +def BitVec.getLsbD_cast' (bv : BitVec n) (h : n = m): + (h ▸ bv).getLsbD i = bv.getLsbD i := by + rcases h; simp + + +-- this is better because card is defeq to n +@[simps] +instance finenum_fin : FinEnum (Fin n) where + card := n + equiv := by rfl + +instance (α : Type) : Inter (Language α) := ⟨Set.inter⟩ +instance (α : Type) : Union (Language α) := ⟨Set.union⟩ + +def Mathlib.Vector.transport (v : Vector α m) (f : Fin n → Fin m) : Vector α n := + Vector.ofFn fun i => v.get (f i) + +def BitVec.transport (f : Fin n2 → Fin n1) (bv : BitVec n1) : BitVec n2 := + BitVec.ofFn fun i => bv.getLsbD (f i) + +@[simp] +lemma BitVec.transport_getLsbD (f : Fin n2 → Fin n1) (bv : BitVec n1) (i : Fin n2) : + (bv.transport f).getLsbD i = bv.getLsbD (f i) := by + simp [transport] + +/-- +The set of `n`-tuples of bit vectors of an arbitrary width. +-/ +structure BitVecs (n : Nat) where + w : Nat + bvs : Vector (BitVec w) n + +abbrev BitVecs.empty : BitVecs n := ⟨0, Mathlib.Vector.replicate n .nil⟩ +abbrev BitVecs.singleton {w : Nat} (bv : BitVec w) : BitVecs 1 := ⟨w, bv ::ᵥ .nil⟩ +abbrev BitVecs.pair {w : Nat} (bv1 bv2 : BitVec w) : BitVecs 2 := ⟨w, bv1 ::ᵥ bv2 ::ᵥ .nil⟩ + +def BitVecs0 : Set (BitVecs n) := + {⟨0, Vector.replicate n (BitVec.zero 0)⟩} + +-- TODO: this ought to be way easier +@[ext (iff := false)] +lemma BitVecs.ext (x y : BitVecs n) : + ∀ (heq : x.w = y.w), + (∀ (i : Fin n), x.bvs.get i = heq ▸ y.bvs.get i) → + x = y := by + intros heq hbvs + rcases x with ⟨wx, bvsx⟩ + rcases y with ⟨wy, bvsy⟩ + congr + rcases heq + apply heq_of_eq + ext i j + simp_all + +/-- +The set of `n`-tuples of bit vectors of an arbitrary width, encoded as a list of +bit vectors of width `n`. The width of the encoded bit vectors is the length of +the list. +-/ +abbrev BitVecs' (n : Nat) := List (BitVec n) + +def enc (bvs : BitVecs n) : BitVecs' n := + (List.finRange bvs.w).map (fun i => + BitVec.ofFn (fun (k : Fin n) => (bvs.bvs.get k)[i])) + +def dec (bvs' : BitVecs' n) : BitVecs n where + w := bvs'.length + bvs := Vector.ofFn fun k => BitVec.ofFn fun i => bvs'[i].getLsbD k + +@[simp] +lemma dec_nil n : dec (n := n) [] = BitVecs.empty := by + ext <;> simp [dec] + +-- The two sets are in bijection. + +@[simp] +lemma enc_length (bvs : BitVecs n) : (enc bvs).length = bvs.w := by + simp [enc] + +@[simp] +lemma dec_w (bvs' : BitVecs' n) : (dec bvs').w = bvs'.length := by + simp [dec] + +@[simp] +lemma enc_spec (bvs : BitVecs n) (i : Fin bvs.w) (k : Fin n) : + (enc bvs)[i][k] = (bvs.bvs.get k)[i] := by + simp [enc, dec] + +@[simp] +lemma dec_spec (bvs' : BitVecs' n) (k : Fin n) (i : Fin bvs'.length) : + ((dec bvs').bvs.get k).getLsbD i = bvs'[i].getLsbD k := by + simp [dec] + +@[simp] +lemma dec_spec' (bvs' : BitVecs' n) (k : Fin n) (i : Fin bvs'.length) : + ((dec bvs').bvs.get k).getLsbD i = bvs'[i].getLsbD k := by + simp [dec] + +lemma dec_enc_w (bvs : BitVecs n) : (dec (enc bvs)).w = bvs.w := by simp [enc, dec] + +lemma helper_dec_enc (bvs : BitVecs n) (h : w' = bvs.w) i (j : Nat) : + (bvs.bvs.get i)[j]?.getD false = (h ▸ bvs.bvs.get i)[j]?.getD false := by + rcases h; simp + +@[simp] +lemma dec_enc : Function.RightInverse (α := BitVecs' n) enc dec := by + intros bvs; ext1; exact dec_enc_w bvs + next i => + simp [enc, dec] + ext j + simp + rw [BitVec.getLsbD_eq_getElem?_getD] + rw [BitVec.getElem_eq_getElem?] + rw [Option.get_eq_getD (fallback := false)] + +@[simp] +lemma enc_dec : Function.LeftInverse (α := BitVecs' n) enc dec := by + intros bvs'; simp [enc, dec] + ext1 k + by_cases hin : k < (List.length bvs') + · simp + rw [List.getElem?_eq_getElem] <;> simp_all + ext1; simp + · simp; repeat rw [List.getElem?_eq_none] <;> simp_all + +@[simp] +lemma dec_enc' : dec (enc bvs) = bvs := by apply dec_enc +@[simp] +lemma enc_dec' : enc (dec bvs') = bvs' := by apply enc_dec + +@[simp] +def dec_bij {n : Nat} : Function.Bijective (dec (n := n)) := by + rw [Function.bijective_iff_has_inverse]; use enc; simp + +def dec_surj (n : Nat) : Function.Surjective (dec (n := n)) := by + exact Function.Bijective.surjective dec_bij + +def dec_inj {n : Nat} : Function.Injective (dec (n := n)) := by + exact Function.Bijective.injective dec_bij + +@[simp] +lemma dec_snoc n (bvs' : BitVecs' n) (a : BitVec n) : dec (bvs' ++ [a]) = + { w := bvs'.length + 1 + bvs := Vector.ofFn fun k => BitVec.cons (a.getLsbD k) ((dec bvs').bvs.get k) } := by + ext k i <;> simp [dec] + rw [BitVec.getLsbD_cons] + rcases i with ⟨i, hi⟩; simp at hi ⊢ + split + next heq => simp_all + next h => + have hlt : i < List.length bvs' := by omega + rw [List.getElem_append_left hlt, BitVec.ofFn_getLsbD' _ _ hlt] + +@[simp] +lemma dec_enc_image : dec '' (enc '' S) = S := Function.LeftInverse.image_image dec_enc _ + +@[simp] +lemma env_dec_image : enc '' (dec '' S) = S := Function.LeftInverse.image_image enc_dec _ + +def BitVecs.transport (f : Fin n → Fin m) (bvs : BitVecs m) : BitVecs n := + { w := bvs.w, bvs := bvs.bvs.transport f } + + +@[simp] +lemma BitVecs.transport_w {bvs : BitVecs n} : (BitVecs.transport f bvs).w = bvs.w := by + simp [transport] + +@[simp] +lemma BitVecs.transport_getElem {bvs : BitVecs m} (f : Fin n → Fin m) (i : Fin n) : + (bvs.transport f).bvs.get i = bvs.bvs.get (f i) := by + simp [transport, Mathlib.Vector.transport] + +def BitVecs'.transport (f : Fin n → Fin m) (bvs' : BitVecs' m): BitVecs' n := + bvs'.map fun bv => bv.transport f + +@[simp] +lemma BitVecs'.tranport_length {bvs' : BitVecs' n} : (BitVecs'.transport f bvs').length = bvs'.length := by + simp [transport] + +@[simp] +lemma BitVecs'.transport_getElem {bvs' : BitVecs' m} (f : Fin n → Fin m) (i : Fin bvs'.length) : + (bvs'.transport f)[i] = bvs'[i].transport f := by + simp [transport] + +@[simp] +lemma BitVecs'.transport_getElem' {bvs' : BitVecs' m} (f : Fin n → Fin m) (i : Nat) (h : i < bvs'.length) : + (bvs'.transport f)[i]'(by simp_all) = (bvs'[i]'h).transport f := by + simp [transport] + +-- TODO: this script generates an ill typed proof :( +set_option debug.skipKernelTC true in +@[simp] +def dec_transport_idx {bvs' : BitVecs' n} (f : Fin m → Fin n) : + have h : (BitVecs.transport f (dec bvs')).w = (dec (BitVecs'.transport f bvs')).w := by simp + (dec (bvs'.transport f)).bvs.get i = h ▸ (((dec bvs').transport f).bvs.get i) := by + intros h + simp [dec] + ext1 i + simp + rw [BitVecs'.transport_getElem' f i] + rcases i with ⟨i, hi⟩; simp + rw [BitVec.ofFn_getLsbD' _ i (by simp_all)] + simp + +@[simp] +def dec_transport : + dec (bvs'.transport f) = (dec bvs').transport f := by + ext k j <;> simp + +@[simp] +def enc_transport_idx {bvs : BitVecs n} (f : Fin m → Fin n) (i : Fin bvs.w) : + -- have h : (BitVecs.transport f (dec bvs')).w = (dec (BitVecs'.transport f bvs')).w := by simp + (enc (bvs.transport f))[i] = (enc bvs)[i].transport f := by + ext1 k; simp [enc]; rfl + +@[simp] +def enc_transport : + enc (bvs.transport f) = (enc bvs).transport f := by + apply List.ext_getElem <;> simp + intros i hi hi' + have _ := enc_transport_idx f ⟨i, hi⟩ + simp_all + +@[simp] +def dec_transport_preim : + dec '' (BitVecs'.transport f ⁻¹' S) = BitVecs.transport f ⁻¹' (dec '' S) := by + ext1 bvs; simp; constructor + · rintro ⟨bvs', htr, hdec⟩ + use bvs'.transport f; constructor; apply htr + simp [← hdec] + · rintro ⟨bvs', hS, hdec⟩ + use enc bvs + rw [←enc_transport] + constructor <;> simp_all [←hdec, enc_dec] + +@[simp] +def dec_transport_image (f : Fin m → Fin n) : + dec '' (BitVecs'.transport f '' S) = BitVecs.transport f '' (dec '' S) := by + ext1; simp + +namespace NFA + +def Complete' (M : NFA α σ) : Prop := ∀ q a, M.step q a ≠ ∅ + +def Complete (M : NFA α σ) : Prop := ∀ w, Nonempty (M.eval w) + +lemma complete_stepSet_ne {M : NFA α σ} {hc : M.Complete'} : S ≠ ∅ → M.stepSet S a ≠ ∅ := by + push_neg; rintro ⟨q, hq⟩ + have hne := hc q a + push_neg at hne + rcases hne with ⟨q', hq'⟩ + use q'; simp [stepSet]; use q + +structure Deterministic (M : NFA α σ) : Prop where + start : M.start.Subsingleton + step : ∀ q a, M.step q a |>.Subsingleton + +attribute [simp] Deterministic.start Deterministic.step + +lemma deterministic_stepSet_subsingleton {M : NFA α σ} {S : Set σ} (hd : M.Deterministic) : + S.Subsingleton → (M.stepSet S a |>.Subsingleton) := by + intros hS + simp_all [stepSet, Set.Subsingleton] + intros q1' q1 hq1 hq1' q2' q2 hq2 hq2' + obtain rfl := hS hq1 hq2 + obtain rfl := hd.step q1 a hq1' hq2' + rfl + +lemma deterministic_eval_subsingleton {M : NFA α σ} (hd : M.Deterministic) w : + M.eval w |>.Subsingleton := by + induction w using List.list_reverse_induction + case base => simp_all + case ind w a ih => simp; apply deterministic_stepSet_subsingleton <;> assumption + +private noncomputable instance {M : NFA α σ} : Decidable M.Complete := + Classical.propDecidable _ + + +@[simp, aesop 50% unsafe] +theorem stepSet_mono (M : NFA α σ) (S₁ S₂ : Set σ) (a : α) (h : S₁ ⊆ S₂) : + M.stepSet S₁ a ⊆ M.stepSet S₂ a := by + simp only [stepSet]; apply biUnion_mono <;> simp_all + +@[simp, aesop 50% unsafe] +theorem evalFrom_mono (M : NFA α σ) (S₁ S₂ : Set σ) (x : List α) (h : S₁ ⊆ S₂) : + M.evalFrom S₁ x ⊆ M.evalFrom S₂ x := by + simp only [evalFrom]; induction' x with a x ih generalizing S₁ S₂ <;> simp_all [List.foldl_cons] + +def Reachable (M : NFA α σ) : Set σ := λ q ↦ ∃ w, q ∈ M.eval w + +def reduce (M : NFA α σ) : NFA α M.Reachable where + start q := M.start q.val + accept q := M.accept q.val + step q a q' := M.step q.val a q'.val + +lemma reduce_stepSet {M : NFA α σ} {q : σ} (S1 : Set M.Reachable) (S2 : Set σ) : + (∀ q, (∃ hq, S1 ⟨q, hq⟩) ↔ S2 q) → + ((∃ hq, ⟨q, hq⟩ ∈ M.reduce.stepSet S1 a) ↔ q ∈ M.stepSet S2 a) := by + intros h + simp_all [reduce, stepSet]; constructor + · rintro ⟨hq, q', ⟨hr, hs1⟩, hs⟩ + have hin : S2 q' := by rw [←h q']; use hr; apply hs1 + use q'; constructor; apply hin; apply hs + · rintro ⟨q', hs2, hs⟩ + obtain ⟨hr', hs1⟩ :=(h q').mpr hs2 + have hr : q ∈ M.Reachable := by + obtain ⟨w, he⟩ := hr' + use (w ++ [a]); simp [stepSet]; use q' + use hr, q'; constructor + · use hr'; apply hs1 + · apply hs + +lemma reduce_stepSet' {M : NFA α σ} (q : M.Reachable) (S1 : Set M.Reachable) (S2 : Set σ) : + (∀ q, (∃ hq, S1 ⟨q, hq⟩) ↔ S2 q) → + (q ∈ M.reduce.stepSet S1 a → q.val ∈ M.stepSet S2 a) := by + intros h; simp [←reduce_stepSet _ _ h] + +lemma reduce_eval {M : NFA α σ} {w} (q : σ) : (∃ hq, ⟨q, hq⟩ ∈ M.reduce.eval w) ↔ q ∈ M.eval w := by + induction w using List.list_reverse_induction generalizing q + case base => simp [reduce, Set.instMembership, Set.Mem]; intros hs; use .nil; simpa + case ind a w ih => + simp [eval]; constructor + · rintro ⟨hq, hs⟩ + apply reduce_stepSet' at hs + apply hs + apply ih + · rintro hs + rw [←reduce_stepSet] at hs + apply hs + apply ih + +@[simp] +lemma reduce_spec (M : NFA α σ) : M.reduce.accepts = M.accepts := by + ext w; simp [accepts]; constructor + · rintro ⟨q, hr, ha, he⟩ + use q + constructor + · apply ha + · simp_all [←reduce_eval q] + · rintro ⟨q, ha, he⟩ + obtain ⟨hq, he'⟩ := reduce_eval q |>.mpr he + use q, hq + constructor + · apply ha + · simp_all [←reduce_eval q] + +-- TODO: M.reduce is reduced + +def closed_set (M : NFA α σ) (S : Set σ) := M.start ⊆ S ∧ ∀ a, M.stepSet S a ⊆ S + +theorem reachable_sub_closed_set (M : NFA α σ) (S : Set σ) (hcl: M.closed_set S) : + M.Reachable ⊆ S := by + rintro q ⟨w, hw⟩ + rcases hcl with ⟨hstart, hincl⟩ + induction w using List.list_reverse_induction generalizing q + case base => aesop + case ind w a ih => + simp only [eval] at hw + rw [evalFrom_append_singleton, mem_stepSet] at hw + rcases hw with ⟨q', h1, h2⟩ + apply ih at h1 + suffices _ : q ∈ M.stepSet S a by aesop + rw [mem_stepSet]; use q' + +@[simps] +def complete (M : NFA α σ) : NFA α (σ ⊕ Unit) where + start := { x | match x with | .inl x => x ∈ M.start | .inr () => True } + accept := { x | match x with | .inl x => x ∈ M.accept | .inr () => False } + step x a := { y | + match x with + | .inl x => match y with | .inl y => y ∈ M.step x a | .inr () => False + | .inr () => y = .inr () } + +@[simp] +lemma accepts_cast {M : NFA α σ} (h : σ = ς): (h ▸ M).accepts = M.accepts := by + rcases h; simp + +@[simp] +lemma step_cast {M : NFA α σ} (h : σ = ς) (q q' : σ): (h ▸ q') ∈ (h ▸ M).step (h ▸ q) a ↔ q' ∈ M.step q a := by + rcases h; simp + +@[simp] +lemma complete_cast {M : NFA α σ} (h : σ = ς) : (h ▸ M).Complete ↔ M.Complete := by + rcases h; simp + +@[simp] +lemma complete_stepSet {M : NFA α σ} (q : σ) : + (∀ q, (Sum.inl q ∈ S1) ↔ S2 q) → + ((.inl q ∈ M.complete.stepSet S1 a) ↔ q ∈ M.stepSet S2 a) := by + simp_all [complete, stepSet, Set.instMembership, Set.Mem] + +lemma complete_stepSet_sink {M : NFA α σ} : + .inr () ∈ S → .inr () ∈ M.complete.stepSet S a := by + simp_all [complete, stepSet, Set.instMembership, Set.Mem] + +@[simp] +lemma complete_eval {M : NFA α σ} {w} (q : σ) : + (.inl q ∈ M.complete.eval w) ↔ q ∈ M.eval w := by + induction w using List.list_reverse_induction generalizing q + case base => simp [complete, Set.instMembership, Set.Mem] + case ind a w ih => + simp only [eval]; constructor + · simp; rintro _; rw [←complete_stepSet]; assumption; apply ih + · simp; rintro _; rw [complete_stepSet]; assumption; apply ih + +@[simp] +theorem complete_accepts (M : NFA α σ) : M.complete.accepts = M.accepts := by + simp [accepts] + +@[simp] +theorem complete_complete (M : NFA α σ) : M.complete.Complete := by + intros w + use (.inr ()) + induction w using List.list_reverse_induction + case base => simp + case ind w a ih => + simp [eval] + apply complete_stepSet_sink + apply ih + +def product (accept? : Prop → Prop → Prop) (M : NFA α σ) (N : NFA α ς) : NFA α (σ × ς) where + step := fun (q₁, q₂) a => { (q₁', q₂') | (q₁' ∈ M.step q₁ a) ∧ (q₂' ∈ N.step q₂ a) } + start := { (q₁, q₂) | (q₁ ∈ M.start) ∧ (q₂ ∈ N.start) } + accept := { (q₁, q₂) | accept? (q₁ ∈ M.accept) (q₂ ∈ N.accept) } + +def inter (M : NFA α σ) (N : NFA α ς) : NFA α (σ × ς) := product And M N + +-- Note: the automata need to be complete! +def union' (M : NFA α σ) (N : NFA α ς) : NFA α (σ × ς) := product Or M N + +def union (M : NFA α σ) (N : NFA α ς) : NFA α ((σ ⊕ Unit) × (ς ⊕ Unit)) := + M.complete.union' N.complete + +@[simp] +lemma product_accept {M : NFA α σ} {N : NFA α ς} : + (q1, q2) ∈ (M.product accept? N).accept ↔ accept? (q1 ∈ M.accept) (q2 ∈ N.accept) := by + simp [product] + +@[simp] +lemma product_stepSet {M : NFA α σ} {N : NFA α ς} : + (M.product accept? N).stepSet (S1 ×ˢ S2) a = ((M.stepSet S1 a) ×ˢ (N.stepSet S2 a)) := by + ext ⟨q1, q2⟩; simp [product, stepSet]; constructor + · rintro ⟨q1', hq1, q2', hS, hq2⟩; constructor + · use q1'; simp_all + · use q2'; simp_all + · rintro ⟨⟨q1', h1, hs1⟩, ⟨q2', h2, hs2⟩⟩ + use q1'; constructor; assumption; use q2' + +@[simp] +lemma product_eval {M : NFA α σ} {N : NFA α ς} {w} : + (M.product accept? N).eval w = M.eval w ×ˢ N.eval w := by + unfold eval; induction w using List.list_reverse_induction + case base => ext; simp [product] + case ind w a ih => simp only [eval, evalFrom_append_singleton, product_stepSet, ih] + +@[simp] +theorem inter_accepts (M : NFA α σ) (N : NFA α ς) : + (M.inter N).accepts = M.accepts ∩ N.accepts:= by + ext w; simp [accepts, inter]; constructor + · rintro ⟨q1, q2, ⟨_, _⟩, _, _⟩; constructor; use q1; use q2 + · rintro ⟨⟨q1, _⟩, q2, _⟩; use q1, q2; simp_all + +@[simp] +theorem union'_accepts (M : NFA α σ) (N : NFA α ς) (hcM: M.Complete) (hcN : N.Complete) : + (M.union' N).accepts = M.accepts ∪ N.accepts := by + ext w; constructor + · simp [accepts] + rintro ⟨q1, q2, ha, he⟩ + simp [union'] at he ha + rcases ha with ha | ha + · left; use q1; simp_all + · right; use q2; simp_all + · simp [accepts] + rintro (⟨q1, ha, he⟩ | ⟨q2, ha, he⟩) + · obtain ⟨q2, he2⟩ := hcN w + use q1, q2; simp_all [union'] + · obtain ⟨q1, he1⟩ := hcM w + use q1, q2; simp_all [union'] + +@[simp] +theorem union_accepts (M : NFA α σ) (N : NFA α ς) : + (M.union N).accepts = M.accepts ∪ N.accepts := by + simp [union] + +def flipAccept (M : NFA α σ) : NFA α σ where + start := M.start + accept := M.accept.compl + step := M.step + +@[simp] +theorem flipAccept_eval {M : NFA α σ} : M.flipAccept.eval w = M.eval w := by + simp [flipAccept, eval, evalFrom]; unfold stepSet; simp + +@[simp] +theorem flipAccept_accepts (M : NFA α σ) (hc : M.Complete) (hdet : M.Deterministic) : + M.flipAccept.accepts = M.acceptsᶜ := by + ext w; constructor; simp [accepts, Language.eq_def, Set.compl_def]; rintro q ha he + · intros q' ha' he' + obtain rfl := deterministic_eval_subsingleton hdet w he he' + simp_all [flipAccept, Set.compl] + · simp [accepts, Language.eq_def, Set.compl_def] + intros hw + obtain ⟨qf, hqf⟩ := hc w + have ha : ¬ qf ∈ M.accept := by by_contra; apply hw <;> assumption + use qf; simp_all [flipAccept, Set.compl] + +def neg (M : NFA α σ) := M.toDFA.toNFA.flipAccept + +@[simp] +lemma determinize_complete (M : NFA α σ) : + M.toDFA.toNFA.Complete := by + simp [Complete, eval] + +@[simp] +lemma determinize_deternistic (M : NFA α σ) : + M.toDFA.toNFA.Deterministic := by + simp [Deterministic, DFA.toNFA, toDFA] + constructor <;> simp + +@[simp] +theorem neg_accepts (M : NFA α σ) : + M.neg.accepts = M.acceptsᶜ := by + simp [neg] + + +/- +NOTE: all that follows is defined in terms of bit vectors, even though it should +probably be defined in terms of `Vec n α` for an arbitrary type `α`. +-/ + +/-- Defined as bv'[i] = bv[f i] -/ +@[simps] +def lift (M: NFA (BitVec n1) σ) (f : Fin n1 → Fin n2) : NFA (BitVec n2) σ where + start := M.start + accept := M.accept + step q a := M.step q (a.transport f) + +@[simp] +lemma lift_stepSet (M : NFA (BitVec n) σ) (f : Fin n → Fin m) : + (M.lift f).stepSet S a = M.stepSet S (a.transport f) := by + simp [lift, stepSet] + +@[simp] +lemma lift_eval (M : NFA (BitVec n) σ) (f : Fin n → Fin m) : + (M.lift f).eval w = M.eval (BitVecs'.transport f w) := by + induction w using List.list_reverse_induction + case base => simp [lift, BitVecs'.transport] + case ind w a ih => simp [BitVecs'.transport, ih] + +@[simp] +lemma lift_accepts (M : NFA (BitVec n) σ) (f : Fin n → Fin m) : + (M.lift f).accepts = BitVecs'.transport f ⁻¹' M.accepts := by + simp [accepts] + +@[simps] +def proj (M: NFA (BitVec n1) σ) (f : Fin n2 → Fin n1) : NFA (BitVec n2) σ where + start := M.start + accept := M.accept + step q a := { q' | ∃ a', a'.transport f = a ∧ q' ∈ M.step q a' } + +@[simp] +lemma proj_stepSet (M : NFA (BitVec m) σ) (f : Fin n → Fin m) : + (M.proj f).stepSet S a = + ⋃ a' ∈ BitVec.transport f ⁻¹' {a}, M.stepSet S a' := by + ext q; simp [proj, stepSet]; constructor + · rintro ⟨q', hS, a', htr, hs⟩ + use a'; constructor; assumption; use q' + · rintro ⟨a', htr, q', hS, hs⟩ + use q'; constructor; assumption; use a' + +@[simp] +lemma proj_eval (M : NFA (BitVec m) σ) (f : Fin n → Fin m) : + (M.proj f).eval w = + ⋃ w' ∈ BitVecs'.transport f ⁻¹' {w}, M.eval w' := by + induction w using List.list_reverse_induction + case base => simp [proj, BitVecs'.transport] + case ind w a ih => + ext q; simp [BitVecs'.transport]; constructor + · rintro ⟨a', htr, S, hrS, hqS⟩ + rcases hrS with ⟨q', rfl⟩ + simp [ih] at hqS + rcases hqS with ⟨⟨w', htr', he⟩, hs⟩ + use w' ++ [a']; constructor + · simp_all; exact htr' + · simp; use M.step q' a'; constructor + on_goal 2 => assumption + use q'; simp_all + · rintro ⟨wa', heq, he⟩ + by_cases hemp : wa' = [] + · simp_all + have hdl := List.dropLast_concat_getLast hemp + rw [←hdl] at heq he + simp at heq + use List.getLast wa' hemp; constructor + · apply List.append_inj_right' at heq; simp_all + · obtain rfl := List.append_inj_left' heq (by simp) + simp at he; rcases he with ⟨S, ⟨q', rfl⟩, hqS⟩ + simp at hqS; rcases hqS with ⟨he, hs⟩ + simp only [stepSet, mem_iUnion, exists_prop] + use q' + simp [ih]; constructor + on_goal 2 => assumption + use wa'.dropLast + simp_all [BitVecs'.transport] + +@[simp] +lemma proj_accepts (M : NFA (BitVec m) σ) (f : Fin n → Fin m) : + (M.proj f).accepts = BitVecs'.transport f '' M.accepts := by + ext w; simp [accepts]; constructor + · rintro ⟨q, ha, w', htr, he⟩ + use w'; simp [htr]; use q + · rintro ⟨w', ⟨q, he, hv⟩, htr⟩ + use q; simp [he]; use w' diff --git a/SSA/Experimental/Bits/AutoStructs/FormulaToAuto.lean b/SSA/Experimental/Bits/AutoStructs/FormulaToAuto.lean index 6f28883a4..da1b59c6d 100644 --- a/SSA/Experimental/Bits/AutoStructs/FormulaToAuto.lean +++ b/SSA/Experimental/Bits/AutoStructs/FormulaToAuto.lean @@ -6,14 +6,163 @@ import Std.Data.HashMap import Mathlib.Data.Fintype.Basic import Mathlib.Data.Finset.Basic import Mathlib.Data.FinEnum +import Mathlib.Data.Vector.Basic +import Mathlib.Data.Vector.Defs import Mathlib.Tactic.FinCases import SSA.Experimental.Bits.AutoStructs.Basic import SSA.Experimental.Bits.AutoStructs.Constructions import SSA.Experimental.Bits.AutoStructs.Defs import SSA.Experimental.Bits.AutoStructs.FinEnum import SSA.Experimental.Bits.AutoStructs.FiniteStateMachine +import SSA.Experimental.Bits.AutoStructs.GoodNFA open AutoStructs +open Mathlib + +@[simp] theorem Language.mem_setOf_eq {x : List α} {p : List α → Prop} : + @Membership.mem (List α) (Language α) instMembershipListLanguage {y | p y} x = p x := by + rfl + +@[simp] theorem Language.trivial : x ∈ (⊤ : Language α) := by trivial + +def NFA.sa (_ : NFA α σ) := σ → Language α + +structure NFA.correct (M : NFA α σ) (ζ : M.sa) (L : Language α) where + cond1 : ∀ w, (w ∈ L ↔ ∃ q ∈ M.accept, w ∈ ζ q) + cond2 : ∀ w q, q ∈ M.eval w ↔ w ∈ ζ q + +lemma NFA.correct_spec {M : NFA α σ} {ζ : M.sa} {L : Language α} : + M.correct ζ L → M.accepts = L := by + rintro ⟨h1, h2⟩ + simp [accepts]; ext w + simp_all + +abbrev BVRel := ∀ ⦃w⦄, BitVec w → BitVec w → Prop +abbrev BVNRel n := ∀ ⦃w⦄, Vector (BitVec w) n → Prop + +def GoodNFA.sa (M : GoodNFA n) := M.σ → BVNRel n +def GoodNFA.sa2 (M : GoodNFA 2) := M.σ → BVRel + +def langRel (R : BVNRel n) : Set (BitVecs n) := + { bvs | R bvs.bvs } + +def langRel2 (R : BVRel) : Set (BitVecs 2) := + { bvs | R (bvs.bvs.get 0) (bvs.bvs.get 1) } + +@[simp] +lemma in_enc : x ∈ enc '' S ↔ dec x ∈ S := by + simp; constructor + · simp; rintro y hS rfl; simp_all + · rintro hS; use dec x; simp_all + +@[simp] +lemma Mathlib.Vector.ofFn_0 {f : Fin 0 → α} : ofFn f = .nil := by + simp [ofFn] + +@[simp] +lemma BitVec.ofFn_0 {f : Fin 0 → Bool} : ofFn f = .nil := by + apply eq_nil + +@[simp] +lemma dec_snoc_in_langRel {n} {R : BVNRel n} {w : BitVecs' n} {a : BitVec n} : + dec (w ++ [a]) ∈ langRel R ↔ + R (Vector.ofFn fun k => .cons (a.getLsbD k) ((dec w).bvs.get k)) := by + simp [langRel] + +@[simp] +lemma dec_snoc_in_langRel2 : + dec (w ++ [a]) ∈ langRel2 R ↔ R (.cons (a.getLsbD 0) ((dec w).bvs.get 0)) + (.cons (a.getLsbD 1) ((dec w).bvs.get 1)) := by + simp [langRel2] + +-- move +@[simp] +theorem BitVec.cast_inj (h : w = w') {x y : BitVec w} : cast h x = cast h y ↔ x = y := by + rcases h; simp + +-- move +@[simp] +lemma Fin.cast_val {a : Fin n} (h : n = m) : (h ▸ a).val = a.val := by + rcases h; simp + +-- move +@[simp] +theorem BitVec.append_inj {x1 x2 : BitVec w} {y1 y2 : BitVec w'} : + x1 ++ y1 = x2 ++ y2 ↔ x1 = x2 ∧ y1 = y2 := by + constructor + · rintro heq + have h : ∀ (i : Fin (w + w')), (x1 ++ y1).getLsbD i = (x2 ++ y2).getLsbD i := by simp [heq] + constructor + · apply eq_of_getLsbD_eq; intros i + specialize h (i.addNat w') + simp [getLsbD_append] at h + assumption + · apply eq_of_getLsbD_eq; intros i + specialize h (Nat.add_comm _ _ ▸ (i.castAdd w)) + simp [getLsbD_append] at h + assumption + · rintro ⟨rfl, rfl⟩; rfl + +@[simp] +lemma BitVec.cons_inj : cons b1 bv1 = cons b2 bv2 ↔ (b1 = b2) ∧ bv1 = bv2 := by + simp [cons] + +@[simp] lemma BitVec.lk30 : (3#2 : BitVec 2)[0] = true := by rfl +@[simp] lemma BitVec.lk31 : (3#2 : BitVec 2)[1] = true := by rfl +@[simp] lemma BitVec.lk20 : (2#2 : BitVec 2)[0] = false := by rfl +@[simp] lemma BitVec.lk21 : (2#2 : BitVec 2)[1] = true := by rfl +@[simp] lemma BitVec.lk10 : (1#2 : BitVec 2)[0] = true := by rfl +@[simp] lemma BitVec.lk11 : (1#2 : BitVec 2)[1] = false := by rfl +@[simp] lemma BitVec.lk00 : (0#2 : BitVec 2)[0] = false := by rfl +@[simp] lemma BitVec.lk01 : (0#2 : BitVec 2)[1] = false := by rfl + +structure GoodNFA.correct (M : GoodNFA n) (ζ : M.sa) (L : BVNRel n) where + cond1 : ∀ ⦃w⦄ (bvn : Vector (BitVec w) n), (L bvn ↔ ∃ q ∈ M.M.accept, ζ q bvn) + cond2 q : q ∈ M.M.start ↔ ζ q (Vector.replicate n .nil) + cond3 q a {w} (bvn : Vector (BitVec w) n) : q ∈ M.M.stepSet { q | ζ q bvn } a ↔ + ζ q (Vector.ofFn fun k => BitVec.cons (a.getLsbD k) (bvn.get k)) + +structure GoodNFA.correct2 (M : GoodNFA 2) (ζ : M.sa2) (L : BVRel) where + cond1 : ∀ (bv1 bv2 : BitVec w), (L bv1 bv2 ↔ ∃ q ∈ M.M.accept, ζ q bv1 bv2) + cond2 q : q ∈ M.M.start ↔ ζ q .nil .nil + cond3 q a w (bv1 bv2 : BitVec w) : q ∈ M.M.stepSet { q | ζ q bv1 bv2 } a ↔ + ζ q (BitVec.cons (a.getLsbD 0) bv1) (BitVec.cons (a.getLsbD 1) bv2) + +lemma GoodNFA.correct_spec {M : GoodNFA n} {ζ : M.sa} {L : BVNRel n} : + M.correct ζ L → M.accepts = langRel L := by + rintro ⟨h1, h2, h3⟩ + simp [accepts, accepts'] + have heq : dec '' (enc '' langRel L) = langRel L := by simp + rw [←heq] + congr! + suffices h : M.M.correct (fun q => enc '' langRel (ζ q)) (enc '' langRel L) by + apply NFA.correct_spec h + constructor + · intros w; rw [in_enc]; simp [langRel, h1]; simp_rw [@in_enc _ _ w]; rfl + intros w; induction w using List.list_reverse_induction + case base => + intros q; simp only [NFA.eval_nil]; rw [in_enc]; simp [h2, langRel] + case ind w a ih => + rintro q + simp only [NFA.eval_append_singleton] + rw [in_enc] + have h : M.M.eval w = { q | w ∈ enc '' langRel (ζ q) } := by + ext; rw [ih]; dsimp; rfl + rw [dec_snoc_in_langRel] + rw [h]; simp_rw [in_enc] + simp [langRel, h3] + +lemma GoodNFA.correct2_spec {M : GoodNFA 2} {ζ : M.sa2} {L : BVRel} : + M.correct2 ζ L → M.accepts = langRel2 L := by + rintro ⟨h1, h2, h3⟩ + suffices hc : M.correct (fun q w (bvn : Vector (BitVec w) 2) => ζ q (bvn.get 0) (bvn.get 1)) + (fun w bvn => L (bvn.get 0) (bvn.get 1)) by + rw [M.correct_spec hc] + simp [langRel2, langRel] + constructor + · simp_all + · intros q; simp_all; rfl + · simp_all section fsm @@ -21,60 +170,224 @@ abbrev Alphabet (arity: Type) [FinEnum arity] := BitVec (FinEnum.card arity + 1) variable {arity : Type} [FinEnum arity] -private structure fsm.State (carryLen : Nat) where - m : NFA $ Alphabet (arity := arity) -- TODO: ugly all over... - map : Std.HashMap (BitVec carryLen) _root_.State := ∅ - worklist : Array (BitVec carryLen) := ∅ - def finFunToBitVec (c : carry → Bool) [FinEnum carry] : BitVec (FinEnum.card carry) := ((FinEnum.toList carry).enum.map (fun (i, x) => c x |> Bool.toNat * 2^i)).foldl (init := 0) Nat.add |> BitVec.ofNat _ -def bitVecToFinFun [FinEnum ar] (bv : BitVec $ FinEnum.card ar) : ar → Bool := fun c => bv[FinEnum.equiv.toFun c] +def bitVecToFinFun [FinEnum ar] (bv : BitVec $ FinEnum.card ar) : ar → Bool := + fun c => bv[FinEnum.equiv.toFun c] + +def NFA.ofFSM (p : FSM arity) : NFA (Alphabet arity) (p.α → Bool) where + start := { q | q = p.initCarry } + accept := ⊤ + step s a := {s' | + let (s'', b) := p.nextBit s (bitVecToFinFun (a.truncate $ FinEnum.card arity)) + s' = s'' ∧ a.msb = b } + +def _root_.GoodNFA.ofFSM' (p : FSM arity) : GoodNFA (FinEnum.card arity + 1) where + σ := p.α → Bool + M := NFA.ofFSM p + +@[simp] +abbrev inFSMRel (p : FSM arity) {w} (bvn : Vector (BitVec w) _) := + bvn.get (Fin.last (FinEnum.card arity)) = p.evalBV (fun ar => bvn.get (FinEnum.equiv.toFun ar)) + +def GoodNFA.ofFSM_sa (p : FSM arity) : (GoodNFA.ofFSM' p).sa := fun q _ bvn => + inFSMRel p bvn ∧ q = p.carryBV (fun ar => bvn.get (FinEnum.equiv.toFun ar)) + +-- TODO: improve this proof +def GoodNFA.ofFSM_correct (p : FSM arity) : + (GoodNFA.ofFSM' p).correct (ofFSM_sa p) (fun _ bvn => inFSMRel p bvn) := by + constructor + · simp [inFSMRel, NFA.ofFSM, ofFSM', ofFSM_sa] + · simp [inFSMRel, NFA.ofFSM, ofFSM', ofFSM_sa]; intros q; constructor + · rintro rfl; constructor + · apply Subsingleton.allEq + · simp [FSM.carryBV] + · rintro ⟨-, rfl⟩; simp [FSM.carryBV] + · simp [inFSMRel, ofFSM']; intros q a w bvn + have heq : a.getLsbD (FinEnum.card arity) = a.msb := by + simp [BitVec.msb_eq_getLsbD_last] + constructor + · simp [NFA.stepSet] + rintro x hsa hst + simp [NFA.ofFSM] at hst + rcases hst with ⟨hq, hmsb⟩ + simp [ofFSM_sa]; constructor + · simp [FSM.evalBV] + rw [heq, hmsb] + unfold bitVecToFinFun + simp + ext i + simp [BitVec.getLsbD_cons] + split + next hi => + rw [hi] + simp [FSM.eval] + congr + rcases hsa with ⟨-, rfl⟩ + simp [FSM.carryBV] + · apply FSM.carry_eq_up_to; rintro ar k hk; simp [BitStream.ofBitVec] + rw [ite_cond_eq_true] + on_goal 2 => simp; omega + rw [ite_cond_eq_true] + on_goal 2 => simp; omega + simp [BitVec.getLsbD_cons] + rw [ite_cond_eq_false] + simp; omega + · ext ar; simp [BitVec.getLsbD_cons] + next hne => + rcases i with ⟨i, hi⟩ + simp at hne ⊢ + have hlt : i < w := by omega + rcases hsa with ⟨hsa, -⟩; simp [inFSMRel] at hsa + simp [hsa, FSM.evalBV] + rw [BitVec.ofFn_getLsbD' _ _ hlt] + simp + apply FSM.eval_eq_up_to; rintro ar k hk; simp [BitStream.ofBitVec] + rw [ite_cond_eq_true] + on_goal 2 => simp; omega + rw [ite_cond_eq_true] + on_goal 2 => simp; omega + simp [BitVec.getLsbD_cons] + rw [ite_cond_eq_false] + simp; omega + · rw [hq] + rcases hsa with ⟨-, rfl⟩ + simp [FSM.carryBV, FSM.carry]; congr + · apply FSM.carry_eq_up_to; rintro ar k hk; simp [BitStream.ofBitVec] + rw [ite_cond_eq_true] + on_goal 2 => simp; omega + rw [ite_cond_eq_true] + on_goal 2 => simp; omega + simp [BitVec.getLsbD_cons] + rw [ite_cond_eq_false] + simp; omega + · unfold bitVecToFinFun; simp [BitVec.getLsbD_cons] + · rintro hsa; simp [NFA.stepSet] + use p.carryBV (fun ar => bvn.get (FinEnum.equiv.toFun ar)) + rcases hsa with ⟨hrel, hcar⟩ + constructor + · constructor + on_goal 2 => rfl + simp [inFSMRel] at * + ext ⟨i, hi⟩ + simp + rw [BitVec.eq_of_getLsbD_eq_iff] at hrel + specialize hrel ⟨i, by omega⟩ + simp [BitVec.getLsbD_cons] at hrel + rw [ite_cond_eq_false] at hrel + on_goal 2 => simp; omega + rw [hrel] + simp [FSM.evalBV] + repeat rw [BitVec.ofFn_getLsbD' _ _ (by omega)] + simp + apply FSM.eval_eq_up_to; rintro ar k hk; simp [BitStream.ofBitVec] + rw [ite_cond_eq_true] + on_goal 2 => simp; omega + rw [ite_cond_eq_true] + on_goal 2 => simp; omega + simp [BitVec.getLsbD_cons] + omega + · rw [hcar]; simp [NFA.ofFSM] + constructor + · simp [FSM.carryBV, FSM.carry]; congr + · apply FSM.carry_eq_up_to; rintro ar k hk; simp [BitStream.ofBitVec] + rw [ite_cond_eq_true] + on_goal 2 => simp; omega + rw [ite_cond_eq_true] + on_goal 2 => simp; omega + simp [BitVec.getLsbD_cons] + omega + · unfold bitVecToFinFun; simp [BitVec.getLsbD_cons] + · unfold inFSMRel at hrel + rw [BitVec.eq_of_getLsbD_eq_iff] at hrel + specialize hrel (Fin.last w) + simp [BitVec.getLsbD_cons, heq] at hrel + rw [hrel]; simp [FSM.evalBV, FSM.eval, FSM.carryBV]; congr + · apply FSM.carry_eq_up_to; rintro ar k hk; simp [BitStream.ofBitVec] + rw [ite_cond_eq_true] + on_goal 2 => simp; omega + rw [ite_cond_eq_true] + on_goal 2 => simp; omega + simp [BitVec.getLsbD_cons] + omega + · unfold bitVecToFinFun; simp [BitVec.getLsbD_cons] + +def _root_.GoodNFA.ofFSM (p : FSM arity) : GoodNFA (FinEnum.card arity + 1) := + _root_.GoodNFA.ofFSM' p |>.reduce + +open BitStream in +lemma evalFinStream_evalFin {t : Term} {k : Nat} (hlt : k < w) (vars : Fin t.arity → BitVec w) : + EqualUpTo w (t.evalFinStream (fun ar => BitStream.ofBitVec (vars ar))) (ofBitVec $ t.evalFin vars) := by + induction t <;> simp + case var => rfl + case zero => unfold BitStream.ofBitVec; rintro _ _; simp + case negOne => + unfold BitStream.ofBitVec; rintro _ _; simp [BitVec.negOne_eq_allOnes]; left; assumption + case one => + unfold BitStream.ofBitVec; rintro k hk; simp + cases k <;> simp_all + case and => apply BitStream.and_congr <;> simp_all + case or => apply BitStream.or_congr <;> simp_all + case xor => apply BitStream.xor_congr <;> simp_all + case not => + rcases w with ⟨⟩ | ⟨w⟩ + · intros _ _; omega + · simp; apply BitStream.not_congr; simp_all + case add => + symm; transitivity; apply ofBitVec_add + symm; apply BitStream.add_congr <;> simp_all + case sub => + symm; transitivity; apply ofBitVec_sub + symm; apply BitStream.sub_congr <;> simp_all + case neg => + symm; transitivity; apply ofBitVec_neg + symm; apply BitStream.neg_congr; simp_all + +@[simp] +lemma FSM.eval_bv (bvn : Vector (BitVec w) (t.arity + 1)) : + ((FSM.ofTerm t).evalBV fun ar => bvn.get ar.castSucc) = + (t.evalFin fun ar => bvn.get ar.castSucc) := by + simp [FSM.evalBV]; ext ⟨k, hk⟩ + simp [BitVec.ofFn_getLsbD' _ _ hk, FSM.ofTerm] + rw [←(termEvalEqFSM t).good, evalFinStream_evalFin hk _ _ hk] + simp only [ite_eq_left_iff, not_lt] + intros _; omega + +@[simp] +lemma GoodNFA.ofFSM_spec (t : Term) : + (ofFSM (FSM.ofTerm t)).accepts = t.language := by + simp [ofFSM, correct_spec (ofFSM_correct (FSM.ofTerm t)), langRel, Term.language] + ext bvs; simp; tauto /-- -Transforms an `FSM` of arity `k` to an `NFA` of arity `k+1`. +Transforms an `FSM` of arity `k` to an `CNFA` of arity `k+1`. This correponds to transforming a function with `k` inputs and one output to a `k+1`-ary relation. By convention, the output is the MSB of the alphabet. -/ -partial -def NFA.ofFSM (p : FSM arity) [FinEnum p.α] : NFA (Alphabet (arity := arity)) := - let m := NFA.empty - let (s, m) := m.newState - let initState := finFunToBitVec p.initCarry - let m := m.addInitial s - let map := Std.HashMap.empty.insert initState s - let worklist := Array.singleton initState - let st : fsm.State (arity := arity) (FinEnum.card p.α) := { m, map, worklist } - go st -where go (st : fsm.State (arity := arity) (FinEnum.card p.α)) : NFA _ := Id.run do - let some carry := st.worklist.get? (st.worklist.size - 1) | return st.m - let some s := st.map.get? carry | return NFA.empty - let m := st.m.addFinal s - let st := { st with m, worklist := st.worklist.pop } - let st := (FinEnum.toList (BitVec (FinEnum.card arity))).foldl (init := st) fun st a => - let eval x := (p.nextBitCirc x).eval (Sum.elim (bitVecToFinFun carry) (bitVecToFinFun a)) - let res : Bool := eval none - let carry' : BitVec (FinEnum.card p.α) := finFunToBitVec (fun c => eval (some c)) - - let (s', st) := if let some s' := st.map.get? carry' then (s', st) else - let (s', m) := st.m.newState - let map := st.map.insert carry' s' - let worklist := st.worklist.push carry' - (s', {m, map, worklist}) - - let m := st.m.addTrans (a.cons res) s s' - { st with m } - go st +def GoodCNFA.ofFSM (p : FSM arity) : GoodCNFA (FinEnum.card arity + 1) := + worklistRun (BitVec (FinEnum.card p.α)) + (fun _ => true) + #[finFunToBitVec p.initCarry] + (by apply List.nodup_singleton) + fun carry => + (FinEnum.toList (BitVec (FinEnum.card arity))).foldl (init := #[]) fun ts a => + let eval x := (p.nextBitCirc x).eval (Sum.elim (bitVecToFinFun carry) (bitVecToFinFun a)) + let res : Bool := eval none + let carry' : BitVec (FinEnum.card p.α) := finFunToBitVec (fun c => eval (some c)) + ts.push (a.cons res, carry') + +lemma GoodCNFA.ofFSM_spec (p : FSM arity) : + (GoodCNFA.ofFSM p).Sim (GoodNFA.ofFSM p) := by + sorry end fsm - - -/- A bunch of NFAs that implement the relations we care about -/ +/- A bunch of CNFAs that implement the relations we care about -/ section nfas_relations -def NFA.ofConst {w} (bv : BitVec w) : NFA (BitVec 1) := - let m := NFA.empty +def CNFA.ofConst {w} (bv : BitVec w) : CNFA (BitVec 1) := + let m := CNFA.empty let (s, m) := m.newState let m := m.addInitial s let (s', m) := (List.range w).foldl (init := (s, m)) fun (s, m) i => @@ -84,8 +397,8 @@ def NFA.ofConst {w} (bv : BitVec w) : NFA (BitVec 1) := (s', m) m.addFinal s' -def NFA.autEq : NFA (BitVec 2) := - let m := NFA.empty +def CNFA.autEq : CNFA (BitVec 2) := + let m := CNFA.empty let (s, m) := m.newState let m := m.addInitial s let m := m.addFinal s @@ -93,8 +406,123 @@ def NFA.autEq : NFA (BitVec 2) := let m := m.addTrans 3 s s m -def NFA.autSignedCmp (cmp: RelationOrdering) : NFA (BitVec 2) := - let m := NFA.empty +def GoodCNFA.autEq : GoodCNFA 2 := + ⟨CNFA.autEq, by simp [CNFA.autEq]; sorry⟩ + +def NFA.autEq : NFA (BitVec 2) Unit := + { start := ⊤, accept := ⊤, step := fun () a => if a = 0 ∨ a = 3 then ⊤ else ⊥ } + +def GoodNFA.autEq : GoodNFA 2 := + ⟨Unit, { start := ⊤, accept := ⊤, step := fun () a => if a = 0 ∨ a = 3 then ⊤ else ⊥ }⟩ + +def GoodNFA.eqRel : BVRel := fun _ x y => x = y + +lemma GoodNFA.autEq_correct : autEq.correct2 (fun _ => eqRel) eqRel := by + constructor <;> simp [autEq, eqRel] + rintro ⟨⟩ ⟨a⟩ w bv1 bv2 + fin_cases a <;> simp [NFA.stepSet] + +-- Automata recognizing unsigned comparisons + +def CNFA.autUnsignedCmp (cmp: RelationOrdering) : CNFA (BitVec 2) := + let m := CNFA.empty + let (seq, m) := m.newState + let (sgt, m) := m.newState + let (slt, m) := m.newState + let m := m.addInitial seq + let m := m.addManyTrans [0#2, 3#2] seq seq + let m := m.addTrans 1#2 seq sgt + let m := m.addTrans 2#2 seq slt + let m := m.addManyTrans [0#2, 1#2, 3#2] sgt sgt + let m := m.addTrans 2#2 sgt slt + let m := m.addManyTrans [0#2, 2#2, 3#2] slt slt + let m := m.addTrans 1#2 slt sgt + match cmp with + | .lt => m.addFinal slt + | .le => (m.addFinal slt).addFinal seq + | .gt => m.addFinal sgt + | .ge => (m.addFinal sgt).addFinal seq + +def GoodCNFA.autUnsignedCmp (cmp: RelationOrdering) : GoodCNFA 2 := + ⟨CNFA.autUnsignedCmp cmp, by sorry⟩ + +inductive NFA.unsignedCmpState : Type where +| eq | gt | lt + +def NFA.unsignedCmpStep (q : NFA.unsignedCmpState) (a : BitVec 2) : Set NFA.unsignedCmpState := + match q, a with + | .eq, 0 => { .eq } | .eq, 3 => { .eq } | .eq, 1 => { .gt } | .eq, 2 => { .lt } + | .gt, 0 => { .gt } | .gt, 1 => { .gt } | .gt, 3 => { .gt } | .gt, 2 => { .lt } + | .lt, 0 => { .lt } | .lt, 1 => { .gt } | .lt, 2 => { .lt } | .lt, 3 => { .lt } + +def NFA.autUnsignedCmp (cmp: RelationOrdering) : NFA (BitVec 2) unsignedCmpState where + step := unsignedCmpStep + start := {.eq} + accept := match cmp with | .lt => {.lt} | .le => {.lt, .eq} | .gt => {.gt} | .ge => {.gt, .eq} + +def GoodNFA.autUnsignedCmp (cmp: RelationOrdering) : GoodNFA 2 := + ⟨_, NFA.autUnsignedCmp cmp⟩ + +def AutoStructs.RelationOrdering.urel (cmp : RelationOrdering) : BVRel := + match cmp with + | .lt => fun _ bv1 bv2 => bv1 <ᵤ bv2 + | .le => fun _ bv1 bv2 => bv1 ≤ᵤ bv2 + | .gt => fun _ bv1 bv2 => bv1 >ᵤ bv2 + | .ge => fun _ bv1 bv2 => bv1 ≥ᵤ bv2 + +def GoodNFA.autUnsignedCmpSA (q : NFA.unsignedCmpState) : BVRel := + match q with + | .eq => fun _ bv1 bv2 => bv1 = bv2 + | .lt => fun _ bv1 bv2 => bv1 <ᵤ bv2 + | .gt => fun _ bv1 bv2 => bv1 >ᵤ bv2 + +lemma BitVec.ule_iff_ult_or_eq {w : ℕ} (bv1 bv2 : BitVec w): + (bv2 ≥ᵤ bv1) = true ↔ (bv2 >ᵤ bv1) = true ∨ bv1 = bv2 := by + simp [BitVec.ule, BitVec.ult, le_iff_lt_or_eq, BitVec.toNat_eq] + +@[simp] +lemma BitVec.cons_ugt_iff {w} {bv1 bv2 : BitVec w} : + (BitVec.cons b1 bv1 >ᵤ BitVec.cons b2 bv2) ↔ (if b1 = b2 then bv1 >ᵤ bv2 else b1) := by + simp [BitVec.ult, Nat.shiftLeft_eq] + rw [Nat.mul_comm] + nth_rw 2 [Nat.mul_comm] + have _ := bv1.isLt + have _ := bv2.isLt + repeat rw [←Nat.mul_add_lt_is_or] <;> try assumption + cases b1 <;> cases b2 <;> simp <;> omega + +@[simp] +lemma ucmp_tricho : (bv1 >ᵤ bv2) = false → (bv2 >ᵤ bv1) = false → bv1 = bv2 := by + simp [BitVec.ule, BitVec.ult, BitVec.toNat_eq] + apply Nat.le_antisymm + +lemma GoodNFA.autUnsignedCmp_correct cmp : autUnsignedCmp cmp |>.correct2 autUnsignedCmpSA cmp.urel := by + let getState {w} (bv1 bv2 : BitVec w) : NFA.unsignedCmpState := + if bv1 >ᵤ bv2 then .gt else if bv2 >ᵤ bv1 then .lt else .eq + constructor <;> simp [NFA.autUnsignedCmp, autUnsignedCmp, autUnsignedCmpSA, AutoStructs.RelationOrdering.urel] + · cases cmp <;> simp [BitVec.ule_iff_ult_or_eq]; tauto + · rintro (_ | _ | _) <;> simp + · rintro (_ | _ | _) a w bv1 bv2 <;> simp [NFA.stepSet, NFA.unsignedCmpStep] + · constructor + · rintro ⟨i, hi⟩; cases i <;> fin_cases a <;> simp_all [NFA.unsignedCmpStep, instFinEnumBitVec_sSA] + · rintro ⟨_, _⟩; use .eq; simp; fin_cases a <;> simp [instFinEnumBitVec_sSA] at * <;> tauto + · constructor + · rintro ⟨i, hi⟩; cases i <;> fin_cases a <;> simp_all [NFA.unsignedCmpStep, instFinEnumBitVec_sSA] + · rintro _; fin_cases a <;> simp [instFinEnumBitVec_sSA] at * + · use .gt; simp_all + · use (getState bv1 bv2); simp [getState]; split_ifs <;> simp_all; apply ucmp_tricho <;> assumption + · use .gt; simp_all + · constructor + · rintro ⟨i, hi⟩; cases i <;> fin_cases a <;> simp_all [NFA.unsignedCmpStep, instFinEnumBitVec_sSA] + · rintro _; fin_cases a <;> simp [instFinEnumBitVec_sSA] at * + · use .lt; simp_all + · use (getState bv1 bv2); simp [getState]; split_ifs <;> simp_all; apply ucmp_tricho <;> assumption + · use .lt; simp_all + +-- Automata recognizing signed comparisons + +def CNFA.autSignedCmp (cmp: RelationOrdering) : CNFA (BitVec 2) := + let m := CNFA.empty let (seq, m) := m.newState let (sgt, m) := m.newState let (slt, m) := m.newState @@ -120,136 +548,393 @@ def NFA.autSignedCmp (cmp: RelationOrdering) : NFA (BitVec 2) := | .gt => m.addFinal sgtfin | .ge => (m.addFinal sgtfin).addFinal seq -def NFA.autUnsignedCmp (cmp: RelationOrdering) : NFA (BitVec 2) := - let m := NFA.empty - let (seq, m) := m.newState - let (sgt, m) := m.newState - let (slt, m) := m.newState - let m := m.addInitial seq - let m := m.addManyTrans [0#2, 3#2] seq seq - let m := m.addTrans 1#2 seq sgt - let m := m.addTrans 2#2 seq slt - let m := m.addManyTrans [0#2, 1#2, 3#2] sgt sgt - let m := m.addTrans 2#2 sgt slt - let m := m.addManyTrans [0#2, 2#2, 3#2] slt slt - let m := m.addTrans 1#2 slt sgt +def GoodCNFA.autSignedCmp (cmp: RelationOrdering) : GoodCNFA 2 := + ⟨CNFA.autSignedCmp cmp, by sorry⟩ + +inductive NFA.signedCmpState : Type where +| eq | gt | lt | ltfin | gtfin + +def NFA.signedCmpStep (q : NFA.signedCmpState) (a : BitVec 2) : Set NFA.signedCmpState := + match q, a with + | .eq, 0 => { .eq } | .eq, 3 => { .eq } | .eq, 1 => { .gt, .ltfin } | .eq, 2 => { .lt, .gtfin } + | .gt, 0 => { .gt, .gtfin } | .gt, 1 => { .gt, .ltfin } | .gt, 3 => { .gt, .gtfin } | .gt, 2 => { .lt, .gtfin } + | .lt, 0 => { .lt, .ltfin } | .lt, 1 => { .gt, .ltfin } | .lt, 2 => { .lt, .gtfin } | .lt, 3 => { .lt, .ltfin } + | .gtfin, _ => ∅ + | .ltfin, _ => ∅ + +def NFA.autSignedCmp (cmp: RelationOrdering) : NFA (BitVec 2) signedCmpState where + step := signedCmpStep + start := {.eq} + accept := match cmp with | .lt => {.ltfin} | .le => {.ltfin, .eq} | .gt => {.gtfin} | .ge => {.gtfin, .eq} + +def GoodNFA.autSignedCmp (cmp: RelationOrdering) : GoodNFA 2 := + ⟨_, NFA.autSignedCmp cmp⟩ + +def AutoStructs.RelationOrdering.srel (cmp : RelationOrdering) : BVRel := match cmp with - | .lt => m.addFinal slt - | .le => (m.addFinal slt).addFinal seq - | .gt => m.addFinal sgt - | .ge => (m.addFinal sgt).addFinal seq + | .lt => fun _ bv1 bv2 => bv1 <ₛ bv2 + | .le => fun _ bv1 bv2 => bv1 ≤ₛ bv2 + | .gt => fun _ bv1 bv2 => bv1 >ₛ bv2 + | .ge => fun _ bv1 bv2 => bv1 ≥ₛ bv2 + +def GoodNFA.autSignedCmpSA (q : NFA.signedCmpState) : BVRel := + match q with + | .eq => fun _ bv1 bv2 => bv1 = bv2 + | .lt => fun _ bv1 bv2 => bv1 <ᵤ bv2 + | .gt => fun _ bv1 bv2 => bv1 >ᵤ bv2 + | .ltfin => fun _ bv1 bv2 => bv1 <ₛ bv2 + | .gtfin => fun _ bv1 bv2 => bv1 >ₛ bv2 + +-- TODO: why is it BitVec.toInt_inj but its BitVec.toNat_eq? + +lemma BitVec.sle_iff_slt_or_eq {w : ℕ} (bv1 bv2 : BitVec w): + (bv2 ≥ₛ bv1) = true ↔ (bv2 >ₛ bv1) = true ∨ bv1 = bv2 := by + simp [BitVec.sle, BitVec.slt, le_iff_lt_or_eq, BitVec.toInt_inj] + +theorem Nat.add_lt_is_or {a} (a_lt : a < 2^i) : + 2^i + a = 2^i ||| a := by + have _ := Nat.mul_add_lt_is_or a_lt 1 + simp_all -def NFA.autMsbSet : NFA (BitVec 1) := - let m := NFA.empty +@[simp] +lemma BitVec.cons_sgt_iff {w} {bv1 bv2 : BitVec w} : + (BitVec.cons b1 bv1 >ₛ BitVec.cons b2 bv2) ↔ + (if b1 = b2 then bv1 >ᵤ bv2 else b2) := by + simp [BitVec.slt, BitVec.toInt_eq_msb_cond] + have hbv1 := bv1.isLt + have hbv2 := bv2.isLt + cases b1 <;> cases b2 <;> simp [BitVec.ult, Nat.shiftLeft_eq] <;> + repeat rw [←Nat.add_lt_is_or (by assumption)] <;> simp [Nat.two_pow_succ] + · linarith [Nat.two_pow_succ w] -- why do I need to use `two_pow_succ` twice? + · linarith [Nat.two_pow_succ w] + · rw [←Nat.add_lt_is_or hbv1, ←Nat.add_lt_is_or hbv2] + apply Nat.add_lt_add_iff_left + +set_option maxHeartbeats 1000000 in +lemma GoodNFA.autSignedCmp_correct cmp : autSignedCmp cmp |>.correct2 autSignedCmpSA cmp.srel := by + let getState {w} (bv1 bv2 : BitVec w) : NFA.signedCmpState := + if bv1 >ᵤ bv2 then .gt else if bv2 >ᵤ bv1 then .lt else .eq + constructor <;> simp [NFA.autSignedCmp, autSignedCmp, autSignedCmpSA, AutoStructs.RelationOrdering.srel] + · cases cmp <;> simp [BitVec.sle_iff_slt_or_eq]; tauto + · rintro (_ | _ | _) <;> simp + · rintro (_ | _ | _) a w bv1 bv2 <;> simp [NFA.stepSet, NFA.unsignedCmpStep] + · constructor + · rintro ⟨i, hi⟩; cases i <;> fin_cases a <;> simp_all [NFA.signedCmpStep, instFinEnumBitVec_sSA] + · rintro ⟨_, _⟩; use .eq; simp; fin_cases a <;> simp [instFinEnumBitVec_sSA] at * <;> tauto + · constructor + · rintro ⟨i, hi⟩; cases i <;> fin_cases a <;> simp_all [NFA.signedCmpStep, instFinEnumBitVec_sSA] + · rintro _; fin_cases a <;> simp [NFA.signedCmpStep, instFinEnumBitVec_sSA] at * + · use .gt; simp_all + · use (getState bv1 bv2); simp [getState]; split_ifs <;> simp_all; apply ucmp_tricho <;> assumption + · use .gt; simp_all + · constructor + · rintro ⟨i, hi⟩; cases i <;> fin_cases a <;> simp_all [NFA.signedCmpStep, instFinEnumBitVec_sSA] + · rintro _; fin_cases a <;> simp [NFA.signedCmpStep, instFinEnumBitVec_sSA] at * + · use .lt; simp_all + · use (getState bv1 bv2); simp [getState]; split_ifs <;> simp_all; apply ucmp_tricho <;> assumption + · use .lt; simp_all + · constructor + · rintro ⟨i, hi⟩; cases i <;> fin_cases a <;> simp_all [NFA.signedCmpStep, instFinEnumBitVec_sSA] + · rintro _; fin_cases a <;> simp [NFA.signedCmpStep, instFinEnumBitVec_sSA] at * + · use .lt; simp_all + · use (getState bv1 bv2); simp [getState]; split_ifs <;> simp_all; apply ucmp_tricho <;> assumption + · use .lt; simp_all + · constructor + · rintro ⟨i, hi⟩; cases i <;> fin_cases a <;> simp_all [NFA.signedCmpStep, instFinEnumBitVec_sSA] + · rintro _; fin_cases a <;> simp [NFA.signedCmpStep, instFinEnumBitVec_sSA] at * + · use .gt; simp_all + · use (getState bv1 bv2); simp [getState]; split_ifs <;> simp_all; apply ucmp_tricho <;> assumption + · use .gt; simp_all + +def CNFA.autMsbSet' : CNFA (BitVec 1) := + let m := CNFA.empty let (si, m) := m.newState let (sf, m) := m.newState let m := m.addInitial si let m := m.addFinal sf let m := m.addTrans 1 si sf let m := m.addManyTrans [0, 1] si si - m.determinize + m + +def GoodCNFA.autMsbSet : GoodCNFA 1 := + ⟨CNFA.autMsbSet', by sorry⟩ + +inductive NFA.msbState : Type where +| i | f + +def NFA.msbStep (q : NFA.msbState) (a : BitVec 1) : Set NFA.msbState := + match q, a with + | .i, 0 => {.i} + | .i, 1 => {.i, .f} + | _, _ => ∅ + +def NFA.msb : NFA (BitVec 1) msbState where + step := msbStep + start := {.i} + accept := {.f} + +def GoodNFA.autMsbSet : GoodNFA 1 := ⟨_, NFA.msb⟩ + +def NFA.msbLang : Language (BitVec 1) := { bvs | bvs.getLast? = some 1 } + +def NFA.msbSA (q : msbState) : Language (BitVec 1) := + match q with + | .i => ⊤ + | .f => msbLang + +-- TODO: rewrite with the n-ary `correct` predicate! +def NFA.msbCorrect : msb.correct msbSA msbLang := by + constructor + · simp [msb, msbSA] + · intros w; induction w using List.list_reverse_induction + case base => + simp [msb, msbSA, msbLang]; intros q; cases q <;> simp + case ind w a ih => + have h : msb.eval w = { q | w ∈ msbSA q } := by ext; simp [ih] + simp [h]; rintro (_ | _) + · simp [msb, msbSA, msbLang, stepSet, msbStep] + use .i; simp; fin_cases a <;> simp [instFinEnumBitVec_sSA] + · simp [msb, msbSA, msbLang, stepSet, msbStep]; constructor + · intro ⟨q, hq⟩; fin_cases a <;> simp [instFinEnumBitVec_sSA] at * + cases q <;> simp_all + · rintro rfl; use .i; simp + +lemma GoodCNFA.autMsbSet_spec : GoodCNFA.autMsbSet.Sim GoodNFA.autMsbSet := by + sorry + +@[simp] +lemma autMsbSet_accepts : GoodNFA.autMsbSet.accepts = langMsb := by + simp [GoodNFA.accepts, GoodNFA.accepts', GoodNFA.autMsbSet] + rw [NFA.correct_spec NFA.msbCorrect, NFA.msbLang] + ext bvs; simp only [BitVec.ofNat_eq_ofNat, Set.mem_image, Set.mem_setOf_eq] + constructor + · rintro ⟨bvs', hl, heq⟩ + have _ : bvs'.length ≠ 0 := by cases bvs'; tauto; simp + rw [←heq] + simp [dec] + rw [BitVec.msb_eq_getLsbD_last] + rw [BitVec.ofFn_getLsbD' _ _ (by omega)] + simp + rw [List.getLast?_eq_getElem?] at hl + rw [List.getElem?_eq_getElem (by omega)] at hl + injection hl + simp_all only [BitVec.getLsbD_one, zero_lt_one, decide_true, Bool.and_self] + · intros h; use enc bvs + simp only [dec_enc', and_true] + simp [enc] + have hw : bvs.w ≠ 0 := by + rcases bvs with ⟨w, bvs⟩; rintro rfl + simp_all [BitVec.eq_nil (bvs.head)] + use ⟨bvs.w - 1, by omega⟩ + simp; rw [List.getLast?_eq_getElem?] + simp; constructor + · rw [List.getElem?_eq_getElem (by simp; omega)]; simp + · ext; rw [BitVec.ofFn_getLsbD' _ _ (by omega)] + rw [BitVec.msb_eq_getLsbD_last] at h + simp [←BitVec.getLsbD_eq_getElem] + exact h end nfas_relations --- A bunch of maps from `Fin n` to `Fin m` that we use to --- lift and project variables when we interpret formulas -def liftMaxSucc1 (n m : Nat) : Fin (n + 1) → Fin (max n m + 2) := - fun k => if _ : k = n then Fin.last (max n m) else k.castLE (by omega) -def liftMaxSucc2 (n m : Nat) : Fin (m + 1) → Fin (max n m + 2) := - fun k => if _ : k = m then Fin.last (max n m + 1) else k.castLE (by omega) -def liftLast2 n : Fin 2 → Fin (n + 2) -| 0 => n -| 1 => n + 1 -def liftExcecpt2 n : Fin n → Fin (n + 2) := - fun k => Fin.castLE (by omega) k -def liftMax1 (n m : Nat) : Fin n → Fin (max n m) := - fun k => k.castLE (by omega) -def liftMax2 (n m : Nat) : Fin m → Fin (max n m) := - fun k => k.castLE (by omega) - --- TODO(leo): style? upstream? +def AutoStructs.Relation.autOfRelation : Relation → GoodCNFA 2 +| .eq => GoodCNFA.autEq +| .signed ord => GoodCNFA.autSignedCmp ord +| .unsigned ord => GoodCNFA.autUnsignedCmp ord + +def AutoStructs.Relation.absAutOfRelation (rel : Relation) : GoodNFA 2 := + match rel with + | .eq => GoodNFA.autEq + | .unsigned cmp => GoodNFA.autUnsignedCmp cmp + | .signed cmp => GoodNFA.autSignedCmp cmp + +lemma autOfRelation_spec (r : AutoStructs.Relation) : + r.autOfRelation.Sim r.absAutOfRelation := by + sorry + @[simp] -lemma finEnumCardFin n : FinEnum.card (Fin n) = n := by - rw [FinEnum.card, FinEnum.fin, FinEnum.ofList, FinEnum.ofNodupList] - simp only - rw [List.Nodup.dedup] - · simp - · apply List.nodup_finRange - -def AutoStructs.Relation.autOfRelation : Relation → NFA (BitVec 2) -| .eq => NFA.autEq -| .signed ord => NFA.autSignedCmp ord -| .unsigned ord => NFA.autUnsignedCmp ord - -def unopNfa {A} [BEq A] [FinEnum A] [Hashable A] - (op : Unop) (m : NFA A) : NFA A := +lemma autOfRelation_accepts (r : AutoStructs.Relation) : + r.absAutOfRelation.accepts = r.language := by + simp [AutoStructs.Relation.absAutOfRelation] + rcases r with ⟨⟩ | ⟨cmp⟩ | ⟨cmp⟩ <;> simp + · rw [GoodNFA.correct2_spec GoodNFA.autEq_correct] + simp [langRel2, GoodNFA.eqRel, evalRelation] + · rw [GoodNFA.correct2_spec (GoodNFA.autSignedCmp_correct cmp)] + simp [langRel2, evalRelation, RelationOrdering.srel] + cases cmp <;> simp + · rw [GoodNFA.correct2_spec (GoodNFA.autUnsignedCmp_correct cmp)] + simp [langRel2, evalRelation, RelationOrdering.urel] + cases cmp <;> simp + +def unopNfa (op : Unop) (m : GoodCNFA n) : GoodCNFA n := match op with | .neg => m.neg --- TODO(leo) : why is the typchecking so slow? -def binopNfa {A} [BEq A] [FinEnum A] [Hashable A] - (op : Binop) (m1 : NFA A) (m2 : NFA A) : NFA A := +def unopAbsNfa (op : Unop) (M : GoodNFA n) : GoodNFA n := + match op with + | .neg => M.neg + +lemma unopNfa_spec (op : Unop) (m : GoodCNFA n) (M : GoodNFA n) : + m.Sim M → (unopNfa op m).Sim (unopAbsNfa op M) := by + rcases op with ⟨⟩ + intros hsim + apply GoodCNFA.neg_spec; assumption + +def binopNfa (op : Binop) (m1 m2 : GoodCNFA n) : GoodCNFA n := match op with | .and => m1.inter m2 | .or => m1.union m2 | .impl => m1.neg.union m2 | .equiv => (m1.neg.union m2).inter (m2.neg.union m1) +def binopAbsNfa (op : Binop) (M1 M2: GoodNFA n) : GoodNFA n := + match op with + | .and => M1.inter M2 + | .or => M1.union M2 + | .impl => M1.neg.union M2 + | .equiv => (M1.neg.union M2).inter (M2.neg.union M1) --- TODO(leo) : why is it so slow? 40 seconds on my machine --- the slow part is the compilation apparently -def nfaOfFormula (φ : Formula) : NFA (BitVec φ.arity) := +def nfaOfFormula (φ : Formula) : GoodCNFA φ.arity := match φ with | .atom rel t1 t2 => - let m1 := (termEvalEqFSM t1).toFSM |> NFA.ofFSM - let m2 := (termEvalEqFSM t2).toFSM |> NFA.ofFSM + let m1 := FSM.ofTerm t1 |> GoodCNFA.ofFSM + let m2 := FSM.ofTerm t2 |> GoodCNFA.ofFSM let f1 := liftMaxSucc1 (FinEnum.card $ Fin t1.arity) (FinEnum.card $ Fin t2.arity) let m1' := m1.lift f1 let f2 := liftMaxSucc2 (FinEnum.card $ Fin t1.arity) (FinEnum.card $ Fin t2.arity) let m2' := m2.lift f2 let meq := rel.autOfRelation.lift $ liftLast2 (max (FinEnum.card (Fin t1.arity)) (FinEnum.card (Fin t2.arity))) - let m := NFA.inter m1' m2' |> NFA.inter meq - let mfinal := m.proj (liftExcecpt2 _) - have h : (Formula.atom .eq t1 t2).arity = max (FinEnum.card (Fin t1.arity)) (FinEnum.card (Fin t2.arity)) := by simp [FinEnum.card] - h ▸ mfinal + let m := GoodCNFA.inter m1' m2' |> GoodCNFA.inter meq + let mfinal := m.proj (liftExcept2 _) + mfinal | .msbSet t => - let m := (termEvalEqFSM t).toFSM |> NFA.ofFSM - let mMsb := NFA.autMsbSet.lift $ fun _ => Fin.last t.arity - have h : t.arity + 1 = FinEnum.card (Fin t.arity) + 1 := by - simp [FinEnum.card] - let m : NFA (BitVec (t.arity + 1)) := h.symm ▸ m + let m := (termEvalEqFSM t).toFSM |> GoodCNFA.ofFSM + let mMsb := GoodCNFA.autMsbSet.lift $ fun _ => Fin.last t.arity let res := m.inter mMsb - res.proj $ fun n => n.castLE (by rw [Formula.arity]; omega) + res.proj $ fun n => n.castLE (by simp [Formula.arity, FinEnum.card]) | .unop op φ => unopNfa op (nfaOfFormula φ) | .binop op φ1 φ2 => let m1 := (nfaOfFormula φ1).lift $ liftMax1 φ1.arity φ2.arity let m2 := (nfaOfFormula φ2).lift $ liftMax2 φ1.arity φ2.arity binopNfa op m1 m2 +def absNfaOfFormula (φ : Formula) : GoodNFA φ.arity := + match φ with + | .atom rel t1 t2 => + let m1 := FSM.ofTerm t1 |> GoodNFA.ofFSM + let m2 := FSM.ofTerm t2 |> GoodNFA.ofFSM + let f1 := liftMaxSucc1 (FinEnum.card $ Fin t1.arity) (FinEnum.card $ Fin t2.arity) + let m1' := m1.lift f1 + let f2 := liftMaxSucc2 (FinEnum.card $ Fin t1.arity) (FinEnum.card $ Fin t2.arity) + let m2' := m2.lift f2 + let meq := rel.absAutOfRelation.lift $ liftLast2 (max (FinEnum.card (Fin t1.arity)) (FinEnum.card (Fin t2.arity))) + let m := GoodNFA.inter m1' m2' |> GoodNFA.inter meq + let mfinal := m.proj (liftExcept2 _) + mfinal + | .msbSet t => + let m := (termEvalEqFSM t).toFSM |> GoodNFA.ofFSM + let mMsb := GoodNFA.autMsbSet.lift $ fun _ => Fin.last t.arity + let res := m.inter mMsb + res.proj $ fun n => n.castLE (by simp [Formula.arity, FinEnum.card]) + | .unop op φ => unopAbsNfa op (absNfaOfFormula φ) + | .binop op φ1 φ2 => + let m1 := (absNfaOfFormula φ1).lift $ liftMax1 φ1.arity φ2.arity + let m2 := (absNfaOfFormula φ2).lift $ liftMax2 φ1.arity φ2.arity + binopAbsNfa op m1 m2 + +lemma nfaOfFormula_spec φ : (nfaOfFormula φ).Sim (absNfaOfFormula φ) := by + induction φ <;> unfold nfaOfFormula absNfaOfFormula <;> simp + case atom rel t1 t2 => + apply GoodCNFA.proj_spec + apply GoodCNFA.inter_spec + apply GoodCNFA.lift_spec; apply autOfRelation_spec + apply GoodCNFA.inter_spec + apply GoodCNFA.lift_spec; apply GoodCNFA.ofFSM_spec + apply GoodCNFA.lift_spec; apply GoodCNFA.ofFSM_spec + case msbSet t => + apply GoodCNFA.proj_spec + apply GoodCNFA.inter_spec + · apply GoodCNFA.ofFSM_spec + · apply GoodCNFA.lift_spec + apply GoodCNFA.autMsbSet_spec + case unop op φ ih => + rcases op; simp [unopNfa, unopAbsNfa] + apply GoodCNFA.neg_spec + assumption + case binop op φ1 φ2 ih1 ih2 => + rcases op; simp [binopNfa, binopAbsNfa] + · apply GoodCNFA.inter_spec + apply GoodCNFA.lift_spec; assumption + apply GoodCNFA.lift_spec; assumption + · apply GoodCNFA.union_spec + apply GoodCNFA.lift_spec; assumption + apply GoodCNFA.lift_spec; assumption + · apply GoodCNFA.union_spec + · apply GoodCNFA.neg_spec + apply GoodCNFA.lift_spec; assumption + · apply GoodCNFA.lift_spec; assumption + · apply GoodCNFA.inter_spec <;> + · apply GoodCNFA.union_spec + · apply GoodCNFA.neg_spec + apply GoodCNFA.lift_spec; assumption + · apply GoodCNFA.lift_spec; assumption + +lemma absNfaToFomrmula_spec (φ : Formula) : + (absNfaOfFormula φ).accepts = φ.language := by + induction φ + case atom rel t1 t2 => + simp [absNfaOfFormula, binopAbsNfa]; ac_nf + case msbSet t => + simp [absNfaOfFormula] + case unop op φ ih => + simp [absNfaOfFormula, unopAbsNfa, ih] + case binop op φ1 φ2 ih1 ih2 => + rcases op <;> simp [absNfaOfFormula, binopAbsNfa, langBinop, ih1, ih2] + +/-- +The theorem stating that the automaton generated from the formula φ recognizes +exactly the solution of φ. +-/ +theorem absNfaToFomrmula_spec' (φ : Formula) : + (absNfaOfFormula φ).accepts = { (bvs : BitVecs φ.arity) | φ.sat (fun k => bvs.bvs.get k) = true } := by + simp [absNfaToFomrmula_spec, formula_language] + +/-- +info: 'absNfaToFomrmula_spec'' depends on axioms: [propext, Classical.choice, Quot.sound] +-/ +#guard_msgs in #print axioms absNfaToFomrmula_spec' /- Note: it is important to define this function and not inline it, otherwise each call to the tactic will compile a new function, which takes ~350ms on -my machine. -- Leo +my machine. -/ def formulaIsUniversal (f : Formula) : Bool := let m := nfaOfFormula f - m.isUniversal' - --- This is wrong, this is (hopefuly) true only for `w > 0` -axiom decision_procedure_is_correct {w} (φ : Formula) (env : Nat → BitVec w) : - formulaIsUniversal φ → φ.sat' env + m.isUniversal + +theorem decision_procedure_is_correct {w} (φ : Formula) (env : Nat → BitVec w) : + formulaIsUniversal φ → φ.sat' env := by + unfold formulaIsUniversal; simp + intros h; apply GoodCNFA.isUniversal_spec (nfaOfFormula_spec φ) at h + rw [absNfaToFomrmula_spec, formula_language] at h + rw [←sat_impl_sat'] + have hx := env_to_bvs φ (fun k => env k.val) + extract_lets bvs at hx + suffices hin : bvs ∈ (⊤ : Set _) by + rw [←h] at hin + simp [Set.instMembership, Set.Mem] at hin; assumption + simp -- -- For testing the comparison operators. --- def nfaOfCompareConstants (signed : Bool) {w : Nat} (a b : BitVec w) : NFA (BitVec 0) := --- let m1 := NFA.ofConst a --- let m2 := NFA.ofConst b +-- def nfaOfCompareConstants (signed : Bool) {w : Nat} (a b : BitVec w) : CNFA (BitVec 0) := +-- let m1 := CNFA.ofConst a +-- let m2 := CNFA.ofConst b -- let f1 : Fin 1 → Fin 2 := fun 0 => 0 -- let m1' := m1.lift f1 -- let f2 : Fin 1 → Fin 2 := fun 0 => 1 -- let m2' := m2.lift f2 --- let meq := if signed then NFA.autSignedCmp .lt else NFA.autUnsignedCmp .lt --- let m := NFA.inter m1' m2' |> NFA.inter meq +-- let meq := if signed then CNFA.autSignedCmp .lt else CNFA.autUnsignedCmp .lt +-- let m := CNFA.inter m1' m2' |> CNFA.inter meq -- let mfinal := m.proj (liftExcecpt2 _) -- mfinal @@ -265,22 +950,22 @@ axiom decision_procedure_is_correct {w} (φ : Formula) (env : Nat → BitVec w) -- let bv := BitVec.ofNat w n -- let bv' := BitVec.ofNat w m -- if (if signed then bv <ₛ bv' else bv <ᵤ bv') == --- (nfaOfCompareConstants signed bv bv' |> NFA.isNotEmpty) +-- (nfaOfCompareConstants signed bv bv' |> CNFA.isNotEmpty) -- then none else some (bv, bv') -- /-- info: true -/ -- #guard_msgs in #eval! (testLeq true 4 == none) --- def nfaOfMsb {w : Nat} (a : BitVec w) : NFA (BitVec 0) := --- let m := NFA.ofConst a --- let meq := NFA.autMsbSet --- let m := m |> NFA.inter meq +-- def nfaOfMsb {w : Nat} (a : BitVec w) : CNFA (BitVec 0) := +-- let m := CNFA.ofConst a +-- let meq := CNFA.autMsbSet +-- let m := m |> CNFA.inter meq -- let mfinal := m.proj $ fun _ => 0 -- mfinal -- def testMsb (w : Nat) : Bool := -- (List.range (2^w)).all fun n => -- let bv := BitVec.ofNat w n --- (bv.msb == true) == (nfaOfMsb bv |> NFA.isNotEmpty) +-- (bv.msb == true) == (nfaOfMsb bv |> CNFA.isNotEmpty) -- /-- info: true -/ -- #guard_msgs in #eval! testMsb 8 @@ -291,7 +976,7 @@ axiom decision_procedure_is_correct {w} (φ : Formula) (env : Nat → BitVec w) -- Formula.atom .eq (neg x) (not $ sub x 1) -- /-- info: true -/ --- #guard_msgs in #eval! nfaOfFormula ex_formula_neg_eq_neg_not_one |> NFA.isUniversal +-- #guard_msgs in #eval! nfaOfFormula ex_formula_neg_eq_neg_not_one |> CNFA.isUniversal -- -- x &&& ~~~ y = x - (x &&& y) -- def ex_formula_and_not_eq_sub_add : Formula := @@ -300,7 +985,7 @@ axiom decision_procedure_is_correct {w} (φ : Formula) (env : Nat → BitVec w) -- let y := var 1 -- Formula.atom .eq (and x (not y)) (sub x (and x y)) -- /-- info: true -/ --- #guard_msgs in #eval! nfaOfFormula ex_formula_and_not_eq_sub_add |> NFA.isUniversal +-- #guard_msgs in #eval! nfaOfFormula ex_formula_and_not_eq_sub_add |> CNFA.isUniversal -- /- x &&& y ≤ᵤ ~~~(x ^^^ y) -/ -- def ex_formula_and_ule_not_xor : Formula := @@ -310,7 +995,7 @@ axiom decision_procedure_is_correct {w} (φ : Formula) (env : Nat → BitVec w) -- .atom (.unsigned .le) (.and x y) (.not (.xor x y)) -- /-- info: true -/ --- #guard_msgs in #eval! nfaOfFormula ex_formula_and_ule_not_xor |> NFA.isUniversal +-- #guard_msgs in #eval! nfaOfFormula ex_formula_and_ule_not_xor |> CNFA.isUniversal -- -- Only true for `w > 0`! -- -- x = 0 ↔ (~~~ (x ||| -x)).msb @@ -322,7 +1007,7 @@ axiom decision_procedure_is_correct {w} (φ : Formula) (env : Nat → BitVec w) -- (.msbSet (.not (.or x (.neg x)))) -- /-- info: true -/ --- #guard_msgs in #eval! nfaOfFormula ex_formula_eq_zero_iff_not_or_sub |> NFA.isUniversal' +-- #guard_msgs in #eval! nfaOfFormula ex_formula_eq_zero_iff_not_or_sub |> CNFA.isUniversal' -- -- (x <ₛ 0) ↔ x.msb := by -- def ex_formula_lst_iff : Formula := @@ -333,4 +1018,4 @@ axiom decision_procedure_is_correct {w} (φ : Formula) (env : Nat → BitVec w) -- (.msbSet x) -- /-- info: true -/ --- #guard_msgs in #eval! nfaOfFormula ex_formula_lst_iff |> NFA.isUniversal +-- #guard_msgs in #eval! nfaOfFormula ex_formula_lst_iff |> CNFA.isUniversal diff --git a/SSA/Experimental/Bits/AutoStructs/GoodNFA.lean b/SSA/Experimental/Bits/AutoStructs/GoodNFA.lean new file mode 100644 index 000000000..c93ba16d7 --- /dev/null +++ b/SSA/Experimental/Bits/AutoStructs/GoodNFA.lean @@ -0,0 +1,94 @@ +import Batteries.Data.Fin.Basic +import Mathlib.Computability.NFA +import Mathlib.Data.FinEnum +import Mathlib.Data.Vector.Basic +import Mathlib.Data.Vector.Defs +import SSA.Experimental.Bits.AutoStructs.ForLean +import SSA.Experimental.Bits.AutoStructs.ForMathlib + +structure GoodNFA (n : Nat) where + σ : Type + M : NFA (BitVec n) σ + -- all reachable? complete? etc + +namespace GoodNFA + +/-- +The encoded tuples of bit vectors accepted by an automaton. +-/ +def accepts' (M : GoodNFA n) : Set (BitVecs' n) := M.M.accepts + +/-- +The tuples of bit vectors accepted by an automaton. +-/ +def accepts (M : GoodNFA n) : Set (BitVecs n) := dec '' M.accepts' + + +noncomputable def complete (M : GoodNFA n) : GoodNFA n where + σ := _ + M := M.M.complete + + +def product (final? : Prop → Prop → Prop) (M N : GoodNFA n) : GoodNFA n where + σ := _ + M := M.M.product final? N.M + +def inter (M N : GoodNFA n) : GoodNFA n := ⟨_, M.M.inter N.M⟩ + +lemma inter_eq (M N : GoodNFA n) : M.inter N = GoodNFA.product And M N := by + simp [inter, product, NFA.inter] + +@[simp] +lemma inter_accepts (M N : GoodNFA n) : + (M.inter N).accepts = M.accepts ∩ N.accepts := by + simp [accepts, accepts', inter, Set.image_inter dec_inj] + +def union (M N : GoodNFA n) : GoodNFA n := ⟨_, M.M.union N.M⟩ + +lemma union_eq (M N : GoodNFA n) : M.union N = GoodNFA.product Or M.complete N.complete := by + simp [union, product, NFA.union, NFA.union', complete] + +@[simp] +lemma union_accepts (M N : GoodNFA n) : + (M.union N).accepts = M.accepts ∪ N.accepts := by + simp [accepts, accepts', union]; rw [Set.image_union] + +def neg (M : GoodNFA n) : GoodNFA n where + σ := _ + M := M.M.neg + +@[simp] +lemma neg_accepts (M : GoodNFA n) : + M.neg.accepts = M.acceptsᶜ:= by + simp [accepts, accepts', neg, Set.image_compl_eq (dec_bij)] + +def reduce (M : GoodNFA n) : GoodNFA n where + σ := _ + M := M.M.reduce + +@[simp] +lemma reduce_accepts {M : GoodNFA n} : M.reduce.accepts = M.accepts := by + simp [reduce, accepts, accepts'] + + +def determinize (M : GoodNFA n) : GoodNFA n where + σ := _ + M := M.M.toDFA.toNFA + +def lift (f : Fin n → Fin m) (M : GoodNFA n) : GoodNFA m where + σ := _ + M := M.M.lift f + +def proj (f : Fin m → Fin n) (M : GoodNFA n) : GoodNFA m where + σ := _ + M := M.M.proj f + +@[simp] +lemma lift_accepts (M : GoodNFA n) (f : Fin n → Fin m) : + (M.lift f).accepts = BitVecs.transport f ⁻¹' M.accepts := by + simp [accepts, accepts', lift] + +@[simp] +lemma proj_accepts (M : GoodNFA m) (f : Fin n → Fin m) : + (M.proj f).accepts = BitVecs.transport f '' M.accepts := by + simp [accepts, accepts', proj] diff --git a/SSA/Experimental/Bits/AutoStructs/Tactic.lean b/SSA/Experimental/Bits/AutoStructs/Tactic.lean index 63ce0a049..c90581afd 100644 --- a/SSA/Experimental/Bits/AutoStructs/Tactic.lean +++ b/SSA/Experimental/Bits/AutoStructs/Tactic.lean @@ -112,8 +112,6 @@ def AutoStructs.Term.toExpr (t : Term) : Expr := | .sub t1 t2 => mkApp2 (mkConst ``sub) t1.toExpr t2.toExpr | .not t => mkApp (mkConst ``Term.not) t.toExpr | .neg t => mkApp (mkConst ``neg) t.toExpr - | .incr t => mkApp (mkConst ``incr) t.toExpr - | .decr t => mkApp (mkConst ``decr) t.toExpr def AutoStructs.Relation.toExpr (rel : Relation) : Expr := open Relation in @@ -174,13 +172,13 @@ def addAsVar (e : Expr) : M AutoStructs.Term := do set ({varMap, invMap } : State) pure (.var v) --- TODO(leo): make this work +-- TODO: make this work def checkBVs (es : List Expr) : M Bool := do for e in es do let_expr BitVec _ := e | return false pure true --- TODO(leo): make the shortcuts better +-- TODO: make the shortcuts better partial def parseTerm (e : Expr) : M AutoStructs.Term := do match_expr e with | OfNat.ofNat α n _ => @@ -368,7 +366,6 @@ elab "bv_automata_inner" : tactic => do let (φ, st) ← parseFormula e|>.run default assertSame φ st --- TODO(leo): make the tactic more structured (in Coq `bv_inner; [by simp | by ...]) macro "bv_automata'" : tactic => `(tactic| ( bv_automata_inner @@ -409,8 +406,21 @@ theorem ult_iff_not_ule : (x <ᵤ y) ↔ ¬ (y ≤ᵤ x) := by bv_automata' theorem sub_neg_sub : (x - y) = - (y - x) := by bv_automata' -theorem eq_iff_not_sub_or_sub : - x = y ↔ (~~~ (x - y ||| y - x)).msb := by bv_automata' +-- only for w > 0 +-- theorem eq_iff_not_sub_or_sub : +-- x = y ↔ (~~~ (x - y ||| y - x)).msb := by bv_automata' + +theorem zulip_example : + ¬(n <ᵤ ~~~k) ∨ + (((a + k - a <ᵤ a + k + 1#64 - a) ∧ (a + k - a <ᵤ a + k + 1#64 + n - a)) ∧ + a + k + 1#64 + n - (a + k + 1#64) <ᵤ a - (a + k + 1#64)) ∧ + a + k + 1#64 + n - (a + k + 1#64) <ᵤ a + k - (a + k + 1#64) := by + bv_automata' + +theorem zulip_example' : + ¬(n <ᵤ ~~~k) ∨ + (((k <ᵤ k + 1) ∧ (k <ᵤ k + 1 + n)) ∧ n <ᵤ -k - 1) ∧ n <ᵤ -1 := by + bv_automata' theorem lt_iff_sub_xor_xor_and_sub_xor : (x <ₛ y) ↔ ((x - y) ^^^ ((x ^^^ y) &&& ((x - y) ^^^ x))).msb := by