Replaced some cases instances with grind

InductiveVerification/Event.lean

@@ -15,6 +15,7 @@ class HasInitState (α : Type) where
 variable [ hasInitStateAgent : HasInitState Agent ]
   
 open HasInitState
+attribute [simp] initState
   
 -- Define the `bad` set
 abbrev DecidableMem ( A : Set Agent ) := (a : Agent) →  Decidable (a ∈ A)
@@ -27,8 +28,8 @@ class Bad where
 instance [Bad] : DecidableMem Bad.bad := Bad.decidableBad
 open Bad
 
--- attribute [simp] Spy_in_bad
+attribute [simp, grind .] Spy_in_bad
--- attribute [simp] Server_not_bad
+attribute [simp] Server_not_bad
 
 instance decidableAgentEq : DecidableEq Agent :=
   λ a b =>
@@ -61,8 +62,11 @@ def knows [Bad] : Agent → List Event → Set Msg
 | A, Event.Notes A' X :: evs =>
   if A = A' then insert X (knows A evs) else knows A evs
   
+attribute [simp] knows
+
 -- Define the `spies` abbreviation
 abbrev spies (evs : List Event) [Bad] : Set Msg := knows Agent.Spy evs
+attribute [simp] spies
 
 -- Define the `used` function
 def used : List Event → Set Msg
@@ -172,6 +176,7 @@ lemma Notes_imp_knows_Spy [Bad] {A : Agent} {X : Msg} {evs : List Event} :
 
 -- Elimination rules: derive contradictions from old Says events containing
 -- items known to be fresh
+@[grind ., grind! .]
 lemma Says_imp_parts_knows_Spy [Bad] :
   ∀ {A B : Agent} {X : Msg} {evs : List Event},
     Event.Says A B X ∈ evs → X ∈ parts (knows Agent.Spy evs) := by
@@ -364,6 +369,7 @@ lemma knows_Spy_imp_Says_Notes_initState [Bad] {X : Msg} {evs : List Event} :
       · apply ih at h; aapply knows_Spy_imp_Says_Notes_initState_aux
 
 -- Parts of what the Spy knows are a subset of what is used
+@[grind! .]
 lemma parts_knows_Spy_subset_used [Bad] :
     parts (knows Agent.Spy evs) ⊆ used evs := by
   induction evs with

InductiveVerification/Message.lean

@@ -604,6 +604,12 @@ by
   | snd h ih => exact analz.snd ih
   | decrypt h₁ h₂ ih₁ ih₂ => exact analz.decrypt ih₁ ih₂
 
+@[grind .]
+lemma analz_insert_mono [InvKey] :
+  X ∈ analz H → X ∈ analz (insert Y H)
+:= by
+  apply_rules [ analz_mono, Set.subset_insert]
+
 lemma analz_mono_neg [InvKey] { h : A ⊆ B } :
   X ∉ analz B → X ∉ analz A
 := by
@@ -624,7 +630,7 @@ by
   · apply analz.fst h
   · apply analz.snd h
 
-@[simp]
+@[simp, grind! .]
 lemma analz_increasing [InvKey] {H : Set Msg} : H ⊆ analz H :=
   λ _ hx => analz.inj hx
 
@@ -637,6 +643,7 @@ by
   | snd _ ih => aapply parts.snd
   | decrypt _ _ ih₁ => aapply parts.body
 
+@[grind! .]
 lemma analz_subset_parts {H : Set Msg} [InvKey] : analz H ⊆ parts H :=
   λ _ hx => analz_into_parts hx
 
@@ -1628,5 +1635,3 @@ X ∈ A ∨ h₁ → X ∈ B ∨ h₁
   intro h; cases h <;> try simp_all
   left; aapply h
 
-attribute [-simp] Key.injEq
-

InductiveVerification/NS_Public.lean

@@ -40,75 +40,68 @@ theorem possibility_property :
   constructor
   · apply ns_public.NS3
     · apply ns_public.NS2
-      · apply_rules [ns_public.NS1, ns_public.Nil, Nonce_notin_used_empty]
+      · apply_rules[ns_public.NS1, ns_public.Nil, Nonce_notin_used_empty]
       · simp
       · tauto
     all_goals tauto
   · simp
 
 -- Spy never sees another agent's private key unless it's bad at the start
-@[simp]
+@[simp, grind =]
 theorem Spy_see_priEK {h : ns_public evs} :
   (Key (priEK A) ∈ parts (spies evs)) ↔ A ∈ bad := by
   constructor
   · induction h with
-    | Nil =>
+    | Nil => simp[priEK]
-      simp[spies, knows, initState, pubEK, priEK, pubSK]
+    | Fake _ h =>
-    | Fake _ h ih =>
       apply Fake_parts_sing at h
       intro h₁; simp at h₁; apply Fake_parts_sing_helper (h := h) at h₁
       simp_all
     | NS1 => simp_all
     | NS2 => simp_all
     | NS3 => simp_all
-  · intro h₁; apply parts_increasing; aapply Spy_spies_bad_privateKey
+  · intro _; apply_rules [ parts_increasing, Spy_spies_bad_privateKey ]
 
 @[simp]
 theorem Spy_analz_priEK {h : ns_public evs} :
-  Key (priEK A) ∈ analz (spies evs) ↔ A ∈ bad := by
+  Key (priEK A) ∈ analz (spies evs) ↔ A ∈ bad
-  constructor
+:= by grind
-  · intro h₁; apply analz_subset_parts at h₁; aapply Spy_see_priEK.mp
-  · intro h₁; apply analz_increasing; aapply Spy_spies_bad_privateKey
 
--- It is impossible to re-use a nonce in both NS1 and NS2, provided the nonce is secret
+-- It is impossible to re-use a nonce in both NS1 and NS2, provided the nonce is
+-- secret
+@[grind! .]
 theorem no_nonce_NS1_NS2 { evs: List Event} { h : ns_public evs  } :
   (Crypt (pubEK C) ⦃NA', Nonce NA, Agent D⦄ ∈ parts (spies evs) →
   (Crypt (pubEK B) ⦃Nonce NA, Agent A⦄ ∈ parts (spies evs) →
   Nonce NA ∈ analz (spies evs))) := by
   intro h₁ h₂
   induction h with
-  | Nil => simp[spies, knows] at h₂
+  | Nil => simp at h₂
-  | Fake _ h ih =>
+  | Fake _ h =>
-      simp; apply analz_insert;
+    simp [*] at *
     apply Fake_parts_sing at h
-      simp at h₁; apply Fake_parts_sing_helper (h := h) at h₁; simp at h₁
+    apply Fake_parts_sing_helper (h := h) at h₁
-      simp at h₂; apply Fake_parts_sing_helper (h := h) at h₂; simp at h₂
+    apply Fake_parts_sing_helper (h := h) at h₂
-      rcases h₁ with ((_ | _) | _) <;>
+    simp_all; grind
-      rcases h₂ with ((_ | _) | _) <;>
+  | NS1 =>
-      simp_all
-      all_goals (right; aapply ih <;> aapply analz_subset_parts)
-  | NS1 _ nonce_not_used =>
-    apply analz_spies_mono
     simp [*] at *
-    apply parts_knows_Spy_subset_used_neg at nonce_not_used;
     expand_parts_element at h₁; expand_parts_element at h₂;
-    cases h₂ <;> simp_all
+    grind
-  | NS2 _ nonce_not_used =>
+  | NS2 =>
-    apply analz_spies_mono
     simp [*] at *
-    apply parts_knows_Spy_subset_used_neg at nonce_not_used;
     expand_parts_element at h₂;
-    cases h₁ <;> simp_all[-Key.injEq]
+    grind
-  | NS3 _ _ _ a_ih => apply analz_spies_mono; simp_all
+  | NS3 => apply analz_spies_mono; simp_all
 
 -- Unicity for NS1: nonce NA identifies agents A and B
+@[grind! .]
 theorem unique_NA { h : ns_public evs } :
   (Crypt (pubEK B) ⦃Nonce NA, Agent A⦄ ∈ parts (spies evs) →
   (Crypt (pubEK B') ⦃Nonce NA, Agent A'⦄ ∈ parts (spies evs) →
   (Nonce NA ∉ analz (spies evs) →
   A = A' ∧ B = B'))) := by
   induction h with
-  | Nil => simp[spies, knows]
+  | Nil => simp
   | Fake _ a a_ih =>
     apply Fake_parts_sing at a; intro h₁ h₂ h₃;
     apply analz_spies_mono_neg at h₃;
@@ -116,18 +109,14 @@ theorem unique_NA { h : ns_public evs } :
     apply Fake_parts_sing_helper (h := a) at h₁
     apply Fake_parts_sing_helper (h := a) at h₂
     simp_all
-  | NS1 _ nonce_not_used a_ih =>
+  | NS1 =>
-    intro h₁ h₂ h₃
+    intro h₁ h₂ _; simp [*] at *
-    apply analz_insert_mono_neg at h₃
+    expand_parts_element at h₁; expand_parts_element at h₂; grind
-    simp [*] at *
+  | NS2 => intro _ _ _; simp_all; grind
-    expand_parts_element at h₁
+  | NS3 => intro _ _ _; simp_all; grind
-    expand_parts_element at h₂
-    apply parts_knows_Spy_subset_used_neg at nonce_not_used
-    cases h₁ <;> cases h₂ <;> simp_all
-  | NS2 => intro _ _ h₃; apply analz_insert_mono_neg at h₃; simp_all
-  | NS3 => intro _ _ h₃; apply analz_insert_mono_neg at h₃; simp_all;
 
 -- Spy does not see the nonce sent in NS1 if A and B are secure
+@[grind! .]
 theorem Spy_not_see_NA { h : ns_public evs  }
   { not_bad_A : A ∉ bad }
   { not_bad_B : B ∉ bad } :
@@ -136,37 +125,27 @@ theorem Spy_not_see_NA { h : ns_public evs  }
   intro h₁ h₄
   induction h with
   | Nil => simp_all
-  | Fake _ a =>
+  | Fake _ a => apply Fake_analz_insert at a; apply a at h₄; simp_all
-    have _ := Spy_in_bad; apply Fake_analz_insert at a; apply a at h₄; simp_all
+  | NS1 _ a =>
-  | NS1 _ a a_ih =>
     simp_all; rcases h₁ with (_ | h)
     · simp_all; apply a; aapply analz_knows_Spy_subset_used
     · apply analz_insert_Crypt_subset at h₄; simp at h₄; cases h₄ <;> simp_all
-      apply Says_imp_used at h; apply used_parts_subset_parts at h
+      apply Says_imp_used at h; apply used_parts_subset_parts at h;
       simp_all[Set.subset_def]
-  | NS2 _ not_used_NB a a_ih =>
+  | NS2 _ _ a a_ih =>
-    simp at h₁
+    simp [*] at *; have _ := h₄; have c := h₁
-    have _ := h₄
-    simp at h₄; apply analz_insert_Crypt_subset at h₄
-    simp at h₄; rcases h₄ with ( h | h | h)
-    · simp [*] at *; have c := h₁; apply a_ih at c;
-      have _ := c;
     apply Says_imp_parts_knows_Spy at h₁
-      apply Says_imp_parts_knows_Spy at a
+    have d := h₁
+    expand_parts_element at d
+    apply analz_insert_Crypt_subset at h₄; simp at h₄; rcases h₄ with (h |h |h)
+    <;> simp [*] at *;
+    · apply a_ih at c; have _ := c; apply Says_imp_parts_knows_Spy at a
       apply unique_NA at h₁; apply h₁ at a; apply a at c; all_goals simp_all
-    · simp_all
+    · grind
-      apply not_used_NB; apply parts_knows_Spy_subset_used; apply parts.fst;
+  | NS3 => apply analz_insert_Crypt_subset at h₄; simp[*] at h₄; grind
-      apply parts.body; apply Says_imp_parts_knows_Spy; assumption
-    · aapply a_ih
-  | NS3 _ _ a₂ a_ih =>
-    simp [*] at *
-    have _ := h₄
-    apply analz_insert_Crypt_subset at h₄; simp[*] at h₄;
-    have _ := h₁; simp[*] at h₁; apply Says_imp_parts_knows_Spy at h₁
-    apply Says_imp_parts_knows_Spy at a₂
-    aapply a_ih; apply no_nonce_NS1_NS2 <;> try simp [*] <;> assumption
 
--- Authentication for `A`: if she receives message 2 and has used `NA` to start a run, then `B` has sent message 2.
+-- Authentication for `A`: if she receives message 2 and has used `NA` to start
+-- a run, then `B` has sent message 2.
 theorem A_trusts_NS2 {h : ns_public evs }
   { not_bad_A : A ∉ bad }
   { not_bad_B : B ∉ bad } :
@@ -179,28 +158,19 @@ theorem A_trusts_NS2 {h : ns_public evs }
    -- use unique_NA to show that B' = B
    induction h with
   | Nil => simp_all
-  | Fake _ a a_ih =>
+  | Fake _ a =>
     have snsNA := h₁; apply Spy_not_see_NA at snsNA <;> try assumption
     apply analz_spies_mono_neg at snsNA
     simp [*] at *
     cases h₁
-    · have _ := Spy_in_bad; simp_all
+    · simp_all
     · apply Fake_parts_sing at a;
       apply Fake_parts_sing_helper (h := a) at h₂; simp at h₂
-      rcases h₂ with ((_ | _) | _) <;> (right; aapply a_ih)
+      grind
-      · aapply analz_subset_parts
-      · tauto
     · aapply ns_public.Fake
-  | NS1 _ a a_ih =>
+  | NS1 => simp [*] at *; expand_parts_element at h₂; grind
-    apply parts_knows_Spy_subset_used_neg at a;
+  | NS2 => simp [*] at *; grind
-    simp [*] at *; expand_parts_element at h₂; cases h₁ <;> simp_all
+  | NS3 => simp_all;
-  | NS2 _ _ a a_ih =>
-    simp [*] at *
-    have snsNA := h₁; apply Spy_not_see_NA at snsNA <;> try assumption
-    cases h₂ <;> simp_all
-    apply Says_imp_parts_knows_Spy at a; apply unique_NA at a;
-    apply Says_imp_parts_knows_Spy at h₁; apply a at h₁; all_goals simp_all
-  | NS3 _ _ a a_ih => simp_all;
 
 -- If the encrypted message appears then it originated with Alice in `NS1`
 lemma B_trusts_NS1 { h : ns_public evs} :
@@ -210,19 +180,19 @@ lemma B_trusts_NS1 { h : ns_public evs} :
 := by
   intro h₁ h₂
   induction h with
-  | Nil => simp[spies, knows] at h₁
+  | Nil => simp at h₁
-  | Fake _ a a_ih =>
+  | Fake _ a =>
     apply analz_spies_mono_neg at h₂
     simp at h₁; apply Fake_parts_sing at a;
     apply Fake_parts_sing_helper (h := a) at h₁; simp_all
-  | NS1 _ _ a_ih =>
+  | NS1 => apply analz_spies_mono_neg at h₂; simp_all; cases h₁ <;> simp_all
-    apply analz_spies_mono_neg at h₂; simp_all; cases h₁ <;> simp_all
+  | NS2 => apply analz_spies_mono_neg at h₂; simp_all;
-  | NS2 _ _ _ a_ih => apply analz_spies_mono_neg at h₂; simp_all;
+  | NS3 => apply analz_spies_mono_neg at h₂; simp_all;
-  | NS3 _ _ _ a_ih => apply analz_spies_mono_neg at h₂; simp_all;
 
 -- Authenticity Properties obtained from `NS2`
 
 -- Unicity for `NS2`: nonce `NB` identifies nonce `NA` and agent `A`
+@[grind! .]
 theorem unique_NB { h : ns_public evs } :
   (Crypt (pubEK A) ⦃Nonce NA, Nonce NB, Agent B⦄ ∈ parts (spies evs) →
   (Crypt (pubEK A') ⦃Nonce NA', Nonce NB, Agent B'⦄ ∈ parts (spies evs) →
@@ -230,30 +200,22 @@ theorem unique_NB { h : ns_public evs } :
   A = A' ∧ NA = NA' ∧ B = B'))) := by
   -- Proof closely follows that of unique_NA
   induction h with
-  | Nil => aesop (add norm spies, norm knows, safe analz_insertI)
+  | Nil => aesop (add safe analz_insertI)
-  | Fake _ a a_ih =>
+  | Fake _ a =>
     apply Fake_parts_sing at a; intro h₁ h₂ h₃; simp [*] at *
     apply Fake_parts_sing_helper (h := a) at h₁;
     apply Fake_parts_sing_helper (h := a) at h₂; simp [*] at *
     apply analz_insert_mono_neg at h₃
-    rcases h₁ with ((_ | _) | _) <;>
+    grind
-    rcases h₂ with ((_ | _) | _) <;>
+  | NS1 => intro _ _ h₃; apply analz_spies_mono_neg at h₃; simp_all
-    simp_all
+  | NS2 =>
-    all_goals (aapply a_ih; repeat aapply analz_subset_parts)
+    intro h₁ h₂ _; simp [*] at *
-  | NS1 _ _ a_ih => intro h₁ h₂ h₃; simp at h₁; simp at h₂; aapply a_ih
+    expand_parts_element at h₁; expand_parts_element at h₂
-                    aapply analz_spies_mono_neg
+    grind
-  | NS2 _ nonce_not_used _ a_ih =>
+  | NS3 => intro _ _ _; simp_all; grind
-    intro h₁ h₂ h₃; simp [*] at *
-    expand_parts_element at h₁
-    expand_parts_element at h₂
-    apply analz_insert_mono_neg at h₃;
-    apply parts_knows_Spy_subset_used_neg at nonce_not_used
-    rcases h₁ with (_ | h₁) <;>
-    rcases h₂ with (_ | h₂) <;> simp_all
-  | NS3 _ _ _ a_ih =>
-    intro h₁ h₂ h₃; apply analz_spies_mono_neg at h₃; simp_all[-Key.injEq]
 
 -- `NB` remains secret
+@[grind! .]
 theorem Spy_not_see_NB { h : ns_public evs }
   { not_bad_A : A ∉ bad }
   { not_bad_B : B ∉ bad } :
@@ -263,33 +225,27 @@ theorem Spy_not_see_NB { h : ns_public evs }
   intro h₁ h₄
   induction h with
   | Nil => simp_all
-  | Fake _ a a_ih =>
+  | Fake _ a => apply Fake_analz_insert at a; apply a at h₄; simp_all;
-    have _ := Spy_in_bad; apply Fake_analz_insert at a; apply a at h₄; simp_all;
+  | NS1 =>
-  | NS1 _ nonce_not_used a_ih =>
     simp [*] at *
     apply analz_insert_Crypt_subset at h₄; simp at h₄
-    apply parts_knows_Spy_subset_used_neg at nonce_not_used
     have h₂ := h₁; apply Says_imp_parts_knows_Spy at h₂
-    expand_parts_element at h₂; simp_all
+    expand_parts_element at h₂
-  | NS2 _ not_used_NB a a_ih =>
+    grind
+  | NS2 =>
     simp [*] at *
-    apply parts_knows_Spy_subset_used_neg at not_used_NB
+    have _ := h₄
+    apply analz_insert_Crypt_subset at h₄; simp at h₄
     rcases h₁ with (_ | h₁)
-    · simp_all; apply not_used_NB; aapply analz_subset_parts
+    · simp_all; grind
-    · apply analz_insert_Crypt_subset at h₄; simp at h₄; rcases h₄ with (_ |_ |_ )
+    · have _ := h₁; apply Says_imp_parts_knows_Spy at h₁
-      · aapply a_ih; apply Says_imp_parts_knows_Spy at a;
+      expand_parts_element at h₁; grind
-        apply Says_imp_parts_knows_Spy at h₁; simp_all; aapply no_nonce_NS1_NS2
+  | NS3 =>
-      · apply Says_imp_parts_knows_Spy at h₁;
-        expand_parts_element at h₁; simp_all
-      · aapply a_ih
-  | NS3 _ _ a a_ih =>
     simp at h₁; simp[analz_insert_Crypt_element] at h₄;
-    rcases h₄ with (⟨_, _⟩ | ⟨_, _⟩) <;> simp_all
+    rcases h₄ with (⟨_, _⟩ | ⟨_, _⟩) <;> simp_all; grind
-    apply Says_imp_parts_knows_Spy at a
-    apply Says_imp_parts_knows_Spy at h₁; apply unique_NB at a
-    apply a at h₁; apply h₁ at a_ih; simp_all; assumption
 
--- Authentication for `B`: if he receives message 3 and has used `NB` in message 2, then `A` has sent message 3.
+-- Authentication for `B`: if he receives message 3 and has used `NB` in message
+-- 2, then `A` has sent message 3.
 theorem B_trusts_NS3 { h : ns_public evs }
   { not_bad_A : A ∉ bad }
   { not_bad_B : B ∉ bad } :
@@ -301,28 +257,14 @@ theorem B_trusts_NS3 { h : ns_public evs }
   apply Says_imp_parts_knows_Spy at h₂
   induction h with
   | Nil => simp_all
-  | Fake _ a a_ih =>
+  | Fake _ a =>
     simp [*] at *
     apply Fake_parts_sing at a
     apply Fake_parts_sing_helper (h := a) at h₂; simp at h₂
-    expand_parts_element at h₂;
+    grind
-    rcases h₁ with (_ | h₁) <;>
-    rcases h₂ with ((h₂ | _) | _) <;> simp_all[Spy_in_bad]
-    · apply analz_subset_parts at h₂; simp_all
-    · apply Spy_not_see_NB at h₁ <;> simp_all
   | NS1 => simp_all
-  | NS2 _ nonce_not_used =>
+  | NS2 => simp [*] at *; expand_parts_element at h₂; grind
-    simp [*] at *
+  | NS3 => simp [*] at *; grind
-    apply parts_knows_Spy_subset_used_neg at nonce_not_used;
-    expand_parts_element at h₂; cases h₁ <;> simp_all
-  | NS3 _ _ a₂ =>
-    simp [*] at *;
-    expand_parts_element at h₂; cases h₂ <;> simp_all
-    have h₁c := h₁
-    apply Spy_not_see_NB at h₁c
-    apply Says_imp_parts_knows_Spy at h₁; apply unique_NB at h₁;
-    apply Says_imp_parts_knows_Spy at a₂; apply h₁ at a₂
-    all_goals simp_all
 
 -- Overall guarantee for `B`
 
@@ -337,29 +279,13 @@ theorem B_trusts_protocol { h : ns_public evs  }
   intro h₁ h₂
   induction h with
   | Nil => simp_all
-  | Fake _ a a_ih =>
+  | Fake _ a =>
     simp [*] at *
     apply Fake_parts_sing at a
-    apply Fake_parts_sing_helper (h := a) at h₁;
+    apply Fake_parts_sing_helper (h := a) at h₁; expand_parts_element at h₁
-    expand_parts_element at h₁
+    grind
-    rcases h₂ with (_ | h₂) <;> simp_all[Spy_in_bad]
-    rcases h₁ with (((_ |_ ) | _) | _)  <;> try simp_all
-    · right; aapply a_ih; aapply analz_subset_parts
-    · apply Spy_not_see_NB at h₂ <;> simp_all
   | NS1 => simp_all
-  | NS2 _ nonce_not_used a a_ih =>
+  | NS2 => simp [*] at *; expand_parts_element at h₁; grind
-    simp [*] at *
+  | NS3 => simp [*] at *; grind
-    apply parts_knows_Spy_subset_used_neg at nonce_not_used;
-    expand_parts_element at h₁; cases h₂ <;> simp_all
-  | NS3 _ _ a₂ a_ih =>
-    simp [*] at *
-    expand_parts_element at h₁
-    cases h₁ <;> simp_all
-    have h₂c := h₂
-    apply Spy_not_see_NB at h₂c
-    apply Says_imp_parts_knows_Spy at h₂
-    apply Says_imp_parts_knows_Spy at a₂
-    apply unique_NB at h₂; apply h₂ at a₂
-    apply a₂ at h₂c; all_goals simp_all
 
 end NS_Public

InductiveVerification/Public.lean

@@ -33,6 +33,11 @@ noncomputable abbrev priSK (A : Agent) : Key := privateKey KeyMode.Signature A
 noncomputable abbrev pubK (A : Agent) : Key := pubEK A
 noncomputable abbrev priK (A : Agent) : Key := invKey (pubEK A)
 
+attribute [simp] pubEK
+attribute [simp] pubSK
+-- attribute [simp] priEK
+-- attribute [simp] priSK
+
 -- Axioms for private and public keys
 @[simp]
 axiom privateKey_neq_publicKey {b c : KeyMode} {A A' : Agent} :
@@ -320,7 +325,7 @@ lemma priK_in_initState {b : KeyMode} {A : Agent} :
     Msg.Key (privateKey b A) ∈ initState A := by
   induction A <;>
   simp [HasInitState.initState, initState, privateKey, pubEK, pubSK] <;>
-  cases b <;> simp[Spy_in_bad]
+  cases b <;> simp
 
 @[simp]
 lemma publicKey_in_initState {b : KeyMode} {A : Agent} {B : Agent} :
@@ -344,6 +349,7 @@ lemma analz_spies_pubK : Msg.Key (publicKey b A) ∈ analz (spies evs) := by
   exact analz.inj spies_pubK
 
 -- Spy sees private keys of bad agents
+@[grind .]
 lemma Spy_spies_bad_privateKey { h : A ∈ bad } : Msg.Key (privateKey b A) ∈ spies evs := by
   induction evs with
   | nil => simp_all [spies, knows, pubSK, pubEK]; cases b <;> tauto

Main.lean

@@ -1,5 +1,5 @@
 -- import InductiveVerification
-import InductiveVerification.Public
+import InductiveVerification.NS_Public
 
 def main : IO Unit :=
   IO.println "Hello, world!"