Added expand_parts_element macro

Further simplified proofs in NS_public

InductiveVerification/Message.lean

@@ -1,5 +1,6 @@
 import Init.Data.Nat.Lemmas
 import Init.Prelude
+import Lean
 import Mathlib.Data.Nat.Basic
 import Mathlib.Data.Nat.Dist
 import Mathlib.Data.Set.Basic
@@ -12,6 +13,8 @@ import Mathlib.Order.Lattice
 import Mathlib.Tactic.ApplyAt
 import Mathlib.Tactic.SimpIntro
 import Mathlib.Tactic.NthRewrite
+open Lean Elab Command Term Meta
+open Parser.Tactic
 
 -- Keys are integers
 abbrev Key := Nat
@@ -351,6 +354,14 @@ lemma parts_element:
   · intro h; apply_rules [ parts_subset_iff.mp, Set.singleton_subset_iff.mpr ]
   · intro h; aapply parts_subset_iff.mpr; simp
 
+/--
+A tactic that expands terms like `X ∈ parts H`
+-/
+syntax (name := expandPartsElement) "expand_parts_element" (ppSpace location) : tactic
+macro_rules
+  | `(tactic| expand_parts_element at $loc) =>
+  `(tactic| rw[parts_element, Set.subset_def] at $loc; simp at $loc)
+
 @[simp]
 lemma parts_insert_Agent {H : Set Msg} {agt : Agent} :
   parts (insert (Agent agt) H) = insert (Agent agt) (parts H) :=
@@ -593,6 +604,16 @@ by
   | snd h ih => exact analz.snd ih
   | decrypt h₁ h₂ ih₁ ih₂ => exact analz.decrypt ih₁ ih₂
 
+lemma analz_mono_neg [InvKey] { h : A ⊆ B } :
+  X ∉ analz B → X ∉ analz A
+:= by
+  intro h₁ h₂; apply h₁; aapply analz_mono;
+  
+lemma analz_insert_mono_neg [InvKey] :
+  X ∉ analz (insert Y H) → X ∉ analz H
+:= by
+  apply_rules [ analz_mono_neg, Set.subset_insert ]
+
 -- Making it safe speeds up proofs
 -- @[simp]
 lemma MPair_analz {H : Set Msg} {X Y : Msg} {P : Prop} [InvKey] :
@@ -1597,3 +1618,15 @@ by
   apply subset_trans (b := parts (insert X H))
   · apply parts_mono; simp
   · aapply Fake_parts_insert
+  
+-- Often the result of Fake_parts_sing needs to be applied to a term in a
+-- disjunction
+lemma Fake_parts_sing_helper {A B : Set Msg}
+{ h : A ⊆ B } :
+X ∈ A ∨ h₁ → X ∈ B ∨ h₁
+:= by
+  intro h; cases h <;> try simp_all
+  left; aapply h
+
+attribute [-simp] Key.injEq
+

InductiveVerification/NS_Public.lean

@@ -46,15 +46,6 @@ theorem possibility_property :
     all_goals tauto
   · simp
 
--- Lemmata for some very specific recurring cases in the following proof
-omit [InvKey] [Bad] in
-lemma Fake_parts_sing_helper {A B : Set Msg}
-{ h : A ⊆ B } :
-X ∈ A ∨ h₁ → X ∈ B ∨ h₁
-:= by
-  intro h; cases h <;> try simp_all
-  left; aapply h
-  
 -- Spy never sees another agent's private key unless it's bad at the start
 @[simp]
 theorem Spy_see_priEK {h : ns_public evs} :
@@ -62,17 +53,14 @@ theorem Spy_see_priEK {h : ns_public evs} :
   constructor
   · induction h with
     | Nil =>
-      simp[spies, knows, initState, pubEK, priEK, pubSK]; intro h
-      rcases h with (((⟨B, bad, h⟩ | ⟨B, bad, h⟩) | ⟨B, h⟩) | ⟨B, h⟩) <;>
-      try (apply injective_publicKey at h; simp_all)
-      all_goals (apply publicKey_neq_privateKey at h; contradiction)
+      simp[spies, knows, initState, pubEK, priEK, pubSK]
     | Fake _ h ih =>
       apply Fake_parts_sing at h
       intro h₁; simp at h₁; apply Fake_parts_sing_helper (h := h) at h₁
-      simp at h₁; aapply ih;
-    | NS1 _ _ ih => simp; assumption
-    | NS2 _ _ _ ih => simp; assumption
-    | NS3 _ _ _ ih => simp; assumption
+      simp_all
+    | NS1 => simp_all
+    | NS2 => simp_all
+    | NS3 => simp_all
   · intro h₁; apply parts_increasing; aapply Spy_spies_bad_privateKey
 
 @[simp]
@@ -89,41 +77,29 @@ theorem no_nonce_NS1_NS2 { evs: List Event} { h : ns_public evs  } :
   Nonce NA ∈ analz (spies evs))) := by
   intro h₁ h₂
   induction h with
-  | Nil => rw[spies, knows] at h₂; simp[initState] at h₂
+  | Nil => simp[spies, knows] at h₂
   | Fake _ h ih => 
-      simp; apply analz_insert; right
+      simp; apply analz_insert;
       apply Fake_parts_sing at h
       simp at h₁; apply Fake_parts_sing_helper (h := h) at h₁; simp at h₁
       simp at h₂; apply Fake_parts_sing_helper (h := h) at h₂; simp at h₂
       rcases h₁ with ((_ | _) | _) <;> 
       rcases h₂ with ((_ | _) | _) <;>
-      try simp_all
-      all_goals (aapply ih <;> aapply analz_subset_parts)
+      simp_all
+      all_goals (right; aapply ih <;> aapply analz_subset_parts)
   | NS1 _ nonce_not_used =>
     apply parts_knows_Spy_subset_used_neg at nonce_not_used;
-    simp[spies] at h₁; rw[parts_element, Set.subset_def] at h₁; simp at h₁;
-    simp[spies] at h₂; rw[parts_element, Set.subset_def] at h₂; simp at h₂;
-    apply analz_mono; apply Set.subset_insert
+    simp[spies] at h₁; expand_parts_element at h₁;
+    simp[spies] at h₂; expand_parts_element at h₂;
+    apply analz_spies_mono
     cases h₂ <;> simp_all
   | NS2 _ nonce_not_used =>
     apply parts_knows_Spy_subset_used_neg at nonce_not_used;
-    simp[spies] at h₁; rw[parts_element, Set.subset_def] at h₁; simp at h₁;
-    simp[spies] at h₂; rw[parts_element, Set.subset_def] at h₂; simp at h₂;
-    apply analz_mono; apply Set.subset_insert
+    simp[spies] at h₁
+    simp[spies] at h₂; expand_parts_element at h₂;
+    apply analz_spies_mono
     cases h₁ <;> simp_all
-  | NS3 _ _ _ a_ih => simp at h₁; simp at h₂; apply analz_mono
-                      apply Set.subset_insert; aapply a_ih
-
-@[simp]
-lemma injective_pubEK_helper:
-  ( pubEK A = pubEK B ∧ h) ↔ ( A = B ∧ h )
-:= by
-  constructor
-  · intro h₁
-    rcases h₁ with ⟨e, _⟩
-    apply injective_publicKey at e
-    aapply And.intro; simp_all
-  · intro h₁; simp_all
+  | NS3 _ _ _ a_ih => simp at h₁; simp at h₂; apply analz_spies_mono; aapply a_ih
 
 -- Unicity for NS1: nonce NA identifies agents A and B
 theorem unique_NA { h : ns_public evs } :
@@ -132,36 +108,25 @@ theorem unique_NA { h : ns_public evs } :
   (Nonce NA ∉ analz (spies evs) →
   A = A' ∧ B = B'))) := by
   induction h with
-  | Nil => aesop (add norm spies, norm knows, safe analz_insertI)
+  | Nil => simp[spies, knows]
   | Fake _ a a_ih =>
     apply Fake_parts_sing at a; intro h₁ h₂ h₃;
-    simp[spies, knows] at h₁; apply Fake_parts_sing_helper (h := a) at h₁
-    simp at h₁
-    simp[spies, knows] at h₂; apply Fake_parts_sing_helper (h := a) at h₂
-    simp at h₂
-    simp[spies, knows] at h₃;
+    simp at h₁; apply Fake_parts_sing_helper (h := a) at h₁; simp at h₁
+    simp at h₂; apply Fake_parts_sing_helper (h := a) at h₂; simp at h₂
+    apply analz_spies_mono_neg at h₃;
     rcases h₁ with ((_ | _) | _) <;> 
     rcases h₂ with ((_ | _) | _) <;>
-    try (
-      apply False.elim; apply h₃; apply analz_mono; aapply Set.subset_insert
-      tauto
-    )
-    all_goals (aapply a_ih <;> try aapply analz_subset_parts
-               all_goals (
-                 intro _; apply h₃; aapply analz_mono; aapply Set.subset_insert
-               ))
+    try tauto
+    all_goals (aapply a_ih <;> aapply analz_subset_parts)
   | NS1 _ nonce_not_used a_ih =>
     intro h₁ h₂ h₃
-    simp at h₁; rw[parts_element, Set.subset_def] at h₁; simp at h₁
-    simp at h₂; rw[parts_element, Set.subset_def] at h₂; simp at h₂
+    simp at h₁; expand_parts_element at h₁
+    simp 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
     cases h₁ <;> cases h₂ <;> simp_all
-    aapply a_ih; intro h; apply h₃; apply_rules[analz_mono, Set.subset_insert]
-  | NS2 _ _ _ a_ih => intro h₁ h₂ h₃; simp_all; apply a_ih; intro h; apply h₃
-                      apply_rules [analz_mono, Set.subset_insert]
-  | NS3 _ _ _ a_ih => intro h₁ h₂ h₃; simp at h₁; simp at h₂; aapply a_ih
-                      intro h; apply h₃
-                      apply_rules [analz_mono, Set.subset_insert]
+  | 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
 theorem Spy_not_see_NA { h : ns_public evs  }
@@ -199,7 +164,7 @@ theorem Spy_not_see_NA { h : ns_public evs  }
     cases h₁ with | tail _ b =>
       have _ := h₄
       simp at h₄; apply analz_insert_Crypt_subset at h₄
-      simp at h₄; rcases h₄ with ( h | h | h)
+      simp at h₄; rcases h₄ with ( h | h )
       · have _ := b; have _ := a₁; have _ := a₂
         rw[h] at b; apply Says_imp_parts_knows_Spy at b
         apply Says_imp_parts_knows_Spy at a₂
@@ -207,10 +172,7 @@ theorem Spy_not_see_NA { h : ns_public evs  }
         · assumption
         · rw[h]; exact a₂
         · rw[h]; exact b
-      · aapply a_ih; aapply analz.inj
-      · aapply a_ih; aapply analz.fst
-      · aapply a_ih; aapply analz.snd
-      · aapply a_ih; aapply analz.decrypt
+      · aapply a_ih
       
 -- 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 }
@@ -230,30 +192,23 @@ theorem A_trusts_NS2 {h : ns_public evs }
     simp at h₁; simp at h₂;
     cases h₁
     · have _ := Spy_in_bad; simp_all
-    · right; apply Fake_parts_sing at a;
+    · apply Fake_parts_sing at a;
       apply Fake_parts_sing_helper (h := a) at h₂; simp at h₂
-      rcases h₂ with ((_ | _) | _) <;> aapply a_ih
+      rcases h₂ with ((_ | _) | _) <;> (right; aapply a_ih)
       · aapply analz_subset_parts
       · apply False.elim; apply snsNA; apply analz_spies_mono; tauto;
     · aapply ns_public.Fake
-  | NS1 _ a a_ih => right; simp at h₂; cases h₁
-                    · apply False.elim; apply a
-                      apply parts_knows_Spy_subset_used; apply parts.fst
-                      aapply parts.body
-                    · aapply a_ih; 
+  | NS1 _ a a_ih =>
+    apply parts_knows_Spy_subset_used_neg at a;
+    simp at h₂; expand_parts_element at h₂;
+    simp at h₁; cases h₁ <;> simp_all
   | NS2 _ _ a a_ih =>
-    simp at h₁; have b := h₁; have snsNA := h₁
+    simp at h₁; have snsNA := h₁
     apply Spy_not_see_NA at snsNA <;> try assumption
-    simp at h₂; rcases h₂ with (⟨_ , e₂ , _, e₄⟩ | _)
-    · apply Says_imp_parts_knows_Spy at a
-      apply Says_imp_parts_knows_Spy at b
-      apply unique_NA at a
-      rw[e₂] at b; rw[e₂] at snsNA
-      apply a at b
-      apply b at snsNA
-      simp_all[-e₄]; assumption
-    · right; aapply a_ih
-  | NS3 _ _ a a_ih => simp at h₁; simp at h₂; right; aapply a_ih
+    simp at h₂; 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} :
@@ -263,19 +218,17 @@ lemma B_trusts_NS1 { h : ns_public evs} :
 := by
   intro h₁ h₂
   induction h with
-  | Nil => simp[spies] at h₁; rw[knows] at h₁; simp[initState] at h₁
+  | Nil => simp[spies, knows] at h₁
   | Fake _ a a_ih =>
+    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 at h₁
-    rcases h₁ with ((h₁ | h₁ )| h₁); 
-    · right; aapply a_ih; aapply analz_subset_parts; aapply analz_spies_mono_neg
-    · apply False.elim; apply h₂; apply analz_spies_mono; simp_all
-    · right; aapply a_ih; aapply analz_spies_mono_neg
-  | NS1 _ _ a_ih => simp at h₁; cases h₁
-                    · simp_all
-                    · right; aapply a_ih; aapply analz_spies_mono_neg
-  | NS2 _ _ _ a_ih => simp at h₁; right; aapply a_ih; aapply analz_spies_mono_neg
-  | NS3 _ _ _ a_ih => simp at h₁; right; aapply a_ih; aapply analz_spies_mono_neg
+    rcases h₁ with ((h₁ | _ )| _) <;> simp_all 
+    right; aapply a_ih; aapply analz_subset_parts;
+  | NS1 _ _ a_ih =>
+    apply analz_spies_mono_neg at h₂; simp_all; cases h₁ <;> simp_all
+  | NS2 _ _ _ a_ih => 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`
 
@@ -289,31 +242,26 @@ theorem unique_NB { h : ns_public evs } :
   induction h with
   | Nil => aesop (add norm spies, norm knows, safe analz_insertI)
   | Fake _ a a_ih =>
-    intro h₁ h₂ h₃;
-    apply Fake_parts_sing at a
-    simp[spies, knows] at h₁; apply Fake_parts_sing_helper (h := a) at h₁
-    simp at h₁;
+    apply Fake_parts_sing at a; intro h₁ h₂ h₃;
+    simp at h₁; apply Fake_parts_sing_helper (h := a) at h₁; simp at h₁;
     simp at h₂; apply Fake_parts_sing_helper (h := a) at h₂; simp at h₂;
     apply analz_spies_mono_neg at h₃
-    rcases h₁ with ((h₁ | h₁) | h₁) <;> 
-    rcases h₂ with ((h₂ | h₂) | h₂) <;>
+    rcases h₁ with ((_ | _) | _) <;> 
+    rcases h₂ with ((_ | _) | _) <;>
     simp_all
     all_goals (aapply a_ih; repeat aapply analz_subset_parts)
   | NS1 _ _ a_ih => intro h₁ h₂ h₃; simp at h₁; simp at h₂; aapply a_ih
                     aapply analz_spies_mono_neg
   | NS2 _ nonce_not_used _ a_ih =>
     intro h₁ h₂ h₃;
-    -- This is how to rewrite `M ∈ parts` terms into something useful
-    -- TODO create a macro for this
-    -- TODO this should work with analz as well
-    simp at h₁; rw[parts_element, Set.subset_def] at h₁; simp at h₁
-    simp at h₂; rw[parts_element, Set.subset_def] at h₂; simp at h₂
+    simp at h₁; expand_parts_element at h₁
+    simp at h₂; expand_parts_element at h₂
     apply analz_spies_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;
+    intro h₁ h₂ h₃; apply analz_spies_mono_neg at h₃; simp_all[-Key.injEq]
 
 -- `NB` remains secret 
 theorem Spy_not_see_NB { h : ns_public evs }
@@ -333,7 +281,7 @@ theorem Spy_not_see_NB { h : ns_public evs }
     apply parts_knows_Spy_subset_used_neg at nonce_not_used
     cases h₄ with
     | inl e => apply Says_imp_parts_knows_Spy at h₁;
-               rw[parts_element, Set.subset_def] at h₁; simp_all
+               expand_parts_element at h₁; simp_all
     | inr => aapply a_ih
   | NS2 _ not_used_NB a a_ih =>
     simp at h₁;
@@ -345,7 +293,7 @@ theorem Spy_not_see_NB { h : ns_public evs }
       · aapply a_ih; apply Says_imp_parts_knows_Spy at a; 
         apply Says_imp_parts_knows_Spy at h₁; simp_all; aapply no_nonce_NS1_NS2
       · apply Says_imp_parts_knows_Spy at h₁;
-        rw[parts_element, Set.subset_def] at h₁; simp_all
+        expand_parts_element at h₁; simp_all
       · aapply a_ih
   | NS3 _ _ a a_ih =>
     simp at h₁; simp[analz_insert_Crypt_element] at h₄; 
@@ -367,31 +315,28 @@ theorem B_trusts_NS3 { h : ns_public evs }
   induction h with
   | Nil => simp_all
   | Fake _ a a_ih =>
-    right; simp at h₁
+    simp at h₁
     apply Fake_parts_sing at a
     simp at h₂; apply Fake_parts_sing_helper (h := a) at h₂; simp at h₂
-    rw[parts_element, Set.subset_def] at h₂; simp at h₂
+    expand_parts_element at h₂;
     have _ := Spy_in_bad
-    rcases h₁ with (h₁ | h₁) <;> rcases h₂ with ((h₂ | h₂) | h₂) <;> simp_all
-    · aapply a_ih; aapply analz_subset_parts
+    rcases h₁ with (_ | h₁) <;> rcases h₂ with ((h₂ | _) | _) <;> simp_all
+    · apply analz_subset_parts at h₂; simp_all
     · apply Spy_not_see_NB at h₁ <;> simp_all
-    · aapply a_ih
-  | NS1 _ a a_ih => right; simp at h₂; simp at h₁; aapply a_ih;
-  | NS2 _ nonce_not_used a a_ih =>
-    right
+  | NS1 => simp_all
+  | NS2 _ nonce_not_used =>
     apply parts_knows_Spy_subset_used_neg at nonce_not_used;
-    simp at h₂; rw[parts_element, Set.subset_def] at h₂; simp at h₂
-    simp at h₁; cases h₁ <;> simp_all; aapply a_ih
-  | NS3 _ _ a₂ a_ih =>
+    simp at h₂; expand_parts_element at h₂;
+    simp at h₁; cases h₁ <;> simp_all
+  | NS3 _ _ a₂ =>
     simp at h₁
-    simp at h₂; rw[parts_element, Set.subset_def] at h₂; simp at h₂
+    simp at h₂; 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
+    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`
   
@@ -406,24 +351,22 @@ theorem B_trusts_protocol { h : ns_public evs  }
   induction h with
   | Nil => simp_all
   | Fake _ a a_ih =>
-    right
     apply Fake_parts_sing at a
     simp at h₁; apply Fake_parts_sing_helper (h := a) at h₁;
-    rw[parts_element, Set.subset_def] at h₁; simp at h₁
+    expand_parts_element at h₁
     have _ := Spy_in_bad
     simp at h₂; rcases h₂ with (_ | h₂) <;> simp_all
-    rcases h₁ with (((_ |_ ) | _) | _)  <;> try (aapply a_ih)
-    · aapply analz_subset_parts
+    rcases h₁ with (((_ |_ ) | _) | _)  <;> try simp_all
+    · right; aapply a_ih; aapply analz_subset_parts
     · apply Spy_not_see_NB at h₂ <;> simp_all
-    · simp_all
-  | NS1 _ a a_ih => right; simp at h₂; simp at h₁; aapply a_ih;
-  | NS2 _ _ a a_ih => right; simp at h₁; simp at h₂; cases h₂ with
-    | inl => apply parts.body at h₁; apply parts_knows_Spy_subset_used at h₁
-             simp_all
-    | inr => aapply a_ih
+  | NS1 => simp_all
+  | NS2 _ nonce_not_used a a_ih =>
+    simp at h₁; simp at h₂;
+    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 h₂
-    simp at h₁; rw[parts_element, Set.subset_def] at h₁; simp at h₁
+    simp at h₁; expand_parts_element at h₁
     cases h₁ <;> simp_all
     have h₂c := h₂
     apply Spy_not_see_NB at h₂c

InductiveVerification/Public.lean

@@ -3,7 +3,6 @@ import Init.Data.Nat.Lemmas
 import Mathlib.Data.Nat.Basic
 import Mathlib.Data.Nat.Dist
 import Mathlib.Order.Defs.PartialOrder
-set_option diagnostics true
 
 -- Theory of Public Keys (common to all public-key protocols)
 
@@ -35,15 +34,18 @@ noncomputable abbrev pubK (A : Agent) : Key := pubEK A
 noncomputable abbrev priK (A : Agent) : Key := invKey (pubEK A)
 
 -- Axioms for private and public keys
+@[simp]
 axiom privateKey_neq_publicKey {b c : KeyMode} {A A' : Agent} :
     privateKey b A ≠ publicKey c A'
 
+@[simp]
 lemma publicKey_neq_privateKey {b c : KeyMode} {A A' : Agent} :
     publicKey b A ≠ privateKey c A' := by
   exact privateKey_neq_publicKey.symm
 
 -- Basic properties of pubK and priK
 omit [InvKey] in
+@[simp]
 lemma publicKey_inject {b c : KeyMode} {A A' : Agent} :
     (publicKey b A = publicKey c A') ↔ (b = c ∧ A = A') := by
   grind[injective_publicKey]
@@ -59,7 +61,7 @@ by
 
 lemma not_symKeys_priK {b : KeyMode} {A : Agent} :
     privateKey b A ∉ symKeys := by
-  simp [symKeys, privateKey, invKey_eq]; grind[privateKey_neq_publicKey];
+  simp [symKeys, privateKey, invKey_eq, privateKey_neq_publicKey]
 
 lemma syKey_neq_priEK :
   K ∈ symKeys → K ≠ priEK A := by
@@ -93,7 +95,7 @@ omit [InvKey] in
 @[simp]
 lemma publicKey_image_eq :
     (publicKey b x ∈ publicKey c '' AA) ↔ (b = c ∧ x ∈ AA) := by
-  simp [Set.mem_image, publicKey_inject, And.comm, Eq.comm]
+  simp [Set.mem_image, And.comm, Eq.comm]
 
 @[simp]
 lemma privateKey_notin_image_publicKey :
@@ -252,22 +254,16 @@ lemma MPair_used {P : Prop} :
 lemma keysFor_parts_initState {C : Agent} :
     keysFor (parts (initState C)) = ∅ := by
   cases C <;>
-  simp[initState, keysFor] <;>
-  repeat rw[Set.singleton_def, parts_insert_Key, parts_empty] <;>
-  simp
+  simp[initState, keysFor]
 
 lemma Crypt_notin_initState {B : Agent} :
   Msg.Crypt K X ∉ parts ( initState B ) := by
-  cases B <;> simp[initState, priEK, priSK, shrK] <;>
-  apply And.intro <;> try apply And.intro
-  all_goals repeat rw[Set.singleton_def, parts_insert_Key, parts_empty] <;>
-  simp
+  cases B <;> simp[initState, priEK, priSK]
 
 @[simp]
 lemma Crypt_notin_used_empty :
   Msg.Crypt K X ∉ used [] := by
-  simp[used]; intro A; cases A <;> simp <;> apply And.intro <;> try apply And.intro
-  all_goals (rw[Set.singleton_def, parts_insert_Key, parts_empty] ; simp)
+  simp[used]; intro A; cases A <;> simp
 
 -- Basic properties of shrK
 
@@ -324,10 +320,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 <;>
-  try simp
-  · left; left; right; exists Agent.Spy; apply And.intro; exact Spy_in_bad; rfl
-  · left; left; left; exists Agent.Spy; apply And.intro; exact Spy_in_bad; rfl
+  cases b <;> simp[Spy_in_bad]
 
 @[simp]
 lemma publicKey_in_initState {b : KeyMode} {A : Agent} {B : Agent} :
@@ -342,9 +335,7 @@ lemma publicKey_in_initState {b : KeyMode} {A : Agent} {B : Agent} :
 lemma spies_pubK : Msg.Key (publicKey b A) ∈ spies evs := by
   induction evs with
   | nil => simp [spies, knows]
-           cases b
-           · right; exists A
-           · left; right; exists A
+           cases b <;> tauto
   | cons e evs ih =>
     cases e <;> rw [spies] <;> apply knows_subset_knows_Cons <;> assumption
 
@@ -355,10 +346,7 @@ lemma analz_spies_pubK : Msg.Key (publicKey b A) ∈ analz (spies evs) := by
 -- Spy sees private keys of bad agents
 lemma Spy_spies_bad_privateKey { h : A ∈ bad } : Msg.Key (privateKey b A) ∈ spies evs := by
   induction evs with
-  | nil => simp [spies, knows, pubSK, pubEK]; left; left
-           cases b
-           · right; exists A
-           · left; exists A
+  | nil => simp_all [spies, knows, pubSK, pubEK]; cases b <;> tauto
   | cons e evs ih =>
     cases e <;> rw[spies] <;> aapply knows_subset_knows_Cons
 
@@ -405,14 +393,11 @@ by simp[Crypt_synth_EK];
 @[simp]
 lemma Nonce_notin_initState {B : Agent} : Msg.Nonce N ∉ parts (initState B) := by
   cases B <;>
-  simp [initState] <;> apply And.intro <;> try (apply And.intro)
-  all_goals (rw[Set.singleton_def, parts_insert_Key, parts_empty]; simp)
+  simp [initState]
 
 @[simp]
 lemma Nonce_notin_used_empty : Msg.Nonce N ∉ used [] := by
-  simp [used]; intro A; cases A <;> simp <;>
-  apply And.intro <;> try (apply And.intro)
-  all_goals (rw[Set.singleton_def, parts_insert_Key, parts_empty]; simp)
+  simp [used]; intro A; cases A <;> simp
 
 -- Supply fresh nonces for possibility theorems
 lemma Nonce_supply_lemma : ∃ N, ∀ n, N ≤ n → Msg.Nonce n ∉ used evs := by