From 6f3618855878d86551fda89960261e3fc6e2d4dc Mon Sep 17 00:00:00 2001 From: minki cho Date: Mon, 23 Jul 2018 02:46:11 +0900 Subject: [PATCH] more more speed up --- metasrc/paco.py | 45 ++++++++------- src/paco0.v | 140 ++++++++++++++++++++++---------------------- src/paco1.v | 150 ++++++++++++++++++++++++------------------------ src/paco10.v | 150 ++++++++++++++++++++++++------------------------ src/paco11.v | 150 ++++++++++++++++++++++++------------------------ src/paco12.v | 150 ++++++++++++++++++++++++------------------------ src/paco13.v | 150 ++++++++++++++++++++++++------------------------ src/paco14.v | 150 ++++++++++++++++++++++++------------------------ src/paco15.v | 150 ++++++++++++++++++++++++------------------------ src/paco2.v | 150 ++++++++++++++++++++++++------------------------ src/paco3.v | 150 ++++++++++++++++++++++++------------------------ src/paco4.v | 150 ++++++++++++++++++++++++------------------------ src/paco5.v | 150 ++++++++++++++++++++++++------------------------ src/paco6.v | 150 ++++++++++++++++++++++++------------------------ src/paco7.v | 150 ++++++++++++++++++++++++------------------------ src/paco8.v | 150 ++++++++++++++++++++++++------------------------ src/paco9.v | 150 ++++++++++++++++++++++++------------------------ 17 files changed, 1218 insertions(+), 1217 deletions(-) diff --git a/metasrc/paco.py b/metasrc/paco.py index 16c1cd4..cab62b6 100755 --- a/metasrc/paco.py +++ b/metasrc/paco.py @@ -287,39 +287,40 @@ print ('End Arg'+str(n)+'_'+str(m)+'.') print ('') -print ('End PACO'+str(n)+'.') -print ('') - -for m in range(1,mutsize+1): - for i in range(m): - print ('Global Opaque paco'+str(n)+lev(m)+idx(m,i)+'.') - print ('') - for i in range(m): - print ('Hint Unfold upaco'+str(n)+lev(m)+idx(m,i)+'.') - for i in range(m): - print ('Hint Resolve paco'+str(n)+lev(m)+idx(m,i)+'_fold.') - print ('Hint Unfold monotone'+str(n)+lev(m)+'.') - print ('') - + print ('Arguments paco'+str(n)+lev(m)+idx(m,i)+'_acc'+" : clear implicits.") for i in range(m): - print ('Arguments paco'+str(n)+lev(m)+idx(m,i)+'_acc'+ifpstr(n,' ['+itrstr(" T",n)+' ].'," : clear implicits.")) + print ('Arguments paco'+str(n)+lev(m)+idx(m,i)+'_mon'+" : clear implicits.") for i in range(m): - print ('Arguments paco'+str(n)+lev(m)+idx(m,i)+'_mon'+ifpstr(n,' ['+itrstr(" T",n)+' ].'," : clear implicits.")) + print ('Arguments paco'+str(n)+lev(m)+idx(m,i)+'_mult_strong'+" : clear implicits.") for i in range(m): - print ('Arguments paco'+str(n)+lev(m)+idx(m,i)+'_mult_strong'+ifpstr(n,' ['+itrstr(" T",n)+' ].'," : clear implicits.")) + print ('Arguments paco'+str(n)+lev(m)+idx(m,i)+'_mult'+" : clear implicits.") for i in range(m): - print ('Arguments paco'+str(n)+lev(m)+idx(m,i)+'_mult'+ifpstr(n,' ['+itrstr(" T",n)+' ].'," : clear implicits.")) + print ('Arguments paco'+str(n)+lev(m)+idx(m,i)+'_fold'+" : clear implicits.") for i in range(m): - print ('Arguments paco'+str(n)+lev(m)+idx(m,i)+'_fold'+ifpstr(n,' ['+itrstr(" T",n)+' ].'," : clear implicits.")) - for i in range(m): - print ('Arguments paco'+str(n)+lev(m)+idx(m,i)+'_unfold'+ifpstr(n,' ['+itrstr(" T",n)+' ].'," : clear implicits.")) + print ('Arguments paco'+str(n)+lev(m)+idx(m,i)+'_unfold'+" : clear implicits.") print ('') for i in range(m): - print ("Instance paco"+str(n)+lev(m)+idx(m,i)+"_inst "+itrstr(" T",n)+" ("+itridx("gf",m," ")+": rel"+str(n)+itrstr(" T",n)+"->_)"+itridx(" r",m)+itrstr(" x",n)+" : paco_class (paco"+str(n)+lev(m)+idx(m,i)+itridx(" gf",m)+itridx(" r",m)+itrstr(" x",n)+") :=") + print ("Global Instance paco"+str(n)+lev(m)+idx(m,i)+"_inst "+" ("+itridx("gf",m," ")+": rel"+str(n)+itrstr(" T",n)+"->_)"+itridx(" r",m)+itrstr(" x",n)+" : paco_class (paco"+str(n)+lev(m)+idx(m,i)+itridx(" gf",m)+itridx(" r",m)+itrstr(" x",n)+") :=") print ("{ pacoacc := paco"+str(n)+lev(m)+idx(m,i)+"_acc"+itridx(" gf",m)+";") print (" pacomult := paco"+str(n)+lev(m)+idx(m,i)+"_mult"+itridx(" gf",m)+";") print (" pacofold := paco"+str(n)+lev(m)+idx(m,i)+"_fold"+itridx(" gf",m)+";") print (" pacounfold := paco"+str(n)+lev(m)+idx(m,i)+"_unfold"+itridx(" gf",m)+" }.") print ('') + + +print ('End PACO'+str(n)+'.') +print ('') + +for m in range(1,mutsize+1): + for i in range(m): + print ('Global Opaque paco'+str(n)+lev(m)+idx(m,i)+'.') + print ('') + + for i in range(m): + print ('Hint Unfold upaco'+str(n)+lev(m)+idx(m,i)+'.') + for i in range(m): + print ('Hint Resolve paco'+str(n)+lev(m)+idx(m,i)+'_fold.') + print ('Hint Unfold monotone'+str(n)+lev(m)+'.') + print ('') diff --git a/src/paco0.v b/src/paco0.v index 0df9120..7d93ed4 100644 --- a/src/paco0.v +++ b/src/paco0.v @@ -231,6 +231,19 @@ Qed. End Arg0_1. +Arguments paco0_acc : clear implicits. +Arguments paco0_mon : clear implicits. +Arguments paco0_mult_strong : clear implicits. +Arguments paco0_mult : clear implicits. +Arguments paco0_fold : clear implicits. +Arguments paco0_unfold : clear implicits. + +Global Instance paco0_inst (gf : rel0->_) r : paco_class (paco0 gf r) := +{ pacoacc := paco0_acc gf; + pacomult := paco0_mult gf; + pacofold := paco0_fold gf; + pacounfold := paco0_unfold gf }. + (** 2 Mutual Coinduction *) Section Arg0_2. @@ -408,6 +421,31 @@ Qed. End Arg0_2. +Arguments paco0_2_0_acc : clear implicits. +Arguments paco0_2_1_acc : clear implicits. +Arguments paco0_2_0_mon : clear implicits. +Arguments paco0_2_1_mon : clear implicits. +Arguments paco0_2_0_mult_strong : clear implicits. +Arguments paco0_2_1_mult_strong : clear implicits. +Arguments paco0_2_0_mult : clear implicits. +Arguments paco0_2_1_mult : clear implicits. +Arguments paco0_2_0_fold : clear implicits. +Arguments paco0_2_1_fold : clear implicits. +Arguments paco0_2_0_unfold : clear implicits. +Arguments paco0_2_1_unfold : clear implicits. + +Global Instance paco0_2_0_inst (gf_0 gf_1 : rel0->_) r_0 r_1 : paco_class (paco0_2_0 gf_0 gf_1 r_0 r_1) := +{ pacoacc := paco0_2_0_acc gf_0 gf_1; + pacomult := paco0_2_0_mult gf_0 gf_1; + pacofold := paco0_2_0_fold gf_0 gf_1; + pacounfold := paco0_2_0_unfold gf_0 gf_1 }. + +Global Instance paco0_2_1_inst (gf_0 gf_1 : rel0->_) r_0 r_1 : paco_class (paco0_2_1 gf_0 gf_1 r_0 r_1) := +{ pacoacc := paco0_2_1_acc gf_0 gf_1; + pacomult := paco0_2_1_mult gf_0 gf_1; + pacofold := paco0_2_1_fold gf_0 gf_1; + pacounfold := paco0_2_1_unfold gf_0 gf_1 }. + (** 3 Mutual Coinduction *) Section Arg0_3. @@ -661,73 +699,6 @@ Qed. End Arg0_3. -End PACO0. - -Global Opaque paco0. - -Hint Unfold upaco0. -Hint Resolve paco0_fold. -Hint Unfold monotone0. - -Arguments paco0_acc : clear implicits. -Arguments paco0_mon : clear implicits. -Arguments paco0_mult_strong : clear implicits. -Arguments paco0_mult : clear implicits. -Arguments paco0_fold : clear implicits. -Arguments paco0_unfold : clear implicits. - -Instance paco0_inst (gf : rel0->_) r : paco_class (paco0 gf r) := -{ pacoacc := paco0_acc gf; - pacomult := paco0_mult gf; - pacofold := paco0_fold gf; - pacounfold := paco0_unfold gf }. - -Global Opaque paco0_2_0. -Global Opaque paco0_2_1. - -Hint Unfold upaco0_2_0. -Hint Unfold upaco0_2_1. -Hint Resolve paco0_2_0_fold. -Hint Resolve paco0_2_1_fold. -Hint Unfold monotone0_2. - -Arguments paco0_2_0_acc : clear implicits. -Arguments paco0_2_1_acc : clear implicits. -Arguments paco0_2_0_mon : clear implicits. -Arguments paco0_2_1_mon : clear implicits. -Arguments paco0_2_0_mult_strong : clear implicits. -Arguments paco0_2_1_mult_strong : clear implicits. -Arguments paco0_2_0_mult : clear implicits. -Arguments paco0_2_1_mult : clear implicits. -Arguments paco0_2_0_fold : clear implicits. -Arguments paco0_2_1_fold : clear implicits. -Arguments paco0_2_0_unfold : clear implicits. -Arguments paco0_2_1_unfold : clear implicits. - -Instance paco0_2_0_inst (gf_0 gf_1 : rel0->_) r_0 r_1 : paco_class (paco0_2_0 gf_0 gf_1 r_0 r_1) := -{ pacoacc := paco0_2_0_acc gf_0 gf_1; - pacomult := paco0_2_0_mult gf_0 gf_1; - pacofold := paco0_2_0_fold gf_0 gf_1; - pacounfold := paco0_2_0_unfold gf_0 gf_1 }. - -Instance paco0_2_1_inst (gf_0 gf_1 : rel0->_) r_0 r_1 : paco_class (paco0_2_1 gf_0 gf_1 r_0 r_1) := -{ pacoacc := paco0_2_1_acc gf_0 gf_1; - pacomult := paco0_2_1_mult gf_0 gf_1; - pacofold := paco0_2_1_fold gf_0 gf_1; - pacounfold := paco0_2_1_unfold gf_0 gf_1 }. - -Global Opaque paco0_3_0. -Global Opaque paco0_3_1. -Global Opaque paco0_3_2. - -Hint Unfold upaco0_3_0. -Hint Unfold upaco0_3_1. -Hint Unfold upaco0_3_2. -Hint Resolve paco0_3_0_fold. -Hint Resolve paco0_3_1_fold. -Hint Resolve paco0_3_2_fold. -Hint Unfold monotone0_3. - Arguments paco0_3_0_acc : clear implicits. Arguments paco0_3_1_acc : clear implicits. Arguments paco0_3_2_acc : clear implicits. @@ -747,21 +718,50 @@ Arguments paco0_3_0_unfold : clear implicits. Arguments paco0_3_1_unfold : clear implicits. Arguments paco0_3_2_unfold : clear implicits. -Instance paco0_3_0_inst (gf_0 gf_1 gf_2 : rel0->_) r_0 r_1 r_2 : paco_class (paco0_3_0 gf_0 gf_1 gf_2 r_0 r_1 r_2) := +Global Instance paco0_3_0_inst (gf_0 gf_1 gf_2 : rel0->_) r_0 r_1 r_2 : paco_class (paco0_3_0 gf_0 gf_1 gf_2 r_0 r_1 r_2) := { pacoacc := paco0_3_0_acc gf_0 gf_1 gf_2; pacomult := paco0_3_0_mult gf_0 gf_1 gf_2; pacofold := paco0_3_0_fold gf_0 gf_1 gf_2; pacounfold := paco0_3_0_unfold gf_0 gf_1 gf_2 }. -Instance paco0_3_1_inst (gf_0 gf_1 gf_2 : rel0->_) r_0 r_1 r_2 : paco_class (paco0_3_1 gf_0 gf_1 gf_2 r_0 r_1 r_2) := +Global Instance paco0_3_1_inst (gf_0 gf_1 gf_2 : rel0->_) r_0 r_1 r_2 : paco_class (paco0_3_1 gf_0 gf_1 gf_2 r_0 r_1 r_2) := { pacoacc := paco0_3_1_acc gf_0 gf_1 gf_2; pacomult := paco0_3_1_mult gf_0 gf_1 gf_2; pacofold := paco0_3_1_fold gf_0 gf_1 gf_2; pacounfold := paco0_3_1_unfold gf_0 gf_1 gf_2 }. -Instance paco0_3_2_inst (gf_0 gf_1 gf_2 : rel0->_) r_0 r_1 r_2 : paco_class (paco0_3_2 gf_0 gf_1 gf_2 r_0 r_1 r_2) := +Global Instance paco0_3_2_inst (gf_0 gf_1 gf_2 : rel0->_) r_0 r_1 r_2 : paco_class (paco0_3_2 gf_0 gf_1 gf_2 r_0 r_1 r_2) := { pacoacc := paco0_3_2_acc gf_0 gf_1 gf_2; pacomult := paco0_3_2_mult gf_0 gf_1 gf_2; pacofold := paco0_3_2_fold gf_0 gf_1 gf_2; pacounfold := paco0_3_2_unfold gf_0 gf_1 gf_2 }. +End PACO0. + +Global Opaque paco0. + +Hint Unfold upaco0. +Hint Resolve paco0_fold. +Hint Unfold monotone0. + +Global Opaque paco0_2_0. +Global Opaque paco0_2_1. + +Hint Unfold upaco0_2_0. +Hint Unfold upaco0_2_1. +Hint Resolve paco0_2_0_fold. +Hint Resolve paco0_2_1_fold. +Hint Unfold monotone0_2. + +Global Opaque paco0_3_0. +Global Opaque paco0_3_1. +Global Opaque paco0_3_2. + +Hint Unfold upaco0_3_0. +Hint Unfold upaco0_3_1. +Hint Unfold upaco0_3_2. +Hint Resolve paco0_3_0_fold. +Hint Resolve paco0_3_1_fold. +Hint Resolve paco0_3_2_fold. +Hint Unfold monotone0_3. + diff --git a/src/paco1.v b/src/paco1.v index 84a66d9..7d4522c 100644 --- a/src/paco1.v +++ b/src/paco1.v @@ -233,6 +233,19 @@ Qed. End Arg1_1. +Arguments paco1_acc : clear implicits. +Arguments paco1_mon : clear implicits. +Arguments paco1_mult_strong : clear implicits. +Arguments paco1_mult : clear implicits. +Arguments paco1_fold : clear implicits. +Arguments paco1_unfold : clear implicits. + +Global Instance paco1_inst (gf : rel1 T0->_) r x0 : paco_class (paco1 gf r x0) := +{ pacoacc := paco1_acc gf; + pacomult := paco1_mult gf; + pacofold := paco1_fold gf; + pacounfold := paco1_unfold gf }. + (** 2 Mutual Coinduction *) Section Arg1_2. @@ -410,6 +423,31 @@ Qed. End Arg1_2. +Arguments paco1_2_0_acc : clear implicits. +Arguments paco1_2_1_acc : clear implicits. +Arguments paco1_2_0_mon : clear implicits. +Arguments paco1_2_1_mon : clear implicits. +Arguments paco1_2_0_mult_strong : clear implicits. +Arguments paco1_2_1_mult_strong : clear implicits. +Arguments paco1_2_0_mult : clear implicits. +Arguments paco1_2_1_mult : clear implicits. +Arguments paco1_2_0_fold : clear implicits. +Arguments paco1_2_1_fold : clear implicits. +Arguments paco1_2_0_unfold : clear implicits. +Arguments paco1_2_1_unfold : clear implicits. + +Global Instance paco1_2_0_inst (gf_0 gf_1 : rel1 T0->_) r_0 r_1 x0 : paco_class (paco1_2_0 gf_0 gf_1 r_0 r_1 x0) := +{ pacoacc := paco1_2_0_acc gf_0 gf_1; + pacomult := paco1_2_0_mult gf_0 gf_1; + pacofold := paco1_2_0_fold gf_0 gf_1; + pacounfold := paco1_2_0_unfold gf_0 gf_1 }. + +Global Instance paco1_2_1_inst (gf_0 gf_1 : rel1 T0->_) r_0 r_1 x0 : paco_class (paco1_2_1 gf_0 gf_1 r_0 r_1 x0) := +{ pacoacc := paco1_2_1_acc gf_0 gf_1; + pacomult := paco1_2_1_mult gf_0 gf_1; + pacofold := paco1_2_1_fold gf_0 gf_1; + pacounfold := paco1_2_1_unfold gf_0 gf_1 }. + (** 3 Mutual Coinduction *) Section Arg1_3. @@ -663,6 +701,43 @@ Qed. End Arg1_3. +Arguments paco1_3_0_acc : clear implicits. +Arguments paco1_3_1_acc : clear implicits. +Arguments paco1_3_2_acc : clear implicits. +Arguments paco1_3_0_mon : clear implicits. +Arguments paco1_3_1_mon : clear implicits. +Arguments paco1_3_2_mon : clear implicits. +Arguments paco1_3_0_mult_strong : clear implicits. +Arguments paco1_3_1_mult_strong : clear implicits. +Arguments paco1_3_2_mult_strong : clear implicits. +Arguments paco1_3_0_mult : clear implicits. +Arguments paco1_3_1_mult : clear implicits. +Arguments paco1_3_2_mult : clear implicits. +Arguments paco1_3_0_fold : clear implicits. +Arguments paco1_3_1_fold : clear implicits. +Arguments paco1_3_2_fold : clear implicits. +Arguments paco1_3_0_unfold : clear implicits. +Arguments paco1_3_1_unfold : clear implicits. +Arguments paco1_3_2_unfold : clear implicits. + +Global Instance paco1_3_0_inst (gf_0 gf_1 gf_2 : rel1 T0->_) r_0 r_1 r_2 x0 : paco_class (paco1_3_0 gf_0 gf_1 gf_2 r_0 r_1 r_2 x0) := +{ pacoacc := paco1_3_0_acc gf_0 gf_1 gf_2; + pacomult := paco1_3_0_mult gf_0 gf_1 gf_2; + pacofold := paco1_3_0_fold gf_0 gf_1 gf_2; + pacounfold := paco1_3_0_unfold gf_0 gf_1 gf_2 }. + +Global Instance paco1_3_1_inst (gf_0 gf_1 gf_2 : rel1 T0->_) r_0 r_1 r_2 x0 : paco_class (paco1_3_1 gf_0 gf_1 gf_2 r_0 r_1 r_2 x0) := +{ pacoacc := paco1_3_1_acc gf_0 gf_1 gf_2; + pacomult := paco1_3_1_mult gf_0 gf_1 gf_2; + pacofold := paco1_3_1_fold gf_0 gf_1 gf_2; + pacounfold := paco1_3_1_unfold gf_0 gf_1 gf_2 }. + +Global Instance paco1_3_2_inst (gf_0 gf_1 gf_2 : rel1 T0->_) r_0 r_1 r_2 x0 : paco_class (paco1_3_2 gf_0 gf_1 gf_2 r_0 r_1 r_2 x0) := +{ pacoacc := paco1_3_2_acc gf_0 gf_1 gf_2; + pacomult := paco1_3_2_mult gf_0 gf_1 gf_2; + pacofold := paco1_3_2_fold gf_0 gf_1 gf_2; + pacounfold := paco1_3_2_unfold gf_0 gf_1 gf_2 }. + End PACO1. Global Opaque paco1. @@ -671,19 +746,6 @@ Hint Unfold upaco1. Hint Resolve paco1_fold. Hint Unfold monotone1. -Arguments paco1_acc [ T0 ]. -Arguments paco1_mon [ T0 ]. -Arguments paco1_mult_strong [ T0 ]. -Arguments paco1_mult [ T0 ]. -Arguments paco1_fold [ T0 ]. -Arguments paco1_unfold [ T0 ]. - -Instance paco1_inst T0 (gf : rel1 T0->_) r x0 : paco_class (paco1 gf r x0) := -{ pacoacc := paco1_acc gf; - pacomult := paco1_mult gf; - pacofold := paco1_fold gf; - pacounfold := paco1_unfold gf }. - Global Opaque paco1_2_0. Global Opaque paco1_2_1. @@ -693,31 +755,6 @@ Hint Resolve paco1_2_0_fold. Hint Resolve paco1_2_1_fold. Hint Unfold monotone1_2. -Arguments paco1_2_0_acc [ T0 ]. -Arguments paco1_2_1_acc [ T0 ]. -Arguments paco1_2_0_mon [ T0 ]. -Arguments paco1_2_1_mon [ T0 ]. -Arguments paco1_2_0_mult_strong [ T0 ]. -Arguments paco1_2_1_mult_strong [ T0 ]. -Arguments paco1_2_0_mult [ T0 ]. -Arguments paco1_2_1_mult [ T0 ]. -Arguments paco1_2_0_fold [ T0 ]. -Arguments paco1_2_1_fold [ T0 ]. -Arguments paco1_2_0_unfold [ T0 ]. -Arguments paco1_2_1_unfold [ T0 ]. - -Instance paco1_2_0_inst T0 (gf_0 gf_1 : rel1 T0->_) r_0 r_1 x0 : paco_class (paco1_2_0 gf_0 gf_1 r_0 r_1 x0) := -{ pacoacc := paco1_2_0_acc gf_0 gf_1; - pacomult := paco1_2_0_mult gf_0 gf_1; - pacofold := paco1_2_0_fold gf_0 gf_1; - pacounfold := paco1_2_0_unfold gf_0 gf_1 }. - -Instance paco1_2_1_inst T0 (gf_0 gf_1 : rel1 T0->_) r_0 r_1 x0 : paco_class (paco1_2_1 gf_0 gf_1 r_0 r_1 x0) := -{ pacoacc := paco1_2_1_acc gf_0 gf_1; - pacomult := paco1_2_1_mult gf_0 gf_1; - pacofold := paco1_2_1_fold gf_0 gf_1; - pacounfold := paco1_2_1_unfold gf_0 gf_1 }. - Global Opaque paco1_3_0. Global Opaque paco1_3_1. Global Opaque paco1_3_2. @@ -730,40 +767,3 @@ Hint Resolve paco1_3_1_fold. Hint Resolve paco1_3_2_fold. Hint Unfold monotone1_3. -Arguments paco1_3_0_acc [ T0 ]. -Arguments paco1_3_1_acc [ T0 ]. -Arguments paco1_3_2_acc [ T0 ]. -Arguments paco1_3_0_mon [ T0 ]. -Arguments paco1_3_1_mon [ T0 ]. -Arguments paco1_3_2_mon [ T0 ]. -Arguments paco1_3_0_mult_strong [ T0 ]. -Arguments paco1_3_1_mult_strong [ T0 ]. -Arguments paco1_3_2_mult_strong [ T0 ]. -Arguments paco1_3_0_mult [ T0 ]. -Arguments paco1_3_1_mult [ T0 ]. -Arguments paco1_3_2_mult [ T0 ]. -Arguments paco1_3_0_fold [ T0 ]. -Arguments paco1_3_1_fold [ T0 ]. -Arguments paco1_3_2_fold [ T0 ]. -Arguments paco1_3_0_unfold [ T0 ]. -Arguments paco1_3_1_unfold [ T0 ]. -Arguments paco1_3_2_unfold [ T0 ]. - -Instance paco1_3_0_inst T0 (gf_0 gf_1 gf_2 : rel1 T0->_) r_0 r_1 r_2 x0 : paco_class (paco1_3_0 gf_0 gf_1 gf_2 r_0 r_1 r_2 x0) := -{ pacoacc := paco1_3_0_acc gf_0 gf_1 gf_2; - pacomult := paco1_3_0_mult gf_0 gf_1 gf_2; - pacofold := paco1_3_0_fold gf_0 gf_1 gf_2; - pacounfold := paco1_3_0_unfold gf_0 gf_1 gf_2 }. - -Instance paco1_3_1_inst T0 (gf_0 gf_1 gf_2 : rel1 T0->_) r_0 r_1 r_2 x0 : paco_class (paco1_3_1 gf_0 gf_1 gf_2 r_0 r_1 r_2 x0) := -{ pacoacc := paco1_3_1_acc gf_0 gf_1 gf_2; - pacomult := paco1_3_1_mult gf_0 gf_1 gf_2; - pacofold := paco1_3_1_fold gf_0 gf_1 gf_2; - pacounfold := paco1_3_1_unfold gf_0 gf_1 gf_2 }. - -Instance paco1_3_2_inst T0 (gf_0 gf_1 gf_2 : rel1 T0->_) r_0 r_1 r_2 x0 : paco_class (paco1_3_2 gf_0 gf_1 gf_2 r_0 r_1 r_2 x0) := -{ pacoacc := paco1_3_2_acc gf_0 gf_1 gf_2; - pacomult := paco1_3_2_mult gf_0 gf_1 gf_2; - pacofold := paco1_3_2_fold gf_0 gf_1 gf_2; - pacounfold := paco1_3_2_unfold gf_0 gf_1 gf_2 }. - diff --git a/src/paco10.v b/src/paco10.v index defd83f..718a159 100644 --- a/src/paco10.v +++ b/src/paco10.v @@ -251,6 +251,19 @@ Qed. End Arg10_1. +Arguments paco10_acc : clear implicits. +Arguments paco10_mon : clear implicits. +Arguments paco10_mult_strong : clear implicits. +Arguments paco10_mult : clear implicits. +Arguments paco10_fold : clear implicits. +Arguments paco10_unfold : clear implicits. + +Global Instance paco10_inst (gf : rel10 T0 T1 T2 T3 T4 T5 T6 T7 T8 T9->_) r x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 : paco_class (paco10 gf r x0 x1 x2 x3 x4 x5 x6 x7 x8 x9) := +{ pacoacc := paco10_acc gf; + pacomult := paco10_mult gf; + pacofold := paco10_fold gf; + pacounfold := paco10_unfold gf }. + (** 2 Mutual Coinduction *) Section Arg10_2. @@ -428,6 +441,31 @@ Qed. End Arg10_2. +Arguments paco10_2_0_acc : clear implicits. +Arguments paco10_2_1_acc : clear implicits. +Arguments paco10_2_0_mon : clear implicits. +Arguments paco10_2_1_mon : clear implicits. +Arguments paco10_2_0_mult_strong : clear implicits. +Arguments paco10_2_1_mult_strong : clear implicits. +Arguments paco10_2_0_mult : clear implicits. +Arguments paco10_2_1_mult : clear implicits. +Arguments paco10_2_0_fold : clear implicits. +Arguments paco10_2_1_fold : clear implicits. +Arguments paco10_2_0_unfold : clear implicits. +Arguments paco10_2_1_unfold : clear implicits. + +Global Instance paco10_2_0_inst (gf_0 gf_1 : rel10 T0 T1 T2 T3 T4 T5 T6 T7 T8 T9->_) r_0 r_1 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 : paco_class (paco10_2_0 gf_0 gf_1 r_0 r_1 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9) := +{ pacoacc := paco10_2_0_acc gf_0 gf_1; + pacomult := paco10_2_0_mult gf_0 gf_1; + pacofold := paco10_2_0_fold gf_0 gf_1; + pacounfold := paco10_2_0_unfold gf_0 gf_1 }. + +Global Instance paco10_2_1_inst (gf_0 gf_1 : rel10 T0 T1 T2 T3 T4 T5 T6 T7 T8 T9->_) r_0 r_1 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 : paco_class (paco10_2_1 gf_0 gf_1 r_0 r_1 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9) := +{ pacoacc := paco10_2_1_acc gf_0 gf_1; + pacomult := paco10_2_1_mult gf_0 gf_1; + pacofold := paco10_2_1_fold gf_0 gf_1; + pacounfold := paco10_2_1_unfold gf_0 gf_1 }. + (** 3 Mutual Coinduction *) Section Arg10_3. @@ -681,6 +719,43 @@ Qed. End Arg10_3. +Arguments paco10_3_0_acc : clear implicits. +Arguments paco10_3_1_acc : clear implicits. +Arguments paco10_3_2_acc : clear implicits. +Arguments paco10_3_0_mon : clear implicits. +Arguments paco10_3_1_mon : clear implicits. +Arguments paco10_3_2_mon : clear implicits. +Arguments paco10_3_0_mult_strong : clear implicits. +Arguments paco10_3_1_mult_strong : clear implicits. +Arguments paco10_3_2_mult_strong : clear implicits. +Arguments paco10_3_0_mult : clear implicits. +Arguments paco10_3_1_mult : clear implicits. +Arguments paco10_3_2_mult : clear implicits. +Arguments paco10_3_0_fold : clear implicits. +Arguments paco10_3_1_fold : clear implicits. +Arguments paco10_3_2_fold : clear implicits. +Arguments paco10_3_0_unfold : clear implicits. +Arguments paco10_3_1_unfold : clear implicits. +Arguments paco10_3_2_unfold : clear implicits. + +Global Instance paco10_3_0_inst (gf_0 gf_1 gf_2 : rel10 T0 T1 T2 T3 T4 T5 T6 T7 T8 T9->_) r_0 r_1 r_2 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 : paco_class (paco10_3_0 gf_0 gf_1 gf_2 r_0 r_1 r_2 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9) := +{ pacoacc := paco10_3_0_acc gf_0 gf_1 gf_2; + pacomult := paco10_3_0_mult gf_0 gf_1 gf_2; + pacofold := paco10_3_0_fold gf_0 gf_1 gf_2; + pacounfold := paco10_3_0_unfold gf_0 gf_1 gf_2 }. + +Global Instance paco10_3_1_inst (gf_0 gf_1 gf_2 : rel10 T0 T1 T2 T3 T4 T5 T6 T7 T8 T9->_) r_0 r_1 r_2 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 : paco_class (paco10_3_1 gf_0 gf_1 gf_2 r_0 r_1 r_2 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9) := +{ pacoacc := paco10_3_1_acc gf_0 gf_1 gf_2; + pacomult := paco10_3_1_mult gf_0 gf_1 gf_2; + pacofold := paco10_3_1_fold gf_0 gf_1 gf_2; + pacounfold := paco10_3_1_unfold gf_0 gf_1 gf_2 }. + +Global Instance paco10_3_2_inst (gf_0 gf_1 gf_2 : rel10 T0 T1 T2 T3 T4 T5 T6 T7 T8 T9->_) r_0 r_1 r_2 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 : paco_class (paco10_3_2 gf_0 gf_1 gf_2 r_0 r_1 r_2 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9) := +{ pacoacc := paco10_3_2_acc gf_0 gf_1 gf_2; + pacomult := paco10_3_2_mult gf_0 gf_1 gf_2; + pacofold := paco10_3_2_fold gf_0 gf_1 gf_2; + pacounfold := paco10_3_2_unfold gf_0 gf_1 gf_2 }. + End PACO10. Global Opaque paco10. @@ -689,19 +764,6 @@ Hint Unfold upaco10. Hint Resolve paco10_fold. Hint Unfold monotone10. -Arguments paco10_acc [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 ]. -Arguments paco10_mon [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 ]. -Arguments paco10_mult_strong [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 ]. -Arguments paco10_mult [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 ]. -Arguments paco10_fold [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 ]. -Arguments paco10_unfold [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 ]. - -Instance paco10_inst T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 (gf : rel10 T0 T1 T2 T3 T4 T5 T6 T7 T8 T9->_) r x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 : paco_class (paco10 gf r x0 x1 x2 x3 x4 x5 x6 x7 x8 x9) := -{ pacoacc := paco10_acc gf; - pacomult := paco10_mult gf; - pacofold := paco10_fold gf; - pacounfold := paco10_unfold gf }. - Global Opaque paco10_2_0. Global Opaque paco10_2_1. @@ -711,31 +773,6 @@ Hint Resolve paco10_2_0_fold. Hint Resolve paco10_2_1_fold. Hint Unfold monotone10_2. -Arguments paco10_2_0_acc [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 ]. -Arguments paco10_2_1_acc [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 ]. -Arguments paco10_2_0_mon [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 ]. -Arguments paco10_2_1_mon [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 ]. -Arguments paco10_2_0_mult_strong [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 ]. -Arguments paco10_2_1_mult_strong [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 ]. -Arguments paco10_2_0_mult [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 ]. -Arguments paco10_2_1_mult [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 ]. -Arguments paco10_2_0_fold [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 ]. -Arguments paco10_2_1_fold [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 ]. -Arguments paco10_2_0_unfold [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 ]. -Arguments paco10_2_1_unfold [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 ]. - -Instance paco10_2_0_inst T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 (gf_0 gf_1 : rel10 T0 T1 T2 T3 T4 T5 T6 T7 T8 T9->_) r_0 r_1 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 : paco_class (paco10_2_0 gf_0 gf_1 r_0 r_1 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9) := -{ pacoacc := paco10_2_0_acc gf_0 gf_1; - pacomult := paco10_2_0_mult gf_0 gf_1; - pacofold := paco10_2_0_fold gf_0 gf_1; - pacounfold := paco10_2_0_unfold gf_0 gf_1 }. - -Instance paco10_2_1_inst T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 (gf_0 gf_1 : rel10 T0 T1 T2 T3 T4 T5 T6 T7 T8 T9->_) r_0 r_1 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 : paco_class (paco10_2_1 gf_0 gf_1 r_0 r_1 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9) := -{ pacoacc := paco10_2_1_acc gf_0 gf_1; - pacomult := paco10_2_1_mult gf_0 gf_1; - pacofold := paco10_2_1_fold gf_0 gf_1; - pacounfold := paco10_2_1_unfold gf_0 gf_1 }. - Global Opaque paco10_3_0. Global Opaque paco10_3_1. Global Opaque paco10_3_2. @@ -748,40 +785,3 @@ Hint Resolve paco10_3_1_fold. Hint Resolve paco10_3_2_fold. Hint Unfold monotone10_3. -Arguments paco10_3_0_acc [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 ]. -Arguments paco10_3_1_acc [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 ]. -Arguments paco10_3_2_acc [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 ]. -Arguments paco10_3_0_mon [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 ]. -Arguments paco10_3_1_mon [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 ]. -Arguments paco10_3_2_mon [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 ]. -Arguments paco10_3_0_mult_strong [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 ]. -Arguments paco10_3_1_mult_strong [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 ]. -Arguments paco10_3_2_mult_strong [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 ]. -Arguments paco10_3_0_mult [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 ]. -Arguments paco10_3_1_mult [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 ]. -Arguments paco10_3_2_mult [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 ]. -Arguments paco10_3_0_fold [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 ]. -Arguments paco10_3_1_fold [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 ]. -Arguments paco10_3_2_fold [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 ]. -Arguments paco10_3_0_unfold [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 ]. -Arguments paco10_3_1_unfold [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 ]. -Arguments paco10_3_2_unfold [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 ]. - -Instance paco10_3_0_inst T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 (gf_0 gf_1 gf_2 : rel10 T0 T1 T2 T3 T4 T5 T6 T7 T8 T9->_) r_0 r_1 r_2 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 : paco_class (paco10_3_0 gf_0 gf_1 gf_2 r_0 r_1 r_2 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9) := -{ pacoacc := paco10_3_0_acc gf_0 gf_1 gf_2; - pacomult := paco10_3_0_mult gf_0 gf_1 gf_2; - pacofold := paco10_3_0_fold gf_0 gf_1 gf_2; - pacounfold := paco10_3_0_unfold gf_0 gf_1 gf_2 }. - -Instance paco10_3_1_inst T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 (gf_0 gf_1 gf_2 : rel10 T0 T1 T2 T3 T4 T5 T6 T7 T8 T9->_) r_0 r_1 r_2 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 : paco_class (paco10_3_1 gf_0 gf_1 gf_2 r_0 r_1 r_2 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9) := -{ pacoacc := paco10_3_1_acc gf_0 gf_1 gf_2; - pacomult := paco10_3_1_mult gf_0 gf_1 gf_2; - pacofold := paco10_3_1_fold gf_0 gf_1 gf_2; - pacounfold := paco10_3_1_unfold gf_0 gf_1 gf_2 }. - -Instance paco10_3_2_inst T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 (gf_0 gf_1 gf_2 : rel10 T0 T1 T2 T3 T4 T5 T6 T7 T8 T9->_) r_0 r_1 r_2 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 : paco_class (paco10_3_2 gf_0 gf_1 gf_2 r_0 r_1 r_2 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9) := -{ pacoacc := paco10_3_2_acc gf_0 gf_1 gf_2; - pacomult := paco10_3_2_mult gf_0 gf_1 gf_2; - pacofold := paco10_3_2_fold gf_0 gf_1 gf_2; - pacounfold := paco10_3_2_unfold gf_0 gf_1 gf_2 }. - diff --git a/src/paco11.v b/src/paco11.v index f7fad54..bfe9d99 100644 --- a/src/paco11.v +++ b/src/paco11.v @@ -253,6 +253,19 @@ Qed. End Arg11_1. +Arguments paco11_acc : clear implicits. +Arguments paco11_mon : clear implicits. +Arguments paco11_mult_strong : clear implicits. +Arguments paco11_mult : clear implicits. +Arguments paco11_fold : clear implicits. +Arguments paco11_unfold : clear implicits. + +Global Instance paco11_inst (gf : rel11 T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10->_) r x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 : paco_class (paco11 gf r x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10) := +{ pacoacc := paco11_acc gf; + pacomult := paco11_mult gf; + pacofold := paco11_fold gf; + pacounfold := paco11_unfold gf }. + (** 2 Mutual Coinduction *) Section Arg11_2. @@ -430,6 +443,31 @@ Qed. End Arg11_2. +Arguments paco11_2_0_acc : clear implicits. +Arguments paco11_2_1_acc : clear implicits. +Arguments paco11_2_0_mon : clear implicits. +Arguments paco11_2_1_mon : clear implicits. +Arguments paco11_2_0_mult_strong : clear implicits. +Arguments paco11_2_1_mult_strong : clear implicits. +Arguments paco11_2_0_mult : clear implicits. +Arguments paco11_2_1_mult : clear implicits. +Arguments paco11_2_0_fold : clear implicits. +Arguments paco11_2_1_fold : clear implicits. +Arguments paco11_2_0_unfold : clear implicits. +Arguments paco11_2_1_unfold : clear implicits. + +Global Instance paco11_2_0_inst (gf_0 gf_1 : rel11 T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10->_) r_0 r_1 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 : paco_class (paco11_2_0 gf_0 gf_1 r_0 r_1 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10) := +{ pacoacc := paco11_2_0_acc gf_0 gf_1; + pacomult := paco11_2_0_mult gf_0 gf_1; + pacofold := paco11_2_0_fold gf_0 gf_1; + pacounfold := paco11_2_0_unfold gf_0 gf_1 }. + +Global Instance paco11_2_1_inst (gf_0 gf_1 : rel11 T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10->_) r_0 r_1 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 : paco_class (paco11_2_1 gf_0 gf_1 r_0 r_1 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10) := +{ pacoacc := paco11_2_1_acc gf_0 gf_1; + pacomult := paco11_2_1_mult gf_0 gf_1; + pacofold := paco11_2_1_fold gf_0 gf_1; + pacounfold := paco11_2_1_unfold gf_0 gf_1 }. + (** 3 Mutual Coinduction *) Section Arg11_3. @@ -683,6 +721,43 @@ Qed. End Arg11_3. +Arguments paco11_3_0_acc : clear implicits. +Arguments paco11_3_1_acc : clear implicits. +Arguments paco11_3_2_acc : clear implicits. +Arguments paco11_3_0_mon : clear implicits. +Arguments paco11_3_1_mon : clear implicits. +Arguments paco11_3_2_mon : clear implicits. +Arguments paco11_3_0_mult_strong : clear implicits. +Arguments paco11_3_1_mult_strong : clear implicits. +Arguments paco11_3_2_mult_strong : clear implicits. +Arguments paco11_3_0_mult : clear implicits. +Arguments paco11_3_1_mult : clear implicits. +Arguments paco11_3_2_mult : clear implicits. +Arguments paco11_3_0_fold : clear implicits. +Arguments paco11_3_1_fold : clear implicits. +Arguments paco11_3_2_fold : clear implicits. +Arguments paco11_3_0_unfold : clear implicits. +Arguments paco11_3_1_unfold : clear implicits. +Arguments paco11_3_2_unfold : clear implicits. + +Global Instance paco11_3_0_inst (gf_0 gf_1 gf_2 : rel11 T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10->_) r_0 r_1 r_2 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 : paco_class (paco11_3_0 gf_0 gf_1 gf_2 r_0 r_1 r_2 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10) := +{ pacoacc := paco11_3_0_acc gf_0 gf_1 gf_2; + pacomult := paco11_3_0_mult gf_0 gf_1 gf_2; + pacofold := paco11_3_0_fold gf_0 gf_1 gf_2; + pacounfold := paco11_3_0_unfold gf_0 gf_1 gf_2 }. + +Global Instance paco11_3_1_inst (gf_0 gf_1 gf_2 : rel11 T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10->_) r_0 r_1 r_2 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 : paco_class (paco11_3_1 gf_0 gf_1 gf_2 r_0 r_1 r_2 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10) := +{ pacoacc := paco11_3_1_acc gf_0 gf_1 gf_2; + pacomult := paco11_3_1_mult gf_0 gf_1 gf_2; + pacofold := paco11_3_1_fold gf_0 gf_1 gf_2; + pacounfold := paco11_3_1_unfold gf_0 gf_1 gf_2 }. + +Global Instance paco11_3_2_inst (gf_0 gf_1 gf_2 : rel11 T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10->_) r_0 r_1 r_2 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 : paco_class (paco11_3_2 gf_0 gf_1 gf_2 r_0 r_1 r_2 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10) := +{ pacoacc := paco11_3_2_acc gf_0 gf_1 gf_2; + pacomult := paco11_3_2_mult gf_0 gf_1 gf_2; + pacofold := paco11_3_2_fold gf_0 gf_1 gf_2; + pacounfold := paco11_3_2_unfold gf_0 gf_1 gf_2 }. + End PACO11. Global Opaque paco11. @@ -691,19 +766,6 @@ Hint Unfold upaco11. Hint Resolve paco11_fold. Hint Unfold monotone11. -Arguments paco11_acc [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 ]. -Arguments paco11_mon [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 ]. -Arguments paco11_mult_strong [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 ]. -Arguments paco11_mult [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 ]. -Arguments paco11_fold [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 ]. -Arguments paco11_unfold [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 ]. - -Instance paco11_inst T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 (gf : rel11 T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10->_) r x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 : paco_class (paco11 gf r x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10) := -{ pacoacc := paco11_acc gf; - pacomult := paco11_mult gf; - pacofold := paco11_fold gf; - pacounfold := paco11_unfold gf }. - Global Opaque paco11_2_0. Global Opaque paco11_2_1. @@ -713,31 +775,6 @@ Hint Resolve paco11_2_0_fold. Hint Resolve paco11_2_1_fold. Hint Unfold monotone11_2. -Arguments paco11_2_0_acc [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 ]. -Arguments paco11_2_1_acc [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 ]. -Arguments paco11_2_0_mon [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 ]. -Arguments paco11_2_1_mon [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 ]. -Arguments paco11_2_0_mult_strong [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 ]. -Arguments paco11_2_1_mult_strong [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 ]. -Arguments paco11_2_0_mult [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 ]. -Arguments paco11_2_1_mult [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 ]. -Arguments paco11_2_0_fold [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 ]. -Arguments paco11_2_1_fold [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 ]. -Arguments paco11_2_0_unfold [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 ]. -Arguments paco11_2_1_unfold [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 ]. - -Instance paco11_2_0_inst T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 (gf_0 gf_1 : rel11 T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10->_) r_0 r_1 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 : paco_class (paco11_2_0 gf_0 gf_1 r_0 r_1 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10) := -{ pacoacc := paco11_2_0_acc gf_0 gf_1; - pacomult := paco11_2_0_mult gf_0 gf_1; - pacofold := paco11_2_0_fold gf_0 gf_1; - pacounfold := paco11_2_0_unfold gf_0 gf_1 }. - -Instance paco11_2_1_inst T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 (gf_0 gf_1 : rel11 T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10->_) r_0 r_1 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 : paco_class (paco11_2_1 gf_0 gf_1 r_0 r_1 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10) := -{ pacoacc := paco11_2_1_acc gf_0 gf_1; - pacomult := paco11_2_1_mult gf_0 gf_1; - pacofold := paco11_2_1_fold gf_0 gf_1; - pacounfold := paco11_2_1_unfold gf_0 gf_1 }. - Global Opaque paco11_3_0. Global Opaque paco11_3_1. Global Opaque paco11_3_2. @@ -750,40 +787,3 @@ Hint Resolve paco11_3_1_fold. Hint Resolve paco11_3_2_fold. Hint Unfold monotone11_3. -Arguments paco11_3_0_acc [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 ]. -Arguments paco11_3_1_acc [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 ]. -Arguments paco11_3_2_acc [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 ]. -Arguments paco11_3_0_mon [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 ]. -Arguments paco11_3_1_mon [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 ]. -Arguments paco11_3_2_mon [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 ]. -Arguments paco11_3_0_mult_strong [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 ]. -Arguments paco11_3_1_mult_strong [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 ]. -Arguments paco11_3_2_mult_strong [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 ]. -Arguments paco11_3_0_mult [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 ]. -Arguments paco11_3_1_mult [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 ]. -Arguments paco11_3_2_mult [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 ]. -Arguments paco11_3_0_fold [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 ]. -Arguments paco11_3_1_fold [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 ]. -Arguments paco11_3_2_fold [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 ]. -Arguments paco11_3_0_unfold [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 ]. -Arguments paco11_3_1_unfold [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 ]. -Arguments paco11_3_2_unfold [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 ]. - -Instance paco11_3_0_inst T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 (gf_0 gf_1 gf_2 : rel11 T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10->_) r_0 r_1 r_2 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 : paco_class (paco11_3_0 gf_0 gf_1 gf_2 r_0 r_1 r_2 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10) := -{ pacoacc := paco11_3_0_acc gf_0 gf_1 gf_2; - pacomult := paco11_3_0_mult gf_0 gf_1 gf_2; - pacofold := paco11_3_0_fold gf_0 gf_1 gf_2; - pacounfold := paco11_3_0_unfold gf_0 gf_1 gf_2 }. - -Instance paco11_3_1_inst T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 (gf_0 gf_1 gf_2 : rel11 T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10->_) r_0 r_1 r_2 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 : paco_class (paco11_3_1 gf_0 gf_1 gf_2 r_0 r_1 r_2 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10) := -{ pacoacc := paco11_3_1_acc gf_0 gf_1 gf_2; - pacomult := paco11_3_1_mult gf_0 gf_1 gf_2; - pacofold := paco11_3_1_fold gf_0 gf_1 gf_2; - pacounfold := paco11_3_1_unfold gf_0 gf_1 gf_2 }. - -Instance paco11_3_2_inst T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 (gf_0 gf_1 gf_2 : rel11 T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10->_) r_0 r_1 r_2 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 : paco_class (paco11_3_2 gf_0 gf_1 gf_2 r_0 r_1 r_2 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10) := -{ pacoacc := paco11_3_2_acc gf_0 gf_1 gf_2; - pacomult := paco11_3_2_mult gf_0 gf_1 gf_2; - pacofold := paco11_3_2_fold gf_0 gf_1 gf_2; - pacounfold := paco11_3_2_unfold gf_0 gf_1 gf_2 }. - diff --git a/src/paco12.v b/src/paco12.v index 5fcb7a3..81d54e3 100644 --- a/src/paco12.v +++ b/src/paco12.v @@ -255,6 +255,19 @@ Qed. End Arg12_1. +Arguments paco12_acc : clear implicits. +Arguments paco12_mon : clear implicits. +Arguments paco12_mult_strong : clear implicits. +Arguments paco12_mult : clear implicits. +Arguments paco12_fold : clear implicits. +Arguments paco12_unfold : clear implicits. + +Global Instance paco12_inst (gf : rel12 T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11->_) r x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 : paco_class (paco12 gf r x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11) := +{ pacoacc := paco12_acc gf; + pacomult := paco12_mult gf; + pacofold := paco12_fold gf; + pacounfold := paco12_unfold gf }. + (** 2 Mutual Coinduction *) Section Arg12_2. @@ -432,6 +445,31 @@ Qed. End Arg12_2. +Arguments paco12_2_0_acc : clear implicits. +Arguments paco12_2_1_acc : clear implicits. +Arguments paco12_2_0_mon : clear implicits. +Arguments paco12_2_1_mon : clear implicits. +Arguments paco12_2_0_mult_strong : clear implicits. +Arguments paco12_2_1_mult_strong : clear implicits. +Arguments paco12_2_0_mult : clear implicits. +Arguments paco12_2_1_mult : clear implicits. +Arguments paco12_2_0_fold : clear implicits. +Arguments paco12_2_1_fold : clear implicits. +Arguments paco12_2_0_unfold : clear implicits. +Arguments paco12_2_1_unfold : clear implicits. + +Global Instance paco12_2_0_inst (gf_0 gf_1 : rel12 T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11->_) r_0 r_1 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 : paco_class (paco12_2_0 gf_0 gf_1 r_0 r_1 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11) := +{ pacoacc := paco12_2_0_acc gf_0 gf_1; + pacomult := paco12_2_0_mult gf_0 gf_1; + pacofold := paco12_2_0_fold gf_0 gf_1; + pacounfold := paco12_2_0_unfold gf_0 gf_1 }. + +Global Instance paco12_2_1_inst (gf_0 gf_1 : rel12 T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11->_) r_0 r_1 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 : paco_class (paco12_2_1 gf_0 gf_1 r_0 r_1 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11) := +{ pacoacc := paco12_2_1_acc gf_0 gf_1; + pacomult := paco12_2_1_mult gf_0 gf_1; + pacofold := paco12_2_1_fold gf_0 gf_1; + pacounfold := paco12_2_1_unfold gf_0 gf_1 }. + (** 3 Mutual Coinduction *) Section Arg12_3. @@ -685,6 +723,43 @@ Qed. End Arg12_3. +Arguments paco12_3_0_acc : clear implicits. +Arguments paco12_3_1_acc : clear implicits. +Arguments paco12_3_2_acc : clear implicits. +Arguments paco12_3_0_mon : clear implicits. +Arguments paco12_3_1_mon : clear implicits. +Arguments paco12_3_2_mon : clear implicits. +Arguments paco12_3_0_mult_strong : clear implicits. +Arguments paco12_3_1_mult_strong : clear implicits. +Arguments paco12_3_2_mult_strong : clear implicits. +Arguments paco12_3_0_mult : clear implicits. +Arguments paco12_3_1_mult : clear implicits. +Arguments paco12_3_2_mult : clear implicits. +Arguments paco12_3_0_fold : clear implicits. +Arguments paco12_3_1_fold : clear implicits. +Arguments paco12_3_2_fold : clear implicits. +Arguments paco12_3_0_unfold : clear implicits. +Arguments paco12_3_1_unfold : clear implicits. +Arguments paco12_3_2_unfold : clear implicits. + +Global Instance paco12_3_0_inst (gf_0 gf_1 gf_2 : rel12 T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11->_) r_0 r_1 r_2 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 : paco_class (paco12_3_0 gf_0 gf_1 gf_2 r_0 r_1 r_2 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11) := +{ pacoacc := paco12_3_0_acc gf_0 gf_1 gf_2; + pacomult := paco12_3_0_mult gf_0 gf_1 gf_2; + pacofold := paco12_3_0_fold gf_0 gf_1 gf_2; + pacounfold := paco12_3_0_unfold gf_0 gf_1 gf_2 }. + +Global Instance paco12_3_1_inst (gf_0 gf_1 gf_2 : rel12 T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11->_) r_0 r_1 r_2 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 : paco_class (paco12_3_1 gf_0 gf_1 gf_2 r_0 r_1 r_2 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11) := +{ pacoacc := paco12_3_1_acc gf_0 gf_1 gf_2; + pacomult := paco12_3_1_mult gf_0 gf_1 gf_2; + pacofold := paco12_3_1_fold gf_0 gf_1 gf_2; + pacounfold := paco12_3_1_unfold gf_0 gf_1 gf_2 }. + +Global Instance paco12_3_2_inst (gf_0 gf_1 gf_2 : rel12 T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11->_) r_0 r_1 r_2 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 : paco_class (paco12_3_2 gf_0 gf_1 gf_2 r_0 r_1 r_2 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11) := +{ pacoacc := paco12_3_2_acc gf_0 gf_1 gf_2; + pacomult := paco12_3_2_mult gf_0 gf_1 gf_2; + pacofold := paco12_3_2_fold gf_0 gf_1 gf_2; + pacounfold := paco12_3_2_unfold gf_0 gf_1 gf_2 }. + End PACO12. Global Opaque paco12. @@ -693,19 +768,6 @@ Hint Unfold upaco12. Hint Resolve paco12_fold. Hint Unfold monotone12. -Arguments paco12_acc [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 ]. -Arguments paco12_mon [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 ]. -Arguments paco12_mult_strong [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 ]. -Arguments paco12_mult [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 ]. -Arguments paco12_fold [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 ]. -Arguments paco12_unfold [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 ]. - -Instance paco12_inst T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 (gf : rel12 T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11->_) r x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 : paco_class (paco12 gf r x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11) := -{ pacoacc := paco12_acc gf; - pacomult := paco12_mult gf; - pacofold := paco12_fold gf; - pacounfold := paco12_unfold gf }. - Global Opaque paco12_2_0. Global Opaque paco12_2_1. @@ -715,31 +777,6 @@ Hint Resolve paco12_2_0_fold. Hint Resolve paco12_2_1_fold. Hint Unfold monotone12_2. -Arguments paco12_2_0_acc [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 ]. -Arguments paco12_2_1_acc [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 ]. -Arguments paco12_2_0_mon [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 ]. -Arguments paco12_2_1_mon [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 ]. -Arguments paco12_2_0_mult_strong [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 ]. -Arguments paco12_2_1_mult_strong [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 ]. -Arguments paco12_2_0_mult [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 ]. -Arguments paco12_2_1_mult [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 ]. -Arguments paco12_2_0_fold [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 ]. -Arguments paco12_2_1_fold [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 ]. -Arguments paco12_2_0_unfold [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 ]. -Arguments paco12_2_1_unfold [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 ]. - -Instance paco12_2_0_inst T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 (gf_0 gf_1 : rel12 T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11->_) r_0 r_1 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 : paco_class (paco12_2_0 gf_0 gf_1 r_0 r_1 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11) := -{ pacoacc := paco12_2_0_acc gf_0 gf_1; - pacomult := paco12_2_0_mult gf_0 gf_1; - pacofold := paco12_2_0_fold gf_0 gf_1; - pacounfold := paco12_2_0_unfold gf_0 gf_1 }. - -Instance paco12_2_1_inst T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 (gf_0 gf_1 : rel12 T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11->_) r_0 r_1 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 : paco_class (paco12_2_1 gf_0 gf_1 r_0 r_1 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11) := -{ pacoacc := paco12_2_1_acc gf_0 gf_1; - pacomult := paco12_2_1_mult gf_0 gf_1; - pacofold := paco12_2_1_fold gf_0 gf_1; - pacounfold := paco12_2_1_unfold gf_0 gf_1 }. - Global Opaque paco12_3_0. Global Opaque paco12_3_1. Global Opaque paco12_3_2. @@ -752,40 +789,3 @@ Hint Resolve paco12_3_1_fold. Hint Resolve paco12_3_2_fold. Hint Unfold monotone12_3. -Arguments paco12_3_0_acc [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 ]. -Arguments paco12_3_1_acc [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 ]. -Arguments paco12_3_2_acc [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 ]. -Arguments paco12_3_0_mon [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 ]. -Arguments paco12_3_1_mon [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 ]. -Arguments paco12_3_2_mon [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 ]. -Arguments paco12_3_0_mult_strong [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 ]. -Arguments paco12_3_1_mult_strong [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 ]. -Arguments paco12_3_2_mult_strong [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 ]. -Arguments paco12_3_0_mult [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 ]. -Arguments paco12_3_1_mult [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 ]. -Arguments paco12_3_2_mult [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 ]. -Arguments paco12_3_0_fold [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 ]. -Arguments paco12_3_1_fold [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 ]. -Arguments paco12_3_2_fold [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 ]. -Arguments paco12_3_0_unfold [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 ]. -Arguments paco12_3_1_unfold [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 ]. -Arguments paco12_3_2_unfold [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 ]. - -Instance paco12_3_0_inst T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 (gf_0 gf_1 gf_2 : rel12 T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11->_) r_0 r_1 r_2 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 : paco_class (paco12_3_0 gf_0 gf_1 gf_2 r_0 r_1 r_2 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11) := -{ pacoacc := paco12_3_0_acc gf_0 gf_1 gf_2; - pacomult := paco12_3_0_mult gf_0 gf_1 gf_2; - pacofold := paco12_3_0_fold gf_0 gf_1 gf_2; - pacounfold := paco12_3_0_unfold gf_0 gf_1 gf_2 }. - -Instance paco12_3_1_inst T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 (gf_0 gf_1 gf_2 : rel12 T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11->_) r_0 r_1 r_2 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 : paco_class (paco12_3_1 gf_0 gf_1 gf_2 r_0 r_1 r_2 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11) := -{ pacoacc := paco12_3_1_acc gf_0 gf_1 gf_2; - pacomult := paco12_3_1_mult gf_0 gf_1 gf_2; - pacofold := paco12_3_1_fold gf_0 gf_1 gf_2; - pacounfold := paco12_3_1_unfold gf_0 gf_1 gf_2 }. - -Instance paco12_3_2_inst T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 (gf_0 gf_1 gf_2 : rel12 T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11->_) r_0 r_1 r_2 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 : paco_class (paco12_3_2 gf_0 gf_1 gf_2 r_0 r_1 r_2 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11) := -{ pacoacc := paco12_3_2_acc gf_0 gf_1 gf_2; - pacomult := paco12_3_2_mult gf_0 gf_1 gf_2; - pacofold := paco12_3_2_fold gf_0 gf_1 gf_2; - pacounfold := paco12_3_2_unfold gf_0 gf_1 gf_2 }. - diff --git a/src/paco13.v b/src/paco13.v index 0dc46ce..32da67b 100644 --- a/src/paco13.v +++ b/src/paco13.v @@ -257,6 +257,19 @@ Qed. End Arg13_1. +Arguments paco13_acc : clear implicits. +Arguments paco13_mon : clear implicits. +Arguments paco13_mult_strong : clear implicits. +Arguments paco13_mult : clear implicits. +Arguments paco13_fold : clear implicits. +Arguments paco13_unfold : clear implicits. + +Global Instance paco13_inst (gf : rel13 T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 T12->_) r x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 : paco_class (paco13 gf r x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12) := +{ pacoacc := paco13_acc gf; + pacomult := paco13_mult gf; + pacofold := paco13_fold gf; + pacounfold := paco13_unfold gf }. + (** 2 Mutual Coinduction *) Section Arg13_2. @@ -434,6 +447,31 @@ Qed. End Arg13_2. +Arguments paco13_2_0_acc : clear implicits. +Arguments paco13_2_1_acc : clear implicits. +Arguments paco13_2_0_mon : clear implicits. +Arguments paco13_2_1_mon : clear implicits. +Arguments paco13_2_0_mult_strong : clear implicits. +Arguments paco13_2_1_mult_strong : clear implicits. +Arguments paco13_2_0_mult : clear implicits. +Arguments paco13_2_1_mult : clear implicits. +Arguments paco13_2_0_fold : clear implicits. +Arguments paco13_2_1_fold : clear implicits. +Arguments paco13_2_0_unfold : clear implicits. +Arguments paco13_2_1_unfold : clear implicits. + +Global Instance paco13_2_0_inst (gf_0 gf_1 : rel13 T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 T12->_) r_0 r_1 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 : paco_class (paco13_2_0 gf_0 gf_1 r_0 r_1 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12) := +{ pacoacc := paco13_2_0_acc gf_0 gf_1; + pacomult := paco13_2_0_mult gf_0 gf_1; + pacofold := paco13_2_0_fold gf_0 gf_1; + pacounfold := paco13_2_0_unfold gf_0 gf_1 }. + +Global Instance paco13_2_1_inst (gf_0 gf_1 : rel13 T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 T12->_) r_0 r_1 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 : paco_class (paco13_2_1 gf_0 gf_1 r_0 r_1 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12) := +{ pacoacc := paco13_2_1_acc gf_0 gf_1; + pacomult := paco13_2_1_mult gf_0 gf_1; + pacofold := paco13_2_1_fold gf_0 gf_1; + pacounfold := paco13_2_1_unfold gf_0 gf_1 }. + (** 3 Mutual Coinduction *) Section Arg13_3. @@ -687,6 +725,43 @@ Qed. End Arg13_3. +Arguments paco13_3_0_acc : clear implicits. +Arguments paco13_3_1_acc : clear implicits. +Arguments paco13_3_2_acc : clear implicits. +Arguments paco13_3_0_mon : clear implicits. +Arguments paco13_3_1_mon : clear implicits. +Arguments paco13_3_2_mon : clear implicits. +Arguments paco13_3_0_mult_strong : clear implicits. +Arguments paco13_3_1_mult_strong : clear implicits. +Arguments paco13_3_2_mult_strong : clear implicits. +Arguments paco13_3_0_mult : clear implicits. +Arguments paco13_3_1_mult : clear implicits. +Arguments paco13_3_2_mult : clear implicits. +Arguments paco13_3_0_fold : clear implicits. +Arguments paco13_3_1_fold : clear implicits. +Arguments paco13_3_2_fold : clear implicits. +Arguments paco13_3_0_unfold : clear implicits. +Arguments paco13_3_1_unfold : clear implicits. +Arguments paco13_3_2_unfold : clear implicits. + +Global Instance paco13_3_0_inst (gf_0 gf_1 gf_2 : rel13 T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 T12->_) r_0 r_1 r_2 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 : paco_class (paco13_3_0 gf_0 gf_1 gf_2 r_0 r_1 r_2 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12) := +{ pacoacc := paco13_3_0_acc gf_0 gf_1 gf_2; + pacomult := paco13_3_0_mult gf_0 gf_1 gf_2; + pacofold := paco13_3_0_fold gf_0 gf_1 gf_2; + pacounfold := paco13_3_0_unfold gf_0 gf_1 gf_2 }. + +Global Instance paco13_3_1_inst (gf_0 gf_1 gf_2 : rel13 T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 T12->_) r_0 r_1 r_2 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 : paco_class (paco13_3_1 gf_0 gf_1 gf_2 r_0 r_1 r_2 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12) := +{ pacoacc := paco13_3_1_acc gf_0 gf_1 gf_2; + pacomult := paco13_3_1_mult gf_0 gf_1 gf_2; + pacofold := paco13_3_1_fold gf_0 gf_1 gf_2; + pacounfold := paco13_3_1_unfold gf_0 gf_1 gf_2 }. + +Global Instance paco13_3_2_inst (gf_0 gf_1 gf_2 : rel13 T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 T12->_) r_0 r_1 r_2 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 : paco_class (paco13_3_2 gf_0 gf_1 gf_2 r_0 r_1 r_2 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12) := +{ pacoacc := paco13_3_2_acc gf_0 gf_1 gf_2; + pacomult := paco13_3_2_mult gf_0 gf_1 gf_2; + pacofold := paco13_3_2_fold gf_0 gf_1 gf_2; + pacounfold := paco13_3_2_unfold gf_0 gf_1 gf_2 }. + End PACO13. Global Opaque paco13. @@ -695,19 +770,6 @@ Hint Unfold upaco13. Hint Resolve paco13_fold. Hint Unfold monotone13. -Arguments paco13_acc [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 T12 ]. -Arguments paco13_mon [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 T12 ]. -Arguments paco13_mult_strong [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 T12 ]. -Arguments paco13_mult [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 T12 ]. -Arguments paco13_fold [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 T12 ]. -Arguments paco13_unfold [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 T12 ]. - -Instance paco13_inst T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 T12 (gf : rel13 T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 T12->_) r x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 : paco_class (paco13 gf r x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12) := -{ pacoacc := paco13_acc gf; - pacomult := paco13_mult gf; - pacofold := paco13_fold gf; - pacounfold := paco13_unfold gf }. - Global Opaque paco13_2_0. Global Opaque paco13_2_1. @@ -717,31 +779,6 @@ Hint Resolve paco13_2_0_fold. Hint Resolve paco13_2_1_fold. Hint Unfold monotone13_2. -Arguments paco13_2_0_acc [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 T12 ]. -Arguments paco13_2_1_acc [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 T12 ]. -Arguments paco13_2_0_mon [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 T12 ]. -Arguments paco13_2_1_mon [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 T12 ]. -Arguments paco13_2_0_mult_strong [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 T12 ]. -Arguments paco13_2_1_mult_strong [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 T12 ]. -Arguments paco13_2_0_mult [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 T12 ]. -Arguments paco13_2_1_mult [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 T12 ]. -Arguments paco13_2_0_fold [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 T12 ]. -Arguments paco13_2_1_fold [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 T12 ]. -Arguments paco13_2_0_unfold [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 T12 ]. -Arguments paco13_2_1_unfold [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 T12 ]. - -Instance paco13_2_0_inst T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 T12 (gf_0 gf_1 : rel13 T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 T12->_) r_0 r_1 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 : paco_class (paco13_2_0 gf_0 gf_1 r_0 r_1 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12) := -{ pacoacc := paco13_2_0_acc gf_0 gf_1; - pacomult := paco13_2_0_mult gf_0 gf_1; - pacofold := paco13_2_0_fold gf_0 gf_1; - pacounfold := paco13_2_0_unfold gf_0 gf_1 }. - -Instance paco13_2_1_inst T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 T12 (gf_0 gf_1 : rel13 T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 T12->_) r_0 r_1 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 : paco_class (paco13_2_1 gf_0 gf_1 r_0 r_1 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12) := -{ pacoacc := paco13_2_1_acc gf_0 gf_1; - pacomult := paco13_2_1_mult gf_0 gf_1; - pacofold := paco13_2_1_fold gf_0 gf_1; - pacounfold := paco13_2_1_unfold gf_0 gf_1 }. - Global Opaque paco13_3_0. Global Opaque paco13_3_1. Global Opaque paco13_3_2. @@ -754,40 +791,3 @@ Hint Resolve paco13_3_1_fold. Hint Resolve paco13_3_2_fold. Hint Unfold monotone13_3. -Arguments paco13_3_0_acc [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 T12 ]. -Arguments paco13_3_1_acc [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 T12 ]. -Arguments paco13_3_2_acc [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 T12 ]. -Arguments paco13_3_0_mon [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 T12 ]. -Arguments paco13_3_1_mon [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 T12 ]. -Arguments paco13_3_2_mon [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 T12 ]. -Arguments paco13_3_0_mult_strong [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 T12 ]. -Arguments paco13_3_1_mult_strong [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 T12 ]. -Arguments paco13_3_2_mult_strong [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 T12 ]. -Arguments paco13_3_0_mult [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 T12 ]. -Arguments paco13_3_1_mult [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 T12 ]. -Arguments paco13_3_2_mult [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 T12 ]. -Arguments paco13_3_0_fold [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 T12 ]. -Arguments paco13_3_1_fold [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 T12 ]. -Arguments paco13_3_2_fold [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 T12 ]. -Arguments paco13_3_0_unfold [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 T12 ]. -Arguments paco13_3_1_unfold [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 T12 ]. -Arguments paco13_3_2_unfold [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 T12 ]. - -Instance paco13_3_0_inst T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 T12 (gf_0 gf_1 gf_2 : rel13 T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 T12->_) r_0 r_1 r_2 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 : paco_class (paco13_3_0 gf_0 gf_1 gf_2 r_0 r_1 r_2 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12) := -{ pacoacc := paco13_3_0_acc gf_0 gf_1 gf_2; - pacomult := paco13_3_0_mult gf_0 gf_1 gf_2; - pacofold := paco13_3_0_fold gf_0 gf_1 gf_2; - pacounfold := paco13_3_0_unfold gf_0 gf_1 gf_2 }. - -Instance paco13_3_1_inst T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 T12 (gf_0 gf_1 gf_2 : rel13 T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 T12->_) r_0 r_1 r_2 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 : paco_class (paco13_3_1 gf_0 gf_1 gf_2 r_0 r_1 r_2 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12) := -{ pacoacc := paco13_3_1_acc gf_0 gf_1 gf_2; - pacomult := paco13_3_1_mult gf_0 gf_1 gf_2; - pacofold := paco13_3_1_fold gf_0 gf_1 gf_2; - pacounfold := paco13_3_1_unfold gf_0 gf_1 gf_2 }. - -Instance paco13_3_2_inst T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 T12 (gf_0 gf_1 gf_2 : rel13 T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 T12->_) r_0 r_1 r_2 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 : paco_class (paco13_3_2 gf_0 gf_1 gf_2 r_0 r_1 r_2 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12) := -{ pacoacc := paco13_3_2_acc gf_0 gf_1 gf_2; - pacomult := paco13_3_2_mult gf_0 gf_1 gf_2; - pacofold := paco13_3_2_fold gf_0 gf_1 gf_2; - pacounfold := paco13_3_2_unfold gf_0 gf_1 gf_2 }. - diff --git a/src/paco14.v b/src/paco14.v index f03d402..25f691a 100644 --- a/src/paco14.v +++ b/src/paco14.v @@ -259,6 +259,19 @@ Qed. End Arg14_1. +Arguments paco14_acc : clear implicits. +Arguments paco14_mon : clear implicits. +Arguments paco14_mult_strong : clear implicits. +Arguments paco14_mult : clear implicits. +Arguments paco14_fold : clear implicits. +Arguments paco14_unfold : clear implicits. + +Global Instance paco14_inst (gf : rel14 T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 T12 T13->_) r x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 : paco_class (paco14 gf r x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13) := +{ pacoacc := paco14_acc gf; + pacomult := paco14_mult gf; + pacofold := paco14_fold gf; + pacounfold := paco14_unfold gf }. + (** 2 Mutual Coinduction *) Section Arg14_2. @@ -436,6 +449,31 @@ Qed. End Arg14_2. +Arguments paco14_2_0_acc : clear implicits. +Arguments paco14_2_1_acc : clear implicits. +Arguments paco14_2_0_mon : clear implicits. +Arguments paco14_2_1_mon : clear implicits. +Arguments paco14_2_0_mult_strong : clear implicits. +Arguments paco14_2_1_mult_strong : clear implicits. +Arguments paco14_2_0_mult : clear implicits. +Arguments paco14_2_1_mult : clear implicits. +Arguments paco14_2_0_fold : clear implicits. +Arguments paco14_2_1_fold : clear implicits. +Arguments paco14_2_0_unfold : clear implicits. +Arguments paco14_2_1_unfold : clear implicits. + +Global Instance paco14_2_0_inst (gf_0 gf_1 : rel14 T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 T12 T13->_) r_0 r_1 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 : paco_class (paco14_2_0 gf_0 gf_1 r_0 r_1 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13) := +{ pacoacc := paco14_2_0_acc gf_0 gf_1; + pacomult := paco14_2_0_mult gf_0 gf_1; + pacofold := paco14_2_0_fold gf_0 gf_1; + pacounfold := paco14_2_0_unfold gf_0 gf_1 }. + +Global Instance paco14_2_1_inst (gf_0 gf_1 : rel14 T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 T12 T13->_) r_0 r_1 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 : paco_class (paco14_2_1 gf_0 gf_1 r_0 r_1 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13) := +{ pacoacc := paco14_2_1_acc gf_0 gf_1; + pacomult := paco14_2_1_mult gf_0 gf_1; + pacofold := paco14_2_1_fold gf_0 gf_1; + pacounfold := paco14_2_1_unfold gf_0 gf_1 }. + (** 3 Mutual Coinduction *) Section Arg14_3. @@ -689,6 +727,43 @@ Qed. End Arg14_3. +Arguments paco14_3_0_acc : clear implicits. +Arguments paco14_3_1_acc : clear implicits. +Arguments paco14_3_2_acc : clear implicits. +Arguments paco14_3_0_mon : clear implicits. +Arguments paco14_3_1_mon : clear implicits. +Arguments paco14_3_2_mon : clear implicits. +Arguments paco14_3_0_mult_strong : clear implicits. +Arguments paco14_3_1_mult_strong : clear implicits. +Arguments paco14_3_2_mult_strong : clear implicits. +Arguments paco14_3_0_mult : clear implicits. +Arguments paco14_3_1_mult : clear implicits. +Arguments paco14_3_2_mult : clear implicits. +Arguments paco14_3_0_fold : clear implicits. +Arguments paco14_3_1_fold : clear implicits. +Arguments paco14_3_2_fold : clear implicits. +Arguments paco14_3_0_unfold : clear implicits. +Arguments paco14_3_1_unfold : clear implicits. +Arguments paco14_3_2_unfold : clear implicits. + +Global Instance paco14_3_0_inst (gf_0 gf_1 gf_2 : rel14 T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 T12 T13->_) r_0 r_1 r_2 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 : paco_class (paco14_3_0 gf_0 gf_1 gf_2 r_0 r_1 r_2 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13) := +{ pacoacc := paco14_3_0_acc gf_0 gf_1 gf_2; + pacomult := paco14_3_0_mult gf_0 gf_1 gf_2; + pacofold := paco14_3_0_fold gf_0 gf_1 gf_2; + pacounfold := paco14_3_0_unfold gf_0 gf_1 gf_2 }. + +Global Instance paco14_3_1_inst (gf_0 gf_1 gf_2 : rel14 T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 T12 T13->_) r_0 r_1 r_2 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 : paco_class (paco14_3_1 gf_0 gf_1 gf_2 r_0 r_1 r_2 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13) := +{ pacoacc := paco14_3_1_acc gf_0 gf_1 gf_2; + pacomult := paco14_3_1_mult gf_0 gf_1 gf_2; + pacofold := paco14_3_1_fold gf_0 gf_1 gf_2; + pacounfold := paco14_3_1_unfold gf_0 gf_1 gf_2 }. + +Global Instance paco14_3_2_inst (gf_0 gf_1 gf_2 : rel14 T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 T12 T13->_) r_0 r_1 r_2 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 : paco_class (paco14_3_2 gf_0 gf_1 gf_2 r_0 r_1 r_2 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13) := +{ pacoacc := paco14_3_2_acc gf_0 gf_1 gf_2; + pacomult := paco14_3_2_mult gf_0 gf_1 gf_2; + pacofold := paco14_3_2_fold gf_0 gf_1 gf_2; + pacounfold := paco14_3_2_unfold gf_0 gf_1 gf_2 }. + End PACO14. Global Opaque paco14. @@ -697,19 +772,6 @@ Hint Unfold upaco14. Hint Resolve paco14_fold. Hint Unfold monotone14. -Arguments paco14_acc [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 T12 T13 ]. -Arguments paco14_mon [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 T12 T13 ]. -Arguments paco14_mult_strong [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 T12 T13 ]. -Arguments paco14_mult [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 T12 T13 ]. -Arguments paco14_fold [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 T12 T13 ]. -Arguments paco14_unfold [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 T12 T13 ]. - -Instance paco14_inst T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 T12 T13 (gf : rel14 T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 T12 T13->_) r x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 : paco_class (paco14 gf r x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13) := -{ pacoacc := paco14_acc gf; - pacomult := paco14_mult gf; - pacofold := paco14_fold gf; - pacounfold := paco14_unfold gf }. - Global Opaque paco14_2_0. Global Opaque paco14_2_1. @@ -719,31 +781,6 @@ Hint Resolve paco14_2_0_fold. Hint Resolve paco14_2_1_fold. Hint Unfold monotone14_2. -Arguments paco14_2_0_acc [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 T12 T13 ]. -Arguments paco14_2_1_acc [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 T12 T13 ]. -Arguments paco14_2_0_mon [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 T12 T13 ]. -Arguments paco14_2_1_mon [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 T12 T13 ]. -Arguments paco14_2_0_mult_strong [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 T12 T13 ]. -Arguments paco14_2_1_mult_strong [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 T12 T13 ]. -Arguments paco14_2_0_mult [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 T12 T13 ]. -Arguments paco14_2_1_mult [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 T12 T13 ]. -Arguments paco14_2_0_fold [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 T12 T13 ]. -Arguments paco14_2_1_fold [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 T12 T13 ]. -Arguments paco14_2_0_unfold [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 T12 T13 ]. -Arguments paco14_2_1_unfold [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 T12 T13 ]. - -Instance paco14_2_0_inst T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 T12 T13 (gf_0 gf_1 : rel14 T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 T12 T13->_) r_0 r_1 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 : paco_class (paco14_2_0 gf_0 gf_1 r_0 r_1 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13) := -{ pacoacc := paco14_2_0_acc gf_0 gf_1; - pacomult := paco14_2_0_mult gf_0 gf_1; - pacofold := paco14_2_0_fold gf_0 gf_1; - pacounfold := paco14_2_0_unfold gf_0 gf_1 }. - -Instance paco14_2_1_inst T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 T12 T13 (gf_0 gf_1 : rel14 T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 T12 T13->_) r_0 r_1 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 : paco_class (paco14_2_1 gf_0 gf_1 r_0 r_1 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13) := -{ pacoacc := paco14_2_1_acc gf_0 gf_1; - pacomult := paco14_2_1_mult gf_0 gf_1; - pacofold := paco14_2_1_fold gf_0 gf_1; - pacounfold := paco14_2_1_unfold gf_0 gf_1 }. - Global Opaque paco14_3_0. Global Opaque paco14_3_1. Global Opaque paco14_3_2. @@ -756,40 +793,3 @@ Hint Resolve paco14_3_1_fold. Hint Resolve paco14_3_2_fold. Hint Unfold monotone14_3. -Arguments paco14_3_0_acc [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 T12 T13 ]. -Arguments paco14_3_1_acc [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 T12 T13 ]. -Arguments paco14_3_2_acc [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 T12 T13 ]. -Arguments paco14_3_0_mon [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 T12 T13 ]. -Arguments paco14_3_1_mon [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 T12 T13 ]. -Arguments paco14_3_2_mon [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 T12 T13 ]. -Arguments paco14_3_0_mult_strong [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 T12 T13 ]. -Arguments paco14_3_1_mult_strong [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 T12 T13 ]. -Arguments paco14_3_2_mult_strong [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 T12 T13 ]. -Arguments paco14_3_0_mult [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 T12 T13 ]. -Arguments paco14_3_1_mult [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 T12 T13 ]. -Arguments paco14_3_2_mult [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 T12 T13 ]. -Arguments paco14_3_0_fold [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 T12 T13 ]. -Arguments paco14_3_1_fold [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 T12 T13 ]. -Arguments paco14_3_2_fold [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 T12 T13 ]. -Arguments paco14_3_0_unfold [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 T12 T13 ]. -Arguments paco14_3_1_unfold [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 T12 T13 ]. -Arguments paco14_3_2_unfold [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 T12 T13 ]. - -Instance paco14_3_0_inst T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 T12 T13 (gf_0 gf_1 gf_2 : rel14 T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 T12 T13->_) r_0 r_1 r_2 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 : paco_class (paco14_3_0 gf_0 gf_1 gf_2 r_0 r_1 r_2 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13) := -{ pacoacc := paco14_3_0_acc gf_0 gf_1 gf_2; - pacomult := paco14_3_0_mult gf_0 gf_1 gf_2; - pacofold := paco14_3_0_fold gf_0 gf_1 gf_2; - pacounfold := paco14_3_0_unfold gf_0 gf_1 gf_2 }. - -Instance paco14_3_1_inst T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 T12 T13 (gf_0 gf_1 gf_2 : rel14 T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 T12 T13->_) r_0 r_1 r_2 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 : paco_class (paco14_3_1 gf_0 gf_1 gf_2 r_0 r_1 r_2 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13) := -{ pacoacc := paco14_3_1_acc gf_0 gf_1 gf_2; - pacomult := paco14_3_1_mult gf_0 gf_1 gf_2; - pacofold := paco14_3_1_fold gf_0 gf_1 gf_2; - pacounfold := paco14_3_1_unfold gf_0 gf_1 gf_2 }. - -Instance paco14_3_2_inst T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 T12 T13 (gf_0 gf_1 gf_2 : rel14 T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 T12 T13->_) r_0 r_1 r_2 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 : paco_class (paco14_3_2 gf_0 gf_1 gf_2 r_0 r_1 r_2 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13) := -{ pacoacc := paco14_3_2_acc gf_0 gf_1 gf_2; - pacomult := paco14_3_2_mult gf_0 gf_1 gf_2; - pacofold := paco14_3_2_fold gf_0 gf_1 gf_2; - pacounfold := paco14_3_2_unfold gf_0 gf_1 gf_2 }. - diff --git a/src/paco15.v b/src/paco15.v index 7311ae3..047cd8d 100644 --- a/src/paco15.v +++ b/src/paco15.v @@ -261,6 +261,19 @@ Qed. End Arg15_1. +Arguments paco15_acc : clear implicits. +Arguments paco15_mon : clear implicits. +Arguments paco15_mult_strong : clear implicits. +Arguments paco15_mult : clear implicits. +Arguments paco15_fold : clear implicits. +Arguments paco15_unfold : clear implicits. + +Global Instance paco15_inst (gf : rel15 T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 T12 T13 T14->_) r x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 : paco_class (paco15 gf r x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14) := +{ pacoacc := paco15_acc gf; + pacomult := paco15_mult gf; + pacofold := paco15_fold gf; + pacounfold := paco15_unfold gf }. + (** 2 Mutual Coinduction *) Section Arg15_2. @@ -438,6 +451,31 @@ Qed. End Arg15_2. +Arguments paco15_2_0_acc : clear implicits. +Arguments paco15_2_1_acc : clear implicits. +Arguments paco15_2_0_mon : clear implicits. +Arguments paco15_2_1_mon : clear implicits. +Arguments paco15_2_0_mult_strong : clear implicits. +Arguments paco15_2_1_mult_strong : clear implicits. +Arguments paco15_2_0_mult : clear implicits. +Arguments paco15_2_1_mult : clear implicits. +Arguments paco15_2_0_fold : clear implicits. +Arguments paco15_2_1_fold : clear implicits. +Arguments paco15_2_0_unfold : clear implicits. +Arguments paco15_2_1_unfold : clear implicits. + +Global Instance paco15_2_0_inst (gf_0 gf_1 : rel15 T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 T12 T13 T14->_) r_0 r_1 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 : paco_class (paco15_2_0 gf_0 gf_1 r_0 r_1 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14) := +{ pacoacc := paco15_2_0_acc gf_0 gf_1; + pacomult := paco15_2_0_mult gf_0 gf_1; + pacofold := paco15_2_0_fold gf_0 gf_1; + pacounfold := paco15_2_0_unfold gf_0 gf_1 }. + +Global Instance paco15_2_1_inst (gf_0 gf_1 : rel15 T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 T12 T13 T14->_) r_0 r_1 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 : paco_class (paco15_2_1 gf_0 gf_1 r_0 r_1 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14) := +{ pacoacc := paco15_2_1_acc gf_0 gf_1; + pacomult := paco15_2_1_mult gf_0 gf_1; + pacofold := paco15_2_1_fold gf_0 gf_1; + pacounfold := paco15_2_1_unfold gf_0 gf_1 }. + (** 3 Mutual Coinduction *) Section Arg15_3. @@ -691,6 +729,43 @@ Qed. End Arg15_3. +Arguments paco15_3_0_acc : clear implicits. +Arguments paco15_3_1_acc : clear implicits. +Arguments paco15_3_2_acc : clear implicits. +Arguments paco15_3_0_mon : clear implicits. +Arguments paco15_3_1_mon : clear implicits. +Arguments paco15_3_2_mon : clear implicits. +Arguments paco15_3_0_mult_strong : clear implicits. +Arguments paco15_3_1_mult_strong : clear implicits. +Arguments paco15_3_2_mult_strong : clear implicits. +Arguments paco15_3_0_mult : clear implicits. +Arguments paco15_3_1_mult : clear implicits. +Arguments paco15_3_2_mult : clear implicits. +Arguments paco15_3_0_fold : clear implicits. +Arguments paco15_3_1_fold : clear implicits. +Arguments paco15_3_2_fold : clear implicits. +Arguments paco15_3_0_unfold : clear implicits. +Arguments paco15_3_1_unfold : clear implicits. +Arguments paco15_3_2_unfold : clear implicits. + +Global Instance paco15_3_0_inst (gf_0 gf_1 gf_2 : rel15 T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 T12 T13 T14->_) r_0 r_1 r_2 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 : paco_class (paco15_3_0 gf_0 gf_1 gf_2 r_0 r_1 r_2 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14) := +{ pacoacc := paco15_3_0_acc gf_0 gf_1 gf_2; + pacomult := paco15_3_0_mult gf_0 gf_1 gf_2; + pacofold := paco15_3_0_fold gf_0 gf_1 gf_2; + pacounfold := paco15_3_0_unfold gf_0 gf_1 gf_2 }. + +Global Instance paco15_3_1_inst (gf_0 gf_1 gf_2 : rel15 T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 T12 T13 T14->_) r_0 r_1 r_2 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 : paco_class (paco15_3_1 gf_0 gf_1 gf_2 r_0 r_1 r_2 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14) := +{ pacoacc := paco15_3_1_acc gf_0 gf_1 gf_2; + pacomult := paco15_3_1_mult gf_0 gf_1 gf_2; + pacofold := paco15_3_1_fold gf_0 gf_1 gf_2; + pacounfold := paco15_3_1_unfold gf_0 gf_1 gf_2 }. + +Global Instance paco15_3_2_inst (gf_0 gf_1 gf_2 : rel15 T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 T12 T13 T14->_) r_0 r_1 r_2 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 : paco_class (paco15_3_2 gf_0 gf_1 gf_2 r_0 r_1 r_2 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14) := +{ pacoacc := paco15_3_2_acc gf_0 gf_1 gf_2; + pacomult := paco15_3_2_mult gf_0 gf_1 gf_2; + pacofold := paco15_3_2_fold gf_0 gf_1 gf_2; + pacounfold := paco15_3_2_unfold gf_0 gf_1 gf_2 }. + End PACO15. Global Opaque paco15. @@ -699,19 +774,6 @@ Hint Unfold upaco15. Hint Resolve paco15_fold. Hint Unfold monotone15. -Arguments paco15_acc [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 T12 T13 T14 ]. -Arguments paco15_mon [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 T12 T13 T14 ]. -Arguments paco15_mult_strong [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 T12 T13 T14 ]. -Arguments paco15_mult [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 T12 T13 T14 ]. -Arguments paco15_fold [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 T12 T13 T14 ]. -Arguments paco15_unfold [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 T12 T13 T14 ]. - -Instance paco15_inst T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 T12 T13 T14 (gf : rel15 T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 T12 T13 T14->_) r x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 : paco_class (paco15 gf r x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14) := -{ pacoacc := paco15_acc gf; - pacomult := paco15_mult gf; - pacofold := paco15_fold gf; - pacounfold := paco15_unfold gf }. - Global Opaque paco15_2_0. Global Opaque paco15_2_1. @@ -721,31 +783,6 @@ Hint Resolve paco15_2_0_fold. Hint Resolve paco15_2_1_fold. Hint Unfold monotone15_2. -Arguments paco15_2_0_acc [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 T12 T13 T14 ]. -Arguments paco15_2_1_acc [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 T12 T13 T14 ]. -Arguments paco15_2_0_mon [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 T12 T13 T14 ]. -Arguments paco15_2_1_mon [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 T12 T13 T14 ]. -Arguments paco15_2_0_mult_strong [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 T12 T13 T14 ]. -Arguments paco15_2_1_mult_strong [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 T12 T13 T14 ]. -Arguments paco15_2_0_mult [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 T12 T13 T14 ]. -Arguments paco15_2_1_mult [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 T12 T13 T14 ]. -Arguments paco15_2_0_fold [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 T12 T13 T14 ]. -Arguments paco15_2_1_fold [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 T12 T13 T14 ]. -Arguments paco15_2_0_unfold [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 T12 T13 T14 ]. -Arguments paco15_2_1_unfold [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 T12 T13 T14 ]. - -Instance paco15_2_0_inst T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 T12 T13 T14 (gf_0 gf_1 : rel15 T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 T12 T13 T14->_) r_0 r_1 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 : paco_class (paco15_2_0 gf_0 gf_1 r_0 r_1 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14) := -{ pacoacc := paco15_2_0_acc gf_0 gf_1; - pacomult := paco15_2_0_mult gf_0 gf_1; - pacofold := paco15_2_0_fold gf_0 gf_1; - pacounfold := paco15_2_0_unfold gf_0 gf_1 }. - -Instance paco15_2_1_inst T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 T12 T13 T14 (gf_0 gf_1 : rel15 T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 T12 T13 T14->_) r_0 r_1 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 : paco_class (paco15_2_1 gf_0 gf_1 r_0 r_1 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14) := -{ pacoacc := paco15_2_1_acc gf_0 gf_1; - pacomult := paco15_2_1_mult gf_0 gf_1; - pacofold := paco15_2_1_fold gf_0 gf_1; - pacounfold := paco15_2_1_unfold gf_0 gf_1 }. - Global Opaque paco15_3_0. Global Opaque paco15_3_1. Global Opaque paco15_3_2. @@ -758,40 +795,3 @@ Hint Resolve paco15_3_1_fold. Hint Resolve paco15_3_2_fold. Hint Unfold monotone15_3. -Arguments paco15_3_0_acc [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 T12 T13 T14 ]. -Arguments paco15_3_1_acc [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 T12 T13 T14 ]. -Arguments paco15_3_2_acc [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 T12 T13 T14 ]. -Arguments paco15_3_0_mon [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 T12 T13 T14 ]. -Arguments paco15_3_1_mon [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 T12 T13 T14 ]. -Arguments paco15_3_2_mon [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 T12 T13 T14 ]. -Arguments paco15_3_0_mult_strong [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 T12 T13 T14 ]. -Arguments paco15_3_1_mult_strong [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 T12 T13 T14 ]. -Arguments paco15_3_2_mult_strong [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 T12 T13 T14 ]. -Arguments paco15_3_0_mult [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 T12 T13 T14 ]. -Arguments paco15_3_1_mult [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 T12 T13 T14 ]. -Arguments paco15_3_2_mult [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 T12 T13 T14 ]. -Arguments paco15_3_0_fold [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 T12 T13 T14 ]. -Arguments paco15_3_1_fold [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 T12 T13 T14 ]. -Arguments paco15_3_2_fold [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 T12 T13 T14 ]. -Arguments paco15_3_0_unfold [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 T12 T13 T14 ]. -Arguments paco15_3_1_unfold [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 T12 T13 T14 ]. -Arguments paco15_3_2_unfold [ T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 T12 T13 T14 ]. - -Instance paco15_3_0_inst T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 T12 T13 T14 (gf_0 gf_1 gf_2 : rel15 T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 T12 T13 T14->_) r_0 r_1 r_2 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 : paco_class (paco15_3_0 gf_0 gf_1 gf_2 r_0 r_1 r_2 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14) := -{ pacoacc := paco15_3_0_acc gf_0 gf_1 gf_2; - pacomult := paco15_3_0_mult gf_0 gf_1 gf_2; - pacofold := paco15_3_0_fold gf_0 gf_1 gf_2; - pacounfold := paco15_3_0_unfold gf_0 gf_1 gf_2 }. - -Instance paco15_3_1_inst T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 T12 T13 T14 (gf_0 gf_1 gf_2 : rel15 T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 T12 T13 T14->_) r_0 r_1 r_2 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 : paco_class (paco15_3_1 gf_0 gf_1 gf_2 r_0 r_1 r_2 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14) := -{ pacoacc := paco15_3_1_acc gf_0 gf_1 gf_2; - pacomult := paco15_3_1_mult gf_0 gf_1 gf_2; - pacofold := paco15_3_1_fold gf_0 gf_1 gf_2; - pacounfold := paco15_3_1_unfold gf_0 gf_1 gf_2 }. - -Instance paco15_3_2_inst T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 T12 T13 T14 (gf_0 gf_1 gf_2 : rel15 T0 T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11 T12 T13 T14->_) r_0 r_1 r_2 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 : paco_class (paco15_3_2 gf_0 gf_1 gf_2 r_0 r_1 r_2 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14) := -{ pacoacc := paco15_3_2_acc gf_0 gf_1 gf_2; - pacomult := paco15_3_2_mult gf_0 gf_1 gf_2; - pacofold := paco15_3_2_fold gf_0 gf_1 gf_2; - pacounfold := paco15_3_2_unfold gf_0 gf_1 gf_2 }. - diff --git a/src/paco2.v b/src/paco2.v index 49cd449..6d6b680 100644 --- a/src/paco2.v +++ b/src/paco2.v @@ -235,6 +235,19 @@ Qed. End Arg2_1. +Arguments paco2_acc : clear implicits. +Arguments paco2_mon : clear implicits. +Arguments paco2_mult_strong : clear implicits. +Arguments paco2_mult : clear implicits. +Arguments paco2_fold : clear implicits. +Arguments paco2_unfold : clear implicits. + +Global Instance paco2_inst (gf : rel2 T0 T1->_) r x0 x1 : paco_class (paco2 gf r x0 x1) := +{ pacoacc := paco2_acc gf; + pacomult := paco2_mult gf; + pacofold := paco2_fold gf; + pacounfold := paco2_unfold gf }. + (** 2 Mutual Coinduction *) Section Arg2_2. @@ -412,6 +425,31 @@ Qed. End Arg2_2. +Arguments paco2_2_0_acc : clear implicits. +Arguments paco2_2_1_acc : clear implicits. +Arguments paco2_2_0_mon : clear implicits. +Arguments paco2_2_1_mon : clear implicits. +Arguments paco2_2_0_mult_strong : clear implicits. +Arguments paco2_2_1_mult_strong : clear implicits. +Arguments paco2_2_0_mult : clear implicits. +Arguments paco2_2_1_mult : clear implicits. +Arguments paco2_2_0_fold : clear implicits. +Arguments paco2_2_1_fold : clear implicits. +Arguments paco2_2_0_unfold : clear implicits. +Arguments paco2_2_1_unfold : clear implicits. + +Global Instance paco2_2_0_inst (gf_0 gf_1 : rel2 T0 T1->_) r_0 r_1 x0 x1 : paco_class (paco2_2_0 gf_0 gf_1 r_0 r_1 x0 x1) := +{ pacoacc := paco2_2_0_acc gf_0 gf_1; + pacomult := paco2_2_0_mult gf_0 gf_1; + pacofold := paco2_2_0_fold gf_0 gf_1; + pacounfold := paco2_2_0_unfold gf_0 gf_1 }. + +Global Instance paco2_2_1_inst (gf_0 gf_1 : rel2 T0 T1->_) r_0 r_1 x0 x1 : paco_class (paco2_2_1 gf_0 gf_1 r_0 r_1 x0 x1) := +{ pacoacc := paco2_2_1_acc gf_0 gf_1; + pacomult := paco2_2_1_mult gf_0 gf_1; + pacofold := paco2_2_1_fold gf_0 gf_1; + pacounfold := paco2_2_1_unfold gf_0 gf_1 }. + (** 3 Mutual Coinduction *) Section Arg2_3. @@ -665,6 +703,43 @@ Qed. End Arg2_3. +Arguments paco2_3_0_acc : clear implicits. +Arguments paco2_3_1_acc : clear implicits. +Arguments paco2_3_2_acc : clear implicits. +Arguments paco2_3_0_mon : clear implicits. +Arguments paco2_3_1_mon : clear implicits. +Arguments paco2_3_2_mon : clear implicits. +Arguments paco2_3_0_mult_strong : clear implicits. +Arguments paco2_3_1_mult_strong : clear implicits. +Arguments paco2_3_2_mult_strong : clear implicits. +Arguments paco2_3_0_mult : clear implicits. +Arguments paco2_3_1_mult : clear implicits. +Arguments paco2_3_2_mult : clear implicits. +Arguments paco2_3_0_fold : clear implicits. +Arguments paco2_3_1_fold : clear implicits. +Arguments paco2_3_2_fold : clear implicits. +Arguments paco2_3_0_unfold : clear implicits. +Arguments paco2_3_1_unfold : clear implicits. +Arguments paco2_3_2_unfold : clear implicits. + +Global Instance paco2_3_0_inst (gf_0 gf_1 gf_2 : rel2 T0 T1->_) r_0 r_1 r_2 x0 x1 : paco_class (paco2_3_0 gf_0 gf_1 gf_2 r_0 r_1 r_2 x0 x1) := +{ pacoacc := paco2_3_0_acc gf_0 gf_1 gf_2; + pacomult := paco2_3_0_mult gf_0 gf_1 gf_2; + pacofold := paco2_3_0_fold gf_0 gf_1 gf_2; + pacounfold := paco2_3_0_unfold gf_0 gf_1 gf_2 }. + +Global Instance paco2_3_1_inst (gf_0 gf_1 gf_2 : rel2 T0 T1->_) r_0 r_1 r_2 x0 x1 : paco_class (paco2_3_1 gf_0 gf_1 gf_2 r_0 r_1 r_2 x0 x1) := +{ pacoacc := paco2_3_1_acc gf_0 gf_1 gf_2; + pacomult := paco2_3_1_mult gf_0 gf_1 gf_2; + pacofold := paco2_3_1_fold gf_0 gf_1 gf_2; + pacounfold := paco2_3_1_unfold gf_0 gf_1 gf_2 }. + +Global Instance paco2_3_2_inst (gf_0 gf_1 gf_2 : rel2 T0 T1->_) r_0 r_1 r_2 x0 x1 : paco_class (paco2_3_2 gf_0 gf_1 gf_2 r_0 r_1 r_2 x0 x1) := +{ pacoacc := paco2_3_2_acc gf_0 gf_1 gf_2; + pacomult := paco2_3_2_mult gf_0 gf_1 gf_2; + pacofold := paco2_3_2_fold gf_0 gf_1 gf_2; + pacounfold := paco2_3_2_unfold gf_0 gf_1 gf_2 }. + End PACO2. Global Opaque paco2. @@ -673,19 +748,6 @@ Hint Unfold upaco2. Hint Resolve paco2_fold. Hint Unfold monotone2. -Arguments paco2_acc [ T0 T1 ]. -Arguments paco2_mon [ T0 T1 ]. -Arguments paco2_mult_strong [ T0 T1 ]. -Arguments paco2_mult [ T0 T1 ]. -Arguments paco2_fold [ T0 T1 ]. -Arguments paco2_unfold [ T0 T1 ]. - -Instance paco2_inst T0 T1 (gf : rel2 T0 T1->_) r x0 x1 : paco_class (paco2 gf r x0 x1) := -{ pacoacc := paco2_acc gf; - pacomult := paco2_mult gf; - pacofold := paco2_fold gf; - pacounfold := paco2_unfold gf }. - Global Opaque paco2_2_0. Global Opaque paco2_2_1. @@ -695,31 +757,6 @@ Hint Resolve paco2_2_0_fold. Hint Resolve paco2_2_1_fold. Hint Unfold monotone2_2. -Arguments paco2_2_0_acc [ T0 T1 ]. -Arguments paco2_2_1_acc [ T0 T1 ]. -Arguments paco2_2_0_mon [ T0 T1 ]. -Arguments paco2_2_1_mon [ T0 T1 ]. -Arguments paco2_2_0_mult_strong [ T0 T1 ]. -Arguments paco2_2_1_mult_strong [ T0 T1 ]. -Arguments paco2_2_0_mult [ T0 T1 ]. -Arguments paco2_2_1_mult [ T0 T1 ]. -Arguments paco2_2_0_fold [ T0 T1 ]. -Arguments paco2_2_1_fold [ T0 T1 ]. -Arguments paco2_2_0_unfold [ T0 T1 ]. -Arguments paco2_2_1_unfold [ T0 T1 ]. - -Instance paco2_2_0_inst T0 T1 (gf_0 gf_1 : rel2 T0 T1->_) r_0 r_1 x0 x1 : paco_class (paco2_2_0 gf_0 gf_1 r_0 r_1 x0 x1) := -{ pacoacc := paco2_2_0_acc gf_0 gf_1; - pacomult := paco2_2_0_mult gf_0 gf_1; - pacofold := paco2_2_0_fold gf_0 gf_1; - pacounfold := paco2_2_0_unfold gf_0 gf_1 }. - -Instance paco2_2_1_inst T0 T1 (gf_0 gf_1 : rel2 T0 T1->_) r_0 r_1 x0 x1 : paco_class (paco2_2_1 gf_0 gf_1 r_0 r_1 x0 x1) := -{ pacoacc := paco2_2_1_acc gf_0 gf_1; - pacomult := paco2_2_1_mult gf_0 gf_1; - pacofold := paco2_2_1_fold gf_0 gf_1; - pacounfold := paco2_2_1_unfold gf_0 gf_1 }. - Global Opaque paco2_3_0. Global Opaque paco2_3_1. Global Opaque paco2_3_2. @@ -732,40 +769,3 @@ Hint Resolve paco2_3_1_fold. Hint Resolve paco2_3_2_fold. Hint Unfold monotone2_3. -Arguments paco2_3_0_acc [ T0 T1 ]. -Arguments paco2_3_1_acc [ T0 T1 ]. -Arguments paco2_3_2_acc [ T0 T1 ]. -Arguments paco2_3_0_mon [ T0 T1 ]. -Arguments paco2_3_1_mon [ T0 T1 ]. -Arguments paco2_3_2_mon [ T0 T1 ]. -Arguments paco2_3_0_mult_strong [ T0 T1 ]. -Arguments paco2_3_1_mult_strong [ T0 T1 ]. -Arguments paco2_3_2_mult_strong [ T0 T1 ]. -Arguments paco2_3_0_mult [ T0 T1 ]. -Arguments paco2_3_1_mult [ T0 T1 ]. -Arguments paco2_3_2_mult [ T0 T1 ]. -Arguments paco2_3_0_fold [ T0 T1 ]. -Arguments paco2_3_1_fold [ T0 T1 ]. -Arguments paco2_3_2_fold [ T0 T1 ]. -Arguments paco2_3_0_unfold [ T0 T1 ]. -Arguments paco2_3_1_unfold [ T0 T1 ]. -Arguments paco2_3_2_unfold [ T0 T1 ]. - -Instance paco2_3_0_inst T0 T1 (gf_0 gf_1 gf_2 : rel2 T0 T1->_) r_0 r_1 r_2 x0 x1 : paco_class (paco2_3_0 gf_0 gf_1 gf_2 r_0 r_1 r_2 x0 x1) := -{ pacoacc := paco2_3_0_acc gf_0 gf_1 gf_2; - pacomult := paco2_3_0_mult gf_0 gf_1 gf_2; - pacofold := paco2_3_0_fold gf_0 gf_1 gf_2; - pacounfold := paco2_3_0_unfold gf_0 gf_1 gf_2 }. - -Instance paco2_3_1_inst T0 T1 (gf_0 gf_1 gf_2 : rel2 T0 T1->_) r_0 r_1 r_2 x0 x1 : paco_class (paco2_3_1 gf_0 gf_1 gf_2 r_0 r_1 r_2 x0 x1) := -{ pacoacc := paco2_3_1_acc gf_0 gf_1 gf_2; - pacomult := paco2_3_1_mult gf_0 gf_1 gf_2; - pacofold := paco2_3_1_fold gf_0 gf_1 gf_2; - pacounfold := paco2_3_1_unfold gf_0 gf_1 gf_2 }. - -Instance paco2_3_2_inst T0 T1 (gf_0 gf_1 gf_2 : rel2 T0 T1->_) r_0 r_1 r_2 x0 x1 : paco_class (paco2_3_2 gf_0 gf_1 gf_2 r_0 r_1 r_2 x0 x1) := -{ pacoacc := paco2_3_2_acc gf_0 gf_1 gf_2; - pacomult := paco2_3_2_mult gf_0 gf_1 gf_2; - pacofold := paco2_3_2_fold gf_0 gf_1 gf_2; - pacounfold := paco2_3_2_unfold gf_0 gf_1 gf_2 }. - diff --git a/src/paco3.v b/src/paco3.v index 0b411a9..d07ddc7 100644 --- a/src/paco3.v +++ b/src/paco3.v @@ -237,6 +237,19 @@ Qed. End Arg3_1. +Arguments paco3_acc : clear implicits. +Arguments paco3_mon : clear implicits. +Arguments paco3_mult_strong : clear implicits. +Arguments paco3_mult : clear implicits. +Arguments paco3_fold : clear implicits. +Arguments paco3_unfold : clear implicits. + +Global Instance paco3_inst (gf : rel3 T0 T1 T2->_) r x0 x1 x2 : paco_class (paco3 gf r x0 x1 x2) := +{ pacoacc := paco3_acc gf; + pacomult := paco3_mult gf; + pacofold := paco3_fold gf; + pacounfold := paco3_unfold gf }. + (** 2 Mutual Coinduction *) Section Arg3_2. @@ -414,6 +427,31 @@ Qed. End Arg3_2. +Arguments paco3_2_0_acc : clear implicits. +Arguments paco3_2_1_acc : clear implicits. +Arguments paco3_2_0_mon : clear implicits. +Arguments paco3_2_1_mon : clear implicits. +Arguments paco3_2_0_mult_strong : clear implicits. +Arguments paco3_2_1_mult_strong : clear implicits. +Arguments paco3_2_0_mult : clear implicits. +Arguments paco3_2_1_mult : clear implicits. +Arguments paco3_2_0_fold : clear implicits. +Arguments paco3_2_1_fold : clear implicits. +Arguments paco3_2_0_unfold : clear implicits. +Arguments paco3_2_1_unfold : clear implicits. + +Global Instance paco3_2_0_inst (gf_0 gf_1 : rel3 T0 T1 T2->_) r_0 r_1 x0 x1 x2 : paco_class (paco3_2_0 gf_0 gf_1 r_0 r_1 x0 x1 x2) := +{ pacoacc := paco3_2_0_acc gf_0 gf_1; + pacomult := paco3_2_0_mult gf_0 gf_1; + pacofold := paco3_2_0_fold gf_0 gf_1; + pacounfold := paco3_2_0_unfold gf_0 gf_1 }. + +Global Instance paco3_2_1_inst (gf_0 gf_1 : rel3 T0 T1 T2->_) r_0 r_1 x0 x1 x2 : paco_class (paco3_2_1 gf_0 gf_1 r_0 r_1 x0 x1 x2) := +{ pacoacc := paco3_2_1_acc gf_0 gf_1; + pacomult := paco3_2_1_mult gf_0 gf_1; + pacofold := paco3_2_1_fold gf_0 gf_1; + pacounfold := paco3_2_1_unfold gf_0 gf_1 }. + (** 3 Mutual Coinduction *) Section Arg3_3. @@ -667,6 +705,43 @@ Qed. End Arg3_3. +Arguments paco3_3_0_acc : clear implicits. +Arguments paco3_3_1_acc : clear implicits. +Arguments paco3_3_2_acc : clear implicits. +Arguments paco3_3_0_mon : clear implicits. +Arguments paco3_3_1_mon : clear implicits. +Arguments paco3_3_2_mon : clear implicits. +Arguments paco3_3_0_mult_strong : clear implicits. +Arguments paco3_3_1_mult_strong : clear implicits. +Arguments paco3_3_2_mult_strong : clear implicits. +Arguments paco3_3_0_mult : clear implicits. +Arguments paco3_3_1_mult : clear implicits. +Arguments paco3_3_2_mult : clear implicits. +Arguments paco3_3_0_fold : clear implicits. +Arguments paco3_3_1_fold : clear implicits. +Arguments paco3_3_2_fold : clear implicits. +Arguments paco3_3_0_unfold : clear implicits. +Arguments paco3_3_1_unfold : clear implicits. +Arguments paco3_3_2_unfold : clear implicits. + +Global Instance paco3_3_0_inst (gf_0 gf_1 gf_2 : rel3 T0 T1 T2->_) r_0 r_1 r_2 x0 x1 x2 : paco_class (paco3_3_0 gf_0 gf_1 gf_2 r_0 r_1 r_2 x0 x1 x2) := +{ pacoacc := paco3_3_0_acc gf_0 gf_1 gf_2; + pacomult := paco3_3_0_mult gf_0 gf_1 gf_2; + pacofold := paco3_3_0_fold gf_0 gf_1 gf_2; + pacounfold := paco3_3_0_unfold gf_0 gf_1 gf_2 }. + +Global Instance paco3_3_1_inst (gf_0 gf_1 gf_2 : rel3 T0 T1 T2->_) r_0 r_1 r_2 x0 x1 x2 : paco_class (paco3_3_1 gf_0 gf_1 gf_2 r_0 r_1 r_2 x0 x1 x2) := +{ pacoacc := paco3_3_1_acc gf_0 gf_1 gf_2; + pacomult := paco3_3_1_mult gf_0 gf_1 gf_2; + pacofold := paco3_3_1_fold gf_0 gf_1 gf_2; + pacounfold := paco3_3_1_unfold gf_0 gf_1 gf_2 }. + +Global Instance paco3_3_2_inst (gf_0 gf_1 gf_2 : rel3 T0 T1 T2->_) r_0 r_1 r_2 x0 x1 x2 : paco_class (paco3_3_2 gf_0 gf_1 gf_2 r_0 r_1 r_2 x0 x1 x2) := +{ pacoacc := paco3_3_2_acc gf_0 gf_1 gf_2; + pacomult := paco3_3_2_mult gf_0 gf_1 gf_2; + pacofold := paco3_3_2_fold gf_0 gf_1 gf_2; + pacounfold := paco3_3_2_unfold gf_0 gf_1 gf_2 }. + End PACO3. Global Opaque paco3. @@ -675,19 +750,6 @@ Hint Unfold upaco3. Hint Resolve paco3_fold. Hint Unfold monotone3. -Arguments paco3_acc [ T0 T1 T2 ]. -Arguments paco3_mon [ T0 T1 T2 ]. -Arguments paco3_mult_strong [ T0 T1 T2 ]. -Arguments paco3_mult [ T0 T1 T2 ]. -Arguments paco3_fold [ T0 T1 T2 ]. -Arguments paco3_unfold [ T0 T1 T2 ]. - -Instance paco3_inst T0 T1 T2 (gf : rel3 T0 T1 T2->_) r x0 x1 x2 : paco_class (paco3 gf r x0 x1 x2) := -{ pacoacc := paco3_acc gf; - pacomult := paco3_mult gf; - pacofold := paco3_fold gf; - pacounfold := paco3_unfold gf }. - Global Opaque paco3_2_0. Global Opaque paco3_2_1. @@ -697,31 +759,6 @@ Hint Resolve paco3_2_0_fold. Hint Resolve paco3_2_1_fold. Hint Unfold monotone3_2. -Arguments paco3_2_0_acc [ T0 T1 T2 ]. -Arguments paco3_2_1_acc [ T0 T1 T2 ]. -Arguments paco3_2_0_mon [ T0 T1 T2 ]. -Arguments paco3_2_1_mon [ T0 T1 T2 ]. -Arguments paco3_2_0_mult_strong [ T0 T1 T2 ]. -Arguments paco3_2_1_mult_strong [ T0 T1 T2 ]. -Arguments paco3_2_0_mult [ T0 T1 T2 ]. -Arguments paco3_2_1_mult [ T0 T1 T2 ]. -Arguments paco3_2_0_fold [ T0 T1 T2 ]. -Arguments paco3_2_1_fold [ T0 T1 T2 ]. -Arguments paco3_2_0_unfold [ T0 T1 T2 ]. -Arguments paco3_2_1_unfold [ T0 T1 T2 ]. - -Instance paco3_2_0_inst T0 T1 T2 (gf_0 gf_1 : rel3 T0 T1 T2->_) r_0 r_1 x0 x1 x2 : paco_class (paco3_2_0 gf_0 gf_1 r_0 r_1 x0 x1 x2) := -{ pacoacc := paco3_2_0_acc gf_0 gf_1; - pacomult := paco3_2_0_mult gf_0 gf_1; - pacofold := paco3_2_0_fold gf_0 gf_1; - pacounfold := paco3_2_0_unfold gf_0 gf_1 }. - -Instance paco3_2_1_inst T0 T1 T2 (gf_0 gf_1 : rel3 T0 T1 T2->_) r_0 r_1 x0 x1 x2 : paco_class (paco3_2_1 gf_0 gf_1 r_0 r_1 x0 x1 x2) := -{ pacoacc := paco3_2_1_acc gf_0 gf_1; - pacomult := paco3_2_1_mult gf_0 gf_1; - pacofold := paco3_2_1_fold gf_0 gf_1; - pacounfold := paco3_2_1_unfold gf_0 gf_1 }. - Global Opaque paco3_3_0. Global Opaque paco3_3_1. Global Opaque paco3_3_2. @@ -734,40 +771,3 @@ Hint Resolve paco3_3_1_fold. Hint Resolve paco3_3_2_fold. Hint Unfold monotone3_3. -Arguments paco3_3_0_acc [ T0 T1 T2 ]. -Arguments paco3_3_1_acc [ T0 T1 T2 ]. -Arguments paco3_3_2_acc [ T0 T1 T2 ]. -Arguments paco3_3_0_mon [ T0 T1 T2 ]. -Arguments paco3_3_1_mon [ T0 T1 T2 ]. -Arguments paco3_3_2_mon [ T0 T1 T2 ]. -Arguments paco3_3_0_mult_strong [ T0 T1 T2 ]. -Arguments paco3_3_1_mult_strong [ T0 T1 T2 ]. -Arguments paco3_3_2_mult_strong [ T0 T1 T2 ]. -Arguments paco3_3_0_mult [ T0 T1 T2 ]. -Arguments paco3_3_1_mult [ T0 T1 T2 ]. -Arguments paco3_3_2_mult [ T0 T1 T2 ]. -Arguments paco3_3_0_fold [ T0 T1 T2 ]. -Arguments paco3_3_1_fold [ T0 T1 T2 ]. -Arguments paco3_3_2_fold [ T0 T1 T2 ]. -Arguments paco3_3_0_unfold [ T0 T1 T2 ]. -Arguments paco3_3_1_unfold [ T0 T1 T2 ]. -Arguments paco3_3_2_unfold [ T0 T1 T2 ]. - -Instance paco3_3_0_inst T0 T1 T2 (gf_0 gf_1 gf_2 : rel3 T0 T1 T2->_) r_0 r_1 r_2 x0 x1 x2 : paco_class (paco3_3_0 gf_0 gf_1 gf_2 r_0 r_1 r_2 x0 x1 x2) := -{ pacoacc := paco3_3_0_acc gf_0 gf_1 gf_2; - pacomult := paco3_3_0_mult gf_0 gf_1 gf_2; - pacofold := paco3_3_0_fold gf_0 gf_1 gf_2; - pacounfold := paco3_3_0_unfold gf_0 gf_1 gf_2 }. - -Instance paco3_3_1_inst T0 T1 T2 (gf_0 gf_1 gf_2 : rel3 T0 T1 T2->_) r_0 r_1 r_2 x0 x1 x2 : paco_class (paco3_3_1 gf_0 gf_1 gf_2 r_0 r_1 r_2 x0 x1 x2) := -{ pacoacc := paco3_3_1_acc gf_0 gf_1 gf_2; - pacomult := paco3_3_1_mult gf_0 gf_1 gf_2; - pacofold := paco3_3_1_fold gf_0 gf_1 gf_2; - pacounfold := paco3_3_1_unfold gf_0 gf_1 gf_2 }. - -Instance paco3_3_2_inst T0 T1 T2 (gf_0 gf_1 gf_2 : rel3 T0 T1 T2->_) r_0 r_1 r_2 x0 x1 x2 : paco_class (paco3_3_2 gf_0 gf_1 gf_2 r_0 r_1 r_2 x0 x1 x2) := -{ pacoacc := paco3_3_2_acc gf_0 gf_1 gf_2; - pacomult := paco3_3_2_mult gf_0 gf_1 gf_2; - pacofold := paco3_3_2_fold gf_0 gf_1 gf_2; - pacounfold := paco3_3_2_unfold gf_0 gf_1 gf_2 }. - diff --git a/src/paco4.v b/src/paco4.v index 5939613..348d989 100644 --- a/src/paco4.v +++ b/src/paco4.v @@ -239,6 +239,19 @@ Qed. End Arg4_1. +Arguments paco4_acc : clear implicits. +Arguments paco4_mon : clear implicits. +Arguments paco4_mult_strong : clear implicits. +Arguments paco4_mult : clear implicits. +Arguments paco4_fold : clear implicits. +Arguments paco4_unfold : clear implicits. + +Global Instance paco4_inst (gf : rel4 T0 T1 T2 T3->_) r x0 x1 x2 x3 : paco_class (paco4 gf r x0 x1 x2 x3) := +{ pacoacc := paco4_acc gf; + pacomult := paco4_mult gf; + pacofold := paco4_fold gf; + pacounfold := paco4_unfold gf }. + (** 2 Mutual Coinduction *) Section Arg4_2. @@ -416,6 +429,31 @@ Qed. End Arg4_2. +Arguments paco4_2_0_acc : clear implicits. +Arguments paco4_2_1_acc : clear implicits. +Arguments paco4_2_0_mon : clear implicits. +Arguments paco4_2_1_mon : clear implicits. +Arguments paco4_2_0_mult_strong : clear implicits. +Arguments paco4_2_1_mult_strong : clear implicits. +Arguments paco4_2_0_mult : clear implicits. +Arguments paco4_2_1_mult : clear implicits. +Arguments paco4_2_0_fold : clear implicits. +Arguments paco4_2_1_fold : clear implicits. +Arguments paco4_2_0_unfold : clear implicits. +Arguments paco4_2_1_unfold : clear implicits. + +Global Instance paco4_2_0_inst (gf_0 gf_1 : rel4 T0 T1 T2 T3->_) r_0 r_1 x0 x1 x2 x3 : paco_class (paco4_2_0 gf_0 gf_1 r_0 r_1 x0 x1 x2 x3) := +{ pacoacc := paco4_2_0_acc gf_0 gf_1; + pacomult := paco4_2_0_mult gf_0 gf_1; + pacofold := paco4_2_0_fold gf_0 gf_1; + pacounfold := paco4_2_0_unfold gf_0 gf_1 }. + +Global Instance paco4_2_1_inst (gf_0 gf_1 : rel4 T0 T1 T2 T3->_) r_0 r_1 x0 x1 x2 x3 : paco_class (paco4_2_1 gf_0 gf_1 r_0 r_1 x0 x1 x2 x3) := +{ pacoacc := paco4_2_1_acc gf_0 gf_1; + pacomult := paco4_2_1_mult gf_0 gf_1; + pacofold := paco4_2_1_fold gf_0 gf_1; + pacounfold := paco4_2_1_unfold gf_0 gf_1 }. + (** 3 Mutual Coinduction *) Section Arg4_3. @@ -669,6 +707,43 @@ Qed. End Arg4_3. +Arguments paco4_3_0_acc : clear implicits. +Arguments paco4_3_1_acc : clear implicits. +Arguments paco4_3_2_acc : clear implicits. +Arguments paco4_3_0_mon : clear implicits. +Arguments paco4_3_1_mon : clear implicits. +Arguments paco4_3_2_mon : clear implicits. +Arguments paco4_3_0_mult_strong : clear implicits. +Arguments paco4_3_1_mult_strong : clear implicits. +Arguments paco4_3_2_mult_strong : clear implicits. +Arguments paco4_3_0_mult : clear implicits. +Arguments paco4_3_1_mult : clear implicits. +Arguments paco4_3_2_mult : clear implicits. +Arguments paco4_3_0_fold : clear implicits. +Arguments paco4_3_1_fold : clear implicits. +Arguments paco4_3_2_fold : clear implicits. +Arguments paco4_3_0_unfold : clear implicits. +Arguments paco4_3_1_unfold : clear implicits. +Arguments paco4_3_2_unfold : clear implicits. + +Global Instance paco4_3_0_inst (gf_0 gf_1 gf_2 : rel4 T0 T1 T2 T3->_) r_0 r_1 r_2 x0 x1 x2 x3 : paco_class (paco4_3_0 gf_0 gf_1 gf_2 r_0 r_1 r_2 x0 x1 x2 x3) := +{ pacoacc := paco4_3_0_acc gf_0 gf_1 gf_2; + pacomult := paco4_3_0_mult gf_0 gf_1 gf_2; + pacofold := paco4_3_0_fold gf_0 gf_1 gf_2; + pacounfold := paco4_3_0_unfold gf_0 gf_1 gf_2 }. + +Global Instance paco4_3_1_inst (gf_0 gf_1 gf_2 : rel4 T0 T1 T2 T3->_) r_0 r_1 r_2 x0 x1 x2 x3 : paco_class (paco4_3_1 gf_0 gf_1 gf_2 r_0 r_1 r_2 x0 x1 x2 x3) := +{ pacoacc := paco4_3_1_acc gf_0 gf_1 gf_2; + pacomult := paco4_3_1_mult gf_0 gf_1 gf_2; + pacofold := paco4_3_1_fold gf_0 gf_1 gf_2; + pacounfold := paco4_3_1_unfold gf_0 gf_1 gf_2 }. + +Global Instance paco4_3_2_inst (gf_0 gf_1 gf_2 : rel4 T0 T1 T2 T3->_) r_0 r_1 r_2 x0 x1 x2 x3 : paco_class (paco4_3_2 gf_0 gf_1 gf_2 r_0 r_1 r_2 x0 x1 x2 x3) := +{ pacoacc := paco4_3_2_acc gf_0 gf_1 gf_2; + pacomult := paco4_3_2_mult gf_0 gf_1 gf_2; + pacofold := paco4_3_2_fold gf_0 gf_1 gf_2; + pacounfold := paco4_3_2_unfold gf_0 gf_1 gf_2 }. + End PACO4. Global Opaque paco4. @@ -677,19 +752,6 @@ Hint Unfold upaco4. Hint Resolve paco4_fold. Hint Unfold monotone4. -Arguments paco4_acc [ T0 T1 T2 T3 ]. -Arguments paco4_mon [ T0 T1 T2 T3 ]. -Arguments paco4_mult_strong [ T0 T1 T2 T3 ]. -Arguments paco4_mult [ T0 T1 T2 T3 ]. -Arguments paco4_fold [ T0 T1 T2 T3 ]. -Arguments paco4_unfold [ T0 T1 T2 T3 ]. - -Instance paco4_inst T0 T1 T2 T3 (gf : rel4 T0 T1 T2 T3->_) r x0 x1 x2 x3 : paco_class (paco4 gf r x0 x1 x2 x3) := -{ pacoacc := paco4_acc gf; - pacomult := paco4_mult gf; - pacofold := paco4_fold gf; - pacounfold := paco4_unfold gf }. - Global Opaque paco4_2_0. Global Opaque paco4_2_1. @@ -699,31 +761,6 @@ Hint Resolve paco4_2_0_fold. Hint Resolve paco4_2_1_fold. Hint Unfold monotone4_2. -Arguments paco4_2_0_acc [ T0 T1 T2 T3 ]. -Arguments paco4_2_1_acc [ T0 T1 T2 T3 ]. -Arguments paco4_2_0_mon [ T0 T1 T2 T3 ]. -Arguments paco4_2_1_mon [ T0 T1 T2 T3 ]. -Arguments paco4_2_0_mult_strong [ T0 T1 T2 T3 ]. -Arguments paco4_2_1_mult_strong [ T0 T1 T2 T3 ]. -Arguments paco4_2_0_mult [ T0 T1 T2 T3 ]. -Arguments paco4_2_1_mult [ T0 T1 T2 T3 ]. -Arguments paco4_2_0_fold [ T0 T1 T2 T3 ]. -Arguments paco4_2_1_fold [ T0 T1 T2 T3 ]. -Arguments paco4_2_0_unfold [ T0 T1 T2 T3 ]. -Arguments paco4_2_1_unfold [ T0 T1 T2 T3 ]. - -Instance paco4_2_0_inst T0 T1 T2 T3 (gf_0 gf_1 : rel4 T0 T1 T2 T3->_) r_0 r_1 x0 x1 x2 x3 : paco_class (paco4_2_0 gf_0 gf_1 r_0 r_1 x0 x1 x2 x3) := -{ pacoacc := paco4_2_0_acc gf_0 gf_1; - pacomult := paco4_2_0_mult gf_0 gf_1; - pacofold := paco4_2_0_fold gf_0 gf_1; - pacounfold := paco4_2_0_unfold gf_0 gf_1 }. - -Instance paco4_2_1_inst T0 T1 T2 T3 (gf_0 gf_1 : rel4 T0 T1 T2 T3->_) r_0 r_1 x0 x1 x2 x3 : paco_class (paco4_2_1 gf_0 gf_1 r_0 r_1 x0 x1 x2 x3) := -{ pacoacc := paco4_2_1_acc gf_0 gf_1; - pacomult := paco4_2_1_mult gf_0 gf_1; - pacofold := paco4_2_1_fold gf_0 gf_1; - pacounfold := paco4_2_1_unfold gf_0 gf_1 }. - Global Opaque paco4_3_0. Global Opaque paco4_3_1. Global Opaque paco4_3_2. @@ -736,40 +773,3 @@ Hint Resolve paco4_3_1_fold. Hint Resolve paco4_3_2_fold. Hint Unfold monotone4_3. -Arguments paco4_3_0_acc [ T0 T1 T2 T3 ]. -Arguments paco4_3_1_acc [ T0 T1 T2 T3 ]. -Arguments paco4_3_2_acc [ T0 T1 T2 T3 ]. -Arguments paco4_3_0_mon [ T0 T1 T2 T3 ]. -Arguments paco4_3_1_mon [ T0 T1 T2 T3 ]. -Arguments paco4_3_2_mon [ T0 T1 T2 T3 ]. -Arguments paco4_3_0_mult_strong [ T0 T1 T2 T3 ]. -Arguments paco4_3_1_mult_strong [ T0 T1 T2 T3 ]. -Arguments paco4_3_2_mult_strong [ T0 T1 T2 T3 ]. -Arguments paco4_3_0_mult [ T0 T1 T2 T3 ]. -Arguments paco4_3_1_mult [ T0 T1 T2 T3 ]. -Arguments paco4_3_2_mult [ T0 T1 T2 T3 ]. -Arguments paco4_3_0_fold [ T0 T1 T2 T3 ]. -Arguments paco4_3_1_fold [ T0 T1 T2 T3 ]. -Arguments paco4_3_2_fold [ T0 T1 T2 T3 ]. -Arguments paco4_3_0_unfold [ T0 T1 T2 T3 ]. -Arguments paco4_3_1_unfold [ T0 T1 T2 T3 ]. -Arguments paco4_3_2_unfold [ T0 T1 T2 T3 ]. - -Instance paco4_3_0_inst T0 T1 T2 T3 (gf_0 gf_1 gf_2 : rel4 T0 T1 T2 T3->_) r_0 r_1 r_2 x0 x1 x2 x3 : paco_class (paco4_3_0 gf_0 gf_1 gf_2 r_0 r_1 r_2 x0 x1 x2 x3) := -{ pacoacc := paco4_3_0_acc gf_0 gf_1 gf_2; - pacomult := paco4_3_0_mult gf_0 gf_1 gf_2; - pacofold := paco4_3_0_fold gf_0 gf_1 gf_2; - pacounfold := paco4_3_0_unfold gf_0 gf_1 gf_2 }. - -Instance paco4_3_1_inst T0 T1 T2 T3 (gf_0 gf_1 gf_2 : rel4 T0 T1 T2 T3->_) r_0 r_1 r_2 x0 x1 x2 x3 : paco_class (paco4_3_1 gf_0 gf_1 gf_2 r_0 r_1 r_2 x0 x1 x2 x3) := -{ pacoacc := paco4_3_1_acc gf_0 gf_1 gf_2; - pacomult := paco4_3_1_mult gf_0 gf_1 gf_2; - pacofold := paco4_3_1_fold gf_0 gf_1 gf_2; - pacounfold := paco4_3_1_unfold gf_0 gf_1 gf_2 }. - -Instance paco4_3_2_inst T0 T1 T2 T3 (gf_0 gf_1 gf_2 : rel4 T0 T1 T2 T3->_) r_0 r_1 r_2 x0 x1 x2 x3 : paco_class (paco4_3_2 gf_0 gf_1 gf_2 r_0 r_1 r_2 x0 x1 x2 x3) := -{ pacoacc := paco4_3_2_acc gf_0 gf_1 gf_2; - pacomult := paco4_3_2_mult gf_0 gf_1 gf_2; - pacofold := paco4_3_2_fold gf_0 gf_1 gf_2; - pacounfold := paco4_3_2_unfold gf_0 gf_1 gf_2 }. - diff --git a/src/paco5.v b/src/paco5.v index c8cf65f..0c68bfc 100644 --- a/src/paco5.v +++ b/src/paco5.v @@ -241,6 +241,19 @@ Qed. End Arg5_1. +Arguments paco5_acc : clear implicits. +Arguments paco5_mon : clear implicits. +Arguments paco5_mult_strong : clear implicits. +Arguments paco5_mult : clear implicits. +Arguments paco5_fold : clear implicits. +Arguments paco5_unfold : clear implicits. + +Global Instance paco5_inst (gf : rel5 T0 T1 T2 T3 T4->_) r x0 x1 x2 x3 x4 : paco_class (paco5 gf r x0 x1 x2 x3 x4) := +{ pacoacc := paco5_acc gf; + pacomult := paco5_mult gf; + pacofold := paco5_fold gf; + pacounfold := paco5_unfold gf }. + (** 2 Mutual Coinduction *) Section Arg5_2. @@ -418,6 +431,31 @@ Qed. End Arg5_2. +Arguments paco5_2_0_acc : clear implicits. +Arguments paco5_2_1_acc : clear implicits. +Arguments paco5_2_0_mon : clear implicits. +Arguments paco5_2_1_mon : clear implicits. +Arguments paco5_2_0_mult_strong : clear implicits. +Arguments paco5_2_1_mult_strong : clear implicits. +Arguments paco5_2_0_mult : clear implicits. +Arguments paco5_2_1_mult : clear implicits. +Arguments paco5_2_0_fold : clear implicits. +Arguments paco5_2_1_fold : clear implicits. +Arguments paco5_2_0_unfold : clear implicits. +Arguments paco5_2_1_unfold : clear implicits. + +Global Instance paco5_2_0_inst (gf_0 gf_1 : rel5 T0 T1 T2 T3 T4->_) r_0 r_1 x0 x1 x2 x3 x4 : paco_class (paco5_2_0 gf_0 gf_1 r_0 r_1 x0 x1 x2 x3 x4) := +{ pacoacc := paco5_2_0_acc gf_0 gf_1; + pacomult := paco5_2_0_mult gf_0 gf_1; + pacofold := paco5_2_0_fold gf_0 gf_1; + pacounfold := paco5_2_0_unfold gf_0 gf_1 }. + +Global Instance paco5_2_1_inst (gf_0 gf_1 : rel5 T0 T1 T2 T3 T4->_) r_0 r_1 x0 x1 x2 x3 x4 : paco_class (paco5_2_1 gf_0 gf_1 r_0 r_1 x0 x1 x2 x3 x4) := +{ pacoacc := paco5_2_1_acc gf_0 gf_1; + pacomult := paco5_2_1_mult gf_0 gf_1; + pacofold := paco5_2_1_fold gf_0 gf_1; + pacounfold := paco5_2_1_unfold gf_0 gf_1 }. + (** 3 Mutual Coinduction *) Section Arg5_3. @@ -671,6 +709,43 @@ Qed. End Arg5_3. +Arguments paco5_3_0_acc : clear implicits. +Arguments paco5_3_1_acc : clear implicits. +Arguments paco5_3_2_acc : clear implicits. +Arguments paco5_3_0_mon : clear implicits. +Arguments paco5_3_1_mon : clear implicits. +Arguments paco5_3_2_mon : clear implicits. +Arguments paco5_3_0_mult_strong : clear implicits. +Arguments paco5_3_1_mult_strong : clear implicits. +Arguments paco5_3_2_mult_strong : clear implicits. +Arguments paco5_3_0_mult : clear implicits. +Arguments paco5_3_1_mult : clear implicits. +Arguments paco5_3_2_mult : clear implicits. +Arguments paco5_3_0_fold : clear implicits. +Arguments paco5_3_1_fold : clear implicits. +Arguments paco5_3_2_fold : clear implicits. +Arguments paco5_3_0_unfold : clear implicits. +Arguments paco5_3_1_unfold : clear implicits. +Arguments paco5_3_2_unfold : clear implicits. + +Global Instance paco5_3_0_inst (gf_0 gf_1 gf_2 : rel5 T0 T1 T2 T3 T4->_) r_0 r_1 r_2 x0 x1 x2 x3 x4 : paco_class (paco5_3_0 gf_0 gf_1 gf_2 r_0 r_1 r_2 x0 x1 x2 x3 x4) := +{ pacoacc := paco5_3_0_acc gf_0 gf_1 gf_2; + pacomult := paco5_3_0_mult gf_0 gf_1 gf_2; + pacofold := paco5_3_0_fold gf_0 gf_1 gf_2; + pacounfold := paco5_3_0_unfold gf_0 gf_1 gf_2 }. + +Global Instance paco5_3_1_inst (gf_0 gf_1 gf_2 : rel5 T0 T1 T2 T3 T4->_) r_0 r_1 r_2 x0 x1 x2 x3 x4 : paco_class (paco5_3_1 gf_0 gf_1 gf_2 r_0 r_1 r_2 x0 x1 x2 x3 x4) := +{ pacoacc := paco5_3_1_acc gf_0 gf_1 gf_2; + pacomult := paco5_3_1_mult gf_0 gf_1 gf_2; + pacofold := paco5_3_1_fold gf_0 gf_1 gf_2; + pacounfold := paco5_3_1_unfold gf_0 gf_1 gf_2 }. + +Global Instance paco5_3_2_inst (gf_0 gf_1 gf_2 : rel5 T0 T1 T2 T3 T4->_) r_0 r_1 r_2 x0 x1 x2 x3 x4 : paco_class (paco5_3_2 gf_0 gf_1 gf_2 r_0 r_1 r_2 x0 x1 x2 x3 x4) := +{ pacoacc := paco5_3_2_acc gf_0 gf_1 gf_2; + pacomult := paco5_3_2_mult gf_0 gf_1 gf_2; + pacofold := paco5_3_2_fold gf_0 gf_1 gf_2; + pacounfold := paco5_3_2_unfold gf_0 gf_1 gf_2 }. + End PACO5. Global Opaque paco5. @@ -679,19 +754,6 @@ Hint Unfold upaco5. Hint Resolve paco5_fold. Hint Unfold monotone5. -Arguments paco5_acc [ T0 T1 T2 T3 T4 ]. -Arguments paco5_mon [ T0 T1 T2 T3 T4 ]. -Arguments paco5_mult_strong [ T0 T1 T2 T3 T4 ]. -Arguments paco5_mult [ T0 T1 T2 T3 T4 ]. -Arguments paco5_fold [ T0 T1 T2 T3 T4 ]. -Arguments paco5_unfold [ T0 T1 T2 T3 T4 ]. - -Instance paco5_inst T0 T1 T2 T3 T4 (gf : rel5 T0 T1 T2 T3 T4->_) r x0 x1 x2 x3 x4 : paco_class (paco5 gf r x0 x1 x2 x3 x4) := -{ pacoacc := paco5_acc gf; - pacomult := paco5_mult gf; - pacofold := paco5_fold gf; - pacounfold := paco5_unfold gf }. - Global Opaque paco5_2_0. Global Opaque paco5_2_1. @@ -701,31 +763,6 @@ Hint Resolve paco5_2_0_fold. Hint Resolve paco5_2_1_fold. Hint Unfold monotone5_2. -Arguments paco5_2_0_acc [ T0 T1 T2 T3 T4 ]. -Arguments paco5_2_1_acc [ T0 T1 T2 T3 T4 ]. -Arguments paco5_2_0_mon [ T0 T1 T2 T3 T4 ]. -Arguments paco5_2_1_mon [ T0 T1 T2 T3 T4 ]. -Arguments paco5_2_0_mult_strong [ T0 T1 T2 T3 T4 ]. -Arguments paco5_2_1_mult_strong [ T0 T1 T2 T3 T4 ]. -Arguments paco5_2_0_mult [ T0 T1 T2 T3 T4 ]. -Arguments paco5_2_1_mult [ T0 T1 T2 T3 T4 ]. -Arguments paco5_2_0_fold [ T0 T1 T2 T3 T4 ]. -Arguments paco5_2_1_fold [ T0 T1 T2 T3 T4 ]. -Arguments paco5_2_0_unfold [ T0 T1 T2 T3 T4 ]. -Arguments paco5_2_1_unfold [ T0 T1 T2 T3 T4 ]. - -Instance paco5_2_0_inst T0 T1 T2 T3 T4 (gf_0 gf_1 : rel5 T0 T1 T2 T3 T4->_) r_0 r_1 x0 x1 x2 x3 x4 : paco_class (paco5_2_0 gf_0 gf_1 r_0 r_1 x0 x1 x2 x3 x4) := -{ pacoacc := paco5_2_0_acc gf_0 gf_1; - pacomult := paco5_2_0_mult gf_0 gf_1; - pacofold := paco5_2_0_fold gf_0 gf_1; - pacounfold := paco5_2_0_unfold gf_0 gf_1 }. - -Instance paco5_2_1_inst T0 T1 T2 T3 T4 (gf_0 gf_1 : rel5 T0 T1 T2 T3 T4->_) r_0 r_1 x0 x1 x2 x3 x4 : paco_class (paco5_2_1 gf_0 gf_1 r_0 r_1 x0 x1 x2 x3 x4) := -{ pacoacc := paco5_2_1_acc gf_0 gf_1; - pacomult := paco5_2_1_mult gf_0 gf_1; - pacofold := paco5_2_1_fold gf_0 gf_1; - pacounfold := paco5_2_1_unfold gf_0 gf_1 }. - Global Opaque paco5_3_0. Global Opaque paco5_3_1. Global Opaque paco5_3_2. @@ -738,40 +775,3 @@ Hint Resolve paco5_3_1_fold. Hint Resolve paco5_3_2_fold. Hint Unfold monotone5_3. -Arguments paco5_3_0_acc [ T0 T1 T2 T3 T4 ]. -Arguments paco5_3_1_acc [ T0 T1 T2 T3 T4 ]. -Arguments paco5_3_2_acc [ T0 T1 T2 T3 T4 ]. -Arguments paco5_3_0_mon [ T0 T1 T2 T3 T4 ]. -Arguments paco5_3_1_mon [ T0 T1 T2 T3 T4 ]. -Arguments paco5_3_2_mon [ T0 T1 T2 T3 T4 ]. -Arguments paco5_3_0_mult_strong [ T0 T1 T2 T3 T4 ]. -Arguments paco5_3_1_mult_strong [ T0 T1 T2 T3 T4 ]. -Arguments paco5_3_2_mult_strong [ T0 T1 T2 T3 T4 ]. -Arguments paco5_3_0_mult [ T0 T1 T2 T3 T4 ]. -Arguments paco5_3_1_mult [ T0 T1 T2 T3 T4 ]. -Arguments paco5_3_2_mult [ T0 T1 T2 T3 T4 ]. -Arguments paco5_3_0_fold [ T0 T1 T2 T3 T4 ]. -Arguments paco5_3_1_fold [ T0 T1 T2 T3 T4 ]. -Arguments paco5_3_2_fold [ T0 T1 T2 T3 T4 ]. -Arguments paco5_3_0_unfold [ T0 T1 T2 T3 T4 ]. -Arguments paco5_3_1_unfold [ T0 T1 T2 T3 T4 ]. -Arguments paco5_3_2_unfold [ T0 T1 T2 T3 T4 ]. - -Instance paco5_3_0_inst T0 T1 T2 T3 T4 (gf_0 gf_1 gf_2 : rel5 T0 T1 T2 T3 T4->_) r_0 r_1 r_2 x0 x1 x2 x3 x4 : paco_class (paco5_3_0 gf_0 gf_1 gf_2 r_0 r_1 r_2 x0 x1 x2 x3 x4) := -{ pacoacc := paco5_3_0_acc gf_0 gf_1 gf_2; - pacomult := paco5_3_0_mult gf_0 gf_1 gf_2; - pacofold := paco5_3_0_fold gf_0 gf_1 gf_2; - pacounfold := paco5_3_0_unfold gf_0 gf_1 gf_2 }. - -Instance paco5_3_1_inst T0 T1 T2 T3 T4 (gf_0 gf_1 gf_2 : rel5 T0 T1 T2 T3 T4->_) r_0 r_1 r_2 x0 x1 x2 x3 x4 : paco_class (paco5_3_1 gf_0 gf_1 gf_2 r_0 r_1 r_2 x0 x1 x2 x3 x4) := -{ pacoacc := paco5_3_1_acc gf_0 gf_1 gf_2; - pacomult := paco5_3_1_mult gf_0 gf_1 gf_2; - pacofold := paco5_3_1_fold gf_0 gf_1 gf_2; - pacounfold := paco5_3_1_unfold gf_0 gf_1 gf_2 }. - -Instance paco5_3_2_inst T0 T1 T2 T3 T4 (gf_0 gf_1 gf_2 : rel5 T0 T1 T2 T3 T4->_) r_0 r_1 r_2 x0 x1 x2 x3 x4 : paco_class (paco5_3_2 gf_0 gf_1 gf_2 r_0 r_1 r_2 x0 x1 x2 x3 x4) := -{ pacoacc := paco5_3_2_acc gf_0 gf_1 gf_2; - pacomult := paco5_3_2_mult gf_0 gf_1 gf_2; - pacofold := paco5_3_2_fold gf_0 gf_1 gf_2; - pacounfold := paco5_3_2_unfold gf_0 gf_1 gf_2 }. - diff --git a/src/paco6.v b/src/paco6.v index 1968db1..4b7dad6 100644 --- a/src/paco6.v +++ b/src/paco6.v @@ -243,6 +243,19 @@ Qed. End Arg6_1. +Arguments paco6_acc : clear implicits. +Arguments paco6_mon : clear implicits. +Arguments paco6_mult_strong : clear implicits. +Arguments paco6_mult : clear implicits. +Arguments paco6_fold : clear implicits. +Arguments paco6_unfold : clear implicits. + +Global Instance paco6_inst (gf : rel6 T0 T1 T2 T3 T4 T5->_) r x0 x1 x2 x3 x4 x5 : paco_class (paco6 gf r x0 x1 x2 x3 x4 x5) := +{ pacoacc := paco6_acc gf; + pacomult := paco6_mult gf; + pacofold := paco6_fold gf; + pacounfold := paco6_unfold gf }. + (** 2 Mutual Coinduction *) Section Arg6_2. @@ -420,6 +433,31 @@ Qed. End Arg6_2. +Arguments paco6_2_0_acc : clear implicits. +Arguments paco6_2_1_acc : clear implicits. +Arguments paco6_2_0_mon : clear implicits. +Arguments paco6_2_1_mon : clear implicits. +Arguments paco6_2_0_mult_strong : clear implicits. +Arguments paco6_2_1_mult_strong : clear implicits. +Arguments paco6_2_0_mult : clear implicits. +Arguments paco6_2_1_mult : clear implicits. +Arguments paco6_2_0_fold : clear implicits. +Arguments paco6_2_1_fold : clear implicits. +Arguments paco6_2_0_unfold : clear implicits. +Arguments paco6_2_1_unfold : clear implicits. + +Global Instance paco6_2_0_inst (gf_0 gf_1 : rel6 T0 T1 T2 T3 T4 T5->_) r_0 r_1 x0 x1 x2 x3 x4 x5 : paco_class (paco6_2_0 gf_0 gf_1 r_0 r_1 x0 x1 x2 x3 x4 x5) := +{ pacoacc := paco6_2_0_acc gf_0 gf_1; + pacomult := paco6_2_0_mult gf_0 gf_1; + pacofold := paco6_2_0_fold gf_0 gf_1; + pacounfold := paco6_2_0_unfold gf_0 gf_1 }. + +Global Instance paco6_2_1_inst (gf_0 gf_1 : rel6 T0 T1 T2 T3 T4 T5->_) r_0 r_1 x0 x1 x2 x3 x4 x5 : paco_class (paco6_2_1 gf_0 gf_1 r_0 r_1 x0 x1 x2 x3 x4 x5) := +{ pacoacc := paco6_2_1_acc gf_0 gf_1; + pacomult := paco6_2_1_mult gf_0 gf_1; + pacofold := paco6_2_1_fold gf_0 gf_1; + pacounfold := paco6_2_1_unfold gf_0 gf_1 }. + (** 3 Mutual Coinduction *) Section Arg6_3. @@ -673,6 +711,43 @@ Qed. End Arg6_3. +Arguments paco6_3_0_acc : clear implicits. +Arguments paco6_3_1_acc : clear implicits. +Arguments paco6_3_2_acc : clear implicits. +Arguments paco6_3_0_mon : clear implicits. +Arguments paco6_3_1_mon : clear implicits. +Arguments paco6_3_2_mon : clear implicits. +Arguments paco6_3_0_mult_strong : clear implicits. +Arguments paco6_3_1_mult_strong : clear implicits. +Arguments paco6_3_2_mult_strong : clear implicits. +Arguments paco6_3_0_mult : clear implicits. +Arguments paco6_3_1_mult : clear implicits. +Arguments paco6_3_2_mult : clear implicits. +Arguments paco6_3_0_fold : clear implicits. +Arguments paco6_3_1_fold : clear implicits. +Arguments paco6_3_2_fold : clear implicits. +Arguments paco6_3_0_unfold : clear implicits. +Arguments paco6_3_1_unfold : clear implicits. +Arguments paco6_3_2_unfold : clear implicits. + +Global Instance paco6_3_0_inst (gf_0 gf_1 gf_2 : rel6 T0 T1 T2 T3 T4 T5->_) r_0 r_1 r_2 x0 x1 x2 x3 x4 x5 : paco_class (paco6_3_0 gf_0 gf_1 gf_2 r_0 r_1 r_2 x0 x1 x2 x3 x4 x5) := +{ pacoacc := paco6_3_0_acc gf_0 gf_1 gf_2; + pacomult := paco6_3_0_mult gf_0 gf_1 gf_2; + pacofold := paco6_3_0_fold gf_0 gf_1 gf_2; + pacounfold := paco6_3_0_unfold gf_0 gf_1 gf_2 }. + +Global Instance paco6_3_1_inst (gf_0 gf_1 gf_2 : rel6 T0 T1 T2 T3 T4 T5->_) r_0 r_1 r_2 x0 x1 x2 x3 x4 x5 : paco_class (paco6_3_1 gf_0 gf_1 gf_2 r_0 r_1 r_2 x0 x1 x2 x3 x4 x5) := +{ pacoacc := paco6_3_1_acc gf_0 gf_1 gf_2; + pacomult := paco6_3_1_mult gf_0 gf_1 gf_2; + pacofold := paco6_3_1_fold gf_0 gf_1 gf_2; + pacounfold := paco6_3_1_unfold gf_0 gf_1 gf_2 }. + +Global Instance paco6_3_2_inst (gf_0 gf_1 gf_2 : rel6 T0 T1 T2 T3 T4 T5->_) r_0 r_1 r_2 x0 x1 x2 x3 x4 x5 : paco_class (paco6_3_2 gf_0 gf_1 gf_2 r_0 r_1 r_2 x0 x1 x2 x3 x4 x5) := +{ pacoacc := paco6_3_2_acc gf_0 gf_1 gf_2; + pacomult := paco6_3_2_mult gf_0 gf_1 gf_2; + pacofold := paco6_3_2_fold gf_0 gf_1 gf_2; + pacounfold := paco6_3_2_unfold gf_0 gf_1 gf_2 }. + End PACO6. Global Opaque paco6. @@ -681,19 +756,6 @@ Hint Unfold upaco6. Hint Resolve paco6_fold. Hint Unfold monotone6. -Arguments paco6_acc [ T0 T1 T2 T3 T4 T5 ]. -Arguments paco6_mon [ T0 T1 T2 T3 T4 T5 ]. -Arguments paco6_mult_strong [ T0 T1 T2 T3 T4 T5 ]. -Arguments paco6_mult [ T0 T1 T2 T3 T4 T5 ]. -Arguments paco6_fold [ T0 T1 T2 T3 T4 T5 ]. -Arguments paco6_unfold [ T0 T1 T2 T3 T4 T5 ]. - -Instance paco6_inst T0 T1 T2 T3 T4 T5 (gf : rel6 T0 T1 T2 T3 T4 T5->_) r x0 x1 x2 x3 x4 x5 : paco_class (paco6 gf r x0 x1 x2 x3 x4 x5) := -{ pacoacc := paco6_acc gf; - pacomult := paco6_mult gf; - pacofold := paco6_fold gf; - pacounfold := paco6_unfold gf }. - Global Opaque paco6_2_0. Global Opaque paco6_2_1. @@ -703,31 +765,6 @@ Hint Resolve paco6_2_0_fold. Hint Resolve paco6_2_1_fold. Hint Unfold monotone6_2. -Arguments paco6_2_0_acc [ T0 T1 T2 T3 T4 T5 ]. -Arguments paco6_2_1_acc [ T0 T1 T2 T3 T4 T5 ]. -Arguments paco6_2_0_mon [ T0 T1 T2 T3 T4 T5 ]. -Arguments paco6_2_1_mon [ T0 T1 T2 T3 T4 T5 ]. -Arguments paco6_2_0_mult_strong [ T0 T1 T2 T3 T4 T5 ]. -Arguments paco6_2_1_mult_strong [ T0 T1 T2 T3 T4 T5 ]. -Arguments paco6_2_0_mult [ T0 T1 T2 T3 T4 T5 ]. -Arguments paco6_2_1_mult [ T0 T1 T2 T3 T4 T5 ]. -Arguments paco6_2_0_fold [ T0 T1 T2 T3 T4 T5 ]. -Arguments paco6_2_1_fold [ T0 T1 T2 T3 T4 T5 ]. -Arguments paco6_2_0_unfold [ T0 T1 T2 T3 T4 T5 ]. -Arguments paco6_2_1_unfold [ T0 T1 T2 T3 T4 T5 ]. - -Instance paco6_2_0_inst T0 T1 T2 T3 T4 T5 (gf_0 gf_1 : rel6 T0 T1 T2 T3 T4 T5->_) r_0 r_1 x0 x1 x2 x3 x4 x5 : paco_class (paco6_2_0 gf_0 gf_1 r_0 r_1 x0 x1 x2 x3 x4 x5) := -{ pacoacc := paco6_2_0_acc gf_0 gf_1; - pacomult := paco6_2_0_mult gf_0 gf_1; - pacofold := paco6_2_0_fold gf_0 gf_1; - pacounfold := paco6_2_0_unfold gf_0 gf_1 }. - -Instance paco6_2_1_inst T0 T1 T2 T3 T4 T5 (gf_0 gf_1 : rel6 T0 T1 T2 T3 T4 T5->_) r_0 r_1 x0 x1 x2 x3 x4 x5 : paco_class (paco6_2_1 gf_0 gf_1 r_0 r_1 x0 x1 x2 x3 x4 x5) := -{ pacoacc := paco6_2_1_acc gf_0 gf_1; - pacomult := paco6_2_1_mult gf_0 gf_1; - pacofold := paco6_2_1_fold gf_0 gf_1; - pacounfold := paco6_2_1_unfold gf_0 gf_1 }. - Global Opaque paco6_3_0. Global Opaque paco6_3_1. Global Opaque paco6_3_2. @@ -740,40 +777,3 @@ Hint Resolve paco6_3_1_fold. Hint Resolve paco6_3_2_fold. Hint Unfold monotone6_3. -Arguments paco6_3_0_acc [ T0 T1 T2 T3 T4 T5 ]. -Arguments paco6_3_1_acc [ T0 T1 T2 T3 T4 T5 ]. -Arguments paco6_3_2_acc [ T0 T1 T2 T3 T4 T5 ]. -Arguments paco6_3_0_mon [ T0 T1 T2 T3 T4 T5 ]. -Arguments paco6_3_1_mon [ T0 T1 T2 T3 T4 T5 ]. -Arguments paco6_3_2_mon [ T0 T1 T2 T3 T4 T5 ]. -Arguments paco6_3_0_mult_strong [ T0 T1 T2 T3 T4 T5 ]. -Arguments paco6_3_1_mult_strong [ T0 T1 T2 T3 T4 T5 ]. -Arguments paco6_3_2_mult_strong [ T0 T1 T2 T3 T4 T5 ]. -Arguments paco6_3_0_mult [ T0 T1 T2 T3 T4 T5 ]. -Arguments paco6_3_1_mult [ T0 T1 T2 T3 T4 T5 ]. -Arguments paco6_3_2_mult [ T0 T1 T2 T3 T4 T5 ]. -Arguments paco6_3_0_fold [ T0 T1 T2 T3 T4 T5 ]. -Arguments paco6_3_1_fold [ T0 T1 T2 T3 T4 T5 ]. -Arguments paco6_3_2_fold [ T0 T1 T2 T3 T4 T5 ]. -Arguments paco6_3_0_unfold [ T0 T1 T2 T3 T4 T5 ]. -Arguments paco6_3_1_unfold [ T0 T1 T2 T3 T4 T5 ]. -Arguments paco6_3_2_unfold [ T0 T1 T2 T3 T4 T5 ]. - -Instance paco6_3_0_inst T0 T1 T2 T3 T4 T5 (gf_0 gf_1 gf_2 : rel6 T0 T1 T2 T3 T4 T5->_) r_0 r_1 r_2 x0 x1 x2 x3 x4 x5 : paco_class (paco6_3_0 gf_0 gf_1 gf_2 r_0 r_1 r_2 x0 x1 x2 x3 x4 x5) := -{ pacoacc := paco6_3_0_acc gf_0 gf_1 gf_2; - pacomult := paco6_3_0_mult gf_0 gf_1 gf_2; - pacofold := paco6_3_0_fold gf_0 gf_1 gf_2; - pacounfold := paco6_3_0_unfold gf_0 gf_1 gf_2 }. - -Instance paco6_3_1_inst T0 T1 T2 T3 T4 T5 (gf_0 gf_1 gf_2 : rel6 T0 T1 T2 T3 T4 T5->_) r_0 r_1 r_2 x0 x1 x2 x3 x4 x5 : paco_class (paco6_3_1 gf_0 gf_1 gf_2 r_0 r_1 r_2 x0 x1 x2 x3 x4 x5) := -{ pacoacc := paco6_3_1_acc gf_0 gf_1 gf_2; - pacomult := paco6_3_1_mult gf_0 gf_1 gf_2; - pacofold := paco6_3_1_fold gf_0 gf_1 gf_2; - pacounfold := paco6_3_1_unfold gf_0 gf_1 gf_2 }. - -Instance paco6_3_2_inst T0 T1 T2 T3 T4 T5 (gf_0 gf_1 gf_2 : rel6 T0 T1 T2 T3 T4 T5->_) r_0 r_1 r_2 x0 x1 x2 x3 x4 x5 : paco_class (paco6_3_2 gf_0 gf_1 gf_2 r_0 r_1 r_2 x0 x1 x2 x3 x4 x5) := -{ pacoacc := paco6_3_2_acc gf_0 gf_1 gf_2; - pacomult := paco6_3_2_mult gf_0 gf_1 gf_2; - pacofold := paco6_3_2_fold gf_0 gf_1 gf_2; - pacounfold := paco6_3_2_unfold gf_0 gf_1 gf_2 }. - diff --git a/src/paco7.v b/src/paco7.v index 4f8d140..29a8fe5 100644 --- a/src/paco7.v +++ b/src/paco7.v @@ -245,6 +245,19 @@ Qed. End Arg7_1. +Arguments paco7_acc : clear implicits. +Arguments paco7_mon : clear implicits. +Arguments paco7_mult_strong : clear implicits. +Arguments paco7_mult : clear implicits. +Arguments paco7_fold : clear implicits. +Arguments paco7_unfold : clear implicits. + +Global Instance paco7_inst (gf : rel7 T0 T1 T2 T3 T4 T5 T6->_) r x0 x1 x2 x3 x4 x5 x6 : paco_class (paco7 gf r x0 x1 x2 x3 x4 x5 x6) := +{ pacoacc := paco7_acc gf; + pacomult := paco7_mult gf; + pacofold := paco7_fold gf; + pacounfold := paco7_unfold gf }. + (** 2 Mutual Coinduction *) Section Arg7_2. @@ -422,6 +435,31 @@ Qed. End Arg7_2. +Arguments paco7_2_0_acc : clear implicits. +Arguments paco7_2_1_acc : clear implicits. +Arguments paco7_2_0_mon : clear implicits. +Arguments paco7_2_1_mon : clear implicits. +Arguments paco7_2_0_mult_strong : clear implicits. +Arguments paco7_2_1_mult_strong : clear implicits. +Arguments paco7_2_0_mult : clear implicits. +Arguments paco7_2_1_mult : clear implicits. +Arguments paco7_2_0_fold : clear implicits. +Arguments paco7_2_1_fold : clear implicits. +Arguments paco7_2_0_unfold : clear implicits. +Arguments paco7_2_1_unfold : clear implicits. + +Global Instance paco7_2_0_inst (gf_0 gf_1 : rel7 T0 T1 T2 T3 T4 T5 T6->_) r_0 r_1 x0 x1 x2 x3 x4 x5 x6 : paco_class (paco7_2_0 gf_0 gf_1 r_0 r_1 x0 x1 x2 x3 x4 x5 x6) := +{ pacoacc := paco7_2_0_acc gf_0 gf_1; + pacomult := paco7_2_0_mult gf_0 gf_1; + pacofold := paco7_2_0_fold gf_0 gf_1; + pacounfold := paco7_2_0_unfold gf_0 gf_1 }. + +Global Instance paco7_2_1_inst (gf_0 gf_1 : rel7 T0 T1 T2 T3 T4 T5 T6->_) r_0 r_1 x0 x1 x2 x3 x4 x5 x6 : paco_class (paco7_2_1 gf_0 gf_1 r_0 r_1 x0 x1 x2 x3 x4 x5 x6) := +{ pacoacc := paco7_2_1_acc gf_0 gf_1; + pacomult := paco7_2_1_mult gf_0 gf_1; + pacofold := paco7_2_1_fold gf_0 gf_1; + pacounfold := paco7_2_1_unfold gf_0 gf_1 }. + (** 3 Mutual Coinduction *) Section Arg7_3. @@ -675,6 +713,43 @@ Qed. End Arg7_3. +Arguments paco7_3_0_acc : clear implicits. +Arguments paco7_3_1_acc : clear implicits. +Arguments paco7_3_2_acc : clear implicits. +Arguments paco7_3_0_mon : clear implicits. +Arguments paco7_3_1_mon : clear implicits. +Arguments paco7_3_2_mon : clear implicits. +Arguments paco7_3_0_mult_strong : clear implicits. +Arguments paco7_3_1_mult_strong : clear implicits. +Arguments paco7_3_2_mult_strong : clear implicits. +Arguments paco7_3_0_mult : clear implicits. +Arguments paco7_3_1_mult : clear implicits. +Arguments paco7_3_2_mult : clear implicits. +Arguments paco7_3_0_fold : clear implicits. +Arguments paco7_3_1_fold : clear implicits. +Arguments paco7_3_2_fold : clear implicits. +Arguments paco7_3_0_unfold : clear implicits. +Arguments paco7_3_1_unfold : clear implicits. +Arguments paco7_3_2_unfold : clear implicits. + +Global Instance paco7_3_0_inst (gf_0 gf_1 gf_2 : rel7 T0 T1 T2 T3 T4 T5 T6->_) r_0 r_1 r_2 x0 x1 x2 x3 x4 x5 x6 : paco_class (paco7_3_0 gf_0 gf_1 gf_2 r_0 r_1 r_2 x0 x1 x2 x3 x4 x5 x6) := +{ pacoacc := paco7_3_0_acc gf_0 gf_1 gf_2; + pacomult := paco7_3_0_mult gf_0 gf_1 gf_2; + pacofold := paco7_3_0_fold gf_0 gf_1 gf_2; + pacounfold := paco7_3_0_unfold gf_0 gf_1 gf_2 }. + +Global Instance paco7_3_1_inst (gf_0 gf_1 gf_2 : rel7 T0 T1 T2 T3 T4 T5 T6->_) r_0 r_1 r_2 x0 x1 x2 x3 x4 x5 x6 : paco_class (paco7_3_1 gf_0 gf_1 gf_2 r_0 r_1 r_2 x0 x1 x2 x3 x4 x5 x6) := +{ pacoacc := paco7_3_1_acc gf_0 gf_1 gf_2; + pacomult := paco7_3_1_mult gf_0 gf_1 gf_2; + pacofold := paco7_3_1_fold gf_0 gf_1 gf_2; + pacounfold := paco7_3_1_unfold gf_0 gf_1 gf_2 }. + +Global Instance paco7_3_2_inst (gf_0 gf_1 gf_2 : rel7 T0 T1 T2 T3 T4 T5 T6->_) r_0 r_1 r_2 x0 x1 x2 x3 x4 x5 x6 : paco_class (paco7_3_2 gf_0 gf_1 gf_2 r_0 r_1 r_2 x0 x1 x2 x3 x4 x5 x6) := +{ pacoacc := paco7_3_2_acc gf_0 gf_1 gf_2; + pacomult := paco7_3_2_mult gf_0 gf_1 gf_2; + pacofold := paco7_3_2_fold gf_0 gf_1 gf_2; + pacounfold := paco7_3_2_unfold gf_0 gf_1 gf_2 }. + End PACO7. Global Opaque paco7. @@ -683,19 +758,6 @@ Hint Unfold upaco7. Hint Resolve paco7_fold. Hint Unfold monotone7. -Arguments paco7_acc [ T0 T1 T2 T3 T4 T5 T6 ]. -Arguments paco7_mon [ T0 T1 T2 T3 T4 T5 T6 ]. -Arguments paco7_mult_strong [ T0 T1 T2 T3 T4 T5 T6 ]. -Arguments paco7_mult [ T0 T1 T2 T3 T4 T5 T6 ]. -Arguments paco7_fold [ T0 T1 T2 T3 T4 T5 T6 ]. -Arguments paco7_unfold [ T0 T1 T2 T3 T4 T5 T6 ]. - -Instance paco7_inst T0 T1 T2 T3 T4 T5 T6 (gf : rel7 T0 T1 T2 T3 T4 T5 T6->_) r x0 x1 x2 x3 x4 x5 x6 : paco_class (paco7 gf r x0 x1 x2 x3 x4 x5 x6) := -{ pacoacc := paco7_acc gf; - pacomult := paco7_mult gf; - pacofold := paco7_fold gf; - pacounfold := paco7_unfold gf }. - Global Opaque paco7_2_0. Global Opaque paco7_2_1. @@ -705,31 +767,6 @@ Hint Resolve paco7_2_0_fold. Hint Resolve paco7_2_1_fold. Hint Unfold monotone7_2. -Arguments paco7_2_0_acc [ T0 T1 T2 T3 T4 T5 T6 ]. -Arguments paco7_2_1_acc [ T0 T1 T2 T3 T4 T5 T6 ]. -Arguments paco7_2_0_mon [ T0 T1 T2 T3 T4 T5 T6 ]. -Arguments paco7_2_1_mon [ T0 T1 T2 T3 T4 T5 T6 ]. -Arguments paco7_2_0_mult_strong [ T0 T1 T2 T3 T4 T5 T6 ]. -Arguments paco7_2_1_mult_strong [ T0 T1 T2 T3 T4 T5 T6 ]. -Arguments paco7_2_0_mult [ T0 T1 T2 T3 T4 T5 T6 ]. -Arguments paco7_2_1_mult [ T0 T1 T2 T3 T4 T5 T6 ]. -Arguments paco7_2_0_fold [ T0 T1 T2 T3 T4 T5 T6 ]. -Arguments paco7_2_1_fold [ T0 T1 T2 T3 T4 T5 T6 ]. -Arguments paco7_2_0_unfold [ T0 T1 T2 T3 T4 T5 T6 ]. -Arguments paco7_2_1_unfold [ T0 T1 T2 T3 T4 T5 T6 ]. - -Instance paco7_2_0_inst T0 T1 T2 T3 T4 T5 T6 (gf_0 gf_1 : rel7 T0 T1 T2 T3 T4 T5 T6->_) r_0 r_1 x0 x1 x2 x3 x4 x5 x6 : paco_class (paco7_2_0 gf_0 gf_1 r_0 r_1 x0 x1 x2 x3 x4 x5 x6) := -{ pacoacc := paco7_2_0_acc gf_0 gf_1; - pacomult := paco7_2_0_mult gf_0 gf_1; - pacofold := paco7_2_0_fold gf_0 gf_1; - pacounfold := paco7_2_0_unfold gf_0 gf_1 }. - -Instance paco7_2_1_inst T0 T1 T2 T3 T4 T5 T6 (gf_0 gf_1 : rel7 T0 T1 T2 T3 T4 T5 T6->_) r_0 r_1 x0 x1 x2 x3 x4 x5 x6 : paco_class (paco7_2_1 gf_0 gf_1 r_0 r_1 x0 x1 x2 x3 x4 x5 x6) := -{ pacoacc := paco7_2_1_acc gf_0 gf_1; - pacomult := paco7_2_1_mult gf_0 gf_1; - pacofold := paco7_2_1_fold gf_0 gf_1; - pacounfold := paco7_2_1_unfold gf_0 gf_1 }. - Global Opaque paco7_3_0. Global Opaque paco7_3_1. Global Opaque paco7_3_2. @@ -742,40 +779,3 @@ Hint Resolve paco7_3_1_fold. Hint Resolve paco7_3_2_fold. Hint Unfold monotone7_3. -Arguments paco7_3_0_acc [ T0 T1 T2 T3 T4 T5 T6 ]. -Arguments paco7_3_1_acc [ T0 T1 T2 T3 T4 T5 T6 ]. -Arguments paco7_3_2_acc [ T0 T1 T2 T3 T4 T5 T6 ]. -Arguments paco7_3_0_mon [ T0 T1 T2 T3 T4 T5 T6 ]. -Arguments paco7_3_1_mon [ T0 T1 T2 T3 T4 T5 T6 ]. -Arguments paco7_3_2_mon [ T0 T1 T2 T3 T4 T5 T6 ]. -Arguments paco7_3_0_mult_strong [ T0 T1 T2 T3 T4 T5 T6 ]. -Arguments paco7_3_1_mult_strong [ T0 T1 T2 T3 T4 T5 T6 ]. -Arguments paco7_3_2_mult_strong [ T0 T1 T2 T3 T4 T5 T6 ]. -Arguments paco7_3_0_mult [ T0 T1 T2 T3 T4 T5 T6 ]. -Arguments paco7_3_1_mult [ T0 T1 T2 T3 T4 T5 T6 ]. -Arguments paco7_3_2_mult [ T0 T1 T2 T3 T4 T5 T6 ]. -Arguments paco7_3_0_fold [ T0 T1 T2 T3 T4 T5 T6 ]. -Arguments paco7_3_1_fold [ T0 T1 T2 T3 T4 T5 T6 ]. -Arguments paco7_3_2_fold [ T0 T1 T2 T3 T4 T5 T6 ]. -Arguments paco7_3_0_unfold [ T0 T1 T2 T3 T4 T5 T6 ]. -Arguments paco7_3_1_unfold [ T0 T1 T2 T3 T4 T5 T6 ]. -Arguments paco7_3_2_unfold [ T0 T1 T2 T3 T4 T5 T6 ]. - -Instance paco7_3_0_inst T0 T1 T2 T3 T4 T5 T6 (gf_0 gf_1 gf_2 : rel7 T0 T1 T2 T3 T4 T5 T6->_) r_0 r_1 r_2 x0 x1 x2 x3 x4 x5 x6 : paco_class (paco7_3_0 gf_0 gf_1 gf_2 r_0 r_1 r_2 x0 x1 x2 x3 x4 x5 x6) := -{ pacoacc := paco7_3_0_acc gf_0 gf_1 gf_2; - pacomult := paco7_3_0_mult gf_0 gf_1 gf_2; - pacofold := paco7_3_0_fold gf_0 gf_1 gf_2; - pacounfold := paco7_3_0_unfold gf_0 gf_1 gf_2 }. - -Instance paco7_3_1_inst T0 T1 T2 T3 T4 T5 T6 (gf_0 gf_1 gf_2 : rel7 T0 T1 T2 T3 T4 T5 T6->_) r_0 r_1 r_2 x0 x1 x2 x3 x4 x5 x6 : paco_class (paco7_3_1 gf_0 gf_1 gf_2 r_0 r_1 r_2 x0 x1 x2 x3 x4 x5 x6) := -{ pacoacc := paco7_3_1_acc gf_0 gf_1 gf_2; - pacomult := paco7_3_1_mult gf_0 gf_1 gf_2; - pacofold := paco7_3_1_fold gf_0 gf_1 gf_2; - pacounfold := paco7_3_1_unfold gf_0 gf_1 gf_2 }. - -Instance paco7_3_2_inst T0 T1 T2 T3 T4 T5 T6 (gf_0 gf_1 gf_2 : rel7 T0 T1 T2 T3 T4 T5 T6->_) r_0 r_1 r_2 x0 x1 x2 x3 x4 x5 x6 : paco_class (paco7_3_2 gf_0 gf_1 gf_2 r_0 r_1 r_2 x0 x1 x2 x3 x4 x5 x6) := -{ pacoacc := paco7_3_2_acc gf_0 gf_1 gf_2; - pacomult := paco7_3_2_mult gf_0 gf_1 gf_2; - pacofold := paco7_3_2_fold gf_0 gf_1 gf_2; - pacounfold := paco7_3_2_unfold gf_0 gf_1 gf_2 }. - diff --git a/src/paco8.v b/src/paco8.v index da21969..2e90edf 100644 --- a/src/paco8.v +++ b/src/paco8.v @@ -247,6 +247,19 @@ Qed. End Arg8_1. +Arguments paco8_acc : clear implicits. +Arguments paco8_mon : clear implicits. +Arguments paco8_mult_strong : clear implicits. +Arguments paco8_mult : clear implicits. +Arguments paco8_fold : clear implicits. +Arguments paco8_unfold : clear implicits. + +Global Instance paco8_inst (gf : rel8 T0 T1 T2 T3 T4 T5 T6 T7->_) r x0 x1 x2 x3 x4 x5 x6 x7 : paco_class (paco8 gf r x0 x1 x2 x3 x4 x5 x6 x7) := +{ pacoacc := paco8_acc gf; + pacomult := paco8_mult gf; + pacofold := paco8_fold gf; + pacounfold := paco8_unfold gf }. + (** 2 Mutual Coinduction *) Section Arg8_2. @@ -424,6 +437,31 @@ Qed. End Arg8_2. +Arguments paco8_2_0_acc : clear implicits. +Arguments paco8_2_1_acc : clear implicits. +Arguments paco8_2_0_mon : clear implicits. +Arguments paco8_2_1_mon : clear implicits. +Arguments paco8_2_0_mult_strong : clear implicits. +Arguments paco8_2_1_mult_strong : clear implicits. +Arguments paco8_2_0_mult : clear implicits. +Arguments paco8_2_1_mult : clear implicits. +Arguments paco8_2_0_fold : clear implicits. +Arguments paco8_2_1_fold : clear implicits. +Arguments paco8_2_0_unfold : clear implicits. +Arguments paco8_2_1_unfold : clear implicits. + +Global Instance paco8_2_0_inst (gf_0 gf_1 : rel8 T0 T1 T2 T3 T4 T5 T6 T7->_) r_0 r_1 x0 x1 x2 x3 x4 x5 x6 x7 : paco_class (paco8_2_0 gf_0 gf_1 r_0 r_1 x0 x1 x2 x3 x4 x5 x6 x7) := +{ pacoacc := paco8_2_0_acc gf_0 gf_1; + pacomult := paco8_2_0_mult gf_0 gf_1; + pacofold := paco8_2_0_fold gf_0 gf_1; + pacounfold := paco8_2_0_unfold gf_0 gf_1 }. + +Global Instance paco8_2_1_inst (gf_0 gf_1 : rel8 T0 T1 T2 T3 T4 T5 T6 T7->_) r_0 r_1 x0 x1 x2 x3 x4 x5 x6 x7 : paco_class (paco8_2_1 gf_0 gf_1 r_0 r_1 x0 x1 x2 x3 x4 x5 x6 x7) := +{ pacoacc := paco8_2_1_acc gf_0 gf_1; + pacomult := paco8_2_1_mult gf_0 gf_1; + pacofold := paco8_2_1_fold gf_0 gf_1; + pacounfold := paco8_2_1_unfold gf_0 gf_1 }. + (** 3 Mutual Coinduction *) Section Arg8_3. @@ -677,6 +715,43 @@ Qed. End Arg8_3. +Arguments paco8_3_0_acc : clear implicits. +Arguments paco8_3_1_acc : clear implicits. +Arguments paco8_3_2_acc : clear implicits. +Arguments paco8_3_0_mon : clear implicits. +Arguments paco8_3_1_mon : clear implicits. +Arguments paco8_3_2_mon : clear implicits. +Arguments paco8_3_0_mult_strong : clear implicits. +Arguments paco8_3_1_mult_strong : clear implicits. +Arguments paco8_3_2_mult_strong : clear implicits. +Arguments paco8_3_0_mult : clear implicits. +Arguments paco8_3_1_mult : clear implicits. +Arguments paco8_3_2_mult : clear implicits. +Arguments paco8_3_0_fold : clear implicits. +Arguments paco8_3_1_fold : clear implicits. +Arguments paco8_3_2_fold : clear implicits. +Arguments paco8_3_0_unfold : clear implicits. +Arguments paco8_3_1_unfold : clear implicits. +Arguments paco8_3_2_unfold : clear implicits. + +Global Instance paco8_3_0_inst (gf_0 gf_1 gf_2 : rel8 T0 T1 T2 T3 T4 T5 T6 T7->_) r_0 r_1 r_2 x0 x1 x2 x3 x4 x5 x6 x7 : paco_class (paco8_3_0 gf_0 gf_1 gf_2 r_0 r_1 r_2 x0 x1 x2 x3 x4 x5 x6 x7) := +{ pacoacc := paco8_3_0_acc gf_0 gf_1 gf_2; + pacomult := paco8_3_0_mult gf_0 gf_1 gf_2; + pacofold := paco8_3_0_fold gf_0 gf_1 gf_2; + pacounfold := paco8_3_0_unfold gf_0 gf_1 gf_2 }. + +Global Instance paco8_3_1_inst (gf_0 gf_1 gf_2 : rel8 T0 T1 T2 T3 T4 T5 T6 T7->_) r_0 r_1 r_2 x0 x1 x2 x3 x4 x5 x6 x7 : paco_class (paco8_3_1 gf_0 gf_1 gf_2 r_0 r_1 r_2 x0 x1 x2 x3 x4 x5 x6 x7) := +{ pacoacc := paco8_3_1_acc gf_0 gf_1 gf_2; + pacomult := paco8_3_1_mult gf_0 gf_1 gf_2; + pacofold := paco8_3_1_fold gf_0 gf_1 gf_2; + pacounfold := paco8_3_1_unfold gf_0 gf_1 gf_2 }. + +Global Instance paco8_3_2_inst (gf_0 gf_1 gf_2 : rel8 T0 T1 T2 T3 T4 T5 T6 T7->_) r_0 r_1 r_2 x0 x1 x2 x3 x4 x5 x6 x7 : paco_class (paco8_3_2 gf_0 gf_1 gf_2 r_0 r_1 r_2 x0 x1 x2 x3 x4 x5 x6 x7) := +{ pacoacc := paco8_3_2_acc gf_0 gf_1 gf_2; + pacomult := paco8_3_2_mult gf_0 gf_1 gf_2; + pacofold := paco8_3_2_fold gf_0 gf_1 gf_2; + pacounfold := paco8_3_2_unfold gf_0 gf_1 gf_2 }. + End PACO8. Global Opaque paco8. @@ -685,19 +760,6 @@ Hint Unfold upaco8. Hint Resolve paco8_fold. Hint Unfold monotone8. -Arguments paco8_acc [ T0 T1 T2 T3 T4 T5 T6 T7 ]. -Arguments paco8_mon [ T0 T1 T2 T3 T4 T5 T6 T7 ]. -Arguments paco8_mult_strong [ T0 T1 T2 T3 T4 T5 T6 T7 ]. -Arguments paco8_mult [ T0 T1 T2 T3 T4 T5 T6 T7 ]. -Arguments paco8_fold [ T0 T1 T2 T3 T4 T5 T6 T7 ]. -Arguments paco8_unfold [ T0 T1 T2 T3 T4 T5 T6 T7 ]. - -Instance paco8_inst T0 T1 T2 T3 T4 T5 T6 T7 (gf : rel8 T0 T1 T2 T3 T4 T5 T6 T7->_) r x0 x1 x2 x3 x4 x5 x6 x7 : paco_class (paco8 gf r x0 x1 x2 x3 x4 x5 x6 x7) := -{ pacoacc := paco8_acc gf; - pacomult := paco8_mult gf; - pacofold := paco8_fold gf; - pacounfold := paco8_unfold gf }. - Global Opaque paco8_2_0. Global Opaque paco8_2_1. @@ -707,31 +769,6 @@ Hint Resolve paco8_2_0_fold. Hint Resolve paco8_2_1_fold. Hint Unfold monotone8_2. -Arguments paco8_2_0_acc [ T0 T1 T2 T3 T4 T5 T6 T7 ]. -Arguments paco8_2_1_acc [ T0 T1 T2 T3 T4 T5 T6 T7 ]. -Arguments paco8_2_0_mon [ T0 T1 T2 T3 T4 T5 T6 T7 ]. -Arguments paco8_2_1_mon [ T0 T1 T2 T3 T4 T5 T6 T7 ]. -Arguments paco8_2_0_mult_strong [ T0 T1 T2 T3 T4 T5 T6 T7 ]. -Arguments paco8_2_1_mult_strong [ T0 T1 T2 T3 T4 T5 T6 T7 ]. -Arguments paco8_2_0_mult [ T0 T1 T2 T3 T4 T5 T6 T7 ]. -Arguments paco8_2_1_mult [ T0 T1 T2 T3 T4 T5 T6 T7 ]. -Arguments paco8_2_0_fold [ T0 T1 T2 T3 T4 T5 T6 T7 ]. -Arguments paco8_2_1_fold [ T0 T1 T2 T3 T4 T5 T6 T7 ]. -Arguments paco8_2_0_unfold [ T0 T1 T2 T3 T4 T5 T6 T7 ]. -Arguments paco8_2_1_unfold [ T0 T1 T2 T3 T4 T5 T6 T7 ]. - -Instance paco8_2_0_inst T0 T1 T2 T3 T4 T5 T6 T7 (gf_0 gf_1 : rel8 T0 T1 T2 T3 T4 T5 T6 T7->_) r_0 r_1 x0 x1 x2 x3 x4 x5 x6 x7 : paco_class (paco8_2_0 gf_0 gf_1 r_0 r_1 x0 x1 x2 x3 x4 x5 x6 x7) := -{ pacoacc := paco8_2_0_acc gf_0 gf_1; - pacomult := paco8_2_0_mult gf_0 gf_1; - pacofold := paco8_2_0_fold gf_0 gf_1; - pacounfold := paco8_2_0_unfold gf_0 gf_1 }. - -Instance paco8_2_1_inst T0 T1 T2 T3 T4 T5 T6 T7 (gf_0 gf_1 : rel8 T0 T1 T2 T3 T4 T5 T6 T7->_) r_0 r_1 x0 x1 x2 x3 x4 x5 x6 x7 : paco_class (paco8_2_1 gf_0 gf_1 r_0 r_1 x0 x1 x2 x3 x4 x5 x6 x7) := -{ pacoacc := paco8_2_1_acc gf_0 gf_1; - pacomult := paco8_2_1_mult gf_0 gf_1; - pacofold := paco8_2_1_fold gf_0 gf_1; - pacounfold := paco8_2_1_unfold gf_0 gf_1 }. - Global Opaque paco8_3_0. Global Opaque paco8_3_1. Global Opaque paco8_3_2. @@ -744,40 +781,3 @@ Hint Resolve paco8_3_1_fold. Hint Resolve paco8_3_2_fold. Hint Unfold monotone8_3. -Arguments paco8_3_0_acc [ T0 T1 T2 T3 T4 T5 T6 T7 ]. -Arguments paco8_3_1_acc [ T0 T1 T2 T3 T4 T5 T6 T7 ]. -Arguments paco8_3_2_acc [ T0 T1 T2 T3 T4 T5 T6 T7 ]. -Arguments paco8_3_0_mon [ T0 T1 T2 T3 T4 T5 T6 T7 ]. -Arguments paco8_3_1_mon [ T0 T1 T2 T3 T4 T5 T6 T7 ]. -Arguments paco8_3_2_mon [ T0 T1 T2 T3 T4 T5 T6 T7 ]. -Arguments paco8_3_0_mult_strong [ T0 T1 T2 T3 T4 T5 T6 T7 ]. -Arguments paco8_3_1_mult_strong [ T0 T1 T2 T3 T4 T5 T6 T7 ]. -Arguments paco8_3_2_mult_strong [ T0 T1 T2 T3 T4 T5 T6 T7 ]. -Arguments paco8_3_0_mult [ T0 T1 T2 T3 T4 T5 T6 T7 ]. -Arguments paco8_3_1_mult [ T0 T1 T2 T3 T4 T5 T6 T7 ]. -Arguments paco8_3_2_mult [ T0 T1 T2 T3 T4 T5 T6 T7 ]. -Arguments paco8_3_0_fold [ T0 T1 T2 T3 T4 T5 T6 T7 ]. -Arguments paco8_3_1_fold [ T0 T1 T2 T3 T4 T5 T6 T7 ]. -Arguments paco8_3_2_fold [ T0 T1 T2 T3 T4 T5 T6 T7 ]. -Arguments paco8_3_0_unfold [ T0 T1 T2 T3 T4 T5 T6 T7 ]. -Arguments paco8_3_1_unfold [ T0 T1 T2 T3 T4 T5 T6 T7 ]. -Arguments paco8_3_2_unfold [ T0 T1 T2 T3 T4 T5 T6 T7 ]. - -Instance paco8_3_0_inst T0 T1 T2 T3 T4 T5 T6 T7 (gf_0 gf_1 gf_2 : rel8 T0 T1 T2 T3 T4 T5 T6 T7->_) r_0 r_1 r_2 x0 x1 x2 x3 x4 x5 x6 x7 : paco_class (paco8_3_0 gf_0 gf_1 gf_2 r_0 r_1 r_2 x0 x1 x2 x3 x4 x5 x6 x7) := -{ pacoacc := paco8_3_0_acc gf_0 gf_1 gf_2; - pacomult := paco8_3_0_mult gf_0 gf_1 gf_2; - pacofold := paco8_3_0_fold gf_0 gf_1 gf_2; - pacounfold := paco8_3_0_unfold gf_0 gf_1 gf_2 }. - -Instance paco8_3_1_inst T0 T1 T2 T3 T4 T5 T6 T7 (gf_0 gf_1 gf_2 : rel8 T0 T1 T2 T3 T4 T5 T6 T7->_) r_0 r_1 r_2 x0 x1 x2 x3 x4 x5 x6 x7 : paco_class (paco8_3_1 gf_0 gf_1 gf_2 r_0 r_1 r_2 x0 x1 x2 x3 x4 x5 x6 x7) := -{ pacoacc := paco8_3_1_acc gf_0 gf_1 gf_2; - pacomult := paco8_3_1_mult gf_0 gf_1 gf_2; - pacofold := paco8_3_1_fold gf_0 gf_1 gf_2; - pacounfold := paco8_3_1_unfold gf_0 gf_1 gf_2 }. - -Instance paco8_3_2_inst T0 T1 T2 T3 T4 T5 T6 T7 (gf_0 gf_1 gf_2 : rel8 T0 T1 T2 T3 T4 T5 T6 T7->_) r_0 r_1 r_2 x0 x1 x2 x3 x4 x5 x6 x7 : paco_class (paco8_3_2 gf_0 gf_1 gf_2 r_0 r_1 r_2 x0 x1 x2 x3 x4 x5 x6 x7) := -{ pacoacc := paco8_3_2_acc gf_0 gf_1 gf_2; - pacomult := paco8_3_2_mult gf_0 gf_1 gf_2; - pacofold := paco8_3_2_fold gf_0 gf_1 gf_2; - pacounfold := paco8_3_2_unfold gf_0 gf_1 gf_2 }. - diff --git a/src/paco9.v b/src/paco9.v index e743de6..42509b9 100644 --- a/src/paco9.v +++ b/src/paco9.v @@ -249,6 +249,19 @@ Qed. End Arg9_1. +Arguments paco9_acc : clear implicits. +Arguments paco9_mon : clear implicits. +Arguments paco9_mult_strong : clear implicits. +Arguments paco9_mult : clear implicits. +Arguments paco9_fold : clear implicits. +Arguments paco9_unfold : clear implicits. + +Global Instance paco9_inst (gf : rel9 T0 T1 T2 T3 T4 T5 T6 T7 T8->_) r x0 x1 x2 x3 x4 x5 x6 x7 x8 : paco_class (paco9 gf r x0 x1 x2 x3 x4 x5 x6 x7 x8) := +{ pacoacc := paco9_acc gf; + pacomult := paco9_mult gf; + pacofold := paco9_fold gf; + pacounfold := paco9_unfold gf }. + (** 2 Mutual Coinduction *) Section Arg9_2. @@ -426,6 +439,31 @@ Qed. End Arg9_2. +Arguments paco9_2_0_acc : clear implicits. +Arguments paco9_2_1_acc : clear implicits. +Arguments paco9_2_0_mon : clear implicits. +Arguments paco9_2_1_mon : clear implicits. +Arguments paco9_2_0_mult_strong : clear implicits. +Arguments paco9_2_1_mult_strong : clear implicits. +Arguments paco9_2_0_mult : clear implicits. +Arguments paco9_2_1_mult : clear implicits. +Arguments paco9_2_0_fold : clear implicits. +Arguments paco9_2_1_fold : clear implicits. +Arguments paco9_2_0_unfold : clear implicits. +Arguments paco9_2_1_unfold : clear implicits. + +Global Instance paco9_2_0_inst (gf_0 gf_1 : rel9 T0 T1 T2 T3 T4 T5 T6 T7 T8->_) r_0 r_1 x0 x1 x2 x3 x4 x5 x6 x7 x8 : paco_class (paco9_2_0 gf_0 gf_1 r_0 r_1 x0 x1 x2 x3 x4 x5 x6 x7 x8) := +{ pacoacc := paco9_2_0_acc gf_0 gf_1; + pacomult := paco9_2_0_mult gf_0 gf_1; + pacofold := paco9_2_0_fold gf_0 gf_1; + pacounfold := paco9_2_0_unfold gf_0 gf_1 }. + +Global Instance paco9_2_1_inst (gf_0 gf_1 : rel9 T0 T1 T2 T3 T4 T5 T6 T7 T8->_) r_0 r_1 x0 x1 x2 x3 x4 x5 x6 x7 x8 : paco_class (paco9_2_1 gf_0 gf_1 r_0 r_1 x0 x1 x2 x3 x4 x5 x6 x7 x8) := +{ pacoacc := paco9_2_1_acc gf_0 gf_1; + pacomult := paco9_2_1_mult gf_0 gf_1; + pacofold := paco9_2_1_fold gf_0 gf_1; + pacounfold := paco9_2_1_unfold gf_0 gf_1 }. + (** 3 Mutual Coinduction *) Section Arg9_3. @@ -679,6 +717,43 @@ Qed. End Arg9_3. +Arguments paco9_3_0_acc : clear implicits. +Arguments paco9_3_1_acc : clear implicits. +Arguments paco9_3_2_acc : clear implicits. +Arguments paco9_3_0_mon : clear implicits. +Arguments paco9_3_1_mon : clear implicits. +Arguments paco9_3_2_mon : clear implicits. +Arguments paco9_3_0_mult_strong : clear implicits. +Arguments paco9_3_1_mult_strong : clear implicits. +Arguments paco9_3_2_mult_strong : clear implicits. +Arguments paco9_3_0_mult : clear implicits. +Arguments paco9_3_1_mult : clear implicits. +Arguments paco9_3_2_mult : clear implicits. +Arguments paco9_3_0_fold : clear implicits. +Arguments paco9_3_1_fold : clear implicits. +Arguments paco9_3_2_fold : clear implicits. +Arguments paco9_3_0_unfold : clear implicits. +Arguments paco9_3_1_unfold : clear implicits. +Arguments paco9_3_2_unfold : clear implicits. + +Global Instance paco9_3_0_inst (gf_0 gf_1 gf_2 : rel9 T0 T1 T2 T3 T4 T5 T6 T7 T8->_) r_0 r_1 r_2 x0 x1 x2 x3 x4 x5 x6 x7 x8 : paco_class (paco9_3_0 gf_0 gf_1 gf_2 r_0 r_1 r_2 x0 x1 x2 x3 x4 x5 x6 x7 x8) := +{ pacoacc := paco9_3_0_acc gf_0 gf_1 gf_2; + pacomult := paco9_3_0_mult gf_0 gf_1 gf_2; + pacofold := paco9_3_0_fold gf_0 gf_1 gf_2; + pacounfold := paco9_3_0_unfold gf_0 gf_1 gf_2 }. + +Global Instance paco9_3_1_inst (gf_0 gf_1 gf_2 : rel9 T0 T1 T2 T3 T4 T5 T6 T7 T8->_) r_0 r_1 r_2 x0 x1 x2 x3 x4 x5 x6 x7 x8 : paco_class (paco9_3_1 gf_0 gf_1 gf_2 r_0 r_1 r_2 x0 x1 x2 x3 x4 x5 x6 x7 x8) := +{ pacoacc := paco9_3_1_acc gf_0 gf_1 gf_2; + pacomult := paco9_3_1_mult gf_0 gf_1 gf_2; + pacofold := paco9_3_1_fold gf_0 gf_1 gf_2; + pacounfold := paco9_3_1_unfold gf_0 gf_1 gf_2 }. + +Global Instance paco9_3_2_inst (gf_0 gf_1 gf_2 : rel9 T0 T1 T2 T3 T4 T5 T6 T7 T8->_) r_0 r_1 r_2 x0 x1 x2 x3 x4 x5 x6 x7 x8 : paco_class (paco9_3_2 gf_0 gf_1 gf_2 r_0 r_1 r_2 x0 x1 x2 x3 x4 x5 x6 x7 x8) := +{ pacoacc := paco9_3_2_acc gf_0 gf_1 gf_2; + pacomult := paco9_3_2_mult gf_0 gf_1 gf_2; + pacofold := paco9_3_2_fold gf_0 gf_1 gf_2; + pacounfold := paco9_3_2_unfold gf_0 gf_1 gf_2 }. + End PACO9. Global Opaque paco9. @@ -687,19 +762,6 @@ Hint Unfold upaco9. Hint Resolve paco9_fold. Hint Unfold monotone9. -Arguments paco9_acc [ T0 T1 T2 T3 T4 T5 T6 T7 T8 ]. -Arguments paco9_mon [ T0 T1 T2 T3 T4 T5 T6 T7 T8 ]. -Arguments paco9_mult_strong [ T0 T1 T2 T3 T4 T5 T6 T7 T8 ]. -Arguments paco9_mult [ T0 T1 T2 T3 T4 T5 T6 T7 T8 ]. -Arguments paco9_fold [ T0 T1 T2 T3 T4 T5 T6 T7 T8 ]. -Arguments paco9_unfold [ T0 T1 T2 T3 T4 T5 T6 T7 T8 ]. - -Instance paco9_inst T0 T1 T2 T3 T4 T5 T6 T7 T8 (gf : rel9 T0 T1 T2 T3 T4 T5 T6 T7 T8->_) r x0 x1 x2 x3 x4 x5 x6 x7 x8 : paco_class (paco9 gf r x0 x1 x2 x3 x4 x5 x6 x7 x8) := -{ pacoacc := paco9_acc gf; - pacomult := paco9_mult gf; - pacofold := paco9_fold gf; - pacounfold := paco9_unfold gf }. - Global Opaque paco9_2_0. Global Opaque paco9_2_1. @@ -709,31 +771,6 @@ Hint Resolve paco9_2_0_fold. Hint Resolve paco9_2_1_fold. Hint Unfold monotone9_2. -Arguments paco9_2_0_acc [ T0 T1 T2 T3 T4 T5 T6 T7 T8 ]. -Arguments paco9_2_1_acc [ T0 T1 T2 T3 T4 T5 T6 T7 T8 ]. -Arguments paco9_2_0_mon [ T0 T1 T2 T3 T4 T5 T6 T7 T8 ]. -Arguments paco9_2_1_mon [ T0 T1 T2 T3 T4 T5 T6 T7 T8 ]. -Arguments paco9_2_0_mult_strong [ T0 T1 T2 T3 T4 T5 T6 T7 T8 ]. -Arguments paco9_2_1_mult_strong [ T0 T1 T2 T3 T4 T5 T6 T7 T8 ]. -Arguments paco9_2_0_mult [ T0 T1 T2 T3 T4 T5 T6 T7 T8 ]. -Arguments paco9_2_1_mult [ T0 T1 T2 T3 T4 T5 T6 T7 T8 ]. -Arguments paco9_2_0_fold [ T0 T1 T2 T3 T4 T5 T6 T7 T8 ]. -Arguments paco9_2_1_fold [ T0 T1 T2 T3 T4 T5 T6 T7 T8 ]. -Arguments paco9_2_0_unfold [ T0 T1 T2 T3 T4 T5 T6 T7 T8 ]. -Arguments paco9_2_1_unfold [ T0 T1 T2 T3 T4 T5 T6 T7 T8 ]. - -Instance paco9_2_0_inst T0 T1 T2 T3 T4 T5 T6 T7 T8 (gf_0 gf_1 : rel9 T0 T1 T2 T3 T4 T5 T6 T7 T8->_) r_0 r_1 x0 x1 x2 x3 x4 x5 x6 x7 x8 : paco_class (paco9_2_0 gf_0 gf_1 r_0 r_1 x0 x1 x2 x3 x4 x5 x6 x7 x8) := -{ pacoacc := paco9_2_0_acc gf_0 gf_1; - pacomult := paco9_2_0_mult gf_0 gf_1; - pacofold := paco9_2_0_fold gf_0 gf_1; - pacounfold := paco9_2_0_unfold gf_0 gf_1 }. - -Instance paco9_2_1_inst T0 T1 T2 T3 T4 T5 T6 T7 T8 (gf_0 gf_1 : rel9 T0 T1 T2 T3 T4 T5 T6 T7 T8->_) r_0 r_1 x0 x1 x2 x3 x4 x5 x6 x7 x8 : paco_class (paco9_2_1 gf_0 gf_1 r_0 r_1 x0 x1 x2 x3 x4 x5 x6 x7 x8) := -{ pacoacc := paco9_2_1_acc gf_0 gf_1; - pacomult := paco9_2_1_mult gf_0 gf_1; - pacofold := paco9_2_1_fold gf_0 gf_1; - pacounfold := paco9_2_1_unfold gf_0 gf_1 }. - Global Opaque paco9_3_0. Global Opaque paco9_3_1. Global Opaque paco9_3_2. @@ -746,40 +783,3 @@ Hint Resolve paco9_3_1_fold. Hint Resolve paco9_3_2_fold. Hint Unfold monotone9_3. -Arguments paco9_3_0_acc [ T0 T1 T2 T3 T4 T5 T6 T7 T8 ]. -Arguments paco9_3_1_acc [ T0 T1 T2 T3 T4 T5 T6 T7 T8 ]. -Arguments paco9_3_2_acc [ T0 T1 T2 T3 T4 T5 T6 T7 T8 ]. -Arguments paco9_3_0_mon [ T0 T1 T2 T3 T4 T5 T6 T7 T8 ]. -Arguments paco9_3_1_mon [ T0 T1 T2 T3 T4 T5 T6 T7 T8 ]. -Arguments paco9_3_2_mon [ T0 T1 T2 T3 T4 T5 T6 T7 T8 ]. -Arguments paco9_3_0_mult_strong [ T0 T1 T2 T3 T4 T5 T6 T7 T8 ]. -Arguments paco9_3_1_mult_strong [ T0 T1 T2 T3 T4 T5 T6 T7 T8 ]. -Arguments paco9_3_2_mult_strong [ T0 T1 T2 T3 T4 T5 T6 T7 T8 ]. -Arguments paco9_3_0_mult [ T0 T1 T2 T3 T4 T5 T6 T7 T8 ]. -Arguments paco9_3_1_mult [ T0 T1 T2 T3 T4 T5 T6 T7 T8 ]. -Arguments paco9_3_2_mult [ T0 T1 T2 T3 T4 T5 T6 T7 T8 ]. -Arguments paco9_3_0_fold [ T0 T1 T2 T3 T4 T5 T6 T7 T8 ]. -Arguments paco9_3_1_fold [ T0 T1 T2 T3 T4 T5 T6 T7 T8 ]. -Arguments paco9_3_2_fold [ T0 T1 T2 T3 T4 T5 T6 T7 T8 ]. -Arguments paco9_3_0_unfold [ T0 T1 T2 T3 T4 T5 T6 T7 T8 ]. -Arguments paco9_3_1_unfold [ T0 T1 T2 T3 T4 T5 T6 T7 T8 ]. -Arguments paco9_3_2_unfold [ T0 T1 T2 T3 T4 T5 T6 T7 T8 ]. - -Instance paco9_3_0_inst T0 T1 T2 T3 T4 T5 T6 T7 T8 (gf_0 gf_1 gf_2 : rel9 T0 T1 T2 T3 T4 T5 T6 T7 T8->_) r_0 r_1 r_2 x0 x1 x2 x3 x4 x5 x6 x7 x8 : paco_class (paco9_3_0 gf_0 gf_1 gf_2 r_0 r_1 r_2 x0 x1 x2 x3 x4 x5 x6 x7 x8) := -{ pacoacc := paco9_3_0_acc gf_0 gf_1 gf_2; - pacomult := paco9_3_0_mult gf_0 gf_1 gf_2; - pacofold := paco9_3_0_fold gf_0 gf_1 gf_2; - pacounfold := paco9_3_0_unfold gf_0 gf_1 gf_2 }. - -Instance paco9_3_1_inst T0 T1 T2 T3 T4 T5 T6 T7 T8 (gf_0 gf_1 gf_2 : rel9 T0 T1 T2 T3 T4 T5 T6 T7 T8->_) r_0 r_1 r_2 x0 x1 x2 x3 x4 x5 x6 x7 x8 : paco_class (paco9_3_1 gf_0 gf_1 gf_2 r_0 r_1 r_2 x0 x1 x2 x3 x4 x5 x6 x7 x8) := -{ pacoacc := paco9_3_1_acc gf_0 gf_1 gf_2; - pacomult := paco9_3_1_mult gf_0 gf_1 gf_2; - pacofold := paco9_3_1_fold gf_0 gf_1 gf_2; - pacounfold := paco9_3_1_unfold gf_0 gf_1 gf_2 }. - -Instance paco9_3_2_inst T0 T1 T2 T3 T4 T5 T6 T7 T8 (gf_0 gf_1 gf_2 : rel9 T0 T1 T2 T3 T4 T5 T6 T7 T8->_) r_0 r_1 r_2 x0 x1 x2 x3 x4 x5 x6 x7 x8 : paco_class (paco9_3_2 gf_0 gf_1 gf_2 r_0 r_1 r_2 x0 x1 x2 x3 x4 x5 x6 x7 x8) := -{ pacoacc := paco9_3_2_acc gf_0 gf_1 gf_2; - pacomult := paco9_3_2_mult gf_0 gf_1 gf_2; - pacofold := paco9_3_2_fold gf_0 gf_1 gf_2; - pacounfold := paco9_3_2_unfold gf_0 gf_1 gf_2 }. -