Merge pull request #38 from minkiminki/grespectful

More general respectful functor
snu-sf · Feb 1, 2021 · 492819f · 492819f
2 parents 1f078cb + 1f96823
commit 492819f
Show file tree

Hide file tree

Showing 16 changed files with 928 additions and 0 deletions.
diff --git a/metasrc/gpaco.py b/metasrc/gpaco.py
@@ -679,6 +679,16 @@
 print ("        clo l <"+str(n)+"= paco"+str(n)+" gf (r \\"+str(n)+"/ clo r);")
 print ("    }.")
 print ("")
+print ("Structure grespectful"+str(n)+" (clo: rel -> rel) : Prop :=")
+print ("  grespect"+str(n)+"_intro {")
+print ("      grespect"+str(n)+"_mon: monotone"+str(n)+" clo;")
+print ("      grespect"+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)+"= rclo"+str(n)+" (cpn"+str(n)+" gf) (gf (rclo"+str(n)+" (clo \\"+str(n+1)+"/ gupaco"+str(n)+" gf (cpn"+str(n)+" gf)) r));")
+print ("    }.")
+print ("")
 print ("Definition gf'"+str(n)+" := id /"+str(n+1)+"\\ gf.")
 print ("")
 print ("Definition compatible'"+str(n)+" := compatible"+str(n)+" gf'"+str(n)+".")
@@ -729,6 +739,38 @@
 print ("        eapply RES, H; intros; apply PR.")
 print ("Qed.")
 print ("")
+print ("Lemma grespect"+str(n)+"_compatible'")
+print ("      clo (RES: grespectful"+str(n)+" clo):")
+print ("  compatible'"+str(n)+" (rclo"+str(n)+" (clo \\"+str(n+1)+"/ cpn"+str(n)+" gf)).")
+print ("Proof.")
+print ("  apply wrespect"+str(n)+"_compatible'.")
+print ("  econstructor.")
+print ("  { red; intros. destruct IN.")
+print ("    - left. eapply RES; [apply H|]. apply LE.")
+print ("    - right. eapply cpn"+str(n)+"_mon; [apply H|]. apply LE. }")
+print ("  intros. destruct PR.")
+print ("  - eapply RES.(grespect"+str(n)+"_respect) in H; [|apply LE|apply GF].")
+print ("    apply (@compat"+str(n)+"_compat gf (rclo"+str(n)+" (cpn"+str(n)+" gf))) in H.")
+print ("    2: { apply rclo"+str(n)+"_compat; [apply gf_mon|]. apply cpn"+str(n)+"_compat. apply gf_mon. }")
+print ("    eapply gf_mon; [apply H|].")
+print ("    intros. apply rclo"+str(n)+"_clo. right.")
+print ("    exists (rclo"+str(n)+" (cpn"+str(n)+" gf)).")
+print ("    { apply rclo"+str(n)+"_compat; [apply gf_mon|]. apply cpn"+str(n)+"_compat. apply gf_mon. }")
+print ("    eapply rclo"+str(n)+"_mon; [eapply PR|].")
+print ("    intros. eapply rclo"+str(n)+"_mon_gen; [eapply PR0|..].")
+print ("    + intros. destruct PR1.")
+print ("      * left. apply H0.")
+print ("      * right. apply cpn"+str(n)+"_gupaco; [apply gf_mon|apply H0].")
+print ("    + intros. apply PR1.")
+print ("  - eapply gf_mon.")
+print ("    + apply (@compat"+str(n)+"_compat gf (rclo"+str(n)+" (cpn"+str(n)+" gf))).")
+print ("      { apply rclo"+str(n)+"_compat; [apply gf_mon|]. apply cpn"+str(n)+"_compat. apply gf_mon. }")
+print ("      eapply rclo"+str(n)+"_clo_base. eapply cpn"+str(n)+"_mon; [apply H|apply GF].")
+print ("    + intros. eapply rclo"+str(n)+"_mon_gen; [eapply PR|..].")
+print ("      * intros. right. apply PR0.")
+print ("      * intros. apply PR0.")
+print ("Qed.")
+print ("")
 print ("Lemma compat"+str(n)+"_compatible'")
 print ("      clo (COM: compatible"+str(n)+" gf clo):")
 print ("  compatible'"+str(n)+" clo.")
@@ -787,6 +829,15 @@
 print ("  right. right. apply PR.")
 print ("Qed.")
 print ("")
+print ("Lemma grespect"+str(n)+"_companion")
+print ("      clo (RES: grespectful"+str(n)+" clo):")
+print ("  clo <"+str(n+1)+"= cpn"+str(n)+" gf.")
+print ("Proof.")
+print ("  intros. eapply grespect"+str(n)+"_compatible' in RES.")
+print ("  eapply (@compatible'"+str(n)+"_companion (rclo"+str(n)+" (clo \\"+str(n+1)+"/ cpn"+str(n)+" gf))); [apply RES|].")
+print ("  apply rclo"+str(n)+"_clo_base. left. 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).")
@@ -801,6 +852,13 @@
 print ("  intros. eapply gpaco"+str(n)+"_clo, prespect"+str(n)+"_companion, PR. apply RES.")
 print ("Qed.")
 print ("")
+print ("Lemma grespect"+str(n)+"_uclo")
+print ("      clo (RES: grespectful"+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, grespect"+str(n)+"_companion, PR. apply RES.")
+print ("Qed.")
+print ("")
 print ("End Respectful.")
 print ("")
 print ("End GeneralizedPaco"+str(n)+".")

diff --git a/src/gpaco0.v b/src/gpaco0.v
@@ -666,6 +666,16 @@ Structure prespectful0 (clo: rel -> rel) : Prop :=
         clo l <0= paco0 gf (r \0/ clo r);
     }.
 
+Structure grespectful0 (clo: rel -> rel) : Prop :=
+  grespect0_intro {
+      grespect0_mon: monotone0 clo;
+      grespect0_respect :
+        forall l r
+               (LE: l <0= r)
+               (GF: l <0= gf r),
+        clo l <0= rclo0 (cpn0 gf) (gf (rclo0 (clo \1/ gupaco0 gf (cpn0 gf)) r));
+    }.
+
 Definition gf'0 := id /1\ gf.
 
 Definition compatible'0 := compatible0 gf'0.
@@ -716,6 +726,38 @@ Proof.
         eapply RES, H; intros; apply PR.
 Qed.
 
+Lemma grespect0_compatible'
+      clo (RES: grespectful0 clo):
+  compatible'0 (rclo0 (clo \1/ cpn0 gf)).
+Proof.
+  apply wrespect0_compatible'.
+  econstructor.
+  { red; intros. destruct IN.
+    - left. eapply RES; [apply H|]. apply LE.
+    - right. eapply cpn0_mon; [apply H|]. apply LE. }
+  intros. destruct PR.
+  - eapply RES.(grespect0_respect) in H; [|apply LE|apply GF].
+    apply (@compat0_compat gf (rclo0 (cpn0 gf))) in H.
+    2: { apply rclo0_compat; [apply gf_mon|]. apply cpn0_compat. apply gf_mon. }
+    eapply gf_mon; [apply H|].
+    intros. apply rclo0_clo. right.
+    exists (rclo0 (cpn0 gf)).
+    { apply rclo0_compat; [apply gf_mon|]. apply cpn0_compat. apply gf_mon. }
+    eapply rclo0_mon; [eapply PR|].
+    intros. eapply rclo0_mon_gen; [eapply PR0|..].
+    + intros. destruct PR1.
+      * left. apply H0.
+      * right. apply cpn0_gupaco; [apply gf_mon|apply H0].
+    + intros. apply PR1.
+  - eapply gf_mon.
+    + apply (@compat0_compat gf (rclo0 (cpn0 gf))).
+      { apply rclo0_compat; [apply gf_mon|]. apply cpn0_compat. apply gf_mon. }
+      eapply rclo0_clo_base. eapply cpn0_mon; [apply H|apply GF].
+    + intros. eapply rclo0_mon_gen; [eapply PR|..].
+      * intros. right. apply PR0.
+      * intros. apply PR0.
+Qed.
+
 Lemma compat0_compatible'
       clo (COM: compatible0 gf clo):
   compatible'0 clo.
@@ -774,6 +816,15 @@ Proof.
   right. right. apply PR.
 Qed.
 
+Lemma grespect0_companion
+      clo (RES: grespectful0 clo):
+  clo <1= cpn0 gf.
+Proof.
+  intros. eapply grespect0_compatible' in RES.
+  eapply (@compatible'0_companion (rclo0 (clo \1/ cpn0 gf))); [apply RES|].
+  apply rclo0_clo_base. left. apply PR.
+Qed.
+
 Lemma wrespect0_uclo
       clo (RES: wrespectful0 clo):
   clo <1= gupaco0 gf (cpn0 gf).
@@ -788,6 +839,13 @@ Proof.
   intros. eapply gpaco0_clo, prespect0_companion, PR. apply RES.
 Qed.
 
+Lemma grespect0_uclo
+      clo (RES: grespectful0 clo):
+  clo <1= gupaco0 gf (cpn0 gf).
+Proof.
+  intros. eapply gpaco0_clo, grespect0_companion, PR. apply RES.
+Qed.
+
 End Respectful.
 
 End GeneralizedPaco0.

diff --git a/src/gpaco1.v b/src/gpaco1.v
@@ -667,6 +667,16 @@ Structure prespectful1 (clo: rel -> rel) : Prop :=
         clo l <1= paco1 gf (r \1/ clo r);
     }.
 
+Structure grespectful1 (clo: rel -> rel) : Prop :=
+  grespect1_intro {
+      grespect1_mon: monotone1 clo;
+      grespect1_respect :
+        forall l r
+               (LE: l <1= r)
+               (GF: l <1= gf r),
+        clo l <1= rclo1 (cpn1 gf) (gf (rclo1 (clo \2/ gupaco1 gf (cpn1 gf)) r));
+    }.
+
 Definition gf'1 := id /2\ gf.
 
 Definition compatible'1 := compatible1 gf'1.
@@ -717,6 +727,38 @@ Proof.
         eapply RES, H; intros; apply PR.
 Qed.
 
+Lemma grespect1_compatible'
+      clo (RES: grespectful1 clo):
+  compatible'1 (rclo1 (clo \2/ cpn1 gf)).
+Proof.
+  apply wrespect1_compatible'.
+  econstructor.
+  { red; intros. destruct IN.
+    - left. eapply RES; [apply H|]. apply LE.
+    - right. eapply cpn1_mon; [apply H|]. apply LE. }
+  intros. destruct PR.
+  - eapply RES.(grespect1_respect) in H; [|apply LE|apply GF].
+    apply (@compat1_compat gf (rclo1 (cpn1 gf))) in H.
+    2: { apply rclo1_compat; [apply gf_mon|]. apply cpn1_compat. apply gf_mon. }
+    eapply gf_mon; [apply H|].
+    intros. apply rclo1_clo. right.
+    exists (rclo1 (cpn1 gf)).
+    { apply rclo1_compat; [apply gf_mon|]. apply cpn1_compat. apply gf_mon. }
+    eapply rclo1_mon; [eapply PR|].
+    intros. eapply rclo1_mon_gen; [eapply PR0|..].
+    + intros. destruct PR1.
+      * left. apply H0.
+      * right. apply cpn1_gupaco; [apply gf_mon|apply H0].
+    + intros. apply PR1.
+  - eapply gf_mon.
+    + apply (@compat1_compat gf (rclo1 (cpn1 gf))).
+      { apply rclo1_compat; [apply gf_mon|]. apply cpn1_compat. apply gf_mon. }
+      eapply rclo1_clo_base. eapply cpn1_mon; [apply H|apply GF].
+    + intros. eapply rclo1_mon_gen; [eapply PR|..].
+      * intros. right. apply PR0.
+      * intros. apply PR0.
+Qed.
+
 Lemma compat1_compatible'
       clo (COM: compatible1 gf clo):
   compatible'1 clo.
@@ -775,6 +817,15 @@ Proof.
   right. right. apply PR.
 Qed.
 
+Lemma grespect1_companion
+      clo (RES: grespectful1 clo):
+  clo <2= cpn1 gf.
+Proof.
+  intros. eapply grespect1_compatible' in RES.
+  eapply (@compatible'1_companion (rclo1 (clo \2/ cpn1 gf))); [apply RES|].
+  apply rclo1_clo_base. left. apply PR.
+Qed.
+
 Lemma wrespect1_uclo
       clo (RES: wrespectful1 clo):
   clo <2= gupaco1 gf (cpn1 gf).
@@ -789,6 +840,13 @@ Proof.
   intros. eapply gpaco1_clo, prespect1_companion, PR. apply RES.
 Qed.
 
+Lemma grespect1_uclo
+      clo (RES: grespectful1 clo):
+  clo <2= gupaco1 gf (cpn1 gf).
+Proof.
+  intros. eapply gpaco1_clo, grespect1_companion, PR. apply RES.
+Qed.
+
 End Respectful.
 
 End GeneralizedPaco1.

diff --git a/src/gpaco10.v b/src/gpaco10.v
@@ -676,6 +676,16 @@ Structure prespectful10 (clo: rel -> rel) : Prop :=
         clo l <10= paco10 gf (r \10/ clo r);
     }.
 
+Structure grespectful10 (clo: rel -> rel) : Prop :=
+  grespect10_intro {
+      grespect10_mon: monotone10 clo;
+      grespect10_respect :
+        forall l r
+               (LE: l <10= r)
+               (GF: l <10= gf r),
+        clo l <10= rclo10 (cpn10 gf) (gf (rclo10 (clo \11/ gupaco10 gf (cpn10 gf)) r));
+    }.
+
 Definition gf'10 := id /11\ gf.
 
 Definition compatible'10 := compatible10 gf'10.
@@ -726,6 +736,38 @@ Proof.
         eapply RES, H; intros; apply PR.
 Qed.
 
+Lemma grespect10_compatible'
+      clo (RES: grespectful10 clo):
+  compatible'10 (rclo10 (clo \11/ cpn10 gf)).
+Proof.
+  apply wrespect10_compatible'.
+  econstructor.
+  { red; intros. destruct IN.
+    - left. eapply RES; [apply H|]. apply LE.
+    - right. eapply cpn10_mon; [apply H|]. apply LE. }
+  intros. destruct PR.
+  - eapply RES.(grespect10_respect) in H; [|apply LE|apply GF].
+    apply (@compat10_compat gf (rclo10 (cpn10 gf))) in H.
+    2: { apply rclo10_compat; [apply gf_mon|]. apply cpn10_compat. apply gf_mon. }
+    eapply gf_mon; [apply H|].
+    intros. apply rclo10_clo. right.
+    exists (rclo10 (cpn10 gf)).
+    { apply rclo10_compat; [apply gf_mon|]. apply cpn10_compat. apply gf_mon. }
+    eapply rclo10_mon; [eapply PR|].
+    intros. eapply rclo10_mon_gen; [eapply PR0|..].
+    + intros. destruct PR1.
+      * left. apply H0.
+      * right. apply cpn10_gupaco; [apply gf_mon|apply H0].
+    + intros. apply PR1.
+  - eapply gf_mon.
+    + apply (@compat10_compat gf (rclo10 (cpn10 gf))).
+      { apply rclo10_compat; [apply gf_mon|]. apply cpn10_compat. apply gf_mon. }
+      eapply rclo10_clo_base. eapply cpn10_mon; [apply H|apply GF].
+    + intros. eapply rclo10_mon_gen; [eapply PR|..].
+      * intros. right. apply PR0.
+      * intros. apply PR0.
+Qed.
+
 Lemma compat10_compatible'
       clo (COM: compatible10 gf clo):
   compatible'10 clo.
@@ -784,6 +826,15 @@ Proof.
   right. right. apply PR.
 Qed.
 
+Lemma grespect10_companion
+      clo (RES: grespectful10 clo):
+  clo <11= cpn10 gf.
+Proof.
+  intros. eapply grespect10_compatible' in RES.
+  eapply (@compatible'10_companion (rclo10 (clo \11/ cpn10 gf))); [apply RES|].
+  apply rclo10_clo_base. left. apply PR.
+Qed.
+
 Lemma wrespect10_uclo
       clo (RES: wrespectful10 clo):
   clo <11= gupaco10 gf (cpn10 gf).
@@ -798,6 +849,13 @@ Proof.
   intros. eapply gpaco10_clo, prespect10_companion, PR. apply RES.
 Qed.
 
+Lemma grespect10_uclo
+      clo (RES: grespectful10 clo):
+  clo <11= gupaco10 gf (cpn10 gf).
+Proof.
+  intros. eapply gpaco10_clo, grespect10_companion, PR. apply RES.
+Qed.
+
 End Respectful.
 
 End GeneralizedPaco10.