Add the "prespectful" closure, which is another version of weak

respectful.
snu-sf · Oct 4, 2020 · 0a4f42b · 0a4f42b
1 parent e27d57b
commit 0a4f42b
Show file tree

Hide file tree

Showing 16 changed files with 912 additions and 0 deletions.
diff --git a/metasrc/gpaco.py b/metasrc/gpaco.py
@@ -670,6 +670,17 @@
 print ("    }.")
 print ("Hint Constructors wrespectful"+str(n)+".")
 print ("")
+print ("Structure prespectful"+str(n)+" (clo: rel -> rel) : Prop :=")
+print ("  prespect"+str(n)+"_intro {")
+print ("      prespect"+str(n)+"_mon: monotone"+str(n)+" clo;")
+print ("      prespect"+str(n)+"_respect :")
+print ("        forall l r")
+print ("               (LE: l <"+str(n)+"= r)")
+print ("               (GF: l <"+str(n)+"= gf r),")
+print ("        clo l <"+str(n)+"= paco"+str(n)+" gf (r \\"+str(n)+"/ clo r);")
+print ("    }.")
+print ("Hint Constructors prespectful"+str(n)+".")
+print ("")
 print ("Definition gf'"+str(n)+" := id /"+str(n+1)+"\\ gf.")
 print ("")
 print ("Definition compatible'"+str(n)+" := compatible"+str(n)+" gf'"+str(n)+".")
@@ -690,6 +701,36 @@
 print ("    + intros. apply rclo"+str(n)+"_rclo, PR.")
 print ("Qed.")
 print ("")
+print ("Lemma prespect"+str(n)+"_compatible'")
+print ("      clo (RES: prespectful"+str(n)+" clo):")
+print ("  compatible'"+str(n)+" (fun r => upaco"+str(n)+" gf (r \\"+str(n)+"/ clo r)).")
+print ("Proof.")
+print ("  econstructor.")
+print ("  { red; intros. eapply upaco"+str(n)+"_mon. apply IN.")
+print ("    intros. destruct PR.")
+print ("    - left. apply LE, H.")
+print ("    - right. eapply RES. apply H. intros. apply LE, PR. }")
+print ("")
+print ("  intros r.")
+print ("  assert (LEM: (gf'"+str(n)+" r \\"+str(n)+"/ clo (gf'"+str(n)+" r)) <"+str(n)+"= (r \\"+str(n)+"/ clo r)).")
+print ("  { intros. destruct PR.")
+print ("    - left. apply H.")
+print ("    - right. eapply RES. apply H. intros. apply PR.")
+print ("  }")
+print ("")
+print ("  intros. destruct PR.")
+print ("  - split.")
+print ("    + left. eapply paco"+str(n)+"_mon. apply H. apply LEM.")
+print ("    + apply paco"+str(n)+"_unfold; [apply gf_mon|].")
+print ("      eapply paco"+str(n)+"_mon. apply H. apply LEM.")
+print ("  - split.")
+print ("    + right. apply LEM. apply H.")
+print ("    + destruct H.")
+print ("      * eapply gf_mon. apply H. intros. right. left. apply PR.")
+print ("      * apply paco"+str(n)+"_unfold; [apply gf_mon|].")
+print ("        eapply RES, H; intros; apply PR.")
+print ("Qed.")
+print ("")
 print ("Lemma compat"+str(n)+"_compatible'")
 print ("      clo (COM: compatible"+str(n)+" gf clo):")
 print ("  compatible'"+str(n)+" clo.")
@@ -740,13 +781,28 @@
 print ("  eapply rclo"+str(n)+"_clo_base, PR.")
 print ("Qed.")
 print ("")
+print ("Lemma prespect"+str(n)+"_companion")
+print ("      clo (RES: prespectful"+str(n)+" clo):")
+print ("  clo <"+str(n+1)+"= cpn"+str(n)+" gf.")
+print ("Proof.")
+print ("  intros. eapply compatible'"+str(n)+"_companion. apply prespect"+str(n)+"_compatible'. apply RES.")
+print ("  right. right. apply PR.")
+print ("Qed.")
+print ("")
 print ("Lemma wrespect"+str(n)+"_uclo")
 print ("      clo (RES: wrespectful"+str(n)+" clo):")
 print ("  clo <"+str(n+1)+"= gupaco"+str(n)+" gf (cpn"+str(n)+" gf).")
 print ("Proof.")
 print ("  intros. eapply gpaco"+str(n)+"_clo, wrespect"+str(n)+"_companion, PR. apply RES.")
 print ("Qed.")
 print ("")
+print ("Lemma prespect"+str(n)+"_uclo")
+print ("      clo (RES: prespectful"+str(n)+" clo):")
+print ("  clo <"+str(n+1)+"= gupaco"+str(n)+" gf (cpn"+str(n)+" gf).")
+print ("Proof.")
+print ("  intros. eapply gpaco"+str(n)+"_clo, prespect"+str(n)+"_companion, PR. apply RES.")
+print ("Qed.")
+print ("")
 print ("End Respectful.")
 print ("")
 print ("End GeneralizedPaco"+str(n)+".")
@@ -759,3 +815,4 @@
 print ("Hint Resolve rclo"+str(n)+"_base : paco.")
 print ("Hint Constructors gpaco"+str(n)+" : paco.")
 print ("Hint Resolve wrespect"+str(n)+"_uclo : paco.")
+print ("Hint Resolve prespect"+str(n)+"_uclo : paco.")
diff --git a/src/gpaco0.v b/src/gpaco0.v
@@ -657,6 +657,17 @@ Structure wrespectful0 (clo: rel -> rel) : Prop :=
     }.
 Hint Constructors wrespectful0.
 
+Structure prespectful0 (clo: rel -> rel) : Prop :=
+  prespect0_intro {
+      prespect0_mon: monotone0 clo;
+      prespect0_respect :
+        forall l r
+               (LE: l <0= r)
+               (GF: l <0= gf r),
+        clo l <0= paco0 gf (r \0/ clo r);
+    }.
+Hint Constructors prespectful0.
+
 Definition gf'0 := id /1\ gf.
 
 Definition compatible'0 := compatible0 gf'0.
@@ -677,6 +688,36 @@ Proof.
     + intros. apply rclo0_rclo, PR.
 Qed.
 
+Lemma prespect0_compatible'
+      clo (RES: prespectful0 clo):
+  compatible'0 (fun r => upaco0 gf (r \0/ clo r)).
+Proof.
+  econstructor.
+  { red; intros. eapply upaco0_mon. apply IN.
+    intros. destruct PR.
+    - left. apply LE, H.
+    - right. eapply RES. apply H. intros. apply LE, PR. }
+
+  intros r.
+  assert (LEM: (gf'0 r \0/ clo (gf'0 r)) <0= (r \0/ clo r)).
+  { intros. destruct PR.
+    - left. apply H.
+    - right. eapply RES. apply H. intros. apply PR.
+  }
+
+  intros. destruct PR.
+  - split.
+    + left. eapply paco0_mon. apply H. apply LEM.
+    + apply paco0_unfold; [apply gf_mon|].
+      eapply paco0_mon. apply H. apply LEM.
+  - split.
+    + right. apply LEM. apply H.
+    + destruct H.
+      * eapply gf_mon. apply H. intros. right. left. apply PR.
+      * apply paco0_unfold; [apply gf_mon|].
+        eapply RES, H; intros; apply PR.
+Qed.
+
 Lemma compat0_compatible'
       clo (COM: compatible0 gf clo):
   compatible'0 clo.
@@ -727,13 +768,28 @@ Proof.
   eapply rclo0_clo_base, PR.
 Qed.
 
+Lemma prespect0_companion
+      clo (RES: prespectful0 clo):
+  clo <1= cpn0 gf.
+Proof.
+  intros. eapply compatible'0_companion. apply prespect0_compatible'. apply RES.
+  right. right. apply PR.
+Qed.
+
 Lemma wrespect0_uclo
       clo (RES: wrespectful0 clo):
   clo <1= gupaco0 gf (cpn0 gf).
 Proof.
   intros. eapply gpaco0_clo, wrespect0_companion, PR. apply RES.
 Qed.
 
+Lemma prespect0_uclo
+      clo (RES: prespectful0 clo):
+  clo <1= gupaco0 gf (cpn0 gf).
+Proof.
+  intros. eapply gpaco0_clo, prespect0_companion, PR. apply RES.
+Qed.
+
 End Respectful.
 
 End GeneralizedPaco0.
@@ -746,3 +802,4 @@ Hint Resolve gpaco0_final : paco.
 Hint Resolve rclo0_base : paco.
 Hint Constructors gpaco0 : paco.
 Hint Resolve wrespect0_uclo : paco.
+Hint Resolve prespect0_uclo : paco.
diff --git a/src/gpaco1.v b/src/gpaco1.v
@@ -658,6 +658,17 @@ Structure wrespectful1 (clo: rel -> rel) : Prop :=
     }.
 Hint Constructors wrespectful1.
 
+Structure prespectful1 (clo: rel -> rel) : Prop :=
+  prespect1_intro {
+      prespect1_mon: monotone1 clo;
+      prespect1_respect :
+        forall l r
+               (LE: l <1= r)
+               (GF: l <1= gf r),
+        clo l <1= paco1 gf (r \1/ clo r);
+    }.
+Hint Constructors prespectful1.
+
 Definition gf'1 := id /2\ gf.
 
 Definition compatible'1 := compatible1 gf'1.
@@ -678,6 +689,36 @@ Proof.
     + intros. apply rclo1_rclo, PR.
 Qed.
 
+Lemma prespect1_compatible'
+      clo (RES: prespectful1 clo):
+  compatible'1 (fun r => upaco1 gf (r \1/ clo r)).
+Proof.
+  econstructor.
+  { red; intros. eapply upaco1_mon. apply IN.
+    intros. destruct PR.
+    - left. apply LE, H.
+    - right. eapply RES. apply H. intros. apply LE, PR. }
+
+  intros r.
+  assert (LEM: (gf'1 r \1/ clo (gf'1 r)) <1= (r \1/ clo r)).
+  { intros. destruct PR.
+    - left. apply H.
+    - right. eapply RES. apply H. intros. apply PR.
+  }
+
+  intros. destruct PR.
+  - split.
+    + left. eapply paco1_mon. apply H. apply LEM.
+    + apply paco1_unfold; [apply gf_mon|].
+      eapply paco1_mon. apply H. apply LEM.
+  - split.
+    + right. apply LEM. apply H.
+    + destruct H.
+      * eapply gf_mon. apply H. intros. right. left. apply PR.
+      * apply paco1_unfold; [apply gf_mon|].
+        eapply RES, H; intros; apply PR.
+Qed.
+
 Lemma compat1_compatible'
       clo (COM: compatible1 gf clo):
   compatible'1 clo.
@@ -728,13 +769,28 @@ Proof.
   eapply rclo1_clo_base, PR.
 Qed.
 
+Lemma prespect1_companion
+      clo (RES: prespectful1 clo):
+  clo <2= cpn1 gf.
+Proof.
+  intros. eapply compatible'1_companion. apply prespect1_compatible'. apply RES.
+  right. right. apply PR.
+Qed.
+
 Lemma wrespect1_uclo
       clo (RES: wrespectful1 clo):
   clo <2= gupaco1 gf (cpn1 gf).
 Proof.
   intros. eapply gpaco1_clo, wrespect1_companion, PR. apply RES.
 Qed.
 
+Lemma prespect1_uclo
+      clo (RES: prespectful1 clo):
+  clo <2= gupaco1 gf (cpn1 gf).
+Proof.
+  intros. eapply gpaco1_clo, prespect1_companion, PR. apply RES.
+Qed.
+
 End Respectful.
 
 End GeneralizedPaco1.
@@ -747,3 +803,4 @@ Hint Resolve gpaco1_final : paco.
 Hint Resolve rclo1_base : paco.
 Hint Constructors gpaco1 : paco.
 Hint Resolve wrespect1_uclo : paco.
+Hint Resolve prespect1_uclo : paco.
diff --git a/src/gpaco10.v b/src/gpaco10.v
@@ -667,6 +667,17 @@ Structure wrespectful10 (clo: rel -> rel) : Prop :=
     }.
 Hint Constructors wrespectful10.
 
+Structure prespectful10 (clo: rel -> rel) : Prop :=
+  prespect10_intro {
+      prespect10_mon: monotone10 clo;
+      prespect10_respect :
+        forall l r
+               (LE: l <10= r)
+               (GF: l <10= gf r),
+        clo l <10= paco10 gf (r \10/ clo r);
+    }.
+Hint Constructors prespectful10.
+
 Definition gf'10 := id /11\ gf.
 
 Definition compatible'10 := compatible10 gf'10.
@@ -687,6 +698,36 @@ Proof.
     + intros. apply rclo10_rclo, PR.
 Qed.
 
+Lemma prespect10_compatible'
+      clo (RES: prespectful10 clo):
+  compatible'10 (fun r => upaco10 gf (r \10/ clo r)).
+Proof.
+  econstructor.
+  { red; intros. eapply upaco10_mon. apply IN.
+    intros. destruct PR.
+    - left. apply LE, H.
+    - right. eapply RES. apply H. intros. apply LE, PR. }
+
+  intros r.
+  assert (LEM: (gf'10 r \10/ clo (gf'10 r)) <10= (r \10/ clo r)).
+  { intros. destruct PR.
+    - left. apply H.
+    - right. eapply RES. apply H. intros. apply PR.
+  }
+
+  intros. destruct PR.
+  - split.
+    + left. eapply paco10_mon. apply H. apply LEM.
+    + apply paco10_unfold; [apply gf_mon|].
+      eapply paco10_mon. apply H. apply LEM.
+  - split.
+    + right. apply LEM. apply H.
+    + destruct H.
+      * eapply gf_mon. apply H. intros. right. left. apply PR.
+      * apply paco10_unfold; [apply gf_mon|].
+        eapply RES, H; intros; apply PR.
+Qed.
+
 Lemma compat10_compatible'
       clo (COM: compatible10 gf clo):
   compatible'10 clo.
@@ -737,13 +778,28 @@ Proof.
   eapply rclo10_clo_base, PR.
 Qed.
 
+Lemma prespect10_companion
+      clo (RES: prespectful10 clo):
+  clo <11= cpn10 gf.
+Proof.
+  intros. eapply compatible'10_companion. apply prespect10_compatible'. apply RES.
+  right. right. apply PR.
+Qed.
+
 Lemma wrespect10_uclo
       clo (RES: wrespectful10 clo):
   clo <11= gupaco10 gf (cpn10 gf).
 Proof.
   intros. eapply gpaco10_clo, wrespect10_companion, PR. apply RES.
 Qed.
 
+Lemma prespect10_uclo
+      clo (RES: prespectful10 clo):
+  clo <11= gupaco10 gf (cpn10 gf).
+Proof.
+  intros. eapply gpaco10_clo, prespect10_companion, PR. apply RES.
+Qed.
+
 End Respectful.
 
 End GeneralizedPaco10.
@@ -756,3 +812,4 @@ Hint Resolve gpaco10_final : paco.
 Hint Resolve rclo10_base : paco.
 Hint Constructors gpaco10 : paco.
 Hint Resolve wrespect10_uclo : paco.
+Hint Resolve prespect10_uclo : paco.