Replaced some cases instances with grind

InductiveVerification/Message.lean

@@ -1628,5 +1628,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

@@ -52,16 +52,16 @@ theorem Spy_see_priEK {h : ns_public evs} :
   (Key (priEK A) ∈ parts (spies evs)) ↔ A ∈ bad := by
   constructor
   · induction h with
-    | Nil =>
-      simp[spies, knows, initState, pubEK, priEK, pubSK]
-    | Fake _ h ih =>
+    -- TODO add these attributes to simp, also check what can be added to grind
+    | Nil => simp[spies, knows, initState, pubEK, priEK, pubSK]
+    | Fake _ h =>
       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} :
@@ -70,7 +70,8 @@ theorem Spy_analz_priEK {h : ns_public evs} :
   · 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
 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) →
@@ -78,28 +79,24 @@ theorem no_nonce_NS1_NS2 { evs: List Event} { h : ns_public evs  } :
   intro h₁ h₂
   induction h with
   | Nil => simp[spies, knows] at h₂
-  | Fake _ h ih =>
-      simp; apply analz_insert;
+  | Fake _ h =>
+    apply analz_spies_mono
+    simp [*] at *
     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 ((_ | _) | _) <;>
-      simp_all
-      all_goals (right; aapply ih <;> aapply analz_subset_parts)
-  | NS1 _ nonce_not_used =>
+    apply Fake_parts_sing_helper (h := h) at h₁
+    apply Fake_parts_sing_helper (h := h) at h₂
+    simp [*] at *; grind[analz_subset_parts]
+  | NS1 =>
     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
-  | NS2 _ nonce_not_used =>
+    grind [ parts_knows_Spy_subset_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]
-  | NS3 _ _ _ a_ih => apply analz_spies_mono; simp_all
+    grind [ parts_knows_Spy_subset_used ]
+  | NS3 => apply analz_spies_mono; simp_all
 
 -- Unicity for NS1: nonce NA identifies agents A and B
 theorem unique_NA { h : ns_public evs } :
@@ -116,14 +113,10 @@ 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 =>
-    intro h₁ h₂ h₃
-    apply analz_insert_mono_neg at h₃
-    simp [*] at *
-    expand_parts_element at h₁
-    expand_parts_element at h₂
-    apply parts_knows_Spy_subset_used_neg at nonce_not_used
-    cases h₁ <;> cases h₂ <;> simp_all
+  | NS1 =>
+    intro h₁ h₂ _; simp [*] at *
+    expand_parts_element at h₁; expand_parts_element at h₂
+    grind [ analz_insert_mono_neg, parts_knows_Spy_subset_used_neg ]
   | NS2 => intro _ _ h₃; apply analz_insert_mono_neg at h₃; simp_all
   | NS3 => intro _ _ h₃; apply analz_insert_mono_neg at h₃; simp_all;
 
@@ -136,37 +129,29 @@ theorem Spy_not_see_NA { h : ns_public evs  }
   intro h₁ h₄
   induction h with
   | Nil => simp_all
-  | Fake _ a =>
-    have _ := Spy_in_bad; apply Fake_analz_insert at a; apply a at h₄; simp_all
-  | NS1 _ a a_ih =>
+  | Fake _ a => apply Fake_analz_insert at a; apply a at h₄; simp_all[Spy_in_bad]
+  | NS1 _ a =>
     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
       simp_all[Set.subset_def]
-  | NS2 _ not_used_NB a a_ih =>
-    simp at 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;
+  | NS2 _ _ a a_ih =>
+    simp [*] at *; have _ := h₄; have c := h₁
     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
-      apply not_used_NB; apply parts_knows_Spy_subset_used; apply parts.fst;
-      apply parts.body; apply Says_imp_parts_knows_Spy; assumption
-    · aapply a_ih
-  | NS3 _ _ a₂ a_ih =>
-    simp [*] at *
-    have _ := h₄
+    · grind[parts_knows_Spy_subset_used]
+  | NS3 =>
     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
+    grind [Says_imp_parts_knows_Spy, no_nonce_NS1_NS2]
 
--- 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 +164,23 @@ 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[Spy_in_bad]
     · 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)
-      · aapply analz_subset_parts
-      · tauto
+      grind [analz_subset_parts]
     · aapply ns_public.Fake
-  | NS1 _ a a_ih =>
-    apply parts_knows_Spy_subset_used_neg at a;
-    simp [*] at *; expand_parts_element at h₂; cases h₁ <;> simp_all
-  | NS2 _ _ a a_ih =>
+  | NS1 =>
+    simp [*] at *; expand_parts_element at h₂
+    grind[parts_knows_Spy_subset_used_neg]
+  | NS2 =>
     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;
+    grind [ Spy_not_see_NA, Says_imp_parts_knows_Spy, unique_NA ]
+  | NS3 => simp_all;
 
 -- If the encrypted message appears then it originated with Alice in `NS1`
 lemma B_trusts_NS1 { h : ns_public evs} :
@@ -211,14 +191,13 @@ lemma B_trusts_NS1 { h : ns_public evs} :
   intro h₁ h₂
   induction h with
   | Nil => simp[spies, knows] 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 =>
-    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;
+  | NS1 => apply analz_spies_mono_neg at h₂; simp_all; cases h₁ <;> simp_all
+  | NS2 => apply analz_spies_mono_neg at h₂; simp_all;
+  | NS3 => apply analz_spies_mono_neg at h₂; simp_all;
 
 -- Authenticity Properties obtained from `NS2`
 
@@ -231,27 +210,19 @@ theorem unique_NB { h : ns_public evs } :
   -- Proof closely follows that of unique_NA
   induction h with
   | Nil => aesop (add norm spies, norm knows, 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 ((_ | _) | _) <;>
-    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₃; simp [*] at *
+    grind[analz_subset_parts]
+  | NS1 => intro _ _ h₃; apply analz_spies_mono_neg at h₃; simp_all
+  | NS2 =>
+    intro 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]
+    grind[analz_insert_mono_neg, parts_knows_Spy_subset_used]
+  | NS3 => intro _ _ _; simp_all; grind[analz_insert_mono_neg]
 
 -- `NB` remains secret
 theorem Spy_not_see_NB { h : ns_public evs }
@@ -263,33 +234,34 @@ theorem Spy_not_see_NB { h : ns_public evs }
   intro h₁ h₄
   induction h with
   | Nil => simp_all
-  | Fake _ a a_ih =>
-    have _ := Spy_in_bad; apply Fake_analz_insert at a; apply a at h₄; simp_all;
-  | NS1 _ nonce_not_used a_ih =>
+  | Fake _ a =>
+    apply Fake_analz_insert at a; apply a at h₄; simp_all[Spy_in_bad];
+  | NS1 =>
     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
-  | NS2 _ not_used_NB a a_ih =>
+    expand_parts_element at h₂
+    grind[parts_knows_Spy_subset_used]
+  | 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
-    · apply analz_insert_Crypt_subset at h₄; simp at h₄; rcases h₄ with (_ |_ |_ )
-      · 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₁;
-        expand_parts_element at h₁; simp_all
-      · aapply a_ih
-  | NS3 _ _ a a_ih =>
+    · simp_all; grind [ parts_knows_Spy_subset_used, analz_subset_parts ]
+    · have _ := h₁; apply Says_imp_parts_knows_Spy at h₁
+      expand_parts_element at h₁
+      grind[
+        parts_knows_Spy_subset_used,
+        Says_imp_parts_knows_Spy,
+        no_nonce_NS1_NS2
+      ];
+  | NS3 =>
     simp at h₁; simp[analz_insert_Crypt_element] at h₄;
     rcases h₄ with (⟨_, _⟩ | ⟨_, _⟩) <;> simp_all
-    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
+    grind [ Says_imp_parts_knows_Spy, unique_NB ]
 
--- 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 +273,17 @@ 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₂;
-    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
+    grind [ Spy_in_bad, analz_subset_parts, Spy_not_see_NB ]
   | NS1 => simp_all
-  | NS2 _ nonce_not_used =>
-    simp [*] at *
-    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
+  | NS2 =>
+    simp [*] at *; expand_parts_element at h₂;
+    grind[ parts_knows_Spy_subset_used ];
+  | NS3 =>
+    simp [*] at *; grind [ Spy_not_see_NB, Says_imp_parts_knows_Spy, unique_NB ]
 
 -- Overall guarantee for `B`
 
@@ -337,29 +298,18 @@ 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₁;
     expand_parts_element at h₁
-    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
+    grind[Spy_in_bad, analz_subset_parts, Spy_not_see_NB]
   | NS1 => simp_all
-  | NS2 _ nonce_not_used a a_ih =>
+  | NS2 =>
+    simp [*] at *; expand_parts_element at h₁;
+    grind[parts_knows_Spy_subset_used];
+  | NS3 =>
     simp [*] at *
-    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
+    grind[Spy_not_see_NB, Says_imp_parts_knows_Spy, unique_NB ]
 
 end NS_Public

Main.lean

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