Skip to content

Commit

Permalink
more speed up
Browse files Browse the repository at this point in the history
  • Loading branch information
@minkiminki
minkiminki committed Jul 22, 2018
1 parent 3035adc commit a85b819
Show file tree
Hide file tree
Showing 17 changed files with 1,404 additions and 2,554 deletions.
54 changes: 20 additions & 34 deletions metasrc/paco.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -16,7 +16,7 @@

n = relsize

print ('Section SIGT.')
print ('Section PACO'+str(n)+'.')
print ('')

for i in range(n):
Expand Down Expand Up @@ -102,20 +102,12 @@
print ('Qed.')
print ('')

print ('End SIGT.')
print ('')

print ('(** ** Predicates of Arity '+str(n))
print ('*)')
print ('')

for m in range(1,mutsize+1):
print ('Section Arg'+str(n)+lev(m)+'_def.')
for i in range(n):
print ('Variable T'+str(i)+' : '+ifpstr(i,'forall'),end='')
for j in range(i):
print (' (x'+str(j)+': @T'+str(j)+itrstr(" x",j)+')',end='')
print (ifpstr(i,', ')+'Type.')
print ('Variable'+itridx(" gf",m)+' : '+m*('rel'+str(n)+itrstr(" T",n)+' -> ')+'rel'+str(n)+itrstr(" T",n)+'.')
for i in range(m):
print ('Arguments gf'+idx(m,i)+' : clear implicits.')
Expand All @@ -136,51 +128,40 @@
print ('.')
print ('End Arg'+str(n)+lev(m)+'_def.')
for i in range(m):
print ('Arguments paco'+str(n)+lev(m)+idx(m,i)+ifpstr(n,' ['+itrstr(" T",n)+' ].'," : clear implicits."))
print ('Arguments upaco'+str(n)+lev(m)+idx(m,i)+ifpstr(n,' ['+itrstr(" T",n)+' ].'," : clear implicits."))
print ('Arguments paco'+str(n)+lev(m)+idx(m,i)+' : clear implicits.')
print ('Arguments upaco'+str(n)+lev(m)+idx(m,i)+' : clear implicits.')
print ('Hint Unfold upaco'+str(n)+lev(m)+idx(m,i)+'.')
print ('')

print ("(* Less than or equal - internal use only *)")
print ("Notation \"p <_paco_"+str(n)+"= q\" :=")
print (" (forall"+itrstr(" _paco_x",n)+" (PR: p"+itrstr(" _paco_x",n)+" : Prop), q"+itrstr(" _paco_x",n)+" : Prop)")
print (" (at level 50, no associativity).")
print ('')

for m in range (1,mutsize+1):
print ('(** '+str(m)+' Mutual Coinduction *)')
print ('')
print ('Section Arg'+str(n)+'_'+str(m)+'.')
print ('')
print ("Definition monotone"+str(n)+lev(m)+itrstr(" T",n)+" (gf: "+m*("rel"+str(n)+itrstr(" T",n)+" -> ")+"rel"+str(n)+itrstr(" T",n)+") :=")
print ("Definition monotone"+str(n)+lev(m)+" (gf: "+m*("rel"+str(n)+itrstr(" T",n)+" -> ")+"rel"+str(n)+itrstr(" T",n)+") :=")
print (" forall"+itrstr(" x",n)+itridx(" r",m)+itridx(" r'",m)+" (IN: gf"+itridx(" r",m)+itrstr(" x",n)+") ",end='')
for i in range(m):
print ("(LE"+idx(m,i)+": r"+idx(m,i)+" <"+str(n)+"= r'"+idx(m,i)+")",end='')
print (", gf"+itridx(" r'",m)+itrstr(" x",n)+".")
print ('')
print ("Definition _monotone"+str(n)+lev(m)+itrstr(" T",n)+" (gf: "+m*("rel"+str(n)+itrstr(" T",n)+" -> ")+"rel"+str(n)+itrstr(" T",n)+") :=")
print ("Definition _monotone"+str(n)+lev(m)+" (gf: "+m*("rel"+str(n)+itrstr(" T",n)+" -> ")+"rel"+str(n)+itrstr(" T",n)+") :=")
print (" forall"+itridx(" r",m)+itridx(" r'",m),end='')
for i in range(m):
print ("(LE"+idx(m,i)+": r"+idx(m,i)+" <"+str(n)+"= r'"+idx(m,i)+")",end='')
print (", gf"+itridx(" r",m)+' <'+str(n)+'== gf'+itridx(" r'",m)+'.')
print ('')
print ("Lemma monotone"+str(n)+lev(m)+'_eq'+itrstr(" T",n)+" (gf: "+m*("rel"+str(n)+itrstr(" T",n)+" -> ")+"rel"+str(n)+itrstr(" T",n)+") :")
print ("Lemma monotone"+str(n)+lev(m)+'_eq'+" (gf: "+m*("rel"+str(n)+itrstr(" T",n)+" -> ")+"rel"+str(n)+itrstr(" T",n)+") :")
print (" monotone"+str(n)+lev(m)+' gf <-> _monotone'+str(n)+lev(m)+' gf.')
print ("Proof. unfold monotone"+str(n)+lev(m)+', _monotone'+str(n)+lev(m)+', le'+str(n)+'. split; eauto. Qed.')
print ('')
print ("Lemma monotone"+str(n)+lev(m)+'_map'+itrstr(" T",n)+" (gf: "+m*("rel"+str(n)+itrstr(" T",n)+" -> ")+"rel"+str(n)+itrstr(" T",n)+")")
print ("Lemma monotone"+str(n)+lev(m)+'_map'+" (gf: "+m*("rel"+str(n)+itrstr(" T",n)+" -> ")+"rel"+str(n)+itrstr(" T",n)+")")
print (" (MON: _monotone"+str(n)+lev(m)+' gf) :')
print (" _monotone"+lev(m)+' (fun'+itrstr(' R', m)+' => curry'+str(n)+' (gf'+itrstr(' (uncurry'+str(n)+' R', m, ')')+')).')
print ('Proof.')
print (' repeat_intros '+str(3*m)+'. apply curry_map'+str(n)+'. apply MON; apply uncurry_map'+str(n)+'; auto.')
print ('Qed.')
print ('')

for i in range(n):
print ('Variable T'+str(i)+' : '+ifpstr(i,'forall'),end='')
for j in range(i):
print (' (x'+str(j)+': @T'+str(j)+itrstr(" x",j)+')',end='')
print (ifpstr(i,', ')+'Type.')
print ('Variable'+itridx(" gf",m)+' : '+m*('rel'+str(n)+itrstr(" T",n)+' -> ')+'rel'+str(n)+itrstr(" T",n)+'.')
for i in range(m):
print ('Arguments gf'+idx(m,i)+' : clear implicits.')
Expand Down Expand Up @@ -305,10 +286,22 @@

print ('End Arg'+str(n)+'_'+str(m)+'.')
print ('')
print ('Hint Unfold monotone'+str(n)+lev(m)+'.')

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 ('')

for i in range(m):
print ('Arguments paco'+str(n)+lev(m)+idx(m,i)+'_acc'+ifpstr(n,' ['+itrstr(" T",n)+' ].'," : clear implicits."))
for i in range(m):
Expand All @@ -323,13 +316,6 @@
print ('Arguments paco'+str(n)+lev(m)+idx(m,i)+'_unfold'+ifpstr(n,' ['+itrstr(" T",n)+' ].'," : clear implicits."))
print ('')

for i in range(m):
print ('Global Opaque paco'+str(n)+lev(m)+idx(m,i)+'.')
print ('Global Opaque paco'+str(n)+lev(m)+idx(m,i)+'_acc.')
print ('Global Opaque paco'+str(n)+lev(m)+idx(m,i)+'_mult.')
print ('Global Opaque paco'+str(n)+lev(m)+idx(m,i)+'_fold.')
print ('Global Opaque paco'+str(n)+lev(m)+idx(m,i)+'_unfold.')
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 ("{ pacoacc := paco"+str(n)+lev(m)+idx(m,i)+"_acc"+itridx(" gf",m)+";")
Expand Down
154 changes: 64 additions & 90 deletions src/paco0.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,7 @@ Require Export paconotation pacotacuser.
Require Import paconotation_internal pacotac pacon.
Set Implicit Arguments.

Section SIGT.
Section PACO0.


Record sig0T :=
Expand Down Expand Up @@ -64,8 +64,6 @@ Proof.
apply curry_map_rev0. eapply le1_trans; [|eauto]. apply uncurry_bij1_0.
Qed.

End SIGT.

(** ** Predicates of Arity 0
*)

Expand Down Expand Up @@ -132,11 +130,6 @@ Arguments paco0_3_2 : clear implicits.
Arguments upaco0_3_2 : clear implicits.
Hint Unfold upaco0_3_2.

(* Less than or equal - internal use only *)
Notation "p <_paco_0= q" :=
(forall (PR: p : Prop), q : Prop)
(at level 50, no associativity).

(** 1 Mutual Coinduction *)

Section Arg0_1.
Expand Down Expand Up @@ -238,28 +231,6 @@ Qed.

End Arg0_1.

Hint Unfold monotone0.
Hint Resolve paco0_fold.

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 Opaque paco0.
Global Opaque paco0_acc.
Global Opaque paco0_mult.
Global Opaque paco0_fold.
Global Opaque paco0_unfold.

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.
Expand Down Expand Up @@ -437,47 +408,6 @@ Qed.

End Arg0_2.

Hint Unfold monotone0_2.
Hint Resolve paco0_2_0_fold.
Hint Resolve paco0_2_1_fold.

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 Opaque paco0_2_0.
Global Opaque paco0_2_0_acc.
Global Opaque paco0_2_0_mult.
Global Opaque paco0_2_0_fold.
Global Opaque paco0_2_0_unfold.

Global Opaque paco0_2_1.
Global Opaque paco0_2_1_acc.
Global Opaque paco0_2_1_mult.
Global Opaque paco0_2_1_fold.
Global Opaque paco0_2_1_unfold.

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 }.

(** 3 Mutual Coinduction *)

Section Arg0_3.
Expand Down Expand Up @@ -731,10 +661,72 @@ Qed.

End Arg0_3.

Hint Unfold monotone0_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.
Expand All @@ -755,24 +747,6 @@ Arguments paco0_3_0_unfold : clear implicits.
Arguments paco0_3_1_unfold : clear implicits.
Arguments paco0_3_2_unfold : clear implicits.

Global Opaque paco0_3_0.
Global Opaque paco0_3_0_acc.
Global Opaque paco0_3_0_mult.
Global Opaque paco0_3_0_fold.
Global Opaque paco0_3_0_unfold.

Global Opaque paco0_3_1.
Global Opaque paco0_3_1_acc.
Global Opaque paco0_3_1_mult.
Global Opaque paco0_3_1_fold.
Global Opaque paco0_3_1_unfold.

Global Opaque paco0_3_2.
Global Opaque paco0_3_2_acc.
Global Opaque paco0_3_2_mult.
Global Opaque paco0_3_2_fold.
Global Opaque paco0_3_2_unfold.

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;
Expand Down
Loading

0 comments on commit a85b819

Please sign in to comment.