Skip to content

Commit

Permalink
define n-ary paco using 1-ary paco
Browse files Browse the repository at this point in the history
  • Loading branch information
@minkiminki
minkiminki committed Jul 22, 2018
1 parent 1fe32cc commit 3035adc
Show file tree
Hide file tree
Showing 23 changed files with 9,481 additions and 1,407 deletions.
1 change: 1 addition & 0 deletions .gitignore
View file
Original file line number Diff line number Diff line change
Expand Up @@ -10,3 +10,4 @@ _CoqProject
*.glob
*.pyc
\#*\#
*~
2 changes: 2 additions & 0 deletions metasrc/build.sh
View file
Original file line number Diff line number Diff line change
Expand Up @@ -7,8 +7,10 @@ relsize=15
mutsize=3

python paconotation.py $maxsize > $PACOSRCDIR/paconotation.v
python paconotation_internal.py $maxsize > $PACOSRCDIR/paconotation_internal.v
python pacotac.py $maxsize > $PACOSRCDIR/pacotac.v
python pacotacuser.py > $PACOSRCDIR/pacotacuser.v
python pacon.py ${mutsize} > $PACOSRCDIR/pacon.v

echo "" > $PACOSRCDIR/paco.v
for i in `seq 0 $relsize`; do
Expand Down
498 changes: 339 additions & 159 deletions metasrc/paco.py
View file

Large diffs are not rendered by default.

206 changes: 206 additions & 0 deletions metasrc/pacon.py
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,206 @@
from __future__ import print_function
import sys
from pacolib import *

if len(sys.argv) < 2:
sys.stderr.write('\nUsage: '+sys.argv[0]+' relsize mutsize\n\n')
sys.exit(1)

mutsize = int(sys.argv[1])

print ('Require Export paconotation pacotacuser.')
print ('Require Import pacotac paconotation_internal.')
print ('Set Implicit Arguments.')
print ('')

n = 1

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.')
print ('')
print ('CoInductive ',end='')
for i in range(m):
print (ifpstr(i,"with ")+'paco'+lev(m)+idx(m,i)+'('+itridx(' r',m)+': rel'+str(n)+itrstr(' T',n)+')'+itrstr(" x",n)+' : Prop :=')
print ('| paco'+lev(m)+idx(m,i)+'_pfold'+itridx(' pco',m))
for j in range(m):
print (' (LE : pco'+idx(m,j)+' <'+str(n)+'= (paco'+lev(m)+idx(m,j)+itridx(' r',m)+' \\'+str(n)+'/ r'+idx(m,j)+'))')
print (' (SIM: gf'+idx(m,i)+itridx(' pco',m)+itrstr(" x",n)+')')
print ('.')
for i in range(m):
print ('Definition ',end='')
print ('upaco'+lev(m)+idx(m,i)+'('+itridx(' r',m)+': rel'+str(n)+itrstr(' T',n)+')'+' := '+'paco'+lev(m)+idx(m,i)+itridx(' r',m)+' \\'+str(n)+'/ r'+idx(m,i),end='')
print ('.')
print ('End Arg'+str(n)+lev(m)+'_def.')
for i in range(m):
print ('Arguments paco'+lev(m)+idx(m,i)+ifpstr(n,' ['+itrstr(" T",n)+' ].'," : clear implicits."))
print ('Arguments upaco'+lev(m)+idx(m,i)+ifpstr(n,' ['+itrstr(" T",n)+' ].'," : clear implicits."))
print ('Hint Unfold upaco'+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"+lev(m)+itrstr(" T",n)+" (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"+lev(m)+itrstr(" T",n)+" (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"+lev(m)+'_eq'+itrstr(" T",n)+" (gf: "+m*("rel"+str(n)+itrstr(" T",n)+" -> ")+"rel"+str(n)+itrstr(" T",n)+") :")
print (" monotone"+lev(m)+' gf <-> _monotone'+lev(m)+' gf.')
print ("Proof. unfold monotone"+lev(m)+', _monotone'+lev(m)+', le'+str(n)+'. split; eauto. 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.')
print ('')
for i in range(m):
print ('Theorem paco'+lev(m)+idx(m,i)+'_acc: forall')
print (' l'+itridx(' r',m)+' (OBG: forall rr (INC: r'+idx(m,i)+' <'+str(n)+'= rr) (CIH: l <'+str(n)+'= rr), l <'+str(n)+'= paco'+lev(m)+idx(m,i)+itridx(" gf",m),end='')
for j in range(m):
if j == i:
print (' rr',end='')
else:
print (' r'+idx(m,j),end='')
print ('),')
print (' l <'+str(n)+'= paco'+lev(m)+idx(m,i)+itridx(" gf",m)+itridx(' r',m)+'.')
print ('Proof.')
print (' intros; assert (SIM: paco'+lev(m)+idx(m,i)+itridx(" gf",m),end='')
for j in range(m):
if j == i:
print (' (r'+idx(m,j)+' \\'+str(n)+'/ l)',end='')
else:
print (' r'+idx(m,j),end='')
print (itrstr(" x",n)+') by eauto.')
print (' clear PR; repeat (try left; do '+str(n+1)+' paco_revert; paco_cofix_auto).')
print ('Qed.')
print ('')
for i in range(m):
print ('Theorem paco'+lev(m)+idx(m,i)+'_mon: monotone'+lev(m)+' (paco'+lev(m)+idx(m,i)+itridx(" gf",m)+').')
print ('Proof. paco_cofix_auto; repeat (left; do '+str(n+1)+' paco_revert; paco_cofix_auto). Qed.')
print ('')
for i in range(m):
print ('Theorem paco'+lev(m)+idx(m,i)+'_mult_strong: forall'+itridx(' r',m)+',')
print (' paco'+lev(m)+idx(m,i)+itridx(" gf",m),end='')
for j in range(m):
print (' (upaco'+lev(m)+idx(m,j)+itridx(" gf",m)+itridx(' r',m)+')',end='')
print (' <'+str(n)+'= paco'+lev(m)+idx(m,i)+itridx(" gf",m)+itridx(' r',m)+'.')
print ('Proof. paco_cofix_auto; repeat (left; do '+str(n+1)+' paco_revert; paco_cofix_auto). Qed.')
print ('')
for i in range(m):
print ('Corollary paco'+lev(m)+idx(m,i)+'_mult: forall'+itridx(' r',m)+',')
print (' paco'+lev(m)+idx(m,i)+itridx(" gf",m)+itridx(' (paco'+lev(m),m,itridx(" gf",m)+itridx(' r',m)+')')+' <'+str(n)+'= paco'+lev(m)+idx(m,i)+itridx(" gf",m)+itridx(' r',m)+'.')
print ('Proof. intros; eapply paco'+lev(m)+idx(m,i)+'_mult_strong, paco'+lev(m)+idx(m,i)+'_mon; eauto. Qed.')
print ('')
for i in range(m):
print ('Theorem paco'+lev(m)+idx(m,i)+'_fold: forall'+itridx(' r',m)+',')
print (' gf'+idx(m,i),end='')
for j in range(m):
print (' (upaco'+lev(m)+idx(m,j)+itridx(" gf",m)+itridx(' r',m)+')',end='')
print (' <'+str(n)+'= paco'+lev(m)+idx(m,i)+itridx(" gf",m)+itridx(' r',m)+'.')
print ('Proof. intros; econstructor; ['+m*' |'+'eauto]; eauto. Qed.')
print ('')
for i in range(m):
print ('Theorem paco'+lev(m)+idx(m,i)+'_unfold: forall'+itridx(' (MON: monotone'+lev(m)+' gf',m,')')+itridx(' r',m)+',')
print (' paco'+lev(m)+idx(m,i)+itridx(" gf",m)+itridx(' r',m)+' <'+str(n)+'= gf'+idx(m,i),end='')
for j in range(m):
print (' (upaco'+lev(m)+idx(m,j)+itridx(" gf",m)+itridx(' r',m)+')',end='')
print ('.')
print ('Proof. unfold monotone'+lev(m)+'; intros; destruct PR; eauto. Qed.')
print ('')

for i in range(m):
print ('Theorem _paco'+lev(m)+idx(m,i)+'_acc: forall')
print (' l'+itridx(' r',m)+' (OBG: forall rr (INC: r'+idx(m,i)+' <'+str(n)+'== rr) (CIH: l <'+str(n)+'== rr), l <'+str(n)+'== paco'+lev(m)+idx(m,i)+itridx(" gf",m),end='')
for j in range(m):
if j == i:
print (' rr',end='')
else:
print (' r'+idx(m,j),end='')
print ('),')
print (' l <'+str(n)+'== paco'+lev(m)+idx(m,i)+itridx(" gf",m)+itridx(' r',m)+'.')
print ('Proof. unfold le1. eapply paco'+lev(m)+idx(m,i)+'_acc. Qed.')
print ('')
for i in range(m):
print ('Theorem _paco'+lev(m)+idx(m,i)+'_mon: _monotone'+lev(m)+' (paco'+lev(m)+idx(m,i)+itridx(" gf",m)+').')
print ('Proof. apply monotone'+lev(m)+'_eq. eapply paco'+lev(m)+idx(m,i)+'_mon. Qed.')
print ('')
for i in range(m):
print ('Theorem _paco'+lev(m)+idx(m,i)+'_mult_strong: forall'+itridx(' r',m)+',')
print (' paco'+lev(m)+idx(m,i)+itridx(" gf",m),end='')
for j in range(m):
print (' (upaco'+lev(m)+idx(m,j)+itridx(" gf",m)+itridx(' r',m)+')',end='')
print (' <'+str(n)+'== paco'+lev(m)+idx(m,i)+itridx(" gf",m)+itridx(' r',m)+'.')
print ('Proof. unfold le1. eapply paco'+lev(m)+idx(m,i)+'_mult_strong. Qed.')
print ('')
for i in range(m):
print ('Theorem _paco'+lev(m)+idx(m,i)+'_fold: forall'+itridx(' r',m)+',')
print (' gf'+idx(m,i),end='')
for j in range(m):
print (' (upaco'+lev(m)+idx(m,j)+itridx(" gf",m)+itridx(' r',m)+')',end='')
print (' <'+str(n)+'== paco'+lev(m)+idx(m,i)+itridx(" gf",m)+itridx(' r',m)+'.')
print ('Proof. unfold le1. eapply paco'+lev(m)+idx(m,i)+'_fold. Qed.')
print ('')
for i in range(m):
print ('Theorem _paco'+lev(m)+idx(m,i)+'_unfold: forall'+itridx(' (MON: _monotone'+lev(m)+' gf',m,')')+itridx(' r',m)+',')
print (' paco'+lev(m)+idx(m,i)+itridx(" gf",m)+itridx(' r',m)+' <'+str(n)+'== gf'+idx(m,i),end='')
for j in range(m):
print (' (upaco'+lev(m)+idx(m,j)+itridx(" gf",m)+itridx(' r',m)+')',end='')
print ('.')
print ('Proof.')
print (' unfold le1. repeat_intros '+str(m)+'.')
print (' eapply paco'+lev(m)+idx(m,i)+'_unfold; apply monotone'+lev(m)+'_eq; eauto.')
print ('Qed.')
print ('')

print ('End Arg'+str(n)+'_'+str(m)+'.')
print ('')
print ('Hint Unfold monotone'+lev(m)+'.')
for i in range(m):
print ('Hint Resolve paco'+lev(m)+idx(m,i)+'_fold.')
print ('')
for i in range(m):
print ('Arguments paco'+lev(m)+idx(m,i)+'_acc'+ifpstr(n,' ['+itrstr(" T",n)+' ].'," : clear implicits."))
for i in range(m):
print ('Arguments paco'+lev(m)+idx(m,i)+'_mon'+ifpstr(n,' ['+itrstr(" T",n)+' ].'," : clear implicits."))
for i in range(m):
print ('Arguments paco'+lev(m)+idx(m,i)+'_mult_strong'+ifpstr(n,' ['+itrstr(" T",n)+' ].'," : clear implicits."))
for i in range(m):
print ('Arguments paco'+lev(m)+idx(m,i)+'_mult'+ifpstr(n,' ['+itrstr(" T",n)+' ].'," : clear implicits."))
for i in range(m):
print ('Arguments paco'+lev(m)+idx(m,i)+'_fold'+ifpstr(n,' ['+itrstr(" T",n)+' ].'," : clear implicits."))
for i in range(m):
print ('Arguments paco'+lev(m)+idx(m,i)+'_unfold'+ifpstr(n,' ['+itrstr(" T",n)+' ].'," : clear implicits."))
print ('')
46 changes: 46 additions & 0 deletions metasrc/paconotation_internal.py
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,46 @@
from __future__ import print_function
import sys
from pacolib import *

if len(sys.argv) < 2:
sys.stderr.write('\nUsage: '+sys.argv[0]+' relsize\n\n')
sys.exit(1)

relsize = int(sys.argv[1])

print ("Require Import paconotation.")
print ("")

print ("Tactic Notation \"repeat_intros\" int(n)")
print (" := let name := fresh \"x\" in")
print (" do n (let name := fresh \"x\" in intros name).")
print ()

print ("(** ** Less than or equal *)")
print ()
for n in range (relsize+1):
print ("Definition le"+str(n)+itrstr(" T",n)+" (p q : rel"+str(n)+itrstr(" T",n)+") :=")
print (" (forall"+itrstr(" x",n)+" (PR: p"+itrstr(" x",n)+" : Prop), q"+itrstr(" x",n)+" : Prop).")
print ("Arguments le"+str(n)+ifpstr(n, " ["+itrstr(" T",n)+"].", " : clear implicits."))
print ()

for n in range (relsize+1):
print ("Notation \"p <"+str(n)+"== q\" :=")
print (" (le"+str(n)+" p q)")
print (" (at level 50, no associativity"+ifzstr(n,", only parsing")+").")
print ()

print ("(** ** Tranisitivity and Reflexivity *)")
print ()
for n in range (relsize+1):
print ("Lemma le"+str(n)+"_trans"+itrstr(" T",n)+"(r0 r1 r2 : rel"+str(n)+itrstr(" T",n)+")")
print (" (LE0 : r0 <"+str(n)+"== r1) (LE1 : r1 <"+str(n)+"== r2) :")
print (" r0 <"+str(n)+"== r2.")
print ("Proof. repeat_intros "+str(n)+". intros H. auto. Qed.")
print ()

for n in range (relsize+1):
print ("Lemma le"+str(n)+"_refl"+itrstr(" T",n)+"(r : rel"+str(n)+itrstr(" T",n)+") :")
print (" r <"+str(n)+"== r.")
print ("Proof. repeat_intros "+str(n)+". intros H. auto. Qed.")
print ()
Loading

0 comments on commit 3035adc

Please sign in to comment.