Update lemmas

1 files changed, 188 insertions, 180 deletions

diff --git a/xacml-proofs/lean/Xacml.lean b/xacml-proofs/lean/Xacml.lean
index 349b817..efe86d2 100644
--- a/xacml-proofs/lean/Xacml.lean
+++ b/xacml-proofs/lean/Xacml.lean
@@ -1393,11 +1393,6 @@ theorem string_equal_self (s : String) (req : Request) :
     req = some (Value.primitive (XmlType.boolean, "True")) := by
   simp [Expression.eval, Expression.apply_eval, Primitive.mk]
 
--- #check List.contains_cons
--- theorem ssdf' {α β : Type} [BEq α] [BEq β] (x y : α) (xs : List α) (f : α → β) : x = y → (x == y) = true := by
---   intro h
---   apply?
-
 theorem contains_implies_map_contains {α β : Type} [BEq α] [LawfulBEq α] [BEq β] [LawfulBEq β] (x : α) (xs : List α) (f : α → β) :
   xs.contains x → (List.map f xs).contains (f x) := by
   induction xs with
@@ -1418,9 +1413,8 @@ theorem contains_implies_map_contains {α β : Type} [BEq α] [LawfulBEq α] [BE
 
 theorem attribute_designator_matches (attr : Attribute) (s : String) :
   attr.value = (XmlType.string, s) →
-  attr.issuer = none →
   AttributeDesignator.matches?
-    { category := attr.category, identifier := attr.identifier, type := XmlType.string, issuer := none, must_be_present := true }
+    { category := attr.category, identifier := attr.identifier, type := XmlType.string, issuer := attr.issuer, must_be_present := true }
     attr = true := by
   intro h
   unfold AttributeDesignator.matches?
@@ -1444,12 +1438,13 @@ theorem filter_elem {α : Type} (x : α) (xs : List α) (f : α → Bool) :
       { simp_all only [List.mem_cons, or_true] }
       { simp_all only }
 
-theorem attribute_designator_eval (attr : Attribute) (s : String) (req : Request) :
+theorem attribute_designator_eval (attr : Attribute) (s : String) (req : List Attribute) (res : List Primitive) :
   attr.value = (XmlType.string, s) →
   req.elem attr →
   AttributeDesignator.eval
-    { category := attr.category, identifier := attr.identifier, type := XmlType.string, issuer := none, must_be_present := true }
-    req = Sum.inl (Value.primitive (XmlType.boolean, "True")) := by
+    { category := attr.category, identifier := attr.identifier, type := XmlType.string, issuer := attr.issuer, must_be_present := true }
+    req = Sum.inl (Value.bag (Bag.mk res))
+  → attr.value ∈ res:= by
   intros h₁ h₂
   unfold AttributeDesignator.eval
   simp
@@ -1457,7 +1452,7 @@ theorem attribute_designator_eval (attr : Attribute) (s : String) (req : Request
   let filter :=
     (List.filter
       (AttributeDesignator.matches?
-        { category := attr.category, identifier := attr.identifier, type := XmlType.string, issuer := none,
+        { category := attr.category, identifier := attr.identifier, type := XmlType.string, issuer := attr.issuer,
           must_be_present := true })
       req)
   let filtermap := List.map (fun x => x.value) filter
@@ -1465,20 +1460,34 @@ theorem attribute_designator_eval (attr : Attribute) (s : String) (req : Request
     List.map (fun x => x.value)
       (List.filter
         (AttributeDesignator.matches?
-          { category := attr.category, identifier := attr.identifier, type := XmlType.string, issuer := none,
+          { category := attr.category, identifier := attr.identifier, type := XmlType.string, issuer := attr.issuer,
             must_be_present := true })
         req) = filtermap
     by rfl
 
-  have h : attr ∈ filter := by sorry
-  sorry
-  -- have h : attr.value ∈ filtermap := by
-
+  have h : List.contains filter attr := by
+    apply List.elem_eq_true_of_mem
+    apply filter_elem
+    apply List.mem_of_elem_eq_true
+    apply h₂
+    apply attribute_designator_matches
+    apply h₁
+  have h : attr.value ∈ filtermap := by
+    apply List.mem_of_elem_eq_true
+    apply contains_implies_map_contains
+    exact h
 
+  match filtermap with
+  | [] => contradiction
+  | a :: as =>
+    simp
+    intro h'
+    rw [←h']
+    assumption
 
 theorem match_eval (attr : Attribute) (s : String) (req : Request) :
   attr.value = (XmlType.string, s) →
-  req.contains attr →
+  req.elem attr →
   Match.eval { function := "urn:oasis:names:tc:xacml:1.0:function:string-equal",
                designator :=
                  { category := attr.category,
@@ -1501,7 +1510,7 @@ theorem match_eval (attr : Attribute) (s : String) (req : Request) :
   | Sum.inl (Value.primitive p) =>
     simp
     sorry -- contradiction by designator_always_returns_bag
-  | Sum.inl (Value.bag b) =>
+  | Sum.inl (Value.bag (Bag.mk attrs)) =>
     simp
     let f := ((fun x =>
                   match x with
@@ -1512,15 +1521,18 @@ theorem match_eval (attr : Attribute) (s : String) (req : Request) :
                   (Expression.apply "urn:oasis:names:tc:xacml:1.0:function:string-equal"
                     [Value.primitive (XmlType.string, s), Value.primitive attr])
                   req)
-    have h_branch :
-      List.elem (Value.primitive (#<XmlType.boolean,"True">))
-            (List.map f b.contents) =
-          true := by sorry
-
-
+    have h_asdf : attr.value ∈ attrs := by
+      apply attribute_designator_eval
+      apply h₁
+      apply h₂
+      sorry
+    sorry
+    -- have h_branch :
+    --   List.elem (Value.primitive (#<XmlType.boolean,"True">))
+    --         (List.map f attrs) =
+    --       true := by
 
-    simp [h_branch]
-    simp [Primitive.mk]
+    --     | nil => contradiction
   | Sum.inr _ => sorry
   -- wts: eval results in a list with the attribute in it
   -- wts: streq map containing attribute contains true
@@ -1967,11 +1979,23 @@ def separation_of_duty (req : Request) :=
     req.contains (Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:subject" "role" none (XmlType.string, role'))
     ↔ role = role'
 
-def well_formed (req : Request) :=
+def well_formed' (req : Request) :=
   ∃ (role res : String),
       req.contains (Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:resource" "resource-class" none (XmlType.string, res))
     ∧ req.contains (Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:subject" "role" none (XmlType.string, role))
 
+def well_formed (req : Request) :=
+  ∃ (role res : String),
+      AttributeDesignator.eval
+      { category := "urn:oasis:names:tc:xacml:3.0:attribute-category:resource", identifier := "resource-class",
+        type := XmlType.string, issuer := none, must_be_present := true }
+      req = Sum.inl (Value.bag (Bag.mk [(XmlType.string, res)]))
+    ∧ AttributeDesignator.eval
+      { category := "urn:oasis:names:tc:xacml:3.0:attribute-category:subject", identifier := "role",
+        type := XmlType.string, issuer := none, must_be_present := true }
+      req = Sum.inl (Value.bag (Bag.mk [(XmlType.string, role)]))
+
+
 theorem compiled_RPSFaculty100_element_unchanged :
   compiled_RPSFaculty100_element = compiled_RPSFaculty100_element' := by rfl
 
@@ -1995,27 +2019,63 @@ theorem match_eval_distrib (req_head : Attribute) (req_tail : Request) (m : Matc
     by apply designator_eval_distrib req_head req_tail m.designator h
   rfl
 
-theorem student_not_applicable (req : Request) :
-  ¬req.contains (Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:subject" "role" none (XmlType.string, "Student"))
-  → (ElementTree.eval' req compiled_RPSStudent100_element []).1 = Decision'.not_applicable := by
-  intro h
-  simp [ElementTree.eval', compiled_RPSStudent100_element, compiled_RPSStudent100_metadata, compiled_PPSStudent100_element, compiled_PPSStudent100_metadata, compiled_gradedp100_element, compiled_gradedp100_metadata, PolicyElement.eval, compiled_gradedViewgrades_element, compiled_gradedViewgrades_metadata, PolicySet.eval]
-  sorry
-  -- intro h
-  -- rw_local
-  --   Target.eval
-  --     [[[{ function := "urn:oasis:names:tc:xacml:1.0:function:string-equal",
-  --             designator :=
-  --               { category := "urn:oasis:names:tc:xacml:3.0:attribute-category:subject", identifier := "role",
-  --                 type := XmlType.string, issuer := none, must_be_present := true },
-  --             value := Value.primitive (XmlType.string, "Student") }]]]
-  --     req = MatchResult.no_match
-  --   by sorry
+theorem allof_no_match (req : Request) (role : String) :
+    Match.eval
+      { function := "urn:oasis:names:tc:xacml:1.0:function:string-equal",
+        designator :=
+          { category := "urn:oasis:names:tc:xacml:3.0:attribute-category:subject", identifier := "role",
+            type := XmlType.string, issuer := none, must_be_present := true },
+        value := Value.primitive (XmlType.string, role) }
+      req = some (Value.primitive (XmlType.boolean, "False"))
+  → AllOf.eval
+      [{ function := "urn:oasis:names:tc:xacml:1.0:function:string-equal",
+         designator :=
+           { category := "urn:oasis:names:tc:xacml:3.0:attribute-category:subject", identifier := "role",
+             type := XmlType.string, issuer := none, must_be_present := true },
+         value := Value.primitive (XmlType.string, role) }]
+      req = MatchResult.no_match := by
+  intro h_not_role
+  unfold AllOf.eval
+  simp [h_not_role]
+  trivial
+
+theorem anyof_no_match (req : Request) (role : String) :
+    Match.eval
+      { function := "urn:oasis:names:tc:xacml:1.0:function:string-equal",
+        designator :=
+          { category := "urn:oasis:names:tc:xacml:3.0:attribute-category:subject", identifier := "role",
+            type := XmlType.string, issuer := none, must_be_present := true },
+        value := Value.primitive (XmlType.string, role) }
+      req = some (Value.primitive (XmlType.boolean, "False"))
+  → AnyOf.eval
+      [[{ function := "urn:oasis:names:tc:xacml:1.0:function:string-equal",
+            designator :=
+              { category := "urn:oasis:names:tc:xacml:3.0:attribute-category:subject", identifier := "role",
+                type := XmlType.string, issuer := none, must_be_present := true },
+            value := Value.primitive (XmlType.string, role) }]]
+      req = MatchResult.no_match := by
+  intro h_not_role
+  unfold AnyOf.eval
+  simp [List.isEmpty]
+  have hint :
+    AllOf.eval
+      [{ function := "urn:oasis:names:tc:xacml:1.0:function:string-equal",
+          designator :=
+            { category := "urn:oasis:names:tc:xacml:3.0:attribute-category:subject", identifier := "role",
+              type := XmlType.string, issuer := none, must_be_present := true },
+          value := Value.primitive (XmlType.string, role) }]
+      req = MatchResult.no_match := by
+      apply allof_no_match req role h_not_role
+  simp [hint]
 
 theorem target_no_match (req : Request) (role : String) :
-  separation_of_duty req
-  → well_formed req
-  → ¬ req.contains (Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:subject" "role" none (XmlType.string, role))
+    Match.eval
+      { function := "urn:oasis:names:tc:xacml:1.0:function:string-equal",
+        designator :=
+          { category := "urn:oasis:names:tc:xacml:3.0:attribute-category:subject", identifier := "role",
+            type := XmlType.string, issuer := none, must_be_present := true },
+        value := Value.primitive (XmlType.string, role) }
+      req = some (Value.primitive (XmlType.boolean, "False"))
   → Target.eval
       [[[{ function := "urn:oasis:names:tc:xacml:1.0:function:string-equal",
            designator :=
@@ -2023,32 +2083,95 @@ theorem target_no_match (req : Request) (role : String) :
                type := XmlType.string, issuer := none, must_be_present := true },
                value := Value.primitive (XmlType.string, role) }]]]
       req = MatchResult.no_match := by
-  intros hsod hwf h_not_role
-  induction req with
-  | nil => sorry
-  | cons _ _ _ => sorry
+  intro h_not_role
+  unfold Target.eval
+  simp
+  have hint :
+    AnyOf.eval
+      [[{ function := "urn:oasis:names:tc:xacml:1.0:function:string-equal",
+          designator :=
+            { category := "urn:oasis:names:tc:xacml:3.0:attribute-category:subject", identifier := "role",
+              type := XmlType.string, issuer := none, must_be_present := true },
+          value := Value.primitive (XmlType.string, role) }]]
+      req = MatchResult.no_match := by
+      apply anyof_no_match req role h_not_role
+  simp [hint]
 
-theorem student_not_applicable' (req : Request) :
-  separation_of_duty req
-  → well_formed req
-  → ¬req.contains (Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:subject" "role" none (XmlType.string, "Student"))
+theorem student_not_applicable (req : Request) :
+    Match.eval
+      { function := "urn:oasis:names:tc:xacml:1.0:function:string-equal",
+        designator :=
+          { category := "urn:oasis:names:tc:xacml:3.0:attribute-category:subject", identifier := "role",
+            type := XmlType.string, issuer := none, must_be_present := true },
+        value := Value.primitive (XmlType.string, "Student") }
+      req = some (Value.primitive (XmlType.boolean, "False"))
   → (ElementTree.eval' req compiled_RPSStudent100_element []).1 = Decision'.not_applicable := by
-  intros hsod hwf hnot_student
-  simp [ElementTree.eval', compiled_RPSStudent100_element, compiled_RPSStudent100_metadata, compiled_PPSStudent100_element, compiled_PPSStudent100_metadata, compiled_gradedp100_element, compiled_gradedp100_metadata, PolicyElement.eval, compiled_gradedViewgrades_element, compiled_gradedViewgrades_metadata, PolicySet.eval]
-  sorry
+  intro h_not_role
+  simp [ElementTree.eval', PolicyElement.eval, PolicySet.eval,
+        compiled_RPSStudent100_element, compiled_RPSStudent100_metadata,
+        compiled_PPSStudent100_element, compiled_PPSStudent100_metadata,
+        compiled_gradedp100_element, compiled_gradedp100_metadata,
+        compiled_gradedViewgrades_element, compiled_gradedViewgrades_metadata]
+  have hint :
+    Target.eval
+      [[[{ function := "urn:oasis:names:tc:xacml:1.0:function:string-equal",
+           designator :=
+             { category := "urn:oasis:names:tc:xacml:3.0:attribute-category:subject", identifier := "role",
+               type := XmlType.string, issuer := none, must_be_present := true },
+           value := Value.primitive (XmlType.string, "Student") }]]]
+      req = MatchResult.no_match := by
+      apply target_no_match req "Student" h_not_role
+  simp [hint]
 
 theorem faculty_not_applicable (req : Request) :
-  ¬req.contains (Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:subject" "role" none (XmlType.string, "Faculty"))
+    Match.eval
+      { function := "urn:oasis:names:tc:xacml:1.0:function:string-equal",
+        designator :=
+          { category := "urn:oasis:names:tc:xacml:3.0:attribute-category:subject", identifier := "role",
+            type := XmlType.string, issuer := none, must_be_present := true },
+        value := Value.primitive (XmlType.string, "Faculty") }
+      req = some (Value.primitive (XmlType.boolean, "False"))
   → (ElementTree.eval' req compiled_RPSFaculty100_element []).1 = Decision'.not_applicable := by
-  sorry
+  intro h_not_role
+  simp [ElementTree.eval', PolicyElement.eval, PolicySet.eval,
+        compiled_RPSFaculty100_element, compiled_RPSFaculty100_metadata]
+  have hint :
+    Target.eval
+      [[[{ function := "urn:oasis:names:tc:xacml:1.0:function:string-equal",
+           designator :=
+             { category := "urn:oasis:names:tc:xacml:3.0:attribute-category:subject", identifier := "role",
+               type := XmlType.string, issuer := none, must_be_present := true },
+           value := Value.primitive (XmlType.string, "Faculty") }]]]
+      req = MatchResult.no_match := by
+      apply target_no_match req "Faculty" h_not_role
+  simp [hint]
 
 theorem ta_not_applicable (req : Request) :
-  ¬req.contains (Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:subject" "role" none (XmlType.string, "TA"))
+    Match.eval
+      { function := "urn:oasis:names:tc:xacml:1.0:function:string-equal",
+        designator :=
+          { category := "urn:oasis:names:tc:xacml:3.0:attribute-category:subject", identifier := "role",
+            type := XmlType.string, issuer := none, must_be_present := true },
+        value := Value.primitive (XmlType.string, "TA") }
+      req = some (Value.primitive (XmlType.boolean, "False"))
   → (ElementTree.eval' req compiled_RPSTA100_element' []).1 = Decision'.not_applicable := by
-  sorry
+  intro h_not_role
+  simp [ElementTree.eval', PolicyElement.eval, PolicySet.eval,
+        compiled_RPSTA100_element', compiled_RPSTA100_metadata']
+  have hint :
+    Target.eval
+      [[[{ function := "urn:oasis:names:tc:xacml:1.0:function:string-equal",
+           designator :=
+             { category := "urn:oasis:names:tc:xacml:3.0:attribute-category:subject", identifier := "role",
+               type := XmlType.string, issuer := none, must_be_present := true },
+           value := Value.primitive (XmlType.string, "TA") }]]]
+      req = MatchResult.no_match := by
+      apply target_no_match req "TA" h_not_role
+  simp [hint]
 
 theorem ta_external_grades_not_applicable (req : Request) :
-    req.contains (Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:subject" "role" none (XmlType.string, "TA"))
+    well_formed req
+  → req.contains (Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:subject" "role" none (XmlType.string, "TA"))
   → req.contains (Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:resource" "resource-class" none (XmlType.string, "ExternalGrades"))
   → (ElementTree.eval' req compiled_RPSTA100_element' []).1 = Decision'.not_applicable := by
   sorry
@@ -2083,116 +2206,6 @@ theorem separation_of_duty_imp_other_role_not_in_req (req : Request) (role₁ ro
     all_goals assumption
   contradiction
 
-theorem student_not_indeterminate (req : Request) (result : Decision') :
-    well_formed req
-  → (ElementTree.eval' req compiled_RPSStudent100_element []).1 = result →
-      result ≠ Decision'.indeterminate
-    ∧ result ≠ Decision'.indeterminate_d
-    ∧ result ≠ Decision'.indeterminate_p
-    ∧ result ≠ Decision'.indeterminate_dp := by
-  unfold well_formed
-  intro hwf
-  simp [ElementTree.eval',
-        compiled_RPSStudent100_element,    compiled_RPSStudent100_metadata,
-        compiled_PPSStudent100_element,    compiled_PPSStudent100_metadata,
-        compiled_gradedp100_element,       compiled_gradedp100_metadata,
-        compiled_gradedViewgrades_element, compiled_gradedViewgrades_metadata]
-  match PolicyElement.eval req
-                      (PolicyElement.Rule
-                        {
-                          target :=
-                            [[[{ function := "urn:oasis:names:tc:xacml:1.0:function:string-equal",
-                                    designator :=
-                                      { category := "urn:oasis:names:tc:xacml:3.0:attribute-category:resource",
-                                        identifier := "resource-class", type := XmlType.string, issuer := none,
-                                        must_be_present := true },
-                                    value := Value.primitive (XmlType.string, "ExternalGrades") },
-                                  { function := "urn:oasis:names:tc:xacml:1.0:function:string-equal",
-                                    designator :=
-                                      { category := "urn:oasis:names:tc:xacml:3.0:attribute-category:action",
-                                        identifier := "command", type := XmlType.string, issuer := none,
-                                        must_be_present := true },
-                                    value := Value.primitive (XmlType.string, "Receive") }]]],
-                          condition := none, effect := EffectType.permit, obligations := [], advice := [] })
-                      [] with
-  | (Decision'.permit, _) =>
-    simp [PolicyElement.eval, PolicySet.eval]
-    match Target.eval
-          [[[{ function := "urn:oasis:names:tc:xacml:1.0:function:string-equal",
-                  designator :=
-                    { category := "urn:oasis:names:tc:xacml:3.0:attribute-category:subject", identifier := "role",
-                      type := XmlType.string, issuer := none, must_be_present := true },
-                  value := Value.primitive (XmlType.string, "Student") }]]]
-          req with
-    | MatchResult.is_match =>
-      simp [Target.eval]
-      simp [Policy.eval, Target.eval]
-      simp [RuleCombinatorAlgorithm.eval_legacy_permit_overrides, PolicyCombinatorAlgorithm.eval_legacy_permit_overrides]
-      intro h
-      repeat' apply And.intro
-      all_goals { intro hbad
-                  simp [hbad] at h }
-    | MatchResult.no_match =>
-      simp [Target.eval]
-      intro h
-      repeat' apply And.intro
-      all_goals { intro hbad
-                  simp [hbad] at h }
-    | MatchResult.indeterminate => sorry
-  | (Decision'.deny, _) =>
-    simp [PolicyElement.eval, PolicySet.eval]
-    match Target.eval
-          [[[{ function := "urn:oasis:names:tc:xacml:1.0:function:string-equal",
-                  designator :=
-                    { category := "urn:oasis:names:tc:xacml:3.0:attribute-category:subject", identifier := "role",
-                      type := XmlType.string, issuer := none, must_be_present := true },
-                  value := Value.primitive (XmlType.string, "Student") }]]]
-          req with
-    | MatchResult.is_match =>
-      simp [Target.eval]
-      simp [Policy.eval, Target.eval]
-      simp [RuleCombinatorAlgorithm.eval_legacy_permit_overrides, PolicyCombinatorAlgorithm.eval_legacy_permit_overrides]
-      intro h
-      repeat' apply And.intro
-      all_goals { intro hbad
-                  simp [hbad] at h }
-    | MatchResult.no_match =>
-      simp [Target.eval]
-      intro h
-      repeat' apply And.intro
-      all_goals { intro hbad
-                  simp [hbad] at h }
-    | MatchResult.indeterminate => sorry
-  | (Decision'.not_applicable, _) =>
-    simp [PolicyElement.eval, PolicySet.eval]
-    match Target.eval
-          [[[{ function := "urn:oasis:names:tc:xacml:1.0:function:string-equal",
-                  designator :=
-                    { category := "urn:oasis:names:tc:xacml:3.0:attribute-category:subject", identifier := "role",
-                      type := XmlType.string, issuer := none, must_be_present := true },
-                  value := Value.primitive (XmlType.string, "Student") }]]]
-          req with
-    | MatchResult.is_match =>
-      simp [Target.eval]
-      simp [Policy.eval, Target.eval]
-      simp [RuleCombinatorAlgorithm.eval_legacy_permit_overrides, PolicyCombinatorAlgorithm.eval_legacy_permit_overrides]
-      intro h
-      repeat' apply And.intro
-      all_goals { intro hbad
-                  simp [hbad] at h }
-    | MatchResult.no_match =>
-      simp [Target.eval]
-      intro h
-      repeat' apply And.intro
-      all_goals { intro hbad
-                  simp [hbad] at h }
-    | MatchResult.indeterminate => sorry
-  | (Decision'.indeterminate, _) => sorry
-  | (Decision'.indeterminate_d, _) => sorry
-  | (Decision'.indeterminate_p, _) => sorry
-  | (Decision'.indeterminate_dp, _) => sorry
-
-
 theorem not_applicable_no_effect (xs : List Decision') :
   PolicyCombinatorAlgorithm.eval_legacy_permit_overrides xs =
   PolicyCombinatorAlgorithm.eval_legacy_permit_overrides (xs ++ [Decision'.not_applicable]) := by
@@ -2205,9 +2218,6 @@ theorem not_applicable_no_effect (xs : List Decision') :
       | nil => simp [h]
       | cons head tail ih =>
         simp [List.contains_cons]
-        -- match (x == head) with
-        -- | true => simp
-        -- | false => simp
 
         cases Classical.em (x == head) with
         | inl h' =>
@@ -2248,12 +2258,10 @@ theorem pr' :
   | inl h =>
     rw_local
       (ElementTree.eval' req compiled_RPSStudent100_element []).1 = Decision'.not_applicable
-      -- by apply student_not_applicable req (separation_of_duty_imp_other_role_not_in_req req "TA" "Student" hsod (by simp) h)
-      by apply student_not_applicable req (separation_of_duty_imp_other_role_not_in_req req "TA" "Student" hsod (by sorry) h)
+      by apply student_not_applicable req hsod hwf (separation_of_duty_imp_other_role_not_in_req req "TA" "Student" hsod (by exact (bne_iff_ne "TA" "Student").mp rfl) h)
     rw_local
       (ElementTree.eval' req compiled_RPSFaculty100_element []).1 = Decision'.not_applicable
-      -- by apply faculty_not_applicable req (separation_of_duty_imp_other_role_not_in_req req "TA" "Faculty" hsod (by simp) h)
-      by apply faculty_not_applicable req (separation_of_duty_imp_other_role_not_in_req req "TA" "Faculty" hsod (by sorry) h)
+      by apply faculty_not_applicable req hsod hwf (separation_of_duty_imp_other_role_not_in_req req "TA" "Faculty" hsod (by exact (bne_iff_ne "TA" "Faculty").mp rfl) h)
     rw_local
       (ElementTree.eval' req compiled_RPSTA100_element' []).1 = Decision'.not_applicable
       by apply ta_external_grades_not_applicable req h hres
@@ -2262,7 +2270,7 @@ theorem pr' :
   | inr h =>
     rw_local
       (ElementTree.eval' req compiled_RPSTA100_element' []).1 = Decision'.not_applicable
-      by apply ta_not_applicable req h
+      by apply ta_not_applicable req hsod hwf h
     rw [not_applicable_no_effect']
 
 theorem pr :