(****************************************************************
A Sample Session

# A Sample Session

Try out the new tactics by the miracle of cut and paste. Thrill as they take years and generate spurious diagnostic noise! You'll need the version of the library back up a page.

*) Load lib_finite; (* The existing module system can't cope with utility theorems being generated on the fly: they get shoved into the context when they're made and dumped into whatever .o file is being built at the time. Next time you do Make with a different dependency pattern and the thing you need isn't there. I know how to fix it. But. *) (* A bit of programming: a program is a goal with a sigma-type whose .1 is a function and whose .2 is a sigma of universally quantified equations. *) Goal LIFT : <lift:{m,n|nat}{f:(fin n)->fin m}{x:fin (suc n)}fin (suc m)> ({m,n:nat}{f:(fin n)->fin m} Eq (lift f (f_zero n)) (f_zero m))# ({m,n|nat}{f:(fin n)->fin m}{x:fin n} Eq (lift f (f_suc x)) (f_suc (f x))); Eduardo x; (* The Eduardo tactic unwinds structural recursion on a nominated argument. The name comes from the stated type of lift. Do not be alarmed by the strange noises: that's just rattling from the shed. *) Dale; (* See? We have two new programs, but they're just *) Dale; (* imitiation: beta-0 will see to them. *) (* After a long delay, it typechecks. Now we do... *) SaveReductions lift; (* What has happened? Let's find out. *) Ctxt 3; (* LIFT has been saved as usual, but lift has also been added, frozen, but with the reduction behaviour given by the equations from LIFT: these are checked first to make sure they correspond to genuine conversions, but I don't check that they don't break SN... In general, Freeze now switches a defined var between its delta-reduction behaviour and any special reduction behaviour you might have given it. *) Goal THIN : <thin:{n|nat}{w:fin (suc n)}{x:fin n}fin (suc n)> ({n|nat} Eq (thin (f_zero n)) (f_suc|n))# ({n|nat}{w:fin (suc n)} Eq (thin (f_suc w)) (lift (thin w))); Eduardo w; Dale; Eduardo n; (* need an extra pattern split on n: *) Dale; (* there's an implicit (suc n) in the pattern *) Cases x; (* we must also kill the impossible case *) SaveReductions thin; (* Let's declare a type! *) [A:Type]; Inductive [maybe:Type] Theorems (* Theorems causes my stuff to be generated. *) Constructors [yes:A->maybe] [no:maybe]; (* much work takes place *) Discharge A ?; (* The ? is a nasty hack, predating the better hack in the last official release of LEGO. *) (* What's happened? *) Ctxt 26; (* quite a lot *) (* Let's use infix! *) Configure Infix / right 4; [T,S|Type]; Goal PROPAGATE : <op/:{f:S->T}{x:maybe S}maybe T> ({f:S->T}{s:S} Eq (f / (yes s)) (yes (f s)))# ({f:S->T} Eq (f / (no S)) (no T)); Eduardo x Then Dale; (* if you've got tacticals, you might as well use 'em *) SaveReductions op/; (* Why didn't I fix f as well? Try it and see... *) [f:S->T]; Goal propElim : {Phi:(maybe S)->(maybe T)->Type} {phiYes:{s:S}Phi (yes s) (yes (f s))} {phiNo:Phi (no ?) (no ?)} {x:maybe S}Phi x (f / x); intros ___; Cases x; (* this sees x is a maybe and looks up %maybe cases% you try it too... *) %maybe cases%; (* see ? *) (* try this too *) %37%; (* sorry, got distracted *) Immed; Save; Discharge T; Goal THICK : <thick:{n|nat}{w,i:fin (suc n)}maybe (fin n)> ({n|nat} Eq (thick (f_zero n) (f_zero n)) (no ?))# (* ? is OK *) ({n|nat}{i:fin n} Eq (thick (f_zero n) (f_suc i)) (yes i))# ({n|nat}{w:fin (suc n)} Eq (thick (f_suc w) (f_zero ?)) (yes (f_zero ?)))# ({n|nat}{w,i:fin (suc n)} Eq (thick (f_suc w) (f_suc i)) ((f_suc|?) / (thick w i))); Eduardo w; Eduardo i Then Dale; Eduardo n; Eduardo i Then Dale; Cases x; (* several years later... *) SaveReductions thick; (* this'll take a while too... *) (* usually I look up the reductions, copy them into the script and comment out the proof that generated them *) (* By the way, when you Eduardo a variable, the recursion scheme generated will only include the stuff to the right of it. Basically, you've got to put the arguments left to right lexicographically. You can't do Ackermann's backwards. *) Goal thickElim : {n|nat}{w:fin (suc n)} {Phi:{i:fin (suc n)}{j:maybe (fin n)}Type} {phiHit:Phi w (no ?)} {phiMiss:{j:fin n}Phi (thin w j) (yes j)} {i:fin (suc n)}Phi i (thick w i); Induction w; (* finds the type of w, fin, eliminates by %fin elim%, unifies *) Cases i (* same deal but with %fin cases% *) Then intros Then Immed; Cases n; Cases x; (* kills fin zero *) Cases i; intros; Refine phiMiss (f_zero ?); intros n i w wh ___; Refine wh (Eq_refl ?) (* sorry, my tactic isn't *) ([i:fin (suc n)][j:maybe (fin n)] (* clever enough yet *) Phi (f_suc i) (f_suc|n / j)); Immed; intros j; Refine phiMiss (f_suc ?); Save; (* What else? *) Goal blah : {n|nat}{x:fin (suc n)}Prop; (* ?0 : {n|nat}(fin (suc n))->Prop *) (* LEGO is suppressing the name, but it's still there *) Induction x; (* see ? *) Undo 1; Induction 1; (* the unnamed arguments may also be accessed by numbers, *) KillRef; (* counting 1,2... from the left *) (* If you want to do unification separately... *) Goal {x:nat}(Eq x (suc (suc (suc x))))->absurd; KJunify; (* it's dead *) Goal {x:nat}(Eq x %3%)->Eq (plus x %1%) %4%; KJunify; (* this works *) Undo 1; intros x; KJunify; (* this doesn't (sorry about the uncaught exception) *) KillRef; (* KJunify only regards goal premises as flexible variables; it never does any intros, unlike ye olde Qnify *) (* If you want to eliminate without unification... *) Goal {x,y:nat}(Eq x y)->Prop; Induction x; (* see, it's even unified in the inductive hypothesis ? *) Undo 1; Clobber x nat_elim; (* just unification and nothing else *) Undo 1; Elim x nat_elim; (* a longer way of saying Induction x *) Undo 1; Clobber x nat_elim Then KJunify; Next+1; (* no unification in the inductive hypothesis: Elim does more than Clobber Then KJunify *) KillRef; (* You can use Clobber and Elim with your own elim rules! *) (* Finally, let's make mu-type fins *) (* Erm... *) Configure Infix + right 3; [L,R:Type]; Inductive [op+:Type] Theorems Constructors [inL:L->op+] [inR:R->op+]; Discharge L ?; op+_elim; (* grrrrr *) %op+ elim %; (* phew *) (* but we're gonna break the module system *) Inductive [empty:Type] Theorems Constructors; (* Here goes... *) Goal FIN : <Fin:nat->Type> (Eq (Fin zero) empty)# ({n:nat} Eq (Fin (suc n)) (unit + (Fin n))); Eduardo 1 Then Dale; SaveReductions Fin; (* then let's equip them with constructors... *) [Fz [n:nat] = inL (Fin n) void] [Fs [n|nat][x:Fin n] = inR unit x]; (* ...and an elim rule... *) Goal FinElim : {Phi:{n|nat}(Fin n)->Type} {phiz:{n:nat}Phi|(suc n) (Fz n)} {phis:{n|nat}{x:Fin n}(Phi x)->Phi|(suc n) (Fs x)} {n|nat}{x:Fin n}Phi x; intros ___; Induction n; Cases x; (* that'll be a bug, then *) Undo 1; Refine empty_elim; (* sorry *) Cases x; Cases x2; intros n nh; Refine phiz n; intros n x nh; Refine phis x; Immed; Save; (* Now you can do stuff with this like so *) Goal FinEq : {n|nat}(Fin n)->(Fin n)->bool; Elim 1 FinElim; KillRef; (* Or you can tell the tactics about Fin *) Configure Memo Fin Fin; (* first a tag as in % % then the tagged identifier *) Configure Memo Fin elim FinElim; (* % % *) Goal FinEq : {n|nat}(Fin n)->(Fin n)->bool; Induction 1; KillRef; (* hang on a minute *); (* I like to see what I'm doing... *) [FINEQ [n|nat][x,y:Fin n] = bool]; Goal FinEq : {n|nat}{x,y:Fin n}FINEQ x y; Induction x Then Cases y; intros; Refine true; intros; Refine false; intros; Refine false; intros n y x xh; Refine xh y; Save; (* How about that to start with? *) (**)