From f41122ed8a2a2b06035be4ebba700aeb04634b54 Mon Sep 17 00:00:00 2001 From: Pierre Courtieu Date: Fri, 10 Oct 2025 19:25:37 +0200 Subject: [PATCH 01/10] WIP: refine_hd in ltac2. First working version. --- LibHyps/Especialize.v | 360 +++++++++++++++++++++++++++++++++--------- 1 file changed, 288 insertions(+), 72 deletions(-) diff --git a/LibHyps/Especialize.v b/LibHyps/Especialize.v index 499aa71..a707283 100644 --- a/LibHyps/Especialize.v +++ b/LibHyps/Especialize.v @@ -160,7 +160,7 @@ Proof. Abort. (* debug *) -(*Require Import LibHyps.LibHypsTactics. +Require Import LibHyps.LibHypsTactics. Module Prgoal_Notation. Ltac pr_goal := match goal with @@ -191,82 +191,298 @@ 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. + + +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 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). + +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. + +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. + + +(* +Goal False. + let ev1 := open_constr:(_) in + assert ev1. + ltac2:(intro_typed (Option.get (Ident.of_string "toto")) constr:(nat)). *) -(* 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] + +Ltac2 Type directarg := [ Quantif | QuantifIgnore | SubGoal | Evar(ident) ]. +Ltac2 Type namearg := [ + SubGoalAtName(ident) (* make a subgoal with named arg *) + | EvarAtName(ident,ident) (* make an evar with the named arg. *) +]. +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. *) + ]. + +(* FIXME *) +Ltac2 is_dep_prod (t:constr): bool := + match kind t with + | Prod _ subt => Bool.neg (is_closed subt) + | _ => false + end. + +Ltac2 pr_numarg () a := + match a with + | SubGoalAtNum(i) => fprintf "SubGoalAtNum(%i)" i + | SubGoalUntilNum(i) => fprintf "SubGoalUntilNum(%i)" i + | SubGoalAtAll => fprintf "SubGoalAtAll" + end. + +Ltac2 backtrack (msg:string) := Control.zero (Tactic_failure (Some (fprintf "Backtrack: %s" msg))). +Ltac2 invalid_arg (msg:string) := Control.throw (Invalid_argument (Some (Message.of_string msg))). + +Ltac2 rec refine_hd (h:ident) (ldirectarg:directarg list) (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 *) + (* pr_goal(); *) + printf "th = %t" th; + printf "%a" pr_numarg (List.hd lnumargs); + (* msgc th; *) + let newn := if is_dep_prod th then n else (Int.add n 1) in + match ldirectarg,lnameargs,lnumargs with + | [],[],[] => exact $hc (* let tc := ltac1:(h |- exact h) in tc (Ltac1.of_constr hc) *) + | (directarg::ldirectarg'),_,_ => + match Unsafe.kind th with + | Prod bnd _ => + msgs "ICI"; + 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 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 + | _ => + match lnumargs with + | [SubGoalAtAll] => exact $hc + | _ => let _ := printf "th: %t" th in + invalid_arg "Not a product (directarg)" end - | _ => idtac "Not enough products." (*; fail*) end - end. + | _ => + msgs "ICI 2"; + Control.plus + (fun() => refine_hd_name h ldirectarg lnameargs lnumargs n) + (fun _ => Control.plus + (fun () => refine_hd_num h ldirectarg lnameargs lnumargs n) + (fun _ => refine_hd h [Quantif] lnameargs lnumargs n)) + + (* (refine_hd_num (h:ident) (ldirectarg:directarg list) (lnameargs:namearg list) *) + (* (lnumargs:numarg list) (n:int)) *) + end + with refine_hd_name (h:ident) (ldirectarg:directarg list) (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 ldirectarg,lnameargs,lnumargs with + | [],[],[] => invalid_arg "refine_hd_name: assert false" + | [], (namearg :: lnameargs') , _ => + 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 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) (ldirectarg:directarg list) (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 ldirectarg,lnameargs,lnumargs with + | [],[],[] => invalid_arg "refine_hd_num: assert false" + | [],_,numarg::lnumargs' => + match Unsafe.kind th with + | Prod bnd _ => + 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 + let _ := msgc th in + let _ := msgs "not dep" in + if Int.equal newn num + then refine_hd h [SubGoal] lnameargs lnumargs' n + else refine_hd h [SubGoal] lnameargs lnumargs n + + | SubGoalAtAll => + let _ := msgs "SubGoalAtAll:" in + let _ := msgc th in + if is_dep_prod th + then backtrack "refine_hd_num: SubGoalAtAll, dep" + else refine_hd h [SubGoal] lnameargs lnumargs n + end + | _ => backtrack "Not a product (refine_hd_num)." + end + | _ => backtrack "refine_hd_num: no numarg" + end +. + +(* 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. + + let ev1 := open_constr:(_) in + assert ev1. + + + (ltac2:(refine_hd + (Option.get (Ident.of_string "H")) + [] + [EvarAtName @m @m] + [SubGoalAtAll] + 0)). + + (ltac2:(refine_hd + (Option.get (Ident.of_string "H")) + [] + [EvarAtName @m @m] + [SubGoalUntilNum 3] + 0)). + + + + + (ltac2:(refine_hd + (Option.get (Ident.of_string "H")) + [Evar @ev] + [EvarAtName @p @p ;SubGoalAtName @iii] + [SubGoalAtNum 3] + 0)). + + + + + let ev1 := open_constr:(_) in + assert ev1; + [ (ltac2:(refine_hd (Option.get (Ident.of_string "H")) + [Quantif; Quantif; Evar @p] [] [] 0)) |]. + + + match goal with | |- False => idtac end; match type of X with forall (n:_) (m:_), n < m -> _ => idtac end . + Undo 1. + especialize H with n, p; + [ match goal with | |- False => idtac end; match type of H with forall (m:_), _ < m -> _ => idtac end ]. + Undo 1. + especialize H with p as h; + [ match goal with | |- False => idtac end; match type of h with forall (n:_) (m:_), n < m -> _ => idtac end ]. + Undo 1. + especialize H with n, p as h; + [ match goal with | |- False => idtac end; match type of h with forall (m:_), _ < m -> _ => idtac end ]. + Undo 1. + especialize H with p as ?; + [ match goal with | |- False => idtac end; match type of H_spec_ with forall (n:_) (m:_), n < m -> _ => idtac end ]. + Undo 1. + especialize H with n, p as ?; + [ match goal with | |- False => idtac end; match type of H_spec_ with forall (m:_), _ < m -> _ => idtac end ]. + Undo 1. + + +Goal forall (h:forall t z x y:nat, x = y -> x = x -> z = y -> x <= y), False. +Proof. + intros h. + let ev1 := open_constr:(_) in + assert ev1. + + (* epose _. *) + (* unshelve (ltac2:(epose (_) as hhh)). *) + (* unshelve (ltac2:(specialize_id_cstr @h constr:(hhh))). *) + + + + (ltac2:(refine_hd (Option.get (Ident.of_string "h")) + [Quantif;Quantif;Evar @myx; Quantif; SubGoal; SubGoal] [] [] 0)). + + + + + + + ltac2:(intro_typed (Option.get (Ident.of_string "toto")) constr:(nat)). + + -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',_,_) => From 5af46451a306a58b8c4ca4b9cffdfdd54c25a2d7 Mon Sep 17 00:00:00 2001 From: Pierre Courtieu Date: Sat, 11 Oct 2025 19:12:18 +0200 Subject: [PATCH 02/10] Ltac2 version of especialize. --- LibHyps/Especialize.v | 914 ++++++++++++++++---------------------- LibHyps/LibHypsDebug.v | 45 ++ Makefile | 11 +- configure.sh | 31 +- testDebug.sh | 22 + tests/Especialize_tests.v | 2 +- 6 files changed, 493 insertions(+), 532 deletions(-) create mode 100644 LibHyps/LibHypsDebug.v create mode 100755 testDebug.sh diff --git a/LibHyps/Especialize.v b/LibHyps/Especialize.v index a707283..eba8bef 100644 --- a/LibHyps/Especialize.v +++ b/LibHyps/Especialize.v @@ -1,108 +1,24 @@ -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 - 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 +(* Utilities *) +Local Ltac2 is_dep_prod (t:constr): bool := + match kind t with + | Prod _ subt => Bool.neg (is_closed subt) + | _ => false 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)). +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. (* ESPECIALIZE INTERNAL DOC *) @@ -159,179 +75,167 @@ 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. +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])). +*) -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. -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 "". +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). + -Ltac2 intro_typed (name:ident) (typ:constr) := +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). -Ltac2 specialize_id_id (h:ident) (arg:ident) : unit := +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. -Ltac2 specialize_id_cstr (h:ident) (c:constr) : unit := +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. -(* -Goal False. - let ev1 := open_constr:(_) in - assert ev1. - ltac2:(intro_typed (Option.get (Ident.of_string "toto")) constr:(nat)). -*) +(* 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. *) -Ltac2 Type directarg := [ Quantif | QuantifIgnore | SubGoal | Evar(ident) ]. -Ltac2 Type namearg := [ - SubGoalAtName(ident) (* make a subgoal with named arg *) - | EvarAtName(ident,ident) (* make an evar with the named arg. *) -]. -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. *) - ]. -(* FIXME *) -Ltac2 is_dep_prod (t:constr): bool := - match kind t with - | Prod _ subt => Bool.neg (is_closed subt) - | _ => false - end. - -Ltac2 pr_numarg () a := - match a with - | SubGoalAtNum(i) => fprintf "SubGoalAtNum(%i)" i - | SubGoalUntilNum(i) => fprintf "SubGoalUntilNum(%i)" i - | SubGoalAtAll => fprintf "SubGoalAtAll" - end. - -Ltac2 backtrack (msg:string) := Control.zero (Tactic_failure (Some (fprintf "Backtrack: %s" msg))). -Ltac2 invalid_arg (msg:string) := Control.throw (Invalid_argument (Some (Message.of_string msg))). - -Ltac2 rec refine_hd (h:ident) (ldirectarg:directarg list) (lnameargs:namearg list) +Local Ltac2 rec refine_hd (h:ident) (ldirectarg:directarg list) (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 *) - (* pr_goal(); *) - printf "th = %t" th; - printf "%a" pr_numarg (List.hd lnumargs); - (* msgc th; *) + (* 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 - match ldirectarg,lnameargs,lnumargs with - | [],[],[] => exact $hc (* let tc := ltac1:(h |- exact h) in tc (Ltac1.of_constr hc) *) - | (directarg::ldirectarg'),_,_ => - match Unsafe.kind th with - | Prod bnd _ => - msgs "ICI"; - 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 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 - | _ => - match lnumargs with - | [SubGoalAtAll] => exact $hc - | _ => let _ := printf "th: %t" th in - invalid_arg "Not a product (directarg)" + (* 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 + | _ => (*base case *) + match ldirectarg,lnameargs,lnumargs with + | [],[],[] => exact $hc + | [],[],[SubGoalAtAll] => exact $hc + | _ => invalid_arg "Not a product (others)" end - | _ => - msgs "ICI 2"; - Control.plus - (fun() => refine_hd_name h ldirectarg lnameargs lnumargs n) - (fun _ => Control.plus - (fun () => refine_hd_num h ldirectarg lnameargs lnumargs n) - (fun _ => refine_hd h [Quantif] lnameargs lnumargs n)) - (* (refine_hd_num (h:ident) (ldirectarg:directarg list) (lnameargs:namearg list) *) (* (lnumargs:numarg list) (n:int)) *) end - with refine_hd_name (h:ident) (ldirectarg:directarg list) (lnameargs:namearg list) + 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 ldirectarg,lnameargs,lnumargs with - | [],[],[] => invalid_arg "refine_hd_name: assert false" - | [], (namearg :: lnameargs') , _ => + match lnameargs with + | namearg :: lnameargs' => 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 namearg with | SubGoalAtName nme => if map_default (Ident.equal nme) false h_premis @@ -346,16 +250,15 @@ Ltac2 rec refine_hd (h:ident) (ldirectarg:directarg list) (lnameargs:namearg lis end | _ => backtrack "refine_hd_name: no namearg" end - with refine_hd_num (h:ident) (ldirectarg:directarg list) (lnameargs:namearg list) + 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 ldirectarg,lnameargs,lnumargs with - | [],[],[] => invalid_arg "refine_hd_num: assert false" - | [],_,numarg::lnumargs' => + match lnumargs with + | numarg::lnumargs' => match Unsafe.kind th with - | Prod bnd _ => + | Prod _ _ => match numarg with | SubGoalAtNum num => if is_dep_prod th @@ -369,29 +272,52 @@ Ltac2 rec refine_hd (h:ident) (ldirectarg:directarg list) (lnameargs:namearg lis if is_dep_prod th then backtrack "refine_hd_num: SubGoalUntilNum, dep" else - let _ := msgc th in - let _ := msgs "not dep" in if Int.equal newn num then refine_hd h [SubGoal] lnameargs lnumargs' n else refine_hd h [SubGoal] lnameargs lnumargs n | SubGoalAtAll => - let _ := msgs "SubGoalAtAll:" in - let _ := msgc th in if is_dep_prod th then backtrack "refine_hd_num: SubGoalAtAll, dep" else refine_hd h [SubGoal] lnameargs lnumargs n end - | _ => backtrack "Not a product (refine_hd_num)." + | _ => invalid_arg "Not a product (refine_hd_num)." end | _ => backtrack "refine_hd_num: no numarg" - end -. + end. + +(* initialize n to zero. *) +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), @@ -406,12 +332,11 @@ Proof. assert ev1. - (ltac2:(refine_hd - (Option.get (Ident.of_string "H")) - [] - [EvarAtName @m @m] - [SubGoalAtAll] - 0)). + ltac2:(refine_spec + (Option.get (Ident.of_string "H")) + [EvarAtName @m @m] + [SubGoalAtAll]). + Undo 1. (ltac2:(refine_hd (Option.get (Ident.of_string "H")) @@ -419,164 +344,28 @@ Proof. [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 3] + [SubGoalAtNum 4] 0)). +*) - - - let ev1 := open_constr:(_) in - assert ev1; - [ (ltac2:(refine_hd (Option.get (Ident.of_string "H")) - [Quantif; Quantif; Evar @p] [] [] 0)) |]. - - - match goal with | |- False => idtac end; match type of X with forall (n:_) (m:_), n < m -> _ => idtac end . - Undo 1. - especialize H with n, p; - [ match goal with | |- False => idtac end; match type of H with forall (m:_), _ < m -> _ => idtac end ]. - Undo 1. - especialize H with p as h; - [ match goal with | |- False => idtac end; match type of h with forall (n:_) (m:_), n < m -> _ => idtac end ]. - Undo 1. - especialize H with n, p as h; - [ match goal with | |- False => idtac end; match type of h with forall (m:_), _ < m -> _ => idtac end ]. - Undo 1. - especialize H with p as ?; - [ match goal with | |- False => idtac end; match type of H_spec_ with forall (n:_) (m:_), n < m -> _ => idtac end ]. - Undo 1. - especialize H with n, p as ?; - [ match goal with | |- False => idtac end; match type of H_spec_ with forall (m:_), _ < m -> _ => idtac end ]. - Undo 1. - - -Goal forall (h:forall t z x y:nat, x = y -> x = x -> z = y -> x <= y), False. -Proof. - intros h. - let ev1 := open_constr:(_) in - assert ev1. - - (* epose _. *) - (* unshelve (ltac2:(epose (_) as hhh)). *) - (* unshelve (ltac2:(specialize_id_cstr @h constr:(hhh))). *) - - - - (ltac2:(refine_hd (Option.get (Ident.of_string "h")) - [Quantif;Quantif;Evar @myx; Quantif; SubGoal; SubGoal] [] [] 0)). - - - - - - - ltac2:(intro_typed (Option.get (Ident.of_string "toto")) constr:(nat)). - - - - let newn := if_is_dep_prod h ltac:(constr:(n)) ltac:(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) - end - | _ => fail 0 +Local Ltac2 cmp_numarg a b := + match a with + SubGoalAtNum na => + match b with + SubGoalAtNum nb => Int.compare na nb + | _ => -1 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" + | _ => -1 end. -(* initialize n to zero. *) -Ltac refine_spec h lnameargs lnumargs := refine_hd h constr:(@nil spec_arg) lnameargs lnumargs 0. - +Local Ltac2 sort_numargs (l: numarg list): numarg list:= List.sort cmp_numarg l. @@ -590,150 +379,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). - -(* 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."))) +Local Ltac2 interp_ltac1_hyp (h:Ltac1.t) : constr := Option.get (Ltac1.to_constr h). - | _ => [] - 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 @@ -749,10 +536,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 @@ -776,7 +562,6 @@ Ltac gen_hyp_name h := match goal with end. Ltac dummy_term := constr:(Prop). - (* ESPECIALIZE AT *) (* ********************* *) @@ -965,7 +750,42 @@ 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: *) (* @@ -1005,7 +825,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. @@ -1036,3 +856,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/LibHypsDebug.v b/LibHyps/LibHypsDebug.v new file mode 100644 index 0000000..1b16a4a --- /dev/null +++ b/LibHyps/LibHypsDebug.v @@ -0,0 +1,45 @@ +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 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_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. + + +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 "". + 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..6569323 100755 --- a/configure.sh +++ b/configure.sh @@ -1,5 +1,27 @@ #!/bin/bash +DEVOPT=no + +POSITIONAL=() +while [[ $# -gt 0 ]] +do +key="$1" + +case $key in + --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.) @@ -27,11 +49,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" + FILESTEST=$(cd tests && find . -name "*.v" | grep -v "incremental" ) PROJECTDIRTESTS="tests" gen_projet_file "$FILESTEST" "$PROJECTDIRTESTS" "resources/coq_project.tests" 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 *) From 2d71c73cc6f5c64c25c20fb74ee4f45ff0e9acf4 Mon Sep 17 00:00:00 2001 From: Pierre Courtieu Date: Tue, 21 Oct 2025 19:59:45 +0200 Subject: [PATCH 03/10] WIP Ltac2 libHypsNaming. --- LibHyps/Especialize.v | 9 - LibHyps/LibHypsDebug.v | 13 +- LibHyps/LibHypsNaming.v | 572 ++++++++++++++++++++++++++++++++++++++-- LibHyps/TacNewHyps.v | 362 +++++++++---------------- 4 files changed, 692 insertions(+), 264 deletions(-) diff --git a/LibHyps/Especialize.v b/LibHyps/Especialize.v index eba8bef..8c15c92 100644 --- a/LibHyps/Especialize.v +++ b/LibHyps/Especialize.v @@ -11,15 +11,6 @@ Local Ltac2 is_dep_prod (t:constr): bool := | _ => false 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. - (* ESPECIALIZE INTERNAL DOC *) (* We show here by hand what the especialize tactic does. We start diff --git a/LibHyps/LibHypsDebug.v b/LibHyps/LibHypsDebug.v index 1b16a4a..c7b2a7c 100644 --- a/LibHyps/LibHypsDebug.v +++ b/LibHyps/LibHypsDebug.v @@ -24,17 +24,28 @@ 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) := + +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 diff --git a/LibHyps/LibHypsNaming.v b/LibHyps/LibHypsNaming.v index 94f15b2..cd77426 100644 --- a/LibHyps/LibHypsNaming.v +++ b/LibHyps/LibHypsNaming.v @@ -4,9 +4,16 @@ From Stdlib Require Import Arith ZArith List. Require Import LibHyps.TacNewHyps. -Import ListNotations. -Local Open Scope list. - +(* 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))). + (** This file defines a tactic "autorename h" (and "autorename_strict h") that automatically rename hypothesis h followinh a systematic, but customizable heuristic. @@ -45,6 +52,539 @@ Ltac rename_hyp1 n th := Ltac rename_hyp ::= my_rename_hyp. >> *) +Ltac2 Type hypnames := string list. +Ltac2 add_suffix := true. + +(* Elements of l are supposed to already start with "_" *) +Ltac2 build_name_gen (sep:string) (suffx:bool) (l:string list) := + String.app (String.concat sep l) (if suffx then "_" else ""). + +Ltac2 build_name l := build_name_gen "_" add_suffix l. +Ltac2 build_name_no_suffix l := build_name_gen "_" false l. + +(* 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_. + + 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 *) + +Ltac2 Type numerical_names_style := bool. + +Ltac2 string_of_int (i:int) := Message.to_string (Message.of_int i). + +(** Generate fresh name for numerical constants. + + Warning: problem here: hyps names may end with a digit: Coq may + *replace* the digit in case of name clash. If you are bitten by + 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 *) +Ltac2 num_nosufx (i:int) := + msgs ". num_nosufx"; + printf ". i = %s" (string_of_int i); + let res := String.app "_" (string_of_int i) in + printf ". res = %s" res; + msgs ". num_nosufx: end"; + res. +Ltac2 num_sufx (i:int) (sfx:string) := String.app "_" (String.app (string_of_int i) sfx). + +(* TODO: find a way to make a string from nat, Z and N *) +Ltac2 numerical_names_nosufx (t:constr):string := + printf "...NUM: %t" t; + if is_closed t then + match! t with + | 0%Z => num_nosufx 0 + | 1%Z => num_nosufx 1 + | 2%Z => num_nosufx 2 + | 3%Z => num_nosufx 3 + | 4%Z => num_nosufx 4 + | 5%Z => num_nosufx 5 + | 6%Z => num_nosufx 6 + | 7%Z => num_nosufx 7 + | 8%Z => num_nosufx 8 + | 9%Z => num_nosufx 9 + | 10%Z => num_nosufx 10 + (* | Z0 => num_nosufx 0 *) + | O%nat => num_nosufx 0 + | 1%nat => num_nosufx 1 + | 2%nat => num_nosufx 2 + | 3%nat => num_nosufx 3 + | 4%nat => num_nosufx 4 + | 5%nat => num_nosufx 5 + | 6%nat => num_nosufx 6 + | 7%nat => num_nosufx 7 + | 8%nat => num_nosufx 8 + | 9%nat => num_nosufx 9 + | 10%nat => num_nosufx 10 + | O%N => num_nosufx 0 + | 1%N => num_nosufx 1 + | 2%N => num_nosufx 2 + | 3%N => num_nosufx 3 + | 4%N => num_nosufx 4 + | 5%N => num_nosufx 5 + | 6%N => num_nosufx 6 + | 7%N => num_nosufx 7 + | 8%N => num_nosufx 8 + | 9%N => num_nosufx 9 + | 10%N => num_nosufx 10 + | _ => backtrack "not recognized as a number " + end + else + backtrack "not a nameable number". + +Ltac2 numerical_names_sufx t := + match! t with + | 0%Z => num_sufx 0 "z" + | 1%Z => num_sufx 1 "z" + | 2%Z => num_sufx 2 "z" + | 3%Z => num_sufx 3 "z" + | 4%Z => num_sufx 4 "z" + | 5%Z => num_sufx 5 "z" + | 6%Z => num_sufx 6 "z" + | 7%Z => num_sufx 7 "z" + | 8%Z => num_sufx 8 "z" + | 9%Z => num_sufx 9 "z" + | 10%Z => num_sufx 10 "z" + (* | Z0 => num_sufx 0 *) + | O%nat => num_sufx 0 "n" + | 1%nat => num_sufx 1 "n" + | 2%nat => num_sufx 2 "n" + | 3%nat => num_sufx 3 "n" + | 4%nat => num_sufx 4 "n" + | 5%nat => num_sufx 5 "n" + | 6%nat => num_sufx 6 "n" + | 7%nat => num_sufx 7 "n" + | 8%nat => num_sufx 8 "n" + | 9%nat => num_sufx 9 "n" + | 10%nat => num_sufx 10 "n" + | O%N => num_sufx 0 "N" + | 1%N => num_sufx 1 "N" + | 2%N => num_sufx 2 "N" + | 3%N => num_sufx 3 "N" + | 4%N => num_sufx 4 "N" + | 5%N => num_sufx 5 "N" + | 6%N => num_sufx 6 "N" + | 7%N => num_sufx 7 "N" + | 8%N => num_sufx 8 "N" + | 9%N => num_sufx 9 "N" + | 10%N => num_sufx 10 "N" + end. + +(* Redefine at will *) +Ltac2 numerical_names: constr -> string:= numerical_names_nosufx. + +(** 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 rename_depth := 3. + +(** Default prefix for hypothesis names. *) +Ltac2 default_prefix():string := "h". + +(** A few special default chunks, for special cases in the naming heuristic. *) +Ltac2 impl_prefix() := "_impl". +Ltac2 forall_prefix() := "_all". +Ltac2 exists_prefix() := "_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 rename_hyp stop th := backtrack "rename_hyp". +Ltac2 rename_hyp_default n th := backtrack "rename_hyp_default". + +(* TODO: 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 1 + | _ => let _ := constr:(fun b => ($z b, $z b)) in 2 + end + end + | _ => 0 + end. + + + +Ltac2 percent():char := (Char.of_int 37). +Ltac2 arobase():char := (Char.of_int 64). +Ltac2 space():char := (Char.of_int 32). +Ltac2 parg():char := (Char.of_int 40). +Ltac2 pard():char := (Char.of_int 41). + +(* Ltac2 Eval (Char.to_int (String.get ")" 0)). *) + +Ltac2 set_forbidden_chars (): char list := [space();pard();parg()]. +Ltac2 set_removable_chars (): char list := [percent();arobase()]. +Ltac2 set_suspect_chars (): char list := List.append (set_forbidden_chars()) (set_removable_chars()). +Ltac2 set_forbidden_charints (): int list := List.map Char.to_int (set_forbidden_chars()). +Ltac2 set_removable_charints (): int list := List.map Char.to_int (set_removable_chars()). +Ltac2 set_suspect_charints (): int list := List.map Char.to_int (set_suspect_chars()). + +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. + +Ltac2 string_count_if (p:char -> bool) (s:string) : int := + let lgth := String.length s in + let rec count acc i := + if Int.ge i lgth then acc + else if p (String.get s i) then count (Int.add 1 acc) (Int.add 1 i) + else count acc (Int.add 1 i) + in + count 0 0. + +Ltac2 string_remove (p:char -> bool) (s:string) : string := + let lgth := String.length s in + let nbgood := string_count_if (fun c => Bool.neg (p c)) s in + let res := String.make nbgood (arobase()) in + let rec fill k i: unit := + if Int.ge i lgth then () + else + let c := String.get s i in + if p c then fill k (Int.add 1 i) + else (String.set res k c; fill (Int.add 1 k) (Int.add 1 i)) in + fill 0 0; + res. + +Ltac2 forbidden_charint (c:char):bool := (List.mem Int.equal (Char.to_int c) (set_forbidden_charints())). +Ltac2 removeable_charint (c:char):bool := (List.mem Int.equal (Char.to_int c) (set_removable_charints())). +Ltac2 suspect_charint (c:char):bool := (List.mem Int.equal (Char.to_int c) (set_suspect_charints())). + +Ltac2 Eval (string_remove (fun c => (Char.equal c (arobase()))) "az@er% % @o"). +Ltac2 Eval (string_remove forbidden_charint "az@er% % @o"). +Ltac2 Eval (string_remove suspect_charint "az@er% % @o"). + +Ltac2 id_of_constr (t:constr) : string option := + let s:string := Message.to_string (fprintf "%t" t) in + if string_forall (fun c => Bool.neg (forbidden_charint c)) s + then + let s := string_remove removeable_charint s in + if string_forall (fun c => Bool.neg (Char.equal (space()) c)) s then Some s else None + else None. + + + +(* Ltac2 print_id (t:constr) : string option := *) +(* let (idopt,_) := Fresh.next (Fresh.Free.empty) t in *) +(* Some (Ident.to_string idopt). *) + +(** Build a chunk from a simple term: either a number or a freshable + term. *) +Ltac2 box_name t : ident := + 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 => s + | None => + match Unsafe.kind t with + | Unsafe.Constant cstt _ => + let id:ident := List.last (Env.path (Std.ConstRef cstt)) in + id + | Unsafe.Var id => 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 + Option.get (Ident.of_string s) + | _ => + if is_closed t then + printf ". BEFORE NUM %t" t; + let s := numerical_names t in + printf ". AFTER NUM %t -> %s" t s; + Option.get (Ident.of_string s) + else backtrack "cannot be a number" + end + end. + +Local Ltac2 is_dep_prod (t:constr): bool := + match kind t with + | Prod _ subt => Bool.neg (is_closed subt) + | _ => false + end. + + +(** 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. *) +Ltac2 rec rename_app (nonimpl:int) (stop:int) (acc:string list) th: string list := + match id_of_constr th with + | Some s => s::acc + | None => + printf "## rename_app (nonimpl=%i) (stop=%i) %t " nonimpl stop th; + match Unsafe.kind th with + | App f args => + let newstop:int := Int.sub stop 1 in + printf "...Arrays.sub args %i %i: " (Int.sub (Array.length args) nonimpl) nonimpl; + Array.iter (fun e => printf "....%t" e) args; + let nonimplicitsargs := Array.sub args (Int.sub (Array.length args) nonimpl) nonimpl in + let nme_array := + Array.map (fun arg => (*Control.plus*) ((*fun () => *) fallback_rename_hyp newstop arg) (* (fun _ => [])*)) + nonimplicitsargs in + let l: string list := List.flatten (Array.to_list nme_array) in + let f' := Control.plus (fun() => Ident.to_string(box_name f)) (fun _ => "?1") in + f' :: (List.append l acc) + | _ => (let f':string := Control.plus (fun() => Ident.to_string(box_name th)) (fun _ => "?2") in + printf ". NO APP %s" f'; f' :: acc) +end +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:constr) : string list := + printf "## fallback_rename_hyp_quantif (stop=%i) %t " stop th; + let newstop := Int.sub stop 1 in + match Unsafe.kind th with + | Prod bnd subth => + if is_dep_prod th + then + let sufx:ident := Option.default (Option.get (Ident.of_string "_h")) (Constr.Binder.name bnd) in + let remain := fallback_rename_hyp newstop subth in + forall_prefix() :: Ident.to_string sufx :: remain + else + let sufx := fallback_rename_hyp 1 (Constr.Binder.type bnd) in + let remain := fallback_rename_hyp newstop subth in + impl_prefix() :: (List.append sufx remain) + | _ => backtrack "no product" + end + +with fallback_rename_hyp_specials stop th :string list := + printf "## fallback_rename_hyp_specials (stop=%i) %t " stop th; + let newstop := Int.sub stop 1 in + Control.plus + (* First see if user has something that applies *) + (fun() => rename_hyp newstop th) + (* if it fails try default specials *) + (fun _ => rename_hyp_default newstop th) + +with fallback_rename_hyp stop th:string list := + printf "## fallback_rename_hyp (stop=%i) %t " stop th; + if Int.le stop 0 then [] + else + Control.plus (fun () => fallback_rename_hyp_specials stop th) + (fun _ => match Unsafe.kind th with + | Prod _ _ => fallback_rename_hyp_quantif stop th + | _ => + printf "...before count_impl: %t" th; + let numnonimpl := count_impl th in + printf "..after count_impl: %i" numnonimpl; + printf "## FALLBACK 1 rename_app %i %i %t " numnonimpl stop th; + let res := rename_app numnonimpl stop [] th in + msgs "..FALLBACK 2"; + res + end). + + + Unset Printing Notations. + +(* Ltac2 Eval (count_impl constr:(3 + 4)). *) + +Parameters X Y: nat -> Prop. +Parameters PX: X 3. +Parameters PY: Y 3. + +Goal forall [A : Type] (P Q : A -> Prop) (x : A), P x -> Q x -> (exists2 x : A, P x & Q x) -> False. + + intros A P Q x H H0 H1. + ltac2:(let l := fallback_rename_hyp 9 constr:(exists2 x0 : A, P x0 & Q x0) in + printf "BEFORE BUILDNAME %a " (pr_list pr_string) l; + let nme := build_name l in + printf "%s" nme). +Abort. + +Goal forall n m p : nat, n m<= p -> True. +Proof. + intros n m p H H0. + + Unset Printing Notations. + + ltac2:(let l := fallback_rename_hyp 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 := fallback_rename_hyp 3 constr:(Nat.clearbit 3 4%nat = 0) in + printf "BEFORE BUILDNAME"; + let nme := build_name l in + printf "%s" nme). + + ltac2:(let l := fallback_rename_hyp 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 := fallback_rename_hyp 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 := fallback_rename_hyp 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 := fallback_rename_hyp 4 constr:(Nat.clearbit 3%nat 4%nat) in + let nme := build_name l in + printf "%s" nme). + + ltac2:(let l := fallback_rename_hyp 4 constr:(Nat.clearbit 3%nat 4%nat) in + printf "%a" (pr_list (fun () s => fprintf "%s" s)) l). + + ltac2:(let nme := rename_app 1 2 [] constr:(Nat.clearbit 3%nat 4%nat) in + printf "%s" (List.hd nme)). + . + + + +(** 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. *) +Ltac rename_hyp stop th := fail. +(** This will later contain a few default fallback naming strategy. *) +Ltac rename_hyp_default stop th := + fail. + +(** 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. + + +Ltac build_name l := build_name_gen add_suffix l. +Ltac build_name_no_suffix l := build_name_gen constr:(false) l. + + (** * Implementation principle: @@ -531,7 +1071,7 @@ Local Close Scope autonaming_scope. (* Entry point of the renaming code. *) Ltac fallback_rename_hyp_name th := let depth := rename_depth in - let h := constr:(ltac:(let x := default_prefix in exact x)) in + let $h := constr:(ltac:(let x := default_prefix in exact x)) in let l := fallback_rename_hyp depth th in match l with nil => fail 1 @@ -543,38 +1083,38 @@ Ltac fallback_rename_hyp_name th := Inductive LHMsg t (h:t) := LHMsgC: LHMsg t h. Notation "h : t" := (LHMsgC t h) (at level 1,only printing, format -"'[ ' h ':' '/' '[' t ']' ']'"). +"'[ ' $h ':' '/' '[' t ']' ']'"). -Ltac rename_hyp_with_name h th := fail. +Ltac 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 +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 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 *) + 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 *) + rename $h into 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 *) + fail 1 "no renaming pattern for " c (* "no renaming pattern for " $h *) + | _ => idtac (* not in Prop or "no renaming pattern for " $h *) end end. (* Tactic renaming hypothesis H. *) -Ltac autorename H := try autorename_strict H. +Ltac autorename $h := try autorename_strict H. (* (* Tests *) @@ -586,9 +1126,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/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 }. *) From 177157ab5d9ce051f82b614cc3a7adc86b36f3b9 Mon Sep 17 00:00:00 2001 From: Pierre Courtieu Date: Fri, 24 Oct 2025 19:50:44 +0200 Subject: [PATCH 04/10] First version of Ltac2 autorename. --- LibHyps/LibHypsNaming.v | 650 ++++++++++++++++++++++++++++++---------- 1 file changed, 485 insertions(+), 165 deletions(-) diff --git a/LibHyps/LibHypsNaming.v b/LibHyps/LibHypsNaming.v index cd77426..543bd73 100644 --- a/LibHyps/LibHypsNaming.v +++ b/LibHyps/LibHypsNaming.v @@ -3,7 +3,8 @@ "expat license". You should have recieved a LICENSE file with it. *) From Stdlib Require Import Arith ZArith List. -Require Import LibHyps.TacNewHyps. +Require LibHyps.TacNewHyps. +Import TacNewHyps.Notations. (* Import ListNotations. *) (* Local Open Scope list. *) Require Import Ltac2.Ltac2. @@ -13,7 +14,7 @@ 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 _ => ()). (** This file defines a tactic "autorename h" (and "autorename_strict h") that automatically rename hypothesis h followinh a systematic, but customizable heuristic. @@ -52,15 +53,18 @@ Ltac rename_hyp1 n th := Ltac rename_hyp ::= my_rename_hyp. >> *) +Ltac2 Type rename_directive := [ String(string) | RecRename(int,constr) ]. +Ltac2 Type rename_directives := rename_directive list. + Ltac2 Type hypnames := string list. -Ltac2 add_suffix := true. +Ltac2 mutable add_suffix := true. (* Elements of l are supposed to already start with "_" *) Ltac2 build_name_gen (sep:string) (suffx:bool) (l:string list) := String.app (String.concat sep l) (if suffx then "_" else ""). -Ltac2 build_name l := build_name_gen "_" add_suffix l. -Ltac2 build_name_no_suffix l := build_name_gen "_" false l. +Ltac2 build_name l := build_name_gen "_" add_suffix (List.rev l). +Ltac2 build_name_no_suffix l := build_name_gen "_" false (List.rev l). (* This sets the way numerical constants are displayed, default value is set below to numerical_names_nosufx, which will give the same @@ -71,6 +75,7 @@ Ltac2 build_name_no_suffix l := build_name_gen "_" false l. Ltac numerical_names ::= numerical_names_sufx *) Ltac2 Type numerical_names_style := bool. +Ltac2 mutable numerical_names := false. Ltac2 string_of_int (i:int) := Message.to_string (Message.of_int i). @@ -88,47 +93,47 @@ Ltac2 num_nosufx (i:int) := printf ". res = %s" res; msgs ". num_nosufx: end"; res. -Ltac2 num_sufx (i:int) (sfx:string) := String.app "_" (String.app (string_of_int i) sfx). +(* Ltac2 num_sufx (i:int) (sfx:string) := (String.app (string_of_int i) sfx). *) + (* TODO: find a way to make a string from nat, Z and N *) Ltac2 numerical_names_nosufx (t:constr):string := printf "...NUM: %t" t; if is_closed t then match! t with - | 0%Z => num_nosufx 0 - | 1%Z => num_nosufx 1 - | 2%Z => num_nosufx 2 - | 3%Z => num_nosufx 3 - | 4%Z => num_nosufx 4 - | 5%Z => num_nosufx 5 - | 6%Z => num_nosufx 6 - | 7%Z => num_nosufx 7 - | 8%Z => num_nosufx 8 - | 9%Z => num_nosufx 9 - | 10%Z => num_nosufx 10 - (* | Z0 => num_nosufx 0 *) - | O%nat => num_nosufx 0 - | 1%nat => num_nosufx 1 - | 2%nat => num_nosufx 2 - | 3%nat => num_nosufx 3 - | 4%nat => num_nosufx 4 - | 5%nat => num_nosufx 5 - | 6%nat => num_nosufx 6 - | 7%nat => num_nosufx 7 - | 8%nat => num_nosufx 8 - | 9%nat => num_nosufx 9 - | 10%nat => num_nosufx 10 - | O%N => num_nosufx 0 - | 1%N => num_nosufx 1 - | 2%N => num_nosufx 2 - | 3%N => num_nosufx 3 - | 4%N => num_nosufx 4 - | 5%N => num_nosufx 5 - | 6%N => num_nosufx 6 - | 7%N => num_nosufx 7 - | 8%N => num_nosufx 8 - | 9%N => num_nosufx 9 - | 10%N => num_nosufx 10 + | 0%Z => "0" + | 1%Z => "1" + | 2%Z => "2" + | 3%Z => "3" + | 4%Z => "4" + | 5%Z => "5" + | 6%Z => "6" + | 7%Z => "7" + | 8%Z => "8" + | 9%Z => "9" + | 10%Z => "10" + | O%nat => "0" + | 1%nat => "1" + | 2%nat => "2" + | 3%nat => "3" + | 4%nat => "4" + | 5%nat => "5" + | 6%nat => "6" + | 7%nat => "7" + | 8%nat => "8" + | 9%nat => "9" + | 10%nat => "10" + | O%N => "0" + | 1%N => "1" + | 2%N => "2" + | 3%N => "3" + | 4%N => "4" + | 5%N => "5" + | 6%N => "6" + | 7%N => "7" + | 8%N => "8" + | 9%N => "9" + | 10%N => "10" | _ => backtrack "not recognized as a number " end else @@ -136,66 +141,68 @@ Ltac2 numerical_names_nosufx (t:constr):string := Ltac2 numerical_names_sufx t := match! t with - | 0%Z => num_sufx 0 "z" - | 1%Z => num_sufx 1 "z" - | 2%Z => num_sufx 2 "z" - | 3%Z => num_sufx 3 "z" - | 4%Z => num_sufx 4 "z" - | 5%Z => num_sufx 5 "z" - | 6%Z => num_sufx 6 "z" - | 7%Z => num_sufx 7 "z" - | 8%Z => num_sufx 8 "z" - | 9%Z => num_sufx 9 "z" - | 10%Z => num_sufx 10 "z" + | 0%Z => "0z" + | 1%Z => "1z" + | 2%Z => "2z" + | 3%Z => "3z" + | 4%Z => "4z" + | 5%Z => "5z" + | 6%Z => "6z" + | 7%Z => "7z" + | 8%Z => "8z" + | 9%Z => "9z" + | 10%Z => "10z" (* | Z0 => num_sufx 0 *) - | O%nat => num_sufx 0 "n" - | 1%nat => num_sufx 1 "n" - | 2%nat => num_sufx 2 "n" - | 3%nat => num_sufx 3 "n" - | 4%nat => num_sufx 4 "n" - | 5%nat => num_sufx 5 "n" - | 6%nat => num_sufx 6 "n" - | 7%nat => num_sufx 7 "n" - | 8%nat => num_sufx 8 "n" - | 9%nat => num_sufx 9 "n" - | 10%nat => num_sufx 10 "n" - | O%N => num_sufx 0 "N" - | 1%N => num_sufx 1 "N" - | 2%N => num_sufx 2 "N" - | 3%N => num_sufx 3 "N" - | 4%N => num_sufx 4 "N" - | 5%N => num_sufx 5 "N" - | 6%N => num_sufx 6 "N" - | 7%N => num_sufx 7 "N" - | 8%N => num_sufx 8 "N" - | 9%N => num_sufx 9 "N" - | 10%N => num_sufx 10 "N" + | O%nat => "0n" + | 1%nat => "1n" + | 2%nat => "2n" + | 3%nat => "3n" + | 4%nat => "4n" + | 5%nat => "5n" + | 6%nat => "6n" + | 7%nat => "7n" + | 8%nat => "8n" + | 9%nat => "9n" + | 10%nat => "10n" + | O%N => "0N" + | 1%N => "1N" + | 2%N => "2N" + | 3%N => "3N" + | 4%N => "4N" + | 5%N => "5N" + | 6%N => "6N" + | 7%N => "7N" + | 8%N => "8N" + | 9%N => "9N" + | 10%N => "10N" end. (* Redefine at will *) -Ltac2 numerical_names: constr -> string:= numerical_names_nosufx. +Ltac2 add_numerical_names (): constr -> string:= + if numerical_names then numerical_names_sufx else numerical_names_nosufx. + (** 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 rename_depth := 3. +Ltac2 mutable rename_depth := 3. (** Default prefix for hypothesis names. *) Ltac2 default_prefix():string := "h". (** A few special default chunks, for special cases in the naming heuristic. *) -Ltac2 impl_prefix() := "_impl". -Ltac2 forall_prefix() := "_all". -Ltac2 exists_prefix() := "_ex". +Ltac2 impl_prefix() := "impl". +Ltac2 forall_prefix() := "all". +Ltac2 exists_prefix() := "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 rename_hyp stop th := backtrack "rename_hyp". -Ltac2 rename_hyp_default n th := backtrack "rename_hyp_default". +Ltac2 mutable rename_hyp (stop:int) (th:constr): rename_directives := backtrack "rename_hyp". +Ltac2 mutable rename_hyp_default (n:int) (th:constr): rename_directives := backtrack "rename_hyp_default". (* TODO: find something better to detect implicits!! *) (* Determines the number of non "head" implicit arguments, i.e. implicit @@ -304,8 +311,8 @@ Ltac2 count_impl th := end | (?z _) => match! th with - | _ => let _ := constr:(fun b => ($z b, $z _)) in 1 - | _ => let _ := constr:(fun b => ($z b, $z b)) in 2 + | _ => let _ := constr:(fun b => ($z b, $z _)) in 0 + | _ => let _ := constr:(fun b => ($z b, $z b)) in 1 end end | _ => 0 @@ -365,13 +372,6 @@ Ltac2 Eval (string_remove (fun c => (Char.equal c (arobase()))) "az@er% % @o"). Ltac2 Eval (string_remove forbidden_charint "az@er% % @o"). Ltac2 Eval (string_remove suspect_charint "az@er% % @o"). -Ltac2 id_of_constr (t:constr) : string option := - let s:string := Message.to_string (fprintf "%t" t) in - if string_forall (fun c => Bool.neg (forbidden_charint c)) s - then - let s := string_remove removeable_charint s in - if string_forall (fun c => Bool.neg (Char.equal (space()) c)) s then Some s else None - else None. @@ -381,36 +381,45 @@ Ltac2 id_of_constr (t:constr) : string option := (** Build a chunk from a simple term: either a number or a freshable term. *) -Ltac2 box_name t : ident := +Ltac2 box_name t : string := 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 => s - | None => + | Some _ => s + | None => match Unsafe.kind t with | Unsafe.Constant cstt _ => let id:ident := List.last (Env.path (Std.ConstRef cstt)) in - id - | Unsafe.Var id => id + 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 - Option.get (Ident.of_string s) + s | _ => if is_closed t then printf ". BEFORE NUM %t" t; - let s := numerical_names t in + let s := add_numerical_names () t in printf ". AFTER NUM %t -> %s" t s; - Option.get (Ident.of_string s) + s else backtrack "cannot be a number" end end. +(* Ltac2 id_of_constr (t:constr) : string option := *) +(* let s:string := Message.to_string (fprintf "%t" t) in *) +(* if string_forall (fun c => Bool.neg (forbidden_charint c)) s *) +(* then *) +(* let s := string_remove removeable_charint s in *) +(* if string_forall (fun c => Bool.neg (Char.equal (space()) c)) s then Some s else None *) +(* else None. *) + + Local Ltac2 is_dep_prod (t:constr): bool := match kind t with | Prod _ subt => Bool.neg (is_closed subt) @@ -418,79 +427,349 @@ Local Ltac2 is_dep_prod (t:constr): bool := 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. *) -Ltac2 rec rename_app (nonimpl:int) (stop:int) (acc:string list) th: string list := - match id_of_constr th with - | Some s => s::acc - | None => - printf "## rename_app (nonimpl=%i) (stop=%i) %t " nonimpl stop th; - match Unsafe.kind th with - | App f args => - let newstop:int := Int.sub stop 1 in - printf "...Arrays.sub args %i %i: " (Int.sub (Array.length args) nonimpl) nonimpl; - Array.iter (fun e => printf "....%t" e) args; - let nonimplicitsargs := Array.sub args (Int.sub (Array.length args) nonimpl) nonimpl in - let nme_array := - Array.map (fun arg => (*Control.plus*) ((*fun () => *) fallback_rename_hyp newstop arg) (* (fun _ => [])*)) - nonimplicitsargs in - let l: string list := List.flatten (Array.to_list nme_array) in - let f' := Control.plus (fun() => Ident.to_string(box_name f)) (fun _ => "?1") in - f' :: (List.append l acc) - | _ => (let f':string := Control.plus (fun() => Ident.to_string(box_name th)) (fun _ => "?2") in - printf ". NO APP %s" f'; f' :: acc) -end -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:constr) : string list := - printf "## fallback_rename_hyp_quantif (stop=%i) %t " stop th; +Ltac2 rec rename_app (nonimpl:int) (stop:int) (acc:string list ref) th: unit := + Control.plus (fun () => let s := box_name th in + Ref.set acc (s:: Ref.get acc)) + (fun _ => + printf "## rename_app (nonimpl=%i) (stop=%i) %t " nonimpl stop th; + 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 _ := msgs "ICI DEP 20" in + 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 newstop acc subth' in + (in_context nme typ tac_under_binder); + () + else + let _ := msgs "ICI DEP 20" in + rename_hyp_chained_quantifs stop acc subth + | _ => fallback_rename_hyp stop acc th + end + +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 => + msgs "ICI 12"; if is_dep_prod th then - let sufx:ident := Option.default (Option.get (Ident.of_string "_h")) (Constr.Binder.name bnd) in - let remain := fallback_rename_hyp newstop subth in - forall_prefix() :: Ident.to_string sufx :: remain + let _ := msgs "ICI 13" in + 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 - let sufx := fallback_rename_hyp 1 (Constr.Binder.type bnd) in - let remain := fallback_rename_hyp newstop subth in - impl_prefix() :: (List.append sufx remain) + (Ref.set acc (impl_prefix() :: Ref.get acc); + (* fallback_rename_hyp 1 acc (Constr.Binder.type bnd); *) + rename_hyp_chained_quantifs newstop acc subth) | _ => backtrack "no product" end -with fallback_rename_hyp_specials stop th :string list := + +with fallback_rename_hyp_specials stop (acc:string list ref) th :unit := printf "## fallback_rename_hyp_specials (stop=%i) %t " stop th; let newstop := Int.sub stop 1 in Control.plus (* First see if user has something that applies *) - (fun() => rename_hyp newstop th) + (fun() => let dirs := rename_hyp newstop th in + interp_directives acc (List.rev dirs) ) (* if it fails try default specials *) - (fun _ => rename_hyp_default newstop th) + (fun _ => let dirs := rename_hyp_default newstop th in + interp_directives acc (List.rev dirs)) -with fallback_rename_hyp stop th:string list := - printf "## fallback_rename_hyp (stop=%i) %t " stop th; - if Int.le stop 0 then [] +with fallback_rename_hyp stop (acc:string list ref) th:unit := + printf "## fallback_rename_hyp (stop=%i) %t (acc = %a) " stop th (pr_list pr_string) (Ref.get acc); + if Int.le stop 0 then () else - Control.plus (fun () => fallback_rename_hyp_specials stop th) + Control.plus (fun () => fallback_rename_hyp_specials stop acc th) (fun _ => match Unsafe.kind th with - | Prod _ _ => fallback_rename_hyp_quantif stop th - | _ => - printf "...before count_impl: %t" th; - let numnonimpl := count_impl th in - printf "..after count_impl: %i" numnonimpl; - printf "## FALLBACK 1 rename_app %i %i %t " numnonimpl stop th; - let res := rename_app numnonimpl stop [] th in - msgs "..FALLBACK 2"; - res - end). + | Prod _ _ => 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 acc ld:unit := + List.fold_right (fun d _ => interp_directive acc d) ld () + +with interp_directive acc d := + match d with + | String s => Ref.set acc (s :: (Ref.get acc)) + | RecRename n t => fallback_rename_hyp n acc t + end. +Ltac2 rename_acc n th := + let acc := Ref.ref [] in + (* Here we intentionally create a separate goal to discard all side + effect (renames) ont he current goal. The constr actually returned by in_context does not matter. *) + let _ := in_context (Option.get (Ident.of_string "DUMMY_SUBGOAL")) constr:(Prop) (fun () => fallback_rename_hyp n acc th) in + Ref.get acc. - Unset Printing Notations. +Ltac2 fallback_rename_hyp_name th: ident := + let depth := rename_depth in + msgs "ICI 1"; + let l := rename_acc depth th in + msgs "ICI10"; + match l with + [] => backtrack "No name built" + | _ => (printf "FINAL acc = %a" (pr_list pr_string) l; + let nme := String.app "h_" (build_name l) in + let id := Option.get (Ident.of_string nme) in + Fresh.in_goal id) + end. + +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). *) +Ltac2 autorename_strict (h:ident) := + let th := Constr.type (Control.hyp h) in + printf "th = %t" th ; + let tth := Constr.type th in + printf "th = %t" tth ; + match! tth 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.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 + Std.rename [(dummy_name,newname)] + | Prop => + let msg := fprintf "no renaming pattern for %I : %t" h th in + backtrack (Message.to_string msg) + (* | _ => () (* not in Prop or "no renaming pattern for " $h *) *) + end. + +(* Tactic renaming hypothesis H. *) + +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. + + +Tactic Notation "autorename" hyp(h) := + let tac := ltac2:(h |- ltac1_autorename h) in + tac h. + +Ltac2 decr (n:int):int := + if Int.equal n 0 then 0 else Int.sub n 1. + +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)). + + + +(* Ltac2 Notation x(constr) "#" y(tactic(1)) := (RecRename x y). *) + + +Ltac2 Set rename_hyp_default := + fun n th: rename_directives => + if Int.lt n 0 then [] + else + match! th with + | ?x <> ?y => [String "neq"; RecRename (decr n) x; RecRename (decr n) y] + | @cons _ ?x (cons ?y ?l) => [String "cons"; RecRename n x; RecRename n y; RecRename (decr (decr n)) l] + | @cons _ ?x ?l => if Int.ge n 1 then [String "cons"; RecRename n x; RecRename (decr n) l] else [String "cons"] + | (@Some _ ?x) => [RecRename (Int.add 1 n) x] + | (@None _) => [String "None"] + end. + +Definition DUMMY: Prop -> Prop. + exact (fun x:Prop => x). +Qed. + +Ltac2 recRename n x := + RecRename (Option.get (Ltac1.to_int n)) (Option.get (Ltac1.to_constr x)). + + +(* ********** CUSTOMIZATION ********** *) + +(** 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. *) + + + +(* 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_names := true. + +(* From there this is LibHypTest from 1f7a1ed2289e439c291fcbd06c51705547feef1e *) +Ltac2 rename_hyp_2 n th := + match! th with + | true <> false => [String "tNEQf"] + | true = false => [String "tEQf"] + 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" ; RecRename n x ; RecRename n y] + | true = Nat.eqb ?x ?y => [String "Neqb" ; RecRename n x ; RecRename n y] + | _ => rename_hyp_2 n th (* call the previously defined tactic *) + end. + +Ltac2 Set rename_hyp := rename_hyp_3. + +Ltac2 Set rename_depth := 3. + +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 -> + (0 = 1)%Z -> + ~x = y -> + true = Nat.eqb 3 4 -> + Nat.eqb 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. + + intros;{(fun h => autorename h)}. + + 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_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_3n_4n0 with (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_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 [] => 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)). *) @@ -498,58 +777,99 @@ Parameters X Y: nat -> Prop. Parameters PX: X 3. Parameters PY: Y 3. -Goal forall [A : Type] (P Q : A -> Prop) (x : A), P x -> Q x -> (exists2 x : A, P x & Q x) -> False. - intros A P Q x H H0 H1. - ltac2:(let l := fallback_rename_hyp 9 constr:(exists2 x0 : A, P x0 & Q x0) in +Goal forall [A : Type] (P Q : A -> Prop) (x : A), P x -> Q x -> (exists2 x : A, P x & Q x) -> ex2 P Q -> False. + + intros A P Q x H H0 H1 H2. + + autorename H1. + autorename H2. + autorename H. + autorename H0. + assert (HH: (fun x => x = x) 1). + 2:{ autorename HH. + + + ltac2:(let l := rename_acc 3 constr:(exists2 x0 : A, P x0 & Q x0) in + printf "BEFORE BUILDNAME %a " (pr_list pr_string) l; + let nme := build_name l in + printf "%s" nme). + + ltac2:(let l := rename_acc 9 constr:(ex2 P Q) in printf "BEFORE BUILDNAME %a " (pr_list pr_string) l; let nme := build_name l in printf "%s" nme). Abort. -Goal forall n m p : nat, n m<= p -> True. +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 H H0. + 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 := fallback_rename_hyp 9 constr:(Nat.clearbit n m = p) in + + + + 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 := fallback_rename_hyp 3 constr:(Nat.clearbit 3 4%nat = 0) in + 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 := fallback_rename_hyp 4 constr:(Nat.clearbit 3 4%nat = 0 -> Nat.clearbit 3 4%nat = 7) in + 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 := fallback_rename_hyp 4 constr:(forall x:nat, Nat.clearbit x 4%nat = 0) in + 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 := fallback_rename_hyp 4 constr:(forall x:Z, BinIntDef.Z.quot x x = 1%Z) in + 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 := fallback_rename_hyp 4 constr:(Nat.clearbit 3%nat 4%nat) in + 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 := fallback_rename_hyp 4 constr:(Nat.clearbit 3%nat 4%nat) in - printf "%a" (pr_list (fun () s => fprintf "%s" s)) l). - ltac2:(let nme := rename_app 1 2 [] constr:(Nat.clearbit 3%nat 4%nat) in - printf "%s" (List.hd 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. + + +*) + (** This is the customizable naming tactic that the user should From b52cc00cff3b7c90e3643b2933c20441373bec09 Mon Sep 17 00:00:00 2001 From: Pierre Courtieu Date: Sat, 25 Oct 2025 23:04:38 +0200 Subject: [PATCH 05/10] Forward compatibility of autorename. WIP. --- LibHyps/LibHypsNaming.v | 63 ++++++++++++++++++++++------------------- 1 file changed, 34 insertions(+), 29 deletions(-) diff --git a/LibHyps/LibHypsNaming.v b/LibHyps/LibHypsNaming.v index 543bd73..d734410 100644 --- a/LibHyps/LibHypsNaming.v +++ b/LibHyps/LibHypsNaming.v @@ -440,7 +440,6 @@ Ltac2 rec rename_app (nonimpl:int) (stop:int) (acc:string list ref) th: unit := Control.plus (fun () => let s := box_name th in Ref.set acc (s:: Ref.get acc)) (fun _ => - printf "## rename_app (nonimpl=%i) (stop=%i) %t " nonimpl stop th; match Unsafe.kind th with | App f args => (* control_try? *) @@ -461,7 +460,6 @@ with rename_hyp_chained_quantifs stop (acc:string list ref) (th:constr) : unit : | Prod bnd subth => if is_dep_prod th then - let _ := msgs "ICI DEP 20" in 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 @@ -469,16 +467,15 @@ with rename_hyp_chained_quantifs stop (acc:string list ref) (th:constr) : unit : 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); + (* 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 newstop acc subth' in + rename_hyp_chained_quantifs stop acc subth' in (in_context nme typ tac_under_binder); () else - let _ := msgs "ICI DEP 20" in rename_hyp_chained_quantifs stop acc subth | _ => fallback_rename_hyp stop acc th end @@ -487,10 +484,8 @@ 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 => - msgs "ICI 12"; if is_dep_prod th then - let _ := msgs "ICI 13" in 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 @@ -498,7 +493,7 @@ with fallback_rename_hyp_quantif stop (acc:string list ref) (th:constr) : unit : 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); + 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 @@ -509,14 +504,26 @@ with fallback_rename_hyp_quantif stop (acc:string list ref) (th:constr) : unit : else (Ref.set acc (impl_prefix() :: Ref.get acc); - (* fallback_rename_hyp 1 acc (Constr.Binder.type bnd); *) rename_hyp_chained_quantifs newstop acc subth) - | _ => backtrack "no product" + | App f args => + match Unsafe.kind f, Unsafe.kind constr:(@Init.Logic.ex) with + | Ind ind _, Ind ind' _ => + if Ind.equal ind ind' + then ( + msgs "EXXXX"; + 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 + | _ => backtrack "no quantif" end with fallback_rename_hyp_specials stop (acc:string list ref) th :unit := - printf "## fallback_rename_hyp_specials (stop=%i) %t " stop th; let newstop := Int.sub stop 1 in Control.plus (* First see if user has something that applies *) @@ -527,16 +534,16 @@ with fallback_rename_hyp_specials stop (acc:string list ref) th :unit := interp_directives acc (List.rev dirs)) with fallback_rename_hyp stop (acc:string list ref) th:unit := - printf "## fallback_rename_hyp (stop=%i) %t (acc = %a) " stop th (pr_list pr_string) (Ref.get acc); if Int.le stop 0 then () else Control.plus (fun () => fallback_rename_hyp_specials stop acc th) - (fun _ => match Unsafe.kind th with - | Prod _ _ => fallback_rename_hyp_quantif stop acc th - | _ => let numnonimpl := count_impl th in - let _ := rename_app numnonimpl stop acc th in - () - end) + (fun _ => 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 acc ld:unit := List.fold_right (fun d _ => interp_directive acc d) ld () @@ -573,7 +580,6 @@ Ltac2 rename_hyp_with_name h th := fail. renaming can be computed. Example of failing type: H:((fun x => True) true). *) Ltac2 autorename_strict (h:ident) := let th := Constr.type (Control.hyp h) in - printf "th = %t" th ; let tth := Constr.type th in printf "th = %t" tth ; match! tth with @@ -717,7 +723,6 @@ Lemma dummy: forall x y, (forall w w',w < w' -> ~(true=false)) -> (0 < 1 -> ~(1<0)) -> (0 < 1 -> 1<0) -> 0 < z -> True. - intros;{(fun h => autorename h)}. match type of x with nat => idtac | _ => fail "test failed!" end. @@ -735,23 +740,23 @@ Lemma dummy: forall x y, 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_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_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_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 [] => 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. From 01e56486555fe19e8523589d2a96fbd956d08e1a Mon Sep 17 00:00:00 2001 From: Pierre Courtieu Date: Sun, 26 Oct 2025 12:24:30 +0100 Subject: [PATCH 06/10] Cleaning backtracking in libhypsnaming. --- LibHyps/LibHypsDebug.v | 2 ++ LibHyps/LibHypsNaming.v | 77 +++++++++++++++++++++++++++-------------- 2 files changed, 53 insertions(+), 26 deletions(-) diff --git a/LibHyps/LibHypsDebug.v b/LibHyps/LibHypsDebug.v index c7b2a7c..490c2d5 100644 --- a/LibHyps/LibHypsDebug.v +++ b/LibHyps/LibHypsDebug.v @@ -54,3 +54,5 @@ Ltac2 pr_goal() := 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 d734410..7234ed9 100644 --- a/LibHyps/LibHypsNaming.v +++ b/LibHyps/LibHypsNaming.v @@ -66,6 +66,13 @@ Ltac2 build_name_gen (sep:string) (suffx:bool) (l:string list) := Ltac2 build_name l := build_name_gen "_" add_suffix (List.rev l). Ltac2 build_name_no_suffix l := build_name_gen "_" false (List.rev l). + +Ltac2 pr_directive () (d:rename_directive) := + match d with + String s => fprintf "%s" s + | RecRename i c => fprintf "(%i,%t)" i c + end. + (* 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_. @@ -395,7 +402,7 @@ Ltac2 box_name t : string := Ident.to_string id | Unsafe.Var id => Ident.to_string id | Unsafe.Ind _ _ => - printf "IND: %t" t; + (* 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) @@ -403,9 +410,9 @@ Ltac2 box_name t : string := s | _ => if is_closed t then - printf ". BEFORE NUM %t" t; + (* printf ". BEFORE NUM %t" t; *) let s := add_numerical_names () t in - printf ". AFTER NUM %t -> %s" t s; + (* printf ". AFTER NUM %t -> %s" t s; *) s else backtrack "cannot be a number" end @@ -426,8 +433,6 @@ Local Ltac2 is_dep_prod (t:constr): bool := | _ => false end. - - Ltac2 is_hyp (id:ident) := let hyps := Control.hyps () in List.exist (fun (x,_,_) => Ident.equal id x) hyps. @@ -437,7 +442,7 @@ Ltac2 is_hyp (id:ident) := recursively or simply. Parameters at positions below nonimpl are considered implicit and not considered. *) Ltac2 rec rename_app (nonimpl:int) (stop:int) (acc:string list ref) th: unit := - Control.plus (fun () => let s := box_name th in + Control.once_plus (fun () => let s := box_name th in Ref.set acc (s:: Ref.get acc)) (fun _ => match Unsafe.kind th with @@ -510,7 +515,6 @@ with fallback_rename_hyp_quantif stop (acc:string list ref) (th:constr) : unit : | Ind ind _, Ind ind' _ => if Ind.equal ind ind' then ( - msgs "EXXXX"; 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 @@ -524,31 +528,47 @@ with fallback_rename_hyp_quantif stop (acc:string list ref) (th:constr) : unit : with fallback_rename_hyp_specials stop (acc:string list ref) th :unit := + (* printf "hyp_specials = %a ; th : %t" pr_acc (Ref.get acc) th; *) let newstop := Int.sub stop 1 in - Control.plus + 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 acc (List.rev dirs) ) (* if it fails try default specials *) (fun _ => let dirs := rename_hyp_default newstop th in - interp_directives acc (List.rev dirs)) + (* msgs "C'est LA"; *) + (* printf "acc = %a" pr_acc (Ref.get acc); *) + (* printf "dirs = %a" (pr_list pr_directive) dirs; *) + Ref.set acc freeze; (* backtracking acc by hand here *) + interp_directives acc (List.rev dirs) + (* printf "acc AFTER = %a" pr_acc (Ref.get acc) *) + + ) with fallback_rename_hyp stop (acc:string list ref) th:unit := + (* printf "rename hyp %a ; th : %t" pr_acc (Ref.get acc) th; *) if Int.le stop 0 then () else - Control.plus (fun () => fallback_rename_hyp_specials stop acc th) - (fun _ => 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) + Control.once_plus (fun () => + fallback_rename_hyp_specials stop acc th + (* printf "rename_hyp 1 %a : %t" pr_acc (Ref.get acc) th *) + ) + (fun _ => + (* printf "special failed %a : %t" pr_acc (Ref.get acc) th; *) + 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 acc ld:unit := List.fold_right (fun d _ => interp_directive acc d) ld () with interp_directive 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)) | RecRename n t => fallback_rename_hyp n acc t @@ -556,19 +576,22 @@ with interp_directive acc d := Ltac2 rename_acc n th := let acc := Ref.ref [] in - (* Here we intentionally create a separate goal to discard all side - effect (renames) ont he current goal. The constr actually returned by in_context does not matter. *) - let _ := in_context (Option.get (Ident.of_string "DUMMY_SUBGOAL")) constr:(Prop) (fun () => fallback_rename_hyp n acc th) in - Ref.get acc. + (* Here we intentionally create a separate goal to discard all side effect + (renames) ont he current goal. The constr actually returned by in_context + does not matter. We also backtrack at the end to forget about this + separate goal. *) + let dummy_nme := Option.get (Ident.of_string "DUMMY_SUBGOAL") in + Control.once_plus (fun () => in_context dummy_nme constr:(Prop) (fun () => fallback_rename_hyp n acc th) ; + backtrack "Forgetting about the dummy subgoal") + (fun _ => Ref.get acc). Ltac2 fallback_rename_hyp_name th: ident := let depth := rename_depth in - msgs "ICI 1"; let l := rename_acc depth th in - msgs "ICI10"; + (* printf "ICI10 : %a" pr_acc l; *) match l with [] => backtrack "No name built" - | _ => (printf "FINAL acc = %a" (pr_list pr_string) l; + | _ => ( (*printf "FINAL acc = %a" (pr_list pr_string) l;*) let nme := String.app "h_" (build_name l) in let id := Option.get (Ident.of_string nme) in Fresh.in_goal id) @@ -581,7 +604,7 @@ renaming can be computed. Example of failing type: H:((fun x => True) true). *) Ltac2 autorename_strict (h:ident) := let th := Constr.type (Control.hyp h) in let tth := Constr.type th in - printf "th = %t" tth ; + (* printf "th = %t" tth ; *) match! tth with (* | _ => *) (* let l := rename_hyp_with_name $h th in *) @@ -630,7 +653,7 @@ Ltac2 Set rename_hyp_default := fun n th: rename_directives => if Int.lt n 0 then [] else - match! th with + lazy_match! th with | ?x <> ?y => [String "neq"; RecRename (decr n) x; RecRename (decr n) y] | @cons _ ?x (cons ?y ?l) => [String "cons"; RecRename n x; RecRename n y; RecRename (decr (decr n)) l] | @cons _ ?x ?l => if Int.ge n 1 then [String "cons"; RecRename n x; RecRename (decr n) l] else [String "cons"] @@ -723,6 +746,8 @@ Lemma dummy: forall x y, (forall w w',w < w' -> ~(true=false)) -> (0 < 1 -> ~(1<0)) -> (0 < 1 -> 1<0) -> 0 < z -> True. + + intros;{(fun h => autorename h)}. match type of x with nat => idtac | _ => fail "test failed!" end. From ad12e212117e6d86ec4d9ae919b81ab101762344 Mon Sep 17 00:00:00 2001 From: Pierre Courtieu Date: Sun, 26 Oct 2025 20:23:22 +0100 Subject: [PATCH 07/10] Cleaning LibHypsNaming. --- LibHyps/LibHypsNaming.v | 832 +++++----------------------------------- 1 file changed, 91 insertions(+), 741 deletions(-) diff --git a/LibHyps/LibHypsNaming.v b/LibHyps/LibHypsNaming.v index 7234ed9..331fe52 100644 --- a/LibHyps/LibHypsNaming.v +++ b/LibHyps/LibHypsNaming.v @@ -1,10 +1,17 @@ (* 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. *) +(* **************************************************************** *) + +(** This file defines a tactic "autorename h" (and "autorename_strict + 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 TacNewHyps.Notations. + (* Import ListNotations. *) (* Local Open Scope list. *) Require Import Ltac2.Ltac2. @@ -15,74 +22,81 @@ 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 _ => ()). -(** This file defines a tactic "autorename h" (and "autorename_strict - h") that automatically rename hypothesis h followinh a systematic, - but customizable heuristic. - - Comments welcome. *) (* 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 - - 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. - - Typical use, in increasing order of complexity, approximatively - equivalent to the decreasing order of interest. - -<< -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) - end. ->> -(* Overwrite the definition of rename_hyp using the ::= operator. :*) - -<< -Ltac rename_hyp ::= my_rename_hyp. ->> *) - Ltac2 Type rename_directive := [ String(string) | RecRename(int,constr) ]. Ltac2 Type rename_directives := rename_directive list. +(* For debugging *) +Ltac2 pr_directive () (d:rename_directive) := + match d with + String s => fprintf "%s" s + | RecRename i c => fprintf "(%i,%t)" i c + end. + Ltac2 Type hypnames := string list. + +(* The pretty printing of numerical values is by default 1, 2... Set this to + true (Ltac2 Set numerical_names := 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. -(* Elements of l are supposed to already start with "_" *) -Ltac2 build_name_gen (sep:string) (suffx:bool) (l:string list) := - String.app (String.concat sep l) (if suffx then "_" else ""). +(** Default prefix for hypothesis names. *) +Ltac2 default_prefix():string := "h". -Ltac2 build_name l := build_name_gen "_" add_suffix (List.rev l). -Ltac2 build_name_no_suffix l := build_name_gen "_" false (List.rev l). +(** A few special default chunks, for special cases in the naming heuristic. *) +Ltac2 impl_prefix() := "impl". +Ltac2 forall_prefix() := "all". +Ltac2 exists_prefix() := "ex". +(** ** 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". -Ltac2 pr_directive () (d:rename_directive) := - match d with - String s => fprintf "%s" s - | RecRename i c => fprintf "(%i,%t)" i c +(* 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. +>> *) + +(* This one is similar but for internal use *) +Ltac2 mutable rename_hyp_default (n:int) (th:constr): rename_directives := backtrack "rename_hyp_default". -(* 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_. - 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 *) +(* 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 "")). -Ltac2 Type numerical_names_style := bool. -Ltac2 mutable numerical_names := false. +Ltac2 build_name (l:string list): string := build_name_gen "_" add_prefix add_suffix (List.rev l). Ltac2 string_of_int (i:int) := Message.to_string (Message.of_int i). @@ -93,19 +107,9 @@ Ltac2 string_of_int (i:int) := Message.to_string (Message.of_int i). 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 *) -Ltac2 num_nosufx (i:int) := - msgs ". num_nosufx"; - printf ". i = %s" (string_of_int i); - let res := String.app "_" (string_of_int i) in - printf ". res = %s" res; - msgs ". num_nosufx: end"; - res. -(* Ltac2 num_sufx (i:int) (sfx:string) := (String.app (string_of_int i) sfx). *) - (* TODO: find a way to make a string from nat, Z and N *) Ltac2 numerical_names_nosufx (t:constr):string := - printf "...NUM: %t" t; if is_closed t then match! t with | 0%Z => "0" @@ -186,7 +190,7 @@ Ltac2 numerical_names_sufx t := (* Redefine at will *) Ltac2 add_numerical_names (): constr -> string:= - if numerical_names then numerical_names_sufx else numerical_names_nosufx. + if numerical_sufx then numerical_names_sufx else numerical_names_nosufx. (** This determines the depth of the recursive analysis of a type to @@ -195,22 +199,9 @@ Ltac2 add_numerical_names (): constr -> string:= too often. *) Ltac2 mutable rename_depth := 3. -(** Default prefix for hypothesis names. *) -Ltac2 default_prefix():string := "h". -(** A few special default chunks, for special cases in the naming heuristic. *) -Ltac2 impl_prefix() := "impl". -Ltac2 forall_prefix() := "all". -Ltac2 exists_prefix() := "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 mutable rename_hyp (stop:int) (th:constr): rename_directives := backtrack "rename_hyp". -Ltac2 mutable rename_hyp_default (n:int) (th:constr): rename_directives := backtrack "rename_hyp_default". - (* TODO: 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 @@ -327,68 +318,13 @@ Ltac2 count_impl th := -Ltac2 percent():char := (Char.of_int 37). Ltac2 arobase():char := (Char.of_int 64). -Ltac2 space():char := (Char.of_int 32). -Ltac2 parg():char := (Char.of_int 40). -Ltac2 pard():char := (Char.of_int 41). - -(* Ltac2 Eval (Char.to_int (String.get ")" 0)). *) - -Ltac2 set_forbidden_chars (): char list := [space();pard();parg()]. -Ltac2 set_removable_chars (): char list := [percent();arobase()]. -Ltac2 set_suspect_chars (): char list := List.append (set_forbidden_chars()) (set_removable_chars()). -Ltac2 set_forbidden_charints (): int list := List.map Char.to_int (set_forbidden_chars()). -Ltac2 set_removable_charints (): int list := List.map Char.to_int (set_removable_chars()). -Ltac2 set_suspect_charints (): int list := List.map Char.to_int (set_suspect_chars()). - -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. - -Ltac2 string_count_if (p:char -> bool) (s:string) : int := - let lgth := String.length s in - let rec count acc i := - if Int.ge i lgth then acc - else if p (String.get s i) then count (Int.add 1 acc) (Int.add 1 i) - else count acc (Int.add 1 i) - in - count 0 0. - -Ltac2 string_remove (p:char -> bool) (s:string) : string := - let lgth := String.length s in - let nbgood := string_count_if (fun c => Bool.neg (p c)) s in - let res := String.make nbgood (arobase()) in - let rec fill k i: unit := - if Int.ge i lgth then () - else - let c := String.get s i in - if p c then fill k (Int.add 1 i) - else (String.set res k c; fill (Int.add 1 k) (Int.add 1 i)) in - fill 0 0; - res. - -Ltac2 forbidden_charint (c:char):bool := (List.mem Int.equal (Char.to_int c) (set_forbidden_charints())). -Ltac2 removeable_charint (c:char):bool := (List.mem Int.equal (Char.to_int c) (set_removable_charints())). -Ltac2 suspect_charint (c:char):bool := (List.mem Int.equal (Char.to_int c) (set_suspect_charints())). - -Ltac2 Eval (string_remove (fun c => (Char.equal c (arobase()))) "az@er% % @o"). -Ltac2 Eval (string_remove forbidden_charint "az@er% % @o"). -Ltac2 Eval (string_remove suspect_charint "az@er% % @o"). - - -(* Ltac2 print_id (t:constr) : string option := *) -(* let (idopt,_) := Fresh.next (Fresh.Free.empty) t in *) -(* Some (Ident.to_string idopt). *) - (** Build a chunk from a simple term: either a number or a freshable term. *) 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) @@ -408,25 +344,10 @@ Ltac2 box_name t : string := then String.sub s 1 (Int.sub (String.length s) 1) else s in s - | _ => - if is_closed t then - (* printf ". BEFORE NUM %t" t; *) - let s := add_numerical_names () t in - (* printf ". AFTER NUM %t -> %s" t s; *) - s - else backtrack "cannot be a number" + | _ => add_numerical_names () t end end. -(* Ltac2 id_of_constr (t:constr) : string option := *) -(* let s:string := Message.to_string (fprintf "%t" t) in *) -(* if string_forall (fun c => Bool.neg (forbidden_charint c)) s *) -(* then *) -(* let s := string_remove removeable_charint s in *) -(* if string_forall (fun c => Bool.neg (Char.equal (space()) c)) s then Some s else None *) -(* else None. *) - - Local Ltac2 is_dep_prod (t:constr): bool := match kind t with | Prod _ subt => Bool.neg (is_closed subt) @@ -528,7 +449,6 @@ with fallback_rename_hyp_quantif stop (acc:string list ref) (th:constr) : unit : with fallback_rename_hyp_specials stop (acc:string list ref) th :unit := - (* printf "hyp_specials = %a ; th : %t" pr_acc (Ref.get acc) th; *) let newstop := Int.sub stop 1 in let freeze := Ref.get acc in Control.once_plus @@ -537,25 +457,14 @@ with fallback_rename_hyp_specials stop (acc:string list ref) th :unit := interp_directives acc (List.rev dirs) ) (* if it fails try default specials *) (fun _ => let dirs := rename_hyp_default newstop th in - (* msgs "C'est LA"; *) - (* printf "acc = %a" pr_acc (Ref.get acc); *) - (* printf "dirs = %a" (pr_list pr_directive) dirs; *) Ref.set acc freeze; (* backtracking acc by hand here *) - interp_directives acc (List.rev dirs) - (* printf "acc AFTER = %a" pr_acc (Ref.get acc) *) - - ) + interp_directives acc (List.rev dirs)) with fallback_rename_hyp stop (acc:string list ref) th:unit := - (* printf "rename hyp %a ; th : %t" pr_acc (Ref.get acc) th; *) if Int.le stop 0 then () else - Control.once_plus (fun () => - fallback_rename_hyp_specials stop acc th - (* printf "rename_hyp 1 %a : %t" pr_acc (Ref.get acc) th *) - ) + Control.once_plus (fun () => fallback_rename_hyp_specials stop acc th) (fun _ => - (* printf "special failed %a : %t" pr_acc (Ref.get acc) th; *) lazy_match! th with | forall _, _ => fallback_rename_hyp_quantif stop acc th | exists _, _ => fallback_rename_hyp_quantif stop acc th @@ -574,16 +483,20 @@ with interp_directive acc d := | RecRename n t => fallback_rename_hyp n acc t end. +(* 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 - (* Here we intentionally create a separate goal to discard all side effect - (renames) ont he current goal. The constr actually returned by in_context - does not matter. We also backtrack at the end to forget about this - separate goal. *) + (* 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 - Control.once_plus (fun () => in_context dummy_nme constr:(Prop) (fun () => fallback_rename_hyp n acc th) ; - backtrack "Forgetting about the dummy subgoal") - (fun _ => Ref.get acc). + 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 @@ -591,12 +504,14 @@ Ltac2 fallback_rename_hyp_name th: ident := (* printf "ICI10 : %a" pr_acc l; *) match l with [] => backtrack "No name built" - | _ => ( (*printf "FINAL acc = %a" (pr_list pr_string) l;*) - let nme := String.app "h_" (build_name l) in + | _ => let nme := build_name l in let id := Option.get (Ident.of_string nme) in - Fresh.in_goal id) + Fresh.in_goal id end. +(* 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 @@ -606,6 +521,7 @@ Ltac2 autorename_strict (h:ident) := let tth := Constr.type th in (* printf "th = %t" tth ; *) match! tth with + (* TODO: the deep entry point *) (* | _ => *) (* let l := rename_hyp_with_name $h th in *) (* let dummy_name := fresh "dummy" in *) @@ -685,7 +601,7 @@ Ltac2 recRename n x := (* 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_names := true. +Ltac2 Set numerical_sufx := true. (* From there this is LibHypTest from 1f7a1ed2289e439c291fcbd06c51705547feef1e *) Ltac2 rename_hyp_2 n th := @@ -707,7 +623,7 @@ Ltac2 rename_hyp_3 n th := 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, @@ -817,7 +733,7 @@ Goal forall [A : Type] (P Q : A -> Prop) (x : A), P x -> Q x -> (exists2 x : A, autorename H. autorename H0. assert (HH: (fun x => x = x) 1). - 2:{ autorename HH. + 2:{ autorename HH. } ltac2:(let l := rename_acc 3 constr:(exists2 x0 : A, P x0 & Q x0) in @@ -838,7 +754,7 @@ Proof. intros n m p b H H0. assert (forall z, foo b z). - 2:{ + 2:{ } ltac2:(let l := rename_acc 4 constr:(forall b:nat, Nat.clearbit b 4%nat = 0) in printf "BEFORE BUILDNAME"; @@ -900,572 +816,6 @@ Abort. *) - - -(** 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. *) -Ltac rename_hyp stop th := fail. -(** This will later contain a few default fallback naming strategy. *) -Ltac rename_hyp_default stop th := - fail. - -(** 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. - - -Ltac build_name l := build_name_gen add_suffix l. -Ltac build_name_no_suffix l := build_name_gen constr:(false) l. - - - -(** * 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: - - [(∀ h,DUMMY h) ; (∀ _eq,DUMMY _eq) ; (∀ _foo, DUMMY _foo)] - - where DUMMY is an opaque (identity) function but we don't care. *) - - -(** We define DUMMY as an opaque symbol. *) -Definition DUMMY: Prop -> Prop. - exact (fun x:Prop => x). -Qed. - -(* ********** CUSTOMIZATION ********** *) - -(** 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). - -(* 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_. - - 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. - -(** 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). - -(** 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. *) - - Ltac rename_hyp stop th := fail. - -(* ************************************** *) - - -(** 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. - -Ltac build_name l := build_name_gen add_suffix l. -Ltac build_name_no_suffix l := build_name_gen constr:(false) l. - - -(** 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 - *replace* the digit in case of name clash. If you are bitten by - 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" - 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) :: [])). - -(** 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 - 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) - end. - - -(** 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 - 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)) - end - | _ => fallback_rename_hyp stop th - 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 - end. - -Local Close Scope autonaming_scope. - -(* Entry point of the renaming code. *) -Ltac fallback_rename_hyp_name th := - 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 - match l with - nil => fail 1 - | _ => let nme := build_name (h::l) in - fresh nme - 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. - - -(* 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 *) - 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 - end. - -(* Tactic renaming hypothesis H. *) - -Ltac autorename $h := try autorename_strict H. - (* (* Tests *) Print Visibility. From 15286724c60d6db1f569a14641373a2a2b9195dd Mon Sep 17 00:00:00 2001 From: Pierre Courtieu Date: Sun, 26 Oct 2025 22:30:03 +0100 Subject: [PATCH 08/10] Re-implementing renaming tacticals. --- LibHyps/LibHypsNaming.v | 185 +++++++++++++++++----------------------- 1 file changed, 76 insertions(+), 109 deletions(-) diff --git a/LibHyps/LibHypsNaming.v b/LibHyps/LibHypsNaming.v index 331fe52..1edcf81 100644 --- a/LibHyps/LibHypsNaming.v +++ b/LibHyps/LibHypsNaming.v @@ -39,8 +39,13 @@ Ltac2 pr_directive () (d:rename_directive) := 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_names := true) to have 1z, 1n or 1N depending of the type nat, Z or N. *) + 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. @@ -100,109 +105,67 @@ Ltac2 build_name (l:string list): string := build_name_gen "_" add_prefix add_su Ltac2 string_of_int (i:int) := Message.to_string (Message.of_int i). -(** Generate fresh name for numerical constants. - Warning: problem here: hyps names may end with a digit: Coq may - *replace* the digit in case of name clash. If you are bitten by - 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 *) -(* TODO: find a way to make a string from nat, Z and N *) -Ltac2 numerical_names_nosufx (t:constr):string := - if is_closed t then - match! t with - | 0%Z => "0" - | 1%Z => "1" - | 2%Z => "2" - | 3%Z => "3" - | 4%Z => "4" - | 5%Z => "5" - | 6%Z => "6" - | 7%Z => "7" - | 8%Z => "8" - | 9%Z => "9" - | 10%Z => "10" - | O%nat => "0" - | 1%nat => "1" - | 2%nat => "2" - | 3%nat => "3" - | 4%nat => "4" - | 5%nat => "5" - | 6%nat => "6" - | 7%nat => "7" - | 8%nat => "8" - | 9%nat => "9" - | 10%nat => "10" - | O%N => "0" - | 1%N => "1" - | 2%N => "2" - | 3%N => "3" - | 4%N => "4" - | 5%N => "5" - | 6%N => "6" - | 7%N => "7" - | 8%N => "8" - | 9%N => "9" - | 10%N => "10" - | _ => backtrack "not recognized as a number " - end - else - backtrack "not a nameable number". - -Ltac2 numerical_names_sufx t := - match! t with - | 0%Z => "0z" - | 1%Z => "1z" - | 2%Z => "2z" - | 3%Z => "3z" - | 4%Z => "4z" - | 5%Z => "5z" - | 6%Z => "6z" - | 7%Z => "7z" - | 8%Z => "8z" - | 9%Z => "9z" - | 10%Z => "10z" - (* | Z0 => num_sufx 0 *) - | O%nat => "0n" - | 1%nat => "1n" - | 2%nat => "2n" - | 3%nat => "3n" - | 4%nat => "4n" - | 5%nat => "5n" - | 6%nat => "6n" - | 7%nat => "7n" - | 8%nat => "8n" - | 9%nat => "9n" - | 10%nat => "10n" - | O%N => "0N" - | 1%N => "1N" - | 2%N => "2N" - | 3%N => "3N" - | 4%N => "4N" - | 5%N => "5N" - | 6%N => "6N" - | 7%N => "7N" - | 8%N => "8N" - | 9%N => "9N" - | 10%N => "10N" - end. +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. -(* Redefine at will *) -Ltac2 add_numerical_names (): constr -> string:= - if numerical_sufx then numerical_names_sufx else numerical_names_nosufx. +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). -(** 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. +Ltac2 is_digit (c:char): bool := + let code := Char.to_int c in + Bool.and (Int.le (code0()) code) (Int.le code (code9())). +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. +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. -(* TODO: find something better to detect implicits!! *) + +(** Generate fresh name for numerical constants. + + Warning: problem here: hyps names may end with a digit: Coq may + *replace* the digit in case of name clash. If you are bitten by + 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 *) + +(* 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 @@ -344,7 +307,7 @@ Ltac2 box_name t : string := then String.sub s 1 (Int.sub (String.length s) 1) else s in s - | _ => add_numerical_names () t + | _ => build_numerical_name t end end. @@ -516,11 +479,12 @@ 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). *) +#[global] Ltac2 autorename_strict (h:ident) := let th := Constr.type (Control.hyp h) in let tth := Constr.type th in (* printf "th = %t" tth ; *) - match! tth with + lazy_match! tth with (* TODO: the deep entry point *) (* | _ => *) (* let l := rename_hyp_with_name $h th in *) @@ -536,7 +500,11 @@ Ltac2 autorename_strict (h:ident) := | Prop => let msg := fprintf "no renaming pattern for %I : %t" h th in backtrack (Message.to_string msg) - (* | _ => () (* not in Prop or "no renaming pattern for " $h *) *) + | _ => + 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. *) @@ -548,11 +516,18 @@ Ltac2 ltac1_autorename (h:Ltac1.t) := let h: ident := Option.get (Ltac1.to_ident h) in ltac2_autorename h. +#[global]Ltac2 ltac1_autorename_strict (h:Ltac1.t) := + let h: ident := Option.get (Ltac1.to_ident h) in + autorename_strict h. Tactic Notation "autorename" hyp(h) := let tac := ltac2:(h |- ltac1_autorename h) in tac h. +Tactic Notation "autorename_strict" hyp(h) := + let tac := ltac2:(h |- ltac1_autorename_strict h) in + tac h. + Ltac2 decr (n:int):int := if Int.equal n 0 then 0 else Int.sub n 1. @@ -587,15 +562,6 @@ Ltac2 recRename n x := (* ********** CUSTOMIZATION ********** *) -(** 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. *) - - - (* TESTS *) (* This settings should reproduce the naming scheme of libhypps-1.0.0 @@ -633,6 +599,7 @@ Lemma dummy: forall x y, x = y -> Some x = Some y -> 0 = 1 -> + 223 = 426 -> (0 = 1)%Z -> ~x = y -> true = Nat.eqb 3 4 -> @@ -662,8 +629,7 @@ Lemma dummy: forall x y, (forall w w',w < w' -> ~(true=false)) -> (0 < 1 -> ~(1<0)) -> (0 < 1 -> 1<0) -> 0 < z -> True. - - +Proof. intros;{(fun h => autorename h)}. match type of x with nat => idtac | _ => fail "test failed!" end. @@ -672,6 +638,7 @@ Lemma dummy: forall x y, 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. From cfd87a77073a5a47a521ddc3f272730cdf756e34 Mon Sep 17 00:00:00 2001 From: Pierre Courtieu Date: Tue, 24 Mar 2026 10:15:58 +0100 Subject: [PATCH 09/10] Auto naming works ok. Needs cleaning. Now working on (ltac2) hyps grouping. --- LibHyps/LibHyps.v | 104 +++++++++++++-------- LibHyps/LibHypsNaming.v | 189 +++++++++++++++++++++++++++----------- LibHyps/LibHypsTactics.v | 81 ++-------------- configure.sh | 20 +++- tests/LibHypsRegression.v | 59 +++++++++++- tests/demo.v | 2 +- 6 files changed, 281 insertions(+), 174 deletions(-) diff --git a/LibHyps/LibHyps.v b/LibHyps/LibHyps.v index 25d96d6..3ba4768 100644 --- a/LibHyps/LibHyps.v +++ b/LibHyps/LibHyps.v @@ -5,10 +5,38 @@ Require Export LibHyps.TacNewHyps. Require Export LibHyps.LibHypsNaming. Require Export LibHyps.Especialize. -Require Export LibHyps.LibHypsTactics. +(* Require Export LibHyps.LibHypsTactics. *) (* We export ; { } etc. ";;" also. *) +Ltac rename_or_revert H := autorename_strict H + generalize 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,30 +55,33 @@ 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). +(* (* 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). (* usual combinations *) -Tactic Notation (at level 4) tactic4(Tac) "//" := (Tac /s/n/g). +(*Tactic Notation (at level 4) tactic4(Tac) "//" := (Tac /s/n/g). Tactic Notation (at level 4) tactic4(Tac) "/" "sng" := (Tac /s/n/g). -Tactic Notation (at level 4) tactic4(Tac) "/" "sgn" := (Tac /s/g/n). +Tactic Notation (at level 4) tactic4(Tac) "/" "sgn" := (Tac /s/g/n). *) Tactic Notation (at level 4) tactic4(Tac) "/" "sn" := (Tac /s/n). Tactic Notation (at level 4) tactic4(Tac) "/" "sr" := (Tac /s/r). -Tactic Notation (at level 4) tactic4(Tac) "/" "sg" := (Tac /s/g). +(*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) 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) ; group_up_list all_hyps). *) Module LegacyNotations. Import Notations. @@ -61,7 +92,7 @@ Module LegacyNotations. (* like !!tac + tries to subst with each new hypothesis. *) Tactic Notation "!!!" tactic3(Tac) := Tac/s/n?. (* Like !!! + regroup new Type-sorted hyps at top. *) - Tactic Notation (at level 4) "!!!!" tactic4(Tac) := Tac /s/n?/g. + (* Tactic Notation (at level 4) "!!!!" tactic4(Tac) := Tac /s/n?/g. *) (* Other Experimental combinations *) @@ -85,49 +116,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/LibHypsNaming.v b/LibHyps/LibHypsNaming.v index 1edcf81..f64ebff 100644 --- a/LibHyps/LibHypsNaming.v +++ b/LibHyps/LibHypsNaming.v @@ -27,16 +27,23 @@ Local Ltac2 control_try tac := Control.plus tac (fun _ => ()). ZArith to be loaded *) From Stdlib Require Import ZArith. -Ltac2 Type rename_directive := [ String(string) | RecRename(int,constr) ]. +Ltac2 decr (n:int):int := + if Int.equal n 0 then 0 else Int.sub n 1. + +Ltac2 incr (n:int):int := Int.add n 1. + +Ltac2 Type rename_directive := [ String(string) | Rename(constr) | RenameN(int,constr) ]. Ltac2 Type rename_directives := rename_directive list. (* For debugging *) +Module Debug. Ltac2 pr_directive () (d:rename_directive) := match d with String s => fprintf "%s" s - | RecRename i c => fprintf "(%i,%t)" i c + | Rename c => fprintf "%t" c + | RenameN i c => fprintf "N(%i,%t)" i c end. - +End Debug. Ltac2 Type hypnames := string list. (** This determines the depth of the recursive analysis of a type to @@ -68,6 +75,7 @@ Ltac2 exists_prefix() := "ex". default naming scheme to apply. *) Ltac2 mutable rename_hyp (stop:int) (th:constr): rename_directives := backtrack "rename_hyp". + (* Typical use, in increasing order of complexity, approximatively equivalent to the decreasing order of interest. *) (** @@ -95,6 +103,7 @@ Ltac2 Set rename_hyp := rename_hyp_3. (* This one is similar but for internal use *) Ltac2 mutable rename_hyp_default (n:int) (th:constr): rename_directives := backtrack "rename_hyp_default". +Module Ltac2. (* 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) := @@ -324,7 +333,7 @@ Ltac2 is_hyp (id:ident) := (** 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. *) + 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)) @@ -344,7 +353,7 @@ Ltac2 rec rename_app (nonimpl:int) (stop:int) (acc:string list ref) th: unit := 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 + let _newstop := Int.sub stop 1 in match Unsafe.kind th with | Prod bnd subth => if is_dep_prod th @@ -401,7 +410,7 @@ with fallback_rename_hyp_quantif stop (acc:string list ref) (th:constr) : unit : 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 + | Lambda _bnd subth => rename_hyp_chained_quantifs newstop acc subth | _ => backtrack "not exist" end) else backtrack "not exist" @@ -417,11 +426,11 @@ with fallback_rename_hyp_specials stop (acc:string list ref) th :unit := Control.once_plus (* First see if user has something that applies *) (fun() => let dirs := rename_hyp newstop th in - interp_directives acc (List.rev dirs) ) + 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 acc (List.rev dirs)) + interp_directives newstop acc (List.rev dirs)) with fallback_rename_hyp stop (acc:string list ref) th:unit := if Int.le stop 0 then () @@ -436,14 +445,15 @@ with fallback_rename_hyp stop (acc:string list ref) th:unit := () end) -with interp_directives acc ld:unit := - List.fold_right (fun d _ => interp_directive acc d) ld () +with interp_directives stop acc ld:unit := + List.fold_right (fun d _ => interp_directive stop acc d) ld () -with interp_directive acc d := +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)) - | RecRename n t => fallback_rename_hyp n acc t + | Rename t => fallback_rename_hyp stop acc t + | RenameN n t => fallback_rename_hyp n acc t end. (* Like in_context but then forget about the new goal. Only side effects are @@ -509,58 +519,103 @@ Ltac2 autorename_strict (h:ident) := (* Tactic renaming hypothesis H. *) -Ltac2 ltac2_autorename (h:ident) := +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. -#[global]Ltac2 ltac1_autorename_strict (h:Ltac1.t) := +Ltac2 ltac1_autorename_strict (h:Ltac1.t) := let h: ident := Option.get (Ltac1.to_ident h) in autorename_strict h. -Tactic Notation "autorename" hyp(h) := - let tac := ltac2:(h |- ltac1_autorename h) in - tac h. - -Tactic Notation "autorename_strict" hyp(h) := - let tac := ltac2:(h |- ltac1_autorename_strict h) in - tac h. - -Ltac2 decr (n:int):int := - if Int.equal n 0 then 0 else Int.sub n 1. - 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. - -(* Ltac2 Notation x(constr) "#" y(tactic(1)) := (RecRename x y). *) - - +(* This is the default renaming hard-coded in LibHYps *) Ltac2 Set rename_hyp_default := - fun n th: rename_directives => + fun n th => if Int.lt n 0 then [] else lazy_match! th with - | ?x <> ?y => [String "neq"; RecRename (decr n) x; RecRename (decr n) y] - | @cons _ ?x (cons ?y ?l) => [String "cons"; RecRename n x; RecRename n y; RecRename (decr (decr n)) l] - | @cons _ ?x ?l => if Int.ge n 1 then [String "cons"; RecRename n x; RecRename (decr n) l] else [String "cons"] - | (@Some _ ?x) => [RecRename (Int.add 1 n) x] + | ?x <> ?y => [ String "neq" ; Rename x ; Rename y ] + | (@Some _ ?x) => [RenameN (incr n) x] | (@None _) => [String "None"] end. -Definition DUMMY: Prop -> Prop. - exact (fun x:Prop => x). -Qed. +(* 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. -Ltac2 recRename n x := - RecRename (Option.get (Ltac1.to_int n)) (Option.get (Ltac1.to_constr x)). +Global Ltac mytac h := + let tac := ltac2:(h |- ltac1_mytac h) in + tac h. +Local Set Default Proof Mode "Classic". -(* ********** CUSTOMIZATION ********** *) +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 *) @@ -569,11 +624,21 @@ Ltac2 recRename n x := 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. @@ -581,8 +646,8 @@ 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" ; RecRename n x ; RecRename n y] - | true = Nat.eqb ?x ?y => [String "Neqb" ; RecRename n x ; RecRename n y] + | 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. @@ -592,6 +657,7 @@ 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 -> @@ -601,9 +667,11 @@ Lemma dummy: forall x y, 0 = 1 -> 223 = 426 -> (0 = 1)%Z -> - ~x = y -> + x <> y -> + Nat.eqb (x + 1) 0 <> Nat.eqb 1 y -> true = Nat.eqb 3 4 -> - Nat.eqb 3 4 = true -> + Nat.eqb (x + 3) 4 = true -> + Nat.eqb (2 * (x + 3)) 4 = true -> true = Nat.leb 3 4 -> 1 = 0 -> ~x = y -> @@ -630,7 +698,10 @@ Lemma dummy: forall x y, (0 < 1 -> ~(1<0)) -> (0 < 1 -> 1<0) -> 0 < z -> True. Proof. - intros;{(fun h => autorename h)}. + 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. @@ -643,10 +714,12 @@ Proof. 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_3n_4n0 with (3 =? 4) = true => 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. @@ -677,7 +750,9 @@ Proof. Qed. -(* + + + (* Ltac autorename h := *) (* let tac := ltac2:(h |- ltac2_autorename h) in *) (* tac h. *) @@ -686,31 +761,35 @@ Qed. (* 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) -> ex2 P Q -> False. +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 H2. + intros A P Q x H H0 H1 HH H2. autorename H1. autorename H2. autorename H. autorename H0. - assert (HH: (fun x => x = x) 1). - 2:{ autorename HH. } + Fail autorename_strict HH. + rename_or_revert HH. + intros ; { rename_or_revert }. + Fail intros ; { autorename_strict }. - ltac2:(let l := rename_acc 3 constr:(exists2 x0 : A, P x0 & Q x0) in + 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 := build_name l in + let nme := Ltac2.build_name l in printf "%s" nme). - ltac2:(let l := rename_acc 9 constr:(ex2 P Q) in + ltac2:(let l := Ltac2.rename_acc 9 constr:(ex2 P Q) in printf "BEFORE BUILDNAME %a " (pr_list pr_string) l; - let nme := build_name l in + let nme := Ltac2.build_name l in printf "%s" nme). Abort. diff --git a/LibHyps/LibHypsTactics.v b/LibHyps/LibHypsTactics.v index 3943acd..313cdcb 100644 --- a/LibHyps/LibHypsTactics.v +++ b/LibHyps/LibHypsTactics.v @@ -6,7 +6,8 @@ Require Export LibHyps.TacNewHyps. Require Export LibHyps.LibHypsNaming. (* Require Export LibHyps.LibSpecialize. *) -(* debug +(* START DEBUG *) +(* Module Prgoal_Notation. Ltac pr_goal := match goal with @@ -26,81 +27,12 @@ Proof. (* 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. +Abort. +(* END DEBUG *) + *) +(* TODO (* 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. *) @@ -348,3 +280,4 @@ Proof. intros ; { fun h => idtac h }. intros ; { ltac:(fun h => idtac h) }. *) +*) diff --git a/configure.sh b/configure.sh index 6569323..4904fe4 100755 --- a/configure.sh +++ b/configure.sh @@ -1,6 +1,7 @@ #!/bin/bash DEVOPT=no +STDLIB= POSITIONAL=() while [[ $# -gt 0 ]] @@ -8,6 +9,11 @@ do key="$1" case $key in + --stdlib|-stdlib) + shift + STDLIB=$1 + shift + ;; --dev) DEVOPT=yes shift @@ -28,10 +34,18 @@ set -- "${POSITIONAL[@]}" # restore positional parameters (i.e. 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" @@ -57,10 +71,10 @@ else 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/tests/LibHypsRegression.v b/tests/LibHypsRegression.v index 284b385..b357c7b 100644 --- a/tests/LibHypsRegression.v +++ b/tests/LibHypsRegression.v @@ -8,11 +8,45 @@ 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. *) +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. + +Ltac2 Set rename_hyp := rename_hyp_2. + +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. + +(* Ltac add_suffix ::= constr:(false). Ltac numerical_names ::= numerical_names_sufx. @@ -38,7 +72,7 @@ Ltac rename_hyp_3 n th := Ltac rename_hyp ::= rename_hyp_3. Ltac rename_depth ::= constr:(3). - +*) Close Scope Z_scope. Open Scope nat_scope. Lemma dummy: forall x y, @@ -49,7 +83,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 +127,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 +140,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. @@ -124,6 +163,7 @@ 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. @@ -140,19 +180,28 @@ Proof. 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/demo.v b/tests/demo.v index 7c24db4..93caba1 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 *) From acd120b08a7194eb2fd20fa25c98ba01a391d18f Mon Sep 17 00:00:00 2001 From: Pierre Courtieu Date: Tue, 24 Mar 2026 14:25:51 +0100 Subject: [PATCH 10/10] grouping hyps now works with ltac2. --- LibHyps/LibHyps.v | 18 ++- LibHyps/LibHypsTactics.v | 312 +++++++++++--------------------------- tests/LibHypsRegression.v | 39 +---- tests/LibHypsTest.v | 168 ++++---------------- tests/demo.v | 52 ++----- 5 files changed, 150 insertions(+), 439 deletions(-) diff --git a/LibHyps/LibHyps.v b/LibHyps/LibHyps.v index 3ba4768..f600dda 100644 --- a/LibHyps/LibHyps.v +++ b/LibHyps/LibHyps.v @@ -5,11 +5,11 @@ Require Export LibHyps.TacNewHyps. Require Export LibHyps.LibHypsNaming. Require Export LibHyps.Especialize. -(* Require Export LibHyps.LibHypsTactics. *) +Require Export LibHyps.LibHypsTactics. (* We export ; { } etc. ";;" also. *) -Ltac rename_or_revert H := autorename_strict H + generalize dependent H. +Ltac rename_or_revert H := autorename_strict H + revert dependent H. (* Some usual tactics one may want to use on new hyps. *) @@ -55,6 +55,8 @@ 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). *) @@ -68,20 +70,20 @@ Tactic Notation (at level 4) tactic4(Tac) "/" "s" := Tac ; { subst_or_idtac }. Tactic Notation (at level 4) "/" "s" := (onAllHyps subst_or_idtac). (* usual combinations *) -(*Tactic Notation (at level 4) tactic4(Tac) "//" := (Tac /s/n/g). +Tactic Notation (at level 4) tactic4(Tac) "//" := (Tac /s/n/g). Tactic Notation (at level 4) tactic4(Tac) "/" "sng" := (Tac /s/n/g). -Tactic Notation (at level 4) tactic4(Tac) "/" "sgn" := (Tac /s/g/n). *) +Tactic Notation (at level 4) tactic4(Tac) "/" "sgn" := (Tac /s/g/n). Tactic Notation (at level 4) tactic4(Tac) "/" "sn" := (Tac /s/n). Tactic Notation (at level 4) tactic4(Tac) "/" "sr" := (Tac /s/r). -(*Tactic Notation (at level 4) tactic4(Tac) "/" "sg" := (Tac /s/g). +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) 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) "/" "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. @@ -92,7 +94,7 @@ Module LegacyNotations. (* like !!tac + tries to subst with each new hypothesis. *) Tactic Notation "!!!" tactic3(Tac) := Tac/s/n?. (* Like !!! + regroup new Type-sorted hyps at top. *) - (* Tactic Notation (at level 4) "!!!!" tactic4(Tac) := Tac /s/n?/g. *) + Tactic Notation (at level 4) "!!!!" tactic4(Tac) := Tac /s/n?/g. (* Other Experimental combinations *) diff --git a/LibHyps/LibHypsTactics.v b/LibHyps/LibHypsTactics.v index 313cdcb..ca3c68e 100644 --- a/LibHyps/LibHypsTactics.v +++ b/LibHyps/LibHypsTactics.v @@ -5,249 +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 *) -(* -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. +(* +Require Import LibHypsDebug. + (* 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. + (pr_goal()). Abort. (* END DEBUG *) - *) - -(* TODO - -(* 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. - -(* 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. +*) -(* 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 - 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' + else if foundone then Some id + else find_above_which false t lH' + | [] => None 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 @@ -259,25 +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/tests/LibHypsRegression.v b/tests/LibHypsRegression.v index b357c7b..c2520d6 100644 --- a/tests/LibHypsRegression.v +++ b/tests/LibHypsRegression.v @@ -46,33 +46,6 @@ Ltac2 rename_hyp_3 n th := Ltac2 Set rename_hyp := rename_hyp_3. -(* -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`) - end. - -Ltac 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) - | _ => rename_hyp_2 n th (* call the previously defined tactic *) - end. - -Ltac rename_hyp ::= rename_hyp_3. -Ltac rename_depth ::= constr:(3). -*) Close Scope Z_scope. Open Scope nat_scope. Lemma dummy: forall x y, @@ -162,23 +135,23 @@ 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 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 93caba1..67b20da 100644 --- a/tests/demo.v +++ b/tests/demo.v @@ -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.