Last active
August 29, 2015 14:02
-
-
Save jcmckeown/9d4895eece12f3f0d422 to your computer and use it in GitHub Desktop.
Some trivial coq tactics whose purpose is to automagically extract/fold particular subterms of the goal type. The idea is to reduce ambiguity in human/coq interactions.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Require Import HoTT. | |
(* or your favourite source for the needed arrithmetic types *) | |
Open Scope list_scope. | |
(** | |
These are tactics to aid human consumption/production of terms compatible | |
with the goal type --- sometimes coq prettyprinting produces ambiguous | |
appearances, while refine fails unless you fill in more holes --- which is | |
hard to do if the first refinement coq finds for an ambiguously-filled hole | |
is wrong! Happily, we don't need coq to have sneakier pattern matching/ | |
unification : coq already knows all the subterms of the goal, and can pull | |
them out for us! here are some trivial ways of doing this. Someone cleverer | |
than I with Ltac or such can figure out how to customize the names of terms | |
at runtime, how to make parameters optional, etc. | |
I emphasize: these are intended to aid human interaction; I see little use | |
to calling them from your own Ltac scripts. For instance, folding terms | |
into definitional hypotheses makes it harder for later tactics to get hold | |
of them! Ltac doesn't seem to have tools for reference by name. And that's OK. | |
*) | |
Ltac inLHS := | |
match goal with | |
| |- ?A = ?B => | |
let H := fresh "lhs" in | |
set (H := A) | |
| _ => idtac "nothing to do" end. | |
Ltac inRHS := | |
match goal with | |
| |- ?A = ?B => | |
let H := fresh "rhs" in | |
set (H := B) | |
| _ => idtac "nothing to do" end. | |
(** Danger, Gill Robertsvale! it's more than possible these coercions | |
may break lots of things! That is, it's more than credible that making | |
more expressions meaningful will hide where errors are happening | |
later on. | |
*) | |
Definition lib := list Bool. | |
Definition apb : lib -> lib -> lib := (@app Bool). | |
Coercion apb : lib >-> Funclass. | |
Definition quotb : Bool -> lib := | |
fun b => (cons b nil). | |
Coercion quotb : Bool >-> lib. | |
Notation bt := true. | |
Notation bf := false. | |
(** so now, we can | |
:< Check ( bt bt bt bf bf bt bf bt bt bt ) | |
is a (list Bool), or (lib). It might also be a (lib -> lib), if necessary, but | |
not now, it isn't! | |
*) | |
(** we assume a binary tree model for all terms, which is in fact correctish! | |
however, while the natural address for a subtree of a binary tree is a binary | |
string, it's much easier to write numbers than binary strings ; and you can | |
all do base-2 arrithmetic in base-10, right? | |
*) | |
Ltac subTermOf anum Thing := | |
let z := eval vm_compute (* so we can just write our ( bft ) string and it'll work *) | |
in anum in | |
match Thing with | |
| ?A ?B => match z with | |
| nil => Thing | |
| true => A (* because we don't want to be writing ( bf : lib ) all the time ... *) | |
| false => B (* ... coercions are lazy, which is the Right Thing *) | |
| cons true ?num => subTermOf num A | |
| cons false ?num => subTermOf num B | |
end | |
| _ => Thing | |
end. | |
Ltac goalSubTerm anum := | |
let H := fresh "subterm" in | |
match goal with | |
| |- ?T => | |
let w := subTermOf anum T in | |
pose ( H := w ) end. | |
Ltac goalSubTermN anum nom := | |
let H := fresh nom in | |
match goal with | |
| |- ?T => | |
let w := subTermOf anum T in | |
pose ( H := w ) end. | |
(** this version, using set instead of pose, folds the newly named subterm | |
wherever coq thinks it appears. This may not mean that every *convertible* | |
subterm gets folded, just those that don't take work. | |
Since this changes the parse tree, [foldSubTerm]s are not commutative! | |
( More detail: strictly, the tree is only pruned a little, | |
so | |
[foldSubTerm 10w ; foldSubTerm 1w] | |
is quite reasonable, but | |
[foldSubTerm 1w ; foldSubTerm 10w ] | |
gives a [subtermN := _ : _ |- _ ] and a [ subtermN' := subtermN : _ |- _ ] | |
which probably isn't what you wanted. ) | |
*) | |
Ltac foldSubTerm anum := | |
let H := fresh "subterm" in | |
match goal with | |
| |- ?T => | |
let w := subTermOf anum T in | |
set ( H := w ) in * end. | |
Ltac foldSubTermN anum nom := | |
let H := fresh nom in | |
match goal with | |
| |- ?T => | |
let w := subTermOf anum T in | |
set ( H := w ) in * end. | |
Ltac introSubTerm n thing := | |
let w := subTermOf n thing in | |
let H := fresh "subterm" in | |
pose ( H := w ). | |
Ltac dependOnLastH := | |
match goal with | |
| [ f := _ : _ |- _ ] => | |
try clearbody f; | |
revert f | |
| [ f : _ |- _ ] => revert f | |
| _ => idtac "it had better be true!" end; | |
match goal with | |
| |- forall x, @?T x => let g := fresh "f" in | |
pose (g := T) ; intros | |
| _ => idtac "i'm confused" end. | |
Ltac dependOnLastTwo := | |
try match goal with | |
| [ f : _ , gf : _ |- _ ] => | |
try clearbody gf; try clearbody f; | |
revert f gf | |
| _ => idtac "maybe there's only one?" | |
end; | |
match goal with | |
| |- forall x, forall y, @?T x y => | |
let h := fresh "fTwo" in | |
pose ( h := T ) ; intros | |
| _ => idtac "i'm confused." | |
end. | |
Ltac remember_as thing name := | |
let H := fresh name | |
with Heq := fresh name "_eq" in | |
set ( H := thing ) in * ; | |
assert ( Heq := idpath : H = thing ); | |
clearbody H. |
In the latest revision, exploit coq's magic Coercion engine to enable really tidy notations for lists of Booleans. Of course, you could do the same for nearly any type in the place of Bool, but I don't think I recommend it. This will break scripts actually using subTermOf, but translating them isn't hard.
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
It Occurs to me that one could use division by 10 instead of by 2, and then write binary-looking numbers in base 10 and it wouldn't make much difference, except perhaps the vm_compute would run slower. Or Something.
NEWS turns out, working base-10 actually leads to STACK OVERFLOW. Bah, thou Unary Naturals Notations!