Add the notatoin "cgres{n}".

snu-sf · Mar 4, 2019 · 4c32bcb · 4c32bcb
1 parent 7ddf313
commit 4c32bcb
Show file tree

Hide file tree

Showing 20 changed files with 261 additions and 160 deletions.
diff --git a/metasrc/upto.py b/metasrc/upto.py
@@ -276,8 +276,11 @@
 print ('Qed.')
 print ('')
 
+print ("Definition cgres"+str(n)+" := compose gf gres"+str(n)+".")
+print ("")
+
 print ('Lemma upto'+str(n)+'_init:')
-print ('  paco'+str(n)+' (compose gf gres'+str(n)+') bot'+str(n)+' <'+str(n)+'= paco'+str(n)+' gf bot'+str(n)+'.')
+print ('  paco'+str(n)+' cgres'+str(n)+' bot'+str(n)+' <'+str(n)+'= paco'+str(n)+' gf bot'+str(n)+'.')
 print ('Proof.')
 print ('  apply sound'+str(n)+'_is_gf.')
 print ('  apply respectful'+str(n)+'_is_sound'+str(n)+'.')
@@ -286,7 +289,7 @@
 print ('')
 
 print ('Lemma upto'+str(n)+'_final:')
-print ('  paco'+str(n)+' gf <'+str(n+1)+'= paco'+str(n)+' (compose gf gres'+str(n)+').')
+print ('  paco'+str(n)+' gf <'+str(n+1)+'= paco'+str(n)+' cgres'+str(n)+'.')
 print ('Proof.')
 print ('  pcofix CIH. intros. _punfold PR; [|apply gf_mon]. pfold.')
 print ('  eapply gf_mon; [|apply grespectful'+str(n)+'_incl].')
@@ -297,7 +300,7 @@
 
 print ('Lemma upto'+str(n)+'_step')
 print ('      r clo (RES: weak_respectful'+str(n)+' clo):')
-print ('  clo (paco'+str(n)+' (compose gf gres'+str(n)+') r) <'+str(n)+'= paco'+str(n)+' (compose gf gres'+str(n)+') r.')
+print ('  clo (paco'+str(n)+' cgres'+str(n)+' r) <'+str(n)+'= paco'+str(n)+' cgres'+str(n)+' r.')
 print ('Proof.')
 print ('  intros. apply grespectful'+str(n)+'_incl_rev.')
 print ('  assert (RES\' := weak_respectful'+str(n)+'_respectful'+str(n)+' RES).')
@@ -364,6 +367,7 @@
 print ('Hint Resolve grespectful'+str(n)+'_incl.')
 print ('Hint Resolve rclo'+str(n)+'_mon: paco.')
 print ('Hint Constructors weak_respectful'+str(n)+'.')
+print ('Hint Unfold cgres'+str(n)+'.')
 print ('')
 
 print ("(* User Tactics *)")
@@ -373,18 +377,20 @@
 print ('Ltac pupto'+str(n)+' H := first [eapply upto'+str(n)+'_step|eapply upto'+str(n)+'_step_under]; [|eapply H|]; [eauto with paco|].')
 print ('')
 print ("Ltac pfold"+str(n)+"_reverse_ :=")
-print ("    match goal with")
-print ("    | [|- ?gf (upaco"+str(n)+" _"*n+")"+" _"*n+"] => eapply (paco"+str(n)+"_unfold gf)")
-print ("    | [|- ?gf (?gres (upaco"+str(n)+" _"*n+"))"+" _"*n+"] => eapply (paco"+str(n)+"_unfold (gf:=compose gf gres))")
-print ("    end.")
+print ("  repeat red;")
+print ("  match goal with")
+print ("  | [|- ?gf (upaco"+str(n)+" _"*n+")"+" _"*n+"] => eapply (paco"+str(n)+"_unfold (gf := gf))")
+print ("  | [|- ?gf (?gres (upaco"+str(n)+" _"*n+"))"+" _"*n+"] => eapply (paco"+str(n)+"_unfold (gf := cgres"+str(n)+" gf))")
+print ("  end.")
 print ("")
 print ("Ltac pfold"+str(n)+"_reverse := pfold"+str(n)+"_reverse_; eauto with paco.")
 print ("")
 print ("Ltac punfold"+str(n)+"_reverse_ H :=")
+print ("  repeat red in H;")
 print ("  let PP := type of H in")
 print ("  match PP with")
 print ("  | ?gf (upaco"+str(n)+" _"*n+")"+" _"*n+" => eapply (paco"+str(n)+"_fold gf) in H")
-print ("  | ?gf (?gres (upaco"+str(n)+" _"*n+"))"+" _"*n+" => eapply (paco"+str(n)+"_fold (compose gf gres)) in H")
+print ("  | ?gf (?gres (upaco"+str(n)+" _"*n+"))"+" _"*n+" => eapply (paco"+str(n)+"_fold (cgres"+str(n)+" gf)) in H")
 print ("  end.")
 print ("")
 print ("Ltac punfold"+str(n)+"_reverse H := punfold"+str(n)+"_reverse_ H; eauto with paco.")

diff --git a/src/paco0_upto.v b/src/paco0_upto.v
@@ -234,16 +234,18 @@ Proof.
     intros. eapply rclo0_mon; [apply R', PR| apply LE].
 Qed.
 
+Definition cgres0 := compose gf gres0.
+
 Lemma upto0_init:
-  paco0 (compose gf gres0) bot0 <0= paco0 gf bot0.
+  paco0 cgres0 bot0 <0= paco0 gf bot0.
 Proof.
   apply sound0_is_gf.
   apply respectful0_is_sound0.
   apply grespectful0_respectful0.
 Qed.
 
 Lemma upto0_final:
-  paco0 gf <1= paco0 (compose gf gres0).
+  paco0 gf <1= paco0 cgres0.
 Proof.
   pcofix CIH. intros. _punfold PR; [|apply gf_mon]. pfold.
   eapply gf_mon; [|apply grespectful0_incl].
@@ -253,7 +255,7 @@ Qed.
 
 Lemma upto0_step
       r clo (RES: weak_respectful0 clo):
-  clo (paco0 (compose gf gres0) r) <0= paco0 (compose gf gres0) r.
+  clo (paco0 cgres0 r) <0= paco0 cgres0 r.
 Proof.
   intros. apply grespectful0_incl_rev.
   assert (RES' := weak_respectful0_respectful0 RES).
@@ -314,6 +316,7 @@ Hint Resolve gfgres0_mon : paco.
 Hint Resolve grespectful0_incl.
 Hint Resolve rclo0_mon: paco.
 Hint Constructors weak_respectful0.
+Hint Unfold cgres0.
 
 (* User Tactics *)
 
@@ -322,18 +325,20 @@ Ltac pupto0_final := first [eapply upto0_final; [eauto with paco|] | eapply gres
 Ltac pupto0 H := first [eapply upto0_step|eapply upto0_step_under]; [|eapply H|]; [eauto with paco|].
 
 Ltac pfold0_reverse_ :=
-    match goal with
-    | [|- ?gf (upaco0)] => eapply (paco0_unfold gf)
-    | [|- ?gf (?gres (upaco0))] => eapply (paco0_unfold (gf:=compose gf gres))
-    end.
+  repeat red;
+  match goal with
+  | [|- ?gf (upaco0)] => eapply (paco0_unfold (gf := gf))
+  | [|- ?gf (?gres (upaco0))] => eapply (paco0_unfold (gf := cgres0 gf))
+  end.
 
 Ltac pfold0_reverse := pfold0_reverse_; eauto with paco.
 
 Ltac punfold0_reverse_ H :=
+  repeat red in H;
   let PP := type of H in
   match PP with
   | ?gf (upaco0) => eapply (paco0_fold gf) in H
-  | ?gf (?gres (upaco0)) => eapply (paco0_fold (compose gf gres)) in H
+  | ?gf (?gres (upaco0)) => eapply (paco0_fold (cgres0 gf)) in H
   end.
 
 Ltac punfold0_reverse H := punfold0_reverse_ H; eauto with paco.

diff --git a/src/paco10_upto.v b/src/paco10_upto.v
@@ -244,16 +244,18 @@ Proof.
     intros. eapply rclo10_mon; [apply R', PR| apply LE].
 Qed.
 
+Definition cgres10 := compose gf gres10.
+
 Lemma upto10_init:
-  paco10 (compose gf gres10) bot10 <10= paco10 gf bot10.
+  paco10 cgres10 bot10 <10= paco10 gf bot10.
 Proof.
   apply sound10_is_gf.
   apply respectful10_is_sound10.
   apply grespectful10_respectful10.
 Qed.
 
 Lemma upto10_final:
-  paco10 gf <11= paco10 (compose gf gres10).
+  paco10 gf <11= paco10 cgres10.
 Proof.
   pcofix CIH. intros. _punfold PR; [|apply gf_mon]. pfold.
   eapply gf_mon; [|apply grespectful10_incl].
@@ -263,7 +265,7 @@ Qed.
 
 Lemma upto10_step
       r clo (RES: weak_respectful10 clo):
-  clo (paco10 (compose gf gres10) r) <10= paco10 (compose gf gres10) r.
+  clo (paco10 cgres10 r) <10= paco10 cgres10 r.
 Proof.
   intros. apply grespectful10_incl_rev.
   assert (RES' := weak_respectful10_respectful10 RES).
@@ -324,6 +326,7 @@ Hint Resolve gfgres10_mon : paco.
 Hint Resolve grespectful10_incl.
 Hint Resolve rclo10_mon: paco.
 Hint Constructors weak_respectful10.
+Hint Unfold cgres10.
 
 (* User Tactics *)
 
@@ -332,18 +335,20 @@ Ltac pupto10_final := first [eapply upto10_final; [eauto with paco|] | eapply gr
 Ltac pupto10 H := first [eapply upto10_step|eapply upto10_step_under]; [|eapply H|]; [eauto with paco|].
 
 Ltac pfold10_reverse_ :=
-    match goal with
-    | [|- ?gf (upaco10 _ _ _ _ _ _ _ _ _ _) _ _ _ _ _ _ _ _ _ _] => eapply (paco10_unfold gf)
-    | [|- ?gf (?gres (upaco10 _ _ _ _ _ _ _ _ _ _)) _ _ _ _ _ _ _ _ _ _] => eapply (paco10_unfold (gf:=compose gf gres))
-    end.
+  repeat red;
+  match goal with
+  | [|- ?gf (upaco10 _ _ _ _ _ _ _ _ _ _) _ _ _ _ _ _ _ _ _ _] => eapply (paco10_unfold (gf := gf))
+  | [|- ?gf (?gres (upaco10 _ _ _ _ _ _ _ _ _ _)) _ _ _ _ _ _ _ _ _ _] => eapply (paco10_unfold (gf := cgres10 gf))
+  end.
 
 Ltac pfold10_reverse := pfold10_reverse_; eauto with paco.
 
 Ltac punfold10_reverse_ H :=
+  repeat red in H;
   let PP := type of H in
   match PP with
   | ?gf (upaco10 _ _ _ _ _ _ _ _ _ _) _ _ _ _ _ _ _ _ _ _ => eapply (paco10_fold gf) in H
-  | ?gf (?gres (upaco10 _ _ _ _ _ _ _ _ _ _)) _ _ _ _ _ _ _ _ _ _ => eapply (paco10_fold (compose gf gres)) in H
+  | ?gf (?gres (upaco10 _ _ _ _ _ _ _ _ _ _)) _ _ _ _ _ _ _ _ _ _ => eapply (paco10_fold (cgres10 gf)) in H
   end.
 
 Ltac punfold10_reverse H := punfold10_reverse_ H; eauto with paco.

diff --git a/src/paco11_upto.v b/src/paco11_upto.v
@@ -245,16 +245,18 @@ Proof.
     intros. eapply rclo11_mon; [apply R', PR| apply LE].
 Qed.
 
+Definition cgres11 := compose gf gres11.
+
 Lemma upto11_init:
-  paco11 (compose gf gres11) bot11 <11= paco11 gf bot11.
+  paco11 cgres11 bot11 <11= paco11 gf bot11.
 Proof.
   apply sound11_is_gf.
   apply respectful11_is_sound11.
   apply grespectful11_respectful11.
 Qed.
 
 Lemma upto11_final:
-  paco11 gf <12= paco11 (compose gf gres11).
+  paco11 gf <12= paco11 cgres11.
 Proof.
   pcofix CIH. intros. _punfold PR; [|apply gf_mon]. pfold.
   eapply gf_mon; [|apply grespectful11_incl].
@@ -264,7 +266,7 @@ Qed.
 
 Lemma upto11_step
       r clo (RES: weak_respectful11 clo):
-  clo (paco11 (compose gf gres11) r) <11= paco11 (compose gf gres11) r.
+  clo (paco11 cgres11 r) <11= paco11 cgres11 r.
 Proof.
   intros. apply grespectful11_incl_rev.
   assert (RES' := weak_respectful11_respectful11 RES).
@@ -325,6 +327,7 @@ Hint Resolve gfgres11_mon : paco.
 Hint Resolve grespectful11_incl.
 Hint Resolve rclo11_mon: paco.
 Hint Constructors weak_respectful11.
+Hint Unfold cgres11.
 
 (* User Tactics *)
 
@@ -333,18 +336,20 @@ Ltac pupto11_final := first [eapply upto11_final; [eauto with paco|] | eapply gr
 Ltac pupto11 H := first [eapply upto11_step|eapply upto11_step_under]; [|eapply H|]; [eauto with paco|].
 
 Ltac pfold11_reverse_ :=
-    match goal with
-    | [|- ?gf (upaco11 _ _ _ _ _ _ _ _ _ _ _) _ _ _ _ _ _ _ _ _ _ _] => eapply (paco11_unfold gf)
-    | [|- ?gf (?gres (upaco11 _ _ _ _ _ _ _ _ _ _ _)) _ _ _ _ _ _ _ _ _ _ _] => eapply (paco11_unfold (gf:=compose gf gres))
-    end.
+  repeat red;
+  match goal with
+  | [|- ?gf (upaco11 _ _ _ _ _ _ _ _ _ _ _) _ _ _ _ _ _ _ _ _ _ _] => eapply (paco11_unfold (gf := gf))
+  | [|- ?gf (?gres (upaco11 _ _ _ _ _ _ _ _ _ _ _)) _ _ _ _ _ _ _ _ _ _ _] => eapply (paco11_unfold (gf := cgres11 gf))
+  end.
 
 Ltac pfold11_reverse := pfold11_reverse_; eauto with paco.
 
 Ltac punfold11_reverse_ H :=
+  repeat red in H;
   let PP := type of H in
   match PP with
   | ?gf (upaco11 _ _ _ _ _ _ _ _ _ _ _) _ _ _ _ _ _ _ _ _ _ _ => eapply (paco11_fold gf) in H
-  | ?gf (?gres (upaco11 _ _ _ _ _ _ _ _ _ _ _)) _ _ _ _ _ _ _ _ _ _ _ => eapply (paco11_fold (compose gf gres)) in H
+  | ?gf (?gres (upaco11 _ _ _ _ _ _ _ _ _ _ _)) _ _ _ _ _ _ _ _ _ _ _ => eapply (paco11_fold (cgres11 gf)) in H
   end.
 
 Ltac punfold11_reverse H := punfold11_reverse_ H; eauto with paco.

diff --git a/src/paco12_upto.v b/src/paco12_upto.v
@@ -246,16 +246,18 @@ Proof.
     intros. eapply rclo12_mon; [apply R', PR| apply LE].
 Qed.
 
+Definition cgres12 := compose gf gres12.
+
 Lemma upto12_init:
-  paco12 (compose gf gres12) bot12 <12= paco12 gf bot12.
+  paco12 cgres12 bot12 <12= paco12 gf bot12.
 Proof.
   apply sound12_is_gf.
   apply respectful12_is_sound12.
   apply grespectful12_respectful12.
 Qed.
 
 Lemma upto12_final:
-  paco12 gf <13= paco12 (compose gf gres12).
+  paco12 gf <13= paco12 cgres12.
 Proof.
   pcofix CIH. intros. _punfold PR; [|apply gf_mon]. pfold.
   eapply gf_mon; [|apply grespectful12_incl].
@@ -265,7 +267,7 @@ Qed.
 
 Lemma upto12_step
       r clo (RES: weak_respectful12 clo):
-  clo (paco12 (compose gf gres12) r) <12= paco12 (compose gf gres12) r.
+  clo (paco12 cgres12 r) <12= paco12 cgres12 r.
 Proof.
   intros. apply grespectful12_incl_rev.
   assert (RES' := weak_respectful12_respectful12 RES).
@@ -326,6 +328,7 @@ Hint Resolve gfgres12_mon : paco.
 Hint Resolve grespectful12_incl.
 Hint Resolve rclo12_mon: paco.
 Hint Constructors weak_respectful12.
+Hint Unfold cgres12.
 
 (* User Tactics *)
 
@@ -334,18 +337,20 @@ Ltac pupto12_final := first [eapply upto12_final; [eauto with paco|] | eapply gr
 Ltac pupto12 H := first [eapply upto12_step|eapply upto12_step_under]; [|eapply H|]; [eauto with paco|].
 
 Ltac pfold12_reverse_ :=
-    match goal with
-    | [|- ?gf (upaco12 _ _ _ _ _ _ _ _ _ _ _ _) _ _ _ _ _ _ _ _ _ _ _ _] => eapply (paco12_unfold gf)
-    | [|- ?gf (?gres (upaco12 _ _ _ _ _ _ _ _ _ _ _ _)) _ _ _ _ _ _ _ _ _ _ _ _] => eapply (paco12_unfold (gf:=compose gf gres))
-    end.
+  repeat red;
+  match goal with
+  | [|- ?gf (upaco12 _ _ _ _ _ _ _ _ _ _ _ _) _ _ _ _ _ _ _ _ _ _ _ _] => eapply (paco12_unfold (gf := gf))
+  | [|- ?gf (?gres (upaco12 _ _ _ _ _ _ _ _ _ _ _ _)) _ _ _ _ _ _ _ _ _ _ _ _] => eapply (paco12_unfold (gf := cgres12 gf))
+  end.
 
 Ltac pfold12_reverse := pfold12_reverse_; eauto with paco.
 
 Ltac punfold12_reverse_ H :=
+  repeat red in H;
   let PP := type of H in
   match PP with
   | ?gf (upaco12 _ _ _ _ _ _ _ _ _ _ _ _) _ _ _ _ _ _ _ _ _ _ _ _ => eapply (paco12_fold gf) in H
-  | ?gf (?gres (upaco12 _ _ _ _ _ _ _ _ _ _ _ _)) _ _ _ _ _ _ _ _ _ _ _ _ => eapply (paco12_fold (compose gf gres)) in H
+  | ?gf (?gres (upaco12 _ _ _ _ _ _ _ _ _ _ _ _)) _ _ _ _ _ _ _ _ _ _ _ _ => eapply (paco12_fold (cgres12 gf)) in H
   end.
 
 Ltac punfold12_reverse H := punfold12_reverse_ H; eauto with paco.

diff --git a/src/paco13_upto.v b/src/paco13_upto.v
@@ -247,16 +247,18 @@ Proof.
     intros. eapply rclo13_mon; [apply R', PR| apply LE].
 Qed.
 
+Definition cgres13 := compose gf gres13.
+
 Lemma upto13_init:
-  paco13 (compose gf gres13) bot13 <13= paco13 gf bot13.
+  paco13 cgres13 bot13 <13= paco13 gf bot13.
 Proof.
   apply sound13_is_gf.
   apply respectful13_is_sound13.
   apply grespectful13_respectful13.
 Qed.
 
 Lemma upto13_final:
-  paco13 gf <14= paco13 (compose gf gres13).
+  paco13 gf <14= paco13 cgres13.
 Proof.
   pcofix CIH. intros. _punfold PR; [|apply gf_mon]. pfold.
   eapply gf_mon; [|apply grespectful13_incl].
@@ -266,7 +268,7 @@ Qed.
 
 Lemma upto13_step
       r clo (RES: weak_respectful13 clo):
-  clo (paco13 (compose gf gres13) r) <13= paco13 (compose gf gres13) r.
+  clo (paco13 cgres13 r) <13= paco13 cgres13 r.
 Proof.
   intros. apply grespectful13_incl_rev.
   assert (RES' := weak_respectful13_respectful13 RES).
@@ -327,6 +329,7 @@ Hint Resolve gfgres13_mon : paco.
 Hint Resolve grespectful13_incl.
 Hint Resolve rclo13_mon: paco.
 Hint Constructors weak_respectful13.
+Hint Unfold cgres13.
 
 (* User Tactics *)
 
@@ -335,18 +338,20 @@ Ltac pupto13_final := first [eapply upto13_final; [eauto with paco|] | eapply gr
 Ltac pupto13 H := first [eapply upto13_step|eapply upto13_step_under]; [|eapply H|]; [eauto with paco|].
 
 Ltac pfold13_reverse_ :=
-    match goal with
-    | [|- ?gf (upaco13 _ _ _ _ _ _ _ _ _ _ _ _ _) _ _ _ _ _ _ _ _ _ _ _ _ _] => eapply (paco13_unfold gf)
-    | [|- ?gf (?gres (upaco13 _ _ _ _ _ _ _ _ _ _ _ _ _)) _ _ _ _ _ _ _ _ _ _ _ _ _] => eapply (paco13_unfold (gf:=compose gf gres))
-    end.
+  repeat red;
+  match goal with
+  | [|- ?gf (upaco13 _ _ _ _ _ _ _ _ _ _ _ _ _) _ _ _ _ _ _ _ _ _ _ _ _ _] => eapply (paco13_unfold (gf := gf))
+  | [|- ?gf (?gres (upaco13 _ _ _ _ _ _ _ _ _ _ _ _ _)) _ _ _ _ _ _ _ _ _ _ _ _ _] => eapply (paco13_unfold (gf := cgres13 gf))
+  end.
 
 Ltac pfold13_reverse := pfold13_reverse_; eauto with paco.
 
 Ltac punfold13_reverse_ H :=
+  repeat red in H;
   let PP := type of H in
   match PP with
   | ?gf (upaco13 _ _ _ _ _ _ _ _ _ _ _ _ _) _ _ _ _ _ _ _ _ _ _ _ _ _ => eapply (paco13_fold gf) in H
-  | ?gf (?gres (upaco13 _ _ _ _ _ _ _ _ _ _ _ _ _)) _ _ _ _ _ _ _ _ _ _ _ _ _ => eapply (paco13_fold (compose gf gres)) in H
+  | ?gf (?gres (upaco13 _ _ _ _ _ _ _ _ _ _ _ _ _)) _ _ _ _ _ _ _ _ _ _ _ _ _ => eapply (paco13_fold (cgres13 gf)) in H
   end.
 
 Ltac punfold13_reverse H := punfold13_reverse_ H; eauto with paco.