From 430f7f16fa8c6ae858b44a650324ab9958dfcd99 Mon Sep 17 00:00:00 2001
From: Jakob L. Kreuze
Date: Thu, 21 Dec 2023 14:30:43 -0500
Subject: s/simp/rfl/ where necessary

---
 xacml-proofs/lean/Xacml.lean | 22 +++++++++++-----------
 1 file changed, 11 insertions(+), 11 deletions(-)

diff --git a/xacml-proofs/lean/Xacml.lean b/xacml-proofs/lean/Xacml.lean
index 439b867..349b817 100644
--- a/xacml-proofs/lean/Xacml.lean
+++ b/xacml-proofs/lean/Xacml.lean
@@ -1813,11 +1813,11 @@ theorem pr₁ :
   ∧ req.contains (Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:resource" "resource-class" none (XmlType.string, "ExternalGrades"))
   ∧ (ElementTree.eval req compiled_college100_element).fst == Decision'.permit := by
   have h₁ : bad_req.contains (Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:subject"  "role"           none (XmlType.string, "Student")) := by
-    { simp }
+    { rfl }
   have h₂ : bad_req.contains (Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:action"   "command"        none (XmlType.string, "Assign")) := by
-    { simp }
+    { rfl }
   have h₃ : bad_req.contains (Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:resource" "resource-class" none (XmlType.string, "ExternalGrades")) := by
-    { simp }
+    { rfl }
 
   apply Exists.intro bad_req
   apply And.intro
@@ -1870,11 +1870,11 @@ theorem pr₃ :
    { apply Exists.intro bad_req₀
 
      have h₁ : bad_req₀.contains (Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:subject"  "role"           none (XmlType.string, "Student")) := by
-       { simp }
+       { rfl }
      have h₂ : bad_req₀.contains (Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:action"   "command"        none (XmlType.string, "Receive")) := by
-       { simp }
-     have h₃ : bad_req₀.contains (Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:resource" "resource-class" none (XmlType.string, "ExternalGrades")) := by
-       { simp }
+       { rfl }
+     -- have h₃ : bad_req₀.contains (Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:resource" "resource-class" none (XmlType.string, "ExternalGrades")) := by
+     --   { rfl }
 
      apply And.intro
      { rw_local
@@ -1888,11 +1888,11 @@ theorem pr₃ :
    { apply Exists.intro bad_req₁
 
      have h₁ : bad_req₁.contains (Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:subject"  "role"           none (XmlType.string, "Student")) := by
-       { simp }
+       { rfl }
      have h₂ : bad_req₁.contains (Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:action"   "command"        none (XmlType.string, "Assign")) := by
-       { simp }
-     have h₃ : bad_req₁.contains (Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:resource" "resource-class" none (XmlType.string, "ExternalGrades")) := by
-       { simp }
+       { rfl }
+     -- have h₃ : bad_req₁.contains (Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:resource" "resource-class" none (XmlType.string, "ExternalGrades")) := by
+     --   { rfl }
 
      apply And.intro
      { rw_local
-- 
cgit v1.3