Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Re: Ltac automation.

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Re: Ltac automation.


chronological Thread 
  • From: Tom Prince <tom.prince AT ualberta.net>
  • To: Coq Club <coq-club AT inria.fr>
  • Subject: [Coq-Club] Re: Ltac automation.
  • Date: Sat, 12 Feb 2011 23:00:16 -0500
(* I managed to come up with a couple of solutions to my automation
problem *)

(******** SETUP ***)
Inductive Term :=
  | Var: nat → Term
  | Op: Term → Term → Term.

Fixpoint eval_term {A: Type} (op: A → A → A) (var: nat → A) (t: Term) :=
  match t with
    | Var n => var n
    | Op x y => op (eval_term op var x) (eval_term op var y)
  end.

Inductive Equal := Eq: Term → Term → Equal.

Fixpoint eval_eq {A: Type} (op: A → A → A) (var: nat → A) (e: Equal) :=
  let (x, y) := e in (eval_term op var x) = (eval_term op var y).

Inductive Laws : Equal -> Prop :=
  | law_1 : Laws (Eq (Var 0) (Op (Var 0) (Var 1)))
  | law_2 : Laws (Eq (Op (Var 0) (Var 0)) (Op (Var 1) (Var 0))).

Axiom (A: Type).
Axiom (op: A→A→A).

Definition laws_true_type := λ {E} (_: Laws E), ∀ x y, eval_eq op (fun n => 
match n with | 0 => x | _ => y end) E.
Axiom (laws_true: ∀ {E} (laws: Laws E), laws_true_type laws).

Record rec (A: Type) (op: A→A→A) := { m1 : ∀ x y, x = (op x y) ; m2: ∀ x y, 
(op x x) = (op y x) }.
(******** END ***)

(* Here is the manual solution to the problem *)
Goal rec A op.
constructor; [apply (laws_true law_1) | apply (laws_true law_2)].
Defined.

(* Now, I know each of the goals can be solved by applying laws_true to
a constructor, so I wanted to figure out how to refer to constuctors by
number, so I could iterate over them: *)
Goal rec A op.
constructor.
let n:= fresh in (evar (n:Equal); assert (Laws n) as P; subst n; [ 
constructor 1 | apply (laws_true P)]).
let n:= fresh in (evar (n:Equal); assert (Laws n) as P; subst n; [ 
constructor 2 | apply (laws_true P)]).
Defined.

(* Then I ran into problems trying to iterate.
   - the constructor tactic only takes numbers, not ltac variables bound
     to numbers 
(http://www.lix.polytechnique.fr/coq/bugs/show_bug.cgi?id=2496)
   - you can do arithmetic with and matching with numbers represented as
     coq terms, but you can't then pass those numbers to tactics
     expecting numbers like constructor or do.
     
   I created patches for both these issues; although the second should
   probably do more sanity checking to insure the term is actually meant
   to be a number.
   
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 917a98c..fb454d9 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1046,8 +1046,41 @@ let interp_hint_base ist s =
   try try_interp_ltac_var coerce_to_hint_base ist None (dloc,id_of_string s)
   with Not_found -> s
 
+(**** BEGIN: copied from plugins/syntax_nat_syntax.ml and plugins/micromega/coq_micromega.ml ******)
+exception Non_closed_number
+
+let get_left_construct term =
+        match Term.kind_of_term term with
+        | Term.Construct(_,i) -> (i,[| |])
+        | Term.App(l,rst) ->
+                        (match Term.kind_of_term l with
+                        | Term.Construct(_,i) ->
+                                        (i,rst)
+                        | _ -> raise Non_closed_number)
+        | _ ->   raise Non_closed_number
+let rec parse_nat term =
+        let (i,c) = get_left_construct term in
+        match i with
+        | 1 -> 0
+        | 2 -> 1 + (parse_nat (c.(0)))
+        | i -> raise Non_closed_number
+
+let uninterp_nat p =
+  try
+    Some (parse_nat p)
+  with
+    Non_closed_number -> None
+(**** END: copied from plugins/syntax_nat_syntax.ml and plugins/micromega/coq_micromega.ml ******)
+
 let coerce_to_int = function
   | VInteger n -> n
+  | VConstr ([], c) ->
+        try
+          match uninterp_nat c with
+          | Some n -> n
+          | None -> raise (CannotCoerceTo "an integer")
+        with
+          Non_closed_number -> raise (CannotCoerceTo "an integer")
   | v -> raise (CannotCoerceTo "an integer")
 
 let interp_int ist locid =

   Thus, the following code works.
*)
Goal rec A op.
Tactic Notation "do_with_nat" constr(n) tactic(T) := let rec LOOP n := match 
n with S ?n' => T n || LOOP n' end in LOOP n.
constructor; do_with_nat 2 fun k => let n:= fresh "n" in (evar (n:Equal); 
assert (Laws n) as P; subst n); [ constructor k | apply (laws_true P) ].
Defined.

(* But, it would be nice avoid the contusions required above. So I
   pieced together two tactics in ML, that do exactly what I need.
Caml1999M0127plugins/intro/intro.ml4PhS=<砠"Pp7plugins/intro/intro.ml4CkkCkr@$Pcoq
        Dss
Ds|@&GenargE}}E}H@)ExtraargsFIIFIW@)Mod_subst!GXX"GXf@%Names)Hgg*Hgq@'Tacexpr1Irr2Ir~@)Glob_term9J:J@'TacticsAKBK@$UtilILJL@#EvdQMRM@(EqualityYNZN@&CompataObO@'RefineriPjP@'TacmachqQrQ@@"ic|T}T@
 
@!cTT@@#envU
 
U#@&Global#envU&U0@
 
"()@@U0U2@@U&U2@%sigmaU7U<@#Evd%emptyU?UH@@,Constrintern-interp_constrVLNVLh@)%sigmaVLiVLn@2#envVLoVLr@;!cVLsVLt@@VLNVLt@UUt@@TTt@@TTt@@"tyXvzXv|@{@!cXv}Xv~@&Typing'type_of
Xv
Xv@p&Global#envXvXv@}|@@!Xv"Xv@@$Xv%Xv@#Evd%empty/Xv0Xv@!c8Xv9Xv@@;Xv<Xv@@>Xv}?Xv@@AXvvBXv@@)ltac_callL[M[@@#tacV[W[@@$argsb[c[@$list/glob_tactic_arg@n[o[@@q[r[@t[u[@&TacArg'TacCall)dummy_loc\ \@&ArgArg)dummy_loc\\&@$Lazy%force\(\2@#tac\3\6@@\(\6@@\\7@@\\7@$args\8\<@@\\=@@\\=@@\\>@@[[>@@[[>@@[[>@@*ltac_lcall_ei_es@_@#tac_et_ew@i@$args_ex_e|@&TacArg'TacCall)dummy_loc``@&ArgVar)dummy_loc``@,id_of_string``@#tac&`'`@@)`*`@@,`-`@@/`0`@$args7`8`@@:`;`@@=`>`@@@`A`@@C_exD_e@@F_etG_e@@I_eeJ_e@@*ltac_letinTbUb@@!xabbb@"e1hbib@@kblb@@"e2ubvb@(TacLetIn%false@@cc@"::)dummy_loccc@,id_of_stringcc
@!xc
c@@cc@@cc@"e1cc@@cc@"[]@@cc@@cc@@cc@"e2cc@@cc@@cc@@bb@@bb@@bb@@*ltac_applyee'@r@!fe)e*@0glob_tactic_expr@e+e;@e(e<@@$argse>eB@$list/glob_tactic_arg@eCeR@@eC
 
eW@"e=#eX@)Tacinterp+eval_tactic-f[].f[r@*ltac_letin8gsx9gs@!FDgsEgs@&Tacexp!fQgsRgs@@TgsUgs@@WgsXgs@*ltac_lcallbgscgs@Ơ!Fkgslgs@Ϡ$argstgsugs@@wgsxgs@@zgsx{gs@@}f[]~f[@@e=e@@e(e@@ee@@+ltac_recordii@@$fldsii@&TacFun$Some,id_of_stringjj@$projjj@@jj@@jj@
    
@@jj@@jj@@jj@*ltac_lcalljj@B$projjj@K$fldsjj@@jj@@jj@@jj@@ii@@ii@@$carg
m m       
@@!cm
m @*TacDynamic)dummy_loc#m$m"@)Pretyping)constr_in/m#0m6@!c8m79m8@@;m#<m8@@>m?m9@@AmBm9@@Dm
Em9@@GmHm9@,DeclarationsOqMMPqM^@$TermWr__Xr_h@@*map_constrbtjnctjx@@!cltjymtjz@@#tacvtj{wtj~@@"gltjtj@@$minduu@%redcluu@@uu@;pf_reduce_to_quantified_induu@"gluu@
!cuu@@uu@@@'nconstrvv@%Array&lengthvv@.#sndvv@;&Global0lookup_inductivevv@H$mindvv@@vv@@vv@.mind_consnamesvv
@@vv
@@@$consww@$List#mapww&@t@!iw,w-@+mkConstruct%w1&w<@<ith_constructor_of_inductive0w>1wZ@$mind9w[:w_@!iBw`Cwa@@Ew>Fwa@@Hw1Iwb@@Kw(Lwb@(intervalVxdmWxdu@A^xdv_xdw@ 'nconstrgxdxhxd@@jxdmkxd@@mwnw@@$List#mapxyyy@ܠ@!cyy@*ltac_applyyy@񠐐#tacyy@$cargyy@

!cyy@@yy@@@yy@@yy@@yy@@yy@@yy@+$consyy@@yy@ww@vv@uu@@tjtj@@tj{tj@@tjytj@@tjjtj@@/try_with_constr{{@w@!c{{@@#tac{{@@"gl{{@(tclFIRST||@~*map_constr%|&|@!c.|/|@#tac7|8|@"gl@|A|@@C|D|@"glL|M|@@O|P|@@R{S{@@U{V{@@X{Y{@@[{\{@@/for_each_constrf~g~@@!cp~q~@@#tacz~{~@@"gl~~@+tclTHENLIST"-@񠤠*map_constr/9@!c:;@#tac<?@"gl@B@@/B@"glEG@@!G@@~~G@@~~G@@~~G@@~~G@@1h_try_with_constrAIIAI@]@!cBgBg@g@#tacBgBg@'Refiner8abstract_extended_tacticAIIAI@\/try_with_constr
 
@@@@Af"::&Genarg&in_genBgBg@{&Genarg*wit_constr"Bg#Bg@!c+Bg,Bg@@.Bg/Bg@+*)?Bg@Bg@

#WIT(ExtrawitNBgOBg@@#witYBgZBg@+wit_tactic5`BgaBg@@cBgdBg@@fBggBg@#WIT#witoBgpBg@rBgsBg@֠#tac{Bg|Bg@@~BgBg@"[]@@@@@@A@BgBg@@BgBg@@BgBg@@BgBg@@#tacBgBg@BgBg@@/try_with_constrBgBg@!cBgBg@#tacBgBg@@BgBg@BgBg@@AIIAI@@BgBg@@BgBg@@AIIAI@@@AIIAI@)Tacinterp*add_tacticAIIAI@O/try_with_constr@@@@AXz@"::!c@@@@A#tac@@@@A"[]@@@@@@A@
 
@@!@@A@#@@$@@A@&@@'@@A@)@@*@@A"&&5Bg6Bg@!=@BgABg@&Genarg*genarg_tagMBgNBg@!cVBgWBg@@YBgZBg@&Genarg-ConstrArgType@@dBgeBg@@gBghBg@ˠ=qBgrBg@ՠ<{Bg|Bg@ߠ;:BgBg@ꠐ#tacBgBg@@BgBg@&Genarg,ExtraArgType'tactic5BgBg@@BgBg@@BgBg@

$true@@BgBg@@BgBg@@BgBg@@!cBgBg@&Genarg'out_genBgBg@0BgBg@9BgBg@@BgBg@@@#tacBgBg@)(BgBg@W
        Bg     
Bg@@
   
Bg      
Bg@+wit_tactic5
       Bg     Bg@@  Bg     Bg@@  
Bg     
Bg@
    Bg     
Bg@
      !Bg     
"Bg@@
    )Bg     *Bg@@  ,Bg     -Bg@@  
4Bg     
5Bg@
   <Bg     
=Bg@
   DBg     EBg@@  GBg     
HBg@
      JBg     
KBg@
      MBg     
NBg@
      PBg     
QBg@@
  VAII     
WAI@(failwith
        _AII     
`AI@à7Extension:
 cannot occur      hAII     iAI@@  kAII     
lAI@@  nAII     oAI@@  qAII     
rAI@@$List$iter  |AII     
}AI@࠳
 
@!s
        AII     
AI@)Tacinterp4add_primitive_tactic
 AII     
AI@!s
    AII     
AI@
      
'Tacexpr'TacAtom$Util)dummy_loc@@@@A'Tacexpr)TacExtend@@@@A!s
    AII     
AI@"[]@@
     AII     AI@@  AII     AI@@  
AII     AI@@  AII     AI@@  AII   
  AI@@  AII     AI@@  AII     
AI@
      
I"[]@@@@@@A@
    AII     
AI@
      AII     
AI@!e
        AII     
AI@"Pp"pp
AII
AI@
      k'Cerrors+explain_exn
AII
AI@
      x!e
AII
AI@@
 AII
!AI@@
#AII
$AI@@
&AII
'AI@(Egrammar5extend_tactic_grammar
3AII
4AI@
      /try_with_constr;@@<@@A       
"::(Egrammar,GramTerminal/try_with_constrZ@@[@@A@]@@^@@A!(Egrammar/GramNonTerminalǰv@@w@@A@@
Bg
Bg@$Pcoq&Aentry&constr@@@@A&constr@@@@A@@@@@A@@@@@A$Some%Names,id_of_string@@@@A
!c@@@@A@@@@@A@@@@@A@
Bg
Bg@@
Bg
Bg@gf-,@@@@AIH'tactic5
Bg
Bg@@
Bg
Bg@ml&tactic@@@@A&tactic@@@@A@@@@@A@
 @@
@@Akji@@@@A
|#tac 
@@!@@A@#@@$@@A@&@@'@@A@ *Bg +Bg@@ -Bg .Bg@G@@3@@4@@A@ 7Bg@ 8Bg@@ :Bg@ ;Bg@@ =Bg@ >Bg@@ @Bg@ ABg@@B@@C@@@E@@F@@`@@L@@M@@A@O@@P@@@R@@S@@@ VAII WAI@$List$iter aAII bAI@
Š(Pptactic;declare_extra_tactic_pprule lAII mAI@
Р0/try_with_constr~@@@@A"::-,@@ Bg Bg@'tactic5 Bg Bg@@ Bg Bg@"[]@@ Bg Bg@@ Bg Bg@@ Bg Bg@@ Bg Bg@@ Bg Bg@@@@@@A$Some/try_with_constr@@@@A@@@@@A$None@@ Bg Bg@@@ Bg Bg@@@@@@@A@

Bg@
Bg@@
Bg@
Bg@@
Bg@
 Bg@@
Bg@
Bg@@
@@@@@@@@@@
Bg Bg@@ Bg
Bg@1@@@@@@A@

!Bg@
"Bg@@
$Bg@
%Bg@@ 'AII
(AI@
*AII
+AI@
-AII
.AI@
0AII
1AI@@1h_for_each_constr
;D
<D&@ @!c
EE
FE@ @#tac
OE
PE@ba
XD
YD&@ /for_each_constr`@@a@@A Š_^]
sE
tE@ נ\[
|E
}E@ ࠐ!c
E E@@ E
E@
E
E@ 
ZY E
E@@X
E
E@+wit_tactic5
E E@@ E E@@ E
E@WV
E
E@
E
E@
+#tac E E@@ E
E@U@@@@@@A@
E E@@ E E@@ E
E@@ E
E@

J@#tac
E E @ E E 
@@/for_each_constr
E 
E@
e!c

E
E@
n#tac
E
E @@
E 
E @
E
E @@
D
D&@@
E
 E@@
"E
#E@@
%D
&D&@@@
4D
5D&@TS
=D
>D&@ /for_each_constrE@@F@@A 
>@R!cX@@Y@@A`#tacf@@g@@AQ@@m@@n@@A@p@@q@@A@s@@t@@A@v@@w@@A@y@@z@@AP
E
E @ 蠤O
E
E @ 򠤠NM
E
E @ !c
E
E @@
E
E @
        LK@@
E
E@@
E
E @

E
E @

E
E @
)
E
E @
4#tac
E
E @@
E
E @
@JI'tactic5
E
E@@
E
E@@
E
E @
TH@@
E 
E @@
E
E @@
E
E 
@@!cE
        E @GFEE @
uEE @
~"E#E @@%E&E 
@@@#tac/E0E
 @nm8E9E @
 EEFE 
@@OEPE
 @+wit_tactic5VEWE @@YEZE 
@@\E]E @cEdE 
@fEgE @
ʠ@nEoE
 @@qErE 
@@yyE zE@
ݠxEE@
堐wEE @@E E 
@EE @EE @EE 
@@DD&@EDD&@7Extension:
 cannot 
occurDD&@@DD&@@DD&@@DD&@@DCDD&@"D@BDD&@A@DD&@6?DD&@>>=<;@@@@A:9LK@@@@A8DD&@7@@
      D
D&@@ D
D&@@DD&@@DD&@@DD&@@DD&@@DD&@6@@"@@#@@A@&D'D&@)D*D&@50D1D&@439D:D&@21DDED&@0LDMD&@@ODPD&@@RDSD&@@UDVD&@/.`DaD&@Ġ/for_each_constrh@@i@@A͠-4,+/for_each_constr@@@@A@@@@@AK*)@@@@AED@@EE@('&constr@@@@A&constr@@@@A@@@@@A@@@@@A&%$@@@@A7!c@@@@A@@@@@A@@@@@A@EE@@EE@PO@@@@Alk'tactic5
E
E@@EE@&tactic
   @@ @@A&tactic    &@@ 
'@@A@
 )@@ 
*@@A@
 ,@@ -@@A   :@@ ;@@A#tac   
C@@ 
D@@A@
 F@@ 
G@@A@
 I@@ 
J@@A@MENE@@PEQE@j@@
      V@@ 
W@@A@ZE@[E@@]E@^E@@`E@aE@@cE@dE@@
      e@@ 
f@@@
       h@@ 
i@@@@
       o@@ 
p@@A@
 r@@ 
s@@@
       u@@ 
v@@@yDzD&@#"DD&@栐!
 DD&@O/for_each_constr @@ 
@@AKJ@@EE@.!
 
'tactic5EE@@EE@@@E E
 @@EE @@EE 
@@EE @@EE 
@@
  @@ @@A/for_each_constr  @@ 
@@A@
 @@ 
@@A@@EE@Ȑ*@@EE@-@@
@@
@@A@E@E@@
 
E@!E@@#E@$E@@&E@'E@@
(@@
)@@@
+@@
,@@@/E 0E
 @@2E 3E @L@@
8@@
9@@A@<E@=E
 
@@?E@@E
 
@@BDCD&@EDFD&@HDID&@KDLD&@@
   That is, iterating over constructors. 

   for_each_constr Inductive TAC => TAC constr_1; TAC constr_2; ...; TAC 
constr_n
   try_each_constr Inductive TAC => first [ TAC constr_1| TAC constr_2| ...| 
TAC constr_n ]
*)

Declare ML Module "intro".

Goal rec A op.
for_each_constr Laws fun c => (idtac c;pose (laws_true c)).
constructor; auto.
Defined.

Goal rec A op.
constructor; try_with_constr Laws fun c => apply (laws_true c).
Defined.

Archive powered by MhonArc 2.6.16.

Top of Page