From a73411ab7cd9afa7d0da1f25f3fcc585aa27a292 Mon Sep 17 00:00:00 2001
From: Junyoung/Clare Jang <jjc9310@gmail.com>
Date: Mon, 6 May 2024 01:25:49 -0400
Subject: [PATCH] Finish all PERs

---
 theories/Core/Semantic/PERLemmas.v | 68 +++++++++++++++++++++++++++++-
 1 file changed, 66 insertions(+), 2 deletions(-)

diff --git a/theories/Core/Semantic/PERLemmas.v b/theories/Core/Semantic/PERLemmas.v
index 82737baa..681aef1d 100644
--- a/theories/Core/Semantic/PERLemmas.v
+++ b/theories/Core/Semantic/PERLemmas.v
@@ -64,6 +64,71 @@ Qed.
 #[export]
 Hint Resolve per_bot_trans : mcltt.
 
+Lemma PER_per_bot : PER per_bot.
+Proof with solve [mauto].
+  econstructor...
+Qed.
+
+Lemma per_top_sym : forall m n,
+    {{ Dom m ≈ n ∈ per_top }} ->
+    {{ Dom n ≈ m ∈ per_top }}.
+Proof with solve [mauto].
+  intros * H s.
+  destruct (H s) as [? []]...
+Qed.
+
+#[export]
+Hint Resolve per_top_sym : mcltt.
+
+Lemma per_top_trans : forall m n l,
+    {{ Dom m ≈ n ∈ per_top }} ->
+    {{ Dom n ≈ l ∈ per_top }} ->
+    {{ Dom m ≈ l ∈ per_top }}.
+Proof with solve [mauto].
+  intros * Hmn Hnl s.
+  destruct (Hmn s) as [? []].
+  destruct (Hnl s) as [? []].
+  functional_read_rewrite_clear...
+Qed.
+
+#[export]
+Hint Resolve per_top_trans : mcltt.
+
+Lemma PER_per_top : PER per_top.
+Proof with solve [mauto].
+  econstructor...
+Qed.
+
+Lemma per_top_typ_sym : forall m n,
+    {{ Dom m ≈ n ∈ per_top_typ }} ->
+    {{ Dom n ≈ m ∈ per_top_typ }}.
+Proof with solve [mauto].
+  intros * H s.
+  destruct (H s) as [? []]...
+Qed.
+
+#[export]
+Hint Resolve per_top_typ_sym : mcltt.
+
+Lemma per_top_typ_trans : forall m n l,
+    {{ Dom m ≈ n ∈ per_top_typ }} ->
+    {{ Dom n ≈ l ∈ per_top_typ }} ->
+    {{ Dom m ≈ l ∈ per_top_typ }}.
+Proof with solve [mauto].
+  intros * Hmn Hnl s.
+  destruct (Hmn s) as [? []].
+  destruct (Hnl s) as [? []].
+  functional_read_rewrite_clear...
+Qed.
+
+#[export]
+Hint Resolve per_top_typ_trans : mcltt.
+
+Lemma PER_per_top_typ : PER per_top_typ.
+Proof with solve [mauto].
+  econstructor...
+Qed.
+
 Lemma per_nat_sym : forall m n,
     {{ Dom m ≈ n ∈ per_nat }} ->
     {{ Dom n ≈ m ∈ per_nat }}.
@@ -154,7 +219,7 @@ Lemma per_univ_elem_sym : forall i A B R,
     per_univ_elem i A B R ->
     per_univ_elem i B A R /\ (forall a b, {{ Dom a ≈ b ∈ R }} <-> {{ Dom b ≈ a ∈ R }}).
 Proof.
-  intros. induction H using per_univ_elem_ind; subst.
+  induction 1 using per_univ_elem_ind; subst.
   - split.
     + apply per_univ_elem_core_univ'; trivial.
     + intros. split; intros [].
@@ -177,7 +242,6 @@ Proof.
       functional_eval_rewrite_clear.
       per_univ_elem_right_irrel_rewrite.
       assumption.
-
     + assert (forall a b : domain,
                  (forall (c c' : domain) (equiv_c_c' : in_rel c c'), rel_mod_app (out_rel c c' equiv_c_c') a c b c') ->
                  (forall (c c' : domain) (equiv_c_c' : in_rel c c'), rel_mod_app (out_rel c c' equiv_c_c') b c a c')).