From 713ac976bcb09bc06ebbecd88cfed35a7f154216 Mon Sep 17 00:00:00 2001 From: Patrick Nicodemus Date: Thu, 20 Oct 2022 22:58:49 -0400 Subject: [PATCH 1/4] Have a couple different versions of the "hide" function that I'm debugging. --- Construction/Comma/Adjunction.v | 432 ++++++++++++++++++++++++++++++-- 1 file changed, 416 insertions(+), 16 deletions(-) diff --git a/Construction/Comma/Adjunction.v b/Construction/Comma/Adjunction.v index d3299649..458be06f 100644 --- a/Construction/Comma/Adjunction.v +++ b/Construction/Comma/Adjunction.v @@ -1,3 +1,5 @@ +From Ltac2 Require Ltac2. +From Ltac2 Require Import Notations. Require Import Category.Lib. Require Import Category.Theory.Category. Require Import Category.Theory.Isomorphism. @@ -106,9 +108,15 @@ Proof. destruct (iso_from_to (lawvere_iso E)), (projG E), (projF E). destruct X; split. - simpl in e2 |- *. - rewrite <- e2; cat. + refine (transitivity _ e2); + refine (transitivity _ (symmetry (id_right _))); + refine (transitivity _ (symmetry (id_left _))); + reflexivity. - simpl in e3 |- *. - rewrite <- e3; cat. + refine (transitivity _ e3). + refine (transitivity _ (symmetry (id_right _))); + refine (transitivity _ (symmetry (id_left _))); + reflexivity. Qed. Lemma μ_κ_θ : ∀ x, `1 (μ E x) ≈ κ E (ψ E x) ∘ θ E x. @@ -121,11 +129,165 @@ Proof. destruct (iso_to_from (lawvere_iso E)), (projG E), (projF E). destruct X; split. - simpl in e2 |- *. - rewrite <- e2; cat. + refine (transitivity _ e2); + refine (transitivity _ (symmetry (id_right _))); + refine (transitivity _ (symmetry (id_left _))); + reflexivity. - simpl in e3 |- *. - rewrite <- e3; cat. + refine (transitivity _ e3). + refine (transitivity _ (symmetry (id_right _))); + refine (transitivity _ (symmetry (id_left _))); + reflexivity. Qed. +(* traverse_thunk accepts an Ltac2 function f : A -> B and a thunk l : 1 -> A. It tries + to apply f to the result of computing l. If this is successful the computation + terminates; else it passes control to an error-handling function. + (Here,the function l will be the same but the value returned by l may be different.) + *) +Ltac2 rec traverse_thunk f l := + match Control.case l with + | Init.Val pair => let (val, c_p) := pair in + match Control.case (fun () => f val) with + | Init.Val pair => () + | Init.Err e => traverse_thunk f (fun () => (c_p e)) + end + | Init.Err e => () + end. +(* Intended usage : To select a subterm of the goal, + supply a SetPattern (an ordinary "pattern" with only holes but no metavariables) or + a SetInPattern (a pattern with one metavariable ?z, ?z will be the thing which is + selected. + *) +Ltac2 Type pattern_type := [ SetPattern (Init.unit -> Init.constr) + | SetInPattern (Init.pattern) ]. +Ltac2 only_in_goal := { Std.on_hyps := Init.Some [] ; Std.on_concl := Std.AllOccurrences }. +(* Feed this function a list of patterns and a (thunked) tactical, + and the function will capture and "set" all the subterms caught by the patterns; + then execute the tactical; + then clear the subterms in the reverse order they were established. *) + +Ltac2 rec hide pattern_list tac := + match pattern_list with + | [] => tac () + | head :: tail => + match head with + | SetPattern p => + let h := Fresh.in_goal @tempvar in + (Std.set + Init.false + (fun () => (Init.Some h, p ())) + { Std.on_hyps := Init.Some [] ; + Std.on_concl := Std.AllOccurrences }); + hide tail tac; + Std.unfold ((Std.VarRef h, Std.AllOccurrences) :: []) only_in_goal; + Std.clear (h :: []) + | SetInPattern p => + let subterm_stream := (fun () => Pattern.matches_subterm p (Control.goal ())) in + traverse_thunk + (fun l => let (_ , list_pairs) := l in + let rec hidepairs lp := + (match lp with + | [] => hide tail tac + | occ_head :: occ_tail => + let (_ , subterm) := occ_head in + if (Constr.is_var subterm) + then (Control.zero Init.Not_found) + else + (Message.print (Message.of_constr subterm); + let h := Fresh.in_goal @tempvar in + (set ($h := ($subterm)); + hide tail tac; + Std.unfold + ((Std.VarRef h, Std.AllOccurrences) :: []) only_in_goal; + Std.clear (h :: []))) + end) in hidepairs list_pairs) subterm_stream + end + end. + +Ltac2 hide1 p := + (* subterm_stream is a thunk of type context * ((ident * constr) list) *) + let subterm_stream := fun () => Pattern.matches_subterm p (Control.goal ()) in + let rec traverse_thunk' thunk := + match Control.case thunk with + | Init.Val pair => + let (a , c_p ) := pair in + let ( ctx , id_constr_list) := a in + match id_constr_list with + | [] => Control.zero Init.No_value (* The list shouldn't be empty, if you put in a + pattern with 1 quantifier you should get a + list with one element. *) + | x :: xs => let (ident, term) := x in + if Constr.is_var term then + (Message.print (Message.concat + (Message.of_string "Variable identified: ") + (Message.of_constr term)); + traverse_thunk' (fun () => c_p Init.Not_found)) + else + ( Message.print (Message.concat + (Message.of_string "Nontrivial subterm identified: ") + (Message.of_constr term)); + let h := Fresh.in_goal @tempvar in + match Control.case + (fun () => (progress (Std.set + Init.false + (fun () => (Init.Some h, term)) only_in_goal))) with + | Init.Val pair => let (a, _) := pair in a + | Init.Err e => + Message.print (Message.of_string "...but set failed."); + traverse_thunk' (fun () => c_p e) + end) + end + | Init.Err e => fail + end in traverse_thunk' subterm_stream. + + +Ltac2 hide1 p := + (* subterm_stream is a thunk of type context * ((ident * constr) list) *) + let subterm_stream := fun () => Pattern.matches_subterm p (Control.goal ()) in + let rec traverse_thunk' thunk := + match Control.case thunk with + | Init.Val pair => + let (a , c_p ) := pair in + let ( ctx , id_constr_list) := a in + match id_constr_list with + | [] => Control.zero Init.No_value (* The list shouldn't be empty, if you put in a + pattern with 1 quantifier you should get a + list with one element. *) + | x :: xs => let (ident, term) := x in + if Constr.is_var term then + traverse_thunk' (fun () => c_p Init.Not_found) + else + Message.print (Message.concat + (Message.of_string "Subterm identified: ") + (Message.of_constr term)); + let abc := Pattern.instantiate ctx open_constr:(_) in + Message.print (Message.concat + (Message.of_string "Pattern identified: ") + (Message.of_constr abc)); + let h := Fresh.in_goal @tempvar in + (Std.set Init.false (fun () => (Init.Some h, term)) only_in_goal) + end + | Init.Err e => fail + end in traverse_thunk' subterm_stream. + +(* Ltac2 hide1 p := *) +(* let subterm_stream := fun () => Pattern.matches_subterm p (Control.goal ()) in *) +(* traverse_thunk *) +(* (fun l => let (_ , list_pairs) := l in *) +(* let rec hidepairs lp := *) +(* (match lp with *) +(* | [] => () *) +(* | occ_head :: occ_tail => *) +(* let (_ , subterm) := occ_head in *) +(* if (Constr.is_var subterm) *) +(* then (Control.zero Init.Not_found) *) +(* else *) +(* (Message.print (Message.of_constr subterm); *) +(* let h := Fresh.in_goal @tempvar in *) +(* set ($h := ($subterm))) *) +(* end) in hidepairs list_pairs) subterm_stream. *) + Theorem ψ_φ_equiv : ∀ x, snd (from (κ E x)) ∘ snd (from (θ E (φ E x))) @@ -135,21 +297,257 @@ Theorem ψ_φ_equiv : ≈ `2 x. Proof. intros [[a b] f]; simpl in f |- *. - rewrite (snd_comp _ _ _ (κ E ((a, b); f))⁻¹ (θ E (φ E _))⁻¹). - rewrite <- !comp_assoc. - rewrite <- fmap_comp. - rewrite (fst_comp _ _ _ (θ E (φ E _)) (κ E ((a, b); f))). - rewrite <- η_θ_κ. - rewrite (`2 (η E ((a, b); f))). - rewrite η_θ_κ. - rewrite comp_assoc. - rewrite (snd_comp _ _ _ - ((κ E _)⁻¹ ∘ (θ E (φ E _))⁻¹) - (θ E (φ E _) ∘ κ E ((a, b); f))). - rewrite <- comp_assoc. + set (j1 := from (κ E _)); + set (j2 := (from (θ E _))); + change (snd j1 ∘ snd j2) with (snd (j1 ∘ j2)); + unfold j2, j1; clear j1 j2. + (* time(rewrite <- ! comp_assoc). *) + (* Tactic call ran for 0.474 secs (0.472u,0.s) (success) *) + (* Each pattern corresponds to a subterm of the goal which will be + "hidden" from the tactic. + Equivalent to: + set (j1 := snd _); + set (J2 := snd _); + set (j3 := fmap[F] _); + set (j4 := fmap[F] _); + match goal with + | [ |- context[@compose _ ?z]] => set (j5 := z) + end ; + match goal with + | [ |- context[@compose _ ?z]] => set (j6 := z) + end ; + rewrite <- ! comp_assoc; + ... + unfold j3; clear j3; + unfold j2; clear j2; + unfold j1; clear j1 *) + (* This call takes about 0.05 secs. *) + ltac2:(hide ( + SetPattern (fun () => '(snd _)) :: + SetPattern (fun () => '(snd _)) :: + SetPattern (fun () => '(`2 _)) :: + SetPattern (fun () => '(fmap[F] _)) :: + SetPattern (fun () => '(fmap[F] _)) :: + SetInPattern pat:(@compose _ ?z) :: + SetInPattern pat:(@compose _ ?z) :: + SetInPattern pat:(@compose _ ?z) :: + []) (fun () => ltac1:(rewrite <- ! comp_assoc))). + + (* Tactic call ran for 0.069 secs (0.069u,0.s) (success) *) + set (fst _); + set (fst _); + set (fst _); + set (y2 := fst _); + set (y3 := fst _); + assert (M := fmap_comp y2 y3); revert M; + set (snd _); + set (snd _); + set (`2 _); + intro H; rewrite <- H; + unfold y6, y5, y4, y3, y2, y1, y0, y; + clear y y0 y1 y2 y3 y4 y5 y6 H. + + (* 0.15 secs *) + set (j1 := θ E (fobj[φ E] ((a,b);f))); set (j2 := κ E ((a, b); f)); + change ((fst _ ∘ fst _)) with (fst (j1 ∘ j2)); + unfold j2, j1; clear j1 j2. + + (* Original tactic call ran for 0.846 secs (0.848u,0.s) (success) *) + (* rewrite <- η_θ_κ. *) + assert (M := η_θ_κ ((a, b); f)). + (* snd ((κ E ((a, b); f))⁻¹ ∘ (θ E (fobj[φ E] ((a, b); f)))⁻¹) + ∘ (`2 (fobj[ψ E] (fobj[φ E] ((a, b); f))) ∘ fmap[F] (fst `1 (η E ((a, b); f)))) ≈ f *) + revert M. + + set (κ E ((a, b); f)). + set (θ E _). + set (`1 _). + set (`1 _). + set (`2 _). + set (`1 _). + set (snd _). + set (snd _). + set (snd _). + ltac2:(hide1 pat:(@compose _ ?z)). + ltac2:(hide1 pat:(@compose _ ?z)). + set (@prod_setoid _ _ _ _ ). + ltac2:(hide1 pat:(@fst _ ?z)). + (* Unexpected behavior. *) + Set Printing All. +(* forall + _ : @equiv _ s y2 + (@compose (Product D C) tempvar1 + (@fobj _ _ (@comma_proj D C D (@Id D) G) + (@fobj _ _ (φ E) + (@existT (prod (@obj D) tempvar2) + (fun p : @obj (Product D C) => + @hom C (@fobj _ _ F (@fst (@obj D) tempvar2 p)) + (@fobj _ _ (@Id C) (@snd (@obj D) tempvar2 p))) + (@pair (@obj D) tempvar2 a b) f))) + (@fobj _ _ + (@Compose (@Comma D C D (@Id D) G) (@Comma D C C F (@Id C)) + (Product D C) (@comma_proj D C C F (@Id C)) (@from _ _ _ (lawvere_iso E))) *) + ltac2:(hide1 pat:(@fst _ ?z)). + Print Setoid. +(* Pattern identified: +(forall + _ : @equiv (prod (@hom D (?y y) (@fst (@obj D) (@obj C) y0)) (@hom C y3 y4)) s + y2 + (@compose (Product D C) tempvar1 *) + + ltac2:(hide1 pat:(@fst _ ?z)). + + + + time(ltac2:(hide ( + SetPattern (fun () => '(κ E ((a, b); f))) :: + SetPattern (fun () => '(θ E (fobj[φ E] ((a, b); f)))) :: + SetPattern (fun () => '(`1 _)) :: + SetPattern (fun () => '(`1 _)) :: + SetPattern (fun () => '(`2 _)) :: + SetPattern (fun () => '(`1 _)) :: + SetPattern (fun () => '(snd _)) :: + SetPattern (fun () => '(snd _)) :: + SetPattern (fun () => '(snd _)) :: + SetInPattern pat:(@compose _ ?z) :: + SetInPattern pat:(@compose _ ?z) :: + SetInPattern pat:(@fst _ _ ?z) :: + SetInPattern pat:(@fst ?z) :: + SetInPattern pat:(@fst _ _ ?z) :: + SetInPattern pat:(@fst _ _ ?z) :: + []) (fun () => ltac1:(intro M; rewrite <- M; clear M)))). + (* New call ran for .19 seconds *) + + (* time(rewrite (`2 (η E ((a, b); f)))). *) + (* Tactic call ran for 0.675 secs (0.675u,0.s) (success) *) + time( assert (M := (`2 (η E ((a, b); f)))); simpl in M; revert M; + ltac2:(hide ( + SetPattern (fun () => '(snd _)) :: + SetPattern (fun () => '(snd _)) :: + SetPattern (fun () => '(snd _)) :: + SetPattern (fun () => '(fst _)) :: + SetPattern (fun () => '(fst _)) :: + []) (fun () => ltac1:(intro M; rewrite M; clear M)))). + + assert (M := η_θ_κ ((a, b); f)); + set ( p1 := `1 (η E ((a, b); _))) in *. + (* Pattern matching did not grab the term we want to replace, + so we have to use unification *) + match goal with + | [ |- _ ∘ (snd ?j ∘ _) ≈ f ] => set (p2 := j) + end; change p2 with p1; clear p2; + revert M; + time(ltac2:(hide( + SetPattern (fun () => '(snd _)) :: + SetPattern (fun () => '(snd _)) :: + SetPattern (fun () => '(snd _)) :: + SetPattern (fun () => '(θ _ _)) :: + SetPattern (fun () => '(_ ∘ _)) :: + SetPattern (fun () => '(_ ∘ _)) :: + SetPattern (fun () => '(fst _)) :: + SetInPattern pat:(@compose _ ?a) :: + SetInPattern pat:(@equiv ?a) :: + SetInPattern pat:(@equiv ?a) :: + SetInPattern pat:(@equiv ?a) :: + SetInPattern pat:(@snd _ ?a) :: + SetInPattern pat:(@snd _ ?a) :: + SetInPattern pat:(@equiv ?a) :: + SetInPattern pat:(@equiv _ ?a) :: + SetInPattern pat:(@equiv _ ?a) :: + SetInPattern pat:(@snd ?a) :: + []) (fun () => ltac1:(intro M; rewrite M; clear M)))). + clear p1. + (* set (snd _). *) + (* set (snd _). *) + (* set (snd _). *) + (* set (θ _ _ ). *) + (* set (_ ∘ _). *) + (* set (_ ∘ _). *) + (* set (fst _). *) + (* ltac2:(hide1 pat:(@compose _ ?a)). *) + (* ltac2:(hide1 pat:(@equiv ?a)). *) + (* ltac2:(hide1 pat:(@equiv ?a)). *) + (* ltac2:(hide1 pat:(@equiv ?a)). *) + (* ltac2:(hide1 pat:(@snd _ ?a)). *) + (* ltac2:(hide1 pat:(@snd _ ?a)). *) + (* ltac2:(hide1 pat:(@equiv ?a)). *) + (* ltac2:(hide1 pat:(@equiv _ ?a)). *) + (* ltac2:(hide1 pat:(@equiv _ ?a)). *) + (* ltac2:(hide1 pat:(@snd ?a)). *) + (* set (fst _). *) + (* Set Printing All. *) + (* time(intro M; rewrite M; clear M). *) + + (* rewrite M. *) + + (* set ( p2 := `1 (η E ((a, b); f))). *) + + (* set ( p:= `1 (η _ _)). *) + + (* match goal with *) + (* | *) + (* rewrite M. *) + + + (* time(intro M; rewrite M; clear M). *) + (* set (κ _ _). *) + (* set (θ _ _). *) + + (* set (from _ ∘ from _). *) + (* set (@fobj _ _). *) + + + + (* time( ltac2:(hide ( *) + (* SetPattern (fun () => '(κ _ _)) :: *) + (* SetPattern (fun () => '(θ _ _)) :: *) + (* SetPattern (fun () => '(from _ ∘ _)) :: *) + (* SetPattern (fun () => '(@fobj _ _)) :: *) + + (* []) (fun () => ltac1:(intro M; rewrite M; clear M)))). *) + + (* time( ltac2:(hide ( *) + (* SetPattern (fun () => '(κ _ _)) :: *) + (* SetPattern (fun () => '(θ _ _)) :: *) + (* SetPattern (fun () => '(from _ ∘ _)) :: *) + (* SetPattern (fun () => '(@fobj _ _)) :: *) + + (* []) (fun () => ltac1:(rewrite (η_θ_κ ((a, b); f)))))). *) + + (* (* set (κ _ _); *) *) + (* (* set (θ _ _). *) *) + (* (* set (from _ ∘ _ ). *) *) + (* (* set (snd h). *) *) + (* (* set (@fobj _ _ ). *) *) + (* (* set (snd h). *) *) + + time(ltac2:(hide( + SetPattern (fun () => '(snd _)) :: + SetPattern (fun () => '(snd _)) :: + SetPattern (fun () => '(snd _)) :: + SetInPattern pat:(@compose _ ?a) :: + [] ) (fun () => ltac1:(rewrite comp_assoc)))). + (*********** *) + change (snd ((κ E _)⁻¹ ∘ (θ E (φ E _))⁻¹) ∘ snd _) with + (snd ( (κ E ((a, b); f))⁻¹ ∘ (θ E (fobj[φ E] ((a, b); f)))⁻¹ ∘ + (θ E (fobj[φ E] ((a, b); f)) ∘ κ E ((a, b); f)))). + (* time(rewrite <- comp_assoc). *) + (* 0.26 secs *) + ltac2:(hide1 pat:(@snd ?a)). + ltac2:(hide1 pat:(@compose _ ?a)). + + set(somecat := _ : Category). + + time(rewrite <- comp_assoc). + + +(*********) + + rewrite (comp_assoc (θ E (φ E ((a, b); f)))⁻¹ _). rewrite iso_from_to, id_left. now rewrite iso_from_to; cat. + Qed. Theorem φ_ψ_equiv : @@ -216,6 +614,8 @@ Next Obligation. rewrite H1; clear H1. comp_right. rewrite <- !comp_assoc. + Set Printing All. + rewrite (comp_assoc (fst _) _). spose (iso_to_from (κ E ((a, b); y))) as H0. destruct H0 as [H3 _]. From b3c236c693d7815a9ed1b624d0424744ab8876df Mon Sep 17 00:00:00 2001 From: Patrick Nicodemus Date: Fri, 21 Oct 2022 05:10:09 -0400 Subject: [PATCH 2/4] Finished working through proof-of-concept --- Construction/Comma/Adjunction.v | 611 ++++++++++++++++---------------- 1 file changed, 315 insertions(+), 296 deletions(-) diff --git a/Construction/Comma/Adjunction.v b/Construction/Comma/Adjunction.v index 458be06f..8d4b82c5 100644 --- a/Construction/Comma/Adjunction.v +++ b/Construction/Comma/Adjunction.v @@ -140,20 +140,6 @@ Proof. reflexivity. Qed. -(* traverse_thunk accepts an Ltac2 function f : A -> B and a thunk l : 1 -> A. It tries - to apply f to the result of computing l. If this is successful the computation - terminates; else it passes control to an error-handling function. - (Here,the function l will be the same but the value returned by l may be different.) - *) -Ltac2 rec traverse_thunk f l := - match Control.case l with - | Init.Val pair => let (val, c_p) := pair in - match Control.case (fun () => f val) with - | Init.Val pair => () - | Init.Err e => traverse_thunk f (fun () => (c_p e)) - end - | Init.Err e => () - end. (* Intended usage : To select a subterm of the goal, supply a SetPattern (an ordinary "pattern" with only holes but no metavariables) or a SetInPattern (a pattern with one metavariable ?z, ?z will be the thing which is @@ -166,7 +152,12 @@ Ltac2 only_in_goal := { Std.on_hyps := Init.Some [] ; Std.on_concl := Std.AllOcc and the function will capture and "set" all the subterms caught by the patterns; then execute the tactical; then clear the subterms in the reverse order they were established. *) - +Ltac2 progress_in_goal tac := + let old_goal := Control.goal() in + ( tac() ; + if Constr.equal old_goal (Control.goal()) then + Control.zero (Init.Tactic_failure + (Init.Some (Message.of_string "No change in goal"))) else () ). Ltac2 rec hide pattern_list tac := match pattern_list with | [] => tac () @@ -184,110 +175,88 @@ Ltac2 rec hide pattern_list tac := Std.clear (h :: []) | SetInPattern p => let subterm_stream := (fun () => Pattern.matches_subterm p (Control.goal ())) in - traverse_thunk - (fun l => let (_ , list_pairs) := l in - let rec hidepairs lp := - (match lp with - | [] => hide tail tac - | occ_head :: occ_tail => - let (_ , subterm) := occ_head in - if (Constr.is_var subterm) - then (Control.zero Init.Not_found) - else - (Message.print (Message.of_constr subterm); - let h := Fresh.in_goal @tempvar in - (set ($h := ($subterm)); - hide tail tac; - Std.unfold + let rec traverse_thunk subtermlist := + match Control.case subtermlist with + | Init.Val pair => let (subtermlist', c_p) := pair in + let (_ , list_pairs) := subtermlist' in + match list_pairs with + | [] => Control.throw ( + (Init.Tactic_failure (Init.Some (Message.of_string + "Patterns are required to have at least one metavariable.")))) + | occ_head :: occ_tail => let (_ , subterm) := occ_head in + if (Constr.is_var subterm) then + traverse_thunk + (fun () => c_p + (Init.Tactic_failure (Init.Some (Message.of_string + "Variable, skipping this pattern match.")))) + else ( + let h := Fresh.in_goal @tempvar in ( + let try_set := + (fun () => progress_in_goal + (fun () => Std.set Init.false + (fun () => (Init.Some h, subterm)) + only_in_goal)) in ( + match Control.case try_set with + | Init.Val _ => hide tail tac; + Std.unfold ((Std.VarRef h, Std.AllOccurrences) :: []) only_in_goal; - Std.clear (h :: []))) - end) in hidepairs list_pairs) subterm_stream + Std.clear (h :: []) + | Init.Err e => + traverse_thunk + (fun () => c_p + (Init.Tactic_failure (Init.Some (Message.of_string + "set failed to modify the goal.")))) + end))) + end + | Init.Err e => () + end in traverse_thunk subterm_stream end end. -Ltac2 hide1 p := - (* subterm_stream is a thunk of type context * ((ident * constr) list) *) - let subterm_stream := fun () => Pattern.matches_subterm p (Control.goal ()) in - let rec traverse_thunk' thunk := - match Control.case thunk with - | Init.Val pair => - let (a , c_p ) := pair in - let ( ctx , id_constr_list) := a in - match id_constr_list with - | [] => Control.zero Init.No_value (* The list shouldn't be empty, if you put in a - pattern with 1 quantifier you should get a - list with one element. *) - | x :: xs => let (ident, term) := x in - if Constr.is_var term then - (Message.print (Message.concat - (Message.of_string "Variable identified: ") - (Message.of_constr term)); - traverse_thunk' (fun () => c_p Init.Not_found)) - else - ( Message.print (Message.concat - (Message.of_string "Nontrivial subterm identified: ") - (Message.of_constr term)); - let h := Fresh.in_goal @tempvar in - match Control.case - (fun () => (progress (Std.set - Init.false - (fun () => (Init.Some h, term)) only_in_goal))) with - | Init.Val pair => let (a, _) := pair in a - | Init.Err e => - Message.print (Message.of_string "...but set failed."); - traverse_thunk' (fun () => c_p e) - end) - end - | Init.Err e => fail - end in traverse_thunk' subterm_stream. - +(** hide1 accepts a pattern p which is expected to have a single metavariable, i.e. + pat:(compose _ _ ?z). + + subterm_stream is a thunk of type context * ((ident * constr) list), where the + constr "term" is the subterm matched by ?z. + + If "term" is not a variable, we "set (H := term)", where H is a fresh variable name. + If "term" is a variable, or if "set H := term" fails to progress, we raise an + exception to the thunk subterm_stream, which responds by returning the next subterm + of the goal matching the p. We repeat this recursively until we either successfully + set a variable in the goal or exhaust all subterms. + *) Ltac2 hide1 p := - (* subterm_stream is a thunk of type context * ((ident * constr) list) *) let subterm_stream := fun () => Pattern.matches_subterm p (Control.goal ()) in let rec traverse_thunk' thunk := match Control.case thunk with | Init.Val pair => - let (a , c_p ) := pair in + let (a , c_p ) := pair in (* c_p - exception hander in + continuation-passing style *) let ( ctx , id_constr_list) := a in match id_constr_list with - | [] => Control.zero Init.No_value (* The list shouldn't be empty, if you put in a + | [] => + Control.zero Init.No_value (* The list shouldn't be empty, if you put in a pattern with 1 quantifier you should get a list with one element. *) - | x :: xs => let (ident, term) := x in - if Constr.is_var term then - traverse_thunk' (fun () => c_p Init.Not_found) - else - Message.print (Message.concat - (Message.of_string "Subterm identified: ") - (Message.of_constr term)); - let abc := Pattern.instantiate ctx open_constr:(_) in - Message.print (Message.concat - (Message.of_string "Pattern identified: ") - (Message.of_constr abc)); - let h := Fresh.in_goal @tempvar in - (Std.set Init.false (fun () => (Init.Some h, term)) only_in_goal) + | x :: xs => + let (ident, term) := x in + (if Constr.is_var term then + traverse_thunk' (fun () => c_p Init.Not_found) + else + let h := Fresh.in_goal @tempvar in + let try_set := (fun () => progress_in_goal + (fun () => + Std.set Init.false + (fun () => (Init.Some h, term)) only_in_goal)) in + match Control.case try_set with + | Init.Val pair => let (a, _) := pair in a + | Init.Err e => traverse_thunk' (fun () => c_p e) + end) end | Init.Err e => fail end in traverse_thunk' subterm_stream. -(* Ltac2 hide1 p := *) -(* let subterm_stream := fun () => Pattern.matches_subterm p (Control.goal ()) in *) -(* traverse_thunk *) -(* (fun l => let (_ , list_pairs) := l in *) -(* let rec hidepairs lp := *) -(* (match lp with *) -(* | [] => () *) -(* | occ_head :: occ_tail => *) -(* let (_ , subterm) := occ_head in *) -(* if (Constr.is_var subterm) *) -(* then (Control.zero Init.Not_found) *) -(* else *) -(* (Message.print (Message.of_constr subterm); *) -(* let h := Fresh.in_goal @tempvar in *) -(* set ($h := ($subterm))) *) -(* end) in hidepairs list_pairs) subterm_stream. *) - Theorem ψ_φ_equiv : ∀ x, snd (from (κ E x)) ∘ snd (from (θ E (φ E x))) @@ -321,9 +290,7 @@ Proof. unfold j3; clear j3; unfold j2; clear j2; unfold j1; clear j1 *) - (* This call takes about 0.05 secs. *) - ltac2:(hide ( - SetPattern (fun () => '(snd _)) :: + time(ltac2:(hide ( SetPattern (fun () => '(snd _)) :: SetPattern (fun () => '(`2 _)) :: SetPattern (fun () => '(fmap[F] _)) :: @@ -331,21 +298,87 @@ Proof. SetInPattern pat:(@compose _ ?z) :: SetInPattern pat:(@compose _ ?z) :: SetInPattern pat:(@compose _ ?z) :: - []) (fun () => ltac1:(rewrite <- ! comp_assoc))). + []) (fun () => ltac1:(rewrite <- ! comp_assoc)))). (* Tactic call ran for 0.069 secs (0.069u,0.s) (success) *) - set (fst _); - set (fst _); - set (fst _); - set (y2 := fst _); - set (y3 := fst _); - assert (M := fmap_comp y2 y3); revert M; - set (snd _); - set (snd _); - set (`2 _); - intro H; rewrite <- H; - unfold y6, y5, y4, y3, y2, y1, y0, y; - clear y y0 y1 y2 y3 y4 y5 y6 H. + + + (* I am trying to workshop a design pattern for doing this kind of + thing efficiently. This is what I have come up with so far. *) + (* First, get the equation you are rewriting with in the context. *) + match goal with + | |- context[ fmap[F] ?f1' ∘ fmap[F] ?g1' ] => + set(f1 := f1'); set (g1 := g1'); + assert (M := fmap_comp f1 g1); symmetry in M + end. + (* Then, we make sure that LHS of the equation M is bound to the + same variable as the term we want to rewrite. This ensures that no + simplifications we make to the goal will prevent the rewrite from succeeding + because it can no longer identify the terms we wanted to rewrite. + + The "context" operator in the goal helps us in the event that "set" is unable to + capture both the LHS of M and the term to be rewritten. + "set" does not perform any unification afaik, so we have to unify them + explicitly with "change." + *) + match goal with + | [h : ?a ≈ ?b |- context[(`2 _) ∘ ?c ]] => set (j1 := a) in *; change c with j1; revert h + end. + (* Now we can focus on simplifying the goal. *) + (* The idea is to think through the Proper hints and replace by a variable any + dependency which is only a parameter to the Proper hint and serves no role in the + resolution algorithm. + Here is a (not comprehensive) list of examples of type + information which usually plays no role in the Proper typeclass resolution. + + 1. in the rule p ≈ q => fst A B p, A and B are irrelevant to the pattern match, and + if A and B are complicated we can replace them both by variables to improve the + performance of the typeclass resolution. + 2. in the rules f ≈ f' -> @compose A B C f g ≈ @compose A B C f' g and + g ≈ g' -> @compose A B C f g ≈ @compose A B C f' g, + A, B, C are irrelevant to the pattern match. + 3. in functor composition, F ≈ F' -> @Compose C D E F G ≈ @Compose C D E F' G, + the categories are parameters and can be opaqued. + 4. In general the details of the equivalences _themselves_ cannot be opaqued, i.e., + if one has p : equiv A S f g where S is a setoid structure on A, opaquing + S would probably make little difference to the runtime because the resolution + algorithm would have to unfold it anyway to see what the equivalence relation is. + *However*, if the type A = A(p,q) is parametric in some p, q + and the setoid structure is also parametric in p, q, it might be possible to + opaque the parameters p, q. Example, in the hint + fmap_respects c d : forall f, g : hom c d, f ≈ g -> F f ≈ F g, + it would be possible to opaque the arguments c and d without the typeclass + resolution algorithm getting held up by this. + Thus we can safely call + ltac2:(hide1 pat:(@homset ?A)) - opaque the category + ltac2:(hide1 pat:(@homset _ ?A)) - opaque the domain + ltac2:(hide1 pat:(@homset _ _ ?A)) - opaque the codomain. + 5. Another example of 4, by the definition of prod_setoid, if f ≈ f' and g ≈ g' + then (f, f') ≈ (g, g'). + But the types of f,g and f' g' need not be fed to the typeclass resolution algorithm + concretely, just the setoid structures. The type of f and g can be opaqued, i.e., + ltac2:(hide1 pat:(@prod_setoid ?A)) + ltac2:(hide1 pat:(@prod_setoid _ ?B)) + 6. In fmap, the domain and codomain of the source morphism can be opaqued. + 7. As a general rule if all objects are fixed, and the computation is only on + morphisms, then we can opaque the objects. Thus + ltac2:(hide1 pat:(@hom _ ?c)) + ltac2:(hide1 pat:(@hom _ _ ?d)) + A possible future direction might be to assemble a list of such parameters which are + unlikely to play a role in typeclass resolution and write an automated script that + "opaques" all terms in the goal which seem irrelevant to the rewrite. + *) + time(ltac2:(hide( + SetPattern(fun () => '(fmap[F] _)) :: + SetPattern(fun () => '(snd _)) :: + SetPattern(fun () => '(snd _)) :: + SetPattern(fun () => '(`2 _)) :: + SetInPattern pat:(@compose _ ?a) :: + SetInPattern pat:(@compose _ _ ?a) :: + SetInPattern pat:(@homset _ _ ?a) :: + []) (fun () => ltac1:(intro M; rewrite M; clear M)))). + (* 0.049 secs *) + unfold f1, g1, j1; clear f1 g1 j1. (* 0.15 secs *) set (j1 := θ E (fobj[φ E] ((a,b);f))); set (j2 := κ E ((a, b); f)); @@ -354,200 +387,186 @@ Proof. (* Original tactic call ran for 0.846 secs (0.848u,0.s) (success) *) (* rewrite <- η_θ_κ. *) - assert (M := η_θ_κ ((a, b); f)). - (* snd ((κ E ((a, b); f))⁻¹ ∘ (θ E (fobj[φ E] ((a, b); f)))⁻¹) - ∘ (`2 (fobj[ψ E] (fobj[φ E] ((a, b); f))) ∘ fmap[F] (fst `1 (η E ((a, b); f)))) ≈ f *) - revert M. - set (κ E ((a, b); f)). - set (θ E _). - set (`1 _). - set (`1 _). - set (`2 _). - set (`1 _). - set (snd _). - set (snd _). - set (snd _). - ltac2:(hide1 pat:(@compose _ ?z)). - ltac2:(hide1 pat:(@compose _ ?z)). - set (@prod_setoid _ _ _ _ ). - ltac2:(hide1 pat:(@fst _ ?z)). - (* Unexpected behavior. *) - Set Printing All. -(* forall - _ : @equiv _ s y2 - (@compose (Product D C) tempvar1 - (@fobj _ _ (@comma_proj D C D (@Id D) G) - (@fobj _ _ (φ E) - (@existT (prod (@obj D) tempvar2) - (fun p : @obj (Product D C) => - @hom C (@fobj _ _ F (@fst (@obj D) tempvar2 p)) - (@fobj _ _ (@Id C) (@snd (@obj D) tempvar2 p))) - (@pair (@obj D) tempvar2 a b) f))) - (@fobj _ _ - (@Compose (@Comma D C D (@Id D) G) (@Comma D C C F (@Id C)) - (Product D C) (@comma_proj D C C F (@Id C)) (@from _ _ _ (lawvere_iso E))) *) - ltac2:(hide1 pat:(@fst _ ?z)). - Print Setoid. -(* Pattern identified: -(forall - _ : @equiv (prod (@hom D (?y y) (@fst (@obj D) (@obj C) y0)) (@hom C y3 y4)) s - y2 - (@compose (Product D C) tempvar1 *) - - ltac2:(hide1 pat:(@fst _ ?z)). - - - - time(ltac2:(hide ( - SetPattern (fun () => '(κ E ((a, b); f))) :: - SetPattern (fun () => '(θ E (fobj[φ E] ((a, b); f)))) :: - SetPattern (fun () => '(`1 _)) :: - SetPattern (fun () => '(`1 _)) :: - SetPattern (fun () => '(`2 _)) :: - SetPattern (fun () => '(`1 _)) :: - SetPattern (fun () => '(snd _)) :: - SetPattern (fun () => '(snd _)) :: - SetPattern (fun () => '(snd _)) :: - SetInPattern pat:(@compose _ ?z) :: - SetInPattern pat:(@compose _ ?z) :: - SetInPattern pat:(@fst _ _ ?z) :: - SetInPattern pat:(@fst ?z) :: - SetInPattern pat:(@fst _ _ ?z) :: - SetInPattern pat:(@fst _ _ ?z) :: - []) (fun () => ltac1:(intro M; rewrite <- M; clear M)))). - (* New call ran for .19 seconds *) - - (* time(rewrite (`2 (η E ((a, b); f)))). *) - (* Tactic call ran for 0.675 secs (0.675u,0.s) (success) *) - time( assert (M := (`2 (η E ((a, b); f)))); simpl in M; revert M; - ltac2:(hide ( - SetPattern (fun () => '(snd _)) :: - SetPattern (fun () => '(snd _)) :: - SetPattern (fun () => '(snd _)) :: - SetPattern (fun () => '(fst _)) :: - SetPattern (fun () => '(fst _)) :: - []) (fun () => ltac1:(intro M; rewrite M; clear M)))). - - assert (M := η_θ_κ ((a, b); f)); - set ( p1 := `1 (η E ((a, b); _))) in *. - (* Pattern matching did not grab the term we want to replace, - so we have to use unification *) + (* Another instance of this technique / pattern. *) + assert (M := η_θ_κ ((a, b); f)). match goal with - | [ |- _ ∘ (snd ?j ∘ _) ≈ f ] => set (p2 := j) - end; change p2 with p1; clear p2; - revert M; + | [ h : ?a ≈ ?b |- context[ fst ?c ] ] => + set (j1 := a) in *; set (j2 := b) in * ; change c with j2; revert M + end. time(ltac2:(hide( - SetPattern (fun () => '(snd _)) :: - SetPattern (fun () => '(snd _)) :: - SetPattern (fun () => '(snd _)) :: - SetPattern (fun () => '(θ _ _)) :: - SetPattern (fun () => '(_ ∘ _)) :: - SetPattern (fun () => '(_ ∘ _)) :: - SetPattern (fun () => '(fst _)) :: - SetInPattern pat:(@compose _ ?a) :: - SetInPattern pat:(@equiv ?a) :: - SetInPattern pat:(@equiv ?a) :: - SetInPattern pat:(@equiv ?a) :: - SetInPattern pat:(@snd _ ?a) :: - SetInPattern pat:(@snd _ ?a) :: - SetInPattern pat:(@equiv ?a) :: - SetInPattern pat:(@equiv _ ?a) :: - SetInPattern pat:(@equiv _ ?a) :: - SetInPattern pat:(@snd ?a) :: - []) (fun () => ltac1:(intro M; rewrite M; clear M)))). - clear p1. - (* set (snd _). *) - (* set (snd _). *) - (* set (snd _). *) - (* set (θ _ _ ). *) - (* set (_ ∘ _). *) - (* set (_ ∘ _). *) - (* set (fst _). *) - (* ltac2:(hide1 pat:(@compose _ ?a)). *) - (* ltac2:(hide1 pat:(@equiv ?a)). *) - (* ltac2:(hide1 pat:(@equiv ?a)). *) - (* ltac2:(hide1 pat:(@equiv ?a)). *) - (* ltac2:(hide1 pat:(@snd _ ?a)). *) - (* ltac2:(hide1 pat:(@snd _ ?a)). *) - (* ltac2:(hide1 pat:(@equiv ?a)). *) - (* ltac2:(hide1 pat:(@equiv _ ?a)). *) - (* ltac2:(hide1 pat:(@equiv _ ?a)). *) - (* ltac2:(hide1 pat:(@snd ?a)). *) - (* set (fst _). *) - (* Set Printing All. *) - (* time(intro M; rewrite M; clear M). *) - - (* rewrite M. *) - - (* set ( p2 := `1 (η E ((a, b); f))). *) - - (* set ( p:= `1 (η _ _)). *) - - (* match goal with *) - (* | *) - (* rewrite M. *) - - - (* time(intro M; rewrite M; clear M). *) - (* set (κ _ _). *) - (* set (θ _ _). *) - - (* set (from _ ∘ from _). *) - (* set (@fobj _ _). *) - - - - (* time( ltac2:(hide ( *) - (* SetPattern (fun () => '(κ _ _)) :: *) - (* SetPattern (fun () => '(θ _ _)) :: *) - (* SetPattern (fun () => '(from _ ∘ _)) :: *) - (* SetPattern (fun () => '(@fobj _ _)) :: *) - - (* []) (fun () => ltac1:(intro M; rewrite M; clear M)))). *) - - (* time( ltac2:(hide ( *) - (* SetPattern (fun () => '(κ _ _)) :: *) - (* SetPattern (fun () => '(θ _ _)) :: *) - (* SetPattern (fun () => '(from _ ∘ _)) :: *) - (* SetPattern (fun () => '(@fobj _ _)) :: *) + SetInPattern pat:( _ -> ?a ∘ _ ≈ f) :: + SetPattern (fun () => '(`2 _)) :: + SetInPattern pat:(@hom _ ?a) :: + SetInPattern pat:(@hom _ ?a) :: + SetInPattern pat:(@hom _ ?a) :: + SetInPattern pat:(@hom _ ?a) :: + SetInPattern pat:(@hom _ ?a) :: + SetInPattern pat:(@hom _ _ ?a) :: + SetInPattern pat:(@hom _ _ ?a) :: + SetInPattern pat:(@hom _ _ ?a) :: + SetInPattern pat:(@hom _ _ ?a) :: + SetInPattern pat:(@compose _ _ ?a) :: + SetInPattern pat:(@compose _ _ ?a) :: + SetInPattern pat:(@prod_setoid _ ?a) :: + SetInPattern pat:(@prod_setoid _ _ ?a) :: + []) (fun () => intro M; rewrite <- M; clear M))). + (* It is clear that this process could be more automated, + for example by giving an option to repeating "hide" for each + pattern application until it fails and new variables cannot be introduced. *) + unfold j1, j2; clear j1 j2. + + (* We will repeat this for each rewrite step in the proof. *) + + time(assert (M := (`2 (η E ((a, b); f)))); simpl in M; + match goal with + | [h : ?a ≈ ?b |- context[(snd _) ∘ ?c ≈ f] ] => + set (j1 := a) in *; set (j2 := b) in *; change c with j1 + end; + ltac2:(hide ( + SetInPattern pat:(?a ∘ _) :: + SetInPattern pat:(@compose _ ?a) :: + SetInPattern pat:(@compose _ _ ?a) :: + []) (fun () => ltac1:(rewrite M; clear M))); + unfold j1, j2; clear). - (* []) (fun () => ltac1:(rewrite (η_θ_κ ((a, b); f)))))). *) - (* (* set (κ _ _); *) *) - (* (* set (θ _ _). *) *) - (* (* set (from _ ∘ _ ). *) *) - (* (* set (snd h). *) *) - (* (* set (@fobj _ _ ). *) *) - (* (* set (snd h). *) *) - - time(ltac2:(hide( + assert (M := η_θ_κ ((a, b); f)); + match goal with + | [ h : ?a ≈ ?b |- _ ∘ (snd ?c ∘ _) ≈ f ] => + set (j1 := a) in *; set (j2 := b) in *; change c with j1; revert M + end; + ltac2:(hide( + SetInPattern pat:( _ → ?a ∘ _ ≈ _) :: + SetInPattern pat:(@compose _ ?a) :: + SetInPattern pat:(@compose _ ?a) :: + SetInPattern pat:(@compose _ _ ?a) :: + SetInPattern pat:(@compose _ _ ?a) :: + SetInPattern pat:(@compose _ _ _ ?a) :: + SetInPattern pat:(@snd ?a) :: + SetInPattern pat:(@snd ?a) :: + SetInPattern pat:(@snd _ ?b) :: + SetInPattern pat:(@snd _ ?b) :: + SetInPattern pat:(@hom _ ?b) :: + SetInPattern pat:(@hom _ _ ?b) :: + SetInPattern pat:(@prod_setoid ?a) :: + SetInPattern pat:(@prod_setoid _ ?b) :: + []) (fun () => ltac1:(intro M; rewrite M; clear M))); + unfold j1, j2; clear j1 j2. + + time(ltac2:(hide( SetPattern (fun () => '(snd _)) :: SetPattern (fun () => '(snd _)) :: SetPattern (fun () => '(snd _)) :: SetInPattern pat:(@compose _ ?a) :: - [] ) (fun () => ltac1:(rewrite comp_assoc)))). - (*********** *) - change (snd ((κ E _)⁻¹ ∘ (θ E (φ E _))⁻¹) ∘ snd _) with + [] ) (fun () => ltac1:(rewrite comp_assoc)))). + + change (snd ((κ E _)⁻¹ ∘ (θ E (φ E _))⁻¹) ∘ snd _) with (snd ( (κ E ((a, b); f))⁻¹ ∘ (θ E (fobj[φ E] ((a, b); f)))⁻¹ ∘ (θ E (fobj[φ E] ((a, b); f)) ∘ κ E ((a, b); f)))). - (* time(rewrite <- comp_assoc). *) - (* 0.26 secs *) - ltac2:(hide1 pat:(@snd ?a)). - ltac2:(hide1 pat:(@compose _ ?a)). - - set(somecat := _ : Category). - - time(rewrite <- comp_assoc). - -(*********) + match goal with + | [ |- context[?f1' ∘ ?f2' ∘ ?f3'] ] => + set (f1 := f1'); set (f2 := f2'); set (f3 := f3'); + assert (M := comp_assoc f1 f2 f3); revert M; + set (j2 := f1 ∘ f2 ∘ f3) in * + end; + ltac2:(hide( + SetInPattern pat:(@snd _ ?a) :: + SetInPattern pat:(@snd _ ?a) :: + SetInPattern pat:(@compose ?a) :: + SetInPattern pat:(@compose _ ?a) :: + SetInPattern pat:(@compose _ _ ?a) :: + SetInPattern pat:(@compose _ _ ?a) :: + []) (fun () => ltac1:(intro M; rewrite <- M; clear M))); + unfold j2, f3, f2, f1; clear. + + match goal with + | [ |- context[_ ∘ (?f1' ∘ (?f2' ∘ ?f3'))] ] => + set (f1 := f1'); set (f2 := f2'); set (f3 := f3') + end; + assert (M := comp_assoc f1 f2 f3); + set (j1 := f1 ∘ (f2 ∘ f3)) in *; + match goal with + | [ h : ?a ≈ ?b |- snd (_ ∘ ?x) ∘ f ≈ f ] => change x with j1 + end; + revert M; + ltac2:(hide( + SetPattern (fun () => '(from _)) :: + SetInPattern pat:(@snd ?a) :: + SetInPattern pat:(@snd ?a) :: + SetInPattern pat:(@snd _ ?b) :: + SetInPattern pat:(@snd _ ?b) :: + SetInPattern pat:(@compose ?c) :: + SetInPattern pat:(@compose _ ?c) :: + SetInPattern pat:(@compose _ ?c) :: + SetInPattern pat:(@compose _ ?c) :: + SetInPattern pat:(@compose _ _ ?c) :: + SetInPattern pat:(@compose _ _ ?c) :: + []) (fun () => ltac1:(intro M; rewrite M; clear M))); + unfold f1, f2, f3, j1; clear. - rewrite (comp_assoc (θ E (φ E ((a, b); f)))⁻¹ _). - rewrite iso_from_to, id_left. - now rewrite iso_from_to; cat. + match goal with + | [ |- context[from ?f1' ∘ to ?f1'] ] => set (f1 := f1') + end. + assert (M := iso_from_to f1). + match goal with + | [ h : ?a ≈ ?b |- _ ] => set (j1 := a) in * + end. + revert M. + ltac2:(hide( + SetInPattern pat:(snd (?a ∘ _) ∘ _) :: + SetInPattern pat:(snd (_ ∘ (_ ∘ ?b))) :: + SetInPattern pat:(@compose ?a) :: + SetInPattern pat:(@compose _ ?a) :: + SetInPattern pat:(@compose _ ?a) :: + SetInPattern pat:(@compose _ _ ?a) :: + SetInPattern pat:(@compose _ _ ?a) :: + SetInPattern pat:(@snd ?a) :: + SetInPattern pat:(@snd ?a) :: + SetInPattern pat:(@snd _ ?a) :: + []) (fun () => ltac1:(intro M; rewrite M; clear M))); + unfold j1, f1; clear j1 f1. + + match goal with + | [ |- context[ id ∘ ?f1' ] ] => + assert (M := id_left f1'); set (f1 := f1') in *; set (j1 := id ∘ f1) in * + end; + match goal with + | [ |- snd (_ ∘ ?a) ∘ _ ≈ _ ] => change a with j1 + end; + revert M; + ltac2:(hide( + SetInPattern pat:(@snd ?a) :: + SetInPattern pat:(@snd ?a) :: + SetInPattern pat:(@snd _ ?a) :: + SetInPattern pat:(@compose ?a) :: + SetInPattern pat:(@compose _ ?a) :: + SetInPattern pat:(@compose _ ?a) :: + SetInPattern pat:(@compose _ _ ?a) :: + []) (fun () => ltac1:(intro M; rewrite M; clear M))); + unfold j1, f1; clear j1 f1. + + match goal with + | [ |- context[from ?f1' ∘ to ?f1'] ] => set (f1 := f1') + end. + assert (M := iso_from_to f1). + match goal with + | [ h : ?a ≈ ?b |- _ ] => set (j1 := a) in * + end. + revert M. + ltac2:(hide( + SetInPattern pat:(@snd ?a) :: + SetInPattern pat:(@snd ?a) :: + SetInPattern pat:(@snd _ ?a) :: + SetInPattern pat:(@snd _ ?a) :: + SetInPattern pat:(@compose _ ?a) :: + []) (fun () => ltac1:(intro M; rewrite M; clear M))); + unfold j1, f1; clear j1 f1. + simpl. + exact (id_left f). Qed. Theorem φ_ψ_equiv : From 3d469f23ef54834fb05da86fee84088c016770f9 Mon Sep 17 00:00:00 2001 From: Patrick Nicodemus Date: Fri, 21 Oct 2022 14:35:03 -0400 Subject: [PATCH 3/4] About to make some big changes to the definitions of "hide" and related functions, saving my work before I continue. --- Construction/Comma/Adjunction.v | 50 +++++++++++++++++++++++++++++---- 1 file changed, 44 insertions(+), 6 deletions(-) diff --git a/Construction/Comma/Adjunction.v b/Construction/Comma/Adjunction.v index 8d4b82c5..96552a73 100644 --- a/Construction/Comma/Adjunction.v +++ b/Construction/Comma/Adjunction.v @@ -145,19 +145,57 @@ Qed. a SetInPattern (a pattern with one metavariable ?z, ?z will be the thing which is selected. *) -Ltac2 Type pattern_type := [ SetPattern (Init.unit -> Init.constr) - | SetInPattern (Init.pattern) ]. +Ltac2 Type pattern_type := [ SetPattern_ntimes ( (Init.unit -> Init.constr) * Init.int ) + | SetPatternRepeat (Init.unit -> Init.constr) + | SetInPattern_ntimes (Init.pattern * Init.int) + | SetInPatternRepeat (Init.pattern) ]. Ltac2 only_in_goal := { Std.on_hyps := Init.Some [] ; Std.on_concl := Std.AllOccurrences }. -(* Feed this function a list of patterns and a (thunked) tactical, - and the function will capture and "set" all the subterms caught by the patterns; - then execute the tactical; - then clear the subterms in the reverse order they were established. *) + +(* progress_in_goal is like progress, but it only succeeds + if there is a change on the RHS of the sequent; + whereas "progress" succeeds if there is a change + in either the goals or hypotheses. *) + Ltac2 progress_in_goal tac := let old_goal := Control.goal() in ( tac() ; if Constr.equal old_goal (Control.goal()) then Control.zero (Init.Tactic_failure (Init.Some (Message.of_string "No change in goal"))) else () ). + +(* strictset accepts an identifier and a thunked term. It tries to "set identifier := term." + If the goal is unchanged, it raises an exception. *) +Ltac2 strictset ident term := + progress_in_goal + (fun () => Std.set Init.false (fun () => (Init.Some ident, term() )) + { Std.on_hyps := Init.Some [] ; Std.on_concl := Std.AllOccurrences }). + +Ltac2 rec hide_SetPattern_ntimes thunk n := + if (Int.lt n 0) then Control.zero (Control.throw( + Init.Tactic_failure (Init.Some (Message.of_string "Pattern asked to repeat < 0 times")))) + else if (Int.equal n 0) then [] + else let h := Fresh.in_goal @tmpvar in + (strictset h thunk); h :: (hide_SetPattern_ntimes thunk (Int.sub n 1)). + +(* This function should accept as input a pattern list. + It should go through them one by one and "set" each item in the list. + It should return a list of identifiers corresponding to the terms that + were successfully set. + *) +Ltac2 hide_draft1 pattern_list := + match pattern_list with + | [] => [] + | hhead :: ttail => + match head with + | SetPattern_ntimes tthunk nat => + if (n < 0) then + + else if (n = 0) then [] + else + end + end + + Ltac2 rec hide pattern_list tac := match pattern_list with | [] => tac () From dec5be18e407a235a9865b7d7fd1dc52fca18b00 Mon Sep 17 00:00:00 2001 From: Patrick Nicodemus Date: Sat, 22 Oct 2022 08:42:51 -0400 Subject: [PATCH 4/4] Redefined the basic "hide" functions and tested them out. --- Construction/Comma/Adjunction.v | 540 +++++++++++++++----------------- 1 file changed, 254 insertions(+), 286 deletions(-) diff --git a/Construction/Comma/Adjunction.v b/Construction/Comma/Adjunction.v index 96552a73..252b7db8 100644 --- a/Construction/Comma/Adjunction.v +++ b/Construction/Comma/Adjunction.v @@ -140,22 +140,26 @@ Proof. reflexivity. Qed. -(* Intended usage : To select a subterm of the goal, - supply a SetPattern (an ordinary "pattern" with only holes but no metavariables) or - a SetInPattern (a pattern with one metavariable ?z, ?z will be the thing which is - selected. - *) +(* I have not used this type yet but it might be useful to pass a list of + elements of type pattern_type to a master function which "opaques" + every subterm of the goal corresponding to flags in the list. + Right now there are many different functions which could be unified + under this approach. *) Ltac2 Type pattern_type := [ SetPattern_ntimes ( (Init.unit -> Init.constr) * Init.int ) | SetPatternRepeat (Init.unit -> Init.constr) | SetInPattern_ntimes (Init.pattern * Init.int) | SetInPatternRepeat (Init.pattern) ]. + Ltac2 only_in_goal := { Std.on_hyps := Init.Some [] ; Std.on_concl := Std.AllOccurrences }. (* progress_in_goal is like progress, but it only succeeds if there is a change on the RHS of the sequent; whereas "progress" succeeds if there is a change - in either the goals or hypotheses. *) - + in either the goals or hypotheses. + This is useful for a tactic like "set", where intuitively it "progresses" + only if it actually replaces a term in the goal, not merely if it adds a new + definition to the context. +*) Ltac2 progress_in_goal tac := let old_goal := Control.goal() in ( tac() ; @@ -170,130 +174,135 @@ Ltac2 strictset ident term := (fun () => Std.set Init.false (fun () => (Init.Some ident, term() )) { Std.on_hyps := Init.Some [] ; Std.on_concl := Std.AllOccurrences }). +(* hide_SetPattern_ntimes accepts a thunked constr, + possibly with holes, and a natural number n.*) +(* It replaces exactly n of the subterms matched by the pattern, or fails. + It returns a list of identifiers corresponding to the new variable names + created in the context. + *) Ltac2 rec hide_SetPattern_ntimes thunk n := if (Int.lt n 0) then Control.zero (Control.throw( Init.Tactic_failure (Init.Some (Message.of_string "Pattern asked to repeat < 0 times")))) else if (Int.equal n 0) then [] else let h := Fresh.in_goal @tmpvar in (strictset h thunk); h :: (hide_SetPattern_ntimes thunk (Int.sub n 1)). - -(* This function should accept as input a pattern list. - It should go through them one by one and "set" each item in the list. - It should return a list of identifiers corresponding to the terms that - were successfully set. - *) -Ltac2 hide_draft1 pattern_list := - match pattern_list with - | [] => [] - | hhead :: ttail => - match head with - | SetPattern_ntimes tthunk nat => - if (n < 0) then - - else if (n = 0) then [] - else - end - end - -Ltac2 rec hide pattern_list tac := - match pattern_list with - | [] => tac () - | head :: tail => - match head with - | SetPattern p => - let h := Fresh.in_goal @tempvar in - (Std.set - Init.false - (fun () => (Init.Some h, p ())) - { Std.on_hyps := Init.Some [] ; - Std.on_concl := Std.AllOccurrences }); - hide tail tac; - Std.unfold ((Std.VarRef h, Std.AllOccurrences) :: []) only_in_goal; - Std.clear (h :: []) - | SetInPattern p => - let subterm_stream := (fun () => Pattern.matches_subterm p (Control.goal ())) in - let rec traverse_thunk subtermlist := - match Control.case subtermlist with - | Init.Val pair => let (subtermlist', c_p) := pair in - let (_ , list_pairs) := subtermlist' in - match list_pairs with - | [] => Control.throw ( - (Init.Tactic_failure (Init.Some (Message.of_string - "Patterns are required to have at least one metavariable.")))) - | occ_head :: occ_tail => let (_ , subterm) := occ_head in +(* hide_SetPatternRepeat accepts a thunked constr. *) +(* It tries to pattern-match with this constr repeatedly, + replacing its value with a variable, until it can no longer make progress. + It returns a list of identifiers corresponding to the new variable names + created in the context. +*) +Ltac2 rec hide_SetPatternRepeat thunk := + let h := Fresh.in_goal @tmpvar in + match Control.case (fun () => (strictset h thunk)) with + | Init.Val _ => h :: (hide_SetPatternRepeat thunk) + | Init.Err _ => [] + end. + +(* hide_SetInPattern_ntimes accepts a pattern with one metavariable ?z. *) +(* It tries to pattern-match with this pattern exactly n times, in each match + replacing the value of ?z with a variable until it can no longer make progress. + It returns a list of identifiers corresponding to the new variable names + created in the context. +*) +Ltac2 rec hide_SetInPattern_ntimes pat n := + if (Int.lt n 0) then Control.zero (Control.throw( + Init.Tactic_failure (Init.Some (Message.of_string "Pattern asked to repeat < 0 times")))) + else if (Int.equal n 0) then [] else + let subterm_stream := (fun () => Pattern.matches_subterm pat (Control.goal ())) in + let rec traverse_thunk subtermlist := + match Control.case subtermlist with + | Init.Val pair => + let (subtermlist', c_p) := pair in + let (_ , list_pairs) := subtermlist' in + match list_pairs with + | [] => Control.throw ((Init.Tactic_failure (Init.Some (Message.of_string + "Patterns are required to have at least one metavariable.")))) + | occ_head :: occ_tail => let (_ , subterm) := occ_head in if (Constr.is_var subterm) then traverse_thunk (fun () => c_p (Init.Tactic_failure (Init.Some (Message.of_string "Variable, skipping this pattern match.")))) - else ( - let h := Fresh.in_goal @tempvar in ( - let try_set := - (fun () => progress_in_goal - (fun () => Std.set Init.false - (fun () => (Init.Some h, subterm)) - only_in_goal)) in ( - match Control.case try_set with - | Init.Val _ => hide tail tac; - Std.unfold - ((Std.VarRef h, Std.AllOccurrences) :: []) only_in_goal; - Std.clear (h :: []) - | Init.Err e => - traverse_thunk + else + let h := Fresh.in_goal @tmpvar in + match Control.case (fun () => (strictset h (fun () => subterm))) with + | Init.Val _ => h :: (hide_SetInPattern_ntimes pat (Int.sub n 1)) + | Init.Err e => traverse_thunk + (fun () => c_p + (Init.Tactic_failure (Init.Some (Message.of_string + "set failed to modify the goal.")))) + end + end + | Init.Err e => [] + end in traverse_thunk subterm_stream. + +(* Analogous to hide_SetPatternRepeat except that it accepts a "pattern" (with metavariables) + rather than an "constr" (a term, potentially with holes). *) +Ltac2 rec hide_SetInPatternRepeat pat := + let subterm_stream := (fun () => Pattern.matches_subterm pat (Control.goal ())) in + let rec traverse_thunk subtermlist := + match Control.case subtermlist with + | Init.Val pair => + let (subtermlist', c_p) := pair in + let (_ , list_pairs) := subtermlist' in + match list_pairs with + | [] => Control.throw ((Init.Tactic_failure (Init.Some (Message.of_string + "Patterns are required to have at least one metavariable.")))) + | occ_head :: occ_tail => let (_ , subterm) := occ_head in + if (Constr.is_var subterm) then + traverse_thunk (fun () => c_p (Init.Tactic_failure (Init.Some (Message.of_string - "set failed to modify the goal.")))) - end))) - end - | Init.Err e => () - end in traverse_thunk subterm_stream - end - end. - -(** hide1 accepts a pattern p which is expected to have a single metavariable, i.e. - pat:(compose _ _ ?z). - - subterm_stream is a thunk of type context * ((ident * constr) list), where the - constr "term" is the subterm matched by ?z. - - If "term" is not a variable, we "set (H := term)", where H is a fresh variable name. - If "term" is a variable, or if "set H := term" fails to progress, we raise an - exception to the thunk subterm_stream, which responds by returning the next subterm - of the goal matching the p. We repeat this recursively until we either successfully - set a variable in the goal or exhaust all subterms. - *) - -Ltac2 hide1 p := - let subterm_stream := fun () => Pattern.matches_subterm p (Control.goal ()) in - let rec traverse_thunk' thunk := - match Control.case thunk with - | Init.Val pair => - let (a , c_p ) := pair in (* c_p - exception hander in - continuation-passing style *) - let ( ctx , id_constr_list) := a in - match id_constr_list with - | [] => - Control.zero Init.No_value (* The list shouldn't be empty, if you put in a - pattern with 1 quantifier you should get a - list with one element. *) - | x :: xs => - let (ident, term) := x in - (if Constr.is_var term then - traverse_thunk' (fun () => c_p Init.Not_found) - else - let h := Fresh.in_goal @tempvar in - let try_set := (fun () => progress_in_goal - (fun () => - Std.set Init.false - (fun () => (Init.Some h, term)) only_in_goal)) in - match Control.case try_set with - | Init.Val pair => let (a, _) := pair in a - | Init.Err e => traverse_thunk' (fun () => c_p e) - end) - end - | Init.Err e => fail - end in traverse_thunk' subterm_stream. + "Variable, skipping this pattern match.")))) + else + let h := Fresh.in_goal @tmpvar in + match Control.case (fun () => (strictset h (fun () => subterm))) with + | Init.Val _ => h :: (hide_SetInPatternRepeat pat) + | Init.Err e => traverse_thunk + (fun () => c_p + (Init.Tactic_failure (Init.Some (Message.of_string + "set failed to modify the goal.")))) + end + end + | Init.Err e => [] + end in traverse_thunk subterm_stream. + +(* "Opaque" all typing annotations to morphism composition, i.e. + replace "compose cat dom cod f g" with "compose var1 var2 var3 f g" *) +Ltac2 hide_compose() := + List.append (hide_SetInPatternRepeat pat:(@compose ?a)) + (List.append (hide_SetInPatternRepeat pat:(@compose _ ?a)) + (List.append (hide_SetInPatternRepeat pat:(@compose _ _ ?a)) + (hide_SetInPatternRepeat pat:(@compose _ _ _ ?a)))). +(* "Opaque" annotations to the setoid structure on homsets, i.e. + replace "equiv _ (homset cat dom cod)" with "equiv _ (homset var1 var2 var3)" *) +Ltac2 hide_homset() := + List.append (hide_SetInPatternRepeat pat:(@homset ?a)) + (List.append (hide_SetInPatternRepeat pat:(@homset _ ?a)) + (hide_SetInPatternRepeat pat:(@homset _ _ ?a))). +(* @fst X Y pair => @fst var1 var2 pair, @snd X Y pair => @snd var1 var2 pair *) +Ltac2 hide_fstsnd() := + List.append (hide_SetInPatternRepeat pat:(@fst ?a)) + (List.append (hide_SetInPatternRepeat pat:(@fst _ ?a)) + (List.append (hide_SetInPatternRepeat pat:(@snd ?a)) + (hide_SetInPatternRepeat pat:(@snd _ ?a)))). + +(* This function takes in a list of identifiers, unfolds them everywhere they occur, + and clears them. + For convenience of application, the list is reversed inside the function + before it is unfolded. Thus if you do: + set (a := ..); set (b := fa); + unfold_and_clear (a :: b :: []) + b will be unfolded first, and then a, + so that no mentions of a occur in the goal afterward and "clear" + can successfully remove it. +*) +Ltac2 unfold_and_clear ll := + Std.unfold (List.map (fun z => (Std.VarRef z, Std.AllOccurrences)) (List.rev ll)) + { Std.on_hyps := Init.None ; Std.on_concl := Std.AllOccurrences }; + Std.clear ll. Theorem ψ_φ_equiv : ∀ x, snd (from (κ E x)) @@ -312,37 +321,31 @@ Proof. (* Tactic call ran for 0.474 secs (0.472u,0.s) (success) *) (* Each pattern corresponds to a subterm of the goal which will be "hidden" from the tactic. - Equivalent to: - set (j1 := snd _); - set (J2 := snd _); - set (j3 := fmap[F] _); - set (j4 := fmap[F] _); - match goal with - | [ |- context[@compose _ ?z]] => set (j5 := z) - end ; + Equivalent to something like + repeat (set (freshvar := snd _)); + repeat (set (freshvar := fmap[F] _)); + repeat(match goal with + | [ |- context[@compose _ ?z]] => set (freshvar := z) + end) match goal with | [ |- context[@compose _ ?z]] => set (j6 := z) end ; + (...) rewrite <- ! comp_assoc; - ... - unfold j3; clear j3; - unfold j2; clear j2; - unfold j1; clear j1 *) - time(ltac2:(hide ( - SetPattern (fun () => '(snd _)) :: - SetPattern (fun () => '(`2 _)) :: - SetPattern (fun () => '(fmap[F] _)) :: - SetPattern (fun () => '(fmap[F] _)) :: - SetInPattern pat:(@compose _ ?z) :: - SetInPattern pat:(@compose _ ?z) :: - SetInPattern pat:(@compose _ ?z) :: - []) (fun () => ltac1:(rewrite <- ! comp_assoc)))). - - (* Tactic call ran for 0.069 secs (0.069u,0.s) (success) *) - - - (* I am trying to workshop a design pattern for doing this kind of - thing efficiently. This is what I have come up with so far. *) + unfold freshvar7, freshvar6, freshvar 5.... + clear freshvar1 freshvar2 ... + *) + time(ltac2:(let ll := + List.concat ( + (hide_SetPatternRepeat (fun () => '(snd _))) :: + (hide_SetPattern_ntimes (fun () => '(`2 _)) 1) :: + (hide_SetPatternRepeat (fun () => '(fmap[F] _))) :: + hide_compose() :: []) in + ltac1:(rewrite <- ! comp_assoc); + unfold_and_clear ll + )). + + (* Suggested design pattern *) (* First, get the equation you are rewriting with in the context. *) match goal with | |- context[ fmap[F] ?f1' ∘ fmap[F] ?g1' ] => @@ -353,6 +356,8 @@ Proof. same variable as the term we want to rewrite. This ensures that no simplifications we make to the goal will prevent the rewrite from succeeding because it can no longer identify the terms we wanted to rewrite. + Then revert M so that all masking simplifications in the goal also affect the + rewrite equation. The "context" operator in the goal helps us in the event that "set" is unable to capture both the LHS of M and the term to be rewritten. @@ -387,16 +392,14 @@ Proof. fmap_respects c d : forall f, g : hom c d, f ≈ g -> F f ≈ F g, it would be possible to opaque the arguments c and d without the typeclass resolution algorithm getting held up by this. - Thus we can safely call - ltac2:(hide1 pat:(@homset ?A)) - opaque the category - ltac2:(hide1 pat:(@homset _ ?A)) - opaque the domain - ltac2:(hide1 pat:(@homset _ _ ?A)) - opaque the codomain. + Thus the function "hide_homset" which "opaques" all matches for + @hide_homset ?cat, @hide_homset _ ?dom, @hide_homset _ _ ?cod. 5. Another example of 4, by the definition of prod_setoid, if f ≈ f' and g ≈ g' then (f, f') ≈ (g, g'). But the types of f,g and f' g' need not be fed to the typeclass resolution algorithm concretely, just the setoid structures. The type of f and g can be opaqued, i.e., - ltac2:(hide1 pat:(@prod_setoid ?A)) - ltac2:(hide1 pat:(@prod_setoid _ ?B)) + hide_SetInPatternRepeat pat:(@prod_setoid ?X) + hide_SetInPatternRepeat pat:(@prod_setoid _ ?Y) 6. In fmap, the domain and codomain of the source morphism can be opaqued. 7. As a general rule if all objects are fixed, and the computation is only on morphisms, then we can opaque the objects. Thus @@ -405,17 +408,19 @@ Proof. A possible future direction might be to assemble a list of such parameters which are unlikely to play a role in typeclass resolution and write an automated script that "opaques" all terms in the goal which seem irrelevant to the rewrite. + The functions hide_homset, hide_compose and hide_fstsnd + are first steps in this direction. *) - time(ltac2:(hide( - SetPattern(fun () => '(fmap[F] _)) :: - SetPattern(fun () => '(snd _)) :: - SetPattern(fun () => '(snd _)) :: - SetPattern(fun () => '(`2 _)) :: - SetInPattern pat:(@compose _ ?a) :: - SetInPattern pat:(@compose _ _ ?a) :: - SetInPattern pat:(@homset _ _ ?a) :: - []) (fun () => ltac1:(intro M; rewrite M; clear M)))). - (* 0.049 secs *) + ltac2:(let ll := + List.concat( + (hide_SetPattern_ntimes (fun () => '(fmap[F] _)) 1) :: + (hide_SetPattern_ntimes (fun () => '(snd _)) 2) :: + (hide_SetPattern_ntimes (fun () => '(`2 _)) 1) :: + (hide_compose()) :: + (hide_SetInPattern_ntimes pat:(@homset _ _ ?a) 1) + :: []) in + ltac1:(intro M; rewrite M; clear M); + unfold_and_clear ll). unfold f1, g1, j1; clear f1 g1 j1. (* 0.15 secs *) @@ -428,96 +433,77 @@ Proof. (* Another instance of this technique / pattern. *) assert (M := η_θ_κ ((a, b); f)). + (* rewrite <- M; clear M. 1.03 secs *) match goal with | [ h : ?a ≈ ?b |- context[ fst ?c ] ] => set (j1 := a) in *; set (j2 := b) in * ; change c with j2; revert M - end. - time(ltac2:(hide( - SetInPattern pat:( _ -> ?a ∘ _ ≈ f) :: - SetPattern (fun () => '(`2 _)) :: - SetInPattern pat:(@hom _ ?a) :: - SetInPattern pat:(@hom _ ?a) :: - SetInPattern pat:(@hom _ ?a) :: - SetInPattern pat:(@hom _ ?a) :: - SetInPattern pat:(@hom _ ?a) :: - SetInPattern pat:(@hom _ _ ?a) :: - SetInPattern pat:(@hom _ _ ?a) :: - SetInPattern pat:(@hom _ _ ?a) :: - SetInPattern pat:(@hom _ _ ?a) :: - SetInPattern pat:(@compose _ _ ?a) :: - SetInPattern pat:(@compose _ _ ?a) :: - SetInPattern pat:(@prod_setoid _ ?a) :: - SetInPattern pat:(@prod_setoid _ _ ?a) :: - []) (fun () => intro M; rewrite <- M; clear M))). - (* It is clear that this process could be more automated, - for example by giving an option to repeating "hide" for each - pattern application until it fails and new variables cannot be introduced. *) - unfold j1, j2; clear j1 j2. - - (* We will repeat this for each rewrite step in the proof. *) - - time(assert (M := (`2 (η E ((a, b); f)))); simpl in M; - match goal with - | [h : ?a ≈ ?b |- context[(snd _) ∘ ?c ≈ f] ] => - set (j1 := a) in *; set (j2 := b) in *; change c with j1 end; - ltac2:(hide ( - SetInPattern pat:(?a ∘ _) :: - SetInPattern pat:(@compose _ ?a) :: - SetInPattern pat:(@compose _ _ ?a) :: - []) (fun () => ltac1:(rewrite M; clear M))); - unfold j1, j2; clear). - - - assert (M := η_θ_κ ((a, b); f)); + ltac2:(let ll := List.concat + ((hide_SetInPattern_ntimes pat:( _ -> ?a ∘ _ ≈ f) 1) :: + (hide_SetPattern_ntimes (fun () => '(`2 _)) 1) :: + (hide_SetInPatternRepeat pat:(@hom _ ?a)) :: + (hide_SetInPatternRepeat pat:(@hom _ _ ?a)) :: + hide_compose () :: + (hide_SetInPatternRepeat pat:(@prod_setoid _ ?a)) :: + (hide_SetInPatternRepeat pat:(@prod_setoid _ _ ?a)) :: + (hide_SetInPatternRepeat pat:(@fmap _ _ F _ ?a)) :: + []) in + ltac1:(intro M; rewrite <- M; clear M); + unfold_and_clear ll + ); unfold j1, j2; clear j1 j2. + + (* We will repeat this for each rewrite step in the proof. *) + assert (M := (`2 (η E ((a, b); f)))); + cbn beta in M; + match goal with + | [h : ?a ≈ ?b |- context[(snd _) ∘ ?c ≈ f] ] => + set (j1 := a) in M; set (j2 := b) in M; change c with j1 + end; cbn in j2; revert M; + ltac2:(let ll := List.concat( + (hide_SetInPatternRepeat pat:(?a ∘ _)) :: + (hide_compose()) :: + (hide_homset()) + :: []) in ltac1:(intro M; rewrite M; clear M) ; + unfold_and_clear ll); + unfold j1, j2; clear. + + assert (M := η_θ_κ ((a, b); f)); match goal with | [ h : ?a ≈ ?b |- _ ∘ (snd ?c ∘ _) ≈ f ] => set (j1 := a) in *; set (j2 := b) in *; change c with j1; revert M end; - ltac2:(hide( - SetInPattern pat:( _ → ?a ∘ _ ≈ _) :: - SetInPattern pat:(@compose _ ?a) :: - SetInPattern pat:(@compose _ ?a) :: - SetInPattern pat:(@compose _ _ ?a) :: - SetInPattern pat:(@compose _ _ ?a) :: - SetInPattern pat:(@compose _ _ _ ?a) :: - SetInPattern pat:(@snd ?a) :: - SetInPattern pat:(@snd ?a) :: - SetInPattern pat:(@snd _ ?b) :: - SetInPattern pat:(@snd _ ?b) :: - SetInPattern pat:(@hom _ ?b) :: - SetInPattern pat:(@hom _ _ ?b) :: - SetInPattern pat:(@prod_setoid ?a) :: - SetInPattern pat:(@prod_setoid _ ?b) :: - []) (fun () => ltac1:(intro M; rewrite M; clear M))); - unfold j1, j2; clear j1 j2. - - time(ltac2:(hide( - SetPattern (fun () => '(snd _)) :: - SetPattern (fun () => '(snd _)) :: - SetPattern (fun () => '(snd _)) :: - SetInPattern pat:(@compose _ ?a) :: - [] ) (fun () => ltac1:(rewrite comp_assoc)))). + ltac2:(let ll := List.concat( + (hide_SetInPattern_ntimes pat:( _ → ?a ∘ _ ≈ _) 1) :: + hide_compose() :: + hide_SetInPatternRepeat pat:(@snd ?a) :: + hide_SetInPatternRepeat pat:(@snd _ ?a) :: + hide_SetInPatternRepeat pat:(@hom _ ?a) :: + hide_SetInPatternRepeat pat:(@hom _ _ ?a) :: + hide_SetInPatternRepeat pat:(@prod_setoid ?a) :: + hide_SetInPatternRepeat pat:(@prod_setoid _ ?a) :: + [] ) in + ltac1:(intro M; rewrite M; clear M); unfold_and_clear ll); + unfold j1, j2; clear j1 j2. + + ltac2:(let ll := List.concat( + hide_SetPatternRepeat (fun () => '(snd _)) :: + hide_compose() :: + []) in ltac1:(rewrite comp_assoc); unfold_and_clear ll). change (snd ((κ E _)⁻¹ ∘ (θ E (φ E _))⁻¹) ∘ snd _) with (snd ( (κ E ((a, b); f))⁻¹ ∘ (θ E (fobj[φ E] ((a, b); f)))⁻¹ ∘ (θ E (fobj[φ E] ((a, b); f)) ∘ κ E ((a, b); f)))). - match goal with | [ |- context[?f1' ∘ ?f2' ∘ ?f3'] ] => set (f1 := f1'); set (f2 := f2'); set (f3 := f3'); assert (M := comp_assoc f1 f2 f3); revert M; set (j2 := f1 ∘ f2 ∘ f3) in * end; - ltac2:(hide( - SetInPattern pat:(@snd _ ?a) :: - SetInPattern pat:(@snd _ ?a) :: - SetInPattern pat:(@compose ?a) :: - SetInPattern pat:(@compose _ ?a) :: - SetInPattern pat:(@compose _ _ ?a) :: - SetInPattern pat:(@compose _ _ ?a) :: - []) (fun () => ltac1:(intro M; rewrite <- M; clear M))); + ltac2:(let ll := List.append + (hide_SetInPatternRepeat pat:(@snd _ ?a)) + (hide_compose()) in + ltac1:(intro M; rewrite <- M; clear M); unfold_and_clear ll); unfold j2, f3, f2, f1; clear. match goal with @@ -530,44 +516,31 @@ Proof. | [ h : ?a ≈ ?b |- snd (_ ∘ ?x) ∘ f ≈ f ] => change x with j1 end; revert M; - ltac2:(hide( - SetPattern (fun () => '(from _)) :: - SetInPattern pat:(@snd ?a) :: - SetInPattern pat:(@snd ?a) :: - SetInPattern pat:(@snd _ ?b) :: - SetInPattern pat:(@snd _ ?b) :: - SetInPattern pat:(@compose ?c) :: - SetInPattern pat:(@compose _ ?c) :: - SetInPattern pat:(@compose _ ?c) :: - SetInPattern pat:(@compose _ ?c) :: - SetInPattern pat:(@compose _ _ ?c) :: - SetInPattern pat:(@compose _ _ ?c) :: - []) (fun () => ltac1:(intro M; rewrite M; clear M))); - unfold f1, f2, f3, j1; clear. + ltac2:(let ll := List.concat( + (hide_SetPatternRepeat (fun () => '(from _))) :: + (hide_SetInPatternRepeat pat:(@snd ?a)) :: + (hide_SetInPatternRepeat pat:(@snd _ ?a)) :: + (hide_compose()) :: []) in + ltac1:(intro M; rewrite M; clear M); unfold_and_clear ll); + unfold f3, f2, f1; clear. match goal with | [ |- context[from ?f1' ∘ to ?f1'] ] => set (f1 := f1') - end. - assert (M := iso_from_to f1). + end; + assert (M := iso_from_to f1); match goal with | [ h : ?a ≈ ?b |- _ ] => set (j1 := a) in * - end. - revert M. - - ltac2:(hide( - SetInPattern pat:(snd (?a ∘ _) ∘ _) :: - SetInPattern pat:(snd (_ ∘ (_ ∘ ?b))) :: - SetInPattern pat:(@compose ?a) :: - SetInPattern pat:(@compose _ ?a) :: - SetInPattern pat:(@compose _ ?a) :: - SetInPattern pat:(@compose _ _ ?a) :: - SetInPattern pat:(@compose _ _ ?a) :: - SetInPattern pat:(@snd ?a) :: - SetInPattern pat:(@snd ?a) :: - SetInPattern pat:(@snd _ ?a) :: - []) (fun () => ltac1:(intro M; rewrite M; clear M))); + end; + revert M; + ltac2:(let ll := List.concat( + hide_SetInPattern_ntimes pat:(snd (?a ∘ _) ∘ _) 1 :: + hide_SetInPattern_ntimes pat:(snd (_ ∘ (_ ∘ ?b))) 1 :: + hide_compose() :: + hide_SetInPatternRepeat pat:(@snd ?a) :: + hide_SetInPatternRepeat pat:(@snd _ ?a) :: []) + in ltac1:(intro M; rewrite M; clear M); unfold_and_clear ll); unfold j1, f1; clear j1 f1. - + match goal with | [ |- context[ id ∘ ?f1' ] ] => assert (M := id_left f1'); set (f1 := f1') in *; set (j1 := id ∘ f1) in * @@ -576,34 +549,29 @@ Proof. | [ |- snd (_ ∘ ?a) ∘ _ ≈ _ ] => change a with j1 end; revert M; - ltac2:(hide( - SetInPattern pat:(@snd ?a) :: - SetInPattern pat:(@snd ?a) :: - SetInPattern pat:(@snd _ ?a) :: - SetInPattern pat:(@compose ?a) :: - SetInPattern pat:(@compose _ ?a) :: - SetInPattern pat:(@compose _ ?a) :: - SetInPattern pat:(@compose _ _ ?a) :: - []) (fun () => ltac1:(intro M; rewrite M; clear M))); - unfold j1, f1; clear j1 f1. + ltac2:(let ll := List.concat( + hide_fstsnd() :: + hide_compose() :: + hide_SetPattern_ntimes (fun () => '(from _)) 1 :: + []) in + ltac1:(intro M; rewrite M; clear M); unfold_and_clear ll); + unfold f1, j1; clear f1 j1. match goal with | [ |- context[from ?f1' ∘ to ?f1'] ] => set (f1 := f1') - end. - assert (M := iso_from_to f1). + end; + assert (M := iso_from_to f1); match goal with | [ h : ?a ≈ ?b |- _ ] => set (j1 := a) in * - end. - revert M. - ltac2:(hide( - SetInPattern pat:(@snd ?a) :: - SetInPattern pat:(@snd ?a) :: - SetInPattern pat:(@snd _ ?a) :: - SetInPattern pat:(@snd _ ?a) :: - SetInPattern pat:(@compose _ ?a) :: - []) (fun () => ltac1:(intro M; rewrite M; clear M))); - unfold j1, f1; clear j1 f1. - simpl. + end; + revert M; + ltac2:(let ll := List.concat( + hide_fstsnd() :: + hide_compose() :: + []) in + ltac1:(intro M; rewrite M; clear M); unfold_and_clear ll); + unfold f1, j1; clear f1 j1. + exact (id_left f). Qed.