diff --git a/LibHyps/Especialize.v b/LibHyps/Especialize.v index 499aa71..8c15c92 100644 --- a/LibHyps/Especialize.v +++ b/LibHyps/Especialize.v @@ -1,109 +1,16 @@ -From Stdlib Require Import String. -(* Require ident_of_string. *) Require Import Ltac2.Ltac2. From Ltac2 Require Import Option Constr Printf. Import Constr.Unsafe. -(* Declare Scope specialize_scope. *) -(* Delimit Scope specialize_scope with spec. *) -(* Local Open Scope specialize_scope. *) -Require IdentParsing. - -From Stdlib Require Import String Ascii. -Open Scope string_scope. Local Set Default Proof Mode "Classic". +(* Require Import LibHyps.LibHypsDebug. *) -(* The type describing how to specialize the arguments of a hyp. Premises are either -- transformed into a sub goal -- transformed into an evar -- requantified (default). *) -Inductive spec_arg : Type := - (* This 4 are meant to be put in a exhaustive list of what to do - with args in order. The others are actually transformed into these - ones on the fly *) - Quantif | QuantifIgnore | SubGoal | Evar: string -> spec_arg -| SubGoalAtName: string -> spec_arg (* make a subgoal with named arg *) -| SubGoalAtNum: nat -> spec_arg (* make a subgoal with arg's number *) -| EvarAtName: string -> string -> spec_arg (* make an evar with the named arg. *) -| SubGoalUntilNum: nat -> spec_arg (* make subgoals with all non dep hyp until nth one. *) -| SubGoalAtAll: spec_arg. (* make subgoals with all non dep hyp. *) - -Definition spec_args := list spec_arg . - -(* List storing heterogenous terms, for storing telescopes. A simple - product could also be used. *) -(* -Inductive Depl := -| DNil: Depl -| DCons: forall (A:Type) (x:A), Depl -> Depl. -*) - -(* if H head product is dependent, call tac1, else call tac2 *) -Ltac if_is_dep_prod H tac1 tac2 := - (* tryif is_dep_prod H then ltac:(tac1) else ltac:(tac2). *) - let t := type of H in - match goal with - | |- _ => match goal with - | |- _ => assert t; - let h := fresh "__h__" in - intro h; - (tryif clear h then fail else fail 1) (* we fail in both cases to backtrack the assert*) - | |- _ => tac2 - | |- _ => fail 2 (* don't fall back to tac1 *) - end - | |- _ => tac1 +(* Utilities *) +Local Ltac2 is_dep_prod (t:constr): bool := + match kind t with + | Prod _ subt => Bool.neg (is_closed subt) + | _ => false end. -Ltac2 rec length_constr_string (xs : constr) : int := - match kind xs with - | App _ args => - match Int.equal (Array.length args) 2 with - | true => Int.add 1 (length_constr_string (Array.get args 1)) - | _ => if equal xs 'String.EmptyString then 0 else Control.throw No_value - end - | Constr.Unsafe.Constructor _ _ => 0 - | _ => Control.throw No_value - end. - -Ltac2 string_of_constr_string (s : constr) : string := - let s := eval vm_compute in ($s : String.string) in - let ret := String.make (length_constr_string s) (Char.of_int 0) in - let t := constr:(true) in - let rec fill i s := - (match kind s with - | App _ args => - (if Int.equal (Array.length args) 2 then - (String.set ret i (match kind (Array.get args 0) with App _ b => Char.of_int ( - Int.add (if equal (Array.get b 0) t then 1 else 0) ( - Int.add (if equal (Array.get b 1) t then 2 else 0) ( - Int.add (if equal (Array.get b 2) t then 4 else 0) ( - Int.add (if equal (Array.get b 3) t then 8 else 0) ( - Int.add (if equal (Array.get b 4) t then 16 else 0) ( - Int.add (if equal (Array.get b 5) t then 32 else 0) ( - Int.add (if equal (Array.get b 6) t then 64 else 0) ( - (if equal (Array.get b 7) t then 128 else 0))))))))) - | _ => Control.throw No_value end); - fill (Int.add i 1) (Array.get args 1)) - else ()) - | _ => () - end) in - fill 0 s; - ret. - -Ltac if_eqstr := - ltac2:(ident s tac1 tac2 |- - (if String.equal - (Ident.to_string (Option.get (Ltac1.to_ident ident))) - (string_of_constr_string (Option.get (Ltac1.to_constr s))) - then Ltac1.apply tac1 [] - else Ltac1.apply tac2 []) Ltac1.run). - -Ltac2 ident_of_constr_string (s : constr) := Option.get (Ident.of_string (string_of_constr_string s)). - -Ltac ident_of_constr_string_cps := ltac2:(s tac |- - Ltac1.apply tac [Ltac1.of_ident (ident_of_constr_string (Option.get (Ltac1.to_constr s)))] Ltac1.run). - -Ltac evar_as_string s t := ident_of_constr_string_cps s ltac:(fun s => let s' := fresh s in evar(s':t)). - (* ESPECIALIZE INTERNAL DOC *) (* We show here by hand what the especialize tactic does. We start @@ -159,208 +66,297 @@ Proof. been specialized. *) Abort. -(* debug *) -(*Require Import LibHyps.LibHypsTactics. -Module Prgoal_Notation. - Ltac pr_goal := - match goal with - |- ?g => - let allh := harvest_hyps revert_clearbody_all in - (* let allh := all_hyps in *) - idtac "GOAL: " allh " ⊢ " g - end. -End Prgoal_Notation. +Local Ltac2 Type directarg := [ Quantif | QuantifIgnore | SubGoal | Evar(ident) ]. +Local Ltac2 Type namearg := [ + SubGoalAtName(ident) (* make a subgoal with named arg *) + | EvarAtName(ident,ident) (* make an evar with the named arg. *) +]. +Local Ltac2 Type numarg := [ + | SubGoalAtNum(int) (* make a subgoal with arg's number *) + | SubGoalUntilNum(int) (* make subgoals with all non dep hyp until nth one. *) + | SubGoalAtAll (* make subgoals with all non dep hyp. *) + ]. -Local Ltac2 tag_info s := (String.concat "" [ ""; s; "" ]). -Local Ltac2 tag_msg m := Message.concat - (Message.concat (Message.of_string "") m) - (Message.of_string ""). -Local Ltac2 str_to_msg s := tag_msg (Message.of_string s). -Local Ltac2 int_to_msg i := tag_msg (Message.of_int i). -Local Ltac2 id_to_msg id := tag_msg (Message.of_ident id). -Local Ltac2 constr_to_msg c := tag_msg (Message.of_constr c). -Local Ltac2 msgs s := Message.print (str_to_msg s). -Local Ltac2 msgi i := Message.print (int_to_msg i). -Local Ltac2 msgc c := Message.print (constr_to_msg c). -Local Ltac2 msgid id := Message.print (id_to_msg id). +Local Ltac2 pr_numarg () a := + match a with + | SubGoalAtNum(i) => fprintf "SubGoalAtNum(%i)" i + | SubGoalUntilNum(i) => fprintf "SubGoalUntilNum(%i)" i + | SubGoalAtAll => fprintf "SubGoalAtAll" + end. +Local Ltac2 pr_directarg () a := + match a with + | Quantif => fprintf "Quantif" + | QuantifIgnore => fprintf "QuantifIgnore" + | SubGoal => fprintf "SubGoal" + | Evar(id) => fprintf "Evar(%I)" id + end. -Ltac2 pr_binder () (b:binder) := - let nme:ident option := Binder.name b in - let typ:constr := Binder.type b in - fprintf "(%I:%t)" (Option.get nme) typ. -*) -(* This performs the refinement of the current goal by mimicking h and - making evars and subgoals according to args. n is the number of - dependent product we have already met. *) -Ltac refine_hd_OLD h largs n := - let newn := if_is_dep_prod h ltac:(constr:(n)) ltac:(constr:(S n)) in - (* let newn := tryif is_dep_prod h then constr:(n) else constr:(S n) in *) - lazymatch largs with - | nil => exact h - | _ => - lazymatch type of h with - | (forall (h_premis:?t) , _) => - let id := ident:(h_premis) in (* ltac hack, if the product was not named, - then "h_premis" is taken "as is" by fresh *) - let intronme := (*fresh*) id in - lazymatch largs with - | nil => exact h - | cons Quantif ?largs' => - refine (fun intronme: t => _); - specialize (h intronme); - refine_hd_OLD h largs' newn - | cons QuantifIgnore ?largs' => - (* let intronme := fresh x in *) - refine (fun intronme: t => _); - specialize (h intronme); - clear h_premis; - refine_hd_OLD h largs' newn - | cons (SubGoalAtName ?nme) ?largs' => - if_eqstr ident:(h_premis) nme - ltac:(idtac;refine_hd_OLD h (cons SubGoal largs') n) - ltac:(idtac;refine_hd_OLD h (cons Quantif largs) n) - | cons (EvarAtName ?nmearg ?nameevar) ?largs' => - if_eqstr ident:(h_premis) nmearg - ltac:(idtac;refine_hd_OLD h (cons (Evar nameevar) largs') n) - ltac:(idtac;refine_hd_OLD h (cons Quantif largs) n) - | cons (SubGoalAtNum ?num) ?largs' => - if_is_dep_prod h - ltac:((idtac;refine_hd_OLD h (cons Quantif largs) n)) - ltac:(idtac;tryif convert num newn - then refine_hd_OLD h (cons SubGoal largs') n - else refine_hd_OLD h (cons Quantif largs) n) - | cons (SubGoalUntilNum ?num) ?largs' => - if_is_dep_prod h - ltac:((idtac;refine_hd_OLD h (cons Quantif largs) n)) - ltac:(idtac;tryif convert num newn - then refine_hd_OLD h (cons SubGoal largs') n - else refine_hd_OLD h (cons SubGoal largs) n) - | cons (Evar ?ename) ?largs' => - evar_as_string ename t; - (* hackish: this should get the evar just created *) - let hename := match goal with H:t|-_ => H end in - specialize (h hename); - subst hename; - (* idtac "subst"; *) - refine_hd_OLD h largs' newn - | cons SubGoal ?largs' => - (unshelve evar_as_string "SubGoal" t); - (* hackish: this should get the evar just created *) - [ | let hename := match goal with - H:t|-_ => H - end in - specialize (h hename); - clearbody hename; - (* idtac "subst"; *) - refine_hd_OLD h largs' newn] - end - | _ => idtac "Not enough products." (*; fail*) - end +Local Ltac2 pr_namearg () a := + match a with + | SubGoalAtName id => fprintf "SubGoalAtName(%I)" id + | EvarAtName id1 id2 => fprintf "EvarAtName(%I,%I)" id1 id2 end. +(* +Goal True. + ltac2:(printf "%a" pr_namearg (SubGoalAtName @toto)). + ltac2:(printf "%a" (pr_list pr_namearg) ([SubGoalAtName @toto; EvarAtName @titi1 @titi2])). +*) -Ltac refine_hd h ldirectarg lnameargs lnumargs n := - let th := type of h in - let newn := if_is_dep_prod h ltac:(constr:(n)) ltac:(constr:(S n)) in - (* idtac "REFINE_HD: " th; *) - (* idtac " " h "ldirect:" ldirectarg " , lnames:" lnameargs " , lnums" lnumargs; *) - (* let newn := tryif is_dep_prod h then constr:(n) else constr:(S n) in *) - match constr:((ldirectarg,lnameargs,lnumargs)) with - | (nil,nil,nil) => exact h - | (cons ?directarg ?ldirectarg',_,_) => - lazymatch type of h with - | (forall (h_premis:?t) , _) => - let intronme := ident:(h_premis) in (* ltac hack, if the product was not named, - then "h_premis" is taken "as is" by fresh *) - match directarg with - | Quantif => - refine (fun intronme: t => _); - specialize (h intronme); - refine_hd h ldirectarg' lnameargs lnumargs newn - | QuantifIgnore => - (* let intronme := fresh x in *) - refine (fun intronme: t => _); - specialize (h intronme); - clear h_premis; - refine_hd h ldirectarg' lnameargs lnumargs newn - | Evar ?ename => - evar_as_string ename t; - (* hackish: this should get the evar just created *) - let hename := match goal with H:t|-_ => H end in - specialize (h hename); - subst hename; - refine_hd h ldirectarg' lnameargs lnumargs newn - | SubGoal => - (unshelve evar_as_string "SubGoal" t); - (* hackish: this should get the evar just created *) - [ | let hename := match goal with - H:t|-_ => H - end in - specialize (h hename); - clearbody hename; - refine_hd h ldirectarg' lnameargs lnumargs newn ] - end - | _ => fail 1 - end - | (nil,cons ?namearg ?lnameargs',_) => - lazymatch type of h with - | (forall (h_premis:?t) , _) => - let intronme := ident:(h_premis) in (* ltac hack, if the product was not named, - then "h_premis" is taken "as is" by fresh *) - lazymatch namearg with - | (SubGoalAtName ?nme) => - if_eqstr ident:(h_premis) nme - ltac:(idtac;refine_hd h (cons SubGoal nil) lnameargs' lnumargs n) - ltac:(fail 0) - | (EvarAtName ?nme ?nameevar) => - if_eqstr ident:(h_premis) nme - ltac:(idtac;refine_hd h (cons (Evar nameevar) nil) lnameargs' lnumargs n) - ltac:(fail 0) - end - | _ => fail 0 - end - | (nil,_,cons ?numarg ?lnumargs') => - lazymatch type of h with - | (forall (h_premis:?t) , _) => - let intronme := ident:(h_premis) in (* ltac hack, if the product was not named, - then "h_premis" is taken "as is" by fresh *) - match numarg with - | (SubGoalAtNum ?num) => - if_is_dep_prod h - ltac:(fail 0) - ltac:(idtac; - tryif convert constr:(PeanoNat.Nat.leb newn num) constr:(true) - then - tryif convert num newn - then refine_hd h (cons SubGoal nil) lnameargs lnumargs' n - else (fail 3) - else - (fail 10000 "Did you not order the evar numbers?")) - | (SubGoalUntilNum ?num) => - if_is_dep_prod h - ltac:(fail 0) - ltac:(idtac;tryif convert num newn - then refine_hd h (cons SubGoal nil) lnameargs lnumargs' n - else refine_hd h (cons SubGoal nil) lnameargs lnumargs n) - | SubGoalAtAll => - if_is_dep_prod h - ltac:(fail 0) - ltac:(idtac; refine_hd h (cons SubGoal nil) lnameargs lnumargs n) + + +Local Ltac2 backtrack (msg:string) := Control.zero (Tactic_failure (Some (fprintf "Backtrack: %s" msg))). +Local Ltac2 invalid_arg (msg:string) := Control.throw (Invalid_argument (Some (Message.of_string msg))). + +Local Ltac2 mk_evar ename typ := + let tac := ltac1:(ename typ|- evar (ename:typ)) in + tac (Ltac1.of_ident ename) (Ltac1.of_constr typ). + +Local Ltac2 assert_evar nme := + let tac := ltac1:(nme |-let ev1 := open_constr:(_) in assert ev1 as nme) in + tac (Ltac1.of_ident nme). + + +Local Ltac2 intro_typed (name:ident) (typ:constr) := + let tac := ltac1:(name typ |- refine (fun (name:typ) => _)) in + tac (Ltac1.of_ident name) (Ltac1.of_constr typ). + +Local Ltac2 specialize_id_id (h:ident) (arg:ident) : unit := + let newhyp := Control.hyp arg in + let hc:constr := Control.hyp h in + let special := Unsafe.make (Unsafe.App hc [|newhyp|]) in + Std.specialize (special , Std.NoBindings) None. + +Local Ltac2 specialize_id_cstr (h:ident) (c:constr) : unit := + let hc:constr := Control.hyp h in + let special := Unsafe.make (Unsafe.App hc [|c|]) in + Std.specialize (special , Std.NoBindings) None. + + +(* Local Ltac2 pr_debug (h:ident) (ldirectarg:directarg list) (lnameargs:namearg list) *) +(* (lnumargs:numarg list) (n:int) := *) +(* let hc := Control.hyp h in *) +(* let th := Constr.type hc in *) +(* LibHyps.LibHypsDebug.msgs "--------------"; *) +(* (* LibHyps.dev.LibHypsDebug.pr_goal(); *) *) +(* printf "n = %i ; th = %t" n th; *) +(* printf "lnumargs = %a" (pr_list pr_numarg) lnumargs; *) +(* printf "lnameargs = %a" (pr_list pr_namearg) lnameargs; *) +(* printf "ldirectarg = %a" (pr_list pr_directarg) ldirectarg. *) + + +Local Ltac2 rec refine_hd (h:ident) (ldirectarg:directarg list) (lnameargs:namearg list) + (lnumargs:numarg list) (n:int) := + (* pr_debug h ldirectarg lnameargs lnumargs n; *) + let hc := Control.hyp h in + let th := Constr.type hc in + let newn := if is_dep_prod th then n else (Int.add n 1) in + (* msgc th; *) + match Unsafe.kind th with + | Prod _ _ => + match ldirectarg with + | directarg::ldirectarg' => + match Unsafe.kind th with + | Prod bnd _ => + let h_premis := Constr.Binder.name bnd in + let typ_premis := Constr.Binder.type bnd in + let intronme:ident := + match h_premis with + None => Option.get (Ident.of_string "h_premis") + | Some idh => idh + end in + match directarg with + | Quantif => + intro_typed intronme typ_premis; + specialize_id_id h intronme; + refine_hd h ldirectarg' lnameargs lnumargs newn + | QuantifIgnore => + intro_typed intronme typ_premis; + specialize_id_id h intronme; + clear $intronme; + refine_hd h ldirectarg' lnameargs lnumargs newn + | Evar ename => + let ename := Fresh.in_goal ename in + mk_evar ename typ_premis; + (* let tac := ltac1:(ename typ_premis|- evar (ename:typ_premis)) in *) + (* tac (Ltac1.of_ident ename) (Ltac1.of_constr typ_premis) ; *) + specialize_id_id h ename; + subst $ename; + refine_hd h ldirectarg' lnameargs lnumargs newn + | SubGoal => + let gl := Fresh.in_goal @h in (* this uses base name "h" *) + (unshelve (epose (_:$typ_premis) as $gl)) > + [ | + let special := Control.hyp gl in + specialize_id_cstr h special; + refine_hd h ldirectarg' lnameargs lnumargs newn ] + end + | _ => invalid_arg "Not a product (directarg)" + end + | _ => + (* If this succeeds, never go back here from later backtrack. *) + Control.once + (fun () => Control.plus + (fun() => refine_hd_name h lnameargs lnumargs n) + (fun _ => + (* msgs "Backtracking from refine_hd_name "; *) + Control.plus + (fun () => refine_hd_num h lnameargs lnumargs n) + (fun _ => + (*msgs "Backtracking from refine_hd_num "; *) + refine_hd h [Quantif] lnameargs lnumargs n))) + end - | _ => fail 0 + | _ => (*base case *) + match ldirectarg,lnameargs,lnumargs with + | [],[],[] => exact $hc + | [],[],[SubGoalAtAll] => exact $hc + | _ => invalid_arg "Not a product (others)" end - | _ => lazymatch type of h with - | (forall (h_premis:?t) , _) => refine_hd h (cons Quantif nil) lnameargs lnumargs n - | _ => refine_hd h (@nil spec_arg)(@nil spec_arg)(@nil spec_arg) n - end - | _ => fail "refine_hd" - end. + (* (refine_hd_num (h:ident) (ldirectarg:directarg list) (lnameargs:namearg list) *) + (* (lnumargs:numarg list) (n:int)) *) + end + with refine_hd_name (h:ident) (lnameargs:namearg list) + (lnumargs:numarg list) (n:int) := + let hc:constr := Control.hyp h in (* h as a constr *) + let th:constr := Constr.type hc in (* type of h as a constr *) + match lnameargs with + | namearg :: lnameargs' => + match Unsafe.kind th with + | Prod bnd _ => + let h_premis := Constr.Binder.name bnd in + match namearg with + | SubGoalAtName nme => + if map_default (Ident.equal nme) false h_premis + then refine_hd h [SubGoal] lnameargs' lnumargs n + else backtrack "refine_hd_name: SubGoalAtName" + | EvarAtName nme nameevar => + if map_default (Ident.equal nme) false h_premis + then refine_hd h [Evar nameevar] lnameargs' lnumargs n + else backtrack "refine_hd_name: EvarAtName" + end + | _ => invalid_arg "Not a product (refine_hd_name)" + end + | _ => backtrack "refine_hd_name: no namearg" + end + with refine_hd_num (h:ident) (lnameargs:namearg list) + (lnumargs:numarg list) (n:int) := + let hc:constr := Control.hyp h in (* h as a constr *) + let th:constr := Constr.type hc in (* type of h as a constr *) + let newn := if is_dep_prod th then n else (Int.add n 1) in + match lnumargs with + | numarg::lnumargs' => + match Unsafe.kind th with + | Prod _ _ => + match numarg with + | SubGoalAtNum num => + if is_dep_prod th + then backtrack "refine_hd_num: SubGoalAtNum, dep" + else if Int.le newn num + then if Int.equal newn num + then refine_hd h [SubGoal] lnameargs lnumargs' n + else backtrack "refine_hd_num: SubGoalAtNum,nodep" + else invalid_arg "Did you not order the evar numbers?" + | SubGoalUntilNum num => + if is_dep_prod th + then backtrack "refine_hd_num: SubGoalUntilNum, dep" + else + if Int.equal newn num + then refine_hd h [SubGoal] lnameargs lnumargs' n + else refine_hd h [SubGoal] lnameargs lnumargs n + + | SubGoalAtAll => + if is_dep_prod th + then backtrack "refine_hd_num: SubGoalAtAll, dep" + else refine_hd h [SubGoal] lnameargs lnumargs n + end + | _ => invalid_arg "Not a product (refine_hd_num)." + end + | _ => backtrack "refine_hd_num: no numarg" + end. (* initialize n to zero. *) -Ltac refine_spec h lnameargs lnumargs := refine_hd h constr:(@nil spec_arg) lnameargs lnumargs 0. +Local Ltac2 refine_spec h lnameargs lnumargs := refine_hd h [] lnameargs lnumargs 0. +(* +(* tests *) +Definition eq_one (i:nat) := i = 1. +Definition hidden_product := forall i j :nat, i+1=j -> i+1=j -> i+1=j. + +Axiom ex_hyp : (forall (b:bool), forall x: nat, eq_one 1 -> forall y:nat, eq_one 2 ->eq_one 3 ->eq_one 4 ->eq_one x ->eq_one 6 ->eq_one y -> eq_one 8 -> eq_one 9 -> False). + +Lemma test_esepec: True. +Proof. + (* specialize ex_hyp as h. *) + (* especialize ex_hyp at 2 as h. *) + specialize ex_hyp as H. + + ltac2:(assert_evar @hhh). + + let ev1 := open_constr:(_) in + assert ev1 as hhh;[ + ltac2:(refine_spec + (Option.get (Ident.of_string "H")) + [EvarAtName @b @b; EvarAtName @x @x; EvarAtName @y @y] + [SubGoalAtNum 3]) + | ]; + [ | match type of hhh with eq_one 1 -> eq_one 3 -> eq_one 4 -> eq_one _ -> eq_one 6 -> eq_one _ -> eq_one 8 -> eq_one 9 -> False => idtac end]. + [ .. | match type of hhh with eq_one 1 -> eq_one 3 -> eq_one 4 -> eq_one _ -> eq_one 6 -> eq_one _ -> eq_one 8 -> eq_one 9 -> False => idtac end]. + + +especialize ex_hyp at 3 with b,x,y as h; + Undo. + + +Lemma foo: forall x y : nat, + (forall (n m p :nat) (hhh:n < m) (iii:n <= m), + p > 0 + -> p > 2 + -> p > 1 + -> hidden_product) -> False. +Proof. + intros x y H. + + let ev1 := open_constr:(_) in + assert ev1. + + + ltac2:(refine_spec + (Option.get (Ident.of_string "H")) + [EvarAtName @m @m] + [SubGoalAtAll]). + Undo 1. + + (ltac2:(refine_hd + (Option.get (Ident.of_string "H")) + [] + [EvarAtName @m @m] + [SubGoalUntilNum 3] + 0)). + Undo 1. + + (ltac2:(refine_hd + (Option.get (Ident.of_string "H")) + [Evar @ev] + [EvarAtName @p @p ;SubGoalAtName @iii] + [SubGoalAtNum 4] + 0)). + +*) + +Local Ltac2 cmp_numarg a b := + match a with + SubGoalAtNum na => + match b with + SubGoalAtNum nb => Int.compare na nb + | _ => -1 + end + | _ => -1 + end. + +Local Ltac2 sort_numargs (l: numarg list): numarg list:= List.sort cmp_numarg l. @@ -374,150 +370,148 @@ Ltac refine_spec h lnameargs lnumargs := refine_hd h constr:(@nil spec_arg) lnam From Stdlib Require Sorting.Mergesort Structures.OrdersEx. -Module SpecargOrder <: Structures.Orders.TotalLeBool. - Definition t := spec_arg. - - Definition leb a b := - match a with - SubGoalAtNum na => - match b with - SubGoalAtNum nb => Nat.leb na nb - | _ => true - end - | _ => true - end. - -(* Nat.leb. *) - - Theorem leb_total : forall a1 a2, leb a1 a2 = true \/ leb a2 a1 = true. - Proof. - intros a1 a2. - destruct a1;destruct a2;auto. - setoid_rewrite PeanoNat.Nat.leb_le. - apply PeanoNat.Nat.le_ge_cases. - Qed. -End SpecargOrder. - - -Module NatSort := Sorting.Mergesort.Sort(SpecargOrder). - -Local Ltac espec_gen H lnames lnums name replaceb := - (* morally this evar is of type Type, don't know how to enforce this - without having an ugly cast in goals *) - (* idtac "espec_gen " H " " l " " name " " replaceb; *) - (* idtac "lnums = " lnums; *) - let lnums := eval compute in (NatSort.sort lnums) in - (* idtac "lnums = " lnums; *) - tryif is_var H - then (let ev1 := open_constr:(_) in - match replaceb with - true => - assert ev1 as name ; [ (refine_spec H lnames lnums) - | clear H;try rename name into H ] - | false => - assert ev1 as name; [ (refine_spec H lnames lnums) | ] - end) - else (* replaceb should be false in this case. *) - (let H' := fresh "H" in - specialize H as H'; - let ev1 := open_constr:(_) in - assert ev1 as name; [ (refine_spec H' lnames lnums) | clear H' ]). - -(* ltac2 int -> constr nat *) -Ltac2 rec int_to_coq_nat n := - match Int.equal n 0 with - | true => constr:(O) - | false => let n := int_to_coq_nat (Int.sub n 1) in - constr:(S $n) +Local Ltac2 dest_var (c:constr) : ident := + match Unsafe.kind c with + | Unsafe.Var x => x + | _ => Control.throw (Invalid_argument (Some (Message.of_string "dest_var"))) end. -Ltac2 int_to_constr_nat n := - let val := int_to_coq_nat n in - Std.eval_vm None val. - -Ltac2 rec li_to_speclist_SGAtNum (li: int list): constr := - match li with - [] => constr:(@nil spec_arg) - | i :: l' => - let cl := li_to_speclist_SGAtNum l' in - let ci := int_to_constr_nat i in - constr:(cons (SubGoalAtNum $ci) $cl) - end. +Local Ltac2 espec_gen (h:constr) lnames lnums name (replaceb:bool) := + let lnums := sort_numargs lnums in + if is_var h + then + let h := dest_var h in + match replaceb with + true => + assert_evar name > [ (refine_spec h lnames lnums) + | Std.clear [h]; Std.rename [(name, h)] ] + | false => + assert_evar name > [ (refine_spec h lnames lnums) | ] + end + else + (* replaceb should be false in this case. *) + (let h' := Fresh.in_goal @H in + Std.specialize (h , Std.NoBindings) (Some (Std.IntroNaming (Std.IntroIdentifier h'))); + assert_evar name > [ (refine_spec h' lnames lnums) | Std.clear [h'] ]). -Ltac2 rec li_to_speclist_SGUntilNum (li: int list): constr := - match li with - [] => constr:(@nil spec_arg) - | i :: l' => - let cl := li_to_speclist_SGUntilNum l' in - let ci := int_to_constr_nat i in - constr:(cons (SubGoalUntilNum $ci) $cl) - end. -Ltac2 rec li_to_speclist_EVAtName (li: ident list): constr := - match li with - [] => constr:(@nil spec_arg) - | i :: l' => - let cl := li_to_speclist_EVAtName l' in - let istr := Ident.to_string i in - let icstr := IdentParsing.coq_string_of_string istr in - constr:(cons (EvarAtName $icstr $icstr) $cl) - end. -(* Ltac2 occurrences_to_evaratname (li:ident list): constr := li_to_speclist_EVAtName li. *) +(* +(* tests *) +Definition eq_one (i:nat) := i = 1. +Definition hidden_product := forall i j :nat, i+1=j -> i+1=j -> i+1=j. -Ltac2 espec_at_using_ltac1_gen (h:constr) (li:int list) (occsevar:ident list) (newH: ident) (replaceb:bool):unit := - (* FIXME: we should also refuse when a section variables is given. *) +Lemma foo: forall x y : nat, + (forall (n m p :nat) (hhh:n < m) (iii:n <= m), + p > 0 + -> p > 2 + -> p > 1 + -> hidden_product) -> False. +Proof. + intros x y H. + + ltac2:(espec_gen constr:(H) [EvarAtName @m @m] [SubGoalAtAll] @toto false). + Undo 1. + ltac2:(espec_gen constr:(H) [EvarAtName @m @m] [SubGoalAtAll] @toto true). + Undo 1. + ltac2:(espec_gen constr:(H) [EvarAtName @m @m] [SubGoalUntilNum 3] @toto false). + Undo 1. + ltac2:(espec_gen constr:(H) [EvarAtName @m @m] [SubGoalUntilNum 3] @toto true). + Undo 1. + ltac2:(espec_gen constr:(H) [EvarAtName @m @m] [SubGoalAtAll] @toto false). + Undo 1. + ltac2:(espec_gen constr:(H) [EvarAtName @n @n; EvarAtName @m @m] [SubGoalAtNum 4] @toto false). + Undo 1. + ltac2:(espec_gen constr:(H) [EvarAtName @n @n; EvarAtName @m @m] [SubGoalAtNum 4] @toto true). + Undo 1. +*) + +Local Ltac2 sgatnum_from_lint (li:int list): numarg list := + List.map (fun i => SubGoalAtNum i) li. + +Local Ltac2 evatname_from_lid (li:ident list): namearg list := + List.map (fun i => EvarAtName i i) li. + +(* FIXME li should really be a single int *) +Local Ltac2 sguntilnum_from_lid (li:int list): numarg list := + List.map (fun i => SubGoalUntilNum i) li. + +Local Ltac2 espec_at_using_ltac1_gen (h:constr) (li:int list) (occsevar:ident list) (newH: ident) (replaceb:bool):unit := if Bool.and (Bool.neg (is_var h)) replaceb - then - Control.zero (Tactic_failure (Some (fprintf "You must provide a name with 'as'."))) - else - let c1 := li_to_speclist_SGAtNum li in - let c2 := li_to_speclist_EVAtName occsevar in - (* let c := Std.eval_red constr:(List.app $c2 $c1) in *) - let replaceb := if replaceb then constr:(true) else constr:(false) in - ltac1:(h c2 c1 newH replaceb |- espec_gen h c2 c1 newH replaceb) - (Ltac1.of_constr h) - (Ltac1.of_constr c2) - (Ltac1.of_constr c1) - (Ltac1.of_ident newH) - (Ltac1.of_constr replaceb). - -Ltac2 espec_until_using_ltac1_gen (h:constr) (li:int list) (occsevar:ident list) (newH: ident) (replaceb:bool) (atAll:bool):unit := + then Control.zero (Tactic_failure (Some (fprintf "You must provide a name with 'as'."))) + else espec_gen h (evatname_from_lid occsevar) (sgatnum_from_lint li) newH replaceb. + +Local Ltac2 espec_until_using_ltac1_gen (h:constr) (li:int list) (occsevar:ident list) (newH: ident) (replaceb:bool) (atAll:bool):unit := (* FIXME: we should also refuse when a section variables is given. *) if Bool.and (Bool.neg (is_var h)) replaceb then Control.zero (Tactic_failure (Some (fprintf "You must provide a name with 'as'."))) else - let c1 := if atAll then constr:(cons SubGoalAtAll nil) else li_to_speclist_SGUntilNum li in - let c2 := li_to_speclist_EVAtName occsevar in - (* let c := Std.eval_red constr:(List.app $c2 $c1) in *) - let replaceb := if replaceb then constr:(true) else constr:(false) in - ltac1:(h c2 c1 newH replaceb |- espec_gen h c2 c1 newH replaceb) - (Ltac1.of_constr h) - (Ltac1.of_constr c2) - (Ltac1.of_constr c1) - (Ltac1.of_ident newH) - (Ltac1.of_constr replaceb). - -Ltac2 interp_ltac1_id_list (lid:Ltac1.t) : ident list := + let c1 := if atAll then [SubGoalAtAll] else sguntilnum_from_lid li in + espec_gen h (evatname_from_lid occsevar) c1 newH replaceb. + + +(* +(* tests *) +Definition eq_one (i:nat) := i = 1. +Definition hidden_product := forall i j :nat, i+1=j -> i+1=j -> i+1=j. + +Axiom ex_hyp : (forall (b:bool), forall x: nat, eq_one 1 -> forall y:nat, eq_one 2 ->eq_one 3 ->eq_one 4 ->eq_one x ->eq_one 6 ->eq_one y -> eq_one 8 -> eq_one 9 -> False). + + +Lemma test_espec_namings: forall n:nat, (eq_one n -> eq_one 1 -> False) -> True. +Proof. + intros n h_eqone. + specialize min_l as hhh. + ltac2:(espec_at_using_ltac1_gen constr:(hhh) [1] [@n; @m] @hhh' false). + + let tac := ltac2:(hhh |- call_specialize_ltac2_gen hhh [1] [@n; @m] hhh' false) in + tac hhh. + let tac := ltac2:(h li levars newH |- call_specialize_ltac2_gen h li levars newH false) in + let newH := gen_hyp_name hhh in + tac hhh li levars ident:(newH). + + especialize hhh with n,m at 1 as ?. + especialize min_l with n,m at 1 as ?. + + +Lemma foo: forall x y : nat, + (forall (n m p :nat) (hhh:n < m) (iii:n <= m), + p > 0 + -> p > 2 + -> p > 1 + -> hidden_product) -> False. +Proof. + intros x y H. + + ltac2:(espec_at_using_ltac1_gen constr:(H) [2;4] [@m; @p] @toto false). + Undo 1. + ltac2:(espec_at_using_ltac1_gen constr:(H) [2;4] [@m; @p] @toto true). + Undo 1. + ltac2:(espec_until_using_ltac1_gen constr:(H) [] [@m] @toto false true). + Undo 1. + ltac2:(espec_until_using_ltac1_gen constr:(H) [] [@m] @toto true true). + Undo 1. + ltac2:(espec_until_using_ltac1_gen constr:(H) [3] [@m] @toto false false). + Undo 1. + ltac2:(espec_until_using_ltac1_gen constr:(H) [3] [@m] @toto true false). + Undo 1. + ltac2:(espec_until_using_ltac1_gen constr:(H) [4] [@n ; @m] @toto false false). + Undo 1. + ltac2:(espec_until_using_ltac1_gen constr:(H) [4] [@n ; @m] @toto true false). + Undo 1. +*) + +Local Ltac2 interp_ltac1_id_list (lid:Ltac1.t) : ident list := List.map (fun x => Option.get (Ltac1.to_ident x)) (Option.get (Ltac1.to_list lid)). -Ltac2 interp_ltac1_int_list (li:Ltac1.t) : int list := +Local Ltac2 interp_ltac1_int_list (li:Ltac1.t) : int list := List.map (fun x => Option.get (Ltac1.to_int x)) (Option.get (Ltac1.to_list li)). -Ltac2 interp_ltac1_hyp (h:Ltac1.t) : constr := Option.get (Ltac1.to_constr h). +Local Ltac2 interp_ltac1_hyp (h:Ltac1.t) : constr := Option.get (Ltac1.to_constr h). -(* let t:constr option := Ltac1.to_constr li in - match t with - Some x => if Constr.equal x constr:(SubGoalAtAll) - then constr:(cons SubGoalAtAll nil) - else Control.zero (Tactic_failure (Some (fprintf "bad at specification."))) - - | _ => [] - end - *) (* call Ltac2'especialize on argscoming from Ltac1 notation *) -Ltac2 call_specialize_ltac2_gen (h:Ltac1.t) (li:Ltac1.t) levars newh (replaceb:bool) := +Local Ltac2 call_specialize_ltac2_gen (h:Ltac1.t) (li:Ltac1.t) levars newh (replaceb:bool) := let li2 := match Ltac1.to_list li with None => [] | Some _ => interp_ltac1_int_list li @@ -533,10 +527,9 @@ Ltac2 call_specialize_ltac2_gen (h:Ltac1.t) (li:Ltac1.t) levars newh (replaceb:b (Option.get (Ltac1.to_ident newh)) replaceb. - (* call Ltac2'especialize on argscoming from Ltac1 notation *) -Ltac2 call_specialize_until_ltac2_gen (h:Ltac1.t) li levars newh replaceb (atAll:bool) := +Local Ltac2 call_specialize_until_ltac2_gen (h:Ltac1.t) li levars newh replaceb (atAll:bool) := let li2 := match Ltac1.to_list li with None => [] | Some _ => interp_ltac1_int_list li @@ -560,7 +553,6 @@ Ltac gen_hyp_name h := match goal with end. Ltac dummy_term := constr:(Prop). - (* ESPECIALIZE AT *) (* ********************* *) @@ -749,8 +741,43 @@ Tactic Notation "especialize" constr(h) "until" ne_integer_list_sep(li,",") := let levars := dummy_term in tac h li levars ident:(nme). +(* +(* tests *) +Definition eq_one (i:nat) := i = 1. +Definition hidden_product := forall i j :nat, i+1=j -> i+1=j -> i+1=j. + + +Lemma foo: forall x y : nat, + (forall (n m p :nat) (hhh:n < m) (iii:n <= m), + p > 0 + -> p > 2 + -> p > 1 + -> hidden_product) -> False. +Proof. + intros x y H. + + especialize H with m,p at 2,4 as toto. + + ltac2:(espec_at_using_ltac1_gen constr:(H) [2;4] [@m; @p] @toto false). + Undo 1. + ltac2:(espec_at_using_ltac1_gen constr:(H) [2;4] [@m; @p] @toto true). + Undo 1. + ltac2:(espec_until_using_ltac1_gen constr:(H) [] [@m] @toto false true). + Undo 1. + ltac2:(espec_until_using_ltac1_gen constr:(H) [] [@m] @toto true true). + Undo 1. + ltac2:(espec_until_using_ltac1_gen constr:(H) [3] [@m] @toto false false). + Undo 1. + ltac2:(espec_until_using_ltac1_gen constr:(H) [3] [@m] @toto true false). + Undo 1. + ltac2:(espec_until_using_ltac1_gen constr:(H) [4] [@n ; @m] @toto false false). + Undo 1. + ltac2:(espec_until_using_ltac1_gen constr:(H) [4] [@n ; @m] @toto true false). + Undo 1. +*) + (* Experimenting a small set of tactic to manipulate a hyp: *) (* Ltac quantify H := @@ -789,7 +816,7 @@ Abort. *) - +(* (* tests *) Definition eq_one (i:nat) := i = 1. Definition hidden_product := forall i j :nat, i+1=j -> i+1=j -> i+1=j. @@ -820,3 +847,39 @@ Lemma foo: forall x y : nat, Proof. intros x y H. Abort. + + +Axiom ex_hyp : (forall (b:bool), forall x: nat, eq_one 1 -> forall y:nat, eq_one 2 ->eq_one 3 ->eq_one 4 ->eq_one x ->eq_one 6 ->eq_one y -> eq_one 8 -> eq_one 9 -> False). + +Lemma test_esepec: True. +Proof. + (* specialize ex_hyp as h. *) + (* especialize ex_hyp at 2 as h. *) + + especialize ex_hyp at 3 with b,x,y as h;[ .. | match type of h with eq_one 1 -> eq_one 3 -> eq_one 4 -> eq_one _ -> eq_one 6 -> eq_one _ -> eq_one 8 -> eq_one 9 -> False => idtac end]. + Undo. +Abort. + +Lemma test_espec_namings: forall n:nat, (eq_one n -> eq_one 1 -> False) -> True. +Proof. + intros n h_eqone. + especialize min_l with n,m at 1 as ?. + (* especialize PeanOant.Nat.quadmul_le_squareadd with a at 1 as hh : h. *) + especialize PeanoNat.Nat.quadmul_le_squareadd with a at 1 as hh. + { apply le_n. } + specialize min_l as hhh. + especialize hhh with n,m at 1 as ?. + especialize min_l with n,m at 1 as ?. + { apply (le_n O). } + especialize h_eqone at 2 as h1. + { reflexivity. } + unfold eq_one in min_l_spec_. + (* match type of h2 with 1 = 1 => idtac | _ => fail end. *) + match type of h1 with eq_one n -> False => idtac | _ => fail end. + exact I. +Qed. + + + + +*) diff --git a/LibHyps/LibHyps.v b/LibHyps/LibHyps.v index 25d96d6..f600dda 100644 --- a/LibHyps/LibHyps.v +++ b/LibHyps/LibHyps.v @@ -9,6 +9,34 @@ Require Export LibHyps.LibHypsTactics. (* We export ; { } etc. ";;" also. *) +Ltac rename_or_revert H := autorename_strict H + revert dependent H. + +(* Some usual tactics one may want to use on new hyps. *) + +(* This is similar to subst x, but ensures that H and only H is used. + Even if there is another hyp with the same variable *) +Ltac substHyp H := + match type of H with + (* | Depl => fail 1 (* fail immediately, we are applying on a list of hyps. *) *) + | ?x = ?y => + (* subst would maybe subst using another hyp, so use replace to be sure *) + once ((is_var(x); replace x with y in *; [try clear x ; try clear H] ) + + (is_var(y); replace y with x in * ; [try clear y; try clear H])) + | _ => idtac + end. + +(* revert, fails if impossible, should not fail if hyps are ordered in the right order *) +Ltac revertHyp H := revert H. (* revert is a tactic notation, so we need to define this *) + +(* revert if subst fails. Never fail, be careful not to use this tactic in the + left member of a "+" tactical: *) +Ltac subst_or_revert H := try first [progress substHyp H | generalize dependent H]. + +(* try subst. Never fail, be careful to not use this tactic in the + left member of a "+" tactical: *) +Ltac subst_or_idtac H := substHyp H. + + Export TacNewHyps.Notations. (* There are three variants of the autorename tatic, depending on what @@ -27,11 +55,16 @@ Tactic Notation (at level 4) "/" "n?" := (onAllHyps rename_or_revert). Tactic Notation (at level 4) tactic4(Tac) "/" "r" := Tac ; {< revertHyp }. Tactic Notation (at level 4) "/" "r" := (onAllHypsRev revertHyp). +Tactic Notation (at level 4) tactic4(Tac) "/" "g" := Tac ; { move_up_types }. +(* Tactic Notation (at level 4) tactic4(Tac) "/" "g" := Tac ; {! group_up_list }. *) +(* (* WARNING group_up_list applies to the whole list of hyps directly. *) (* Tactic Notation (at level 4) tactic4(Tac) "/" "g" := (then_allnh Tac group_up_list). *) -Tactic Notation (at level 4) tactic4(Tac) "/" "g" := Tac ; {! group_up_list }. -Tactic Notation (at level 4) "/" "g" := (group_up_list all_hyps). +(* Tactic Notation (at level 4) tactic4(Tac) "/" "g" := Tac ; {! group_up_list }. *) +(* Not yet reimplemented in ltac2 *) +Tactic Notation (at level 4) "/" "g" := (group_up_list all_hyps). +*) (* Tactic Notation (at level 4) tactic4(Tac) "/" "s" := (then_eachnh Tac subst_or_idtac). *) Tactic Notation (at level 4) tactic4(Tac) "/" "s" := Tac ; { subst_or_idtac }. Tactic Notation (at level 4) "/" "s" := (onAllHyps subst_or_idtac). @@ -46,11 +79,11 @@ Tactic Notation (at level 4) tactic4(Tac) "/" "sg" := (Tac /s/g). Tactic Notation (at level 4) tactic4(Tac) "/" "ng" := (Tac /n/g). Tactic Notation (at level 4) tactic4(Tac) "/" "gn" := (Tac /g/n). -Tactic Notation (at level 4) "/" "sng" := - (onAllHyps subst_or_idtac); (onAllHyps autorename); group_up_list all_hyps. +(* Tactic Notation (at level 4) "/" "sng" := *) + (* (onAllHyps subst_or_idtac); (onAllHyps autorename); group_up_list all_hyps. *) Tactic Notation (at level 4) "/" "sn" := (onAllHyps subst_or_idtac); (onAllHyps autorename). Tactic Notation (at level 4) "/" "sr" := (onAllHyps subst_or_idtac); (onAllHyps revertHyp). -Tactic Notation (at level 4) "/" "ng" := ((onAllHyps autorename) ; group_up_list all_hyps). +Tactic Notation (at level 4) "/" "ng" := ((onAllHyps autorename) ; (onAllHyps move_up_types) ). Module LegacyNotations. Import Notations. @@ -85,49 +118,50 @@ Goal forall x1 x3:bool, forall a z e : nat, Proof. (* Set Ltac Debug. *) (* then_nh_rev ltac:(intros) ltac:(subst_or_idtac). *) - intros ; {! group_up_list }. + (* intros ; {! group_up_list }. *) (* intros ? ? ? ? ? ? ? ? ? ?. *) (* group_up_list (DCons bool b1 DNil). *) - Undo. - intros ; { move_up_types }. - Undo. + (* Undo. *) + (* intros ; { move_up_types }. *) + (* Undo. *) intros /n. Undo. intros /s/n. Undo. intros /n. - match goal with - | h: bool => assert - end - Undo. - intros/n. Undo. - intros ; { autorename }; {! group_up_list }. + intros ; { autorename }. (*; {! group_up_list }.*) Undo. - intros/ng. + (* intros/ng. *) + (* Undo. *) + intros ; {subst_or_idtac} ; { autorename }. (* ; {! group_up_list }.*) Undo. - intros ; {subst_or_idtac} ; { autorename } ; {! group_up_list }. - Undo. - intros/sng. - Fail progress intros ; { revertHyp }. + (* intros/sng. *) + (* Fail progress intros ; { revertHyp }. *) - subst_or_idtac (DCons (z0 + r = a) H DNil). + (* subst_or_idtac (DCons (z0 + r = a) H DNil). *) - let hyps := all_hyps in - idtac hyps. - subst_or_idtac hyps. + (* let hyps := all_hyps in *) + (* idtac hyps. *) + (* subst_or_idtac hyps. *) - intros ;!; ltac:(subst_or_idtac_l). + (* intros ;!; ltac:(subst_or_idtac_l). *) - then_nh_one_by_one ltac:(intros) ltac:(subst_or_idtac). -; {< subst_or_idtac }. ; { group_up_list } ; { autorename_l }. - subst_or_idtac h_eq_a_add_z0_t. - intros ; { fun h => autorename_strict h }. + (* then_nh_one_by_one ltac:(intros) ltac:(subst_or_idtac). *) +(* ; {< subst_or_idtac }. ; { group_up_list } ; { autorename_l }. *) + (* subst_or_idtac h_eq_a_add_z0_t. *) + Fail (intros ; { fun h => autorename_strict h }). + intros ; { fun h => autorename_orelse_revert h }. + match goal with + | |- (fun _ : bool => z = e) true -> True => idtac + end. + Undo 2. intros ; { fun h => idtac h }. + Undo. intros ; { ltac:(fun h => idtac h) }. - intros ; [H: sng H]. + *) (* Goal forall x1 x3:bool, True -> forall a z e r t z e r t z e r t z e r t y: nat, False -> forall u i o p q s d f g:nat, forall x2:bool, True -> True. diff --git a/LibHyps/LibHypsDebug.v b/LibHyps/LibHypsDebug.v new file mode 100644 index 0000000..490c2d5 --- /dev/null +++ b/LibHyps/LibHypsDebug.v @@ -0,0 +1,58 @@ +Require Import Ltac2.Ltac2. +From Ltac2 Require Import Option Constr Printf. + +(* debug *) +(* +Require LibHyps.LibHypsTactics. +Module Prgoal_Notation. + Ltac pr_goal := + match goal with + |- ?g => + let allh := LibHyps.TacNewHyps.harvest_hyps LibHyps.TacNewHyps.revert_clearbody_all in + (* let allh := all_hyps in *) + idtac "GOAL: " allh " ⊢ " g + end. +End Prgoal_Notation. +*) + +Ltac2 tag_info s := (String.concat "" [ ""; s; "" ]). +Ltac2 tag_msg m := Message.concat + (Message.concat (Message.of_string "") m) + (Message.of_string ""). +Ltac2 str_to_msg s := tag_msg (Message.of_string s). +Ltac2 int_to_msg i := tag_msg (Message.of_int i). +Ltac2 id_to_msg id := tag_msg (Message.of_ident id). +Ltac2 constr_to_msg c := tag_msg (Message.of_constr c). + +Ltac2 msgm m := Message.print (tag_msg m). +Ltac2 msgs s := Message.print (str_to_msg s). +Ltac2 msgi i := Message.print (int_to_msg i). +Ltac2 msgc c := Message.print (constr_to_msg c). +Ltac2 msgid id := Message.print (id_to_msg id). + +Ltac2 pr_list (pr: unit -> 'a -> message) () (l: 'a list) : message := + let rec pr_list_ () (l: 'a list) := + match l with + | [] => fprintf "" + | [e] => fprintf "%a" pr e + | e::l' => fprintf "%a , %a" pr e pr_list_ l' + end in + fprintf "[ %a ]" pr_list_ l. + + +Ltac2 pr_binder () (b:binder):message := + let nme:ident option := Binder.name b in + let typ:constr := Binder.type b in + fprintf "(%I:%t)" (Option.get nme) typ. + +Ltac2 pr_string () (s:string): message := fprintf "%s" s. + +Ltac2 pr_goal() := + let l := Control.hyps() in + printf " Goal:"; + List.iter (fun (nme,_,typ) => printf "%I : %t" nme typ) l; + printf "⊢ %t" (Control.goal()); + printf "". + +Ltac2 pr_acc () (acc:string list) := + fprintf "[%a]" (pr_list pr_string) acc. diff --git a/LibHyps/LibHypsNaming.v b/LibHyps/LibHypsNaming.v index 94f15b2..f64ebff 100644 --- a/LibHyps/LibHypsNaming.v +++ b/LibHyps/LibHypsNaming.v @@ -1,143 +1,154 @@ (* Copyright 2021 Pierre Courtieu This file is part of LibHyps. It is distributed under the MIT "expat license". You should have recieved a LICENSE file with it. *) - -From Stdlib Require Import Arith ZArith List. -Require Import LibHyps.TacNewHyps. -Import ListNotations. -Local Open Scope list. +(* **************************************************************** *) (** This file defines a tactic "autorename h" (and "autorename_strict - h") that automatically rename hypothesis h followinh a systematic, + h") that automatically rename hypothesis h following a systematic, but customizable heuristic. Comments welcome. *) +From Stdlib Require Import Arith ZArith List. +Require LibHyps.TacNewHyps. + +(* Import ListNotations. *) +(* Local Open Scope list. *) +Require Import Ltac2.Ltac2. +From Ltac2 Require Import Option Constr Printf. +Import Constr.Unsafe. +Local Set Default Proof Mode "Classic". +Require Import LibHyps.LibHypsDebug. + +Local Ltac2 backtrack (msg:string) := Control.zero (Tactic_failure (Some (fprintf "Backtrack: %s" msg))). +Local Ltac2 control_try tac := Control.plus tac (fun _ => ()). + (* Comment this and the Z-dependent lines below if you don't want ZArith to be loaded *) From Stdlib Require Import ZArith. -(** ** The custom renaming tactic +Ltac2 decr (n:int):int := + if Int.equal n 0 then 0 else Int.sub n 1. - The tactic "rename_hyp" should be redefined along a coq development, - it should return a fresh name build from a type th and a depth. It - should fail if no name is found, so that the fallback scheme is - called. +Ltac2 incr (n:int):int := Int.add n 1. - Typical use, in increasing order of complexity, approximatively - equivalent to the decreasing order of interest. +Ltac2 Type rename_directive := [ String(string) | Rename(constr) | RenameN(int,constr) ]. +Ltac2 Type rename_directives := rename_directive list. -<< -Ltac rename_hyp1 n th := - match th with - | List.In ?e ?l => name ( `_lst_in` ++ e#n ++ l#O) - | InA _ ?e ?l => name( `_inA` ++ e#n ++ l#0) - | @StronglySorted _ ?ord ?l => name ( `_strgSorted` ++ l#(S (S n))) - | @Forall _ ?P ?x => name (`_lst_forall` ++ P#n ++ x#n) - | @Forall2 _ _ ?P ?x ?y => name (`_lst_forall2` ++ P#n ++ x#n ++ y#n) - | NoDupA _ ?l => name (`_NoDupA` ++ l#n) - | NoDup _ ?l => name (`_NoDup` ++ l#n) +(* For debugging *) +Module Debug. +Ltac2 pr_directive () (d:rename_directive) := + match d with + String s => fprintf "%s" s + | Rename c => fprintf "%t" c + | RenameN i c => fprintf "N(%i,%t)" i c end. ->> -(* Overwrite the definition of rename_hyp using the ::= operator. :*) - -<< -Ltac rename_hyp ::= my_rename_hyp. ->> *) +End Debug. +Ltac2 Type hypnames := string list. +(** This determines the depth of the recursive analysis of a type to + compute the corresponding hypothesis name. generally 2 or 3 is + enough. More gives too log names, less may give identical names + too often. *) +Ltac2 mutable rename_depth := 3. +(* The pretty printing of numerical values is by default 1, 2... Set this to + true (Ltac2 Set numerical_sufs := true) to have 1z, 1n or 1N depending of the type nat, Z or N. *) +Ltac2 mutable numerical_sufx := false. +(* Whether autorename should add a "_" at the end of every hypothesis name *) +Ltac2 mutable add_suffix := true. +(* Whether autornename should add "h_" at the beginniong of each hypothesis name *) +Ltac2 mutable add_prefix := true. -(** * Implementation principle: - - The name of the hypothesis will be a sequence of chunks. A chunk is - a word generally starting with "_". - - Internally (not seen by the user) this sequence is represented by a - list of small terms. One term of the form (∀ :Prop, DUMMY - ) per chunk. For instance the sequence "h_eq_foo" is - represented by the following coq term: +(** Default prefix for hypothesis names. *) +Ltac2 default_prefix():string := "h". - [(∀ h,DUMMY h) ; (∀ _eq,DUMMY _eq) ; (∀ _foo, DUMMY _foo)] +(** A few special default chunks, for special cases in the naming heuristic. *) +Ltac2 impl_prefix() := "impl". +Ltac2 forall_prefix() := "all". +Ltac2 exists_prefix() := "ex". - where DUMMY is an opaque (identity) function but we don't care. *) +(** ** The custom renaming tactic + + This is the customizable naming tactic that the user should REDEFINE along + his development. See below for an example of such redefinition. It should + always fail when no name suggestion is found, to give a chance to the + default naming scheme to apply. *) +Ltac2 mutable rename_hyp (stop:int) (th:constr): rename_directives := backtrack "rename_hyp". -(** We define DUMMY as an opaque symbol. *) -Definition DUMMY: Prop -> Prop. - exact (fun x:Prop => x). -Qed. +(* Typical use, in increasing order of complexity, approximatively + equivalent to the decreasing order of interest. *) +(** +<< +From Stdlib Require Import Sorting.SetoidList. +Ltac2 rename_hyp_2 n th := + match! th with + | true <> false => [String "tNEQf"] + | true = false => [String "tEQf"] +end. +Ltac2 rename_hyp_3 n th := + match! th with + | List.In ?e ?l => [String "lst_in" ; RecRename n e ; RecRename 0 l] + | InA _ ?e ?l => [String "inA" ; RecRename n e ; RecRename 0 l ] + | @StronglySorted _ ?ord ?l => [ String"strgSorted" ; RecRename (Int.add 2 n) l] + | @Forall _ ?p ?x => [String "lst_forall" ; RecRename n p ; RecRename n x] + | @Forall2 _ _ ?p ?x ?y => [String "_lst_forall2" ; RecRename n p ; RecRename n x; RecRename n y] + | NoDupA _ ?l => [String "_NoDupA" ; RecRename n l ] + | NoDup _ ?l => [String "_NoDup" ; RecRename n l ] + | _ => rename_hyp_2 n th + end. +Ltac2 Set rename_hyp := rename_hyp_3. +>> *) -(* ********** CUSTOMIZATION ********** *) +(* This one is similar but for internal use *) +Ltac2 mutable rename_hyp_default (n:int) (th:constr): rename_directives := backtrack "rename_hyp_default". -(** If this is true, then all hyps names will have a trailing "_". In - case of names ending with a digit (like in "le_1_2" or "le_x1_x2") - this additional suffix avoids Coq's fresh name generation to - *replace* the digit. Although this is esthetically bad, it makes - things more predictable. You may set this to true for backward - compatility. *) -Ltac add_suffix := constr:(true). +Module Ltac2. -(* This sets the way numerical constants are displayed, default value - is set below to numerical_names_nosufx, which will give the same - name to (O<1)%nat and (O<1)%Z and (O<1)%N, i.e. h_lt_0_1_. +(* from [ "foo" ; "bar" ; "oof" ] to "h_oof_bar_foo_". Note the reversing of the list *) +Ltac2 build_name_gen (sep:string) (prefx:bool) (suffx:bool) (l:string list) := + let l := if prefx then (default_prefix()::l) else l in + (String.app (String.concat sep l) (if suffx then "_" else "")). - but you can use this in your development to change it - h_lt_0n_1n_/h_lt_0z_1z_/h_lt_0N_1N_: - Ltac numerical_names ::= numerical_names_sufx *) -Ltac numerical_names := fail. +Ltac2 build_name (l:string list): string := build_name_gen "_" add_prefix add_suffix (List.rev l). -(** This determines the depth of the recursive analysis of a type to - compute the corresponding hypothesis name. generally 2 or 3 is - enough. More gives too log names, less may give identical names - too often. *) -Ltac rename_depth := constr:(3). +Ltac2 string_of_int (i:int) := Message.to_string (Message.of_int i). -(** Default prefix for hypothesis names. *) -Ltac default_prefix :=constr:(forall h, DUMMY h). -(** A few special default chunks, for special cases in the naming heuristic. *) -Ltac impl_prefix := constr:(forall _impl, DUMMY _impl). -Ltac forall_prefix := constr:(forall _all, DUMMY _all). -Ltac exists_prefix := constr:(forall _ex, DUMMY _ex). -(** This is the customizable naming tactic that the user should - REDEFINE along his development. See above for an example of such - redefinition. It should always fail when no name suggestion is - found, to give a chance to the default naming scheme to apply. *) +Ltac2 string_forall (p:char -> bool) (s:string) : bool := + let rec check i := + if Int.ge i (String.length s) then true + else if p (String.get s i) then check (Int.add 1 i) else false + in + check 0. - Ltac rename_hyp stop th := fail. -(* ************************************** *) +Ltac2 codepercent():int := (Char.to_int (String.get "%" 0)). +Ltac2 code0() := Char.to_int (String.get "0" 0). +Ltac2 code9() := Char.to_int (String.get "9" 0). +Ltac2 is_digit (c:char): bool := + let code := Char.to_int c in + Bool.and (Int.le (code0()) code) (Int.le code (code9())). -(** Builds an id from a sequence of chunks. fresh is not supposed to - add suffixes anywhere because all the ids we use start with "_". - As long as no constant or hyp name start with "_" it is ok. *) -Ltac build_name_gen suffx l := - let l := eval lazy beta delta [List.app] iota in l in - match l with - | nil => fail - | (forall id1:Prop, DUMMY id1)::nil => - match suffx with - | true => fresh id1 "_" - | false => fresh id1 - end - | (forall id1:Prop, DUMMY id1)::?l' => - let recres := build_name_gen suffx l' in - (* id1 starts with "_", so fresh do not add any suffix *) - let res := fresh id1 recres in - res - end. +Ltac2 string_first (p:char -> bool) (s:string) : int := + let lgth := String.length s in + let rec count i := + if Int.ge i lgth then i + else if p (String.get s i) then i + else count (Int.add 1 i) + in + count 0. -Ltac build_name l := build_name_gen add_suffix l. -Ltac build_name_no_suffix l := build_name_gen constr:(false) l. +Ltac2 Eval (string_first (fun c => Int.equal (Char.to_int c) (codepercent())) "xxxcc"). +Ltac2 string_shorten_percent (s:string) : string := + let lgth := String.length s in + let i := string_first (fun c => Int.equal (Char.to_int c) (codepercent())) s in + String.sub s 0 i. -(** Check if t is an eligible argument for fresh function. For instance - if t is (forall foo, ...), it is not eligible. *) -Ltac freshable t := - let x := fresh t "_dummy_sufx" in - idtac. - + (** Generate fresh name for numerical constants. Warning: problem here: hyps names may end with a digit: Coq may @@ -145,436 +156,711 @@ Ltac freshable t := this, you should switch to "Ltac add_suffix ::= constr:(true)." so that every hyp name ends with "_", so that coq never mangle with the digits *) -Ltac numerical_names_nosufx t := - match t with - | 0%Z => fresh "_0" - | 1%Z => fresh "_1" - | 2%Z => fresh "_2" - | 3%Z => fresh "_3" - | 4%Z => fresh "_4" - | 5%Z => fresh "_5" - | 6%Z => fresh "_6" - | 7%Z => fresh "_7" - | 8%Z => fresh "_8" - | 9%Z => fresh "_9" - | 10%Z => fresh "_10" - (* | Z0 => fresh "_0" *) - | O%nat => fresh "_0" - | 1%nat => fresh "_1" - | 2%nat => fresh "_2" - | 3%nat => fresh "_3" - | 4%nat => fresh "_4" - | 5%nat => fresh "_5" - | 6%nat => fresh "_6" - | 7%nat => fresh "_7" - | 8%nat => fresh "_8" - | 9%nat => fresh "_9" - | 10%nat => fresh "_10" - | O%N => fresh "_0" - | 1%N => fresh "_1" - | 2%N => fresh "_2" - | 3%N => fresh "_3" - | 4%N => fresh "_4" - | 5%N => fresh "_5" - | 6%N => fresh "_6" - | 7%N => fresh "_7" - | 8%N => fresh "_8" - | 9%N => fresh "_9" - | 10%N => fresh "_10" - end. -Ltac numerical_names_sufx t := - match t with - | 0%Z => fresh "_0z" - | 1%Z => fresh "_1z" - | 2%Z => fresh "_2z" - | 3%Z => fresh "_3z" - | 4%Z => fresh "_4z" - | 5%Z => fresh "_5z" - | 6%Z => fresh "_6z" - | 7%Z => fresh "_7z" - | 8%Z => fresh "_8z" - | 9%Z => fresh "_9z" - | 10%Z => fresh "_10z" - (* | Z0 => fresh "_0" *) - | O%nat => fresh "_0n" - | 1%nat => fresh "_1n" - | 2%nat => fresh "_2n" - | 3%nat => fresh "_3n" - | 4%nat => fresh "_4n" - | 5%nat => fresh "_5n" - | 6%nat => fresh "_6n" - | 7%nat => fresh "_7n" - | 8%nat => fresh "_8n" - | 9%nat => fresh "_9n" - | 10%nat => fresh "_10n" - | O%N => fresh "_0N" - | 1%N => fresh "_1N" - | 2%N => fresh "_2N" - | 3%N => fresh "_3N" - | 4%N => fresh "_4N" - | 5%N => fresh "_5N" - | 6%N => fresh "_6N" - | 7%N => fresh "_7N" - | 8%N => fresh "_8N" - | 9%N => fresh "_9N" - | 10%N => fresh "_10N" +(* FIXME: this relies on printf to build a string from a constr in + nat, Z and N. It feels wrong. *) +Ltac2 build_numerical_name (t:constr):string := + let s := Message.to_string (fprintf "%t" t) in + let s := string_shorten_percent s in (* remove trailing "%scope" *) + if string_forall is_digit s + then if Bool.neg numerical_sufx then s + else + let typ := Constr.type t in + match! typ with + | Z => String.app s "z" + | nat => String.app s "n" + | N => String.app s "N" + end + else backtrack "numerical_names_nosufx". + + +(* FIXME: find something better to detect implicits!! *) +(* Determines the number of non "head" implicit arguments, i.e. implicit + arguments that are before any explicit one. This shall be ignored + when naming an application. This is done in very ugly way. Any + better solution welcome. *) +Ltac2 count_impl th := + (* match Unsafe.kind th with | App _ args => Array.length args | _ => 0 end. *) + match Unsafe.kind th with + | App _ _ => + lazy_match! th with + | (?z _ _ _ _ _ _ _ _ _ _ _) => + match! th with + | _ => let _ := constr:(fun a b c d e f g h i j k => ($z a b c d e f g h i j k , $z _ _ _ _ _ _ _ _ _ _ k)) in 1 + | _ => let _ := constr:(fun a b c d e f g h i j k => ($z a b c d e f g h i j k , $z _ _ _ _ _ _ _ _ _ j k)) in 2 + | _ => let _ := constr:(fun a b c d e f g h i j k => ($z a b c d e f g h i j k , $z _ _ _ _ _ _ _ _ i j k)) in 3 + | _ => let _ := constr:(fun a b c d e f g h i j k => ($z a b c d e f g h i j k , $z _ _ _ _ _ _ _ h i j k)) in 4 + | _ => let _ := constr:(fun a b c d e f g h i j k => ($z a b c d e f g h i j k , $z _ _ _ _ _ _ g h i j k)) in 5 + | _ => let _ := constr:(fun a b c d e f g h i j k => ($z a b c d e f g h i j k , $z _ _ _ _ _ f g h i j k)) in 6 + | _ => let _ := constr:(fun a b c d e f g h i j k => ($z a b c d e f g h i j k , $z _ _ _ _ e f g h i j k)) in 7 + | _ => let _ := constr:(fun a b c d e f g h i j k => ($z a b c d e f g h i j k , $z _ _ _ d e f g h i j k)) in 8 + | _ => let _ := constr:(fun a b c d e f g h i j k => ($z a b c d e f g h i j k , $z _ _ c d e f g h i j k)) in 9 + | _ => let _ := constr:(fun a b c d e f g h i j k => ($z a b c d e f g h i j k , $z _ b c d e f g h i j k)) in 10 + | _ => let _ := constr:(fun a b c d e f g h i j k => ($z a b c d e f g h i j k , $z a b c d e f g h i j k)) in 11 + end + | (?z _ _ _ _ _ _ _ _ _ _) => + match! th with + | _ => let _ := constr:(fun b c d e f g h i j k => ($z b c d e f g h i j k , $z _ _ _ _ _ _ _ _ _ k)) in 1 + | _ => let _ := constr:(fun b c d e f g h i j k => ($z b c d e f g h i j k , $z _ _ _ _ _ _ _ _ j k)) in 2 + | _ => let _ := constr:(fun b c d e f g h i j k => ($z b c d e f g h i j k , $z _ _ _ _ _ _ _ i j k)) in 3 + | _ => let _ := constr:(fun b c d e f g h i j k => ($z b c d e f g h i j k , $z _ _ _ _ _ _ h i j k)) in 4 + | _ => let _ := constr:(fun b c d e f g h i j k => ($z b c d e f g h i j k , $z _ _ _ _ _ g h i j k)) in 5 + | _ => let _ := constr:(fun b c d e f g h i j k => ($z b c d e f g h i j k , $z _ _ _ _ f g h i j k)) in 6 + | _ => let _ := constr:(fun b c d e f g h i j k => ($z b c d e f g h i j k , $z _ _ _ e f g h i j k)) in 7 + | _ => let _ := constr:(fun b c d e f g h i j k => ($z b c d e f g h i j k , $z _ _ d e f g h i j k)) in 8 + | _ => let _ := constr:(fun b c d e f g h i j k => ($z b c d e f g h i j k , $z _ c d e f g h i j k)) in 9 + | _ => let _ := constr:(fun b c d e f g h i j k => ($z b c d e f g h i j k , $z b c d e f g h i j k)) in 10 + end + | (?z _ _ _ _ _ _ _ _ _) => + match! th with + | _ => let _ := constr:(fun c d e f g h i j k => ($z c d e f g h i j k , $z _ _ _ _ _ _ _ _ k)) in 1 + | _ => let _ := constr:(fun c d e f g h i j k => ($z c d e f g h i j k , $z _ _ _ _ _ _ _ j k)) in 2 + | _ => let _ := constr:(fun c d e f g h i j k => ($z c d e f g h i j k , $z _ _ _ _ _ _ i j k)) in 3 + | _ => let _ := constr:(fun c d e f g h i j k => ($z c d e f g h i j k , $z _ _ _ _ _ h i j k)) in 4 + | _ => let _ := constr:(fun c d e f g h i j k => ($z c d e f g h i j k , $z _ _ _ _ g h i j k)) in 5 + | _ => let _ := constr:(fun c d e f g h i j k => ($z c d e f g h i j k , $z _ _ _ f g h i j k)) in 6 + | _ => let _ := constr:(fun c d e f g h i j k => ($z c d e f g h i j k , $z _ _ e f g h i j k)) in 7 + | _ => let _ := constr:(fun c d e f g h i j k => ($z c d e f g h i j k , $z _ d e f g h i j k)) in 8 + | _ => let _ := constr:(fun c d e f g h i j k => ($z c d e f g h i j k , $z c d e f g h i j k)) in 9 + end + | (?z _ _ _ _ _ _ _ _) => + match! th with + | _ => let _ := constr:(fun d e f g h i j k => ($z d e f g h i j k , $z _ _ _ _ _ _ _ k)) in 1 + | _ => let _ := constr:(fun d e f g h i j k => ($z d e f g h i j k , $z _ _ _ _ _ _ j k)) in 2 + | _ => let _ := constr:(fun d e f g h i j k => ($z d e f g h i j k , $z _ _ _ _ _ i j k)) in 3 + | _ => let _ := constr:(fun d e f g h i j k => ($z d e f g h i j k , $z _ _ _ _ h i j k)) in 4 + | _ => let _ := constr:(fun d e f g h i j k => ($z d e f g h i j k , $z _ _ _ g h i j k)) in 5 + | _ => let _ := constr:(fun d e f g h i j k => ($z d e f g h i j k , $z _ _ f g h i j k)) in 6 + | _ => let _ := constr:(fun d e f g h i j k => ($z d e f g h i j k , $z _ e f g h i j k)) in 7 + | _ => let _ := constr:(fun d e f g h i j k => ($z d e f g h i j k , $z d e f g h i j k)) in 8 + end + | (?z _ _ _ _ _ _ _) => + match! th with + | _ => let _ := constr:(fun e f g h i j k => ($z e f g h i j k , $z _ _ _ _ _ _ k)) in 1 + | _ => let _ := constr:(fun e f g h i j k => ($z e f g h i j k , $z _ _ _ _ _ j k)) in 2 + | _ => let _ := constr:(fun e f g h i j k => ($z e f g h i j k , $z _ _ _ _ i j k)) in 3 + | _ => let _ := constr:(fun e f g h i j k => ($z e f g h i j k , $z _ _ _ h i j k)) in 4 + | _ => let _ := constr:(fun e f g h i j k => ($z e f g h i j k , $z _ _ g h i j k)) in 5 + | _ => let _ := constr:(fun e f g h i j k => ($z e f g h i j k , $z _ f g h i j k)) in 6 + | _ => let _ := constr:(fun e f g h i j k => ($z e f g h i j k , $z e f g h i j k)) in 7 + end + | (?z _ _ _ _ _ _) => + match! th with + | _ => let _ := constr:(fun f g h i j k => ($z f g h i j k , $z _ _ _ _ _ k)) in 1 + | _ => let _ := constr:(fun f g h i j k => ($z f g h i j k , $z _ _ _ _ j k)) in 2 + | _ => let _ := constr:(fun f g h i j k => ($z f g h i j k , $z _ _ _ i j k)) in 3 + | _ => let _ := constr:(fun f g h i j k => ($z f g h i j k , $z _ _ h i j k)) in 4 + | _ => let _ := constr:(fun f g h i j k => ($z f g h i j k , $z _ g h i j k)) in 5 + | _ => let _ := constr:(fun f g h i j k => ($z f g h i j k , $z f g h i j k)) in 6 + end + | (?z _ _ _ _ _) => + match! th with + | _ => let _ := constr:(fun g h i j k => ($z g h i j k , $z _ _ _ _ k)) in 1 + | _ => let _ := constr:(fun g h i j k => ($z g h i j k , $z _ _ _ j k)) in 2 + | _ => let _ := constr:(fun g h i j k => ($z g h i j k , $z _ _ i j k)) in 3 + | _ => let _ := constr:(fun g h i j k => ($z g h i j k , $z _ h i j k)) in 4 + | _ => let _ := constr:(fun g h i j k => ($z g h i j k , $z g h i j k)) in 5 + end + | (?z _ _ _ _) => + match! th with + | _ => let _ := constr:(fun h i j k => ($z h i j k , $z _ _ _ k)) in 1 + | _ => let _ := constr:(fun h i j k => ($z h i j k , $z _ _ j k)) in 2 + | _ => let _ := constr:(fun h i j k => ($z h i j k , $z _ i j k)) in 3 + | _ => let _ := constr:(fun h i j k => ($z h i j k , $z h i j k)) in 4 + end + | (?z _ _ _) => + match! th with + | _ => let _ := constr:(fun a b c => ($z a b c, $z _ _ c)) in 1 + | _ => let _ := constr:(fun a b c => ($z a b c, $z _ b c)) in 2 + | _ => let _ := constr:(fun a b c => ($z a b c, $z a b c)) in 3 + end + | (?z _ _) => + match! th with + | _ => let _ := constr:(fun a b => ($z a b, $z _ b)) in 1 + | _ => let _ := constr:(fun a b => ($z a b, $z a b)) in 2 + end + | (?z _) => + match! th with + | _ => let _ := constr:(fun b => ($z b, $z _)) in 0 + | _ => let _ := constr:(fun b => ($z b, $z b)) in 1 + end + end + | _ => 0 end. -(* Default value, see above for another possible one. -Ltac numerical_names ::= numerical_names_sufx *) -Ltac numerical_names ::= numerical_names_nosufx. - -Ltac raw_name X := (constr:((forall X, DUMMY X) :: [])). + +Ltac2 arobase():char := (Char.of_int 64). + (** Build a chunk from a simple term: either a number or a freshable term. *) -Ltac box_name t := - let id_ := - match t with - | _ => numerical_names t - | _ => - let _ := freshable t in - fresh "_" t +Ltac2 box_name t : string := + (* Hackish? *) + let s:string := Message.to_string (fprintf "%t" t) in + let s := if Char.equal (String.get s 0) (arobase()) + then String.sub s 1 (Int.sub (String.length s) 1) + else s in + match Ident.of_string s with + | Some _ => s + | None => + match Unsafe.kind t with + | Unsafe.Constant cstt _ => + let id:ident := List.last (Env.path (Std.ConstRef cstt)) in + Ident.to_string id + | Unsafe.Var id => Ident.to_string id + | Unsafe.Ind _ _ => + (* printf "IND: %t" t; *) + let s:string := Message.to_string (fprintf "%t" t) in + let s := if Char.equal (String.get s 0) (arobase()) + then String.sub s 1 (Int.sub (String.length s) 1) + else s in + s + | _ => build_numerical_name t end - in constr:(forall id_:Prop, DUMMY id_). - - -(** This will later contain a few default fallback naming strategy. *) -Ltac rename_hyp_default stop th := - fail. - -Ltac decr n := - match n with - | S ?n' => n' - | 0 => 0 end. -(* This computes the way we decrement our depth counter when we go - inside of t. For now we forget the idea of traversing Prop sorted - terms indefinitely. It gives too long names. *) -Ltac nextlevel n t := - let tt := type of t in - match tt with - (* | Prop => n *) - | _ => decr n - end. - - -(* Determines the number of "head" implicit arguments, i.e. implicit - arguments that are before any explicit one. This shall be ignored - when naming an application. This is done in very ugly way. Any - better solution welcome. *) -Ltac count_impl th := - lazymatch th with - | (?z ?a ?b ?c ?d ?e ?f ?g ?h ?i ?j ?k) => - match th with - | _ => let foo := constr:(z _ _ _ _ _ _ _ _ _ _ k) in constr:(1%nat) - | _ => let foo := constr:(z _ _ _ _ _ _ _ _ _ j k) in constr:(2%nat) - | _ => let foo := constr:(z _ _ _ _ _ _ _ _ i j k) in constr:(3%nat) - | _ => let foo := constr:(z _ _ _ _ _ _ _ h i j k) in constr:(4%nat) - | _ => let foo := constr:(z _ _ _ _ _ _ g h i j k) in constr:(5%nat) - | _ => let foo := constr:(z _ _ _ _ _ f g h i j k) in constr:(6%nat) - | _ => let foo := constr:(z _ _ _ _ e f g h i j k) in constr:(7%nat) - | _ => let foo := constr:(z _ _ _ d e f g h i j k) in constr:(8%nat) - | _ => let foo := constr:(z _ _ c d e f g h i j k) in constr:(9%nat) - | _ => let foo := constr:(z _ b c d e f g h i j k) in constr:(10%nat) - | _ => let foo := constr:(z a b c d e f g h i j k) in constr:(10%nat) - end - | (?z ?b ?c ?d ?e ?f ?g ?h ?i ?j ?k) => - match th with - | _ => let foo := constr:(z _ _ _ _ _ _ _ _ _ k) in constr:(1%nat) - | _ => let foo := constr:(z _ _ _ _ _ _ _ _ j k) in constr:(2%nat) - | _ => let foo := constr:(z _ _ _ _ _ _ _ i j k) in constr:(3%nat) - | _ => let foo := constr:(z _ _ _ _ _ _ h i j k) in constr:(4%nat) - | _ => let foo := constr:(z _ _ _ _ _ g h i j k) in constr:(5%nat) - | _ => let foo := constr:(z _ _ _ _ f g h i j k) in constr:(6%nat) - | _ => let foo := constr:(z _ _ _ e f g h i j k) in constr:(7%nat) - | _ => let foo := constr:(z _ _ d e f g h i j k) in constr:(8%nat) - | _ => let foo := constr:(z _ c d e f g h i j k) in constr:(9%nat) - | _ => let foo := constr:(z b c d e f g h i j k) in constr:(10%nat) - end - | (?z ?c ?d ?e ?f ?g ?h ?i ?j ?k) => - match th with - | _ => let foo := constr:(z _ _ _ _ _ _ _ _ k) in constr:(1%nat) - | _ => let foo := constr:(z _ _ _ _ _ _ _ j k) in constr:(2%nat) - | _ => let foo := constr:(z _ _ _ _ _ _ i j k) in constr:(3%nat) - | _ => let foo := constr:(z _ _ _ _ _ h i j k) in constr:(4%nat) - | _ => let foo := constr:(z _ _ _ _ g h i j k) in constr:(5%nat) - | _ => let foo := constr:(z _ _ _ f g h i j k) in constr:(6%nat) - | _ => let foo := constr:(z _ _ e f g h i j k) in constr:(7%nat) - | _ => let foo := constr:(z _ d e f g h i j k) in constr:(8%nat) - | _ => let foo := constr:(z c d e f g h i j k) in constr:(9%nat) - end - | (?z ?d ?e ?f ?g ?h ?i ?j ?k) => - match th with - | _ => let foo := constr:(z _ _ _ _ _ _ _ k) in constr:(1%nat) - | _ => let foo := constr:(z _ _ _ _ _ _ j k) in constr:(2%nat) - | _ => let foo := constr:(z _ _ _ _ _ i j k) in constr:(3%nat) - | _ => let foo := constr:(z _ _ _ _ h i j k) in constr:(4%nat) - | _ => let foo := constr:(z _ _ _ g h i j k) in constr:(5%nat) - | _ => let foo := constr:(z _ _ f g h i j k) in constr:(6%nat) - | _ => let foo := constr:(z _ e f g h i j k) in constr:(7%nat) - | _ => let foo := constr:(z d e f g h i j k) in constr:(8%nat) - end - | (?z ?e ?f ?g ?h ?i ?j ?k) => - match th with - | _ => let foo := constr:(z _ _ _ _ _ _ k) in constr:(1%nat) - | _ => let foo := constr:(z _ _ _ _ _ j k) in constr:(2%nat) - | _ => let foo := constr:(z _ _ _ _ i j k) in constr:(3%nat) - | _ => let foo := constr:(z _ _ _ h i j k) in constr:(4%nat) - | _ => let foo := constr:(z _ _ g h i j k) in constr:(5%nat) - | _ => let foo := constr:(z _ f g h i j k) in constr:(6%nat) - | _ => let foo := constr:(z e f g h i j k) in constr:(7%nat) - end - | (?z ?f ?g ?h ?i ?j ?k) => - match th with - | _ => let foo := constr:(z _ _ _ _ _ k) in constr:(1%nat) - | _ => let foo := constr:(z _ _ _ _ j k) in constr:(2%nat) - | _ => let foo := constr:(z _ _ _ i j k) in constr:(3%nat) - | _ => let foo := constr:(z _ _ h i j k) in constr:(4%nat) - | _ => let foo := constr:(z _ g h i j k) in constr:(5%nat) - | _ => let foo := constr:(z f g h i j k) in constr:(6%nat) - end - | (?z ?g ?h ?i ?j ?k) => - match th with - | _ => let foo := constr:(z _ _ _ _ k) in constr:(1%nat) - | _ => let foo := constr:(z _ _ _ j k) in constr:(2%nat) - | _ => let foo := constr:(z _ _ i j k) in constr:(3%nat) - | _ => let foo := constr:(z _ h i j k) in constr:(4%nat) - | _ => let foo := constr:(z g h i j k) in constr:(5%nat) - end - | (?z ?h ?i ?j ?k) => - match th with - | _ => let foo := constr:(z _ _ _ k) in constr:(1%nat) - | _ => let foo := constr:(z _ _ j k) in constr:(2%nat) - | _ => let foo := constr:(z _ i j k) in constr:(3%nat) - | _ => let foo := constr:(z h i j k) in constr:(4%nat) - end - | (?z ?i ?j ?k) => - match th with - | _ => let foo := constr:(z _ _ k) in constr:(1%nat) - | _ => let foo := constr:(z _ j k) in constr:(2%nat) - | _ => let foo := constr:(z i j k) in constr:(3%nat) - end - | (?z ?j ?k) => - match th with - | _ => let foo := constr:(z _ k) in constr:(1%nat) - | _ => let foo := constr:(z j k) in constr:(2%nat) - end - | (?z ?j) => constr:(1%nat) - | _ => constr:(0%nat) +Local Ltac2 is_dep_prod (t:constr): bool := + match kind t with + | Prod _ subt => Bool.neg (is_closed subt) + | _ => false end. +Ltac2 is_hyp (id:ident) := + let hyps := Control.hyps () in + List.exist (fun (x,_,_) => Ident.equal id x) hyps. (** Default naming of an application: we name the function if possible or fail, then we name all parameters that can be named either recursively or simply. Parameters at positions below nonimpl are - considered implicit and not considered. *) -Ltac rename_app nonimpl stop acc th := - match th with - | ?f => let f'' := box_name f in - constr:(f''::acc) - | (?f ?x) => - match nonimpl with - | (S ?nonimpl') => - let newstop := nextlevel stop x in - let namex := match true with - | _ => fallback_rename_hyp newstop x - | _ => constr:(@nil Prop) - end in - let newacc := constr:(namex ++ acc) in - rename_app nonimpl' stop newacc f - | 0%nat => (* don't consider this (implicit) argument *) - rename_app nonimpl stop acc f + ignored as implicits. *) +Ltac2 rec rename_app (nonimpl:int) (stop:int) (acc:string list ref) th: unit := + Control.once_plus (fun () => let s := box_name th in + Ref.set acc (s:: Ref.get acc)) + (fun _ => + match Unsafe.kind th with + | App f args => + (* control_try? *) + (let fun_name:string := box_name f in + Ref.set acc (fun_name:: Ref.get acc)); + let newstop:int := Int.sub stop 1 in + let nonimplicitsargs := Array.sub args (Int.sub (Array.length args) nonimpl) nonimpl in + Array.iter (fun arg => (fallback_rename_hyp newstop acc arg)) nonimplicitsargs + | _ => control_try (fun() => Ref.set acc (box_name th :: Ref.get acc)) + end) + + (** ** Calls the (user-defined) rename_hyp + and fallbacks to some default + namings if needed. [h] is the hypothesis (ident) to rename, [th] is its + type. *) +with rename_hyp_chained_quantifs stop (acc:string list ref) (th:constr) : unit := + let _newstop := Int.sub stop 1 in + match Unsafe.kind th with + | Prod bnd subth => + if is_dep_prod th + then + let nme:ident := Option.get(Binder.name bnd) in + let typ := Binder.type bnd in + (* If there is already a hyp named nme, we rename it so that the + 'in_context nme ...' below does not fail. We could rename the + other way around but we prefer keeping the name found in the + binder. *) + (if is_hyp nme then Std.rename [(nme , Fresh.in_goal nme)] else ()) ; + (* Ref.set acc (Ident.to_string nme :: Ref.get acc); *) + let tac_under_binder := + fun () => + let nme_c:constr := Unsafe.make (Var(nme)) in + let subth' := Constr.Unsafe.substnl [nme_c] 0 subth in + rename_hyp_chained_quantifs stop acc subth' in + (in_context nme typ tac_under_binder); + () + else + rename_hyp_chained_quantifs stop acc subth + | _ => fallback_rename_hyp stop acc th end - | _ => constr:(@nil Prop) - end - -(* Go under binder and rebuild a term with a good name inside, - catchable by a match context. *) -with build_dummy_quantified stop th := - lazymatch th with - | forall __z:?A , ?B => - constr:( - fun __z:A => - ltac:( - let th' := constr:((fun __z => B) __z) in - let th' := eval lazy beta in th' in - let res := build_dummy_quantified stop th' in - exact res)) - | ex ?f => - match f with - | (fun __z:?A => ?B) => - constr:( - fun __z:A => - ltac:( - let th' := constr:((fun __z => B) __z) in - let th' := eval lazy beta in th' in - let res := build_dummy_quantified stop th' in - exact res)) + +with fallback_rename_hyp_quantif stop (acc:string list ref) (th:constr) : unit := + let newstop := Int.sub stop 1 in + match Unsafe.kind th with + | Prod bnd subth => + if is_dep_prod th + then + let nme:ident := Option.get(Binder.name bnd) in + let typ := Binder.type bnd in + (* If there is already a hyp named nme, we rename it so that the + 'in_context nme ...' below does not fail. We could rename the + other way around but we prefer keeping the name found in the + binder. *) + (if is_hyp nme then Std.rename [(nme , Fresh.in_goal nme)] else ()) ; + Ref.set acc ((*Ident.to_string nme ::*) forall_prefix() :: Ref.get acc); + let tac_under_binder := + fun () => + let nme_c:constr := Unsafe.make (Var(nme)) in + let subth' := Constr.Unsafe.substnl [nme_c] 0 subth in + rename_hyp_chained_quantifs newstop acc subth' in + (in_context nme typ tac_under_binder); + () + + else + (Ref.set acc (impl_prefix() :: Ref.get acc); + rename_hyp_chained_quantifs newstop acc subth) + | App f args => + match Unsafe.kind f, Unsafe.kind constr:(@Init.Logic.ex) with + | Ind ind _, Ind ind' _ => + if Ind.equal ind ind' + then ( + Ref.set acc ((*Ident.to_string a ::*) exists_prefix() :: Ref.get acc); + match Unsafe.kind (Array.get args 1) with + | Lambda _bnd subth => rename_hyp_chained_quantifs newstop acc subth + | _ => backtrack "not exist" + end) + else backtrack "not exist" + | _ => backtrack "not exist" end - | _ => fallback_rename_hyp stop th - end + | _ => backtrack "no quantif" + end -(** ** Calls the (user-defined) rename_hyp + and fallbacks to some - default namings if needed. [h] is the hypothesis (ident) to - rename, [th] is its type. *) - -with fallback_rename_hyp_quantif stop th := - let prefx := - match th with - | ?A -> ?B => impl_prefix - | forall _ , _ => forall_prefix - | ex (fun _ => _) => exists_prefix - | _ => fail - end in - let newstop := decr stop in - (* sufx_buried contains a list of dummies *) - let sufx_buried := build_dummy_quantified newstop th in - (* FIXME: a bit fragile *) - let sufx_buried' := eval lazy beta delta [List.app] iota in sufx_buried in - let sufx := - match sufx_buried' with - | context [ (@cons Prop ?x ?y)] => constr:(x::y) - end - in - constr:(prefx::sufx) - -with fallback_rename_hyp_specials stop th := - let newstop := decr stop in - match th with - (* First see if user has something that applies *) - | _ => rename_hyp newstop th - (* if it fails try default specials *) - | _ => rename_hyp_default newstop th - end - -with fallback_rename_hyp stop th := - match stop with - (*| 0 => constr:(cons ltac:(box_name th) nil)*) - | 0 => constr:(@nil Prop) - | S ?n => - match th with - | _ => fallback_rename_hyp_specials stop th - | _ => fallback_rename_hyp_quantif stop th - | _ => - (*let newstop := nextlevel stop th in*) - let numnonimpl := count_impl th in - rename_app numnonimpl stop (@nil Prop) th - end - end. - -(** * Notation to define specific naming strategy *) -Declare Scope autonaming_scope. -(** Notation to build a singleton chunk list *) - -(* from coq-8.13 we should use name instead of ident. But let us wait - a few versions before this change. *) -Notation "'`' idx '`'" := (@cons Prop (forall idx:Prop, DUMMY idx) (@nil Prop)) - (at level 1,idx name,only parsing): autonaming_scope. - - -(** Notation to call naming on a term X, with a given depth n. *) -Notation " X '#' n " := ltac:( - let c := fallback_rename_hyp n X in exact c) - (at level 1,X constr, only parsing): autonaming_scope. - -Notation " X '##' " := - ltac:(let c := raw_name X in exact c) - (at level 1,X constr, only parsing): autonaming_scope. - - -(** It is nicer to write name t than constr:t, see below. *) -Ltac name c := (constr:(c)). - - -(** * Default fallback renaming strategy - - (Re)defining it now that we have everything we need. *) -Local Open Scope autonaming_scope. -Ltac rename_hyp_default n th ::= - let res := - match th with - (* | (@eq _ ?x ?y) => name (`_eq` ++ x#n ++ y#n) *) - (* | Z.le ?A ?B => name (`_Zle` ++ A#n ++ B#n) *) - | ?x <> ?y => name ( `_neq` ++ x#(decr n) ++ y#(decr n)) - | @cons _ ?x (cons ?y ?l) => - match n with - | S ?n' => name (`_cons` ++ x#n ++ y#n ++ l#n') - | 0 => name (`_cons` ++ x#n) - end - | @cons _ ?x ?l => - match n with - | S ?n' => name (`_cons` ++ x#n ++ l#n') - | 0 => name (`_cons` ++ x#n) - end - | (@Some _ ?x) => name (x#(S n)) - | (@None _) => name (`_None`) - | _ => fail - end in - res. - -(* Call this in your own renaming scheme if you want the "hneg" prefix - on negated properties *) -Ltac rename_hyp_neg n th := - match th with - | ~ (_ = _) => fail 1(* h_neq already dealt by fallback *) - | ~ ?th' => name (`not` ++ th'#(S n)) - | _ => fail +with fallback_rename_hyp_specials stop (acc:string list ref) th :unit := + let newstop := Int.sub stop 1 in + let freeze := Ref.get acc in + Control.once_plus + (* First see if user has something that applies *) + (fun() => let dirs := rename_hyp newstop th in + interp_directives newstop acc (List.rev dirs) ) + (* if it fails try default specials *) + (fun _ => let dirs := rename_hyp_default newstop th in + Ref.set acc freeze; (* backtracking acc by hand here *) + interp_directives newstop acc (List.rev dirs)) + +with fallback_rename_hyp stop (acc:string list ref) th:unit := + if Int.le stop 0 then () + else + Control.once_plus (fun () => fallback_rename_hyp_specials stop acc th) + (fun _ => + lazy_match! th with + | forall _, _ => fallback_rename_hyp_quantif stop acc th + | exists _, _ => fallback_rename_hyp_quantif stop acc th + | _ => let numnonimpl := count_impl th in + let _ := rename_app numnonimpl stop acc th in + () + end) + +with interp_directives stop acc ld:unit := + List.fold_right (fun d _ => interp_directive stop acc d) ld () + +with interp_directive stop acc d := + (* printf "interp_directive %a %a" pr_acc (Ref.get acc) pr_directive d; *) + match d with + | String s => Ref.set acc (s :: (Ref.get acc)) + | Rename t => fallback_rename_hyp stop acc t + | RenameN n t => fallback_rename_hyp n acc t end. -Local Close Scope autonaming_scope. - -(* Entry point of the renaming code. *) -Ltac fallback_rename_hyp_name th := +(* Like in_context but then forget about the new goal. Only side effects are + kept *) +Ltac2 in_context_then_forget nme typ f := + Control.once_plus + (fun () => in_context nme typ f; backtrack "forget in_context subgoal") + (fun _ => ()). + +Ltac2 rename_acc n th := + let acc := Ref.ref [] in + (* We intentionally create a separate goal and backtrack it at the end. We + only keep the name stored in acc. *) + let dummy_nme := Option.get (Ident.of_string "DUMMY_SUBGOAL") in + in_context_then_forget dummy_nme constr:(Prop) (fun () => fallback_rename_hyp n acc th); + Ref.get acc. + +Ltac2 fallback_rename_hyp_name th: ident := let depth := rename_depth in - let h := constr:(ltac:(let x := default_prefix in exact x)) in - let l := fallback_rename_hyp depth th in + let l := rename_acc depth th in + (* printf "ICI10 : %a" pr_acc l; *) match l with - nil => fail 1 - | _ => let nme := build_name (h::l) in - fresh nme + [] => backtrack "No name built" + | _ => let nme := build_name l in + let id := Option.get (Ident.of_string nme) in + Fresh.in_goal id end. -(* Formating Error message *) -Inductive LHMsg t (h:t) := LHMsgC: LHMsg t h. - -Notation "h : t" := (LHMsgC t h) (at level 1,only printing, format -"'[ ' h ':' '/' '[' t ']' ']'"). - -Ltac rename_hyp_with_name h th := fail. - +(* This entry point is for really adhoc user renaming that need to inspect the +goal in depth. For instance itf the name of a variable depends on the presence +of some hypothesis. Currently unplugged.*) +Ltac2 rename_hyp_with_name h th := fail. (* Tactic renaming hypothesis H. Ignore Type-sorted hyps, fails if no renaming can be computed. Example of failing type: H:((fun x => True) true). *) -Ltac autorename_strict H := - match type of H with - | ?th => - match type of th with - | _ => - let l := rename_hyp_with_name H th in - let dummy_name := fresh "dummy" in - rename H into dummy_name; (* frees current name of H, in case of idempotency *) - let newname := build_name_no_suffix l in - rename dummy_name into newname - | Prop => - let dummy_name := fresh "dummy" in - rename H into dummy_name; (* frees current name of H, in case of idempotency *) +#[global] +Ltac2 autorename_strict (h:ident) := + let th := Constr.type (Control.hyp h) in + let tth := Constr.type th in + (* printf "th = %t" tth ; *) + lazy_match! tth with + (* TODO: the deep entry point *) + (* | _ => *) + (* let l := rename_hyp_with_name $h th in *) + (* let dummy_name := fresh "dummy" in *) + (* rename $h into dummy_name; (* frees current name of H, in case of idempotency *) *) + (* let newname := build_name_no_suffix l in *) + (* rename dummy_name into newname *) + | Prop => + let dummy_name := Fresh.in_goal (Option.get (Ident.of_string "dummy")) in + Std.rename [(h , dummy_name)]; (* frees current name of H, in case of idempotency *) let newname := fallback_rename_hyp_name th in - rename dummy_name into newname - | Prop => - let c := constr:(LHMsgC th H) in - fail 1 "no renaming pattern for " c (* "no renaming pattern for " H *) - | _ => idtac (* not in Prop or "no renaming pattern for " H *) - end + Std.rename [(dummy_name,newname)] + | Prop => + let msg := fprintf "no renaming pattern for %I : %t" h th in + backtrack (Message.to_string msg) + | _ => + if Constr.equal constr:(Prop) tth + then let msg := fprintf "no renaming pattern for %I : %t" h th in + backtrack (Message.to_string msg) + else () (* not in Prop or "no renaming pattern for " $h *) end. (* Tactic renaming hypothesis H. *) -Ltac autorename H := try autorename_strict H. +Local Ltac2 ltac2_autorename (h:ident) := + control_try (fun () => autorename_strict h). + +Ltac2 ltac1_autorename (h:Ltac1.t) := + let h: ident := Option.get (Ltac1.to_ident h) in + ltac2_autorename h. + +Ltac2 ltac1_autorename_strict (h:Ltac1.t) := + let h: ident := Option.get (Ltac1.to_ident h) in + autorename_strict h. + +Ltac2 rename_list l acc s := + List.iter (fun (n,t) => fallback_rename_hyp n acc t) l; + Ref.set acc (s :: (Ref.get acc)). + +End Ltac2. + +(* This is the default renaming hard-coded in LibHYps *) +Ltac2 Set rename_hyp_default := + fun n th => + if Int.lt n 0 then [] + else + lazy_match! th with + | ?x <> ?y => [ String "neq" ; Rename x ; Rename y ] + | (@Some _ ?x) => [RenameN (incr n) x] + | (@None _) => [String "None"] + end. + +(* This may be due to the definition of ltac1_autorename which uses + Ltac1.to_ident, but this is the only way I found to have + "autorename h" be callable from ltac1: make it a notation expecting + an ident, and then define a tactic using this notation. If I define + directly the tatic autorename instead of a notation, then it does + not accept "autorename id". *) +(* to reproduce: +Ltac2 ltac1_autorename (h:Ltac1.t) := + let h: ident := Option.get (Ltac1.to_ident h) in + ltac2_autorename h. + +Global Ltac autorename h := + let tac := ltac2:(h |- Ltac2.ltac1_autorename h) in + tac h. + +Goal 1 = 2 -> False. +Proof. + intros H. + autorename H. (* Ltac1.to_ident fails with Ltac2 exception: No_value *) + +More generally to reproduce: + +Ltac2 ltac2_mytac (id:ident) := printf "%I" id. + +Ltac2 ltac1_mytac (h:Ltac1.t) := + let h: ident := Option.get (Ltac1.to_ident h) in + ltac2_mytac h. + +Global Ltac mytac h := + let tac := ltac2:(h |- ltac1_mytac h) in + tac h. + +Local Set Default Proof Mode "Classic". + +Goal 1 = 2 -> False. +Proof. + intros H. + Fail mytac H. (* Ltac1.to_ident fails with Ltac2 exception: No_value *) +Abort. + +(* Solution *) +Tactic Notation "XXXmytac" hyp(h) := + let tac := ltac2:(h |- ltac1_mytac h) in + tac h. + +Ltac mytac' h := XXXmytac h. + + +Goal 1 = 2 -> False. +Proof. + intros H. + mytac' H. + +*) + + +Local Tactic Notation "Lautorename" hyp(h) := + let tac := ltac2:(h |- Ltac2.ltac1_autorename h) in + tac h. + +Global Ltac autorename h := Lautorename h. + +Local Tactic Notation "Lautorename_strict" hyp(h) := + let tac := ltac2:(h |- Ltac2.ltac1_autorename_strict h) in + tac h. +Global Ltac autorename_strict h := Lautorename_strict h. + +(* +(* ********** EXAMPLE CUSTOMIZATION ********** *) + +(* TESTS *) + +(* This settings should reproduce the naming scheme of libhypps-1.0.0 + and libhypps-1.0.1. *) +Ltac2 Set add_suffix := false. +Ltac2 Set numerical_sufx := true. + +(* This should maybe be by default *) +Ltac2 rename_hyp_1 n th := + if Int.lt n 0 then [] + else + lazy_match! th with + | @cons _ ?x (cons ?y ?l) => [String "cons"; Rename x; Rename y; RenameN (decr (decr n)) l] + | @cons _ ?x ?l => if Int.ge n 1 then [String "cons"; Rename x; RenameN (decr n) l] else [String "cons"] + end. + +(* From there this is LibHypTest from 1f7a1ed2289e439c291fcbd06c51705547feef1e *) +Ltac2 rename_hyp_2 n th := + match! th with + | true <> false => [String "tNEQf"] + | true = false => [String "tEQf"] + | _ => rename_hyp_1 n th (* call the previously defined tactic *) + end. + +Ltac2 Set rename_hyp := rename_hyp_2. + +(* Suppose I want to add later another naming rule: *) +Ltac2 rename_hyp_3 n th := + match! th with + | Nat.eqb ?x ?y = true => [String "Neqb" ; Rename x ; Rename y] + | true = Nat.eqb ?x ?y => [String "Neqb" ; Rename x ; Rename y] + | _ => rename_hyp_2 n th (* call the previously defined tactic *) + end. + +Ltac2 Set rename_hyp := rename_hyp_3. + +Ltac2 Set rename_depth := 3. +Import TacNewHyps.Notations. +Close Scope Z_scope. +Open Scope nat_scope. + +Lemma dummy: forall x y, + 0 <= 1 -> + (0%Z <= 1%Z)%Z -> + x <= y -> + x = y -> + Some x = Some y -> + 0 = 1 -> + 223 = 426 -> + (0 = 1)%Z -> + x <> y -> + Nat.eqb (x + 1) 0 <> Nat.eqb 1 y -> + true = Nat.eqb 3 4 -> + Nat.eqb (x + 3) 4 = true -> + Nat.eqb (2 * (x + 3)) 4 = true -> + true = Nat.leb 3 4 -> + 1 = 0 -> + ~x = y -> + ~1 < 0 -> + (forall w w':nat , w = w' -> ~true=false) -> + (forall w w':nat , w = w' -> true=false /\ True) -> + (forall w w':nat , w = w' -> False /\ True) -> + (exists w:nat , w = w -> ~(true=(andb false true)) /\ False) -> + (exists w:nat , w = w -> True /\ False) -> + (forall w w':nat , w = w' -> true=false) -> + (forall w w':nat , w = w' -> Nat.eqb 3 4=Nat.eqb 4 3) -> + List.length (cons 3 nil) = (fun x => 0)1 -> + List.length (cons 3 nil) = 0 -> + plus 0 y = y -> + (true=false) -> + (False -> (true=false)) -> + forall (x : nat) (env : list nat), + ~ List.In x nil -> + cons x (cons 3 env) = cons 2 env -> + forall z t:nat, IDProp -> + (0 < 1 -> 0 < 0 -> true = false -> ~(true=false)) -> + (~(true=false)) -> + (forall w w',w < w' -> ~(true=false)) -> + (0 < 1 -> ~(1<0)) -> + (0 < 1 -> 1<0) -> 0 < z -> True. +Proof. + intros x y H. + autorename H. + Undo 2. + intros;{ autorename }. + + match type of x with nat => idtac | _ => fail "test failed!" end. + match type of y with nat => idtac | _ => fail "test failed!" end. + match type of h_le_0n_1n with 0 <= 1 => idtac | _ => fail "test failed!" end. + match type of h_le_0z_1z with (0 <= 1)%Z => idtac | _ => fail "test failed!" end. + match type of h_le_x_y with x <= y => idtac | _ => fail "test failed!" end. + match type of h_eq_x_y with x = y => idtac | _ => fail "test failed!" end. + match type of h_eq_223n_426n with 223 = 426 => idtac | _ => fail "test failed!" end. + match type of h_eq_0n_1n with 0 = 1 => idtac | _ => fail "test failed!" end. + match type of h_eq_0z_1z with 0%Z = 1%Z => idtac | _ => fail "test failed!" end. + match type of h_neq_x_y with x <> y => idtac | _ => fail "test failed!" end. + match type of h_Neqb_3n_4n with true = (3 =? 4) => idtac | _ => fail "test failed!" end. + match type of h_Neqb_add_x_3n_4n with (x + 3 =? 4) = true => idtac | _ => fail "test failed!" end. + match type of h_Neqb_mul_2n_add_4n with (2 * (x + 3) =? 4) = true => idtac | _ => fail "test failed!" end. + match type of h_eq_true_leb_3n_4n with true = (3 <=? 4) => idtac | _ => fail "test failed!" end. + match type of h_eq_1n_0n with 1 = 0 => idtac | _ => fail "test failed!" end. + match type of h_neq_x_y0 with x <> y => idtac | _ => fail "test failed!" end. + match type of h_neq_eqb_add_0n_eqb_1n_y with (x + 1 =? 0) <> (1 =? y) => idtac | _ => fail "test failed!" end. + match type of h_not_lt_1n_0n with ~ 1 < 0 => idtac | _ => fail "test failed!" end. + match type of h_all_tNEQf with forall w w' : nat, w = w' -> true <> false => idtac | _ => fail "test failed!" end. + match type of h_all_and_tEQf_True with forall w w' : nat, w = w' -> true = false /\ True => idtac | _ => fail "test failed!" end. + match type of h_eq_cons_x0_3n_cons_2n with x0 :: 3 :: env = 2 :: env => idtac | _ => fail "test failed!" end. + + match type of h_all_and_False_True with forall w w' : nat, w = w' -> False /\ True => idtac | _ => fail "test failed!" end. + match type of h_ex_and_neq_False with exists w : nat, w = w -> true <> (false && true)%bool /\ False => idtac | _ => fail "test failed!" end. + match type of h_ex_and_True_False with exists w : nat, w = w -> True /\ False => idtac | _ => fail "test failed!" end. + match type of h_all_tEQf with forall w w' : nat, w = w' -> true = false => idtac | _ => fail "test failed!" end. + match type of h_all_eq_eqb_eqb with forall w w' : nat, w = w' -> (3 =? 4) = (4 =? 3) => idtac | _ => fail "test failed!" end. + (* match type of h_eq_length_cons_1n with length (3::nil) = (fun _ : nat => 0) 1 => idtac | _ => fail "test failed!" end. *) + match type of h_eq_length_cons_0n with length (3::nil) = 0 => idtac | _ => fail "test failed!" end. + match type of h_eq_add_0n_y_y with 0 + y = y => idtac | _ => fail "test failed!" end. + match type of h_tEQf with true = false => idtac | _ => fail "test failed!" end. + match type of h_impl_tEQf with False -> true = false => idtac | _ => fail "test failed!" end. + match type of x0 with nat => idtac | _ => fail "test failed!" end. + match type of env with list nat => idtac | _ => fail "test failed!" end. + match type of h_not_In_x0_nil with ~ In x0 nil => idtac | _ => fail "test failed!" end. + match type of h_eq_cons_x0_3n_cons_2n with x0 :: 3 :: env = 2 :: env => idtac | _ => fail "test failed!" end. + match type of h_IDProp with IDProp => idtac | _ => fail "test failed!" end. + match type of h_impl_tNEQf with 0 < 1 -> 0 < 0 -> true = false -> true <> false => idtac | _ => fail "test failed!" end. + match type of h_tNEQf with true <> false => idtac | _ => fail "test failed!" end. + match type of h_all_tNEQf0 with forall w w' : nat, w < w' -> true <> false => idtac | _ => fail "test failed!" end. + match type of h_impl_not_lt with 0 < 1 -> ~ 1 < 0 => idtac | _ => fail "test failed!" end. + match type of h_impl_lt_1n_0n with 0 < 1 -> 1 < 0 => idtac | _ => fail "test failed!" end. + match type of h_lt_0n_z with 0 < z => idtac | _ => fail "test failed!" end. + exact I. +Qed. + + + + + +(* Ltac autorename h := *) + (* let tac := ltac2:(h |- ltac2_autorename h) in *) + (* tac h. *) + + (* Unset Printing Notations. *) + +(* Ltac2 Eval (count_impl constr:(3 + 4)). *) + +Import TacNewHyps.Notations. +Parameters X Y: nat -> Prop. +Parameters PX: X 3. +Parameters PY: Y 3. + +Local Ltac rename_or_revert H := autorename_strict H + (try revert H). + +Goal forall [A : Type] (P Q : A -> Prop) (x : A), P x -> Q x -> (exists2 x : A, P x & Q x) -> ((fun x => x = x) 1) -> ex2 P Q -> False. + + intros A P Q x H H0 H1 HH H2. + + autorename H1. + autorename H2. + autorename H. + autorename H0. + Fail autorename_strict HH. + rename_or_revert HH. + intros ; { rename_or_revert }. + Fail intros ; { autorename_strict }. + + + ltac2:(let l := Ltac2.rename_acc 3 constr:(exists2 x0 : A, P x0 & Q x0) in + printf "BEFORE BUILDNAME %a " (pr_list pr_string) l; + let nme := Ltac2.build_name l in + printf "%s" nme). + + ltac2:(let l := Ltac2.rename_acc 9 constr:(ex2 P Q) in + printf "BEFORE BUILDNAME %a " (pr_list pr_string) l; + let nme := Ltac2.build_name l in + printf "%s" nme). +Abort. + +Definition foo := (fun a b:bool => a = b). + +Goal forall n m p : nat, forall b:bool, n m<= p -> True . +Proof. + intros n m p b H H0. + + assert (forall z, foo b z). + 2:{ } + + ltac2:(let l := rename_acc 4 constr:(forall b:nat, Nat.clearbit b 4%nat = 0) in + printf "BEFORE BUILDNAME"; + let nme := build_name l in + printf "%s" nme). + + Unset Printing Notations. + + + + + ltac2:(let l := rename_acc 9 constr:(Nat.clearbit n m = p) in + printf "BEFORE BUILDNAME %a " (pr_list pr_string) l; + let nme := build_name l in + printf "%s" nme). + + ltac2:(let l := rename_acc 3 constr:(Nat.clearbit 3 4%nat = 0) in + printf "BEFORE BUILDNAME"; + let nme := build_name l in + printf "%s" nme). + + ltac2:(let l := rename_acc 4 constr:(Nat.clearbit 3 4%nat = 0 -> Nat.clearbit 3 4%nat = 7) in + printf "BEFORE BUILDNAME"; + let nme := build_name l in + printf "%s" nme). + + ltac2:(let l := rename_acc 3 constr:(forall x:nat, Nat.clearbit x 4%nat = 0) in + printf "BEFORE BUILDNAME"; + let nme := build_name l in + printf "%s" nme). + + ltac2:(let l := rename_acc 3 constr:(forall b:nat, Nat.clearbit b 4%nat = 0) in + printf "BEFORE BUILDNAME"; + let nme := build_name l in + printf "%s" nme). + + + ltac2:(let l := rename_acc 4 constr:(forall b:nat, Nat.clearbit b 4%nat = 0) in + printf "BEFORE BUILDNAME"; + let nme := build_name l in + printf "%s" nme). + + ltac2:(let l := rename_acc 4 constr:(forall x:nat, Nat.clearbit x 4%nat = 0) in + printf "BEFORE BUILDNAME"; + let nme := build_name l in + printf "%s" nme). + + ltac2:(let l := rename_acc 4 constr:(forall x:Z, BinIntDef.Z.quot x x = 1%Z) in + printf "BEFORE BUILDNAME"; + let nme := build_name l in + printf "%s" nme). + + + ltac2:(let l := rename_acc 4 constr:(Nat.clearbit 3%nat 4%nat) in + let nme := build_name l in + printf "%s" nme). +Abort. + + +*) (* (* Tests *) @@ -586,9 +872,9 @@ Ltac rename_hyp1 n th := | ((?min <= ?x) /\ (?x <= ?max))%nat => name (x#n ++ `_bounded` ++ min#n ++ max#n) end. (* example of adhoc naming from hyp name: *) -Ltac rename_hyp_with_name h th ::= +Ltac rename_hyp_with_name $h th ::= match reverse goal with - | H: ?A = h |- _ => + | H: ?A = $h |- _ => name ( A## ++ `_same`) (* let _ := freshable A in *) (* name (`same_as` ++ A#1) *) diff --git a/LibHyps/LibHypsTactics.v b/LibHyps/LibHypsTactics.v index 3943acd..ca3c68e 100644 --- a/LibHyps/LibHypsTactics.v +++ b/LibHyps/LibHypsTactics.v @@ -5,317 +5,87 @@ Require Export LibHyps.TacNewHyps. Require Export LibHyps.LibHypsNaming. (* Require Export LibHyps.LibSpecialize. *) +Require Import Ltac2.Ltac2. +From Ltac2 Require Import Option Constr Printf. + +(* START DEBUG *) +(* +Require Import LibHypsDebug. -(* debug -Module Prgoal_Notation. - Ltac pr_goal := - match goal with - |- ?g => - let allh := all_hyps in - idtac "[" allh " ⊢ " g "]" - end. - Notation "X : Y ; Z" := (DCons Y X Z) (at level 1, Z at level 1, right associativity,only printing,format "'[v' X : Y ; '/' Z ']' ") . -End Prgoal_Notation. (* example: *) -Import Prgoal_Notation. Lemma test_espec2: forall x:nat, x = 1 -> (forall a y z:nat, a = 1 -> y = 1 -> z+y+a = 2 -> z+1 = x -> False) -> x > 1. Proof. intros x hx h_eqone. (* specevar h_eqone at y. *) - pr_goal. -pr_goal. -Abort. *) - -(* Default behaviour: generalize hypothesis that we failed to rename, - so that no automatic names are introduced by mistake. Of course one - can do "intros" to reintroduce them. - - Revert needs to be done in the other direction (so better do ";; - autorename ;!; revertHyp"), and may fail if something depends on - the reverted hyp. So we should revert everything depending on the - unrenamed hyp. *) -Ltac revert_if_norename H := - let t := type of H in - match type of t with - | Prop => match goal with - | _ => let x := fallback_rename_hyp_name t in idtac - (* since we are only in prop it is almost never the case - that something depends on H but if this happens we revert - everything that does. This needs testing. *) - | _ => try generalize dependent H - end - | _ => idtac - end. - -Ltac rename_or_revert H := autorename_strict H + revert H. - -(* Some usual tactics one may want to use with onNewHypsOf: *) -(* apply subst using H if possible. *) -(*Ltac substHyp H := - match type of H with - | ?x = ?y => move H at top; (* to ensure subst will take this hyp *) - once (subst x + subst y) - end. *) - -(* This is similar to subst x, but ensures that H and only H is used. - Even if there is another hyp with the same variable *) -Ltac substHyp H := - match type of H with - | Depl => fail 1 (* fail immediately, we are applying on a list of hyps. *) - | ?x = ?y => - (* subst would maybe subst using another hyp, so use replace to be sure *) - once ((is_var(x); replace x with y in *; [try clear x ; try clear H] ) - + (is_var(y); replace y with x in * ; [try clear y; try clear H])) - | _ => idtac - end. - -(* revert, fails if impossible, should not fail if hyps are ordered in the right order *) -Ltac revertHyp H := revert H. (* revert is a tactic notation, so we need to define this *) - -(* revert if subst fails. Never fail, be careful not to use this tactic in the - left member of a "+" tactical: *) -Ltac subst_or_revert H := try first [progress substHyp H | revert H]. - -(* try subst. Never fail, be careful to not use this tactic in the - left member of a "+" tactical: *) -Ltac subst_or_idtac H := substHyp H. - -Ltac map_tac tac lH := - lazymatch lH with - (DCons _ ?Hyp ?lH') => (try tac Hyp); map_tac tac lH' - | DNil => idtac - end. - -(* Naive variants for lists of hyps. We might want to optimize if - possible like group_up_list. *) -Ltac subst_or_revert_l := map_tac subst_or_revert. -Ltac subst_or_idtac_l := map_tac subst_or_idtac. -Ltac revertHyp_l := map_tac revertHyp. -Ltac substHyp_l := map_tac ltac:(fun x => try substHyp x) substHyp. -Ltac revert_if_norename_l := map_tac revert_if_norename. -Ltac autorename_l := map_tac autorename. - -(* Auto rename all hypothesis *) -Ltac rename_all_hyps := autorename_l all_hyps. - - - -(* return the lowest hyp with type T in segment lH. We suppose lH is -given lower-first. I.e. we return the first hyp of type T. *) -Ltac find_lowest_T T candidate lH := - lazymatch lH with - | (DCons T ?Hyp _) => Hyp - | (DCons _ ?Hyp ?lH') => find_lowest_T T candidate lH' - | _ => candidate - end. + (pr_goal()). +Abort. -(* Look into the cache for a hyp of type T. If found, returns the hyp - + the cache where hyp is deleted. *) -Ltac find_in_cache_T cache T := - lazymatch cache with - | DCons ?th ?h ?cache' => - match th with - | T => constr:((cache' , h)) - | _ => - let recres := find_in_cache_T cache' T in - match recres with - | (_,@None T) => constr:((cache,@None T)) - | (?newcache1,?res1) => constr:((DCons th h newcache1 , res1)) - end - end - | _ => constr:((cache,@None T)) - end. - -(* if T is not already present in cache, return the (cache + (h:T)), - otherwise return cache unchanged. *) -Ltac find_in_cache_update cache T h := - match find_in_cache_T cache T with - (?c , None) => constr:((DCons T h c , None)) - | (?c , ?res) => constr:((DCons T h c , res)) - end. - -(* Precondition: x must be "below" y at start *) -(* equivalent to move x before belowme but fails if x=bleowme. This - forces the pre-8.14 behaviour of move below. *) -Ltac move_above x y := - match constr:((x , y)) with - | (?c,?c) => idtac - | _ => move x after y - end. - -(* Precondition: x must be "below" y at start *) -(* equivalent to move x after belowme but fails if x=bleowme *) -Ltac move_below x y := - match constr:((x , y)) with - | (?c,?c) => idtac - | _ => move x before y - end. - - -(* move each hyp in lhyps either after the pivot hyp for its type -found in cache, or just above fstProp if there is no pivot. In this -second case we return a new cache with h as a new pivot. *) -(* Example -There is a number of "segments". A segment for type T is the first set -of consecutive variables of type T, located before the first -Prop-sorted hyp. For sintance there are 2 segments in the goal below, -one is x1-x3 and the other is b1-b2. - - x1 : nat - x2 : nat - x3 : nat <-- pivot for nat - b1 : bool - b2 : bool <-- pivot for bool - H : ... : Prop <-- fstProp - H2: ... : Prop not in lhyps - x : nat <-- in lhyps - b : bool <-- in lhyps - c : Z <-- in lhyps - ======= - ... - -This is described by the three arguments: - -- cache is (DCons bool b2 (DCons nat x3 DNil)) i.e. last variable of - each segment -- lhyps is (DCons nat x (DCons bool b (DCons Z c DNil))) list of - variable to move (may not contain all the badly place variables) -- fstProp is H. - -The goal of group_up_list_ is to move all vars of lhyps to there -segment or above fstProp if there segment does not exist yet. - -invariant: the things in lhyps always need to be moved upward, -otherwise move before and move after work the wrong way. *) -Ltac group_up_list_ fstProp cache lhyps := - lazymatch lhyps with - | DCons ?th ?h ?lhyps' => - match type of th with - | Prop => (* lhyps is supposed to be filtered out of Prop already. *) - idtac "LibHyps: This shoud not happen. Please report."; - group_up_list_ fstProp cache lhyps' - | _ => - let upd := find_in_cache_update cache th h in - lazymatch upd with - | (?newcache , None) => (* there was no pivot for th *) - match fstProp with - | @None => idtac (* No Prop Hyp, don't move *) - | ?hfstprop => move_above h hfstprop - end; - group_up_list_ fstProp constr:(DCons th h cache) lhyps' - | (?newcache , ?theplace) => - (* we append h to its segment, and it becomes the new pivot. *) - (try move_below h theplace); - group_up_list_ fstProp newcache lhyps' - end - end - | DNil => idtac (* no more hyps to move *) - end -. - -Ltac find_in t lh := - match lh with - | DNil => None - | (DCons t ?h ?lh') => h - | (DCons _ ?h ?lh') => find_in t lh' - end. +(* END DEBUG *) +*) -(* return a triple for hyps groupinf initiation: -- H: topmost Prop-sorted hyp (where a hyp goes if there is no segment for it). -- list of pivots for each type seen above H (pivot = lowest of the first segment of a type) -- the hypothesis that may need to be moved (not belonging to there first segment). -See group_up_list_ above. - *) -Ltac build_initial_cache_ acc lh := - match acc with - (?fstProp, ?pivots, ?tomove) => - lazymatch lh with - | DNil => constr:((fstProp, pivots , tomove)) - | (DCons ?th ?h ?lh') => - lazymatch type of th with - | Prop => - lazymatch fstProp with (* is this the first Prop? *) - | @None => build_initial_cache_ (h, pivots, tomove) lh' - | _ => build_initial_cache_ (fstProp, pivots, tomove) lh' - end - | _ => (* Type-sorted hyp *) - lazymatch fstProp with (* we haven't reached the fstprop *) - | @None => - (* does this type already have a pivot? if yes don't replace *) - let found := find_in th pivots in - lazymatch found with - | @None => (* no pivot yet, see the next hyp *) - lazymatch lh' with - | (DCons th _ _) => (* h is correctly placed, not the pivot *) - build_initial_cache_ (fstProp, pivots, tomove) lh' - | (DCons _ _ _) => (* h is the pivot for th *) - build_initial_cache_ (fstProp, DCons th h pivots , tomove) lh' - | DNil => (* h is the pivot for th *) - constr:((fstProp, DCons th h pivots , tomove)) - end - | _ => (* there already is a pivot for th, and it needs to move *) - build_initial_cache_ (fstProp, pivots , DCons th h tomove) lh' - end - | _ => (*fstprop already reached, this is not a pivot and needs to move*) - build_initial_cache_ (fstProp, pivots , DCons th h tomove) lh' - end +(* TODO *) + +Ltac2 rec find_above_which (foundone:bool) (t:constr) + (lH:(ident * constr option * constr) list): ident option := + match lH with + | (id,_,tid)::lH' => + if Constr.equal (Constr.type tid) constr:(Prop) then Some id + else + if Constr.equal tid t + then + match find_above_which true t lH' with + | Some x => Some x + | None => Some id end - end + else if foundone then Some id + else find_above_which false t lH' + | [] => None end. -Ltac build_initial_cache lh := build_initial_cache_ constr:((@None, DNil, DNil)) lh. - -Ltac mem x l := - lazymatch l with - | DNil => false - | DCons _ x ?l' => true - | DCons _ _ ?l' => mem x l' - end. - -(* return the intersection of l1 l2 in reverse order of l1 *) -Ltac intersec_ acc l1 l2 := - match l1 with - DNil => acc - | DCons ?th ?h ?l1' => - match (mem h l2) with - | true => intersec_ (DCons th h acc) l1' l2 - | false => intersec_ acc l1' l2 - end - end. - -Ltac intersec l1 l2 := intersec_ DNil l1 l2. +Ltac2 rec cut_at (h:ident) (lH:(ident * constr option * constr) list) := + match lH with + | ((id,_,_) as elt)::lH' => if Ident.equal id h then [elt] else elt :: (cut_at h lH') + | [] => Control.throw (Invalid_argument None) (* Should we fail here? h should always be in lH *) + end. + +Ltac2 move_up_types (h:ident) := + let t := Constr.type (Control.hyp h) in + let tt := Constr.type t in + if Constr.equal constr:(Prop) tt then () + else + let l := (Control.hyps()) in + let l := cut_at h l in + let aboveh := find_above_which false t l in + match aboveh with + | None => () + | Some aboveh => + if Ident.equal aboveh h then () + else Std.move h (Std.MoveAfter aboveh) + end. +(* Ltac2 move_up (h:constr) := *) +(* match Constr.Unsafe.kind h with *) +(* | Constr.Unsafe.Var id => move_up_hyp id *) +(* | _ => Control.throw (Invalid_argument None) *) +(* end. *) -(* Move up non-Prop hypothesis of lhyps up in the goal, to make Prop - hyptohesis closer to the conclusion. Also group non-Prop hyps by - same type to win some place in goal printing. +Ltac2 ltac1_move_up_types (h:Ltac1.t) := + let h: ident := Option.get (Ltac1.to_ident h) in + move_up_types h. -Note: This tactic takes a list of hyps, you should use the tactical -then_allnh (syntax: ";{! group_up_list }") or then_allnh_rev (syntax: -";{!< group_up_list}"). *) -Ltac group_up_list lhyps := - match build_initial_cache all_hyps with - | (?fstProp, ?cache, ?tomove) => - (* tomove is reversed, but intersec re-reverse *) - let tomove2 := intersec tomove lhyps in - group_up_list_ fstProp cache tomove2 - end. +Local Tactic Notation "Lmove_up_type" hyp(h) := + let tac := ltac2:(h |- ltac1_move_up_types h) in + tac h. -(* Stays for compatibility, but for efficiency reason prefer - rename_all_hyps, which applies on the list of hyptohesis to move. - Use the corresponding tactical. *) -Ltac move_up_types H := - let t := type of H in - match t with - Depl => fail "Try to use { } instead of {! }" - | _ => group_up_list constr:(DCons t H DNil) - end. +Global Ltac move_up_types h := Lmove_up_type h. +Local Set Default Proof Mode "Classic". (* (* Tests *) +Require Import LibHyps.LibHyps. Export TacNewHyps.Notations. Goal forall x1 x3:bool, forall a z e : nat, z+e = a @@ -327,24 +97,47 @@ Goal forall x1 x3:bool, forall a z e : nat, Proof. (* Set Ltac Debug. *) (* then_nh_rev ltac:(intros) ltac:(subst_or_idtac). *) - intros ; {! group_up_list }. + intros ; {< move_up_types }. (* intros ? ? ? ? ? ? ? ? ? ?. *) (* group_up_list (DCons bool b1 DNil). *) Undo. intros ; { move_up_types }. Undo. - intros ; { autorename }; {! group_up_list }. + intros ; { autorename }; {< move_up_types }. Undo. - intros ; {subst_or_idtac} ; { autorename } ; {! group_up_list }. + intros ; {subst_or_idtac} ; { autorename } ; {< move_up_types }. Undo. Fail progress intros ; { revertHyp }. intros. - let hyps := all_hyps in - idtac hyps. - Undo 2. then_eachnh ltac:(intros) ltac:(subst_or_idtac). Undo. - Fail intros ; { fun h => autorename_strict h }. + intros ; { fun h => autorename_strict h }. intros ; { fun h => idtac h }. intros ; { ltac:(fun h => idtac h) }. *) + +(* + +Goal forall x y:nat, x x+1 forall z:nat, forall a b : bool, forall n m p : nat, True. +Proof. + intros. + + progress (move_up_types z). + Fail progress (move_up_types z). + Fail progress (move_up_types H). + Fail progress (move_up_types H0). + + + let l:(ident * constr option * constr) list := (Control.hyps()) in + let idopt := find_above_which false constr:(nat) l in + match idopt with + | None => printf "None" + | Some id => printf "res = %I" id + end. + + Std.move ident:(z) (Std.MoveAfter ident:(H)). + + let l:(ident * constr option * constr) list := (Control.hyps()) in + let (h,_,_) := find_lowest constr:(nat) l in + printf "h = %I" h. +*) diff --git a/LibHyps/TacNewHyps.v b/LibHyps/TacNewHyps.v index 7322d61..416d204 100644 --- a/LibHyps/TacNewHyps.v +++ b/LibHyps/TacNewHyps.v @@ -29,268 +29,154 @@ *) -(* Credit for the harvesting of hypothesis: Jonathan Leivant *) -Ltac harvest_hyps harvester := constr:(ltac:(harvester; constructor) : True). -Ltac harvest_hyps_h harvester h := constr:(ltac:(harvester h; constructor) : True). - -(* This will be stuck on section variables if some hypothesis really - depends on it. We can use "revert dependent" but the hypothesis - remains in the goal and make this tactic loop. The trick consisting - of marking hyms with (id) fails on types. Needs more thinking. - Meanwhile harvest_hyps will fail on some section variables. *) -Ltac revert_clearbody_all := - repeat lazymatch goal with - H : _ |- _ => try clearbody H; revert H - end. - -Ltac revert_clearbody_above Hyp := - lazymatch goal with - | _H : ?T |- _ => - match constr:((_H , Hyp)) with - | (?h,?h) => let dummy := constr:(ltac:(apply eq_refl): _H=Hyp) in - (* we have foud Hyp, clear it and register everything up *) - clear _H; revert_clearbody_all - | _ => clear _H; revert_clearbody_above Hyp - end - end. -(* THE GENERIC MECHANISM is to have a tactic that applies directly to - the *list* of hypothesis. Most of the time it will be a simpl - iteration on each hypothesis independently, but sometimes for - efficiency we will need to be smarter (e.g. group_up_list). We - don't use directly the product build by harvest_hyps for efficiency - reasons. Instead we use the dependent list Depl defined below. *) -Inductive Depl := - | DNil: Depl - | DCons: forall (A:Type) (x:A), Depl -> Depl. - -(* Transforming the product from harvest_hyps into a Depl. *) -Ltac prod_to_list_ acc prod := - match prod with - | (?prod' ?h) => - let t := type of h in - let acc := constr:(DCons t h acc) in - prod_to_list_ acc prod' - | _ => acc - end. +Require Import Ltac2.Ltac2. -Ltac prod_to_list prod := prod_to_list_ DNil prod. +From Ltac2 Require Import Option Constr Printf. +Import Constr.Unsafe. +Local Set Default Proof Mode "Classic". +Require Import LibHyps.LibHypsDebug. -(* Same but reversing the list. *) -Ltac prod_to_list_rev prod := - match prod with - | (?prod' ?h) => - let t := type of h in - let recres := prod_to_list_rev prod' in - constr:(DCons t h recres) - | _ => DNil +(* Utilities *) +Local Ltac2 is_dep_prod (t:constr): bool := + match kind t with + | Prod _ subt => Bool.neg (is_closed subt) + | _ => false end. -(* { BUILDING THE LIST OF ALL HYPS } *) - -(* Builds the DList of all hyps *) -Ltac all_hyps := let prod := harvest_hyps revert_clearbody_all in prod_to_list prod. -Ltac all_hyps_rev := let prod := harvest_hyps revert_clearbody_all in prod_to_list_rev prod. - -(* { BUILDING THE LIST OF ALL HYPS ABOVE H }. (useful?). *) -Ltac up_segment H := - let prod := harvest_hyps_h revert_clearbody_above H in prod_to_list prod. -Ltac up_segment_rev H := - let prod := harvest_hyps_h revert_clearbody_above H in prod_to_list_rev prod. - -(* { GENERATING THE LIST OF "NEW" HYPOTHESIS } *) - -(* Remark: this version has several potential efficiency problems: - -1) it is quadratic, but this may be unavoidable unless we replace list -by trees. - -2) it looks for hyp (context) names inside types, instead of only hyp -names. Since context is quite fast it does not seem much visible, -but on big types (class types for instance) it may become problematic. - -I have tried to optimize more the filtering. Mainly trying to avoid to -look at types by iterating by hand in ltac on the list. No real -speedup was observed. - -The filter_new_hyps_optim tactic does speed up significantly in most -cases. *) - -(* Builds the list (DCons/DNil) of hypothesis appearing in lh2 that - are not present in lh1. This version may be slow on big types - because of the "context" will dive into them uselessly. However on - standard goals it is quite efficient. See below for - optimizations. *) -Ltac filter_new_hyps lh2 lh1 := - match lh2 with - (DCons _ ?h ?lh2') => - match lh1 with - (* This context is fast but it may have bad complexity on big hyps - types (e.g. type classes). *) - | context [h] => filter_new_hyps lh2' lh1 - | _ => let th := type of h in - let recres := filter_new_hyps lh2' lh1 in - constr:(DCons th h recres) - end - | _ => DNil - end. +Local Ltac2 pr_list (pr: unit -> 'a -> message) () (l: 'a list) := + let rec pr_list_ () (l: 'a list) := + match l with + | [] => fprintf "" + | [e] => fprintf "%a" pr e + | e::l' => fprintf "%a , %a" pr e pr_list_ l' + end in + fprintf "[ %a ]" pr_list_ l. -(* This naive optimization works pretty well since most of the time - lh1 and lh2 share a significant prefix. *) -Ltac filter_new_hyps_optim lh2 lh1 := - lazymatch lh2 with - | (DCons _ ?h ?lh2') => - lazymatch lh1 with - | (DCons _ h ?lh1') => - filter_new_hyps_optim lh2' lh1' - | _ => filter_new_hyps lh2 lh1 - end - | _ => filter_new_hyps lh2 lh1 - end. -(* { TACTICALS ITERATING ON A GIVEN LIST OF HYPOTHESIS } *) +(* Pure Ltac2 tactics *) +Module Ltac2. + Ltac2 all_hyps_ident() := List.map (fun (x,_,_) => x) (Control.hyps ()). -(* Default way of iterating a tactic on all elements of a Decl. *) -Ltac map_hyps tac l := - match l with - | DNil => idtac - | DCons _ ?h ?l' => tac h; map_hyps tac l' - end. + Ltac2 iter_hyps (tac:ident -> unit) (lh:ident list) := + List.iter tac lh. -(* Same thing in reverse order. Prefer map_hyps on reversed list? *) -Ltac map_hyps_rev tac l := - match l with - | DNil => idtac - | DCons _ ?h ?l' => map_hyps_rev tac l'; tac h - end. + Ltac2 map_all_hyps (tac:'a -> unit) := + let all_hyps := all_hyps_ident() in + iter_hyps tac all_hyps. + + Ltac2 map_all_hyps_rev (tac: 'a -> unit) := + let all_hyps := List.rev (all_hyps_ident()) in + iter_hyps tac all_hyps. + + Ltac2 then_eachnh_gen (tac1:'a -> unit) (tac2:ident -> unit) (rev:bool) := + let hyps_before := all_hyps_ident() in + let _ := tac1() in + Control.enter + (fun () => + let hyps_after := all_hyps_ident() in + let new_hyps: ident list := List.filter_out (fun id => List.mem Ident.equal id hyps_before) hyps_after in + iter_hyps tac2 (if rev then List.rev new_hyps else new_hyps)). + + Ltac2 then_eachnh (tac1:'a -> unit) (tac2:ident -> unit) := + then_eachnh_gen tac1 tac2 false. + + Ltac2 then_eachnh_rev (tac1:'a -> unit) (tac2:ident -> unit) := + then_eachnh_gen tac1 tac2 true. + +End Ltac2. + +(* Ltac2 tacticals on Ltac1 tactics and values. Mainly work + translating them to ltac2 values and call tactical from Ltac2 + above.*) +Module Ltac1. + Ltac2 apply_run (tac:Ltac1.t) lid := + let larg := List.map Ltac1.of_ident lid in + Ltac1.apply tac larg (fun t => Ltac1.run t). + + Ltac2 iter_hyps (tac:Ltac1.t) (lh:ident list): unit := + let tac2:ident -> unit := (fun (id:ident) => apply_run tac [id]) in + Ltac2.iter_hyps tac2 lh. + + (* Iterate tac on all hyps of a goal, top to bottom or reverse. *) + + Ltac2 map_all_hyps (tac:Ltac1.t) := + let tac2:ident -> unit := (fun (id:ident) => apply_run tac [id]) in + Ltac2.map_all_hyps tac2. + + Ltac2 map_all_hyps_rev (tac:Ltac1.t) := + let tac2:ident -> unit := (fun (id:ident) => apply_run tac [id]) in + Ltac2.map_all_hyps_rev tac2. + + Ltac2 then_eachnh (tac1:Ltac1.t) (tac2:Ltac1.t) := + let tac1':unit -> unit := (fun () => Ltac1.run tac1) in + let tac2':ident -> unit := (fun id => apply_run tac2 [id]) in + Ltac2.then_eachnh tac1' tac2'. + + Ltac2 then_eachnh_rev (tac1:Ltac1.t) (tac2:Ltac1.t) := + let tac1':unit -> unit := (fun () => Ltac1.run tac1) in + let tac2':ident -> unit := (fun id => apply_run tac2 [id]) in + Ltac2.then_eachnh_rev tac1' tac2'. +End Ltac1. + +Ltac map_all_hyps tac := + let t := ltac2:(tac |- Ltac1.map_all_hyps tac) in + t tac. + +Ltac map_all_hyps_rev tac := + let t := ltac2:(tac |- Ltac1.map_all_hyps_rev tac) in + t tac. + +(* Ltac tacticals *) +Ltac then_eachnh tac1 tac2 := + let t := ltac2:(tac1 tac2 |- Ltac1.then_eachnh tac1 tac2) in + t tac1 tac2. + +Ltac then_eachnh_rev tac1 tac2 := + let t := ltac2:(tac1 tac2 |- Ltac1.then_eachnh_rev tac1 tac2) in + t tac1 tac2. + + (* then_allnh_rev tac1 ltac:(map_hyps tac2). *) +(* Ltac then_eachnh tac1 tac2 := then_allnh tac1 ltac:(map_hyps tac2). *) -(* { TACTICALS ITERATING ON ALL HYPOTHESIS OF A GOAL } *) -(* Iterate tac on all hyps of a goal, top to bottom or reverse. *) -Ltac map_all_hyps tac := map_hyps tac all_hyps. -Ltac map_all_hyps_rev tac := map_hyps tac all_hyps_rev. (* For less parenthesis: OnAllHyp tacA;tac2. *) -Tactic Notation (at level 4) "onAllHyps" tactic(Tac) := (map_all_hyps Tac). -Tactic Notation (at level 4) "onAllHypsRev" tactic(Tac) := (map_all_hyps_rev Tac). - -(* { TACTICALS ITERATING ON *NEW* HYPOTHESIS AFTER APPLYING A TACTIC } - -The most common tacticals are then_eachnh and then_eachnh_rev, use -then_allnh and then_allnh_rev for efficiency reason (see e.g. -LibHyps.group_up_list). *) - -Ltac then_allnh_gen gathertac tac1 tac2 := - let hyps_before_tac := gathertac idtac in - tac1; - let hyps_after_tac := gathertac idtac in - let l_new_hyps := filter_new_hyps_optim hyps_after_tac hyps_before_tac in - tac2 l_new_hyps. - -(* [then_allnh tac1 tac2] and [then_allnh_rev tac1 tac2] applies tac1 and - then applies tac2 on the list of *new* hypothesis of the resulting - goals. The list is of type [Decl]. - NOTE: tac2 must operates directly on the whole list. For - single-goal minded tac2, use then_eachnh(_rev), below. *) -Ltac then_allnh tac1 tac2 := then_allnh_gen ltac:(fun x => all_hyps) tac1 tac2. -Ltac then_allnh_rev tac1 tac2 := then_allnh_gen ltac:(fun x => all_hyps_rev) tac1 tac2. -(* For a single-goal-minded tac2 (most common use case). *) -Ltac then_eachnh_rev tac1 tac2 := then_allnh_rev tac1 ltac:(map_hyps tac2). -Ltac then_eachnh tac1 tac2 := then_allnh tac1 ltac:(map_hyps tac2). +Tactic Notation (at level 4) "onAllHyps" tactic(tac) := map_all_hyps tac. +Tactic Notation (at level 4) "onAllHypsRev" tactic(tac) := map_all_hyps_rev tac. Module Notations. (* Default syntax: *) - Tactic Notation (at level 4) tactic4(tac)";" "{!" tactic(tach) "}" := then_allnh tac tach. - Tactic Notation (at level 4) tactic4(tac)";" "{!<" tactic(tach)"}":= then_allnh_rev tac tach. + (* Tactic Notation (at level 4) tactic4(tac)";" "{!" tactic(tach) "}" := then_allnh tac tach. *) + (* Tactic Notation (at level 4) tactic4(tac)";" "{!<" tactic(tach)"}":= then_allnh_rev tac tach. *) (* single-goal-minded tach (most common use case). *) Tactic Notation (at level 4) tactic4(tac)";" "{" tactic(tach)"}":= then_eachnh tac tach. Tactic Notation (at level 4) tactic4(tac)";" "{<" tactic(tach)"}":= then_eachnh_rev tac tach. (* Legacy tacticals. Warning: not applicable for tactic operating directly on a list of hyps *) - Tactic Notation (at level 4) tactic4(tac) ";;" tactic4(tach) := then_eachnh tac tach. - Tactic Notation (at level 4) tactic4(tac) ";!;" tactic4(tach) := (then_eachnh_rev tac tach). + (* Tactic Notation (at level 4) tactic4(tac) ";;" tactic4(tach) := then_eachnh tac tach. *) + (* Tactic Notation (at level 4) tactic4(tac) ";!;" tactic4(tach) := (then_eachnh_rev tac tach). *) End Notations. -(* -(* Tests. *) -Ltac r h := revert h. -Ltac rl lh := - match lh with - DCons ?t ?h ?lh' => revert h; rl lh' - | DNil => idtac - end. - - -Ltac p h := idtac h. -Ltac pl lh := - match lh with - DCons ?t ?h ?lh' => idtac h; pl lh' - | DNil => idtac - end. - -(* dummy rename *) -Ltac n h := let nm := fresh "h" in rename h into nm. -Ltac nl lh := - match lh with - DCons ?t ?h ?lh' => (let nm := fresh "h" in rename h into nm) ; nl lh' - | DNil => idtac - end. - -Import TacNewHyps.Notations. -Goal forall x1:bool, forall a z e r t z e r t z e r t z e r t y: nat, True -> forall u i o p q s d f g:nat, forall x2:bool, True -> True. -Proof. - (* intros. let l := all_hyps in idtac l. (* pb dans l'ordre entre map_hyp et all_hyp *) *) - (* intros ;; n. *) - - intros ; { p }; { n }; { r }. - Undo. - intros ; {! pl } ; { n }; { r }. - Undo. - intros ; { n }; { p }; { r }. - Undo. - intros ; {! nl }; { p }; { r }. - Undo. -Import TacNewHyps.SimpleNotations. - - intros ;!; ltac:(fun h => idtac h) ;; ltac:(fun h => revert h). - - ;!; ltac:(fun h => idtac h) - then_nh ltac:(intros) ltac:(revert_l). *) - -(* Testing speedup for filter_new_hyps_optim, when there is a common -prefix in the two lists. *) +Import Notations. (* -Lemma foo: - forall (_ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ - _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ - _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ - _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ - _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ - _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ - _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ - _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ - : (forall (_ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ - _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ - _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ - _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ - :nat), True)) - (a b:bool), True -> forall y z:nat, True. - intros. - Ltac prefx n l := - lazymatch n with - 0%nat => DNil - | S ?n' => - lazymatch l with - DCons ?a ?b ?l' => let p := prefx n' l' in constr:(DCons a b p) - | DNil => DNil - | _ => fail - end - end. - - time let all := all_hyps in - let few := prefx 20 all in - let diff := filter_new_hyps_optim all few in - idtac. +Goal forall n m p q : nat, n m

p<=q -> True. +Proof. + intros n m p q H H0 H1. + Unset Silent. + map_all_hyps ltac:(fun h => idtac h). + map_all_hyps_rev ltac:(fun h => idtac h). + onAllHyps (fun h => idtac h). + onAllHypsRev (fun h => idtac h). + ltac2:(Ltac2.then_eachnh (fun () => induction H) (fun id => printf "%I" id)). + Undo 1. + then_eachnh ltac:(induction H) ltac:(fun h => idtac h). + Undo 1. + then_eachnh_rev ltac:(induction H) ltac:(fun h => idtac h). + Undo 1. + induction H ;{ fun h => idtac h }. + Undo 1. + induction H ;{< fun h => idtac h }. *) diff --git a/Makefile b/Makefile index 8b80794..a6af6cf 100644 --- a/Makefile +++ b/Makefile @@ -1,6 +1,13 @@ -lib: +.PHONY: tests LibHyps + +lib: sanity + make -C LibHyps + +# Use this instead of make lib when the debug code is present +make debug: make -C LibHyps + make -C tests tests: lib make -C tests @@ -18,3 +25,5 @@ clean: install: lib make -C LibHyps install +sanity: + @./testDebug.sh diff --git a/configure.sh b/configure.sh index beabc6c..4904fe4 100755 --- a/configure.sh +++ b/configure.sh @@ -1,15 +1,51 @@ #!/bin/bash +DEVOPT=no +STDLIB= + +POSITIONAL=() +while [[ $# -gt 0 ]] +do +key="$1" + +case $key in + --stdlib|-stdlib) + shift + STDLIB=$1 + shift + ;; + --dev) + DEVOPT=yes + shift + ;; + *) # unknown option + POSITIONAL+=("$1") # save it in an array for later + shift # past argument + ;; +esac +done + +set -- "${POSITIONAL[@]}" # restore positional parameters (i.e. + # parameters that were not recognized by the + # previous code.) function gen_projet_file () { FILES="$1" DIR=$2 + STDLIB=$4 PROJECTFILE=$DIR/_CoqProject RESOURCEFILE=$3 - cat < $RESOURCEFILE > "$PROJECTFILE" + if [ "$STDLIB" != "" ] + then + echo "stdlib detected" + echo "-Q $STDLIB Stdlib" > "$PROJECTFILE" + else echo "" > "$PROJECTFILE" + fi + + cat < $RESOURCEFILE >> "$PROJECTFILE" echo "" >> "$PROJECTFILE" @@ -27,11 +63,18 @@ function gen_projet_file () { } -FILESLH=$(cd LibHyps && find . -name "*.v" | grep -v "ident_of_string\|especialize_ltac2\|LibEspecialize" ) +if [ "$DEVOPT" = "no" ] +then + FILESLH=$(cd LibHyps && find . -name "*.v" | grep -v "ident_of_string\|especialize_ltac2\|LibEspecialize\|LibHypsDebug" ) +else + FILESLH=$(cd LibHyps && find . -name "*.v" | grep -v "ident_of_string\|especialize_ltac2\|LibEspecialize" ) +fi + PROJECTDIRLH="LibHyps" -gen_projet_file "$FILESLH" "$PROJECTDIRLH" "resources/coq_project.libhyps" +gen_projet_file "$FILESLH" "$PROJECTDIRLH" "resources/coq_project.libhyps" "$STDLIB" + FILESTEST=$(cd tests && find . -name "*.v" | grep -v "incremental" ) PROJECTDIRTESTS="tests" -gen_projet_file "$FILESTEST" "$PROJECTDIRTESTS" "resources/coq_project.tests" +gen_projet_file "$FILESTEST" "$PROJECTDIRTESTS" "resources/coq_project.tests" "$STDLIB" diff --git a/testDebug.sh b/testDebug.sh new file mode 100755 index 0000000..b7cc63c --- /dev/null +++ b/testDebug.sh @@ -0,0 +1,22 @@ +#!/bin/bash + + +## Explanation +# - Debug code is in LibHyps/LibHypsDebug.v +# +# - by default ./configure.sh does ignores this file +# - unless we use ./configure.sh --dev +# +# - the present test checks that we have not forgotten to remove +# - refrences to the debug file (by doing ./configure.sh). +# +echo "Sanity check (debug files)" +if grep -q "LibHypsDebug.v" LibHyps/_CoqProject +then + echo "REMAINING DEBUG CODE: ABORTING." + echo "Use ./configure.sh to remove rerferences to debug code." + echo "then make clean; make lib tests" + exit 1 +else + exit 0 +fi diff --git a/tests/Especialize_tests.v b/tests/Especialize_tests.v index 10eef6a..4a3fa03 100644 --- a/tests/Especialize_tests.v +++ b/tests/Especialize_tests.v @@ -1,4 +1,4 @@ -Require Import LibHyps.LibHypsTactics. +(* Require Import LibHyps.LibHypsTactics. *) Require Import LibHyps.Especialize. (* tests *) diff --git a/tests/LibHypsRegression.v b/tests/LibHypsRegression.v index 284b385..c2520d6 100644 --- a/tests/LibHypsRegression.v +++ b/tests/LibHypsRegression.v @@ -8,36 +8,43 @@ Require Export LibHyps.LibHypsNaming. Require Export LibHyps.LibHyps. Export TacNewHyps.Notations. From Stdlib Require Import Arith ZArith List. +Require Import Ltac2.Ltac2. +From Ltac2 Require Import Option Constr Printf. +Local Set Default Proof Mode "Classic". +Import ListNotations. Import LibHyps.LegacyNotations. (* This settings should reproduce the naming scheme of libhypps-1.0.0 and libhypps-1.0.1. *) -Ltac add_suffix ::= constr:(false). -Ltac numerical_names ::= numerical_names_sufx. - -Local Open Scope autonaming_scope. -Import ListNotations. - -(* From there this is LibHypTest from 1f7a1ed2289e439c291fcbd06c51705547feef1e *) -Ltac rename_hyp_2 n th := - match th with - | true <> false => name(`_tNEQf`) - | true = false => name(`_tEQf`) +Ltac2 Set numerical_sufx := true. +Ltac2 Set add_suffix := false. + +Ltac2 rename_hyp_1 n th := + if Int.lt n 0 then [] + else + lazy_match! th with + | @cons _ ?x (cons ?y ?l) => [String "cons"; Rename x; Rename y; RenameN (decr (decr n)) l] + | @cons _ ?x ?l => if Int.ge n 1 then [String "cons"; Rename x; RenameN (decr n) l] else [String "cons"] + end. + +Ltac2 rename_hyp_2 n th := + match! th with + | true <> false => [ String "tNEQf" ] + | true = false => [ String "tEQf"] + | _ => rename_hyp_1 n th (* call the previously defined tactic *) end. -Ltac rename_hyp ::= rename_hyp_2. +Ltac2 Set rename_hyp := rename_hyp_2. -(* Suppose I want to add later another naming rule: *) -Ltac rename_hyp_3 n th := - match th with - | Nat.eqb ?x ?y = true => name(`_Neqb` ++ x#n ++ y#n) - | true = Nat.eqb ?x ?y => name(`_Neqb` ++ x#n ++ y#n) +Ltac2 rename_hyp_3 n th := + match! th with + | Nat.eqb ?x ?y = true => [ String "Neqb" ; Rename x ; Rename y ] + | true = Nat.eqb ?x ?y => [ String "Neqb" ; Rename x ; Rename y ] | _ => rename_hyp_2 n th (* call the previously defined tactic *) end. -Ltac rename_hyp ::= rename_hyp_3. -Ltac rename_depth ::= constr:(3). +Ltac2 Set rename_hyp := rename_hyp_3. Close Scope Z_scope. Open Scope nat_scope. @@ -49,7 +56,10 @@ Lemma dummy: forall x y, 0 = 1 -> (0 = 1)%Z -> ~x = y -> + Nat.eqb (x + 1) 0 <> Nat.eqb 1 y -> true = Nat.eqb 3 4 -> + Nat.eqb (x + 3) 4 = true -> + Nat.eqb (2 * (x + 3)) 4 = true -> Nat.eqb 3 4 = true -> true = Nat.leb 3 4 -> 1 = 0 -> @@ -90,9 +100,11 @@ Lemma dummy: forall x y, match type of h_neq_x_y with x <> y => idtac | _ => fail "test failed!" end. match type of h_Neqb_3n_4n with true = (3 =? 4) => idtac | _ => fail "test failed!" end. match type of h_Neqb_3n_4n0 with (3 =? 4) = true => idtac | _ => fail "test failed!" end. + match type of h_Neqb_mul_2n_add_4n with (2 * (x + 3) =? 4) = true => idtac | _ => fail "test failed!" end. match type of h_eq_true_leb_3n_4n with true = (3 <=? 4) => idtac | _ => fail "test failed!" end. match type of h_eq_1n_0n with 1 = 0 => idtac | _ => fail "test failed!" end. match type of h_neq_x_y0 with x <> y => idtac | _ => fail "test failed!" end. + match type of h_neq_eqb_add_0n_eqb_1n_y with (x + 1 =? 0) <> (1 =? y) => idtac | _ => fail "test failed!" end. match type of h_not_lt_1n_0n with ~ 1 < 0 => idtac | _ => fail "test failed!" end. match type of h_all_tNEQf with forall w w' : nat, w = w' -> true <> false => idtac | _ => fail "test failed!" end. match type of h_all_and_tEQf_True with forall w w' : nat, w = w' -> true = false /\ True => idtac | _ => fail "test failed!" end. @@ -101,7 +113,7 @@ Lemma dummy: forall x y, match type of h_ex_and_True_False with exists w : nat, w = w -> True /\ False => idtac | _ => fail "test failed!" end. match type of h_all_tEQf with forall w w' : nat, w = w' -> true = false => idtac | _ => fail "test failed!" end. match type of h_all_eq_eqb_eqb with forall w w' : nat, w = w' -> (3 =? 4) = (4 =? 3) => idtac | _ => fail "test failed!" end. - match type of h_eq_length_cons with length [3] = (fun _ : nat => 0) 1 => idtac | _ => fail "test failed!" end. + match type of h_eq_length_cons with (length [3] = (fun _ : nat => 0) 1) => idtac | _ => fail "test failed!" end. match type of h_eq_length_cons_0n with length [3] = 0 => idtac | _ => fail "test failed!" end. match type of h_eq_add_0n_y_y with 0 + y = y => idtac | _ => fail "test failed!" end. match type of h_tEQf with true = false => idtac | _ => fail "test failed!" end. @@ -123,36 +135,46 @@ Qed. -(* + +Definition eq_one (i:nat) := i = 1. Lemma test_espec_namings: forall n:nat, (eq_one n -> eq_one 1 -> False) -> True. Proof. intros n h_eqone. - especialize Nat.quadmul_le_squareadd with a at 1 as hh : h. + especialize Nat.quadmul_le_squareadd with a at 1 as hh (*: h*). { apply le_n. } especialize min_l with n,m at 1 as ?. { apply (le_n O). } - especialize h_eqone at 2 as h1 : h2. + especialize h_eqone at 2 as h1 (*: h2 *). { reflexivity. } - unfold eq_one in h2. - match type of h2 with 1 = 1 => idtac | _ => fail end. + (* unfold eq_one in h2. *) + (* match type of h2 with 1 = 1 => idtac | _ => fail end. *) match type of h1 with eq_one n -> False => idtac | _ => fail end. exact I. Qed. -*) + + +Ltac2 rename_hyp_4 n th := + match! th with + | length ?l => [ String "lgth" ; Rename l ] + | _ => rename_hyp_3 n th (* call the previously defined tactic *) + end. + +Ltac2 Set rename_hyp := rename_hyp_4. Require Import LibHyps.LibDecomp. +Ltac2 Set rename_depth := 3. Goal forall l1 l2 l3:list nat, List.length l1 = List.length l2 /\ List.length l1 = List.length l3 -> True. Proof. - intros l1 l2 l3 h. + intros l1 l2 l3 ?/n. (* then_allnh_gen ltac:(fun x => all_hyps) ltac:(fun _ => decomp_logicals h) ltac:(fun lh => idtac lh) . *) (* Set Ltac Debug. *) - decomp_logicals h /sng. + decomp_logicals h_and_eq_lgth_lgth_eq_lgth_lgth /sn. match goal with |- _ => - match type of h_eq_length_l1_length_l2 with + match type of h_eq_lgth_l1_lgth_l2 with length l1 = length l2 => idtac | _ => fail "Test failed (wrong type)!" end diff --git a/tests/LibHypsTest.v b/tests/LibHypsTest.v index 78c2e60..38e9d0e 100644 --- a/tests/LibHypsTest.v +++ b/tests/LibHypsTest.v @@ -4,33 +4,43 @@ From Stdlib Require Import Arith ZArith List. Require Import LibHyps.LibHyps (*LibHyps.LibSpecialize*). +Require Import Ltac2.Ltac2. From Stdlib Require Import List. -Local Open Scope autonaming_scope. Import ListNotations. -Ltac rename_hyp_2 n th := - match th with - | true <> false => name(`_tNEQf`) - | true = false => name(`_tEQf`) +Ltac2 rename_hyp_2 n th := + match! th with + | true <> false => [ String "tNEQf" ] + | true = false => [ String "tEQf" ] end. -Ltac rename_hyp ::= rename_hyp_2. +Ltac2 Set rename_hyp := rename_hyp_2. (* Suppose I want to add later another naming rule: *) -Ltac rename_hyp_3 n th := - match th with - | Nat.eqb ?x ?y = true => name(`_Neqb` ++ x#n ++ y#n) - | true = Nat.eqb ?x ?y => name(`_Neqb` ++ x#n ++ y#n) +Ltac2 rename_hyp_3 n th := + match! th with + | Nat.eqb ?x ?y = true => [ String "Neqb"; Rename x ; Rename y ] + | true = Nat.eqb ?x ?y => [ String "Neqb" ; Rename x ; Rename y ] | _ => rename_hyp_2 n th (* call the previously defined tactic *) end. -Ltac rename_hyp ::= rename_hyp_3. -Ltac rename_depth ::= constr:(3). +Ltac2 Set rename_hyp := rename_hyp_3. + +Ltac2 rename_hyp_4 n th := + lazy_match! th with + | @cons _ ?x (cons ?y ?l) => [String "cons"; Rename x; Rename y; RenameN (decr (decr n)) l] + | @cons _ ?x ?l => if Int.ge n 1 then [String "cons"; Rename x; RenameN (decr n) l] else [String "cons"] + | _ => rename_hyp_3 n th (* call the previously defined tactic *) + end. + +Ltac2 Set rename_hyp := rename_hyp_4. + +Ltac2 rename_depth := 3. -Close Scope autonaming_scope. Close Scope Z_scope. Open Scope nat_scope. +Local Set Default Proof Mode "Classic". Ltac test h th := match type of h with @@ -172,7 +182,9 @@ Lemma test_rename_or_revert: forall x y:nat, (0 < 1 -> 1<0) -> 0 < z -> True. Proof. intros ; { rename_or_revert }. - testg ((fun _ : bool => x = y) true -> True). + match goal with + | |- _ -> True => idtac + end. auto. Qed. @@ -186,7 +198,9 @@ Lemma test_rename_or_revert2: forall x y:nat, (0 < 1 -> 1<0) -> 0 < z -> True. Proof. intros /n?. - testg ((fun _ : bool => x = y) true -> True). + match goal with + | |- _ -> True => idtac + end. test x (nat). test y (nat). (* Checking that hyps after the failed rename are introduced. *) @@ -233,7 +247,7 @@ Lemma test_group_up_list2: forall x y:nat, x = y -> (0 < 1 -> 1<0) -> 0 < z -> True. Proof. - intros ; {! group_up_list }. + intros ; { move_up_types }. lazymatch reverse goal with | Hb:_, Ha:_,Hz : _ , Hy:_ , Hx:_ |- True => let t := constr:((ltac:(reflexivity)): Hb=b) in @@ -291,43 +305,6 @@ Proof. exact I. Qed. -(* group_up_list is insensitive to order of hypothesis. It respects - the respective order of variables in each segment. This has changed - in version 2.0.5 together with a bug fix. - Note that the deprecated move_up_types is sensitive to order. *) -Lemma test_group_up_list1_rev: forall x y:nat, - ((fun f => x = y) true) - -> forall a b: bool, forall z:nat, - 0 <= 1 -> - (0%Z <= 1%Z)%Z -> - x <= y -> - x = y -> - (0 < 1 -> 1<0) -> 0 < z -> True. -Proof. - intros ; {!< group_up_list }. - lazymatch reverse goal with - | Hb:_, Ha:_,Hz : _ , Hy:_ , Hx:_ |- True => - let t := constr:((ltac:(reflexivity)): Hb=b) in - let t := constr:((ltac:(reflexivity)): Ha=a) in - let t := constr:((ltac:(reflexivity)): Hz=z) in - let t := constr:((ltac:(reflexivity)): Hy=y) in - let t := constr:((ltac:(reflexivity)): Hx=x) in - idtac - | _ => fail "test failed (wrong order of hypothesis)!" - end. - lazymatch goal with - | hH1:_, hH2:_,hH3 : _ , hH4:_ , hH5:_ |- True => - let t := constr:((ltac:(reflexivity)):H1=hH1) in - let t := constr:((ltac:(reflexivity)): H2=hH2) in - let t := constr:((ltac:(reflexivity)): H3=hH3) in - let t := constr:((ltac:(reflexivity)): H4=hH4) in - let t := constr:((ltac:(reflexivity)): H5=hH5) in - idtac - | _ => fail "test failed (wrong order of hypothesis)!" - end. - exact I. - Qed. - (* Two more tests for the case where the top hyp is Prop-sorted. *) Lemma test_group_up_list3: @@ -435,7 +412,7 @@ Lemma test_group_up_after_subst: forall x y:nat, x = y -> (0 < 1 -> 1<0) -> 0 < z -> True. Proof. - intros ; { subst_or_idtac } ; {! group_up_list }. + intros ; { subst_or_idtac } ; { move_up_types }. lazymatch reverse goal with | Hb:_, Ha:_,Hz:_ , Hy:_ |- True => let t := constr:((ltac:(reflexivity)): Hb=b) in @@ -459,87 +436,6 @@ Proof. Qed. -Ltac substHyp H ::= - match type of H with - | Depl => fail 1 (* fail immediately, we are applying on a list of hyps. *) - | ?x = ?y => - (* subst would maybe subst using another hyp, so use replace to be sure *) - once ((is_var(x); replace x with y in *; [try clear x ; try clear H] ) - + (is_var(y);replace y with x in * ; [ try clear H])) - | _ => idtac - end. - - -(* Legacy Notations tac ;!; tac2. *) -Lemma test_tactical_semi: forall x y:nat, - ((fun f => x = y) true) - -> forall a b: bool, forall z:nat, - 0 <= 1 -> - (0%Z <= 1%Z)%Z -> - x <= y -> - x = y -> - (0 < 1 -> 1<0) -> 0 < z -> True. -Proof. - (* move_up_types is there for backward compatibility. It moves Type-Sorted hyps up. *) - intros ;; move_up_types. - lazymatch reverse goal with - | Hb:_, Ha:_,Hz : _ , Hy:_ , Hx:_ |- True => - let t := constr:((ltac:(reflexivity)): Hb=b) in - let t := constr:((ltac:(reflexivity)): Ha=a) in - let t := constr:((ltac:(reflexivity)): Hz=z) in - let t := constr:((ltac:(reflexivity)): Hy=y) in - let t := constr:((ltac:(reflexivity)): Hx=x) in - idtac - | _ => fail "test failed (wrong order of hypothesis)!" - end. - lazymatch goal with - | hH1:_, hH2:_,hH3 : _ , hH4:_ , hH5:_ |- True => - let t := constr:((ltac:(reflexivity)): H1=hH1) in - let t := constr:((ltac:(reflexivity)): H2=hH2) in - let t := constr:((ltac:(reflexivity)): H3=hH3) in - let t := constr:((ltac:(reflexivity)): H4=hH4) in - let t := constr:((ltac:(reflexivity)): H5=hH5) in - idtac - | _ => fail "test failed (wrong order of hypothesis)!" - end. - auto. -Qed. - -(* Legacy Notations tac ;; tac2. *) -Lemma test_tactical_semi_rev: forall x y:nat, - ((fun f => x = y) true) - -> forall a b: bool, forall z u:nat, - 0 <= 1 -> - (0%Z <= 1%Z)%Z -> - x <= y -> - x = y -> - (0 < 1 -> 1<0) -> 0 < z -> True. -Proof. - (* move_up_types is there for backward compatibility. It moves Type-Sorted hyps up. *) - intros ;!; move_up_types. - lazymatch reverse goal with - | Ha:_, Hb:_, Hz: _ , Hu : _ , Hy:_ , Hx:_ |- True => - let t := constr:((ltac:(reflexivity)): Hb=b) in - let t := constr:((ltac:(reflexivity)): Ha=a) in - let t := constr:((ltac:(reflexivity)): Hu=u) in - let t := constr:((ltac:(reflexivity)): Hz=z) in - let t := constr:((ltac:(reflexivity)): Hy=y) in - let t := constr:((ltac:(reflexivity)): Hx=x) in - idtac - | _ => fail "test failed (wrong order of hypothesis)!" - end. - lazymatch goal with - | hH1:_, hH2:_,hH3 : _ , hH4:_ , hH5:_ |- True => - let t := constr:((ltac:(reflexivity)): H1=hH1) in - let t := constr:((ltac:(reflexivity)): H2=hH2) in - let t := constr:((ltac:(reflexivity)): H3=hH3) in - let t := constr:((ltac:(reflexivity)): H4=hH4) in - let t := constr:((ltac:(reflexivity)): H5=hH5) in - idtac - | _ => fail "test failed (wrong order of hypothesis)!" - end. - auto. -Qed. (* Legacy Notations !!!!tac. *) @@ -641,7 +537,7 @@ Lemma foo': (a b:bool), True -> forall y z:nat, True. (* Time intros. (* .07s *) *) (* Time intros; { fun x => idtac x}. (* 1,6s *) *) - Time intros /g. (* 3s *) + Time intros /g. (* Ltac with cache: 3s, Ltac2: 0,04s *) (* Time intros ; { move_up_types }. (* ~7mn *) *) (* Time intros /n. (* 19s *) *) exact I. diff --git a/tests/demo.v b/tests/demo.v index 7c24db4..67b20da 100644 --- a/tests/demo.v +++ b/tests/demo.v @@ -20,7 +20,7 @@ From Stdlib Require Import Arith ZArith List. Require Import LibHyps.LibHyps. Lemma demo: forall x y z:nat, - x = y -> forall a b t : nat, a+1 = t+2 -> b + 5 = t - 7 -> (forall u v, v+1 = 1 -> u+1 = 1 -> a+1 = z+2) -> z = b + x-> True. + x = y -> x+y = y+ z -> forall a b t : nat, a+1 = t+2 -> b + 5 = t - 7 -> (forall u v, v+1 = 1 -> u+1 = 1 -> a+1 = z+2) -> z = b + x-> True. Proof. intros. (* ugly names *) @@ -203,10 +203,7 @@ Proof. (* Better do that on new hyps only. *) intros ; { move_up_types }. Undo. - (* Faster version dealing with the whole list of new hyps at once: *) - intros; {! group_up_list }. - Undo. - (* Shortcut for this faster version: *) + (* Shortcut: *) intros /g. Undo. (* combined with subst: *) @@ -270,59 +267,42 @@ Abort. (* customization of autorename *) -Local Open Scope autonaming_scope. +(* Local Open Scope autonaming_scope. *) Import ListNotations. - +Require Import Ltac2.Ltac2. (* Define the naming scheme as new tactic pattern matching on a type th, and the depth n of the recursive naming analysis. Here we state that a type starting with Nat.eqb should start with _Neqb, followed by the name of both arguments. #n here means normal decrement of depth. (S n) would increase depth by 1 (n-1) would decrease depth. *) -Ltac rename_hyp_2 n th := - match th with - | Nat.eqb ?x ?y => name(`_Neqb` ++ x#n ++ y#n) + +Ltac2 rename_hyp_2 _n th := + match! th with + | Nat.eqb ?x ?y => [ String "Neqb" ; Rename x ; Rename y] end. (* Then overwrite the customization hook of the naming tactic *) -Ltac rename_hyp ::= rename_hyp_2. - -Goal forall x y:nat, True. - intros. - (* computing a few names *) - (* Customize the starting depth *) +Ltac2 Set rename_hyp := rename_hyp_2. - let res := fallback_rename_hyp_name (Nat.eqb 1 2) in idtac res. - let res := fallback_rename_hyp_name (Nat.eqb x 4) in idtac res. - let res := fallback_rename_hyp_name (Nat.eqb 1 2 = false) in idtac res. - Ltac rename_depth ::= constr:(2). - let res := fallback_rename_hyp_name (Nat.eqb 1 2 = false) in idtac res. - Ltac rename_depth ::= constr:(3). -Abort. (** Suppose I want to add another naming rule: I need to cumulate the previous scheme with the new one. First define a new tactic that will replace the old one. it should call previous naming schemes in case of failure of the new scheme. It is thus important that rename_hyp_2 was defined by itself and directly as rename_hyp. *) -Ltac rename_hyp_3 n th := - match th with - | ?x = false => name(x#n ++ `_isf`) - | ?x = true => name( x#n ++ `_ist`) +Ltac2 rename_hyp_3 n th := + match! th with + | ?x = false => [ Rename x ; String "isf" ] + | ?x = true => [ Rename x ; String "ist" ] | _ => rename_hyp_2 n th (* previous naming scheme *) end. (* Then update the customization hook *) -Ltac rename_hyp ::= rename_hyp_3. +Ltac2 Set rename_hyp := rename_hyp_3. (* Close the naming scope *) -Local Close Scope autonaming_scope. - -Goal forall x y:nat, True. - intros. - let res := fallback_rename_hyp_name (Nat.eqb 1 2 = false) in - idtac res. -Abort. +Local Set Default Proof Mode "Classic". Lemma foo: forall (x:nat) (b1:bool) (y:nat) (b2:bool), x = y @@ -336,12 +316,12 @@ Lemma foo: forall (x:nat) (b1:bool) (y:nat) (b2:bool), -> z = b + 5-> z' + 1 = b + x-> x < y + b. Proof. (* Customize the starting depth *) - Ltac rename_depth ::= constr:(3). + Ltac2 Set rename_depth := 3. intros/n/g. Undo. (* Have shorter names: *) - Ltac rename_depth ::= constr:(2). + Ltac2 Set rename_depth := 2. intros/n/g.